# HG changeset patch # User wenzelm # Date 931948092 -7200 # Node ID 8121e11ed765b6fbe27969e1964f6151d421b0f5 # Parent 6920cf9b8623c5ee4c2f14f5b883eee2bade8d80 Deriving rules in Isabelle; diff -r 6920cf9b8623 -r 8121e11ed765 src/HOL/Isar_examples/BasicLogic.thy --- a/src/HOL/Isar_examples/BasicLogic.thy Wed Jul 14 10:41:33 1999 +0200 +++ b/src/HOL/Isar_examples/BasicLogic.thy Wed Jul 14 12:28:12 1999 +0200 @@ -8,6 +8,9 @@ theory BasicLogic = Main:; +text {* Just a few tiny examples to get an idea of how Isabelle/Isar + proof documents may look like. *}; + lemma I: "A --> A"; proof; assume A; @@ -24,7 +27,7 @@ qed; lemma K': "A --> B --> A"; -proof single*; +proof single+; txt {* better use sufficient-to-show here \dots *}; assume A; show A; .; qed; @@ -48,6 +51,8 @@ qed; +text {* Variations of backward vs.\ forward reasonong \dots *}; + lemma "A & B --> B & A"; proof; assume "A & B"; @@ -77,7 +82,9 @@ qed; -text {* propositional proof (from 'Introduction to Isabelle') *}; +section {* Examples from 'Introduction to Isabelle' *}; + +text {* 'Propositional proof' *}; lemma "P | P --> P"; proof; @@ -97,7 +104,7 @@ qed; -text {* quantifier proof (from 'Introduction to Isabelle') *}; +text {* 'Quantifier proof' *}; lemma "(EX x. P(f(x))) --> (EX x. P(x))"; proof; @@ -125,4 +132,28 @@ by blast; +subsection {* 'Deriving rules in Isabelle' *}; + +text {* We derive the conjunction elimination rule from the + projections. The proof below follows the basic reasoning of the + script given in the Isabelle Intro Manual closely. Although, the + actual underlying operations on rules and proof states are quite + different: Isabelle/Isar supports non-atomic goals and assumptions + fully transparently, while the original Isabelle classic script + depends on the primitive goal command to decompose the rule into + premises and conclusion, with the result emerging by discharging the + context again later. *}; + +theorem conjE: "A & B ==> (A ==> B ==> C) ==> C"; +proof same; + assume ab: "A & B"; + assume ab_c: "A ==> B ==> C"; + show C; + proof (rule ab_c); + from ab; show A; ..; + from ab; show B; ..; + qed; +qed; + + end;