8. Isar - A Language for Structured Proofs Flashcards
1
Q
What does a typical Isar proof look like?
A
proof
assume formula_0
have formula_1 by simp
….
have formula_n by blast
show formula_n+1 by …
qed
2
Q
What is the proof pattern for case distinction?
A
3
Q
What is the proof pattern for contradiction?
A
4
Q
What is the proof pattern for iff?
A
5
Q
What is the proof pattern for universal quantification?
A
6
Q
What is the proof pattern for existential quantificiation?
A
7
Q
What is the proof pattern for existential elimination?
A
8
Q
What is the proof pattern for set equaility?
A
9
Q
What is the proof pattern for subset?
A
