Stream: Beginner Questions

Topic: Using rule in isar proofs to setup assumptions

Joshua von Mutius (Nov 05 2020 at 11:15):

Is there a way to use rule in an isar proof

proof(rule myrule)
assume "P"
show "Q"
qed

such that one has not to specify P and Q explicitly?

E.g. when using the proof pattern for a proof by contradiction

proof(rule ccontr)
assume "foo"
show "False" ...
qed

I would like something like:

proof(rule ccontr)
assume  ?bot_assm
show "False" ...
qed

where ?bot_assm = "foo" is automatically specified.
At best i would like to also switch out show "False" ... with something like show ?thesis ....

Mathias Fleury (Nov 05 2020 at 11:17):

for rule ccontr , you can use\<not> ?thesis

Mathias Fleury (Nov 05 2020 at 11:20):

Is goal_cases the tactic you want?

Mathias Fleury (Nov 05 2020 at 11:20):

proof(rule ccontr, goal_cases)
case 1
show "?thesis" ...
qed

Joshua von Mutius (Nov 05 2020 at 11:25):

Yes that is exactly what i was searching for thank you very much!

Last updated: Oct 29 2025 at 16:29 UTC