mark schematic statements explicitly;
authorwenzelm
Fri Apr 23 23:35:43 2010 +0200 (2010-04-23)
changeset 363198feb2c4bef1a
parent 36318 3567d0571932
child 36320 549be64e890f
mark schematic statements explicitly;
src/CCL/Fix.thy
src/CCL/Wfd.thy
src/CTT/Arith.thy
src/CTT/ex/Elimination.thy
src/CTT/ex/Synthesis.thy
src/CTT/ex/Typechecking.thy
src/Cube/Example.thy
src/FOL/ex/Classical.thy
src/FOL/ex/Prolog.thy
src/FOL/ex/Quantifiers_Cla.thy
src/FOL/ex/Quantifiers_Int.thy
src/FOLP/FOLP.thy
src/FOLP/IFOLP.thy
src/FOLP/ex/Classical.thy
src/FOLP/ex/Foundation.thy
src/FOLP/ex/If.thy
src/FOLP/ex/Intro.thy
src/FOLP/ex/Intuitionistic.thy
src/FOLP/ex/Nat.thy
src/FOLP/ex/Propositional_Cla.thy
src/FOLP/ex/Propositional_Int.thy
src/FOLP/ex/Quantifiers_Cla.thy
src/FOLP/ex/Quantifiers_Int.thy
src/HOL/Bali/Example.thy
src/HOL/Lambda/Type.thy
src/HOL/MicroJava/J/Example.thy
src/HOL/Nitpick_Examples/Core_Nits.thy
src/HOL/Nitpick_Examples/Refute_Nits.thy
src/HOL/Prolog/Func.thy
src/HOL/Prolog/Test.thy
src/HOL/Prolog/Type.thy
src/HOL/ex/Classical.thy
src/HOL/ex/Groebner_Examples.thy
src/HOL/ex/Refute_Examples.thy
src/HOL/ex/set.thy
src/Sequents/LK/Quantifiers.thy
src/ZF/AC/Cardinal_aux.thy
src/ZF/Constructible/Reflection.thy
     1.1 --- a/src/CCL/Fix.thy	Fri Apr 23 23:33:48 2010 +0200
     1.2 +++ b/src/CCL/Fix.thy	Fri Apr 23 23:35:43 2010 +0200
     1.3 @@ -98,7 +98,7 @@
     1.4  
     1.5  (* All fixed points are lam-expressions *)
     1.6  
     1.7 -lemma idgenfp_lam: "idgen(d) = d ==> d = lam x. ?f(x)"
     1.8 +schematic_lemma idgenfp_lam: "idgen(d) = d ==> d = lam x. ?f(x)"
     1.9    apply (unfold idgen_def)
    1.10    apply (erule ssubst)
    1.11    apply (rule refl)
    1.12 @@ -130,7 +130,7 @@
    1.13    apply simp
    1.14    done
    1.15  
    1.16 -lemma po_eta_lemma: "idgen(d) = d ==> d = lam x. ?f(x)"
    1.17 +schematic_lemma po_eta_lemma: "idgen(d) = d ==> d = lam x. ?f(x)"
    1.18    apply (unfold idgen_def)
    1.19    apply (erule sym)
    1.20    done
     2.1 --- a/src/CCL/Wfd.thy	Fri Apr 23 23:33:48 2010 +0200
     2.2 +++ b/src/CCL/Wfd.thy	Fri Apr 23 23:35:43 2010 +0200
     2.3 @@ -573,29 +573,29 @@
     2.4  
     2.5  subsection {* Factorial *}
     2.6  
     2.7 -lemma
     2.8 +schematic_lemma
     2.9    "letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h))))  
    2.10     in f(succ(succ(zero))) ---> ?a"
    2.11    by eval
    2.12  
    2.13 -lemma
    2.14 +schematic_lemma
    2.15    "letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h))))  
    2.16     in f(succ(succ(succ(zero)))) ---> ?a"
    2.17    by eval
    2.18  
    2.19  subsection {* Less Than Or Equal *}
    2.20  
    2.21 -lemma
    2.22 +schematic_lemma
    2.23    "letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>))))
    2.24     in f(<succ(zero), succ(zero)>) ---> ?a"
    2.25    by eval
    2.26  
    2.27 -lemma
    2.28 +schematic_lemma
    2.29    "letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>))))
    2.30     in f(<succ(zero), succ(succ(succ(succ(zero))))>) ---> ?a"
    2.31    by eval
    2.32  
    2.33 -lemma
    2.34 +schematic_lemma
    2.35    "letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>))))
    2.36     in f(<succ(succ(succ(succ(succ(zero))))), succ(succ(succ(succ(zero))))>) ---> ?a"
    2.37    by eval
    2.38 @@ -603,12 +603,12 @@
    2.39  
    2.40  subsection {* Reverse *}
    2.41  
    2.42 -lemma
    2.43 +schematic_lemma
    2.44    "letrec id l be lcase(l,[],%x xs. x$id(xs))  
    2.45     in id(zero$succ(zero)$[]) ---> ?a"
    2.46    by eval
    2.47  
    2.48 -lemma
    2.49 +schematic_lemma
    2.50    "letrec rev l be lcase(l,[],%x xs. lrec(rev(xs),x$[],%y ys g. y$g))  
    2.51     in rev(zero$succ(zero)$(succ((lam x. x)`succ(zero)))$([])) ---> ?a"
    2.52    by eval
     3.1 --- a/src/CTT/Arith.thy	Fri Apr 23 23:33:48 2010 +0200
     3.2 +++ b/src/CTT/Arith.thy	Fri Apr 23 23:35:43 2010 +0200
     3.3 @@ -256,7 +256,8 @@
     3.4  (*Addition is the inverse of subtraction: if b<=x then b#+(x-b) = x.
     3.5    An example of induction over a quantified formula (a product).
     3.6    Uses rewriting with a quantified, implicative inductive hypothesis.*)
     3.7 -lemma add_diff_inverse_lemma: "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)"
     3.8 +schematic_lemma add_diff_inverse_lemma:
     3.9 +  "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)"
    3.10  apply (tactic {* NE_tac @{context} "b" 1 *})
    3.11  (*strip one "universal quantifier" but not the "implication"*)
    3.12  apply (rule_tac [3] intr_rls)
    3.13 @@ -324,7 +325,7 @@
    3.14  done
    3.15  
    3.16  (*If a+b=0 then a=0.   Surprisingly tedious*)
    3.17 -lemma add_eq0_lemma: "[| a:N;  b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) .  Eq(N,a,0)"
    3.18 +schematic_lemma add_eq0_lemma: "[| a:N;  b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) .  Eq(N,a,0)"
    3.19  apply (tactic {* NE_tac @{context} "a" 1 *})
    3.20  apply (rule_tac [3] replace_type)
    3.21  apply (tactic "arith_rew_tac []")
    3.22 @@ -344,7 +345,7 @@
    3.23  done
    3.24  
    3.25  (*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *)
    3.26 -lemma absdiff_eq0_lem:
    3.27 +schematic_lemma absdiff_eq0_lem:
    3.28      "[| a:N;  b:N;  a |-| b = 0 : N |] ==>
    3.29       ?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)"
    3.30  apply (unfold absdiff_def)
     4.1 --- a/src/CTT/ex/Elimination.thy	Fri Apr 23 23:33:48 2010 +0200
     4.2 +++ b/src/CTT/ex/Elimination.thy	Fri Apr 23 23:35:43 2010 +0200
     4.3 @@ -14,41 +14,41 @@
     4.4  
     4.5  text "This finds the functions fst and snd!"
     4.6  
     4.7 -lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
     4.8 +schematic_lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
     4.9  apply (tactic {* pc_tac [] 1 *})
    4.10  done
    4.11  
    4.12 -lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
    4.13 +schematic_lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
    4.14  apply (tactic {* pc_tac [] 1 *})
    4.15  back
    4.16  done
    4.17  
    4.18  text "Double negation of the Excluded Middle"
    4.19 -lemma "A type ==> ?a : ((A + (A-->F)) --> F) --> F"
    4.20 +schematic_lemma "A type ==> ?a : ((A + (A-->F)) --> F) --> F"
    4.21  apply (tactic "intr_tac []")
    4.22  apply (rule ProdE)
    4.23  apply assumption
    4.24  apply (tactic "pc_tac [] 1")
    4.25  done
    4.26  
    4.27 -lemma "[| A type;  B type |] ==> ?a : (A*B) --> (B*A)"
    4.28 +schematic_lemma "[| A type;  B type |] ==> ?a : (A*B) --> (B*A)"
    4.29  apply (tactic "pc_tac [] 1")
    4.30  done
    4.31  (*The sequent version (ITT) could produce an interesting alternative
    4.32    by backtracking.  No longer.*)
    4.33  
    4.34  text "Binary sums and products"
    4.35 -lemma "[| A type; B type; C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)"
    4.36 +schematic_lemma "[| A type; B type; C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)"
    4.37  apply (tactic "pc_tac [] 1")
    4.38  done
    4.39  
    4.40  (*A distributive law*)
    4.41 -lemma "[| A type;  B type;  C type |] ==> ?a : A * (B+C)  -->  (A*B + A*C)"
    4.42 +schematic_lemma "[| A type;  B type;  C type |] ==> ?a : A * (B+C)  -->  (A*B + A*C)"
    4.43  apply (tactic "pc_tac [] 1")
    4.44  done
    4.45  
    4.46  (*more general version, same proof*)
    4.47 -lemma
    4.48 +schematic_lemma
    4.49    assumes "A type"
    4.50      and "!!x. x:A ==> B(x) type"
    4.51      and "!!x. x:A ==> C(x) type"
    4.52 @@ -57,12 +57,12 @@
    4.53  done
    4.54  
    4.55  text "Construction of the currying functional"
    4.56 -lemma "[| A type;  B type;  C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))"
    4.57 +schematic_lemma "[| A type;  B type;  C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))"
    4.58  apply (tactic "pc_tac [] 1")
    4.59  done
    4.60  
    4.61  (*more general goal with same proof*)
    4.62 -lemma
    4.63 +schematic_lemma
    4.64    assumes "A type"
    4.65      and "!!x. x:A ==> B(x) type"
    4.66      and "!!z. z: (SUM x:A. B(x)) ==> C(z) type"
    4.67 @@ -72,12 +72,12 @@
    4.68  done
    4.69  
    4.70  text "Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)"
    4.71 -lemma "[| A type;  B type;  C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)"
    4.72 +schematic_lemma "[| A type;  B type;  C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)"
    4.73  apply (tactic "pc_tac [] 1")
    4.74  done
    4.75  
    4.76  (*more general goal with same proof*)
    4.77 -lemma
    4.78 +schematic_lemma
    4.79    assumes "A type"
    4.80      and "!!x. x:A ==> B(x) type"
    4.81      and "!!z. z: (SUM x:A . B(x)) ==> C(z) type"
    4.82 @@ -87,12 +87,12 @@
    4.83  done
    4.84  
    4.85  text "Function application"
    4.86 -lemma "[| A type;  B type |] ==> ?a : ((A --> B) * A) --> B"
    4.87 +schematic_lemma "[| A type;  B type |] ==> ?a : ((A --> B) * A) --> B"
    4.88  apply (tactic "pc_tac [] 1")
    4.89  done
    4.90  
    4.91  text "Basic test of quantifier reasoning"
    4.92 -lemma
    4.93 +schematic_lemma
    4.94    assumes "A type"
    4.95      and "B type"
    4.96      and "!!x y.[| x:A;  y:B |] ==> C(x,y) type"
    4.97 @@ -103,7 +103,7 @@
    4.98  done
    4.99  
   4.100  text "Martin-Lof (1984) pages 36-7: the combinator S"
   4.101 -lemma
   4.102 +schematic_lemma
   4.103    assumes "A type"
   4.104      and "!!x. x:A ==> B(x) type"
   4.105      and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type"
   4.106 @@ -113,7 +113,7 @@
   4.107  done
   4.108  
   4.109  text "Martin-Lof (1984) page 58: the axiom of disjunction elimination"
   4.110 -lemma
   4.111 +schematic_lemma
   4.112    assumes "A type"
   4.113      and "B type"
   4.114      and "!!z. z: A+B ==> C(z) type"
   4.115 @@ -123,7 +123,7 @@
   4.116  done
   4.117  
   4.118  (*towards AXIOM OF CHOICE*)
   4.119 -lemma [folded basic_defs]:
   4.120 +schematic_lemma [folded basic_defs]:
   4.121    "[| A type; B type; C type |] ==> ?a : (A --> B*C) --> (A-->B) * (A-->C)"
   4.122  apply (tactic "pc_tac [] 1")
   4.123  done
   4.124 @@ -131,7 +131,7 @@
   4.125  
   4.126  (*Martin-Lof (1984) page 50*)
   4.127  text "AXIOM OF CHOICE!  Delicate use of elimination rules"
   4.128 -lemma
   4.129 +schematic_lemma
   4.130    assumes "A type"
   4.131      and "!!x. x:A ==> B(x) type"
   4.132      and "!!x y.[| x:A;  y:B(x) |] ==> C(x,y) type"
   4.133 @@ -149,7 +149,7 @@
   4.134  done
   4.135  
   4.136  text "Axiom of choice.  Proof without fst, snd.  Harder still!"
   4.137 -lemma [folded basic_defs]:
   4.138 +schematic_lemma [folded basic_defs]:
   4.139    assumes "A type"
   4.140      and "!!x. x:A ==> B(x) type"
   4.141      and "!!x y.[| x:A;  y:B(x) |] ==> C(x,y) type"
   4.142 @@ -174,7 +174,7 @@
   4.143  text "Example of sequent_style deduction"
   4.144  (*When splitting z:A*B, the assumption C(z) is affected;  ?a becomes
   4.145      lam u. split(u,%v w.split(v,%x y.lam z. <x,<y,z>>) ` w)     *)
   4.146 -lemma
   4.147 +schematic_lemma
   4.148    assumes "A type"
   4.149      and "B type"
   4.150      and "!!z. z:A*B ==> C(z) type"
     5.1 --- a/src/CTT/ex/Synthesis.thy	Fri Apr 23 23:33:48 2010 +0200
     5.2 +++ b/src/CTT/ex/Synthesis.thy	Fri Apr 23 23:35:43 2010 +0200
     5.3 @@ -10,7 +10,7 @@
     5.4  begin
     5.5  
     5.6  text "discovery of predecessor function"
     5.7 -lemma "?a : SUM pred:?A . Eq(N, pred`0, 0)
     5.8 +schematic_lemma "?a : SUM pred:?A . Eq(N, pred`0, 0)
     5.9                    *  (PROD n:N. Eq(N, pred ` succ(n), n))"
    5.10  apply (tactic "intr_tac []")
    5.11  apply (tactic eqintr_tac)
    5.12 @@ -20,7 +20,7 @@
    5.13  done
    5.14  
    5.15  text "the function fst as an element of a function type"
    5.16 -lemma [folded basic_defs]:
    5.17 +schematic_lemma [folded basic_defs]:
    5.18    "A type ==> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` <i,j>, i)"
    5.19  apply (tactic "intr_tac []")
    5.20  apply (tactic eqintr_tac)
    5.21 @@ -34,7 +34,7 @@
    5.22  text "An interesting use of the eliminator, when"
    5.23  (*The early implementation of unification caused non-rigid path in occur check
    5.24    See following example.*)
    5.25 -lemma "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0    ,   i>)
    5.26 +schematic_lemma "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0    ,   i>)
    5.27                     * Eq(?A, ?b(inr(i)), <succ(0), i>)"
    5.28  apply (tactic "intr_tac []")
    5.29  apply (tactic eqintr_tac)
    5.30 @@ -46,13 +46,13 @@
    5.31   This prevents the cycle in the first unification (no longer needed).
    5.32   Requires flex-flex to preserve the dependence.
    5.33   Simpler still: make ?A into a constant type N*N.*)
    5.34 -lemma "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0   ,   i>)
    5.35 +schematic_lemma "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0   ,   i>)
    5.36                    *  Eq(?A(i), ?b(inr(i)), <succ(0),i>)"
    5.37  oops
    5.38  
    5.39  text "A tricky combination of when and split"
    5.40  (*Now handled easily, but caused great problems once*)
    5.41 -lemma [folded basic_defs]:
    5.42 +schematic_lemma [folded basic_defs]:
    5.43    "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i)
    5.44                             *  Eq(?A, ?b(inr(<i,j>)), j)"
    5.45  apply (tactic "intr_tac []")
    5.46 @@ -65,18 +65,18 @@
    5.47  done
    5.48  
    5.49  (*similar but allows the type to depend on i and j*)
    5.50 -lemma "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i)
    5.51 +schematic_lemma "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i)
    5.52                            *   Eq(?A(i,j), ?b(inr(<i,j>)), j)"
    5.53  oops
    5.54  
    5.55  (*similar but specifying the type N simplifies the unification problems*)
    5.56 -lemma "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)
    5.57 +schematic_lemma "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)
    5.58                            *   Eq(N, ?b(inr(<i,j>)), j)"
    5.59  oops
    5.60  
    5.61  
    5.62  text "Deriving the addition operator"
    5.63 -lemma [folded arith_defs]:
    5.64 +schematic_lemma [folded arith_defs]:
    5.65    "?c : PROD n:N. Eq(N, ?f(0,n), n)
    5.66                    *  (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))"
    5.67  apply (tactic "intr_tac []")
    5.68 @@ -86,7 +86,7 @@
    5.69  done
    5.70  
    5.71  text "The addition function -- using explicit lambdas"
    5.72 -lemma [folded arith_defs]:
    5.73 +schematic_lemma [folded arith_defs]:
    5.74    "?c : SUM plus : ?A .
    5.75           PROD x:N. Eq(N, plus`0`x, x)
    5.76                  *  (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))"
     6.1 --- a/src/CTT/ex/Typechecking.thy	Fri Apr 23 23:33:48 2010 +0200
     6.2 +++ b/src/CTT/ex/Typechecking.thy	Fri Apr 23 23:35:43 2010 +0200
     6.3 @@ -11,18 +11,18 @@
     6.4  
     6.5  subsection {* Single-step proofs: verifying that a type is well-formed *}
     6.6  
     6.7 -lemma "?A type"
     6.8 +schematic_lemma "?A type"
     6.9  apply (rule form_rls)
    6.10  done
    6.11  
    6.12 -lemma "?A type"
    6.13 +schematic_lemma "?A type"
    6.14  apply (rule form_rls)
    6.15  back
    6.16  apply (rule form_rls)
    6.17  apply (rule form_rls)
    6.18  done
    6.19  
    6.20 -lemma "PROD z:?A . N + ?B(z) type"
    6.21 +schematic_lemma "PROD z:?A . N + ?B(z) type"
    6.22  apply (rule form_rls)
    6.23  apply (rule form_rls)
    6.24  apply (rule form_rls)
    6.25 @@ -37,30 +37,30 @@
    6.26  apply (tactic form_tac)
    6.27  done
    6.28  
    6.29 -lemma "<0, succ(0)> : ?A"
    6.30 +schematic_lemma "<0, succ(0)> : ?A"
    6.31  apply (tactic "intr_tac []")
    6.32  done
    6.33  
    6.34 -lemma "PROD w:N . Eq(?A,w,w) type"
    6.35 +schematic_lemma "PROD w:N . Eq(?A,w,w) type"
    6.36  apply (tactic "typechk_tac []")
    6.37  done
    6.38  
    6.39 -lemma "PROD x:N . PROD y:N . Eq(?A,x,y) type"
    6.40 +schematic_lemma "PROD x:N . PROD y:N . Eq(?A,x,y) type"
    6.41  apply (tactic "typechk_tac []")
    6.42  done
    6.43  
    6.44  text "typechecking an application of fst"
    6.45 -lemma "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A"
    6.46 +schematic_lemma "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A"
    6.47  apply (tactic "typechk_tac []")
    6.48  done
    6.49  
    6.50  text "typechecking the predecessor function"
    6.51 -lemma "lam n. rec(n, 0, %x y. x) : ?A"
    6.52 +schematic_lemma "lam n. rec(n, 0, %x y. x) : ?A"
    6.53  apply (tactic "typechk_tac []")
    6.54  done
    6.55  
    6.56  text "typechecking the addition function"
    6.57 -lemma "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A"
    6.58 +schematic_lemma "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A"
    6.59  apply (tactic "typechk_tac []")
    6.60  done
    6.61  
    6.62 @@ -68,18 +68,18 @@
    6.63    For concreteness, every type variable left over is forced to be N*)
    6.64  ML {* val N_tac = TRYALL (rtac (thm "NF")) *}
    6.65  
    6.66 -lemma "lam w. <w,w> : ?A"
    6.67 +schematic_lemma "lam w. <w,w> : ?A"
    6.68  apply (tactic "typechk_tac []")
    6.69  apply (tactic N_tac)
    6.70  done
    6.71  
    6.72 -lemma "lam x. lam y. x : ?A"
    6.73 +schematic_lemma "lam x. lam y. x : ?A"
    6.74  apply (tactic "typechk_tac []")
    6.75  apply (tactic N_tac)
    6.76  done
    6.77  
    6.78  text "typechecking fst (as a function object)"
    6.79 -lemma "lam i. split(i, %j k. j) : ?A"
    6.80 +schematic_lemma "lam i. split(i, %j k. j) : ?A"
    6.81  apply (tactic "typechk_tac []")
    6.82  apply (tactic N_tac)
    6.83  done
     7.1 --- a/src/Cube/Example.thy	Fri Apr 23 23:33:48 2010 +0200
     7.2 +++ b/src/Cube/Example.thy	Fri Apr 23 23:35:43 2010 +0200
     7.3 @@ -30,98 +30,98 @@
     7.4  
     7.5  subsection {* Simple types *}
     7.6  
     7.7 -lemma "A:* |- A->A : ?T"
     7.8 +schematic_lemma "A:* |- A->A : ?T"
     7.9    by (depth_solve rules)
    7.10  
    7.11 -lemma "A:* |- Lam a:A. a : ?T"
    7.12 +schematic_lemma "A:* |- Lam a:A. a : ?T"
    7.13    by (depth_solve rules)
    7.14  
    7.15 -lemma "A:* B:* b:B |- Lam x:A. b : ?T"
    7.16 +schematic_lemma "A:* B:* b:B |- Lam x:A. b : ?T"
    7.17    by (depth_solve rules)
    7.18  
    7.19 -lemma "A:* b:A |- (Lam a:A. a)^b: ?T"
    7.20 +schematic_lemma "A:* b:A |- (Lam a:A. a)^b: ?T"
    7.21    by (depth_solve rules)
    7.22  
    7.23 -lemma "A:* B:* c:A b:B |- (Lam x:A. b)^ c: ?T"
    7.24 +schematic_lemma "A:* B:* c:A b:B |- (Lam x:A. b)^ c: ?T"
    7.25    by (depth_solve rules)
    7.26  
    7.27 -lemma "A:* B:* |- Lam a:A. Lam b:B. a : ?T"
    7.28 +schematic_lemma "A:* B:* |- Lam a:A. Lam b:B. a : ?T"
    7.29    by (depth_solve rules)
    7.30  
    7.31  
    7.32  subsection {* Second-order types *}
    7.33  
    7.34 -lemma (in L2) "|- Lam A:*. Lam a:A. a : ?T"
    7.35 +schematic_lemma (in L2) "|- Lam A:*. Lam a:A. a : ?T"
    7.36    by (depth_solve rules)
    7.37  
    7.38 -lemma (in L2) "A:* |- (Lam B:*.Lam b:B. b)^A : ?T"
    7.39 +schematic_lemma (in L2) "A:* |- (Lam B:*.Lam b:B. b)^A : ?T"
    7.40    by (depth_solve rules)
    7.41  
    7.42 -lemma (in L2) "A:* b:A |- (Lam B:*.Lam b:B. b) ^ A ^ b: ?T"
    7.43 +schematic_lemma (in L2) "A:* b:A |- (Lam B:*.Lam b:B. b) ^ A ^ b: ?T"
    7.44    by (depth_solve rules)
    7.45  
    7.46 -lemma (in L2) "|- Lam B:*.Lam a:(Pi A:*.A).a ^ ((Pi A:*.A)->B) ^ a: ?T"
    7.47 +schematic_lemma (in L2) "|- Lam B:*.Lam a:(Pi A:*.A).a ^ ((Pi A:*.A)->B) ^ a: ?T"
    7.48    by (depth_solve rules)
    7.49  
    7.50  
    7.51  subsection {* Weakly higher-order propositional logic *}
    7.52  
    7.53 -lemma (in Lomega) "|- Lam A:*.A->A : ?T"
    7.54 +schematic_lemma (in Lomega) "|- Lam A:*.A->A : ?T"
    7.55    by (depth_solve rules)
    7.56  
    7.57 -lemma (in Lomega) "B:* |- (Lam A:*.A->A) ^ B : ?T"
    7.58 +schematic_lemma (in Lomega) "B:* |- (Lam A:*.A->A) ^ B : ?T"
    7.59    by (depth_solve rules)
    7.60  
    7.61 -lemma (in Lomega) "B:* b:B |- (Lam y:B. b): ?T"
    7.62 +schematic_lemma (in Lomega) "B:* b:B |- (Lam y:B. b): ?T"
    7.63    by (depth_solve rules)
    7.64  
    7.65 -lemma (in Lomega) "A:* F:*->* |- F^(F^A): ?T"
    7.66 +schematic_lemma (in Lomega) "A:* F:*->* |- F^(F^A): ?T"
    7.67    by (depth_solve rules)
    7.68  
    7.69 -lemma (in Lomega) "A:* |- Lam F:*->*.F^(F^A): ?T"
    7.70 +schematic_lemma (in Lomega) "A:* |- Lam F:*->*.F^(F^A): ?T"
    7.71    by (depth_solve rules)
    7.72  
    7.73  
    7.74  subsection {* LP *}
    7.75  
    7.76 -lemma (in LP) "A:* |- A -> * : ?T"
    7.77 +schematic_lemma (in LP) "A:* |- A -> * : ?T"
    7.78    by (depth_solve rules)
    7.79  
    7.80 -lemma (in LP) "A:* P:A->* a:A |- P^a: ?T"
    7.81 +schematic_lemma (in LP) "A:* P:A->* a:A |- P^a: ?T"
    7.82    by (depth_solve rules)
    7.83  
    7.84 -lemma (in LP) "A:* P:A->A->* a:A |- Pi a:A. P^a^a: ?T"
    7.85 +schematic_lemma (in LP) "A:* P:A->A->* a:A |- Pi a:A. P^a^a: ?T"
    7.86    by (depth_solve rules)
    7.87  
    7.88 -lemma (in LP) "A:* P:A->* Q:A->* |- Pi a:A. P^a -> Q^a: ?T"
    7.89 +schematic_lemma (in LP) "A:* P:A->* Q:A->* |- Pi a:A. P^a -> Q^a: ?T"
    7.90    by (depth_solve rules)
    7.91  
    7.92 -lemma (in LP) "A:* P:A->* |- Pi a:A. P^a -> P^a: ?T"
    7.93 +schematic_lemma (in LP) "A:* P:A->* |- Pi a:A. P^a -> P^a: ?T"
    7.94    by (depth_solve rules)
    7.95  
    7.96 -lemma (in LP) "A:* P:A->* |- Lam a:A. Lam x:P^a. x: ?T"
    7.97 +schematic_lemma (in LP) "A:* P:A->* |- Lam a:A. Lam x:P^a. x: ?T"
    7.98    by (depth_solve rules)
    7.99  
   7.100 -lemma (in LP) "A:* P:A->* Q:* |- (Pi a:A. P^a->Q) -> (Pi a:A. P^a) -> Q : ?T"
   7.101 +schematic_lemma (in LP) "A:* P:A->* Q:* |- (Pi a:A. P^a->Q) -> (Pi a:A. P^a) -> Q : ?T"
   7.102    by (depth_solve rules)
   7.103  
   7.104 -lemma (in LP) "A:* P:A->* Q:* a0:A |-
   7.105 +schematic_lemma (in LP) "A:* P:A->* Q:* a0:A |-
   7.106          Lam x:Pi a:A. P^a->Q. Lam y:Pi a:A. P^a. x^a0^(y^a0): ?T"
   7.107    by (depth_solve rules)
   7.108  
   7.109  
   7.110  subsection {* Omega-order types *}
   7.111  
   7.112 -lemma (in L2) "A:* B:* |- Pi C:*.(A->B->C)->C : ?T"
   7.113 +schematic_lemma (in L2) "A:* B:* |- Pi C:*.(A->B->C)->C : ?T"
   7.114    by (depth_solve rules)
   7.115  
   7.116 -lemma (in Lomega2) "|- Lam A:*.Lam B:*.Pi C:*.(A->B->C)->C : ?T"
   7.117 +schematic_lemma (in Lomega2) "|- Lam A:*.Lam B:*.Pi C:*.(A->B->C)->C : ?T"
   7.118    by (depth_solve rules)
   7.119  
   7.120 -lemma (in Lomega2) "|- Lam A:*.Lam B:*.Lam x:A. Lam y:B. x : ?T"
   7.121 +schematic_lemma (in Lomega2) "|- Lam A:*.Lam B:*.Lam x:A. Lam y:B. x : ?T"
   7.122    by (depth_solve rules)
   7.123  
   7.124 -lemma (in Lomega2) "A:* B:* |- ?p : (A->B) -> ((B->Pi P:*.P)->(A->Pi P:*.P))"
   7.125 +schematic_lemma (in Lomega2) "A:* B:* |- ?p : (A->B) -> ((B->Pi P:*.P)->(A->Pi P:*.P))"
   7.126    apply (strip_asms rules)
   7.127    apply (rule lam_ss)
   7.128      apply (depth_solve1 rules)
   7.129 @@ -145,14 +145,14 @@
   7.130  
   7.131  subsection {* Second-order Predicate Logic *}
   7.132  
   7.133 -lemma (in LP2) "A:* P:A->* |- Lam a:A. P^a->(Pi A:*.A) : ?T"
   7.134 +schematic_lemma (in LP2) "A:* P:A->* |- Lam a:A. P^a->(Pi A:*.A) : ?T"
   7.135    by (depth_solve rules)
   7.136  
   7.137 -lemma (in LP2) "A:* P:A->A->* |-
   7.138 +schematic_lemma (in LP2) "A:* P:A->A->* |-
   7.139      (Pi a:A. Pi b:A. P^a^b->P^b^a->Pi P:*.P) -> Pi a:A. P^a^a->Pi P:*.P : ?T"
   7.140    by (depth_solve rules)
   7.141  
   7.142 -lemma (in LP2) "A:* P:A->A->* |-
   7.143 +schematic_lemma (in LP2) "A:* P:A->A->* |-
   7.144      ?p: (Pi a:A. Pi b:A. P^a^b->P^b^a->Pi P:*.P) -> Pi a:A. P^a^a->Pi P:*.P"
   7.145    -- {* Antisymmetry implies irreflexivity: *}
   7.146    apply (strip_asms rules)
   7.147 @@ -174,22 +174,22 @@
   7.148  
   7.149  subsection {* LPomega *}
   7.150  
   7.151 -lemma (in LPomega) "A:* |- Lam P:A->A->*.Lam a:A. P^a^a : ?T"
   7.152 +schematic_lemma (in LPomega) "A:* |- Lam P:A->A->*.Lam a:A. P^a^a : ?T"
   7.153    by (depth_solve rules)
   7.154  
   7.155 -lemma (in LPomega) "|- Lam A:*.Lam P:A->A->*.Lam a:A. P^a^a : ?T"
   7.156 +schematic_lemma (in LPomega) "|- Lam A:*.Lam P:A->A->*.Lam a:A. P^a^a : ?T"
   7.157    by (depth_solve rules)
   7.158  
   7.159  
   7.160  subsection {* Constructions *}
   7.161  
   7.162 -lemma (in CC) "|- Lam A:*.Lam P:A->*.Lam a:A. P^a->Pi P:*.P: ?T"
   7.163 +schematic_lemma (in CC) "|- Lam A:*.Lam P:A->*.Lam a:A. P^a->Pi P:*.P: ?T"
   7.164    by (depth_solve rules)
   7.165  
   7.166 -lemma (in CC) "|- Lam A:*.Lam P:A->*.Pi a:A. P^a: ?T"
   7.167 +schematic_lemma (in CC) "|- Lam A:*.Lam P:A->*.Pi a:A. P^a: ?T"
   7.168    by (depth_solve rules)
   7.169  
   7.170 -lemma (in CC) "A:* P:A->* a:A |- ?p : (Pi a:A. P^a)->P^a"
   7.171 +schematic_lemma (in CC) "A:* P:A->* a:A |- ?p : (Pi a:A. P^a)->P^a"
   7.172    apply (strip_asms rules)
   7.173    apply (rule lam_ss)
   7.174      apply (depth_solve1 rules)
   7.175 @@ -201,15 +201,15 @@
   7.176  
   7.177  subsection {* Some random examples *}
   7.178  
   7.179 -lemma (in LP2) "A:* c:A f:A->A |-
   7.180 +schematic_lemma (in LP2) "A:* c:A f:A->A |-
   7.181      Lam a:A. Pi P:A->*.P^c -> (Pi x:A. P^x->P^(f^x)) -> P^a : ?T"
   7.182    by (depth_solve rules)
   7.183  
   7.184 -lemma (in CC) "Lam A:*.Lam c:A. Lam f:A->A.
   7.185 +schematic_lemma (in CC) "Lam A:*.Lam c:A. Lam f:A->A.
   7.186      Lam a:A. Pi P:A->*.P^c -> (Pi x:A. P^x->P^(f^x)) -> P^a : ?T"
   7.187    by (depth_solve rules)
   7.188  
   7.189 -lemma (in LP2)
   7.190 +schematic_lemma (in LP2)
   7.191    "A:* a:A b:A |- ?p: (Pi P:A->*.P^a->P^b) -> (Pi P:A->*.P^b->P^a)"
   7.192    -- {* Symmetry of Leibnitz equality *}
   7.193    apply (strip_asms rules)
     8.1 --- a/src/FOL/ex/Classical.thy	Fri Apr 23 23:33:48 2010 +0200
     8.2 +++ b/src/FOL/ex/Classical.thy	Fri Apr 23 23:35:43 2010 +0200
     8.3 @@ -363,7 +363,7 @@
     8.4  
     8.5  text{*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
     8.6    fast DISCOVERS who killed Agatha. *}
     8.7 -lemma "lives(agatha) & lives(butler) & lives(charles) &  
     8.8 +schematic_lemma "lives(agatha) & lives(butler) & lives(charles) &  
     8.9     (killed(agatha,agatha) | killed(butler,agatha) | killed(charles,agatha)) &  
    8.10     (\<forall>x y. killed(x,y) --> hates(x,y) & ~richer(x,y)) &  
    8.11     (\<forall>x. hates(agatha,x) --> ~hates(charles,x)) &  
     9.1 --- a/src/FOL/ex/Prolog.thy	Fri Apr 23 23:33:48 2010 +0200
     9.2 +++ b/src/FOL/ex/Prolog.thy	Fri Apr 23 23:35:43 2010 +0200
     9.3 @@ -22,18 +22,18 @@
     9.4    revNil:  "rev(Nil,Nil)"
     9.5    revCons: "[| rev(xs,ys);  app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)"
     9.6  
     9.7 -lemma "app(a:b:c:Nil, d:e:Nil, ?x)"
     9.8 +schematic_lemma "app(a:b:c:Nil, d:e:Nil, ?x)"
     9.9  apply (rule appNil appCons)
    9.10  apply (rule appNil appCons)
    9.11  apply (rule appNil appCons)
    9.12  apply (rule appNil appCons)
    9.13  done
    9.14  
    9.15 -lemma "app(?x, c:d:Nil, a:b:c:d:Nil)"
    9.16 +schematic_lemma "app(?x, c:d:Nil, a:b:c:d:Nil)"
    9.17  apply (rule appNil appCons)+
    9.18  done
    9.19  
    9.20 -lemma "app(?x, ?y, a:b:c:d:Nil)"
    9.21 +schematic_lemma "app(?x, ?y, a:b:c:d:Nil)"
    9.22  apply (rule appNil appCons)+
    9.23  back
    9.24  back
    9.25 @@ -46,15 +46,15 @@
    9.26  
    9.27  lemmas rules = appNil appCons revNil revCons
    9.28  
    9.29 -lemma "rev(a:b:c:d:Nil, ?x)"
    9.30 +schematic_lemma "rev(a:b:c:d:Nil, ?x)"
    9.31  apply (rule rules)+
    9.32  done
    9.33  
    9.34 -lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)"
    9.35 +schematic_lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)"
    9.36  apply (rule rules)+
    9.37  done
    9.38  
    9.39 -lemma "rev(?x, a:b:c:Nil)"
    9.40 +schematic_lemma "rev(?x, a:b:c:Nil)"
    9.41  apply (rule rules)+  -- {* does not solve it directly! *}
    9.42  back
    9.43  back
    9.44 @@ -65,22 +65,22 @@
    9.45  val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) (resolve_tac (@{thms rules}) 1)
    9.46  *}
    9.47  
    9.48 -lemma "rev(?x, a:b:c:Nil)"
    9.49 +schematic_lemma "rev(?x, a:b:c:Nil)"
    9.50  apply (tactic prolog_tac)
    9.51  done
    9.52  
    9.53 -lemma "rev(a:?x:c:?y:Nil, d:?z:b:?u)"
    9.54 +schematic_lemma "rev(a:?x:c:?y:Nil, d:?z:b:?u)"
    9.55  apply (tactic prolog_tac)
    9.56  done
    9.57  
    9.58  (*rev([a..p], ?w) requires 153 inferences *)
    9.59 -lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)"
    9.60 +schematic_lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)"
    9.61  apply (tactic {* DEPTH_SOLVE (resolve_tac ([@{thm refl}, @{thm conjI}] @ @{thms rules}) 1) *})
    9.62  done
    9.63  
    9.64  (*?x has 16, ?y has 32;  rev(?y,?w) requires 561 (rather large) inferences
    9.65    total inferences = 2 + 1 + 17 + 561 = 581*)
    9.66 -lemma "a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil = ?x & app(?x,?x,?y) & rev(?y,?w)"
    9.67 +schematic_lemma "a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil = ?x & app(?x,?x,?y) & rev(?y,?w)"
    9.68  apply (tactic {* DEPTH_SOLVE (resolve_tac ([@{thm refl}, @{thm conjI}] @ @{thms rules}) 1) *})
    9.69  done
    9.70  
    10.1 --- a/src/FOL/ex/Quantifiers_Cla.thy	Fri Apr 23 23:33:48 2010 +0200
    10.2 +++ b/src/FOL/ex/Quantifiers_Cla.thy	Fri Apr 23 23:35:43 2010 +0200
    10.3 @@ -58,11 +58,11 @@
    10.4    apply fast?
    10.5    oops
    10.6  
    10.7 -lemma "P(?a) --> (ALL x. P(x))"
    10.8 +schematic_lemma "P(?a) --> (ALL x. P(x))"
    10.9    apply fast?
   10.10    oops
   10.11  
   10.12 -lemma "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
   10.13 +schematic_lemma "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
   10.14    apply fast?
   10.15    oops
   10.16  
   10.17 @@ -76,7 +76,7 @@
   10.18  lemma "(P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
   10.19    by fast
   10.20  
   10.21 -lemma "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
   10.22 +schematic_lemma "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
   10.23    by fast
   10.24  
   10.25  lemma "(ALL x. Q(x))  -->  (EX x. Q(x))"
    11.1 --- a/src/FOL/ex/Quantifiers_Int.thy	Fri Apr 23 23:33:48 2010 +0200
    11.2 +++ b/src/FOL/ex/Quantifiers_Int.thy	Fri Apr 23 23:35:43 2010 +0200
    11.3 @@ -58,11 +58,11 @@
    11.4    apply (tactic "IntPr.fast_tac 1")?
    11.5    oops
    11.6  
    11.7 -lemma "P(?a) --> (ALL x. P(x))"
    11.8 +schematic_lemma "P(?a) --> (ALL x. P(x))"
    11.9    apply (tactic "IntPr.fast_tac 1")?
   11.10    oops
   11.11  
   11.12 -lemma "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
   11.13 +schematic_lemma "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
   11.14    apply (tactic "IntPr.fast_tac 1")?
   11.15    oops
   11.16  
   11.17 @@ -76,7 +76,7 @@
   11.18  lemma "(P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
   11.19    by (tactic "IntPr.fast_tac 1")
   11.20  
   11.21 -lemma "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
   11.22 +schematic_lemma "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
   11.23    by (tactic "IntPr.fast_tac 1")
   11.24  
   11.25  lemma "(ALL x. Q(x))  -->  (EX x. Q(x))"
    12.1 --- a/src/FOLP/FOLP.thy	Fri Apr 23 23:33:48 2010 +0200
    12.2 +++ b/src/FOLP/FOLP.thy	Fri Apr 23 23:35:43 2010 +0200
    12.3 @@ -19,7 +19,7 @@
    12.4  
    12.5  (*** Classical introduction rules for | and EX ***)
    12.6  
    12.7 -lemma disjCI:
    12.8 +schematic_lemma disjCI:
    12.9    assumes "!!x. x:~Q ==> f(x):P"
   12.10    shows "?p : P|Q"
   12.11    apply (rule classical)
   12.12 @@ -28,7 +28,7 @@
   12.13    done
   12.14  
   12.15  (*introduction rule involving only EX*)
   12.16 -lemma ex_classical:
   12.17 +schematic_lemma ex_classical:
   12.18    assumes "!!u. u:~(EX x. P(x)) ==> f(u):P(a)"
   12.19    shows "?p : EX x. P(x)"
   12.20    apply (rule classical)
   12.21 @@ -36,7 +36,7 @@
   12.22    done
   12.23  
   12.24  (*version of above, simplifying ~EX to ALL~ *)
   12.25 -lemma exCI:
   12.26 +schematic_lemma exCI:
   12.27    assumes "!!u. u:ALL x. ~P(x) ==> f(u):P(a)"
   12.28    shows "?p : EX x. P(x)"
   12.29    apply (rule ex_classical)
   12.30 @@ -45,7 +45,7 @@
   12.31    apply (erule exI)
   12.32    done
   12.33  
   12.34 -lemma excluded_middle: "?p : ~P | P"
   12.35 +schematic_lemma excluded_middle: "?p : ~P | P"
   12.36    apply (rule disjCI)
   12.37    apply assumption
   12.38    done
   12.39 @@ -54,7 +54,7 @@
   12.40  (*** Special elimination rules *)
   12.41  
   12.42  (*Classical implies (-->) elimination. *)
   12.43 -lemma impCE:
   12.44 +schematic_lemma impCE:
   12.45    assumes major: "p:P-->Q"
   12.46      and r1: "!!x. x:~P ==> f(x):R"
   12.47      and r2: "!!y. y:Q ==> g(y):R"
   12.48 @@ -65,7 +65,7 @@
   12.49    done
   12.50  
   12.51  (*Double negation law*)
   12.52 -lemma notnotD: "p:~~P ==> ?p : P"
   12.53 +schematic_lemma notnotD: "p:~~P ==> ?p : P"
   12.54    apply (rule classical)
   12.55    apply (erule notE)
   12.56    apply assumption
   12.57 @@ -76,7 +76,7 @@
   12.58  
   12.59  (*Classical <-> elimination.  Proof substitutes P=Q in
   12.60      ~P ==> ~Q    and    P ==> Q  *)
   12.61 -lemma iffCE:
   12.62 +schematic_lemma iffCE:
   12.63    assumes major: "p:P<->Q"
   12.64      and r1: "!!x y.[| x:P; y:Q |] ==> f(x,y):R"
   12.65      and r2: "!!x y.[| x:~P; y:~Q |] ==> g(x,y):R"
   12.66 @@ -91,7 +91,7 @@
   12.67  
   12.68  
   12.69  (*Should be used as swap since ~P becomes redundant*)
   12.70 -lemma swap:
   12.71 +schematic_lemma swap:
   12.72    assumes major: "p:~P"
   12.73      and r: "!!x. x:~Q ==> f(x):P"
   12.74    shows "?p : Q"
   12.75 @@ -136,7 +136,7 @@
   12.76      addSEs [@{thm exE}, @{thm ex1E}] addEs [@{thm all_dupE}];
   12.77  *}
   12.78  
   12.79 -lemma cla_rews:
   12.80 +schematic_lemma cla_rews:
   12.81    "?p1 : P | ~P"
   12.82    "?p2 : ~P | P"
   12.83    "?p3 : ~ ~ P <-> P"
    13.1 --- a/src/FOLP/IFOLP.thy	Fri Apr 23 23:33:48 2010 +0200
    13.2 +++ b/src/FOLP/IFOLP.thy	Fri Apr 23 23:35:43 2010 +0200
    13.3 @@ -159,7 +159,7 @@
    13.4  
    13.5  (*** Sequent-style elimination rules for & --> and ALL ***)
    13.6  
    13.7 -lemma conjE:
    13.8 +schematic_lemma conjE:
    13.9    assumes "p:P&Q"
   13.10      and "!!x y.[| x:P; y:Q |] ==> f(x,y):R"
   13.11    shows "?a:R"
   13.12 @@ -168,7 +168,7 @@
   13.13    apply (rule conjunct2 [OF assms(1)])
   13.14    done
   13.15  
   13.16 -lemma impE:
   13.17 +schematic_lemma impE:
   13.18    assumes "p:P-->Q"
   13.19      and "q:P"
   13.20      and "!!x. x:Q ==> r(x):R"
   13.21 @@ -176,7 +176,7 @@
   13.22    apply (rule assms mp)+
   13.23    done
   13.24  
   13.25 -lemma allE:
   13.26 +schematic_lemma allE:
   13.27    assumes "p:ALL x. P(x)"
   13.28      and "!!y. y:P(x) ==> q(y):R"
   13.29    shows "?p:R"
   13.30 @@ -184,7 +184,7 @@
   13.31    done
   13.32  
   13.33  (*Duplicates the quantifier; for use with eresolve_tac*)
   13.34 -lemma all_dupE:
   13.35 +schematic_lemma all_dupE:
   13.36    assumes "p:ALL x. P(x)"
   13.37      and "!!y z.[| y:P(x); z:ALL x. P(x) |] ==> q(y,z):R"
   13.38    shows "?p:R"
   13.39 @@ -194,21 +194,21 @@
   13.40  
   13.41  (*** Negation rules, which translate between ~P and P-->False ***)
   13.42  
   13.43 -lemma notI:
   13.44 +schematic_lemma notI:
   13.45    assumes "!!x. x:P ==> q(x):False"
   13.46    shows "?p:~P"
   13.47    unfolding not_def
   13.48    apply (assumption | rule assms impI)+
   13.49    done
   13.50  
   13.51 -lemma notE: "p:~P \<Longrightarrow> q:P \<Longrightarrow> ?p:R"
   13.52 +schematic_lemma notE: "p:~P \<Longrightarrow> q:P \<Longrightarrow> ?p:R"
   13.53    unfolding not_def
   13.54    apply (drule (1) mp)
   13.55    apply (erule FalseE)
   13.56    done
   13.57  
   13.58  (*This is useful with the special implication rules for each kind of P. *)
   13.59 -lemma not_to_imp:
   13.60 +schematic_lemma not_to_imp:
   13.61    assumes "p:~P"
   13.62      and "!!x. x:(P-->False) ==> q(x):Q"
   13.63    shows "?p:Q"
   13.64 @@ -217,13 +217,13 @@
   13.65  
   13.66  (* For substitution int an assumption P, reduce Q to P-->Q, substitute into
   13.67     this implication, then apply impI to move P back into the assumptions.*)
   13.68 -lemma rev_mp: "[| p:P;  q:P --> Q |] ==> ?p:Q"
   13.69 +schematic_lemma rev_mp: "[| p:P;  q:P --> Q |] ==> ?p:Q"
   13.70    apply (assumption | rule mp)+
   13.71    done
   13.72  
   13.73  
   13.74  (*Contrapositive of an inference rule*)
   13.75 -lemma contrapos:
   13.76 +schematic_lemma contrapos:
   13.77    assumes major: "p:~Q"
   13.78      and minor: "!!y. y:P==>q(y):Q"
   13.79    shows "?a:~P"
   13.80 @@ -271,7 +271,7 @@
   13.81  
   13.82  (*** If-and-only-if ***)
   13.83  
   13.84 -lemma iffI:
   13.85 +schematic_lemma iffI:
   13.86    assumes "!!x. x:P ==> q(x):Q"
   13.87      and "!!x. x:Q ==> r(x):P"
   13.88    shows "?p:P<->Q"
   13.89 @@ -282,7 +282,7 @@
   13.90  
   13.91  (*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
   13.92    
   13.93 -lemma iffE:
   13.94 +schematic_lemma iffE:
   13.95    assumes "p:P <-> Q"
   13.96      and "!!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R"
   13.97    shows "?p:R"
   13.98 @@ -294,28 +294,28 @@
   13.99  
  13.100  (* Destruct rules for <-> similar to Modus Ponens *)
  13.101  
  13.102 -lemma iffD1: "[| p:P <-> Q; q:P |] ==> ?p:Q"
  13.103 +schematic_lemma iffD1: "[| p:P <-> Q; q:P |] ==> ?p:Q"
  13.104    unfolding iff_def
  13.105    apply (rule conjunct1 [THEN mp], assumption+)
  13.106    done
  13.107  
  13.108 -lemma iffD2: "[| p:P <-> Q; q:Q |] ==> ?p:P"
  13.109 +schematic_lemma iffD2: "[| p:P <-> Q; q:Q |] ==> ?p:P"
  13.110    unfolding iff_def
  13.111    apply (rule conjunct2 [THEN mp], assumption+)
  13.112    done
  13.113  
  13.114 -lemma iff_refl: "?p:P <-> P"
  13.115 +schematic_lemma iff_refl: "?p:P <-> P"
  13.116    apply (rule iffI)
  13.117     apply assumption+
  13.118    done
  13.119  
  13.120 -lemma iff_sym: "p:Q <-> P ==> ?p:P <-> Q"
  13.121 +schematic_lemma iff_sym: "p:Q <-> P ==> ?p:P <-> Q"
  13.122    apply (erule iffE)
  13.123    apply (rule iffI)
  13.124     apply (erule (1) mp)+
  13.125    done
  13.126  
  13.127 -lemma iff_trans: "[| p:P <-> Q; q:Q<-> R |] ==> ?p:P <-> R"
  13.128 +schematic_lemma iff_trans: "[| p:P <-> Q; q:Q<-> R |] ==> ?p:P <-> R"
  13.129    apply (rule iffI)
  13.130     apply (assumption | erule iffE | erule (1) impE)+
  13.131    done
  13.132 @@ -326,7 +326,7 @@
  13.133   do NOT mean the same thing.  The parser treats EX!x y.P(x,y) as sequential.
  13.134  ***)
  13.135  
  13.136 -lemma ex1I:
  13.137 +schematic_lemma ex1I:
  13.138    assumes "p:P(a)"
  13.139      and "!!x u. u:P(x) ==> f(u) : x=a"
  13.140    shows "?p:EX! x. P(x)"
  13.141 @@ -334,7 +334,7 @@
  13.142    apply (assumption | rule assms exI conjI allI impI)+
  13.143    done
  13.144  
  13.145 -lemma ex1E:
  13.146 +schematic_lemma ex1E:
  13.147    assumes "p:EX! x. P(x)"
  13.148      and "!!x u v. [| u:P(x);  v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R"
  13.149    shows "?a : R"
  13.150 @@ -353,7 +353,7 @@
  13.151      REPEAT1 (eresolve_tac [asm_rl, @{thm mp}] i)
  13.152  *}
  13.153  
  13.154 -lemma conj_cong:
  13.155 +schematic_lemma conj_cong:
  13.156    assumes "p:P <-> P'"
  13.157      and "!!x. x:P' ==> q(x):Q <-> Q'"
  13.158    shows "?p:(P&Q) <-> (P'&Q')"
  13.159 @@ -362,12 +362,12 @@
  13.160      erule iffE conjE mp | tactic {* iff_tac @{thms assms} 1 *})+
  13.161    done
  13.162  
  13.163 -lemma disj_cong:
  13.164 +schematic_lemma disj_cong:
  13.165    "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P|Q) <-> (P'|Q')"
  13.166    apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | tactic {* mp_tac 1 *})+
  13.167    done
  13.168  
  13.169 -lemma imp_cong:
  13.170 +schematic_lemma imp_cong:
  13.171    assumes "p:P <-> P'"
  13.172      and "!!x. x:P' ==> q(x):Q <-> Q'"
  13.173    shows "?p:(P-->Q) <-> (P'-->Q')"
  13.174 @@ -376,24 +376,24 @@
  13.175      tactic {* iff_tac @{thms assms} 1 *})+
  13.176    done
  13.177  
  13.178 -lemma iff_cong:
  13.179 +schematic_lemma iff_cong:
  13.180    "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')"
  13.181    apply (erule iffE | assumption | rule iffI | tactic {* mp_tac 1 *})+
  13.182    done
  13.183  
  13.184 -lemma not_cong:
  13.185 +schematic_lemma not_cong:
  13.186    "p:P <-> P' ==> ?p:~P <-> ~P'"
  13.187    apply (assumption | rule iffI notI | tactic {* mp_tac 1 *} | erule iffE notE)+
  13.188    done
  13.189  
  13.190 -lemma all_cong:
  13.191 +schematic_lemma all_cong:
  13.192    assumes "!!x. f(x):P(x) <-> Q(x)"
  13.193    shows "?p:(ALL x. P(x)) <-> (ALL x. Q(x))"
  13.194    apply (assumption | rule iffI allI | tactic {* mp_tac 1 *} | erule allE |
  13.195      tactic {* iff_tac @{thms assms} 1 *})+
  13.196    done
  13.197  
  13.198 -lemma ex_cong:
  13.199 +schematic_lemma ex_cong:
  13.200    assumes "!!x. f(x):P(x) <-> Q(x)"
  13.201    shows "?p:(EX x. P(x)) <-> (EX x. Q(x))"
  13.202    apply (erule exE | assumption | rule iffI exI | tactic {* mp_tac 1 *} |
  13.203 @@ -413,7 +413,7 @@
  13.204  
  13.205  lemmas refl = ieqI
  13.206  
  13.207 -lemma subst:
  13.208 +schematic_lemma subst:
  13.209    assumes prem1: "p:a=b"
  13.210      and prem2: "q:P(a)"
  13.211    shows "?p : P(b)"
  13.212 @@ -423,17 +423,17 @@
  13.213    apply assumption
  13.214    done
  13.215  
  13.216 -lemma sym: "q:a=b ==> ?c:b=a"
  13.217 +schematic_lemma sym: "q:a=b ==> ?c:b=a"
  13.218    apply (erule subst)
  13.219    apply (rule refl)
  13.220    done
  13.221  
  13.222 -lemma trans: "[| p:a=b;  q:b=c |] ==> ?d:a=c"
  13.223 +schematic_lemma trans: "[| p:a=b;  q:b=c |] ==> ?d:a=c"
  13.224    apply (erule (1) subst)
  13.225    done
  13.226  
  13.227  (** ~ b=a ==> ~ a=b **)
  13.228 -lemma not_sym: "p:~ b=a ==> ?q:~ a=b"
  13.229 +schematic_lemma not_sym: "p:~ b=a ==> ?q:~ a=b"
  13.230    apply (erule contrapos)
  13.231    apply (erule sym)
  13.232    done
  13.233 @@ -442,7 +442,7 @@
  13.234  lemmas ssubst = sym [THEN subst, standard]
  13.235  
  13.236  (*A special case of ex1E that would otherwise need quantifier expansion*)
  13.237 -lemma ex1_equalsE: "[| p:EX! x. P(x);  q:P(a);  r:P(b) |] ==> ?d:a=b"
  13.238 +schematic_lemma ex1_equalsE: "[| p:EX! x. P(x);  q:P(a);  r:P(b) |] ==> ?d:a=b"
  13.239    apply (erule ex1E)
  13.240    apply (rule trans)
  13.241     apply (rule_tac [2] sym)
  13.242 @@ -451,17 +451,17 @@
  13.243  
  13.244  (** Polymorphic congruence rules **)
  13.245  
  13.246 -lemma subst_context: "[| p:a=b |]  ==>  ?d:t(a)=t(b)"
  13.247 +schematic_lemma subst_context: "[| p:a=b |]  ==>  ?d:t(a)=t(b)"
  13.248    apply (erule ssubst)
  13.249    apply (rule refl)
  13.250    done
  13.251  
  13.252 -lemma subst_context2: "[| p:a=b;  q:c=d |]  ==>  ?p:t(a,c)=t(b,d)"
  13.253 +schematic_lemma subst_context2: "[| p:a=b;  q:c=d |]  ==>  ?p:t(a,c)=t(b,d)"
  13.254    apply (erule ssubst)+
  13.255    apply (rule refl)
  13.256    done
  13.257  
  13.258 -lemma subst_context3: "[| p:a=b;  q:c=d;  r:e=f |]  ==>  ?p:t(a,c,e)=t(b,d,f)"
  13.259 +schematic_lemma subst_context3: "[| p:a=b;  q:c=d;  r:e=f |]  ==>  ?p:t(a,c,e)=t(b,d,f)"
  13.260    apply (erule ssubst)+
  13.261    apply (rule refl)
  13.262    done
  13.263 @@ -470,7 +470,7 @@
  13.264          a = b
  13.265          |   |
  13.266          c = d   *)
  13.267 -lemma box_equals: "[| p:a=b;  q:a=c;  r:b=d |] ==> ?p:c=d"
  13.268 +schematic_lemma box_equals: "[| p:a=b;  q:a=c;  r:b=d |] ==> ?p:c=d"
  13.269    apply (rule trans)
  13.270     apply (rule trans)
  13.271      apply (rule sym)
  13.272 @@ -478,7 +478,7 @@
  13.273    done
  13.274  
  13.275  (*Dual of box_equals: for proving equalities backwards*)
  13.276 -lemma simp_equals: "[| p:a=c;  q:b=d;  r:c=d |] ==> ?p:a=b"
  13.277 +schematic_lemma simp_equals: "[| p:a=c;  q:b=d;  r:c=d |] ==> ?p:a=b"
  13.278    apply (rule trans)
  13.279     apply (rule trans)
  13.280      apply (assumption | rule sym)+
  13.281 @@ -486,17 +486,17 @@
  13.282  
  13.283  (** Congruence rules for predicate letters **)
  13.284  
  13.285 -lemma pred1_cong: "p:a=a' ==> ?p:P(a) <-> P(a')"
  13.286 +schematic_lemma pred1_cong: "p:a=a' ==> ?p:P(a) <-> P(a')"
  13.287    apply (rule iffI)
  13.288     apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *})
  13.289    done
  13.290  
  13.291 -lemma pred2_cong: "[| p:a=a';  q:b=b' |] ==> ?p:P(a,b) <-> P(a',b')"
  13.292 +schematic_lemma pred2_cong: "[| p:a=a';  q:b=b' |] ==> ?p:P(a,b) <-> P(a',b')"
  13.293    apply (rule iffI)
  13.294     apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *})
  13.295    done
  13.296  
  13.297 -lemma pred3_cong: "[| p:a=a';  q:b=b';  r:c=c' |] ==> ?p:P(a,b,c) <-> P(a',b',c')"
  13.298 +schematic_lemma pred3_cong: "[| p:a=a';  q:b=b';  r:c=c' |] ==> ?p:P(a,b,c) <-> P(a',b',c')"
  13.299    apply (rule iffI)
  13.300     apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *})
  13.301    done
  13.302 @@ -514,14 +514,14 @@
  13.303     R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
  13.304      (preprint, University of St Andrews, 1991)  ***)
  13.305  
  13.306 -lemma conj_impE:
  13.307 +schematic_lemma conj_impE:
  13.308    assumes major: "p:(P&Q)-->S"
  13.309      and minor: "!!x. x:P-->(Q-->S) ==> q(x):R"
  13.310    shows "?p:R"
  13.311    apply (assumption | rule conjI impI major [THEN mp] minor)+
  13.312    done
  13.313  
  13.314 -lemma disj_impE:
  13.315 +schematic_lemma disj_impE:
  13.316    assumes major: "p:(P|Q)-->S"
  13.317      and minor: "!!x y.[| x:P-->S; y:Q-->S |] ==> q(x,y):R"
  13.318    shows "?p:R"
  13.319 @@ -532,7 +532,7 @@
  13.320  
  13.321  (*Simplifies the implication.  Classical version is stronger.
  13.322    Still UNSAFE since Q must be provable -- backtracking needed.  *)
  13.323 -lemma imp_impE:
  13.324 +schematic_lemma imp_impE:
  13.325    assumes major: "p:(P-->Q)-->S"
  13.326      and r1: "!!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q"
  13.327      and r2: "!!x. x:S ==> r(x):R"
  13.328 @@ -542,7 +542,7 @@
  13.329  
  13.330  (*Simplifies the implication.  Classical version is stronger.
  13.331    Still UNSAFE since ~P must be provable -- backtracking needed.  *)
  13.332 -lemma not_impE:
  13.333 +schematic_lemma not_impE:
  13.334    assumes major: "p:~P --> S"
  13.335      and r1: "!!y. y:P ==> q(y):False"
  13.336      and r2: "!!y. y:S ==> r(y):R"
  13.337 @@ -551,7 +551,7 @@
  13.338    done
  13.339  
  13.340  (*Simplifies the implication.   UNSAFE.  *)
  13.341 -lemma iff_impE:
  13.342 +schematic_lemma iff_impE:
  13.343    assumes major: "p:(P<->Q)-->S"
  13.344      and r1: "!!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q"
  13.345      and r2: "!!x y.[| x:Q; y:P-->S |] ==> r(x,y):P"
  13.346 @@ -561,7 +561,7 @@
  13.347    done
  13.348  
  13.349  (*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
  13.350 -lemma all_impE:
  13.351 +schematic_lemma all_impE:
  13.352    assumes major: "p:(ALL x. P(x))-->S"
  13.353      and r1: "!!x. q:P(x)"
  13.354      and r2: "!!y. y:S ==> r(y):R"
  13.355 @@ -570,7 +570,7 @@
  13.356    done
  13.357  
  13.358  (*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
  13.359 -lemma ex_impE:
  13.360 +schematic_lemma ex_impE:
  13.361    assumes major: "p:(EX x. P(x))-->S"
  13.362      and r: "!!y. y:P(a)-->S ==> q(y):R"
  13.363    shows "?p:R"
  13.364 @@ -578,7 +578,7 @@
  13.365    done
  13.366  
  13.367  
  13.368 -lemma rev_cut_eq:
  13.369 +schematic_lemma rev_cut_eq:
  13.370    assumes "p:a=b"
  13.371      and "!!x. x:a=b ==> f(x):R"
  13.372    shows "?p:R"
  13.373 @@ -619,7 +619,7 @@
  13.374  
  13.375  (*** Rewrite rules ***)
  13.376  
  13.377 -lemma conj_rews:
  13.378 +schematic_lemma conj_rews:
  13.379    "?p1 : P & True <-> P"
  13.380    "?p2 : True & P <-> P"
  13.381    "?p3 : P & False <-> False"
  13.382 @@ -631,7 +631,7 @@
  13.383    apply (tactic {* fn st => IntPr.fast_tac 1 st *})+
  13.384    done
  13.385  
  13.386 -lemma disj_rews:
  13.387 +schematic_lemma disj_rews:
  13.388    "?p1 : P | True <-> True"
  13.389    "?p2 : True | P <-> True"
  13.390    "?p3 : P | False <-> P"
  13.391 @@ -641,13 +641,13 @@
  13.392    apply (tactic {* IntPr.fast_tac 1 *})+
  13.393    done
  13.394  
  13.395 -lemma not_rews:
  13.396 +schematic_lemma not_rews:
  13.397    "?p1 : ~ False <-> True"
  13.398    "?p2 : ~ True <-> False"
  13.399    apply (tactic {* IntPr.fast_tac 1 *})+
  13.400    done
  13.401  
  13.402 -lemma imp_rews:
  13.403 +schematic_lemma imp_rews:
  13.404    "?p1 : (P --> False) <-> ~P"
  13.405    "?p2 : (P --> True) <-> True"
  13.406    "?p3 : (False --> P) <-> True"
  13.407 @@ -657,7 +657,7 @@
  13.408    apply (tactic {* IntPr.fast_tac 1 *})+
  13.409    done
  13.410  
  13.411 -lemma iff_rews:
  13.412 +schematic_lemma iff_rews:
  13.413    "?p1 : (True <-> P) <-> P"
  13.414    "?p2 : (P <-> True) <-> P"
  13.415    "?p3 : (P <-> P) <-> True"
  13.416 @@ -666,14 +666,14 @@
  13.417    apply (tactic {* IntPr.fast_tac 1 *})+
  13.418    done
  13.419  
  13.420 -lemma quant_rews:
  13.421 +schematic_lemma quant_rews:
  13.422    "?p1 : (ALL x. P) <-> P"
  13.423    "?p2 : (EX x. P) <-> P"
  13.424    apply (tactic {* IntPr.fast_tac 1 *})+
  13.425    done
  13.426  
  13.427  (*These are NOT supplied by default!*)
  13.428 -lemma distrib_rews1:
  13.429 +schematic_lemma distrib_rews1:
  13.430    "?p1 : ~(P|Q) <-> ~P & ~Q"
  13.431    "?p2 : P & (Q | R) <-> P&Q | P&R"
  13.432    "?p3 : (Q | R) & P <-> Q&P | R&P"
  13.433 @@ -681,7 +681,7 @@
  13.434    apply (tactic {* IntPr.fast_tac 1 *})+
  13.435    done
  13.436  
  13.437 -lemma distrib_rews2:
  13.438 +schematic_lemma distrib_rews2:
  13.439    "?p1 : ~(EX x. NORM(P(x))) <-> (ALL x. ~NORM(P(x)))"
  13.440    "?p2 : ((EX x. NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)"
  13.441    "?p3 : (EX x. NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))"
  13.442 @@ -691,11 +691,11 @@
  13.443  
  13.444  lemmas distrib_rews = distrib_rews1 distrib_rews2
  13.445  
  13.446 -lemma P_Imp_P_iff_T: "p:P ==> ?p:(P <-> True)"
  13.447 +schematic_lemma P_Imp_P_iff_T: "p:P ==> ?p:(P <-> True)"
  13.448    apply (tactic {* IntPr.fast_tac 1 *})
  13.449    done
  13.450  
  13.451 -lemma not_P_imp_P_iff_F: "p:~P ==> ?p:(P <-> False)"
  13.452 +schematic_lemma not_P_imp_P_iff_F: "p:~P ==> ?p:(P <-> False)"
  13.453    apply (tactic {* IntPr.fast_tac 1 *})
  13.454    done
  13.455  
    14.1 --- a/src/FOLP/ex/Classical.thy	Fri Apr 23 23:33:48 2010 +0200
    14.2 +++ b/src/FOLP/ex/Classical.thy	Fri Apr 23 23:35:43 2010 +0200
    14.3 @@ -9,14 +9,14 @@
    14.4  imports FOLP
    14.5  begin
    14.6  
    14.7 -lemma "?p : (P --> Q | R) --> (P-->Q) | (P-->R)"
    14.8 +schematic_lemma "?p : (P --> Q | R) --> (P-->Q) | (P-->R)"
    14.9    by (tactic "fast_tac FOLP_cs 1")
   14.10  
   14.11  (*If and only if*)
   14.12 -lemma "?p : (P<->Q) <-> (Q<->P)"
   14.13 +schematic_lemma "?p : (P<->Q) <-> (Q<->P)"
   14.14    by (tactic "fast_tac FOLP_cs 1")
   14.15  
   14.16 -lemma "?p : ~ (P <-> ~P)"
   14.17 +schematic_lemma "?p : ~ (P <-> ~P)"
   14.18    by (tactic "fast_tac FOLP_cs 1")
   14.19  
   14.20  
   14.21 @@ -32,138 +32,138 @@
   14.22  
   14.23  text "Pelletier's examples"
   14.24  (*1*)
   14.25 -lemma "?p : (P-->Q)  <->  (~Q --> ~P)"
   14.26 +schematic_lemma "?p : (P-->Q)  <->  (~Q --> ~P)"
   14.27    by (tactic "fast_tac FOLP_cs 1")
   14.28  
   14.29  (*2*)
   14.30 -lemma "?p : ~ ~ P  <->  P"
   14.31 +schematic_lemma "?p : ~ ~ P  <->  P"
   14.32    by (tactic "fast_tac FOLP_cs 1")
   14.33  
   14.34  (*3*)
   14.35 -lemma "?p : ~(P-->Q) --> (Q-->P)"
   14.36 +schematic_lemma "?p : ~(P-->Q) --> (Q-->P)"
   14.37    by (tactic "fast_tac FOLP_cs 1")
   14.38  
   14.39  (*4*)
   14.40 -lemma "?p : (~P-->Q)  <->  (~Q --> P)"
   14.41 +schematic_lemma "?p : (~P-->Q)  <->  (~Q --> P)"
   14.42    by (tactic "fast_tac FOLP_cs 1")
   14.43  
   14.44  (*5*)
   14.45 -lemma "?p : ((P|Q)-->(P|R)) --> (P|(Q-->R))"
   14.46 +schematic_lemma "?p : ((P|Q)-->(P|R)) --> (P|(Q-->R))"
   14.47    by (tactic "fast_tac FOLP_cs 1")
   14.48  
   14.49  (*6*)
   14.50 -lemma "?p : P | ~ P"
   14.51 +schematic_lemma "?p : P | ~ P"
   14.52    by (tactic "fast_tac FOLP_cs 1")
   14.53  
   14.54  (*7*)
   14.55 -lemma "?p : P | ~ ~ ~ P"
   14.56 +schematic_lemma "?p : P | ~ ~ ~ P"
   14.57    by (tactic "fast_tac FOLP_cs 1")
   14.58  
   14.59  (*8.  Peirce's law*)
   14.60 -lemma "?p : ((P-->Q) --> P)  -->  P"
   14.61 +schematic_lemma "?p : ((P-->Q) --> P)  -->  P"
   14.62    by (tactic "fast_tac FOLP_cs 1")
   14.63  
   14.64  (*9*)
   14.65 -lemma "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
   14.66 +schematic_lemma "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
   14.67    by (tactic "fast_tac FOLP_cs 1")
   14.68  
   14.69  (*10*)
   14.70 -lemma "?p : (Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)"
   14.71 +schematic_lemma "?p : (Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)"
   14.72    by (tactic "fast_tac FOLP_cs 1")
   14.73  
   14.74  (*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
   14.75 -lemma "?p : P<->P"
   14.76 +schematic_lemma "?p : P<->P"
   14.77    by (tactic "fast_tac FOLP_cs 1")
   14.78  
   14.79  (*12.  "Dijkstra's law"*)
   14.80 -lemma "?p : ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))"
   14.81 +schematic_lemma "?p : ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))"
   14.82    by (tactic "fast_tac FOLP_cs 1")
   14.83  
   14.84  (*13.  Distributive law*)
   14.85 -lemma "?p : P | (Q & R)  <-> (P | Q) & (P | R)"
   14.86 +schematic_lemma "?p : P | (Q & R)  <-> (P | Q) & (P | R)"
   14.87    by (tactic "fast_tac FOLP_cs 1")
   14.88  
   14.89  (*14*)
   14.90 -lemma "?p : (P <-> Q) <-> ((Q | ~P) & (~Q|P))"
   14.91 +schematic_lemma "?p : (P <-> Q) <-> ((Q | ~P) & (~Q|P))"
   14.92    by (tactic "fast_tac FOLP_cs 1")
   14.93  
   14.94  (*15*)
   14.95 -lemma "?p : (P --> Q) <-> (~P | Q)"
   14.96 +schematic_lemma "?p : (P --> Q) <-> (~P | Q)"
   14.97    by (tactic "fast_tac FOLP_cs 1")
   14.98  
   14.99  (*16*)
  14.100 -lemma "?p : (P-->Q) | (Q-->P)"
  14.101 +schematic_lemma "?p : (P-->Q) | (Q-->P)"
  14.102    by (tactic "fast_tac FOLP_cs 1")
  14.103  
  14.104  (*17*)
  14.105 -lemma "?p : ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))"
  14.106 +schematic_lemma "?p : ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))"
  14.107    by (tactic "fast_tac FOLP_cs 1")
  14.108  
  14.109  
  14.110  text "Classical Logic: examples with quantifiers"
  14.111  
  14.112 -lemma "?p : (ALL x. P(x) & Q(x)) <-> (ALL x. P(x))  &  (ALL x. Q(x))"
  14.113 +schematic_lemma "?p : (ALL x. P(x) & Q(x)) <-> (ALL x. P(x))  &  (ALL x. Q(x))"
  14.114    by (tactic "fast_tac FOLP_cs 1")
  14.115  
  14.116 -lemma "?p : (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))"
  14.117 +schematic_lemma "?p : (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))"
  14.118    by (tactic "fast_tac FOLP_cs 1")
  14.119  
  14.120 -lemma "?p : (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q"
  14.121 +schematic_lemma "?p : (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q"
  14.122    by (tactic "fast_tac FOLP_cs 1")
  14.123  
  14.124 -lemma "?p : (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)"
  14.125 +schematic_lemma "?p : (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)"
  14.126    by (tactic "fast_tac FOLP_cs 1")
  14.127  
  14.128  
  14.129  text "Problems requiring quantifier duplication"
  14.130  
  14.131  (*Needs multiple instantiation of ALL.*)
  14.132 -lemma "?p : (ALL x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))"
  14.133 +schematic_lemma "?p : (ALL x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))"
  14.134    by (tactic "best_tac FOLP_dup_cs 1")
  14.135  
  14.136  (*Needs double instantiation of the quantifier*)
  14.137 -lemma "?p : EX x. P(x) --> P(a) & P(b)"
  14.138 +schematic_lemma "?p : EX x. P(x) --> P(a) & P(b)"
  14.139    by (tactic "best_tac FOLP_dup_cs 1")
  14.140  
  14.141 -lemma "?p : EX z. P(z) --> (ALL x. P(x))"
  14.142 +schematic_lemma "?p : EX z. P(z) --> (ALL x. P(x))"
  14.143    by (tactic "best_tac FOLP_dup_cs 1")
  14.144  
  14.145  
  14.146  text "Hard examples with quantifiers"
  14.147  
  14.148  text "Problem 18"
  14.149 -lemma "?p : EX y. ALL x. P(y)-->P(x)"
  14.150 +schematic_lemma "?p : EX y. ALL x. P(y)-->P(x)"
  14.151    by (tactic "best_tac FOLP_dup_cs 1")
  14.152  
  14.153  text "Problem 19"
  14.154 -lemma "?p : EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
  14.155 +schematic_lemma "?p : EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
  14.156    by (tactic "best_tac FOLP_dup_cs 1")
  14.157  
  14.158  text "Problem 20"
  14.159 -lemma "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))      
  14.160 +schematic_lemma "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))      
  14.161      --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"
  14.162    by (tactic "fast_tac FOLP_cs 1")
  14.163  
  14.164  text "Problem 21"
  14.165 -lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))";
  14.166 +schematic_lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))";
  14.167    by (tactic "best_tac FOLP_dup_cs 1")
  14.168  
  14.169  text "Problem 22"
  14.170 -lemma "?p : (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))"
  14.171 +schematic_lemma "?p : (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))"
  14.172    by (tactic "fast_tac FOLP_cs 1")
  14.173  
  14.174  text "Problem 23"
  14.175 -lemma "?p : (ALL x. P | Q(x))  <->  (P | (ALL x. Q(x)))"
  14.176 +schematic_lemma "?p : (ALL x. P | Q(x))  <->  (P | (ALL x. Q(x)))"
  14.177    by (tactic "best_tac FOLP_dup_cs 1")
  14.178  
  14.179  text "Problem 24"
  14.180 -lemma "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &   
  14.181 +schematic_lemma "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &   
  14.182       (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))   
  14.183      --> (EX x. P(x)&R(x))"
  14.184    by (tactic "fast_tac FOLP_cs 1")
  14.185  
  14.186  text "Problem 25"
  14.187 -lemma "?p : (EX x. P(x)) &  
  14.188 +schematic_lemma "?p : (EX x. P(x)) &  
  14.189         (ALL x. L(x) --> ~ (M(x) & R(x))) &  
  14.190         (ALL x. P(x) --> (M(x) & L(x))) &   
  14.191         ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))  
  14.192 @@ -171,13 +171,13 @@
  14.193    oops
  14.194  
  14.195  text "Problem 26"
  14.196 -lemma "?u : ((EX x. p(x)) <-> (EX x. q(x))) &   
  14.197 +schematic_lemma "?u : ((EX x. p(x)) <-> (EX x. q(x))) &   
  14.198       (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))   
  14.199    --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
  14.200    by (tactic "fast_tac FOLP_cs 1")
  14.201  
  14.202  text "Problem 27"
  14.203 -lemma "?p : (EX x. P(x) & ~Q(x)) &    
  14.204 +schematic_lemma "?p : (EX x. P(x) & ~Q(x)) &    
  14.205                (ALL x. P(x) --> R(x)) &    
  14.206                (ALL x. M(x) & L(x) --> P(x)) &    
  14.207                ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))   
  14.208 @@ -185,49 +185,49 @@
  14.209    by (tactic "fast_tac FOLP_cs 1")
  14.210  
  14.211  text "Problem 28.  AMENDED"
  14.212 -lemma "?p : (ALL x. P(x) --> (ALL x. Q(x))) &    
  14.213 +schematic_lemma "?p : (ALL x. P(x) --> (ALL x. Q(x))) &    
  14.214          ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &   
  14.215          ((EX x. S(x)) --> (ALL x. L(x) --> M(x)))   
  14.216      --> (ALL x. P(x) & L(x) --> M(x))"
  14.217    by (tactic "fast_tac FOLP_cs 1")
  14.218  
  14.219  text "Problem 29.  Essentially the same as Principia Mathematica *11.71"
  14.220 -lemma "?p : (EX x. P(x)) & (EX y. Q(y))   
  14.221 +schematic_lemma "?p : (EX x. P(x)) & (EX y. Q(y))   
  14.222      --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->      
  14.223           (ALL x y. P(x) & Q(y) --> R(x) & S(y)))"
  14.224    by (tactic "fast_tac FOLP_cs 1")
  14.225  
  14.226  text "Problem 30"
  14.227 -lemma "?p : (ALL x. P(x) | Q(x) --> ~ R(x)) &  
  14.228 +schematic_lemma "?p : (ALL x. P(x) | Q(x) --> ~ R(x)) &  
  14.229          (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))   
  14.230      --> (ALL x. S(x))"
  14.231    by (tactic "fast_tac FOLP_cs 1")
  14.232  
  14.233  text "Problem 31"
  14.234 -lemma "?p : ~(EX x. P(x) & (Q(x) | R(x))) &  
  14.235 +schematic_lemma "?p : ~(EX x. P(x) & (Q(x) | R(x))) &  
  14.236          (EX x. L(x) & P(x)) &  
  14.237          (ALL x. ~ R(x) --> M(x))   
  14.238      --> (EX x. L(x) & M(x))"
  14.239    by (tactic "fast_tac FOLP_cs 1")
  14.240  
  14.241  text "Problem 32"
  14.242 -lemma "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) &  
  14.243 +schematic_lemma "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) &  
  14.244          (ALL x. S(x) & R(x) --> L(x)) &  
  14.245          (ALL x. M(x) --> R(x))   
  14.246      --> (ALL x. P(x) & M(x) --> L(x))"
  14.247    by (tactic "best_tac FOLP_dup_cs 1")
  14.248  
  14.249  text "Problem 33"
  14.250 -lemma "?p : (ALL x. P(a) & (P(x)-->P(b))-->P(c))  <->     
  14.251 +schematic_lemma "?p : (ALL x. P(a) & (P(x)-->P(b))-->P(c))  <->     
  14.252       (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"
  14.253    by (tactic "best_tac FOLP_dup_cs 1")
  14.254  
  14.255  text "Problem 35"
  14.256 -lemma "?p : EX x y. P(x,y) -->  (ALL u v. P(u,v))"
  14.257 +schematic_lemma "?p : EX x y. P(x,y) -->  (ALL u v. P(u,v))"
  14.258    by (tactic "best_tac FOLP_dup_cs 1")
  14.259  
  14.260  text "Problem 36"
  14.261 -lemma
  14.262 +schematic_lemma
  14.263  "?p : (ALL x. EX y. J(x,y)) &  
  14.264        (ALL x. EX y. G(x,y)) &  
  14.265        (ALL x y. J(x,y) | G(x,y) --> (ALL z. J(y,z) | G(y,z) --> H(x,z)))    
  14.266 @@ -235,7 +235,7 @@
  14.267    by (tactic "fast_tac FOLP_cs 1")
  14.268  
  14.269  text "Problem 37"
  14.270 -lemma "?p : (ALL z. EX w. ALL x. EX y.  
  14.271 +schematic_lemma "?p : (ALL z. EX w. ALL x. EX y.  
  14.272             (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) &  
  14.273          (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) &  
  14.274          ((EX x y. Q(x,y)) --> (ALL x. R(x,x)))   
  14.275 @@ -243,21 +243,21 @@
  14.276    by (tactic "fast_tac FOLP_cs 1")
  14.277  
  14.278  text "Problem 39"
  14.279 -lemma "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
  14.280 +schematic_lemma "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
  14.281    by (tactic "fast_tac FOLP_cs 1")
  14.282  
  14.283  text "Problem 40.  AMENDED"
  14.284 -lemma "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->   
  14.285 +schematic_lemma "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->   
  14.286                ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"
  14.287    by (tactic "fast_tac FOLP_cs 1")
  14.288  
  14.289  text "Problem 41"
  14.290 -lemma "?p : (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))   
  14.291 +schematic_lemma "?p : (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))   
  14.292            --> ~ (EX z. ALL x. f(x,z))"
  14.293    by (tactic "best_tac FOLP_dup_cs 1")
  14.294  
  14.295  text "Problem 44"
  14.296 -lemma "?p : (ALL x. f(x) -->                                     
  14.297 +schematic_lemma "?p : (ALL x. f(x) -->                                     
  14.298                (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &        
  14.299                (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                    
  14.300                --> (EX x. j(x) & ~f(x))"
  14.301 @@ -266,37 +266,37 @@
  14.302  text "Problems (mainly) involving equality or functions"
  14.303  
  14.304  text "Problem 48"
  14.305 -lemma "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c"
  14.306 +schematic_lemma "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c"
  14.307    by (tactic "fast_tac FOLP_cs 1")
  14.308  
  14.309  text "Problem 50"
  14.310  (*What has this to do with equality?*)
  14.311 -lemma "?p : (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))"
  14.312 +schematic_lemma "?p : (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))"
  14.313    by (tactic "best_tac FOLP_dup_cs 1")
  14.314  
  14.315  text "Problem 56"
  14.316 -lemma
  14.317 +schematic_lemma
  14.318   "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
  14.319    by (tactic "fast_tac FOLP_cs 1")
  14.320  
  14.321  text "Problem 57"
  14.322 -lemma
  14.323 +schematic_lemma
  14.324  "?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &  
  14.325        (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))"
  14.326    by (tactic "fast_tac FOLP_cs 1")
  14.327  
  14.328  text "Problem 58  NOT PROVED AUTOMATICALLY"
  14.329 -lemma
  14.330 +schematic_lemma
  14.331    notes f_cong = subst_context [where t = f]
  14.332    shows "?p : (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))"
  14.333    by (tactic {* fast_tac (FOLP_cs addSIs [@{thm f_cong}]) 1 *})
  14.334  
  14.335  text "Problem 59"
  14.336 -lemma "?p : (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))"
  14.337 +schematic_lemma "?p : (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))"
  14.338    by (tactic "best_tac FOLP_dup_cs 1")
  14.339  
  14.340  text "Problem 60"
  14.341 -lemma "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
  14.342 +schematic_lemma "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
  14.343    by (tactic "fast_tac FOLP_cs 1")
  14.344  
  14.345  end
    15.1 --- a/src/FOLP/ex/Foundation.thy	Fri Apr 23 23:33:48 2010 +0200
    15.2 +++ b/src/FOLP/ex/Foundation.thy	Fri Apr 23 23:35:43 2010 +0200
    15.3 @@ -9,7 +9,7 @@
    15.4  imports IFOLP
    15.5  begin
    15.6  
    15.7 -lemma "?p : A&B  --> (C-->A&C)"
    15.8 +schematic_lemma "?p : A&B  --> (C-->A&C)"
    15.9  apply (rule impI)
   15.10  apply (rule impI)
   15.11  apply (rule conjI)
   15.12 @@ -19,7 +19,7 @@
   15.13  done
   15.14  
   15.15  text {*A form of conj-elimination*}
   15.16 -lemma
   15.17 +schematic_lemma
   15.18    assumes "p : A & B"
   15.19      and "!!x y. x : A ==> y : B ==> f(x, y) : C"
   15.20    shows "?p : C"
   15.21 @@ -30,7 +30,7 @@
   15.22  apply (rule prems)
   15.23  done
   15.24  
   15.25 -lemma
   15.26 +schematic_lemma
   15.27    assumes "!!A x. x : ~ ~A ==> cla(x) : A"
   15.28    shows "?p : B | ~B"
   15.29  apply (rule prems)
   15.30 @@ -48,7 +48,7 @@
   15.31  apply assumption
   15.32  done
   15.33  
   15.34 -lemma
   15.35 +schematic_lemma
   15.36    assumes "!!A x. x : ~ ~A ==> cla(x) : A"
   15.37    shows "?p : B | ~B"
   15.38  apply (rule prems)
   15.39 @@ -63,7 +63,7 @@
   15.40  done
   15.41  
   15.42  
   15.43 -lemma
   15.44 +schematic_lemma
   15.45    assumes "p : A | ~A"
   15.46      and "q : ~ ~A"
   15.47    shows "?p : A"
   15.48 @@ -79,7 +79,7 @@
   15.49  
   15.50  subsection "Examples with quantifiers"
   15.51  
   15.52 -lemma
   15.53 +schematic_lemma
   15.54    assumes "p : ALL z. G(z)"
   15.55    shows "?p : ALL z. G(z)|H(z)"
   15.56  apply (rule allI)
   15.57 @@ -87,20 +87,20 @@
   15.58  apply (rule prems [THEN spec])
   15.59  done
   15.60  
   15.61 -lemma "?p : ALL x. EX y. x=y"
   15.62 +schematic_lemma "?p : ALL x. EX y. x=y"
   15.63  apply (rule allI)
   15.64  apply (rule exI)
   15.65  apply (rule refl)
   15.66  done
   15.67  
   15.68 -lemma "?p : EX y. ALL x. x=y"
   15.69 +schematic_lemma "?p : EX y. ALL x. x=y"
   15.70  apply (rule exI)
   15.71  apply (rule allI)
   15.72  apply (rule refl)?
   15.73  oops
   15.74  
   15.75  text {* Parallel lifting example. *}
   15.76 -lemma "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)"
   15.77 +schematic_lemma "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)"
   15.78  apply (rule exI allI)
   15.79  apply (rule exI allI)
   15.80  apply (rule exI allI)
   15.81 @@ -108,7 +108,7 @@
   15.82  apply (rule exI allI)
   15.83  oops
   15.84  
   15.85 -lemma
   15.86 +schematic_lemma
   15.87    assumes "p : (EX z. F(z)) & B"
   15.88    shows "?p : EX z. F(z) & B"
   15.89  apply (rule conjE)
   15.90 @@ -122,7 +122,7 @@
   15.91  done
   15.92  
   15.93  text {* A bigger demonstration of quantifiers -- not in the paper. *}
   15.94 -lemma "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
   15.95 +schematic_lemma "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
   15.96  apply (rule impI)
   15.97  apply (rule allI)
   15.98  apply (rule exE, assumption)
    16.1 --- a/src/FOLP/ex/If.thy	Fri Apr 23 23:33:48 2010 +0200
    16.2 +++ b/src/FOLP/ex/If.thy	Fri Apr 23 23:35:43 2010 +0200
    16.3 @@ -5,14 +5,14 @@
    16.4  definition "if" :: "[o,o,o]=>o" where
    16.5    "if(P,Q,R) == P&Q | ~P&R"
    16.6  
    16.7 -lemma ifI:
    16.8 +schematic_lemma ifI:
    16.9    assumes "!!x. x : P ==> f(x) : Q"  "!!x. x : ~P ==> g(x) : R"
   16.10    shows "?p : if(P,Q,R)"
   16.11  apply (unfold if_def)
   16.12  apply (tactic {* fast_tac (FOLP_cs addIs @{thms assms}) 1 *})
   16.13  done
   16.14  
   16.15 -lemma ifE:
   16.16 +schematic_lemma ifE:
   16.17    assumes 1: "p : if(P,Q,R)" and
   16.18      2: "!!x y. [| x : P; y : Q |] ==> f(x, y) : S" and
   16.19      3: "!!x y. [| x : ~P; y : R |] ==> g(x, y) : S"
   16.20 @@ -22,7 +22,7 @@
   16.21  apply (tactic {* fast_tac (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1 *})
   16.22  done
   16.23  
   16.24 -lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
   16.25 +schematic_lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
   16.26  apply (rule iffI)
   16.27  apply (erule ifE)
   16.28  apply (erule ifE)
   16.29 @@ -32,11 +32,11 @@
   16.30  
   16.31  ML {* val if_cs = FOLP_cs addSIs [@{thm ifI}] addSEs [@{thm ifE}] *}
   16.32  
   16.33 -lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
   16.34 +schematic_lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
   16.35  apply (tactic {* fast_tac if_cs 1 *})
   16.36  done
   16.37  
   16.38 -lemma nested_ifs: "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
   16.39 +schematic_lemma nested_ifs: "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
   16.40  apply (tactic {* fast_tac if_cs 1 *})
   16.41  done
   16.42  
    17.1 --- a/src/FOLP/ex/Intro.thy	Fri Apr 23 23:33:48 2010 +0200
    17.2 +++ b/src/FOLP/ex/Intro.thy	Fri Apr 23 23:35:43 2010 +0200
    17.3 @@ -13,7 +13,7 @@
    17.4  
    17.5  subsubsection {* Some simple backward proofs *}
    17.6  
    17.7 -lemma mythm: "?p : P|P --> P"
    17.8 +schematic_lemma mythm: "?p : P|P --> P"
    17.9  apply (rule impI)
   17.10  apply (rule disjE)
   17.11  prefer 3 apply (assumption)
   17.12 @@ -21,7 +21,7 @@
   17.13  apply assumption
   17.14  done
   17.15  
   17.16 -lemma "?p : (P & Q) | R --> (P | R)"
   17.17 +schematic_lemma "?p : (P & Q) | R --> (P | R)"
   17.18  apply (rule impI)
   17.19  apply (erule disjE)
   17.20  apply (drule conjunct1)
   17.21 @@ -31,7 +31,7 @@
   17.22  done
   17.23  
   17.24  (*Correct version, delaying use of "spec" until last*)
   17.25 -lemma "?p : (ALL x y. P(x,y)) --> (ALL z w. P(w,z))"
   17.26 +schematic_lemma "?p : (ALL x y. P(x,y)) --> (ALL z w. P(w,z))"
   17.27  apply (rule impI)
   17.28  apply (rule allI)
   17.29  apply (rule allI)
   17.30 @@ -43,13 +43,13 @@
   17.31  
   17.32  subsubsection {* Demonstration of @{text "fast"} *}
   17.33  
   17.34 -lemma "?p : (EX y. ALL x. J(y,x) <-> ~J(x,x))
   17.35 +schematic_lemma "?p : (EX y. ALL x. J(y,x) <-> ~J(x,x))
   17.36          -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))"
   17.37  apply (tactic {* fast_tac FOLP_cs 1 *})
   17.38  done
   17.39  
   17.40  
   17.41 -lemma "?p : ALL x. P(x,f(x)) <->
   17.42 +schematic_lemma "?p : ALL x. P(x,f(x)) <->
   17.43          (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
   17.44  apply (tactic {* fast_tac FOLP_cs 1 *})
   17.45  done
   17.46 @@ -57,7 +57,7 @@
   17.47  
   17.48  subsubsection {* Derivation of conjunction elimination rule *}
   17.49  
   17.50 -lemma
   17.51 +schematic_lemma
   17.52    assumes major: "p : P&Q"
   17.53      and minor: "!!x y. [| x : P; y : Q |] ==> f(x, y) : R"
   17.54    shows "?p : R"
   17.55 @@ -71,7 +71,7 @@
   17.56  
   17.57  text {* Derivation of negation introduction *}
   17.58  
   17.59 -lemma
   17.60 +schematic_lemma
   17.61    assumes "!!x. x : P ==> f(x) : False"
   17.62    shows "?p : ~ P"
   17.63  apply (unfold not_def)
   17.64 @@ -80,7 +80,7 @@
   17.65  apply assumption
   17.66  done
   17.67  
   17.68 -lemma
   17.69 +schematic_lemma
   17.70    assumes major: "p : ~P"
   17.71      and minor: "q : P"
   17.72    shows "?p : R"
   17.73 @@ -91,7 +91,7 @@
   17.74  done
   17.75  
   17.76  text {* Alternative proof of the result above *}
   17.77 -lemma
   17.78 +schematic_lemma
   17.79    assumes major: "p : ~P"
   17.80      and minor: "q : P"
   17.81    shows "?p : R"
    18.1 --- a/src/FOLP/ex/Intuitionistic.thy	Fri Apr 23 23:33:48 2010 +0200
    18.2 +++ b/src/FOLP/ex/Intuitionistic.thy	Fri Apr 23 23:35:43 2010 +0200
    18.3 @@ -30,39 +30,39 @@
    18.4  imports IFOLP
    18.5  begin
    18.6  
    18.7 -lemma "?p : ~~(P&Q) <-> ~~P & ~~Q"
    18.8 +schematic_lemma "?p : ~~(P&Q) <-> ~~P & ~~Q"
    18.9    by (tactic {* IntPr.fast_tac 1 *})
   18.10  
   18.11 -lemma "?p : ~~~P <-> ~P"
   18.12 +schematic_lemma "?p : ~~~P <-> ~P"
   18.13    by (tactic {* IntPr.fast_tac 1 *})
   18.14  
   18.15 -lemma "?p : ~~((P --> Q | R)  -->  (P-->Q) | (P-->R))"
   18.16 +schematic_lemma "?p : ~~((P --> Q | R)  -->  (P-->Q) | (P-->R))"
   18.17    by (tactic {* IntPr.fast_tac 1 *})
   18.18  
   18.19 -lemma "?p : (P<->Q) <-> (Q<->P)"
   18.20 +schematic_lemma "?p : (P<->Q) <-> (Q<->P)"
   18.21    by (tactic {* IntPr.fast_tac 1 *})
   18.22  
   18.23  
   18.24  subsection {* Lemmas for the propositional double-negation translation *}
   18.25  
   18.26 -lemma "?p : P --> ~~P"
   18.27 +schematic_lemma "?p : P --> ~~P"
   18.28    by (tactic {* IntPr.fast_tac 1 *})
   18.29  
   18.30 -lemma "?p : ~~(~~P --> P)"
   18.31 +schematic_lemma "?p : ~~(~~P --> P)"
   18.32    by (tactic {* IntPr.fast_tac 1 *})
   18.33  
   18.34 -lemma "?p : ~~P & ~~(P --> Q) --> ~~Q"
   18.35 +schematic_lemma "?p : ~~P & ~~(P --> Q) --> ~~Q"
   18.36    by (tactic {* IntPr.fast_tac 1 *})
   18.37  
   18.38  
   18.39  subsection {* The following are classically but not constructively valid *}
   18.40  
   18.41  (*The attempt to prove them terminates quickly!*)
   18.42 -lemma "?p : ((P-->Q) --> P)  -->  P"
   18.43 +schematic_lemma "?p : ((P-->Q) --> P)  -->  P"
   18.44    apply (tactic {* IntPr.fast_tac 1 *})?
   18.45    oops
   18.46  
   18.47 -lemma "?p : (P&Q-->R)  -->  (P-->R) | (Q-->R)"
   18.48 +schematic_lemma "?p : (P&Q-->R)  -->  (P-->R) | (Q-->R)"
   18.49    apply (tactic {* IntPr.fast_tac 1 *})?
   18.50    oops
   18.51  
   18.52 @@ -70,74 +70,74 @@
   18.53  subsection {* Intuitionistic FOL: propositional problems based on Pelletier *}
   18.54  
   18.55  text "Problem ~~1"
   18.56 -lemma "?p : ~~((P-->Q)  <->  (~Q --> ~P))"
   18.57 +schematic_lemma "?p : ~~((P-->Q)  <->  (~Q --> ~P))"
   18.58    by (tactic {* IntPr.fast_tac 1 *})
   18.59  
   18.60  text "Problem ~~2"
   18.61 -lemma "?p : ~~(~~P  <->  P)"
   18.62 +schematic_lemma "?p : ~~(~~P  <->  P)"
   18.63    by (tactic {* IntPr.fast_tac 1 *})
   18.64  
   18.65  text "Problem 3"
   18.66 -lemma "?p : ~(P-->Q) --> (Q-->P)"
   18.67 +schematic_lemma "?p : ~(P-->Q) --> (Q-->P)"
   18.68    by (tactic {* IntPr.fast_tac 1 *})
   18.69  
   18.70  text "Problem ~~4"
   18.71 -lemma "?p : ~~((~P-->Q)  <->  (~Q --> P))"
   18.72 +schematic_lemma "?p : ~~((~P-->Q)  <->  (~Q --> P))"
   18.73    by (tactic {* IntPr.fast_tac 1 *})
   18.74  
   18.75  text "Problem ~~5"
   18.76 -lemma "?p : ~~((P|Q-->P|R) --> P|(Q-->R))"
   18.77 +schematic_lemma "?p : ~~((P|Q-->P|R) --> P|(Q-->R))"
   18.78    by (tactic {* IntPr.fast_tac 1 *})
   18.79  
   18.80  text "Problem ~~6"
   18.81 -lemma "?p : ~~(P | ~P)"
   18.82 +schematic_lemma "?p : ~~(P | ~P)"
   18.83    by (tactic {* IntPr.fast_tac 1 *})
   18.84  
   18.85  text "Problem ~~7"
   18.86 -lemma "?p : ~~(P | ~~~P)"
   18.87 +schematic_lemma "?p : ~~(P | ~~~P)"
   18.88    by (tactic {* IntPr.fast_tac 1 *})
   18.89  
   18.90  text "Problem ~~8.  Peirce's law"
   18.91 -lemma "?p : ~~(((P-->Q) --> P)  -->  P)"
   18.92 +schematic_lemma "?p : ~~(((P-->Q) --> P)  -->  P)"
   18.93    by (tactic {* IntPr.fast_tac 1 *})
   18.94  
   18.95  text "Problem 9"
   18.96 -lemma "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
   18.97 +schematic_lemma "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
   18.98    by (tactic {* IntPr.fast_tac 1 *})
   18.99  
  18.100  text "Problem 10"
  18.101 -lemma "?p : (Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)"
  18.102 +schematic_lemma "?p : (Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)"
  18.103    by (tactic {* IntPr.fast_tac 1 *})
  18.104  
  18.105  text "11.  Proved in each direction (incorrectly, says Pelletier!!) "
  18.106 -lemma "?p : P<->P"
  18.107 +schematic_lemma "?p : P<->P"
  18.108    by (tactic {* IntPr.fast_tac 1 *})
  18.109  
  18.110  text "Problem ~~12.  Dijkstra's law  "
  18.111 -lemma "?p : ~~(((P <-> Q) <-> R)  <->  (P <-> (Q <-> R)))"
  18.112 +schematic_lemma "?p : ~~(((P <-> Q) <-> R)  <->  (P <-> (Q <-> R)))"
  18.113    by (tactic {* IntPr.fast_tac 1 *})
  18.114  
  18.115 -lemma "?p : ((P <-> Q) <-> R)  -->  ~~(P <-> (Q <-> R))"
  18.116 +schematic_lemma "?p : ((P <-> Q) <-> R)  -->  ~~(P <-> (Q <-> R))"
  18.117    by (tactic {* IntPr.fast_tac 1 *})
  18.118  
  18.119  text "Problem 13.  Distributive law"
  18.120 -lemma "?p : P | (Q & R)  <-> (P | Q) & (P | R)"
  18.121 +schematic_lemma "?p : P | (Q & R)  <-> (P | Q) & (P | R)"
  18.122    by (tactic {* IntPr.fast_tac 1 *})
  18.123  
  18.124  text "Problem ~~14"
  18.125 -lemma "?p : ~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))"
  18.126 +schematic_lemma "?p : ~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))"
  18.127    by (tactic {* IntPr.fast_tac 1 *})
  18.128  
  18.129  text "Problem ~~15"
  18.130 -lemma "?p : ~~((P --> Q) <-> (~P | Q))"
  18.131 +schematic_lemma "?p : ~~((P --> Q) <-> (~P | Q))"
  18.132    by (tactic {* IntPr.fast_tac 1 *})
  18.133  
  18.134  text "Problem ~~16"
  18.135 -lemma "?p : ~~((P-->Q) | (Q-->P))"
  18.136 +schematic_lemma "?p : ~~((P-->Q) | (Q-->P))"
  18.137    by (tactic {* IntPr.fast_tac 1 *})
  18.138  
  18.139  text "Problem ~~17"
  18.140 -lemma "?p : ~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))"
  18.141 +schematic_lemma "?p : ~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))"
  18.142    by (tactic {* IntPr.fast_tac 1 *})  -- slow
  18.143  
  18.144  
  18.145 @@ -145,43 +145,43 @@
  18.146  
  18.147  text "The converse is classical in the following implications..."
  18.148  
  18.149 -lemma "?p : (EX x. P(x)-->Q)  -->  (ALL x. P(x)) --> Q"
  18.150 +schematic_lemma "?p : (EX x. P(x)-->Q)  -->  (ALL x. P(x)) --> Q"
  18.151    by (tactic {* IntPr.fast_tac 1 *})
  18.152  
  18.153 -lemma "?p : ((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)"
  18.154 +schematic_lemma "?p : ((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)"
  18.155    by (tactic {* IntPr.fast_tac 1 *})
  18.156  
  18.157 -lemma "?p : ((ALL x. ~P(x))-->Q)  -->  ~ (ALL x. ~ (P(x)|Q))"
  18.158 +schematic_lemma "?p : ((ALL x. ~P(x))-->Q)  -->  ~ (ALL x. ~ (P(x)|Q))"
  18.159    by (tactic {* IntPr.fast_tac 1 *})
  18.160  
  18.161 -lemma "?p : (ALL x. P(x)) | Q  -->  (ALL x. P(x) | Q)"
  18.162 +schematic_lemma "?p : (ALL x. P(x)) | Q  -->  (ALL x. P(x) | Q)"
  18.163    by (tactic {* IntPr.fast_tac 1 *})
  18.164  
  18.165 -lemma "?p : (EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))"
  18.166 +schematic_lemma "?p : (EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))"
  18.167    by (tactic {* IntPr.fast_tac 1 *})
  18.168  
  18.169  
  18.170  text "The following are not constructively valid!"
  18.171  text "The attempt to prove them terminates quickly!"
  18.172  
  18.173 -lemma "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)"
  18.174 +schematic_lemma "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)"
  18.175    apply (tactic {* IntPr.fast_tac 1 *})?
  18.176    oops
  18.177  
  18.178 -lemma "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))"
  18.179 +schematic_lemma "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))"
  18.180    apply (tactic {* IntPr.fast_tac 1 *})?
  18.181    oops
  18.182  
  18.183 -lemma "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)"
  18.184 +schematic_lemma "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)"
  18.185    apply (tactic {* IntPr.fast_tac 1 *})?
  18.186    oops
  18.187  
  18.188 -lemma "?p : (ALL x. ~~P(x)) --> ~~(ALL x. P(x))"
  18.189 +schematic_lemma "?p : (ALL x. ~~P(x)) --> ~~(ALL x. P(x))"
  18.190    apply (tactic {* IntPr.fast_tac 1 *})?
  18.191    oops
  18.192  
  18.193  (*Classically but not intuitionistically valid.  Proved by a bug in 1986!*)
  18.194 -lemma "?p : EX x. Q(x) --> (ALL x. Q(x))"
  18.195 +schematic_lemma "?p : EX x. Q(x) --> (ALL x. Q(x))"
  18.196    apply (tactic {* IntPr.fast_tac 1 *})?
  18.197    oops
  18.198  
  18.199 @@ -194,32 +194,32 @@
  18.200  *}
  18.201  
  18.202  text "Problem ~~18"
  18.203 -lemma "?p : ~~(EX y. ALL x. P(y)-->P(x))" oops
  18.204 +schematic_lemma "?p : ~~(EX y. ALL x. P(y)-->P(x))" oops
  18.205  (*NOT PROVED*)
  18.206  
  18.207  text "Problem ~~19"
  18.208 -lemma "?p : ~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))" oops
  18.209 +schematic_lemma "?p : ~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))" oops
  18.210  (*NOT PROVED*)
  18.211  
  18.212  text "Problem 20"
  18.213 -lemma "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))      
  18.214 +schematic_lemma "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))      
  18.215      --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"
  18.216    by (tactic {* IntPr.fast_tac 1 *})
  18.217  
  18.218  text "Problem 21"
  18.219 -lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))" oops
  18.220 +schematic_lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))" oops
  18.221  (*NOT PROVED*)
  18.222  
  18.223  text "Problem 22"
  18.224 -lemma "?p : (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))"
  18.225 +schematic_lemma "?p : (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))"
  18.226    by (tactic {* IntPr.fast_tac 1 *})
  18.227  
  18.228  text "Problem ~~23"
  18.229 -lemma "?p : ~~ ((ALL x. P | Q(x))  <->  (P | (ALL x. Q(x))))"
  18.230 +schematic_lemma "?p : ~~ ((ALL x. P | Q(x))  <->  (P | (ALL x. Q(x))))"
  18.231    by (tactic {* IntPr.fast_tac 1 *})
  18.232  
  18.233  text "Problem 24"
  18.234 -lemma "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &   
  18.235 +schematic_lemma "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &   
  18.236       (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))   
  18.237      --> ~~(EX x. P(x)&R(x))"
  18.238  (*Not clear why fast_tac, best_tac, ASTAR and ITER_DEEPEN all take forever*)
  18.239 @@ -230,7 +230,7 @@
  18.240    done
  18.241  
  18.242  text "Problem 25"
  18.243 -lemma "?p : (EX x. P(x)) &   
  18.244 +schematic_lemma "?p : (EX x. P(x)) &   
  18.245          (ALL x. L(x) --> ~ (M(x) & R(x))) &   
  18.246          (ALL x. P(x) --> (M(x) & L(x))) &    
  18.247          ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))   
  18.248 @@ -238,69 +238,69 @@
  18.249    by (tactic "IntPr.best_tac 1")
  18.250  
  18.251  text "Problem 29.  Essentially the same as Principia Mathematica *11.71"
  18.252 -lemma "?p : (EX x. P(x)) & (EX y. Q(y))   
  18.253 +schematic_lemma "?p : (EX x. P(x)) & (EX y. Q(y))   
  18.254      --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->      
  18.255           (ALL x y. P(x) & Q(y) --> R(x) & S(y)))"
  18.256    by (tactic "IntPr.fast_tac 1")
  18.257  
  18.258  text "Problem ~~30"
  18.259 -lemma "?p : (ALL x. (P(x) | Q(x)) --> ~ R(x)) &  
  18.260 +schematic_lemma "?p : (ALL x. (P(x) | Q(x)) --> ~ R(x)) &  
  18.261          (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))   
  18.262      --> (ALL x. ~~S(x))"
  18.263    by (tactic "IntPr.fast_tac 1")
  18.264  
  18.265  text "Problem 31"
  18.266 -lemma "?p : ~(EX x. P(x) & (Q(x) | R(x))) &  
  18.267 +schematic_lemma "?p : ~(EX x. P(x) & (Q(x) | R(x))) &  
  18.268          (EX x. L(x) & P(x)) &  
  18.269          (ALL x. ~ R(x) --> M(x))   
  18.270      --> (EX x. L(x) & M(x))"
  18.271    by (tactic "IntPr.fast_tac 1")
  18.272  
  18.273  text "Problem 32"
  18.274 -lemma "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) &  
  18.275 +schematic_lemma "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) &  
  18.276          (ALL x. S(x) & R(x) --> L(x)) &  
  18.277          (ALL x. M(x) --> R(x))   
  18.278      --> (ALL x. P(x) & M(x) --> L(x))"
  18.279    by (tactic "IntPr.best_tac 1") -- slow
  18.280  
  18.281  text "Problem 39"
  18.282 -lemma "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
  18.283 +schematic_lemma "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
  18.284    by (tactic "IntPr.best_tac 1")
  18.285  
  18.286  text "Problem 40.  AMENDED"
  18.287 -lemma "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->   
  18.288 +schematic_lemma "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->   
  18.289                ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"
  18.290    by (tactic "IntPr.best_tac 1") -- slow
  18.291  
  18.292  text "Problem 44"
  18.293 -lemma "?p : (ALL x. f(x) -->                                    
  18.294 +schematic_lemma "?p : (ALL x. f(x) -->                                    
  18.295                (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &        
  18.296                (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                    
  18.297                --> (EX x. j(x) & ~f(x))"
  18.298    by (tactic "IntPr.best_tac 1")
  18.299  
  18.300  text "Problem 48"
  18.301 -lemma "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c"
  18.302 +schematic_lemma "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c"
  18.303    by (tactic "IntPr.best_tac 1")
  18.304  
  18.305  text "Problem 51"
  18.306 -lemma
  18.307 +schematic_lemma
  18.308      "?p : (EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->   
  18.309       (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)"
  18.310    by (tactic "IntPr.best_tac 1") -- {*60 seconds*}
  18.311  
  18.312  text "Problem 56"
  18.313 -lemma "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
  18.314 +schematic_lemma "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
  18.315    by (tactic "IntPr.best_tac 1")
  18.316  
  18.317  text "Problem 57"
  18.318 -lemma
  18.319 +schematic_lemma
  18.320      "?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &  
  18.321       (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))"
  18.322    by (tactic "IntPr.best_tac 1")
  18.323  
  18.324  text "Problem 60"
  18.325 -lemma "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
  18.326 +schematic_lemma "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
  18.327    by (tactic "IntPr.best_tac 1")
  18.328  
  18.329  end
    19.1 --- a/src/FOLP/ex/Nat.thy	Fri Apr 23 23:33:48 2010 +0200
    19.2 +++ b/src/FOLP/ex/Nat.thy	Fri Apr 23 23:35:43 2010 +0200
    19.3 @@ -44,7 +44,7 @@
    19.4  
    19.5  subsection {* Proofs about the natural numbers *}
    19.6  
    19.7 -lemma Suc_n_not_n: "?p : ~ (Suc(k) = k)"
    19.8 +schematic_lemma Suc_n_not_n: "?p : ~ (Suc(k) = k)"
    19.9  apply (rule_tac n = k in induct)
   19.10  apply (rule notI)
   19.11  apply (erule Suc_neq_0)
   19.12 @@ -53,7 +53,7 @@
   19.13  apply (erule Suc_inject)
   19.14  done
   19.15  
   19.16 -lemma "?p : (k+m)+n = k+(m+n)"
   19.17 +schematic_lemma "?p : (k+m)+n = k+(m+n)"
   19.18  apply (rule induct)
   19.19  back
   19.20  back
   19.21 @@ -63,23 +63,23 @@
   19.22  back
   19.23  oops
   19.24  
   19.25 -lemma add_0 [simp]: "?p : 0+n = n"
   19.26 +schematic_lemma add_0 [simp]: "?p : 0+n = n"
   19.27  apply (unfold add_def)
   19.28  apply (rule rec_0)
   19.29  done
   19.30  
   19.31 -lemma add_Suc [simp]: "?p : Suc(m)+n = Suc(m+n)"
   19.32 +schematic_lemma add_Suc [simp]: "?p : Suc(m)+n = Suc(m+n)"
   19.33  apply (unfold add_def)
   19.34  apply (rule rec_Suc)
   19.35  done
   19.36  
   19.37  
   19.38 -lemma Suc_cong: "p : x = y \<Longrightarrow> ?p : Suc(x) = Suc(y)"
   19.39 +schematic_lemma Suc_cong: "p : x = y \<Longrightarrow> ?p : Suc(x) = Suc(y)"
   19.40    apply (erule subst)
   19.41    apply (rule refl)
   19.42    done
   19.43  
   19.44 -lemma Plus_cong: "[| p : a = x;  q: b = y |] ==> ?p : a + b = x + y"
   19.45 +schematic_lemma Plus_cong: "[| p : a = x;  q: b = y |] ==> ?p : a + b = x + y"
   19.46    apply (erule subst, erule subst, rule refl)
   19.47    done
   19.48  
   19.49 @@ -89,19 +89,19 @@
   19.50    val add_ss = FOLP_ss addcongs @{thms nat_congs} addrews [@{thm add_0}, @{thm add_Suc}]
   19.51  *}
   19.52  
   19.53 -lemma add_assoc: "?p : (k+m)+n = k+(m+n)"
   19.54 +schematic_lemma add_assoc: "?p : (k+m)+n = k+(m+n)"
   19.55  apply (rule_tac n = k in induct)
   19.56  apply (tactic {* SIMP_TAC add_ss 1 *})
   19.57  apply (tactic {* ASM_SIMP_TAC add_ss 1 *})
   19.58  done
   19.59  
   19.60 -lemma add_0_right: "?p : m+0 = m"
   19.61 +schematic_lemma add_0_right: "?p : m+0 = m"
   19.62  apply (rule_tac n = m in induct)
   19.63  apply (tactic {* SIMP_TAC add_ss 1 *})
   19.64  apply (tactic {* ASM_SIMP_TAC add_ss 1 *})
   19.65  done
   19.66  
   19.67 -lemma add_Suc_right: "?p : m+Suc(n) = Suc(m+n)"
   19.68 +schematic_lemma add_Suc_right: "?p : m+Suc(n) = Suc(m+n)"
   19.69  apply (rule_tac n = m in induct)
   19.70  apply (tactic {* ALLGOALS (ASM_SIMP_TAC add_ss) *})
   19.71  done
    20.1 --- a/src/FOLP/ex/Propositional_Cla.thy	Fri Apr 23 23:33:48 2010 +0200
    20.2 +++ b/src/FOLP/ex/Propositional_Cla.thy	Fri Apr 23 23:35:43 2010 +0200
    20.3 @@ -11,103 +11,103 @@
    20.4  
    20.5  
    20.6  text "commutative laws of & and | "
    20.7 -lemma "?p : P & Q  -->  Q & P"
    20.8 +schematic_lemma "?p : P & Q  -->  Q & P"
    20.9    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   20.10  
   20.11 -lemma "?p : P | Q  -->  Q | P"
   20.12 +schematic_lemma "?p : P | Q  -->  Q | P"
   20.13    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   20.14  
   20.15  
   20.16  text "associative laws of & and | "
   20.17 -lemma "?p : (P & Q) & R  -->  P & (Q & R)"
   20.18 +schematic_lemma "?p : (P & Q) & R  -->  P & (Q & R)"
   20.19    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   20.20  
   20.21 -lemma "?p : (P | Q) | R  -->  P | (Q | R)"
   20.22 +schematic_lemma "?p : (P | Q) | R  -->  P | (Q | R)"
   20.23    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   20.24  
   20.25  
   20.26  text "distributive laws of & and | "
   20.27 -lemma "?p : (P & Q) | R  --> (P | R) & (Q | R)"
   20.28 +schematic_lemma "?p : (P & Q) | R  --> (P | R) & (Q | R)"
   20.29    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   20.30  
   20.31 -lemma "?p : (P | R) & (Q | R)  --> (P & Q) | R"
   20.32 +schematic_lemma "?p : (P | R) & (Q | R)  --> (P & Q) | R"
   20.33    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   20.34  
   20.35 -lemma "?p : (P | Q) & R  --> (P & R) | (Q & R)"
   20.36 +schematic_lemma "?p : (P | Q) & R  --> (P & R) | (Q & R)"
   20.37    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   20.38  
   20.39  
   20.40 -lemma "?p : (P & R) | (Q & R)  --> (P | Q) & R"
   20.41 +schematic_lemma "?p : (P & R) | (Q & R)  --> (P | Q) & R"
   20.42    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   20.43  
   20.44  
   20.45  text "Laws involving implication"
   20.46  
   20.47 -lemma "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)"
   20.48 +schematic_lemma "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)"
   20.49    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   20.50  
   20.51 -lemma "?p : (P & Q --> R) <-> (P--> (Q-->R))"
   20.52 +schematic_lemma "?p : (P & Q --> R) <-> (P--> (Q-->R))"
   20.53    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   20.54  
   20.55 -lemma "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
   20.56 +schematic_lemma "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
   20.57    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   20.58  
   20.59 -lemma "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
   20.60 +schematic_lemma "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
   20.61    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   20.62  
   20.63 -lemma "?p : (P --> Q & R) <-> (P-->Q)  &  (P-->R)"
   20.64 +schematic_lemma "?p : (P --> Q & R) <-> (P-->Q)  &  (P-->R)"
   20.65    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   20.66  
   20.67  
   20.68  text "Propositions-as-types"
   20.69  
   20.70  (*The combinator K*)
   20.71 -lemma "?p : P --> (Q --> P)"
   20.72 +schematic_lemma "?p : P --> (Q --> P)"
   20.73    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   20.74  
   20.75  (*The combinator S*)
   20.76 -lemma "?p : (P-->Q-->R)  --> (P-->Q) --> (P-->R)"
   20.77 +schematic_lemma "?p : (P-->Q-->R)  --> (P-->Q) --> (P-->R)"
   20.78    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   20.79  
   20.80  
   20.81  (*Converse is classical*)
   20.82 -lemma "?p : (P-->Q) | (P-->R)  -->  (P --> Q | R)"
   20.83 +schematic_lemma "?p : (P-->Q) | (P-->R)  -->  (P --> Q | R)"
   20.84    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   20.85  
   20.86 -lemma "?p : (P-->Q)  -->  (~Q --> ~P)"
   20.87 +schematic_lemma "?p : (P-->Q)  -->  (~Q --> ~P)"
   20.88    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   20.89  
   20.90  
   20.91  text "Schwichtenberg's examples (via T. Nipkow)"
   20.92  
   20.93 -lemma stab_imp: "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
   20.94 +schematic_lemma stab_imp: "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
   20.95    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   20.96  
   20.97 -lemma stab_to_peirce: "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)  
   20.98 +schematic_lemma stab_to_peirce: "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)  
   20.99                --> ((P --> Q) --> P) --> P"
  20.100    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
  20.101  
  20.102 -lemma peirce_imp1: "?p : (((Q --> R) --> Q) --> Q)  
  20.103 +schematic_lemma peirce_imp1: "?p : (((Q --> R) --> Q) --> Q)  
  20.104                 --> (((P --> Q) --> R) --> P --> Q) --> P --> Q"
  20.105    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
  20.106    
  20.107 -lemma peirce_imp2: "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
  20.108 +schematic_lemma peirce_imp2: "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
  20.109    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
  20.110  
  20.111 -lemma mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q"
  20.112 +schematic_lemma mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q"
  20.113    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
  20.114  
  20.115 -lemma mints_solovev: "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
  20.116 +schematic_lemma mints_solovev: "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
  20.117    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
  20.118  
  20.119 -lemma tatsuta: "?p : (((P7 --> P1) --> P10) --> P4 --> P5)  
  20.120 +schematic_lemma tatsuta: "?p : (((P7 --> P1) --> P10) --> P4 --> P5)  
  20.121            --> (((P8 --> P2) --> P9) --> P3 --> P10)  
  20.122            --> (P1 --> P8) --> P6 --> P7  
  20.123            --> (((P3 --> P2) --> P9) --> P4)  
  20.124            --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5"
  20.125    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
  20.126  
  20.127 -lemma tatsuta1: "?p : (((P8 --> P2) --> P9) --> P3 --> P10)  
  20.128 +schematic_lemma tatsuta1: "?p : (((P8 --> P2) --> P9) --> P3 --> P10)  
  20.129       --> (((P3 --> P2) --> P9) --> P4)  
  20.130       --> (((P6 --> P1) --> P2) --> P9)  
  20.131       --> (((P7 --> P1) --> P10) --> P4 --> P5)  
    21.1 --- a/src/FOLP/ex/Propositional_Int.thy	Fri Apr 23 23:33:48 2010 +0200
    21.2 +++ b/src/FOLP/ex/Propositional_Int.thy	Fri Apr 23 23:35:43 2010 +0200
    21.3 @@ -11,103 +11,103 @@
    21.4  
    21.5  
    21.6  text "commutative laws of & and | "
    21.7 -lemma "?p : P & Q  -->  Q & P"
    21.8 +schematic_lemma "?p : P & Q  -->  Q & P"
    21.9    by (tactic {* IntPr.fast_tac 1 *})
   21.10  
   21.11 -lemma "?p : P | Q  -->  Q | P"
   21.12 +schematic_lemma "?p : P | Q  -->  Q | P"
   21.13    by (tactic {* IntPr.fast_tac 1 *})
   21.14  
   21.15  
   21.16  text "associative laws of & and | "
   21.17 -lemma "?p : (P & Q) & R  -->  P & (Q & R)"
   21.18 +schematic_lemma "?p : (P & Q) & R  -->  P & (Q & R)"
   21.19    by (tactic {* IntPr.fast_tac 1 *})
   21.20  
   21.21 -lemma "?p : (P | Q) | R  -->  P | (Q | R)"
   21.22 +schematic_lemma "?p : (P | Q) | R  -->  P | (Q | R)"
   21.23    by (tactic {* IntPr.fast_tac 1 *})
   21.24  
   21.25  
   21.26  text "distributive laws of & and | "
   21.27 -lemma "?p : (P & Q) | R  --> (P | R) & (Q | R)"
   21.28 +schematic_lemma "?p : (P & Q) | R  --> (P | R) & (Q | R)"
   21.29    by (tactic {* IntPr.fast_tac 1 *})
   21.30  
   21.31 -lemma "?p : (P | R) & (Q | R)  --> (P & Q) | R"
   21.32 +schematic_lemma "?p : (P | R) & (Q | R)  --> (P & Q) | R"
   21.33    by (tactic {* IntPr.fast_tac 1 *})
   21.34  
   21.35 -lemma "?p : (P | Q) & R  --> (P & R) | (Q & R)"
   21.36 +schematic_lemma "?p : (P | Q) & R  --> (P & R) | (Q & R)"
   21.37    by (tactic {* IntPr.fast_tac 1 *})
   21.38  
   21.39  
   21.40 -lemma "?p : (P & R) | (Q & R)  --> (P | Q) & R"
   21.41 +schematic_lemma "?p : (P & R) | (Q & R)  --> (P | Q) & R"
   21.42    by (tactic {* IntPr.fast_tac 1 *})
   21.43  
   21.44  
   21.45  text "Laws involving implication"
   21.46  
   21.47 -lemma "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)"
   21.48 +schematic_lemma "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)"
   21.49    by (tactic {* IntPr.fast_tac 1 *})
   21.50  
   21.51 -lemma "?p : (P & Q --> R) <-> (P--> (Q-->R))"
   21.52 +schematic_lemma "?p : (P & Q --> R) <-> (P--> (Q-->R))"
   21.53    by (tactic {* IntPr.fast_tac 1 *})
   21.54  
   21.55 -lemma "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
   21.56 +schematic_lemma "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
   21.57    by (tactic {* IntPr.fast_tac 1 *})
   21.58  
   21.59 -lemma "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
   21.60 +schematic_lemma "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
   21.61    by (tactic {* IntPr.fast_tac 1 *})
   21.62  
   21.63 -lemma "?p : (P --> Q & R) <-> (P-->Q)  &  (P-->R)"
   21.64 +schematic_lemma "?p : (P --> Q & R) <-> (P-->Q)  &  (P-->R)"
   21.65    by (tactic {* IntPr.fast_tac 1 *})
   21.66  
   21.67  
   21.68  text "Propositions-as-types"
   21.69  
   21.70  (*The combinator K*)
   21.71 -lemma "?p : P --> (Q --> P)"
   21.72 +schematic_lemma "?p : P --> (Q --> P)"
   21.73    by (tactic {* IntPr.fast_tac 1 *})
   21.74  
   21.75  (*The combinator S*)
   21.76 -lemma "?p : (P-->Q-->R)  --> (P-->Q) --> (P-->R)"
   21.77 +schematic_lemma "?p : (P-->Q-->R)  --> (P-->Q) --> (P-->R)"
   21.78    by (tactic {* IntPr.fast_tac 1 *})
   21.79  
   21.80  
   21.81  (*Converse is classical*)
   21.82 -lemma "?p : (P-->Q) | (P-->R)  -->  (P --> Q | R)"
   21.83 +schematic_lemma "?p : (P-->Q) | (P-->R)  -->  (P --> Q | R)"
   21.84    by (tactic {* IntPr.fast_tac 1 *})
   21.85  
   21.86 -lemma "?p : (P-->Q)  -->  (~Q --> ~P)"
   21.87 +schematic_lemma "?p : (P-->Q)  -->  (~Q --> ~P)"
   21.88    by (tactic {* IntPr.fast_tac 1 *})
   21.89  
   21.90  
   21.91  text "Schwichtenberg's examples (via T. Nipkow)"
   21.92  
   21.93 -lemma stab_imp: "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
   21.94 +schematic_lemma stab_imp: "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
   21.95    by (tactic {* IntPr.fast_tac 1 *})
   21.96  
   21.97 -lemma stab_to_peirce: "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)  
   21.98 +schematic_lemma stab_to_peirce: "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)  
   21.99                --> ((P --> Q) --> P) --> P"
  21.100    by (tactic {* IntPr.fast_tac 1 *})
  21.101  
  21.102 -lemma peirce_imp1: "?p : (((Q --> R) --> Q) --> Q)  
  21.103 +schematic_lemma peirce_imp1: "?p : (((Q --> R) --> Q) --> Q)  
  21.104                 --> (((P --> Q) --> R) --> P --> Q) --> P --> Q"
  21.105    by (tactic {* IntPr.fast_tac 1 *})
  21.106    
  21.107 -lemma peirce_imp2: "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
  21.108 +schematic_lemma peirce_imp2: "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
  21.109    by (tactic {* IntPr.fast_tac 1 *})
  21.110  
  21.111 -lemma mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q"
  21.112 +schematic_lemma mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q"
  21.113    by (tactic {* IntPr.fast_tac 1 *})
  21.114  
  21.115 -lemma mints_solovev: "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
  21.116 +schematic_lemma mints_solovev: "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
  21.117    by (tactic {* IntPr.fast_tac 1 *})
  21.118  
  21.119 -lemma tatsuta: "?p : (((P7 --> P1) --> P10) --> P4 --> P5)  
  21.120 +schematic_lemma tatsuta: "?p : (((P7 --> P1) --> P10) --> P4 --> P5)  
  21.121            --> (((P8 --> P2) --> P9) --> P3 --> P10)  
  21.122            --> (P1 --> P8) --> P6 --> P7  
  21.123            --> (((P3 --> P2) --> P9) --> P4)  
  21.124            --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5"
  21.125    by (tactic {* IntPr.fast_tac 1 *})
  21.126  
  21.127 -lemma tatsuta1: "?p : (((P8 --> P2) --> P9) --> P3 --> P10)  
  21.128 +schematic_lemma tatsuta1: "?p : (((P8 --> P2) --> P9) --> P3 --> P10)  
  21.129       --> (((P3 --> P2) --> P9) --> P4)  
  21.130       --> (((P6 --> P1) --> P2) --> P9)  
  21.131       --> (((P7 --> P1) --> P10) --> P4 --> P5)  
    22.1 --- a/src/FOLP/ex/Quantifiers_Cla.thy	Fri Apr 23 23:33:48 2010 +0200
    22.2 +++ b/src/FOLP/ex/Quantifiers_Cla.thy	Fri Apr 23 23:35:43 2010 +0200
    22.3 @@ -10,92 +10,92 @@
    22.4  imports FOLP
    22.5  begin
    22.6  
    22.7 -lemma "?p : (ALL x y. P(x,y))  -->  (ALL y x. P(x,y))"
    22.8 +schematic_lemma "?p : (ALL x y. P(x,y))  -->  (ALL y x. P(x,y))"
    22.9    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   22.10  
   22.11 -lemma "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))"
   22.12 +schematic_lemma "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))"
   22.13    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   22.14  
   22.15  
   22.16  (*Converse is false*)
   22.17 -lemma "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
   22.18 +schematic_lemma "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
   22.19    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   22.20  
   22.21 -lemma "?p : (ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))"
   22.22 +schematic_lemma "?p : (ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))"
   22.23    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   22.24  
   22.25  
   22.26 -lemma "?p : (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)"
   22.27 +schematic_lemma "?p : (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)"
   22.28    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   22.29  
   22.30  
   22.31  text "Some harder ones"
   22.32  
   22.33 -lemma "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
   22.34 +schematic_lemma "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
   22.35    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   22.36  
   22.37  (*Converse is false*)
   22.38 -lemma "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))"
   22.39 +schematic_lemma "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))"
   22.40    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   22.41  
   22.42  
   22.43  text "Basic test of quantifier reasoning"
   22.44  (*TRUE*)
   22.45 -lemma "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
   22.46 +schematic_lemma "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
   22.47    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   22.48  
   22.49 -lemma "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
   22.50 +schematic_lemma "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
   22.51    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   22.52  
   22.53  
   22.54  text "The following should fail, as they are false!"
   22.55  
   22.56 -lemma "?p : (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))"
   22.57 +schematic_lemma "?p : (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))"
   22.58    apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
   22.59    oops
   22.60  
   22.61 -lemma "?p : (EX x. Q(x))  -->  (ALL x. Q(x))"
   22.62 +schematic_lemma "?p : (EX x. Q(x))  -->  (ALL x. Q(x))"
   22.63    apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
   22.64    oops
   22.65  
   22.66 -lemma "?p : P(?a) --> (ALL x. P(x))"
   22.67 +schematic_lemma "?p : P(?a) --> (ALL x. P(x))"
   22.68    apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
   22.69    oops
   22.70  
   22.71 -lemma "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
   22.72 +schematic_lemma "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
   22.73    apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
   22.74    oops
   22.75  
   22.76  
   22.77  text "Back to things that are provable..."
   22.78  
   22.79 -lemma "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
   22.80 +schematic_lemma "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
   22.81    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   22.82  
   22.83  
   22.84  (*An example of why exI should be delayed as long as possible*)
   22.85 -lemma "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
   22.86 +schematic_lemma "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
   22.87    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   22.88  
   22.89 -lemma "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
   22.90 +schematic_lemma "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
   22.91    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   22.92  
   22.93 -lemma "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
   22.94 +schematic_lemma "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
   22.95    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   22.96  
   22.97  
   22.98  text "Some slow ones"
   22.99  
  22.100  (*Principia Mathematica *11.53  *)
  22.101 -lemma "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
  22.102 +schematic_lemma "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
  22.103    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
  22.104  
  22.105  (*Principia Mathematica *11.55  *)
  22.106 -lemma "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
  22.107 +schematic_lemma "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
  22.108    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
  22.109  
  22.110  (*Principia Mathematica *11.61  *)
  22.111 -lemma "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
  22.112 +schematic_lemma "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
  22.113    by (tactic {* Cla.fast_tac FOLP_cs 1 *})
  22.114  
  22.115  end
    23.1 --- a/src/FOLP/ex/Quantifiers_Int.thy	Fri Apr 23 23:33:48 2010 +0200
    23.2 +++ b/src/FOLP/ex/Quantifiers_Int.thy	Fri Apr 23 23:35:43 2010 +0200
    23.3 @@ -10,92 +10,92 @@
    23.4  imports IFOLP
    23.5  begin
    23.6  
    23.7 -lemma "?p : (ALL x y. P(x,y))  -->  (ALL y x. P(x,y))"
    23.8 +schematic_lemma "?p : (ALL x y. P(x,y))  -->  (ALL y x. P(x,y))"
    23.9    by (tactic {* IntPr.fast_tac 1 *})
   23.10  
   23.11 -lemma "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))"
   23.12 +schematic_lemma "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))"
   23.13    by (tactic {* IntPr.fast_tac 1 *})
   23.14  
   23.15  
   23.16  (*Converse is false*)
   23.17 -lemma "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
   23.18 +schematic_lemma "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
   23.19    by (tactic {* IntPr.fast_tac 1 *})
   23.20  
   23.21 -lemma "?p : (ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))"
   23.22 +schematic_lemma "?p : (ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))"
   23.23    by (tactic {* IntPr.fast_tac 1 *})
   23.24  
   23.25  
   23.26 -lemma "?p : (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)"
   23.27 +schematic_lemma "?p : (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)"
   23.28    by (tactic {* IntPr.fast_tac 1 *})
   23.29  
   23.30  
   23.31  text "Some harder ones"
   23.32  
   23.33 -lemma "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
   23.34 +schematic_lemma "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
   23.35    by (tactic {* IntPr.fast_tac 1 *})
   23.36  
   23.37  (*Converse is false*)
   23.38 -lemma "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))"
   23.39 +schematic_lemma "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))"
   23.40    by (tactic {* IntPr.fast_tac 1 *})
   23.41  
   23.42  
   23.43  text "Basic test of quantifier reasoning"
   23.44  (*TRUE*)
   23.45 -lemma "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
   23.46 +schematic_lemma "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
   23.47    by (tactic {* IntPr.fast_tac 1 *})
   23.48  
   23.49 -lemma "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
   23.50 +schematic_lemma "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
   23.51    by (tactic {* IntPr.fast_tac 1 *})
   23.52  
   23.53  
   23.54  text "The following should fail, as they are false!"
   23.55  
   23.56 -lemma "?p : (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))"
   23.57 +schematic_lemma "?p : (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))"
   23.58    apply (tactic {* IntPr.fast_tac 1 *})?
   23.59    oops
   23.60  
   23.61 -lemma "?p : (EX x. Q(x))  -->  (ALL x. Q(x))"
   23.62 +schematic_lemma "?p : (EX x. Q(x))  -->  (ALL x. Q(x))"
   23.63    apply (tactic {* IntPr.fast_tac 1 *})?
   23.64    oops
   23.65  
   23.66 -lemma "?p : P(?a) --> (ALL x. P(x))"
   23.67 +schematic_lemma "?p : P(?a) --> (ALL x. P(x))"
   23.68    apply (tactic {* IntPr.fast_tac 1 *})?
   23.69    oops
   23.70  
   23.71 -lemma "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
   23.72 +schematic_lemma "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
   23.73    apply (tactic {* IntPr.fast_tac 1 *})?
   23.74    oops
   23.75  
   23.76  
   23.77  text "Back to things that are provable..."
   23.78  
   23.79 -lemma "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
   23.80 +schematic_lemma "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
   23.81    by (tactic {* IntPr.fast_tac 1 *})
   23.82  
   23.83  
   23.84  (*An example of why exI should be delayed as long as possible*)
   23.85 -lemma "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
   23.86 +schematic_lemma "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
   23.87    by (tactic {* IntPr.fast_tac 1 *})
   23.88  
   23.89 -lemma "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
   23.90 +schematic_lemma "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
   23.91    by (tactic {* IntPr.fast_tac 1 *})
   23.92  
   23.93 -lemma "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
   23.94 +schematic_lemma "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
   23.95    by (tactic {* IntPr.fast_tac 1 *})
   23.96  
   23.97  
   23.98  text "Some slow ones"
   23.99  
  23.100  (*Principia Mathematica *11.53  *)
  23.101 -lemma "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
  23.102 +schematic_lemma "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
  23.103    by (tactic {* IntPr.fast_tac 1 *})
  23.104  
  23.105  (*Principia Mathematica *11.55  *)
  23.106 -lemma "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
  23.107 +schematic_lemma "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
  23.108    by (tactic {* IntPr.fast_tac 1 *})
  23.109  
  23.110  (*Principia Mathematica *11.61  *)
  23.111 -lemma "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
  23.112 +schematic_lemma "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
  23.113    by (tactic {* IntPr.fast_tac 1 *})
  23.114  
  23.115  end
    24.1 --- a/src/HOL/Bali/Example.thy	Fri Apr 23 23:33:48 2010 +0200
    24.2 +++ b/src/HOL/Bali/Example.thy	Fri Apr 23 23:35:43 2010 +0200
    24.3 @@ -1070,7 +1070,7 @@
    24.4  
    24.5  section "well-typedness"
    24.6  
    24.7 -lemma wt_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
    24.8 +schematic_lemma wt_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
    24.9  apply (unfold test_def arr_viewed_from_def)
   24.10  (* ?pTs = [Class Base] *)
   24.11  apply (rule wtIs (* ;; *))
   24.12 @@ -1122,7 +1122,7 @@
   24.13  
   24.14  section "definite assignment"
   24.15  
   24.16 -lemma da_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>
   24.17 +schematic_lemma da_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>
   24.18                    \<turnstile>{} \<guillemotright>\<langle>test ?pTs\<rangle>\<guillemotright> \<lparr>nrm={VName e},brk=\<lambda> l. UNIV\<rparr>"
   24.19  apply (unfold test_def arr_viewed_from_def)
   24.20  apply (rule da.Comp)
   24.21 @@ -1241,7 +1241,7 @@
   24.22  
   24.23  
   24.24  declare Pair_eq [simp del]
   24.25 -lemma exec_test: 
   24.26 +schematic_lemma exec_test: 
   24.27  "\<lbrakk>the (new_Addr (heap  s1)) = a;  
   24.28    the (new_Addr (heap ?s2)) = b;  
   24.29    the (new_Addr (heap ?s3)) = c\<rbrakk> \<Longrightarrow>  
    25.1 --- a/src/HOL/Lambda/Type.thy	Fri Apr 23 23:33:48 2010 +0200
    25.2 +++ b/src/HOL/Lambda/Type.thy	Fri Apr 23 23:35:43 2010 +0200
    25.3 @@ -83,10 +83,10 @@
    25.4  
    25.5  subsection {* Some examples *}
    25.6  
    25.7 -lemma "e \<turnstile> Abs (Abs (Abs (Var 1 \<degree> (Var 2 \<degree> Var 1 \<degree> Var 0)))) : ?T"
    25.8 +schematic_lemma "e \<turnstile> Abs (Abs (Abs (Var 1 \<degree> (Var 2 \<degree> Var 1 \<degree> Var 0)))) : ?T"
    25.9    by force
   25.10  
   25.11 -lemma "e \<turnstile> Abs (Abs (Abs (Var 2 \<degree> Var 0 \<degree> (Var 1 \<degree> Var 0)))) : ?T"
   25.12 +schematic_lemma "e \<turnstile> Abs (Abs (Abs (Var 2 \<degree> Var 0 \<degree> (Var 1 \<degree> Var 0)))) : ?T"
   25.13    by force
   25.14  
   25.15  
    26.1 --- a/src/HOL/MicroJava/J/Example.thy	Fri Apr 23 23:33:48 2010 +0200
    26.2 +++ b/src/HOL/MicroJava/J/Example.thy	Fri Apr 23 23:35:43 2010 +0200
    26.3 @@ -371,7 +371,7 @@
    26.4  done
    26.5  
    26.6  ML {* val t = resolve_tac @{thms ty_expr_ty_exprs_wt_stmt.intros} 1 *}
    26.7 -lemma wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile>  
    26.8 +schematic_lemma wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile>  
    26.9    Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\<surd>"
   26.10  apply (tactic t) -- ";;"
   26.11  apply  (tactic t) -- "Expr"
   26.12 @@ -400,7 +400,7 @@
   26.13  
   26.14  declare split_if [split del]
   26.15  declare init_vars_def [simp] c_hupd_def [simp] cast_ok_def [simp]
   26.16 -lemma exec_test: 
   26.17 +schematic_lemma exec_test: 
   26.18  " [|new_Addr (heap (snd s0)) = (a, None)|] ==>  
   26.19    tprg\<turnstile>s0 -test-> ?s"
   26.20  apply (unfold test_def)
    27.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Fri Apr 23 23:33:48 2010 +0200
    27.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Fri Apr 23 23:35:43 2010 +0200
    27.3 @@ -325,27 +325,27 @@
    27.4  
    27.5  subsection {* Schematic Variables *}
    27.6  
    27.7 -lemma "x = ?x"
    27.8 +schematic_lemma "x = ?x"
    27.9  nitpick [expect = none]
   27.10  by auto
   27.11  
   27.12 -lemma "\<forall>x. x = ?x"
   27.13 +schematic_lemma "\<forall>x. x = ?x"
   27.14  nitpick [expect = genuine]
   27.15  oops
   27.16  
   27.17 -lemma "\<exists>x. x = ?x"
   27.18 +schematic_lemma "\<exists>x. x = ?x"
   27.19  nitpick [expect = none]
   27.20  by auto
   27.21  
   27.22 -lemma "\<exists>x\<Colon>'a \<Rightarrow> 'b. x = ?x"
   27.23 +schematic_lemma "\<exists>x\<Colon>'a \<Rightarrow> 'b. x = ?x"
   27.24  nitpick [expect = none]
   27.25  by auto
   27.26  
   27.27 -lemma "\<forall>x. ?x = ?y"
   27.28 +schematic_lemma "\<forall>x. ?x = ?y"
   27.29  nitpick [expect = none]
   27.30  by auto
   27.31  
   27.32 -lemma "\<exists>x. ?x = ?y"
   27.33 +schematic_lemma "\<exists>x. ?x = ?y"
   27.34  nitpick [expect = none]
   27.35  by auto
   27.36  
    28.1 --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Fri Apr 23 23:33:48 2010 +0200
    28.2 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Fri Apr 23 23:35:43 2010 +0200
    28.3 @@ -340,12 +340,12 @@
    28.4  
    28.5  subsubsection {* Schematic Variables *}
    28.6  
    28.7 -lemma "?P"
    28.8 +schematic_lemma "?P"
    28.9  nitpick [expect = none]
   28.10  apply auto
   28.11  done
   28.12  
   28.13 -lemma "x = ?y"
   28.14 +schematic_lemma "x = ?y"
   28.15  nitpick [expect = none]
   28.16  apply auto
   28.17  done
    29.1 --- a/src/HOL/Prolog/Func.thy	Fri Apr 23 23:33:48 2010 +0200
    29.2 +++ b/src/HOL/Prolog/Func.thy	Fri Apr 23 23:35:43 2010 +0200
    29.3 @@ -58,11 +58,11 @@
    29.4  
    29.5  lemmas prog_Func = eval
    29.6  
    29.7 -lemma "eval ((S (S Z)) + (S Z)) ?X"
    29.8 +schematic_lemma "eval ((S (S Z)) + (S Z)) ?X"
    29.9    apply (prolog prog_Func)
   29.10    done
   29.11  
   29.12 -lemma "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z)
   29.13 +schematic_lemma "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z)
   29.14                          (n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X"
   29.15    apply (prolog prog_Func)
   29.16    done
    30.1 --- a/src/HOL/Prolog/Test.thy	Fri Apr 23 23:33:48 2010 +0200
    30.2 +++ b/src/HOL/Prolog/Test.thy	Fri Apr 23 23:35:43 2010 +0200
    30.3 @@ -81,7 +81,7 @@
    30.4  
    30.5  lemmas prog_Test = append reverse mappred mapfun age eq bag_appl
    30.6  
    30.7 -lemma "append ?x ?y [a,b,c,d]"
    30.8 +schematic_lemma "append ?x ?y [a,b,c,d]"
    30.9    apply (prolog prog_Test)
   30.10    back
   30.11    back
   30.12 @@ -89,56 +89,56 @@
   30.13    back
   30.14    done
   30.15  
   30.16 -lemma "append [a,b] y ?L"
   30.17 +schematic_lemma "append [a,b] y ?L"
   30.18    apply (prolog prog_Test)
   30.19    done
   30.20  
   30.21 -lemma "!y. append [a,b] y (?L y)"
   30.22 +schematic_lemma "!y. append [a,b] y (?L y)"
   30.23    apply (prolog prog_Test)
   30.24    done
   30.25  
   30.26 -lemma "reverse [] ?L"
   30.27 +schematic_lemma "reverse [] ?L"
   30.28    apply (prolog prog_Test)
   30.29    done
   30.30  
   30.31 -lemma "reverse [23] ?L"
   30.32 +schematic_lemma "reverse [23] ?L"
   30.33    apply (prolog prog_Test)
   30.34    done
   30.35  
   30.36 -lemma "reverse [23,24,?x] ?L"
   30.37 +schematic_lemma "reverse [23,24,?x] ?L"
   30.38    apply (prolog prog_Test)
   30.39    done
   30.40  
   30.41 -lemma "reverse ?L [23,24,?x]"
   30.42 +schematic_lemma "reverse ?L [23,24,?x]"
   30.43    apply (prolog prog_Test)
   30.44    done
   30.45  
   30.46 -lemma "mappred age ?x [23,24]"
   30.47 +schematic_lemma "mappred age ?x [23,24]"
   30.48    apply (prolog prog_Test)
   30.49    back
   30.50    done
   30.51  
   30.52 -lemma "mappred (%x y. ? z. age z y) ?x [23,24]"
   30.53 +schematic_lemma "mappred (%x y. ? z. age z y) ?x [23,24]"
   30.54    apply (prolog prog_Test)
   30.55    done
   30.56  
   30.57 -lemma "mappred ?P [bob,sue] [24,23]"
   30.58 +schematic_lemma "mappred ?P [bob,sue] [24,23]"
   30.59    apply (prolog prog_Test)
   30.60    done
   30.61  
   30.62 -lemma "mapfun f [bob,bob,sue] [?x,?y,?z]"
   30.63 +schematic_lemma "mapfun f [bob,bob,sue] [?x,?y,?z]"
   30.64    apply (prolog prog_Test)
   30.65    done
   30.66  
   30.67 -lemma "mapfun (%x. h x 25) [bob,sue] ?L"
   30.68 +schematic_lemma "mapfun (%x. h x 25) [bob,sue] ?L"
   30.69    apply (prolog prog_Test)
   30.70    done
   30.71  
   30.72 -lemma "mapfun ?F [24,25] [h bob 24,h bob 25]"
   30.73 +schematic_lemma "mapfun ?F [24,25] [h bob 24,h bob 25]"
   30.74    apply (prolog prog_Test)
   30.75    done
   30.76  
   30.77 -lemma "mapfun ?F [24] [h 24 24]"
   30.78 +schematic_lemma "mapfun ?F [24] [h 24 24]"
   30.79    apply (prolog prog_Test)
   30.80    back
   30.81    back
   30.82 @@ -149,12 +149,12 @@
   30.83    apply (prolog prog_Test)
   30.84    done
   30.85  
   30.86 -lemma "age ?x 24 & age ?y 23"
   30.87 +schematic_lemma "age ?x 24 & age ?y 23"
   30.88    apply (prolog prog_Test)
   30.89    back
   30.90    done
   30.91  
   30.92 -lemma "age ?x 24 | age ?x 23"
   30.93 +schematic_lemma "age ?x 24 | age ?x 23"
   30.94    apply (prolog prog_Test)
   30.95    back
   30.96    back
   30.97 @@ -168,7 +168,7 @@
   30.98    apply (prolog prog_Test)
   30.99    done
  30.100  
  30.101 -lemma "age sue 24 .. age bob 23 => age ?x ?y"
  30.102 +schematic_lemma "age sue 24 .. age bob 23 => age ?x ?y"
  30.103    apply (prolog prog_Test)
  30.104    back
  30.105    back
  30.106 @@ -182,7 +182,7 @@
  30.107    done
  30.108  (*reset trace_DEPTH_FIRST;*)
  30.109  
  30.110 -lemma "(!x. age x 25 :- age x 23) => age ?x 25 & age ?y 25"
  30.111 +schematic_lemma "(!x. age x 25 :- age x 23) => age ?x 25 & age ?y 25"
  30.112    apply (prolog prog_Test)
  30.113    back
  30.114    back
  30.115 @@ -193,7 +193,7 @@
  30.116    apply (prolog prog_Test)
  30.117    done
  30.118  
  30.119 -lemma "? P. P & eq P ?x"
  30.120 +schematic_lemma "? P. P & eq P ?x"
  30.121    apply (prolog prog_Test)
  30.122  (*
  30.123    back
  30.124 @@ -248,14 +248,14 @@
  30.125    by fast
  30.126  *)
  30.127  
  30.128 -lemma "!Emp Stk.(
  30.129 +schematic_lemma "!Emp Stk.(
  30.130                         empty    (Emp::'b) .. 
  30.131           (!(X::nat) S. add    X (S::'b)         (Stk X S)) .. 
  30.132           (!(X::nat) S. remove X ((Stk X S)::'b) S))
  30.133   => bag_appl 23 24 ?X ?Y"
  30.134    oops
  30.135  
  30.136 -lemma "!Qu. ( 
  30.137 +schematic_lemma "!Qu. ( 
  30.138            (!L.            empty    (Qu L L)) .. 
  30.139            (!(X::nat) L K. add    X (Qu L (X#K)) (Qu L K)) ..
  30.140            (!(X::nat) L K. remove X (Qu (X#L) K) (Qu L K)))
  30.141 @@ -266,7 +266,7 @@
  30.142    apply (prolog prog_Test)
  30.143    done
  30.144  
  30.145 -lemma "P x .. P y => P ?X"
  30.146 +schematic_lemma "P x .. P y => P ?X"
  30.147    apply (prolog prog_Test)
  30.148    back
  30.149    done
    31.1 --- a/src/HOL/Prolog/Type.thy	Fri Apr 23 23:33:48 2010 +0200
    31.2 +++ b/src/HOL/Prolog/Type.thy	Fri Apr 23 23:35:43 2010 +0200
    31.3 @@ -47,41 +47,41 @@
    31.4  
    31.5  lemmas prog_Type = prog_Func good_typeof common_typeof
    31.6  
    31.7 -lemma "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T"
    31.8 +schematic_lemma "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T"
    31.9    apply (prolog prog_Type)
   31.10    done
   31.11  
   31.12 -lemma "typeof (fix (%x. x)) ?T"
   31.13 +schematic_lemma "typeof (fix (%x. x)) ?T"
   31.14    apply (prolog prog_Type)
   31.15    done
   31.16  
   31.17 -lemma "typeof (fix (%fact. abs(%n. (app fact (n - Z))))) ?T"
   31.18 +schematic_lemma "typeof (fix (%fact. abs(%n. (app fact (n - Z))))) ?T"
   31.19    apply (prolog prog_Type)
   31.20    done
   31.21  
   31.22 -lemma "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z)
   31.23 +schematic_lemma "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z)
   31.24    (n * (app fact (n - (S Z))))))) ?T"
   31.25    apply (prolog prog_Type)
   31.26    done
   31.27  
   31.28 -lemma "typeof (abs(%v. Z)) ?T" (*correct only solution (?A1 -> nat) *)
   31.29 +schematic_lemma "typeof (abs(%v. Z)) ?T" (*correct only solution (?A1 -> nat) *)
   31.30    apply (prolog prog_Type)
   31.31    done
   31.32  
   31.33 -lemma "typeof (abs(%v. Z)) ?T"
   31.34 +schematic_lemma "typeof (abs(%v. Z)) ?T"
   31.35    apply (prolog bad1_typeof common_typeof) (* 1st result ok*)
   31.36    done
   31.37  
   31.38 -lemma "typeof (abs(%v. Z)) ?T"
   31.39 +schematic_lemma "typeof (abs(%v. Z)) ?T"
   31.40    apply (prolog bad1_typeof common_typeof)
   31.41    back (* 2nd result (?A1 -> ?A1) wrong *)
   31.42    done
   31.43  
   31.44 -lemma "typeof (abs(%v. abs(%v. app v v))) ?T"
   31.45 +schematic_lemma "typeof (abs(%v. abs(%v. app v v))) ?T"
   31.46    apply (prolog prog_Type)?  (*correctly fails*)
   31.47    oops
   31.48  
   31.49 -lemma "typeof (abs(%v. abs(%v. app v v))) ?T"
   31.50 +schematic_lemma "typeof (abs(%v. abs(%v. app v v))) ?T"
   31.51    apply (prolog bad2_typeof common_typeof) (* wrong result ((?A3 -> ?B3) -> ?A3 -> ?B3)*)
   31.52    done
   31.53  
    32.1 --- a/src/HOL/ex/Classical.thy	Fri Apr 23 23:33:48 2010 +0200
    32.2 +++ b/src/HOL/ex/Classical.thy	Fri Apr 23 23:35:43 2010 +0200
    32.3 @@ -348,7 +348,7 @@
    32.4  
    32.5  text{*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
    32.6    fast DISCOVERS who killed Agatha. *}
    32.7 -lemma "lives(agatha) & lives(butler) & lives(charles) &
    32.8 +schematic_lemma "lives(agatha) & lives(butler) & lives(charles) &
    32.9     (killed agatha agatha | killed butler agatha | killed charles agatha) &
   32.10     (\<forall>x y. killed x y --> hates x y & ~richer x y) &
   32.11     (\<forall>x. hates agatha x --> ~hates charles x) &
    33.1 --- a/src/HOL/ex/Groebner_Examples.thy	Fri Apr 23 23:33:48 2010 +0200
    33.2 +++ b/src/HOL/ex/Groebner_Examples.thy	Fri Apr 23 23:35:43 2010 +0200
    33.3 @@ -10,13 +10,13 @@
    33.4  
    33.5  subsection {* Basic examples *}
    33.6  
    33.7 -lemma "3 ^ 3 == (?X::'a::{number_ring})"
    33.8 +schematic_lemma "3 ^ 3 == (?X::'a::{number_ring})"
    33.9    by sring_norm
   33.10  
   33.11 -lemma "(x - (-2))^5 == ?X::int"
   33.12 +schematic_lemma "(x - (-2))^5 == ?X::int"
   33.13    by sring_norm
   33.14  
   33.15 -lemma "(x - (-2))^5  * (y - 78) ^ 8 == ?X::int"
   33.16 +schematic_lemma "(x - (-2))^5  * (y - 78) ^ 8 == ?X::int"
   33.17    by sring_norm
   33.18  
   33.19  lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring})"
    34.1 --- a/src/HOL/ex/Refute_Examples.thy	Fri Apr 23 23:33:48 2010 +0200
    34.2 +++ b/src/HOL/ex/Refute_Examples.thy	Fri Apr 23 23:35:43 2010 +0200
    34.3 @@ -347,12 +347,12 @@
    34.4  
    34.5  subsubsection {* Schematic variables *}
    34.6  
    34.7 -lemma "?P"
    34.8 +schematic_lemma "?P"
    34.9    refute
   34.10    apply auto
   34.11  done
   34.12  
   34.13 -lemma "x = ?y"
   34.14 +schematic_lemma "x = ?y"
   34.15    refute
   34.16    apply auto
   34.17  done
    35.1 --- a/src/HOL/ex/set.thy	Fri Apr 23 23:33:48 2010 +0200
    35.2 +++ b/src/HOL/ex/set.thy	Fri Apr 23 23:35:43 2010 +0200
    35.3 @@ -26,7 +26,7 @@
    35.4    Trivial example of term synthesis: apparently hard for some provers!
    35.5  *}
    35.6  
    35.7 -lemma "a \<noteq> b \<Longrightarrow> a \<in> ?X \<and> b \<notin> ?X"
    35.8 +schematic_lemma "a \<noteq> b \<Longrightarrow> a \<in> ?X \<and> b \<notin> ?X"
    35.9    by blast
   35.10  
   35.11  
   35.12 @@ -60,15 +60,15 @@
   35.13    -- {* Requires best-first search because it is undirectional. *}
   35.14    by best
   35.15  
   35.16 -lemma "\<forall>f:: 'a \<Rightarrow> 'a set. \<forall>x. f x \<noteq> ?S f"
   35.17 +schematic_lemma "\<forall>f:: 'a \<Rightarrow> 'a set. \<forall>x. f x \<noteq> ?S f"
   35.18    -- {*This form displays the diagonal term. *}
   35.19    by best
   35.20  
   35.21 -lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
   35.22 +schematic_lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
   35.23    -- {* This form exploits the set constructs. *}
   35.24    by (rule notI, erule rangeE, best)
   35.25  
   35.26 -lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
   35.27 +schematic_lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
   35.28    -- {* Or just this! *}
   35.29    by best
   35.30  
    36.1 --- a/src/Sequents/LK/Quantifiers.thy	Fri Apr 23 23:33:48 2010 +0200
    36.2 +++ b/src/Sequents/LK/Quantifiers.thy	Fri Apr 23 23:35:43 2010 +0200
    36.3 @@ -90,13 +90,13 @@
    36.4    oops
    36.5  
    36.6  (*INVALID*)
    36.7 -lemma "|- P(?a) --> (ALL x. P(x))"
    36.8 +schematic_lemma "|- P(?a) --> (ALL x. P(x))"
    36.9    apply fast?
   36.10    apply (rule _)
   36.11    oops
   36.12  
   36.13  (*INVALID*)
   36.14 -lemma "|- (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
   36.15 +schematic_lemma "|- (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
   36.16    apply fast?
   36.17    apply (rule _)
   36.18    oops
   36.19 @@ -114,7 +114,7 @@
   36.20  
   36.21  text "Solving for a Var"
   36.22  
   36.23 -lemma "|- (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
   36.24 +schematic_lemma "|- (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
   36.25    by fast
   36.26  
   36.27  
    37.1 --- a/src/ZF/AC/Cardinal_aux.thy	Fri Apr 23 23:33:48 2010 +0200
    37.2 +++ b/src/ZF/AC/Cardinal_aux.thy	Fri Apr 23 23:35:43 2010 +0200
    37.3 @@ -71,7 +71,7 @@
    37.4  apply (rule Un_upper1 [THEN subset_imp_lepoll]) 
    37.5  done
    37.6  
    37.7 -lemma paired_bij: "?f \<in> bij({{y,z}. y \<in> x}, x)"
    37.8 +schematic_lemma paired_bij: "?f \<in> bij({{y,z}. y \<in> x}, x)"
    37.9  apply (rule RepFun_bijective)
   37.10  apply (simp add: doubleton_eq_iff, blast)
   37.11  done
    38.1 --- a/src/ZF/Constructible/Reflection.thy	Fri Apr 23 23:33:48 2010 +0200
    38.2 +++ b/src/ZF/Constructible/Reflection.thy	Fri Apr 23 23:35:43 2010 +0200
    38.3 @@ -268,7 +268,7 @@
    38.4  text{*Example 1: reflecting a simple formula.  The reflecting class is first
    38.5  given as the variable @{text ?Cl} and later retrieved from the final 
    38.6  proof state.*}
    38.7 -lemma (in reflection) 
    38.8 +schematic_lemma (in reflection) 
    38.9       "Reflects(?Cl,
   38.10                 \<lambda>x. \<exists>y. M(y) & x \<in> y, 
   38.11                 \<lambda>a x. \<exists>y\<in>Mset(a). x \<in> y)"
   38.12 @@ -285,7 +285,7 @@
   38.13  
   38.14  
   38.15  text{*Example 2*}
   38.16 -lemma (in reflection) 
   38.17 +schematic_lemma (in reflection) 
   38.18       "Reflects(?Cl,
   38.19                 \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y), 
   38.20                 \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x --> z \<in> y)" 
   38.21 @@ -302,14 +302,14 @@
   38.22  by fast
   38.23  
   38.24  text{*Example 2''.  We expand the subset relation.*}
   38.25 -lemma (in reflection) 
   38.26 +schematic_lemma (in reflection) 
   38.27    "Reflects(?Cl,
   38.28          \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) --> (\<forall>w. M(w) --> w\<in>z --> w\<in>x) --> z\<in>y),
   38.29          \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). (\<forall>w\<in>Mset(a). w\<in>z --> w\<in>x) --> z\<in>y)"
   38.30  by fast
   38.31  
   38.32  text{*Example 2'''.  Single-step version, to reveal the reflecting class.*}
   38.33 -lemma (in reflection) 
   38.34 +schematic_lemma (in reflection) 
   38.35       "Reflects(?Cl,
   38.36                 \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y), 
   38.37                 \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x --> z \<in> y)" 
   38.38 @@ -329,21 +329,21 @@
   38.39  
   38.40  text{*Example 3.  Warning: the following examples make sense only
   38.41  if @{term P} is quantifier-free, since it is not being relativized.*}
   38.42 -lemma (in reflection) 
   38.43 +schematic_lemma (in reflection) 
   38.44       "Reflects(?Cl,
   38.45                 \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) --> z \<in> y <-> z \<in> x & P(z)), 
   38.46                 \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<in> y <-> z \<in> x & P(z))"
   38.47  by fast
   38.48  
   38.49  text{*Example 3'*}
   38.50 -lemma (in reflection) 
   38.51 +schematic_lemma (in reflection) 
   38.52       "Reflects(?Cl,
   38.53                 \<lambda>x. \<exists>y. M(y) & y = Collect(x,P),
   38.54                 \<lambda>a x. \<exists>y\<in>Mset(a). y = Collect(x,P))";
   38.55  by fast
   38.56  
   38.57  text{*Example 3''*}
   38.58 -lemma (in reflection) 
   38.59 +schematic_lemma (in reflection) 
   38.60       "Reflects(?Cl,
   38.61                 \<lambda>x. \<exists>y. M(y) & y = Replace(x,P),
   38.62                 \<lambda>a x. \<exists>y\<in>Mset(a). y = Replace(x,P))";
   38.63 @@ -351,7 +351,7 @@
   38.64  
   38.65  text{*Example 4: Axiom of Choice.  Possibly wrong, since @{text \<Pi>} needs
   38.66  to be relativized.*}
   38.67 -lemma (in reflection) 
   38.68 +schematic_lemma (in reflection) 
   38.69       "Reflects(?Cl,
   38.70                 \<lambda>A. 0\<notin>A --> (\<exists>f. M(f) & f \<in> (\<Pi> X \<in> A. X)),
   38.71                 \<lambda>a A. 0\<notin>A --> (\<exists>f\<in>Mset(a). f \<in> (\<Pi> X \<in> A. X)))"