Stream: Beginner Questions

Topic: note in apply script

Jan van Brügge (Dec 07 2023 at 16:11):

Hi, is it somehow possible to use note foo = bar within an apply script or somehow give names to theorems that use local facts without going into an Isar proof?

Mathias Fleury (Dec 07 2023 at 16:19):

like this?

lemma ‹P ⟹ F ⟶ F›
  subgoal premises p
    supply H = p
    using p
    thm H

Mathias Fleury (Dec 07 2023 at 16:19):

subgoal has some side-effects however

Jan van Brügge (Dec 07 2023 at 16:20):

oh, I did not know that supply could be used this way. That's exactly what I wanted

Mathias Fleury (Dec 07 2023 at 16:20):

schematic_goal ‹?p›
  subgoal premises p
  (*?p is now p and cannot be instantiated anymore*)

Jan van Brügge (Dec 07 2023 at 16:21):

yeah, in my case I don't even need the subgoal, the local facts are already Isar-style assumptions

Last updated: Apr 28 2024 at 04:17 UTC