src/FOLP/ex/Intro.thy
changeset 36319 8feb2c4bef1a
parent 35762 af3ff2ba4c54
child 41526 54b4686704af
     1.1 --- a/src/FOLP/ex/Intro.thy	Fri Apr 23 23:33:48 2010 +0200
     1.2 +++ b/src/FOLP/ex/Intro.thy	Fri Apr 23 23:35:43 2010 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5  subsubsection {* Some simple backward proofs *}
     1.6  
     1.7 -lemma mythm: "?p : P|P --> P"
     1.8 +schematic_lemma mythm: "?p : P|P --> P"
     1.9  apply (rule impI)
    1.10  apply (rule disjE)
    1.11  prefer 3 apply (assumption)
    1.12 @@ -21,7 +21,7 @@
    1.13  apply assumption
    1.14  done
    1.15  
    1.16 -lemma "?p : (P & Q) | R --> (P | R)"
    1.17 +schematic_lemma "?p : (P & Q) | R --> (P | R)"
    1.18  apply (rule impI)
    1.19  apply (erule disjE)
    1.20  apply (drule conjunct1)
    1.21 @@ -31,7 +31,7 @@
    1.22  done
    1.23  
    1.24  (*Correct version, delaying use of "spec" until last*)
    1.25 -lemma "?p : (ALL x y. P(x,y)) --> (ALL z w. P(w,z))"
    1.26 +schematic_lemma "?p : (ALL x y. P(x,y)) --> (ALL z w. P(w,z))"
    1.27  apply (rule impI)
    1.28  apply (rule allI)
    1.29  apply (rule allI)
    1.30 @@ -43,13 +43,13 @@
    1.31  
    1.32  subsubsection {* Demonstration of @{text "fast"} *}
    1.33  
    1.34 -lemma "?p : (EX y. ALL x. J(y,x) <-> ~J(x,x))
    1.35 +schematic_lemma "?p : (EX y. ALL x. J(y,x) <-> ~J(x,x))
    1.36          -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))"
    1.37  apply (tactic {* fast_tac FOLP_cs 1 *})
    1.38  done
    1.39  
    1.40  
    1.41 -lemma "?p : ALL x. P(x,f(x)) <->
    1.42 +schematic_lemma "?p : ALL x. P(x,f(x)) <->
    1.43          (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
    1.44  apply (tactic {* fast_tac FOLP_cs 1 *})
    1.45  done
    1.46 @@ -57,7 +57,7 @@
    1.47  
    1.48  subsubsection {* Derivation of conjunction elimination rule *}
    1.49  
    1.50 -lemma
    1.51 +schematic_lemma
    1.52    assumes major: "p : P&Q"
    1.53      and minor: "!!x y. [| x : P; y : Q |] ==> f(x, y) : R"
    1.54    shows "?p : R"
    1.55 @@ -71,7 +71,7 @@
    1.56  
    1.57  text {* Derivation of negation introduction *}
    1.58  
    1.59 -lemma
    1.60 +schematic_lemma
    1.61    assumes "!!x. x : P ==> f(x) : False"
    1.62    shows "?p : ~ P"
    1.63  apply (unfold not_def)
    1.64 @@ -80,7 +80,7 @@
    1.65  apply assumption
    1.66  done
    1.67  
    1.68 -lemma
    1.69 +schematic_lemma
    1.70    assumes major: "p : ~P"
    1.71      and minor: "q : P"
    1.72    shows "?p : R"
    1.73 @@ -91,7 +91,7 @@
    1.74  done
    1.75  
    1.76  text {* Alternative proof of the result above *}
    1.77 -lemma
    1.78 +schematic_lemma
    1.79    assumes major: "p : ~P"
    1.80      and minor: "q : P"
    1.81    shows "?p : R"