--- a/src/CCL/Fix.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/CCL/Fix.thy Fri Apr 23 23:35:43 2010 +0200
@@ -98,7 +98,7 @@
(* All fixed points are lam-expressions *)
-lemma idgenfp_lam: "idgen(d) = d ==> d = lam x. ?f(x)"
+schematic_lemma idgenfp_lam: "idgen(d) = d ==> d = lam x. ?f(x)"
apply (unfold idgen_def)
apply (erule ssubst)
apply (rule refl)
@@ -130,7 +130,7 @@
apply simp
done
-lemma po_eta_lemma: "idgen(d) = d ==> d = lam x. ?f(x)"
+schematic_lemma po_eta_lemma: "idgen(d) = d ==> d = lam x. ?f(x)"
apply (unfold idgen_def)
apply (erule sym)
done
--- a/src/CCL/Wfd.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/CCL/Wfd.thy Fri Apr 23 23:35:43 2010 +0200
@@ -573,29 +573,29 @@
subsection {* Factorial *}
-lemma
+schematic_lemma
"letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h))))
in f(succ(succ(zero))) ---> ?a"
by eval
-lemma
+schematic_lemma
"letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h))))
in f(succ(succ(succ(zero)))) ---> ?a"
by eval
subsection {* Less Than Or Equal *}
-lemma
+schematic_lemma
"letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>))))
in f(<succ(zero), succ(zero)>) ---> ?a"
by eval
-lemma
+schematic_lemma
"letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>))))
in f(<succ(zero), succ(succ(succ(succ(zero))))>) ---> ?a"
by eval
-lemma
+schematic_lemma
"letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>))))
in f(<succ(succ(succ(succ(succ(zero))))), succ(succ(succ(succ(zero))))>) ---> ?a"
by eval
@@ -603,12 +603,12 @@
subsection {* Reverse *}
-lemma
+schematic_lemma
"letrec id l be lcase(l,[],%x xs. x$id(xs))
in id(zero$succ(zero)$[]) ---> ?a"
by eval
-lemma
+schematic_lemma
"letrec rev l be lcase(l,[],%x xs. lrec(rev(xs),x$[],%y ys g. y$g))
in rev(zero$succ(zero)$(succ((lam x. x)`succ(zero)))$([])) ---> ?a"
by eval
--- a/src/CTT/Arith.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/CTT/Arith.thy Fri Apr 23 23:35:43 2010 +0200
@@ -256,7 +256,8 @@
(*Addition is the inverse of subtraction: if b<=x then b#+(x-b) = x.
An example of induction over a quantified formula (a product).
Uses rewriting with a quantified, implicative inductive hypothesis.*)
-lemma add_diff_inverse_lemma: "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)"
+schematic_lemma add_diff_inverse_lemma:
+ "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)"
apply (tactic {* NE_tac @{context} "b" 1 *})
(*strip one "universal quantifier" but not the "implication"*)
apply (rule_tac [3] intr_rls)
@@ -324,7 +325,7 @@
done
(*If a+b=0 then a=0. Surprisingly tedious*)
-lemma add_eq0_lemma: "[| a:N; b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)"
+schematic_lemma add_eq0_lemma: "[| a:N; b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)"
apply (tactic {* NE_tac @{context} "a" 1 *})
apply (rule_tac [3] replace_type)
apply (tactic "arith_rew_tac []")
@@ -344,7 +345,7 @@
done
(*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *)
-lemma absdiff_eq0_lem:
+schematic_lemma absdiff_eq0_lem:
"[| a:N; b:N; a |-| b = 0 : N |] ==>
?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)"
apply (unfold absdiff_def)
--- a/src/CTT/ex/Elimination.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/CTT/ex/Elimination.thy Fri Apr 23 23:35:43 2010 +0200
@@ -14,41 +14,41 @@
text "This finds the functions fst and snd!"
-lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
+schematic_lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
apply (tactic {* pc_tac [] 1 *})
done
-lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
+schematic_lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
apply (tactic {* pc_tac [] 1 *})
back
done
text "Double negation of the Excluded Middle"
-lemma "A type ==> ?a : ((A + (A-->F)) --> F) --> F"
+schematic_lemma "A type ==> ?a : ((A + (A-->F)) --> F) --> F"
apply (tactic "intr_tac []")
apply (rule ProdE)
apply assumption
apply (tactic "pc_tac [] 1")
done
-lemma "[| A type; B type |] ==> ?a : (A*B) --> (B*A)"
+schematic_lemma "[| A type; B type |] ==> ?a : (A*B) --> (B*A)"
apply (tactic "pc_tac [] 1")
done
(*The sequent version (ITT) could produce an interesting alternative
by backtracking. No longer.*)
text "Binary sums and products"
-lemma "[| A type; B type; C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)"
+schematic_lemma "[| A type; B type; C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)"
apply (tactic "pc_tac [] 1")
done
(*A distributive law*)
-lemma "[| A type; B type; C type |] ==> ?a : A * (B+C) --> (A*B + A*C)"
+schematic_lemma "[| A type; B type; C type |] ==> ?a : A * (B+C) --> (A*B + A*C)"
apply (tactic "pc_tac [] 1")
done
(*more general version, same proof*)
-lemma
+schematic_lemma
assumes "A type"
and "!!x. x:A ==> B(x) type"
and "!!x. x:A ==> C(x) type"
@@ -57,12 +57,12 @@
done
text "Construction of the currying functional"
-lemma "[| A type; B type; C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))"
+schematic_lemma "[| A type; B type; C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))"
apply (tactic "pc_tac [] 1")
done
(*more general goal with same proof*)
-lemma
+schematic_lemma
assumes "A type"
and "!!x. x:A ==> B(x) type"
and "!!z. z: (SUM x:A. B(x)) ==> C(z) type"
@@ -72,12 +72,12 @@
done
text "Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)"
-lemma "[| A type; B type; C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)"
+schematic_lemma "[| A type; B type; C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)"
apply (tactic "pc_tac [] 1")
done
(*more general goal with same proof*)
-lemma
+schematic_lemma
assumes "A type"
and "!!x. x:A ==> B(x) type"
and "!!z. z: (SUM x:A . B(x)) ==> C(z) type"
@@ -87,12 +87,12 @@
done
text "Function application"
-lemma "[| A type; B type |] ==> ?a : ((A --> B) * A) --> B"
+schematic_lemma "[| A type; B type |] ==> ?a : ((A --> B) * A) --> B"
apply (tactic "pc_tac [] 1")
done
text "Basic test of quantifier reasoning"
-lemma
+schematic_lemma
assumes "A type"
and "B type"
and "!!x y.[| x:A; y:B |] ==> C(x,y) type"
@@ -103,7 +103,7 @@
done
text "Martin-Lof (1984) pages 36-7: the combinator S"
-lemma
+schematic_lemma
assumes "A type"
and "!!x. x:A ==> B(x) type"
and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type"
@@ -113,7 +113,7 @@
done
text "Martin-Lof (1984) page 58: the axiom of disjunction elimination"
-lemma
+schematic_lemma
assumes "A type"
and "B type"
and "!!z. z: A+B ==> C(z) type"
@@ -123,7 +123,7 @@
done
(*towards AXIOM OF CHOICE*)
-lemma [folded basic_defs]:
+schematic_lemma [folded basic_defs]:
"[| A type; B type; C type |] ==> ?a : (A --> B*C) --> (A-->B) * (A-->C)"
apply (tactic "pc_tac [] 1")
done
@@ -131,7 +131,7 @@
(*Martin-Lof (1984) page 50*)
text "AXIOM OF CHOICE! Delicate use of elimination rules"
-lemma
+schematic_lemma
assumes "A type"
and "!!x. x:A ==> B(x) type"
and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type"
@@ -149,7 +149,7 @@
done
text "Axiom of choice. Proof without fst, snd. Harder still!"
-lemma [folded basic_defs]:
+schematic_lemma [folded basic_defs]:
assumes "A type"
and "!!x. x:A ==> B(x) type"
and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type"
@@ -174,7 +174,7 @@
text "Example of sequent_style deduction"
(*When splitting z:A*B, the assumption C(z) is affected; ?a becomes
lam u. split(u,%v w.split(v,%x y.lam z. <x,<y,z>>) ` w) *)
-lemma
+schematic_lemma
assumes "A type"
and "B type"
and "!!z. z:A*B ==> C(z) type"
--- a/src/CTT/ex/Synthesis.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/CTT/ex/Synthesis.thy Fri Apr 23 23:35:43 2010 +0200
@@ -10,7 +10,7 @@
begin
text "discovery of predecessor function"
-lemma "?a : SUM pred:?A . Eq(N, pred`0, 0)
+schematic_lemma "?a : SUM pred:?A . Eq(N, pred`0, 0)
* (PROD n:N. Eq(N, pred ` succ(n), n))"
apply (tactic "intr_tac []")
apply (tactic eqintr_tac)
@@ -20,7 +20,7 @@
done
text "the function fst as an element of a function type"
-lemma [folded basic_defs]:
+schematic_lemma [folded basic_defs]:
"A type ==> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` <i,j>, i)"
apply (tactic "intr_tac []")
apply (tactic eqintr_tac)
@@ -34,7 +34,7 @@
text "An interesting use of the eliminator, when"
(*The early implementation of unification caused non-rigid path in occur check
See following example.*)
-lemma "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0 , i>)
+schematic_lemma "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0 , i>)
* Eq(?A, ?b(inr(i)), <succ(0), i>)"
apply (tactic "intr_tac []")
apply (tactic eqintr_tac)
@@ -46,13 +46,13 @@
This prevents the cycle in the first unification (no longer needed).
Requires flex-flex to preserve the dependence.
Simpler still: make ?A into a constant type N*N.*)
-lemma "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0 , i>)
+schematic_lemma "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0 , i>)
* Eq(?A(i), ?b(inr(i)), <succ(0),i>)"
oops
text "A tricky combination of when and split"
(*Now handled easily, but caused great problems once*)
-lemma [folded basic_defs]:
+schematic_lemma [folded basic_defs]:
"?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i)
* Eq(?A, ?b(inr(<i,j>)), j)"
apply (tactic "intr_tac []")
@@ -65,18 +65,18 @@
done
(*similar but allows the type to depend on i and j*)
-lemma "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i)
+schematic_lemma "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i)
* Eq(?A(i,j), ?b(inr(<i,j>)), j)"
oops
(*similar but specifying the type N simplifies the unification problems*)
-lemma "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)
+schematic_lemma "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)
* Eq(N, ?b(inr(<i,j>)), j)"
oops
text "Deriving the addition operator"
-lemma [folded arith_defs]:
+schematic_lemma [folded arith_defs]:
"?c : PROD n:N. Eq(N, ?f(0,n), n)
* (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))"
apply (tactic "intr_tac []")
@@ -86,7 +86,7 @@
done
text "The addition function -- using explicit lambdas"
-lemma [folded arith_defs]:
+schematic_lemma [folded arith_defs]:
"?c : SUM plus : ?A .
PROD x:N. Eq(N, plus`0`x, x)
* (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))"
--- a/src/CTT/ex/Typechecking.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/CTT/ex/Typechecking.thy Fri Apr 23 23:35:43 2010 +0200
@@ -11,18 +11,18 @@
subsection {* Single-step proofs: verifying that a type is well-formed *}
-lemma "?A type"
+schematic_lemma "?A type"
apply (rule form_rls)
done
-lemma "?A type"
+schematic_lemma "?A type"
apply (rule form_rls)
back
apply (rule form_rls)
apply (rule form_rls)
done
-lemma "PROD z:?A . N + ?B(z) type"
+schematic_lemma "PROD z:?A . N + ?B(z) type"
apply (rule form_rls)
apply (rule form_rls)
apply (rule form_rls)
@@ -37,30 +37,30 @@
apply (tactic form_tac)
done
-lemma "<0, succ(0)> : ?A"
+schematic_lemma "<0, succ(0)> : ?A"
apply (tactic "intr_tac []")
done
-lemma "PROD w:N . Eq(?A,w,w) type"
+schematic_lemma "PROD w:N . Eq(?A,w,w) type"
apply (tactic "typechk_tac []")
done
-lemma "PROD x:N . PROD y:N . Eq(?A,x,y) type"
+schematic_lemma "PROD x:N . PROD y:N . Eq(?A,x,y) type"
apply (tactic "typechk_tac []")
done
text "typechecking an application of fst"
-lemma "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A"
+schematic_lemma "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A"
apply (tactic "typechk_tac []")
done
text "typechecking the predecessor function"
-lemma "lam n. rec(n, 0, %x y. x) : ?A"
+schematic_lemma "lam n. rec(n, 0, %x y. x) : ?A"
apply (tactic "typechk_tac []")
done
text "typechecking the addition function"
-lemma "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A"
+schematic_lemma "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A"
apply (tactic "typechk_tac []")
done
@@ -68,18 +68,18 @@
For concreteness, every type variable left over is forced to be N*)
ML {* val N_tac = TRYALL (rtac (thm "NF")) *}
-lemma "lam w. <w,w> : ?A"
+schematic_lemma "lam w. <w,w> : ?A"
apply (tactic "typechk_tac []")
apply (tactic N_tac)
done
-lemma "lam x. lam y. x : ?A"
+schematic_lemma "lam x. lam y. x : ?A"
apply (tactic "typechk_tac []")
apply (tactic N_tac)
done
text "typechecking fst (as a function object)"
-lemma "lam i. split(i, %j k. j) : ?A"
+schematic_lemma "lam i. split(i, %j k. j) : ?A"
apply (tactic "typechk_tac []")
apply (tactic N_tac)
done
--- a/src/Cube/Example.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/Cube/Example.thy Fri Apr 23 23:35:43 2010 +0200
@@ -30,98 +30,98 @@
subsection {* Simple types *}
-lemma "A:* |- A->A : ?T"
+schematic_lemma "A:* |- A->A : ?T"
by (depth_solve rules)
-lemma "A:* |- Lam a:A. a : ?T"
+schematic_lemma "A:* |- Lam a:A. a : ?T"
by (depth_solve rules)
-lemma "A:* B:* b:B |- Lam x:A. b : ?T"
+schematic_lemma "A:* B:* b:B |- Lam x:A. b : ?T"
by (depth_solve rules)
-lemma "A:* b:A |- (Lam a:A. a)^b: ?T"
+schematic_lemma "A:* b:A |- (Lam a:A. a)^b: ?T"
by (depth_solve rules)
-lemma "A:* B:* c:A b:B |- (Lam x:A. b)^ c: ?T"
+schematic_lemma "A:* B:* c:A b:B |- (Lam x:A. b)^ c: ?T"
by (depth_solve rules)
-lemma "A:* B:* |- Lam a:A. Lam b:B. a : ?T"
+schematic_lemma "A:* B:* |- Lam a:A. Lam b:B. a : ?T"
by (depth_solve rules)
subsection {* Second-order types *}
-lemma (in L2) "|- Lam A:*. Lam a:A. a : ?T"
+schematic_lemma (in L2) "|- Lam A:*. Lam a:A. a : ?T"
by (depth_solve rules)
-lemma (in L2) "A:* |- (Lam B:*.Lam b:B. b)^A : ?T"
+schematic_lemma (in L2) "A:* |- (Lam B:*.Lam b:B. b)^A : ?T"
by (depth_solve rules)
-lemma (in L2) "A:* b:A |- (Lam B:*.Lam b:B. b) ^ A ^ b: ?T"
+schematic_lemma (in L2) "A:* b:A |- (Lam B:*.Lam b:B. b) ^ A ^ b: ?T"
by (depth_solve rules)
-lemma (in L2) "|- Lam B:*.Lam a:(Pi A:*.A).a ^ ((Pi A:*.A)->B) ^ a: ?T"
+schematic_lemma (in L2) "|- Lam B:*.Lam a:(Pi A:*.A).a ^ ((Pi A:*.A)->B) ^ a: ?T"
by (depth_solve rules)
subsection {* Weakly higher-order propositional logic *}
-lemma (in Lomega) "|- Lam A:*.A->A : ?T"
+schematic_lemma (in Lomega) "|- Lam A:*.A->A : ?T"
by (depth_solve rules)
-lemma (in Lomega) "B:* |- (Lam A:*.A->A) ^ B : ?T"
+schematic_lemma (in Lomega) "B:* |- (Lam A:*.A->A) ^ B : ?T"
by (depth_solve rules)
-lemma (in Lomega) "B:* b:B |- (Lam y:B. b): ?T"
+schematic_lemma (in Lomega) "B:* b:B |- (Lam y:B. b): ?T"
by (depth_solve rules)
-lemma (in Lomega) "A:* F:*->* |- F^(F^A): ?T"
+schematic_lemma (in Lomega) "A:* F:*->* |- F^(F^A): ?T"
by (depth_solve rules)
-lemma (in Lomega) "A:* |- Lam F:*->*.F^(F^A): ?T"
+schematic_lemma (in Lomega) "A:* |- Lam F:*->*.F^(F^A): ?T"
by (depth_solve rules)
subsection {* LP *}
-lemma (in LP) "A:* |- A -> * : ?T"
+schematic_lemma (in LP) "A:* |- A -> * : ?T"
by (depth_solve rules)
-lemma (in LP) "A:* P:A->* a:A |- P^a: ?T"
+schematic_lemma (in LP) "A:* P:A->* a:A |- P^a: ?T"
by (depth_solve rules)
-lemma (in LP) "A:* P:A->A->* a:A |- Pi a:A. P^a^a: ?T"
+schematic_lemma (in LP) "A:* P:A->A->* a:A |- Pi a:A. P^a^a: ?T"
by (depth_solve rules)
-lemma (in LP) "A:* P:A->* Q:A->* |- Pi a:A. P^a -> Q^a: ?T"
+schematic_lemma (in LP) "A:* P:A->* Q:A->* |- Pi a:A. P^a -> Q^a: ?T"
by (depth_solve rules)
-lemma (in LP) "A:* P:A->* |- Pi a:A. P^a -> P^a: ?T"
+schematic_lemma (in LP) "A:* P:A->* |- Pi a:A. P^a -> P^a: ?T"
by (depth_solve rules)
-lemma (in LP) "A:* P:A->* |- Lam a:A. Lam x:P^a. x: ?T"
+schematic_lemma (in LP) "A:* P:A->* |- Lam a:A. Lam x:P^a. x: ?T"
by (depth_solve rules)
-lemma (in LP) "A:* P:A->* Q:* |- (Pi a:A. P^a->Q) -> (Pi a:A. P^a) -> Q : ?T"
+schematic_lemma (in LP) "A:* P:A->* Q:* |- (Pi a:A. P^a->Q) -> (Pi a:A. P^a) -> Q : ?T"
by (depth_solve rules)
-lemma (in LP) "A:* P:A->* Q:* a0:A |-
+schematic_lemma (in LP) "A:* P:A->* Q:* a0:A |-
Lam x:Pi a:A. P^a->Q. Lam y:Pi a:A. P^a. x^a0^(y^a0): ?T"
by (depth_solve rules)
subsection {* Omega-order types *}
-lemma (in L2) "A:* B:* |- Pi C:*.(A->B->C)->C : ?T"
+schematic_lemma (in L2) "A:* B:* |- Pi C:*.(A->B->C)->C : ?T"
by (depth_solve rules)
-lemma (in Lomega2) "|- Lam A:*.Lam B:*.Pi C:*.(A->B->C)->C : ?T"
+schematic_lemma (in Lomega2) "|- Lam A:*.Lam B:*.Pi C:*.(A->B->C)->C : ?T"
by (depth_solve rules)
-lemma (in Lomega2) "|- Lam A:*.Lam B:*.Lam x:A. Lam y:B. x : ?T"
+schematic_lemma (in Lomega2) "|- Lam A:*.Lam B:*.Lam x:A. Lam y:B. x : ?T"
by (depth_solve rules)
-lemma (in Lomega2) "A:* B:* |- ?p : (A->B) -> ((B->Pi P:*.P)->(A->Pi P:*.P))"
+schematic_lemma (in Lomega2) "A:* B:* |- ?p : (A->B) -> ((B->Pi P:*.P)->(A->Pi P:*.P))"
apply (strip_asms rules)
apply (rule lam_ss)
apply (depth_solve1 rules)
@@ -145,14 +145,14 @@
subsection {* Second-order Predicate Logic *}
-lemma (in LP2) "A:* P:A->* |- Lam a:A. P^a->(Pi A:*.A) : ?T"
+schematic_lemma (in LP2) "A:* P:A->* |- Lam a:A. P^a->(Pi A:*.A) : ?T"
by (depth_solve rules)
-lemma (in LP2) "A:* P:A->A->* |-
+schematic_lemma (in LP2) "A:* P:A->A->* |-
(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"
by (depth_solve rules)
-lemma (in LP2) "A:* P:A->A->* |-
+schematic_lemma (in LP2) "A:* P:A->A->* |-
?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"
-- {* Antisymmetry implies irreflexivity: *}
apply (strip_asms rules)
@@ -174,22 +174,22 @@
subsection {* LPomega *}
-lemma (in LPomega) "A:* |- Lam P:A->A->*.Lam a:A. P^a^a : ?T"
+schematic_lemma (in LPomega) "A:* |- Lam P:A->A->*.Lam a:A. P^a^a : ?T"
by (depth_solve rules)
-lemma (in LPomega) "|- Lam A:*.Lam P:A->A->*.Lam a:A. P^a^a : ?T"
+schematic_lemma (in LPomega) "|- Lam A:*.Lam P:A->A->*.Lam a:A. P^a^a : ?T"
by (depth_solve rules)
subsection {* Constructions *}
-lemma (in CC) "|- Lam A:*.Lam P:A->*.Lam a:A. P^a->Pi P:*.P: ?T"
+schematic_lemma (in CC) "|- Lam A:*.Lam P:A->*.Lam a:A. P^a->Pi P:*.P: ?T"
by (depth_solve rules)
-lemma (in CC) "|- Lam A:*.Lam P:A->*.Pi a:A. P^a: ?T"
+schematic_lemma (in CC) "|- Lam A:*.Lam P:A->*.Pi a:A. P^a: ?T"
by (depth_solve rules)
-lemma (in CC) "A:* P:A->* a:A |- ?p : (Pi a:A. P^a)->P^a"
+schematic_lemma (in CC) "A:* P:A->* a:A |- ?p : (Pi a:A. P^a)->P^a"
apply (strip_asms rules)
apply (rule lam_ss)
apply (depth_solve1 rules)
@@ -201,15 +201,15 @@
subsection {* Some random examples *}
-lemma (in LP2) "A:* c:A f:A->A |-
+schematic_lemma (in LP2) "A:* c:A f:A->A |-
Lam a:A. Pi P:A->*.P^c -> (Pi x:A. P^x->P^(f^x)) -> P^a : ?T"
by (depth_solve rules)
-lemma (in CC) "Lam A:*.Lam c:A. Lam f:A->A.
+schematic_lemma (in CC) "Lam A:*.Lam c:A. Lam f:A->A.
Lam a:A. Pi P:A->*.P^c -> (Pi x:A. P^x->P^(f^x)) -> P^a : ?T"
by (depth_solve rules)
-lemma (in LP2)
+schematic_lemma (in LP2)
"A:* a:A b:A |- ?p: (Pi P:A->*.P^a->P^b) -> (Pi P:A->*.P^b->P^a)"
-- {* Symmetry of Leibnitz equality *}
apply (strip_asms rules)
--- a/src/FOL/ex/Classical.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/FOL/ex/Classical.thy Fri Apr 23 23:35:43 2010 +0200
@@ -363,7 +363,7 @@
text{*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
fast DISCOVERS who killed Agatha. *}
-lemma "lives(agatha) & lives(butler) & lives(charles) &
+schematic_lemma "lives(agatha) & lives(butler) & lives(charles) &
(killed(agatha,agatha) | killed(butler,agatha) | killed(charles,agatha)) &
(\<forall>x y. killed(x,y) --> hates(x,y) & ~richer(x,y)) &
(\<forall>x. hates(agatha,x) --> ~hates(charles,x)) &
--- a/src/FOL/ex/Prolog.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/FOL/ex/Prolog.thy Fri Apr 23 23:35:43 2010 +0200
@@ -22,18 +22,18 @@
revNil: "rev(Nil,Nil)"
revCons: "[| rev(xs,ys); app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)"
-lemma "app(a:b:c:Nil, d:e:Nil, ?x)"
+schematic_lemma "app(a:b:c:Nil, d:e:Nil, ?x)"
apply (rule appNil appCons)
apply (rule appNil appCons)
apply (rule appNil appCons)
apply (rule appNil appCons)
done
-lemma "app(?x, c:d:Nil, a:b:c:d:Nil)"
+schematic_lemma "app(?x, c:d:Nil, a:b:c:d:Nil)"
apply (rule appNil appCons)+
done
-lemma "app(?x, ?y, a:b:c:d:Nil)"
+schematic_lemma "app(?x, ?y, a:b:c:d:Nil)"
apply (rule appNil appCons)+
back
back
@@ -46,15 +46,15 @@
lemmas rules = appNil appCons revNil revCons
-lemma "rev(a:b:c:d:Nil, ?x)"
+schematic_lemma "rev(a:b:c:d:Nil, ?x)"
apply (rule rules)+
done
-lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)"
+schematic_lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)"
apply (rule rules)+
done
-lemma "rev(?x, a:b:c:Nil)"
+schematic_lemma "rev(?x, a:b:c:Nil)"
apply (rule rules)+ -- {* does not solve it directly! *}
back
back
@@ -65,22 +65,22 @@
val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) (resolve_tac (@{thms rules}) 1)
*}
-lemma "rev(?x, a:b:c:Nil)"
+schematic_lemma "rev(?x, a:b:c:Nil)"
apply (tactic prolog_tac)
done
-lemma "rev(a:?x:c:?y:Nil, d:?z:b:?u)"
+schematic_lemma "rev(a:?x:c:?y:Nil, d:?z:b:?u)"
apply (tactic prolog_tac)
done
(*rev([a..p], ?w) requires 153 inferences *)
-lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)"
+schematic_lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)"
apply (tactic {* DEPTH_SOLVE (resolve_tac ([@{thm refl}, @{thm conjI}] @ @{thms rules}) 1) *})
done
(*?x has 16, ?y has 32; rev(?y,?w) requires 561 (rather large) inferences
total inferences = 2 + 1 + 17 + 561 = 581*)
-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)"
+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)"
apply (tactic {* DEPTH_SOLVE (resolve_tac ([@{thm refl}, @{thm conjI}] @ @{thms rules}) 1) *})
done
--- a/src/FOL/ex/Quantifiers_Cla.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/FOL/ex/Quantifiers_Cla.thy Fri Apr 23 23:35:43 2010 +0200
@@ -58,11 +58,11 @@
apply fast?
oops
-lemma "P(?a) --> (ALL x. P(x))"
+schematic_lemma "P(?a) --> (ALL x. P(x))"
apply fast?
oops
-lemma "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
+schematic_lemma "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
apply fast?
oops
@@ -76,7 +76,7 @@
lemma "(P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
by fast
-lemma "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
+schematic_lemma "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
by fast
lemma "(ALL x. Q(x)) --> (EX x. Q(x))"
--- a/src/FOL/ex/Quantifiers_Int.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/FOL/ex/Quantifiers_Int.thy Fri Apr 23 23:35:43 2010 +0200
@@ -58,11 +58,11 @@
apply (tactic "IntPr.fast_tac 1")?
oops
-lemma "P(?a) --> (ALL x. P(x))"
+schematic_lemma "P(?a) --> (ALL x. P(x))"
apply (tactic "IntPr.fast_tac 1")?
oops
-lemma "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
+schematic_lemma "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
apply (tactic "IntPr.fast_tac 1")?
oops
@@ -76,7 +76,7 @@
lemma "(P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
by (tactic "IntPr.fast_tac 1")
-lemma "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
+schematic_lemma "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
by (tactic "IntPr.fast_tac 1")
lemma "(ALL x. Q(x)) --> (EX x. Q(x))"
--- a/src/FOLP/FOLP.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/FOLP/FOLP.thy Fri Apr 23 23:35:43 2010 +0200
@@ -19,7 +19,7 @@
(*** Classical introduction rules for | and EX ***)
-lemma disjCI:
+schematic_lemma disjCI:
assumes "!!x. x:~Q ==> f(x):P"
shows "?p : P|Q"
apply (rule classical)
@@ -28,7 +28,7 @@
done
(*introduction rule involving only EX*)
-lemma ex_classical:
+schematic_lemma ex_classical:
assumes "!!u. u:~(EX x. P(x)) ==> f(u):P(a)"
shows "?p : EX x. P(x)"
apply (rule classical)
@@ -36,7 +36,7 @@
done
(*version of above, simplifying ~EX to ALL~ *)
-lemma exCI:
+schematic_lemma exCI:
assumes "!!u. u:ALL x. ~P(x) ==> f(u):P(a)"
shows "?p : EX x. P(x)"
apply (rule ex_classical)
@@ -45,7 +45,7 @@
apply (erule exI)
done
-lemma excluded_middle: "?p : ~P | P"
+schematic_lemma excluded_middle: "?p : ~P | P"
apply (rule disjCI)
apply assumption
done
@@ -54,7 +54,7 @@
(*** Special elimination rules *)
(*Classical implies (-->) elimination. *)
-lemma impCE:
+schematic_lemma impCE:
assumes major: "p:P-->Q"
and r1: "!!x. x:~P ==> f(x):R"
and r2: "!!y. y:Q ==> g(y):R"
@@ -65,7 +65,7 @@
done
(*Double negation law*)
-lemma notnotD: "p:~~P ==> ?p : P"
+schematic_lemma notnotD: "p:~~P ==> ?p : P"
apply (rule classical)
apply (erule notE)
apply assumption
@@ -76,7 +76,7 @@
(*Classical <-> elimination. Proof substitutes P=Q in
~P ==> ~Q and P ==> Q *)
-lemma iffCE:
+schematic_lemma iffCE:
assumes major: "p:P<->Q"
and r1: "!!x y.[| x:P; y:Q |] ==> f(x,y):R"
and r2: "!!x y.[| x:~P; y:~Q |] ==> g(x,y):R"
@@ -91,7 +91,7 @@
(*Should be used as swap since ~P becomes redundant*)
-lemma swap:
+schematic_lemma swap:
assumes major: "p:~P"
and r: "!!x. x:~Q ==> f(x):P"
shows "?p : Q"
@@ -136,7 +136,7 @@
addSEs [@{thm exE}, @{thm ex1E}] addEs [@{thm all_dupE}];
*}
-lemma cla_rews:
+schematic_lemma cla_rews:
"?p1 : P | ~P"
"?p2 : ~P | P"
"?p3 : ~ ~ P <-> P"
--- a/src/FOLP/IFOLP.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/FOLP/IFOLP.thy Fri Apr 23 23:35:43 2010 +0200
@@ -159,7 +159,7 @@
(*** Sequent-style elimination rules for & --> and ALL ***)
-lemma conjE:
+schematic_lemma conjE:
assumes "p:P&Q"
and "!!x y.[| x:P; y:Q |] ==> f(x,y):R"
shows "?a:R"
@@ -168,7 +168,7 @@
apply (rule conjunct2 [OF assms(1)])
done
-lemma impE:
+schematic_lemma impE:
assumes "p:P-->Q"
and "q:P"
and "!!x. x:Q ==> r(x):R"
@@ -176,7 +176,7 @@
apply (rule assms mp)+
done
-lemma allE:
+schematic_lemma allE:
assumes "p:ALL x. P(x)"
and "!!y. y:P(x) ==> q(y):R"
shows "?p:R"
@@ -184,7 +184,7 @@
done
(*Duplicates the quantifier; for use with eresolve_tac*)
-lemma all_dupE:
+schematic_lemma all_dupE:
assumes "p:ALL x. P(x)"
and "!!y z.[| y:P(x); z:ALL x. P(x) |] ==> q(y,z):R"
shows "?p:R"
@@ -194,21 +194,21 @@
(*** Negation rules, which translate between ~P and P-->False ***)
-lemma notI:
+schematic_lemma notI:
assumes "!!x. x:P ==> q(x):False"
shows "?p:~P"
unfolding not_def
apply (assumption | rule assms impI)+
done
-lemma notE: "p:~P \<Longrightarrow> q:P \<Longrightarrow> ?p:R"
+schematic_lemma notE: "p:~P \<Longrightarrow> q:P \<Longrightarrow> ?p:R"
unfolding not_def
apply (drule (1) mp)
apply (erule FalseE)
done
(*This is useful with the special implication rules for each kind of P. *)
-lemma not_to_imp:
+schematic_lemma not_to_imp:
assumes "p:~P"
and "!!x. x:(P-->False) ==> q(x):Q"
shows "?p:Q"
@@ -217,13 +217,13 @@
(* For substitution int an assumption P, reduce Q to P-->Q, substitute into
this implication, then apply impI to move P back into the assumptions.*)
-lemma rev_mp: "[| p:P; q:P --> Q |] ==> ?p:Q"
+schematic_lemma rev_mp: "[| p:P; q:P --> Q |] ==> ?p:Q"
apply (assumption | rule mp)+
done
(*Contrapositive of an inference rule*)
-lemma contrapos:
+schematic_lemma contrapos:
assumes major: "p:~Q"
and minor: "!!y. y:P==>q(y):Q"
shows "?a:~P"
@@ -271,7 +271,7 @@
(*** If-and-only-if ***)
-lemma iffI:
+schematic_lemma iffI:
assumes "!!x. x:P ==> q(x):Q"
and "!!x. x:Q ==> r(x):P"
shows "?p:P<->Q"
@@ -282,7 +282,7 @@
(*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
-lemma iffE:
+schematic_lemma iffE:
assumes "p:P <-> Q"
and "!!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R"
shows "?p:R"
@@ -294,28 +294,28 @@
(* Destruct rules for <-> similar to Modus Ponens *)
-lemma iffD1: "[| p:P <-> Q; q:P |] ==> ?p:Q"
+schematic_lemma iffD1: "[| p:P <-> Q; q:P |] ==> ?p:Q"
unfolding iff_def
apply (rule conjunct1 [THEN mp], assumption+)
done
-lemma iffD2: "[| p:P <-> Q; q:Q |] ==> ?p:P"
+schematic_lemma iffD2: "[| p:P <-> Q; q:Q |] ==> ?p:P"
unfolding iff_def
apply (rule conjunct2 [THEN mp], assumption+)
done
-lemma iff_refl: "?p:P <-> P"
+schematic_lemma iff_refl: "?p:P <-> P"
apply (rule iffI)
apply assumption+
done
-lemma iff_sym: "p:Q <-> P ==> ?p:P <-> Q"
+schematic_lemma iff_sym: "p:Q <-> P ==> ?p:P <-> Q"
apply (erule iffE)
apply (rule iffI)
apply (erule (1) mp)+
done
-lemma iff_trans: "[| p:P <-> Q; q:Q<-> R |] ==> ?p:P <-> R"
+schematic_lemma iff_trans: "[| p:P <-> Q; q:Q<-> R |] ==> ?p:P <-> R"
apply (rule iffI)
apply (assumption | erule iffE | erule (1) impE)+
done
@@ -326,7 +326,7 @@
do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential.
***)
-lemma ex1I:
+schematic_lemma ex1I:
assumes "p:P(a)"
and "!!x u. u:P(x) ==> f(u) : x=a"
shows "?p:EX! x. P(x)"
@@ -334,7 +334,7 @@
apply (assumption | rule assms exI conjI allI impI)+
done
-lemma ex1E:
+schematic_lemma ex1E:
assumes "p:EX! x. P(x)"
and "!!x u v. [| u:P(x); v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R"
shows "?a : R"
@@ -353,7 +353,7 @@
REPEAT1 (eresolve_tac [asm_rl, @{thm mp}] i)
*}
-lemma conj_cong:
+schematic_lemma conj_cong:
assumes "p:P <-> P'"
and "!!x. x:P' ==> q(x):Q <-> Q'"
shows "?p:(P&Q) <-> (P'&Q')"
@@ -362,12 +362,12 @@
erule iffE conjE mp | tactic {* iff_tac @{thms assms} 1 *})+
done
-lemma disj_cong:
+schematic_lemma disj_cong:
"[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P|Q) <-> (P'|Q')"
apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | tactic {* mp_tac 1 *})+
done
-lemma imp_cong:
+schematic_lemma imp_cong:
assumes "p:P <-> P'"
and "!!x. x:P' ==> q(x):Q <-> Q'"
shows "?p:(P-->Q) <-> (P'-->Q')"
@@ -376,24 +376,24 @@
tactic {* iff_tac @{thms assms} 1 *})+
done
-lemma iff_cong:
+schematic_lemma iff_cong:
"[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')"
apply (erule iffE | assumption | rule iffI | tactic {* mp_tac 1 *})+
done
-lemma not_cong:
+schematic_lemma not_cong:
"p:P <-> P' ==> ?p:~P <-> ~P'"
apply (assumption | rule iffI notI | tactic {* mp_tac 1 *} | erule iffE notE)+
done
-lemma all_cong:
+schematic_lemma all_cong:
assumes "!!x. f(x):P(x) <-> Q(x)"
shows "?p:(ALL x. P(x)) <-> (ALL x. Q(x))"
apply (assumption | rule iffI allI | tactic {* mp_tac 1 *} | erule allE |
tactic {* iff_tac @{thms assms} 1 *})+
done
-lemma ex_cong:
+schematic_lemma ex_cong:
assumes "!!x. f(x):P(x) <-> Q(x)"
shows "?p:(EX x. P(x)) <-> (EX x. Q(x))"
apply (erule exE | assumption | rule iffI exI | tactic {* mp_tac 1 *} |
@@ -413,7 +413,7 @@
lemmas refl = ieqI
-lemma subst:
+schematic_lemma subst:
assumes prem1: "p:a=b"
and prem2: "q:P(a)"
shows "?p : P(b)"
@@ -423,17 +423,17 @@
apply assumption
done
-lemma sym: "q:a=b ==> ?c:b=a"
+schematic_lemma sym: "q:a=b ==> ?c:b=a"
apply (erule subst)
apply (rule refl)
done
-lemma trans: "[| p:a=b; q:b=c |] ==> ?d:a=c"
+schematic_lemma trans: "[| p:a=b; q:b=c |] ==> ?d:a=c"
apply (erule (1) subst)
done
(** ~ b=a ==> ~ a=b **)
-lemma not_sym: "p:~ b=a ==> ?q:~ a=b"
+schematic_lemma not_sym: "p:~ b=a ==> ?q:~ a=b"
apply (erule contrapos)
apply (erule sym)
done
@@ -442,7 +442,7 @@
lemmas ssubst = sym [THEN subst, standard]
(*A special case of ex1E that would otherwise need quantifier expansion*)
-lemma ex1_equalsE: "[| p:EX! x. P(x); q:P(a); r:P(b) |] ==> ?d:a=b"
+schematic_lemma ex1_equalsE: "[| p:EX! x. P(x); q:P(a); r:P(b) |] ==> ?d:a=b"
apply (erule ex1E)
apply (rule trans)
apply (rule_tac [2] sym)
@@ -451,17 +451,17 @@
(** Polymorphic congruence rules **)
-lemma subst_context: "[| p:a=b |] ==> ?d:t(a)=t(b)"
+schematic_lemma subst_context: "[| p:a=b |] ==> ?d:t(a)=t(b)"
apply (erule ssubst)
apply (rule refl)
done
-lemma subst_context2: "[| p:a=b; q:c=d |] ==> ?p:t(a,c)=t(b,d)"
+schematic_lemma subst_context2: "[| p:a=b; q:c=d |] ==> ?p:t(a,c)=t(b,d)"
apply (erule ssubst)+
apply (rule refl)
done
-lemma subst_context3: "[| p:a=b; q:c=d; r:e=f |] ==> ?p:t(a,c,e)=t(b,d,f)"
+schematic_lemma subst_context3: "[| p:a=b; q:c=d; r:e=f |] ==> ?p:t(a,c,e)=t(b,d,f)"
apply (erule ssubst)+
apply (rule refl)
done
@@ -470,7 +470,7 @@
a = b
| |
c = d *)
-lemma box_equals: "[| p:a=b; q:a=c; r:b=d |] ==> ?p:c=d"
+schematic_lemma box_equals: "[| p:a=b; q:a=c; r:b=d |] ==> ?p:c=d"
apply (rule trans)
apply (rule trans)
apply (rule sym)
@@ -478,7 +478,7 @@
done
(*Dual of box_equals: for proving equalities backwards*)
-lemma simp_equals: "[| p:a=c; q:b=d; r:c=d |] ==> ?p:a=b"
+schematic_lemma simp_equals: "[| p:a=c; q:b=d; r:c=d |] ==> ?p:a=b"
apply (rule trans)
apply (rule trans)
apply (assumption | rule sym)+
@@ -486,17 +486,17 @@
(** Congruence rules for predicate letters **)
-lemma pred1_cong: "p:a=a' ==> ?p:P(a) <-> P(a')"
+schematic_lemma pred1_cong: "p:a=a' ==> ?p:P(a) <-> P(a')"
apply (rule iffI)
apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *})
done
-lemma pred2_cong: "[| p:a=a'; q:b=b' |] ==> ?p:P(a,b) <-> P(a',b')"
+schematic_lemma pred2_cong: "[| p:a=a'; q:b=b' |] ==> ?p:P(a,b) <-> P(a',b')"
apply (rule iffI)
apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *})
done
-lemma pred3_cong: "[| p:a=a'; q:b=b'; r:c=c' |] ==> ?p:P(a,b,c) <-> P(a',b',c')"
+schematic_lemma pred3_cong: "[| p:a=a'; q:b=b'; r:c=c' |] ==> ?p:P(a,b,c) <-> P(a',b',c')"
apply (rule iffI)
apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *})
done
@@ -514,14 +514,14 @@
R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
(preprint, University of St Andrews, 1991) ***)
-lemma conj_impE:
+schematic_lemma conj_impE:
assumes major: "p:(P&Q)-->S"
and minor: "!!x. x:P-->(Q-->S) ==> q(x):R"
shows "?p:R"
apply (assumption | rule conjI impI major [THEN mp] minor)+
done
-lemma disj_impE:
+schematic_lemma disj_impE:
assumes major: "p:(P|Q)-->S"
and minor: "!!x y.[| x:P-->S; y:Q-->S |] ==> q(x,y):R"
shows "?p:R"
@@ -532,7 +532,7 @@
(*Simplifies the implication. Classical version is stronger.
Still UNSAFE since Q must be provable -- backtracking needed. *)
-lemma imp_impE:
+schematic_lemma imp_impE:
assumes major: "p:(P-->Q)-->S"
and r1: "!!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q"
and r2: "!!x. x:S ==> r(x):R"
@@ -542,7 +542,7 @@
(*Simplifies the implication. Classical version is stronger.
Still UNSAFE since ~P must be provable -- backtracking needed. *)
-lemma not_impE:
+schematic_lemma not_impE:
assumes major: "p:~P --> S"
and r1: "!!y. y:P ==> q(y):False"
and r2: "!!y. y:S ==> r(y):R"
@@ -551,7 +551,7 @@
done
(*Simplifies the implication. UNSAFE. *)
-lemma iff_impE:
+schematic_lemma iff_impE:
assumes major: "p:(P<->Q)-->S"
and r1: "!!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q"
and r2: "!!x y.[| x:Q; y:P-->S |] ==> r(x,y):P"
@@ -561,7 +561,7 @@
done
(*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
-lemma all_impE:
+schematic_lemma all_impE:
assumes major: "p:(ALL x. P(x))-->S"
and r1: "!!x. q:P(x)"
and r2: "!!y. y:S ==> r(y):R"
@@ -570,7 +570,7 @@
done
(*Unsafe: (EX x.P(x))-->S is equivalent to ALL x.P(x)-->S. *)
-lemma ex_impE:
+schematic_lemma ex_impE:
assumes major: "p:(EX x. P(x))-->S"
and r: "!!y. y:P(a)-->S ==> q(y):R"
shows "?p:R"
@@ -578,7 +578,7 @@
done
-lemma rev_cut_eq:
+schematic_lemma rev_cut_eq:
assumes "p:a=b"
and "!!x. x:a=b ==> f(x):R"
shows "?p:R"
@@ -619,7 +619,7 @@
(*** Rewrite rules ***)
-lemma conj_rews:
+schematic_lemma conj_rews:
"?p1 : P & True <-> P"
"?p2 : True & P <-> P"
"?p3 : P & False <-> False"
@@ -631,7 +631,7 @@
apply (tactic {* fn st => IntPr.fast_tac 1 st *})+
done
-lemma disj_rews:
+schematic_lemma disj_rews:
"?p1 : P | True <-> True"
"?p2 : True | P <-> True"
"?p3 : P | False <-> P"
@@ -641,13 +641,13 @@
apply (tactic {* IntPr.fast_tac 1 *})+
done
-lemma not_rews:
+schematic_lemma not_rews:
"?p1 : ~ False <-> True"
"?p2 : ~ True <-> False"
apply (tactic {* IntPr.fast_tac 1 *})+
done
-lemma imp_rews:
+schematic_lemma imp_rews:
"?p1 : (P --> False) <-> ~P"
"?p2 : (P --> True) <-> True"
"?p3 : (False --> P) <-> True"
@@ -657,7 +657,7 @@
apply (tactic {* IntPr.fast_tac 1 *})+
done
-lemma iff_rews:
+schematic_lemma iff_rews:
"?p1 : (True <-> P) <-> P"
"?p2 : (P <-> True) <-> P"
"?p3 : (P <-> P) <-> True"
@@ -666,14 +666,14 @@
apply (tactic {* IntPr.fast_tac 1 *})+
done
-lemma quant_rews:
+schematic_lemma quant_rews:
"?p1 : (ALL x. P) <-> P"
"?p2 : (EX x. P) <-> P"
apply (tactic {* IntPr.fast_tac 1 *})+
done
(*These are NOT supplied by default!*)
-lemma distrib_rews1:
+schematic_lemma distrib_rews1:
"?p1 : ~(P|Q) <-> ~P & ~Q"
"?p2 : P & (Q | R) <-> P&Q | P&R"
"?p3 : (Q | R) & P <-> Q&P | R&P"
@@ -681,7 +681,7 @@
apply (tactic {* IntPr.fast_tac 1 *})+
done
-lemma distrib_rews2:
+schematic_lemma distrib_rews2:
"?p1 : ~(EX x. NORM(P(x))) <-> (ALL x. ~NORM(P(x)))"
"?p2 : ((EX x. NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)"
"?p3 : (EX x. NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))"
@@ -691,11 +691,11 @@
lemmas distrib_rews = distrib_rews1 distrib_rews2
-lemma P_Imp_P_iff_T: "p:P ==> ?p:(P <-> True)"
+schematic_lemma P_Imp_P_iff_T: "p:P ==> ?p:(P <-> True)"
apply (tactic {* IntPr.fast_tac 1 *})
done
-lemma not_P_imp_P_iff_F: "p:~P ==> ?p:(P <-> False)"
+schematic_lemma not_P_imp_P_iff_F: "p:~P ==> ?p:(P <-> False)"
apply (tactic {* IntPr.fast_tac 1 *})
done
--- a/src/FOLP/ex/Classical.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/FOLP/ex/Classical.thy Fri Apr 23 23:35:43 2010 +0200
@@ -9,14 +9,14 @@
imports FOLP
begin
-lemma "?p : (P --> Q | R) --> (P-->Q) | (P-->R)"
+schematic_lemma "?p : (P --> Q | R) --> (P-->Q) | (P-->R)"
by (tactic "fast_tac FOLP_cs 1")
(*If and only if*)
-lemma "?p : (P<->Q) <-> (Q<->P)"
+schematic_lemma "?p : (P<->Q) <-> (Q<->P)"
by (tactic "fast_tac FOLP_cs 1")
-lemma "?p : ~ (P <-> ~P)"
+schematic_lemma "?p : ~ (P <-> ~P)"
by (tactic "fast_tac FOLP_cs 1")
@@ -32,138 +32,138 @@
text "Pelletier's examples"
(*1*)
-lemma "?p : (P-->Q) <-> (~Q --> ~P)"
+schematic_lemma "?p : (P-->Q) <-> (~Q --> ~P)"
by (tactic "fast_tac FOLP_cs 1")
(*2*)
-lemma "?p : ~ ~ P <-> P"
+schematic_lemma "?p : ~ ~ P <-> P"
by (tactic "fast_tac FOLP_cs 1")
(*3*)
-lemma "?p : ~(P-->Q) --> (Q-->P)"
+schematic_lemma "?p : ~(P-->Q) --> (Q-->P)"
by (tactic "fast_tac FOLP_cs 1")
(*4*)
-lemma "?p : (~P-->Q) <-> (~Q --> P)"
+schematic_lemma "?p : (~P-->Q) <-> (~Q --> P)"
by (tactic "fast_tac FOLP_cs 1")
(*5*)
-lemma "?p : ((P|Q)-->(P|R)) --> (P|(Q-->R))"
+schematic_lemma "?p : ((P|Q)-->(P|R)) --> (P|(Q-->R))"
by (tactic "fast_tac FOLP_cs 1")
(*6*)
-lemma "?p : P | ~ P"
+schematic_lemma "?p : P | ~ P"
by (tactic "fast_tac FOLP_cs 1")
(*7*)
-lemma "?p : P | ~ ~ ~ P"
+schematic_lemma "?p : P | ~ ~ ~ P"
by (tactic "fast_tac FOLP_cs 1")
(*8. Peirce's law*)
-lemma "?p : ((P-->Q) --> P) --> P"
+schematic_lemma "?p : ((P-->Q) --> P) --> P"
by (tactic "fast_tac FOLP_cs 1")
(*9*)
-lemma "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
+schematic_lemma "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
by (tactic "fast_tac FOLP_cs 1")
(*10*)
-lemma "?p : (Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)"
+schematic_lemma "?p : (Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)"
by (tactic "fast_tac FOLP_cs 1")
(*11. Proved in each direction (incorrectly, says Pelletier!!) *)
-lemma "?p : P<->P"
+schematic_lemma "?p : P<->P"
by (tactic "fast_tac FOLP_cs 1")
(*12. "Dijkstra's law"*)
-lemma "?p : ((P <-> Q) <-> R) <-> (P <-> (Q <-> R))"
+schematic_lemma "?p : ((P <-> Q) <-> R) <-> (P <-> (Q <-> R))"
by (tactic "fast_tac FOLP_cs 1")
(*13. Distributive law*)
-lemma "?p : P | (Q & R) <-> (P | Q) & (P | R)"
+schematic_lemma "?p : P | (Q & R) <-> (P | Q) & (P | R)"
by (tactic "fast_tac FOLP_cs 1")
(*14*)
-lemma "?p : (P <-> Q) <-> ((Q | ~P) & (~Q|P))"
+schematic_lemma "?p : (P <-> Q) <-> ((Q | ~P) & (~Q|P))"
by (tactic "fast_tac FOLP_cs 1")
(*15*)
-lemma "?p : (P --> Q) <-> (~P | Q)"
+schematic_lemma "?p : (P --> Q) <-> (~P | Q)"
by (tactic "fast_tac FOLP_cs 1")
(*16*)
-lemma "?p : (P-->Q) | (Q-->P)"
+schematic_lemma "?p : (P-->Q) | (Q-->P)"
by (tactic "fast_tac FOLP_cs 1")
(*17*)
-lemma "?p : ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))"
+schematic_lemma "?p : ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))"
by (tactic "fast_tac FOLP_cs 1")
text "Classical Logic: examples with quantifiers"
-lemma "?p : (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))"
+schematic_lemma "?p : (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))"
by (tactic "fast_tac FOLP_cs 1")
-lemma "?p : (EX x. P-->Q(x)) <-> (P --> (EX x. Q(x)))"
+schematic_lemma "?p : (EX x. P-->Q(x)) <-> (P --> (EX x. Q(x)))"
by (tactic "fast_tac FOLP_cs 1")
-lemma "?p : (EX x. P(x)-->Q) <-> (ALL x. P(x)) --> Q"
+schematic_lemma "?p : (EX x. P(x)-->Q) <-> (ALL x. P(x)) --> Q"
by (tactic "fast_tac FOLP_cs 1")
-lemma "?p : (ALL x. P(x)) | Q <-> (ALL x. P(x) | Q)"
+schematic_lemma "?p : (ALL x. P(x)) | Q <-> (ALL x. P(x) | Q)"
by (tactic "fast_tac FOLP_cs 1")
text "Problems requiring quantifier duplication"
(*Needs multiple instantiation of ALL.*)
-lemma "?p : (ALL x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))"
+schematic_lemma "?p : (ALL x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))"
by (tactic "best_tac FOLP_dup_cs 1")
(*Needs double instantiation of the quantifier*)
-lemma "?p : EX x. P(x) --> P(a) & P(b)"
+schematic_lemma "?p : EX x. P(x) --> P(a) & P(b)"
by (tactic "best_tac FOLP_dup_cs 1")
-lemma "?p : EX z. P(z) --> (ALL x. P(x))"
+schematic_lemma "?p : EX z. P(z) --> (ALL x. P(x))"
by (tactic "best_tac FOLP_dup_cs 1")
text "Hard examples with quantifiers"
text "Problem 18"
-lemma "?p : EX y. ALL x. P(y)-->P(x)"
+schematic_lemma "?p : EX y. ALL x. P(y)-->P(x)"
by (tactic "best_tac FOLP_dup_cs 1")
text "Problem 19"
-lemma "?p : EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
+schematic_lemma "?p : EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
by (tactic "best_tac FOLP_dup_cs 1")
text "Problem 20"
-lemma "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))
+schematic_lemma "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))
--> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"
by (tactic "fast_tac FOLP_cs 1")
text "Problem 21"
-lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))";
+schematic_lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))";
by (tactic "best_tac FOLP_dup_cs 1")
text "Problem 22"
-lemma "?p : (ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))"
+schematic_lemma "?p : (ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))"
by (tactic "fast_tac FOLP_cs 1")
text "Problem 23"
-lemma "?p : (ALL x. P | Q(x)) <-> (P | (ALL x. Q(x)))"
+schematic_lemma "?p : (ALL x. P | Q(x)) <-> (P | (ALL x. Q(x)))"
by (tactic "best_tac FOLP_dup_cs 1")
text "Problem 24"
-lemma "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &
+schematic_lemma "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &
(~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))
--> (EX x. P(x)&R(x))"
by (tactic "fast_tac FOLP_cs 1")
text "Problem 25"
-lemma "?p : (EX x. P(x)) &
+schematic_lemma "?p : (EX x. P(x)) &
(ALL x. L(x) --> ~ (M(x) & R(x))) &
(ALL x. P(x) --> (M(x) & L(x))) &
((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))
@@ -171,13 +171,13 @@
oops
text "Problem 26"
-lemma "?u : ((EX x. p(x)) <-> (EX x. q(x))) &
+schematic_lemma "?u : ((EX x. p(x)) <-> (EX x. q(x))) &
(ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))
--> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
by (tactic "fast_tac FOLP_cs 1")
text "Problem 27"
-lemma "?p : (EX x. P(x) & ~Q(x)) &
+schematic_lemma "?p : (EX x. P(x) & ~Q(x)) &
(ALL x. P(x) --> R(x)) &
(ALL x. M(x) & L(x) --> P(x)) &
((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))
@@ -185,49 +185,49 @@
by (tactic "fast_tac FOLP_cs 1")
text "Problem 28. AMENDED"
-lemma "?p : (ALL x. P(x) --> (ALL x. Q(x))) &
+schematic_lemma "?p : (ALL x. P(x) --> (ALL x. Q(x))) &
((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &
((EX x. S(x)) --> (ALL x. L(x) --> M(x)))
--> (ALL x. P(x) & L(x) --> M(x))"
by (tactic "fast_tac FOLP_cs 1")
text "Problem 29. Essentially the same as Principia Mathematica *11.71"
-lemma "?p : (EX x. P(x)) & (EX y. Q(y))
+schematic_lemma "?p : (EX x. P(x)) & (EX y. Q(y))
--> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y)) <->
(ALL x y. P(x) & Q(y) --> R(x) & S(y)))"
by (tactic "fast_tac FOLP_cs 1")
text "Problem 30"
-lemma "?p : (ALL x. P(x) | Q(x) --> ~ R(x)) &
+schematic_lemma "?p : (ALL x. P(x) | Q(x) --> ~ R(x)) &
(ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))
--> (ALL x. S(x))"
by (tactic "fast_tac FOLP_cs 1")
text "Problem 31"
-lemma "?p : ~(EX x. P(x) & (Q(x) | R(x))) &
+schematic_lemma "?p : ~(EX x. P(x) & (Q(x) | R(x))) &
(EX x. L(x) & P(x)) &
(ALL x. ~ R(x) --> M(x))
--> (EX x. L(x) & M(x))"
by (tactic "fast_tac FOLP_cs 1")
text "Problem 32"
-lemma "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) &
+schematic_lemma "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) &
(ALL x. S(x) & R(x) --> L(x)) &
(ALL x. M(x) --> R(x))
--> (ALL x. P(x) & M(x) --> L(x))"
by (tactic "best_tac FOLP_dup_cs 1")
text "Problem 33"
-lemma "?p : (ALL x. P(a) & (P(x)-->P(b))-->P(c)) <->
+schematic_lemma "?p : (ALL x. P(a) & (P(x)-->P(b))-->P(c)) <->
(ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"
by (tactic "best_tac FOLP_dup_cs 1")
text "Problem 35"
-lemma "?p : EX x y. P(x,y) --> (ALL u v. P(u,v))"
+schematic_lemma "?p : EX x y. P(x,y) --> (ALL u v. P(u,v))"
by (tactic "best_tac FOLP_dup_cs 1")
text "Problem 36"
-lemma
+schematic_lemma
"?p : (ALL x. EX y. J(x,y)) &
(ALL x. EX y. G(x,y)) &
(ALL x y. J(x,y) | G(x,y) --> (ALL z. J(y,z) | G(y,z) --> H(x,z)))
@@ -235,7 +235,7 @@
by (tactic "fast_tac FOLP_cs 1")
text "Problem 37"
-lemma "?p : (ALL z. EX w. ALL x. EX y.
+schematic_lemma "?p : (ALL z. EX w. ALL x. EX y.
(P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) &
(ALL x z. ~P(x,z) --> (EX y. Q(y,z))) &
((EX x y. Q(x,y)) --> (ALL x. R(x,x)))
@@ -243,21 +243,21 @@
by (tactic "fast_tac FOLP_cs 1")
text "Problem 39"
-lemma "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
+schematic_lemma "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
by (tactic "fast_tac FOLP_cs 1")
text "Problem 40. AMENDED"
-lemma "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->
+schematic_lemma "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->
~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"
by (tactic "fast_tac FOLP_cs 1")
text "Problem 41"
-lemma "?p : (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))
+schematic_lemma "?p : (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))
--> ~ (EX z. ALL x. f(x,z))"
by (tactic "best_tac FOLP_dup_cs 1")
text "Problem 44"
-lemma "?p : (ALL x. f(x) -->
+schematic_lemma "?p : (ALL x. f(x) -->
(EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) &
(EX x. j(x) & (ALL y. g(y) --> h(x,y)))
--> (EX x. j(x) & ~f(x))"
@@ -266,37 +266,37 @@
text "Problems (mainly) involving equality or functions"
text "Problem 48"
-lemma "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c"
+schematic_lemma "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c"
by (tactic "fast_tac FOLP_cs 1")
text "Problem 50"
(*What has this to do with equality?*)
-lemma "?p : (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))"
+schematic_lemma "?p : (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))"
by (tactic "best_tac FOLP_dup_cs 1")
text "Problem 56"
-lemma
+schematic_lemma
"?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
by (tactic "fast_tac FOLP_cs 1")
text "Problem 57"
-lemma
+schematic_lemma
"?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &
(ALL x y z. P(x,y) & P(y,z) --> P(x,z)) --> P(f(a,b), f(a,c))"
by (tactic "fast_tac FOLP_cs 1")
text "Problem 58 NOT PROVED AUTOMATICALLY"
-lemma
+schematic_lemma
notes f_cong = subst_context [where t = f]
shows "?p : (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))"
by (tactic {* fast_tac (FOLP_cs addSIs [@{thm f_cong}]) 1 *})
text "Problem 59"
-lemma "?p : (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))"
+schematic_lemma "?p : (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))"
by (tactic "best_tac FOLP_dup_cs 1")
text "Problem 60"
-lemma "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
+schematic_lemma "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
by (tactic "fast_tac FOLP_cs 1")
end
--- a/src/FOLP/ex/Foundation.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/FOLP/ex/Foundation.thy Fri Apr 23 23:35:43 2010 +0200
@@ -9,7 +9,7 @@
imports IFOLP
begin
-lemma "?p : A&B --> (C-->A&C)"
+schematic_lemma "?p : A&B --> (C-->A&C)"
apply (rule impI)
apply (rule impI)
apply (rule conjI)
@@ -19,7 +19,7 @@
done
text {*A form of conj-elimination*}
-lemma
+schematic_lemma
assumes "p : A & B"
and "!!x y. x : A ==> y : B ==> f(x, y) : C"
shows "?p : C"
@@ -30,7 +30,7 @@
apply (rule prems)
done
-lemma
+schematic_lemma
assumes "!!A x. x : ~ ~A ==> cla(x) : A"
shows "?p : B | ~B"
apply (rule prems)
@@ -48,7 +48,7 @@
apply assumption
done
-lemma
+schematic_lemma
assumes "!!A x. x : ~ ~A ==> cla(x) : A"
shows "?p : B | ~B"
apply (rule prems)
@@ -63,7 +63,7 @@
done
-lemma
+schematic_lemma
assumes "p : A | ~A"
and "q : ~ ~A"
shows "?p : A"
@@ -79,7 +79,7 @@
subsection "Examples with quantifiers"
-lemma
+schematic_lemma
assumes "p : ALL z. G(z)"
shows "?p : ALL z. G(z)|H(z)"
apply (rule allI)
@@ -87,20 +87,20 @@
apply (rule prems [THEN spec])
done
-lemma "?p : ALL x. EX y. x=y"
+schematic_lemma "?p : ALL x. EX y. x=y"
apply (rule allI)
apply (rule exI)
apply (rule refl)
done
-lemma "?p : EX y. ALL x. x=y"
+schematic_lemma "?p : EX y. ALL x. x=y"
apply (rule exI)
apply (rule allI)
apply (rule refl)?
oops
text {* Parallel lifting example. *}
-lemma "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)"
+schematic_lemma "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)"
apply (rule exI allI)
apply (rule exI allI)
apply (rule exI allI)
@@ -108,7 +108,7 @@
apply (rule exI allI)
oops
-lemma
+schematic_lemma
assumes "p : (EX z. F(z)) & B"
shows "?p : EX z. F(z) & B"
apply (rule conjE)
@@ -122,7 +122,7 @@
done
text {* A bigger demonstration of quantifiers -- not in the paper. *}
-lemma "?p : (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"
+schematic_lemma "?p : (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"
apply (rule impI)
apply (rule allI)
apply (rule exE, assumption)
--- a/src/FOLP/ex/If.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/FOLP/ex/If.thy Fri Apr 23 23:35:43 2010 +0200
@@ -5,14 +5,14 @@
definition "if" :: "[o,o,o]=>o" where
"if(P,Q,R) == P&Q | ~P&R"
-lemma ifI:
+schematic_lemma ifI:
assumes "!!x. x : P ==> f(x) : Q" "!!x. x : ~P ==> g(x) : R"
shows "?p : if(P,Q,R)"
apply (unfold if_def)
apply (tactic {* fast_tac (FOLP_cs addIs @{thms assms}) 1 *})
done
-lemma ifE:
+schematic_lemma ifE:
assumes 1: "p : if(P,Q,R)" and
2: "!!x y. [| x : P; y : Q |] ==> f(x, y) : S" and
3: "!!x y. [| x : ~P; y : R |] ==> g(x, y) : S"
@@ -22,7 +22,7 @@
apply (tactic {* fast_tac (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1 *})
done
-lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
+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))"
apply (rule iffI)
apply (erule ifE)
apply (erule ifE)
@@ -32,11 +32,11 @@
ML {* val if_cs = FOLP_cs addSIs [@{thm ifI}] addSEs [@{thm ifE}] *}
-lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
+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))"
apply (tactic {* fast_tac if_cs 1 *})
done
-lemma nested_ifs: "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
+schematic_lemma nested_ifs: "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
apply (tactic {* fast_tac if_cs 1 *})
done
--- a/src/FOLP/ex/Intro.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/FOLP/ex/Intro.thy Fri Apr 23 23:35:43 2010 +0200
@@ -13,7 +13,7 @@
subsubsection {* Some simple backward proofs *}
-lemma mythm: "?p : P|P --> P"
+schematic_lemma mythm: "?p : P|P --> P"
apply (rule impI)
apply (rule disjE)
prefer 3 apply (assumption)
@@ -21,7 +21,7 @@
apply assumption
done
-lemma "?p : (P & Q) | R --> (P | R)"
+schematic_lemma "?p : (P & Q) | R --> (P | R)"
apply (rule impI)
apply (erule disjE)
apply (drule conjunct1)
@@ -31,7 +31,7 @@
done
(*Correct version, delaying use of "spec" until last*)
-lemma "?p : (ALL x y. P(x,y)) --> (ALL z w. P(w,z))"
+schematic_lemma "?p : (ALL x y. P(x,y)) --> (ALL z w. P(w,z))"
apply (rule impI)
apply (rule allI)
apply (rule allI)
@@ -43,13 +43,13 @@
subsubsection {* Demonstration of @{text "fast"} *}
-lemma "?p : (EX y. ALL x. J(y,x) <-> ~J(x,x))
+schematic_lemma "?p : (EX y. ALL x. J(y,x) <-> ~J(x,x))
--> ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))"
apply (tactic {* fast_tac FOLP_cs 1 *})
done
-lemma "?p : ALL x. P(x,f(x)) <->
+schematic_lemma "?p : ALL x. P(x,f(x)) <->
(EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
apply (tactic {* fast_tac FOLP_cs 1 *})
done
@@ -57,7 +57,7 @@
subsubsection {* Derivation of conjunction elimination rule *}
-lemma
+schematic_lemma
assumes major: "p : P&Q"
and minor: "!!x y. [| x : P; y : Q |] ==> f(x, y) : R"
shows "?p : R"
@@ -71,7 +71,7 @@
text {* Derivation of negation introduction *}
-lemma
+schematic_lemma
assumes "!!x. x : P ==> f(x) : False"
shows "?p : ~ P"
apply (unfold not_def)
@@ -80,7 +80,7 @@
apply assumption
done
-lemma
+schematic_lemma
assumes major: "p : ~P"
and minor: "q : P"
shows "?p : R"
@@ -91,7 +91,7 @@
done
text {* Alternative proof of the result above *}
-lemma
+schematic_lemma
assumes major: "p : ~P"
and minor: "q : P"
shows "?p : R"
--- a/src/FOLP/ex/Intuitionistic.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/FOLP/ex/Intuitionistic.thy Fri Apr 23 23:35:43 2010 +0200
@@ -30,39 +30,39 @@
imports IFOLP
begin
-lemma "?p : ~~(P&Q) <-> ~~P & ~~Q"
+schematic_lemma "?p : ~~(P&Q) <-> ~~P & ~~Q"
by (tactic {* IntPr.fast_tac 1 *})
-lemma "?p : ~~~P <-> ~P"
+schematic_lemma "?p : ~~~P <-> ~P"
by (tactic {* IntPr.fast_tac 1 *})
-lemma "?p : ~~((P --> Q | R) --> (P-->Q) | (P-->R))"
+schematic_lemma "?p : ~~((P --> Q | R) --> (P-->Q) | (P-->R))"
by (tactic {* IntPr.fast_tac 1 *})
-lemma "?p : (P<->Q) <-> (Q<->P)"
+schematic_lemma "?p : (P<->Q) <-> (Q<->P)"
by (tactic {* IntPr.fast_tac 1 *})
subsection {* Lemmas for the propositional double-negation translation *}
-lemma "?p : P --> ~~P"
+schematic_lemma "?p : P --> ~~P"
by (tactic {* IntPr.fast_tac 1 *})
-lemma "?p : ~~(~~P --> P)"
+schematic_lemma "?p : ~~(~~P --> P)"
by (tactic {* IntPr.fast_tac 1 *})
-lemma "?p : ~~P & ~~(P --> Q) --> ~~Q"
+schematic_lemma "?p : ~~P & ~~(P --> Q) --> ~~Q"
by (tactic {* IntPr.fast_tac 1 *})
subsection {* The following are classically but not constructively valid *}
(*The attempt to prove them terminates quickly!*)
-lemma "?p : ((P-->Q) --> P) --> P"
+schematic_lemma "?p : ((P-->Q) --> P) --> P"
apply (tactic {* IntPr.fast_tac 1 *})?
oops
-lemma "?p : (P&Q-->R) --> (P-->R) | (Q-->R)"
+schematic_lemma "?p : (P&Q-->R) --> (P-->R) | (Q-->R)"
apply (tactic {* IntPr.fast_tac 1 *})?
oops
@@ -70,74 +70,74 @@
subsection {* Intuitionistic FOL: propositional problems based on Pelletier *}
text "Problem ~~1"
-lemma "?p : ~~((P-->Q) <-> (~Q --> ~P))"
+schematic_lemma "?p : ~~((P-->Q) <-> (~Q --> ~P))"
by (tactic {* IntPr.fast_tac 1 *})
text "Problem ~~2"
-lemma "?p : ~~(~~P <-> P)"
+schematic_lemma "?p : ~~(~~P <-> P)"
by (tactic {* IntPr.fast_tac 1 *})
text "Problem 3"
-lemma "?p : ~(P-->Q) --> (Q-->P)"
+schematic_lemma "?p : ~(P-->Q) --> (Q-->P)"
by (tactic {* IntPr.fast_tac 1 *})
text "Problem ~~4"
-lemma "?p : ~~((~P-->Q) <-> (~Q --> P))"
+schematic_lemma "?p : ~~((~P-->Q) <-> (~Q --> P))"
by (tactic {* IntPr.fast_tac 1 *})
text "Problem ~~5"
-lemma "?p : ~~((P|Q-->P|R) --> P|(Q-->R))"
+schematic_lemma "?p : ~~((P|Q-->P|R) --> P|(Q-->R))"
by (tactic {* IntPr.fast_tac 1 *})
text "Problem ~~6"
-lemma "?p : ~~(P | ~P)"
+schematic_lemma "?p : ~~(P | ~P)"
by (tactic {* IntPr.fast_tac 1 *})
text "Problem ~~7"
-lemma "?p : ~~(P | ~~~P)"
+schematic_lemma "?p : ~~(P | ~~~P)"
by (tactic {* IntPr.fast_tac 1 *})
text "Problem ~~8. Peirce's law"
-lemma "?p : ~~(((P-->Q) --> P) --> P)"
+schematic_lemma "?p : ~~(((P-->Q) --> P) --> P)"
by (tactic {* IntPr.fast_tac 1 *})
text "Problem 9"
-lemma "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
+schematic_lemma "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
by (tactic {* IntPr.fast_tac 1 *})
text "Problem 10"
-lemma "?p : (Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)"
+schematic_lemma "?p : (Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)"
by (tactic {* IntPr.fast_tac 1 *})
text "11. Proved in each direction (incorrectly, says Pelletier!!) "
-lemma "?p : P<->P"
+schematic_lemma "?p : P<->P"
by (tactic {* IntPr.fast_tac 1 *})
text "Problem ~~12. Dijkstra's law "
-lemma "?p : ~~(((P <-> Q) <-> R) <-> (P <-> (Q <-> R)))"
+schematic_lemma "?p : ~~(((P <-> Q) <-> R) <-> (P <-> (Q <-> R)))"
by (tactic {* IntPr.fast_tac 1 *})
-lemma "?p : ((P <-> Q) <-> R) --> ~~(P <-> (Q <-> R))"
+schematic_lemma "?p : ((P <-> Q) <-> R) --> ~~(P <-> (Q <-> R))"
by (tactic {* IntPr.fast_tac 1 *})
text "Problem 13. Distributive law"
-lemma "?p : P | (Q & R) <-> (P | Q) & (P | R)"
+schematic_lemma "?p : P | (Q & R) <-> (P | Q) & (P | R)"
by (tactic {* IntPr.fast_tac 1 *})
text "Problem ~~14"
-lemma "?p : ~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))"
+schematic_lemma "?p : ~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))"
by (tactic {* IntPr.fast_tac 1 *})
text "Problem ~~15"
-lemma "?p : ~~((P --> Q) <-> (~P | Q))"
+schematic_lemma "?p : ~~((P --> Q) <-> (~P | Q))"
by (tactic {* IntPr.fast_tac 1 *})
text "Problem ~~16"
-lemma "?p : ~~((P-->Q) | (Q-->P))"
+schematic_lemma "?p : ~~((P-->Q) | (Q-->P))"
by (tactic {* IntPr.fast_tac 1 *})
text "Problem ~~17"
-lemma "?p : ~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))"
+schematic_lemma "?p : ~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))"
by (tactic {* IntPr.fast_tac 1 *}) -- slow
@@ -145,43 +145,43 @@
text "The converse is classical in the following implications..."
-lemma "?p : (EX x. P(x)-->Q) --> (ALL x. P(x)) --> Q"
+schematic_lemma "?p : (EX x. P(x)-->Q) --> (ALL x. P(x)) --> Q"
by (tactic {* IntPr.fast_tac 1 *})
-lemma "?p : ((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)"
+schematic_lemma "?p : ((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)"
by (tactic {* IntPr.fast_tac 1 *})
-lemma "?p : ((ALL x. ~P(x))-->Q) --> ~ (ALL x. ~ (P(x)|Q))"
+schematic_lemma "?p : ((ALL x. ~P(x))-->Q) --> ~ (ALL x. ~ (P(x)|Q))"
by (tactic {* IntPr.fast_tac 1 *})
-lemma "?p : (ALL x. P(x)) | Q --> (ALL x. P(x) | Q)"
+schematic_lemma "?p : (ALL x. P(x)) | Q --> (ALL x. P(x) | Q)"
by (tactic {* IntPr.fast_tac 1 *})
-lemma "?p : (EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))"
+schematic_lemma "?p : (EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))"
by (tactic {* IntPr.fast_tac 1 *})
text "The following are not constructively valid!"
text "The attempt to prove them terminates quickly!"
-lemma "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)"
+schematic_lemma "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)"
apply (tactic {* IntPr.fast_tac 1 *})?
oops
-lemma "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))"
+schematic_lemma "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))"
apply (tactic {* IntPr.fast_tac 1 *})?
oops
-lemma "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)"
+schematic_lemma "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)"
apply (tactic {* IntPr.fast_tac 1 *})?
oops
-lemma "?p : (ALL x. ~~P(x)) --> ~~(ALL x. P(x))"
+schematic_lemma "?p : (ALL x. ~~P(x)) --> ~~(ALL x. P(x))"
apply (tactic {* IntPr.fast_tac 1 *})?
oops
(*Classically but not intuitionistically valid. Proved by a bug in 1986!*)
-lemma "?p : EX x. Q(x) --> (ALL x. Q(x))"
+schematic_lemma "?p : EX x. Q(x) --> (ALL x. Q(x))"
apply (tactic {* IntPr.fast_tac 1 *})?
oops
@@ -194,32 +194,32 @@
*}
text "Problem ~~18"
-lemma "?p : ~~(EX y. ALL x. P(y)-->P(x))" oops
+schematic_lemma "?p : ~~(EX y. ALL x. P(y)-->P(x))" oops
(*NOT PROVED*)
text "Problem ~~19"
-lemma "?p : ~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))" oops
+schematic_lemma "?p : ~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))" oops
(*NOT PROVED*)
text "Problem 20"
-lemma "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))
+schematic_lemma "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))
--> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"
by (tactic {* IntPr.fast_tac 1 *})
text "Problem 21"
-lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))" oops
+schematic_lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))" oops
(*NOT PROVED*)
text "Problem 22"
-lemma "?p : (ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))"
+schematic_lemma "?p : (ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))"
by (tactic {* IntPr.fast_tac 1 *})
text "Problem ~~23"
-lemma "?p : ~~ ((ALL x. P | Q(x)) <-> (P | (ALL x. Q(x))))"
+schematic_lemma "?p : ~~ ((ALL x. P | Q(x)) <-> (P | (ALL x. Q(x))))"
by (tactic {* IntPr.fast_tac 1 *})
text "Problem 24"
-lemma "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &
+schematic_lemma "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &
(~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))
--> ~~(EX x. P(x)&R(x))"
(*Not clear why fast_tac, best_tac, ASTAR and ITER_DEEPEN all take forever*)
@@ -230,7 +230,7 @@
done
text "Problem 25"
-lemma "?p : (EX x. P(x)) &
+schematic_lemma "?p : (EX x. P(x)) &
(ALL x. L(x) --> ~ (M(x) & R(x))) &
(ALL x. P(x) --> (M(x) & L(x))) &
((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))
@@ -238,69 +238,69 @@
by (tactic "IntPr.best_tac 1")
text "Problem 29. Essentially the same as Principia Mathematica *11.71"
-lemma "?p : (EX x. P(x)) & (EX y. Q(y))
+schematic_lemma "?p : (EX x. P(x)) & (EX y. Q(y))
--> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y)) <->
(ALL x y. P(x) & Q(y) --> R(x) & S(y)))"
by (tactic "IntPr.fast_tac 1")
text "Problem ~~30"
-lemma "?p : (ALL x. (P(x) | Q(x)) --> ~ R(x)) &
+schematic_lemma "?p : (ALL x. (P(x) | Q(x)) --> ~ R(x)) &
(ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))
--> (ALL x. ~~S(x))"
by (tactic "IntPr.fast_tac 1")
text "Problem 31"
-lemma "?p : ~(EX x. P(x) & (Q(x) | R(x))) &
+schematic_lemma "?p : ~(EX x. P(x) & (Q(x) | R(x))) &
(EX x. L(x) & P(x)) &
(ALL x. ~ R(x) --> M(x))
--> (EX x. L(x) & M(x))"
by (tactic "IntPr.fast_tac 1")
text "Problem 32"
-lemma "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) &
+schematic_lemma "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) &
(ALL x. S(x) & R(x) --> L(x)) &
(ALL x. M(x) --> R(x))
--> (ALL x. P(x) & M(x) --> L(x))"
by (tactic "IntPr.best_tac 1") -- slow
text "Problem 39"
-lemma "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
+schematic_lemma "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
by (tactic "IntPr.best_tac 1")
text "Problem 40. AMENDED"
-lemma "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->
+schematic_lemma "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->
~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"
by (tactic "IntPr.best_tac 1") -- slow
text "Problem 44"
-lemma "?p : (ALL x. f(x) -->
+schematic_lemma "?p : (ALL x. f(x) -->
(EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) &
(EX x. j(x) & (ALL y. g(y) --> h(x,y)))
--> (EX x. j(x) & ~f(x))"
by (tactic "IntPr.best_tac 1")
text "Problem 48"
-lemma "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c"
+schematic_lemma "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c"
by (tactic "IntPr.best_tac 1")
text "Problem 51"
-lemma
+schematic_lemma
"?p : (EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) -->
(EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)"
by (tactic "IntPr.best_tac 1") -- {*60 seconds*}
text "Problem 56"
-lemma "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
+schematic_lemma "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
by (tactic "IntPr.best_tac 1")
text "Problem 57"
-lemma
+schematic_lemma
"?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &
(ALL x y z. P(x,y) & P(y,z) --> P(x,z)) --> P(f(a,b), f(a,c))"
by (tactic "IntPr.best_tac 1")
text "Problem 60"
-lemma "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
+schematic_lemma "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
by (tactic "IntPr.best_tac 1")
end
--- a/src/FOLP/ex/Nat.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/FOLP/ex/Nat.thy Fri Apr 23 23:35:43 2010 +0200
@@ -44,7 +44,7 @@
subsection {* Proofs about the natural numbers *}
-lemma Suc_n_not_n: "?p : ~ (Suc(k) = k)"
+schematic_lemma Suc_n_not_n: "?p : ~ (Suc(k) = k)"
apply (rule_tac n = k in induct)
apply (rule notI)
apply (erule Suc_neq_0)
@@ -53,7 +53,7 @@
apply (erule Suc_inject)
done
-lemma "?p : (k+m)+n = k+(m+n)"
+schematic_lemma "?p : (k+m)+n = k+(m+n)"
apply (rule induct)
back
back
@@ -63,23 +63,23 @@
back
oops
-lemma add_0 [simp]: "?p : 0+n = n"
+schematic_lemma add_0 [simp]: "?p : 0+n = n"
apply (unfold add_def)
apply (rule rec_0)
done
-lemma add_Suc [simp]: "?p : Suc(m)+n = Suc(m+n)"
+schematic_lemma add_Suc [simp]: "?p : Suc(m)+n = Suc(m+n)"
apply (unfold add_def)
apply (rule rec_Suc)
done
-lemma Suc_cong: "p : x = y \<Longrightarrow> ?p : Suc(x) = Suc(y)"
+schematic_lemma Suc_cong: "p : x = y \<Longrightarrow> ?p : Suc(x) = Suc(y)"
apply (erule subst)
apply (rule refl)
done
-lemma Plus_cong: "[| p : a = x; q: b = y |] ==> ?p : a + b = x + y"
+schematic_lemma Plus_cong: "[| p : a = x; q: b = y |] ==> ?p : a + b = x + y"
apply (erule subst, erule subst, rule refl)
done
@@ -89,19 +89,19 @@
val add_ss = FOLP_ss addcongs @{thms nat_congs} addrews [@{thm add_0}, @{thm add_Suc}]
*}
-lemma add_assoc: "?p : (k+m)+n = k+(m+n)"
+schematic_lemma add_assoc: "?p : (k+m)+n = k+(m+n)"
apply (rule_tac n = k in induct)
apply (tactic {* SIMP_TAC add_ss 1 *})
apply (tactic {* ASM_SIMP_TAC add_ss 1 *})
done
-lemma add_0_right: "?p : m+0 = m"
+schematic_lemma add_0_right: "?p : m+0 = m"
apply (rule_tac n = m in induct)
apply (tactic {* SIMP_TAC add_ss 1 *})
apply (tactic {* ASM_SIMP_TAC add_ss 1 *})
done
-lemma add_Suc_right: "?p : m+Suc(n) = Suc(m+n)"
+schematic_lemma add_Suc_right: "?p : m+Suc(n) = Suc(m+n)"
apply (rule_tac n = m in induct)
apply (tactic {* ALLGOALS (ASM_SIMP_TAC add_ss) *})
done
--- a/src/FOLP/ex/Propositional_Cla.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/FOLP/ex/Propositional_Cla.thy Fri Apr 23 23:35:43 2010 +0200
@@ -11,103 +11,103 @@
text "commutative laws of & and | "
-lemma "?p : P & Q --> Q & P"
+schematic_lemma "?p : P & Q --> Q & P"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
-lemma "?p : P | Q --> Q | P"
+schematic_lemma "?p : P | Q --> Q | P"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
text "associative laws of & and | "
-lemma "?p : (P & Q) & R --> P & (Q & R)"
+schematic_lemma "?p : (P & Q) & R --> P & (Q & R)"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
-lemma "?p : (P | Q) | R --> P | (Q | R)"
+schematic_lemma "?p : (P | Q) | R --> P | (Q | R)"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
text "distributive laws of & and | "
-lemma "?p : (P & Q) | R --> (P | R) & (Q | R)"
+schematic_lemma "?p : (P & Q) | R --> (P | R) & (Q | R)"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
-lemma "?p : (P | R) & (Q | R) --> (P & Q) | R"
+schematic_lemma "?p : (P | R) & (Q | R) --> (P & Q) | R"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
-lemma "?p : (P | Q) & R --> (P & R) | (Q & R)"
+schematic_lemma "?p : (P | Q) & R --> (P & R) | (Q & R)"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
-lemma "?p : (P & R) | (Q & R) --> (P | Q) & R"
+schematic_lemma "?p : (P & R) | (Q & R) --> (P | Q) & R"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
text "Laws involving implication"
-lemma "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)"
+schematic_lemma "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
-lemma "?p : (P & Q --> R) <-> (P--> (Q-->R))"
+schematic_lemma "?p : (P & Q --> R) <-> (P--> (Q-->R))"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
-lemma "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
+schematic_lemma "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
-lemma "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
+schematic_lemma "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
-lemma "?p : (P --> Q & R) <-> (P-->Q) & (P-->R)"
+schematic_lemma "?p : (P --> Q & R) <-> (P-->Q) & (P-->R)"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
text "Propositions-as-types"
(*The combinator K*)
-lemma "?p : P --> (Q --> P)"
+schematic_lemma "?p : P --> (Q --> P)"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
(*The combinator S*)
-lemma "?p : (P-->Q-->R) --> (P-->Q) --> (P-->R)"
+schematic_lemma "?p : (P-->Q-->R) --> (P-->Q) --> (P-->R)"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
(*Converse is classical*)
-lemma "?p : (P-->Q) | (P-->R) --> (P --> Q | R)"
+schematic_lemma "?p : (P-->Q) | (P-->R) --> (P --> Q | R)"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
-lemma "?p : (P-->Q) --> (~Q --> ~P)"
+schematic_lemma "?p : (P-->Q) --> (~Q --> ~P)"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
text "Schwichtenberg's examples (via T. Nipkow)"
-lemma stab_imp: "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
+schematic_lemma stab_imp: "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
-lemma stab_to_peirce: "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)
+schematic_lemma stab_to_peirce: "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)
--> ((P --> Q) --> P) --> P"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
-lemma peirce_imp1: "?p : (((Q --> R) --> Q) --> Q)
+schematic_lemma peirce_imp1: "?p : (((Q --> R) --> Q) --> Q)
--> (((P --> Q) --> R) --> P --> Q) --> P --> Q"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
-lemma peirce_imp2: "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
+schematic_lemma peirce_imp2: "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
-lemma mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q"
+schematic_lemma mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
-lemma mints_solovev: "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
+schematic_lemma mints_solovev: "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
-lemma tatsuta: "?p : (((P7 --> P1) --> P10) --> P4 --> P5)
+schematic_lemma tatsuta: "?p : (((P7 --> P1) --> P10) --> P4 --> P5)
--> (((P8 --> P2) --> P9) --> P3 --> P10)
--> (P1 --> P8) --> P6 --> P7
--> (((P3 --> P2) --> P9) --> P4)
--> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
-lemma tatsuta1: "?p : (((P8 --> P2) --> P9) --> P3 --> P10)
+schematic_lemma tatsuta1: "?p : (((P8 --> P2) --> P9) --> P3 --> P10)
--> (((P3 --> P2) --> P9) --> P4)
--> (((P6 --> P1) --> P2) --> P9)
--> (((P7 --> P1) --> P10) --> P4 --> P5)
--- a/src/FOLP/ex/Propositional_Int.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/FOLP/ex/Propositional_Int.thy Fri Apr 23 23:35:43 2010 +0200
@@ -11,103 +11,103 @@
text "commutative laws of & and | "
-lemma "?p : P & Q --> Q & P"
+schematic_lemma "?p : P & Q --> Q & P"
by (tactic {* IntPr.fast_tac 1 *})
-lemma "?p : P | Q --> Q | P"
+schematic_lemma "?p : P | Q --> Q | P"
by (tactic {* IntPr.fast_tac 1 *})
text "associative laws of & and | "
-lemma "?p : (P & Q) & R --> P & (Q & R)"
+schematic_lemma "?p : (P & Q) & R --> P & (Q & R)"
by (tactic {* IntPr.fast_tac 1 *})
-lemma "?p : (P | Q) | R --> P | (Q | R)"
+schematic_lemma "?p : (P | Q) | R --> P | (Q | R)"
by (tactic {* IntPr.fast_tac 1 *})
text "distributive laws of & and | "
-lemma "?p : (P & Q) | R --> (P | R) & (Q | R)"
+schematic_lemma "?p : (P & Q) | R --> (P | R) & (Q | R)"
by (tactic {* IntPr.fast_tac 1 *})
-lemma "?p : (P | R) & (Q | R) --> (P & Q) | R"
+schematic_lemma "?p : (P | R) & (Q | R) --> (P & Q) | R"
by (tactic {* IntPr.fast_tac 1 *})
-lemma "?p : (P | Q) & R --> (P & R) | (Q & R)"
+schematic_lemma "?p : (P | Q) & R --> (P & R) | (Q & R)"
by (tactic {* IntPr.fast_tac 1 *})
-lemma "?p : (P & R) | (Q & R) --> (P | Q) & R"
+schematic_lemma "?p : (P & R) | (Q & R) --> (P | Q) & R"
by (tactic {* IntPr.fast_tac 1 *})
text "Laws involving implication"
-lemma "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)"
+schematic_lemma "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)"
by (tactic {* IntPr.fast_tac 1 *})
-lemma "?p : (P & Q --> R) <-> (P--> (Q-->R))"
+schematic_lemma "?p : (P & Q --> R) <-> (P--> (Q-->R))"
by (tactic {* IntPr.fast_tac 1 *})
-lemma "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
+schematic_lemma "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
by (tactic {* IntPr.fast_tac 1 *})
-lemma "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
+schematic_lemma "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
by (tactic {* IntPr.fast_tac 1 *})
-lemma "?p : (P --> Q & R) <-> (P-->Q) & (P-->R)"
+schematic_lemma "?p : (P --> Q & R) <-> (P-->Q) & (P-->R)"
by (tactic {* IntPr.fast_tac 1 *})
text "Propositions-as-types"
(*The combinator K*)
-lemma "?p : P --> (Q --> P)"
+schematic_lemma "?p : P --> (Q --> P)"
by (tactic {* IntPr.fast_tac 1 *})
(*The combinator S*)
-lemma "?p : (P-->Q-->R) --> (P-->Q) --> (P-->R)"
+schematic_lemma "?p : (P-->Q-->R) --> (P-->Q) --> (P-->R)"
by (tactic {* IntPr.fast_tac 1 *})
(*Converse is classical*)
-lemma "?p : (P-->Q) | (P-->R) --> (P --> Q | R)"
+schematic_lemma "?p : (P-->Q) | (P-->R) --> (P --> Q | R)"
by (tactic {* IntPr.fast_tac 1 *})
-lemma "?p : (P-->Q) --> (~Q --> ~P)"
+schematic_lemma "?p : (P-->Q) --> (~Q --> ~P)"
by (tactic {* IntPr.fast_tac 1 *})
text "Schwichtenberg's examples (via T. Nipkow)"
-lemma stab_imp: "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
+schematic_lemma stab_imp: "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
by (tactic {* IntPr.fast_tac 1 *})
-lemma stab_to_peirce: "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)
+schematic_lemma stab_to_peirce: "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)
--> ((P --> Q) --> P) --> P"
by (tactic {* IntPr.fast_tac 1 *})
-lemma peirce_imp1: "?p : (((Q --> R) --> Q) --> Q)
+schematic_lemma peirce_imp1: "?p : (((Q --> R) --> Q) --> Q)
--> (((P --> Q) --> R) --> P --> Q) --> P --> Q"
by (tactic {* IntPr.fast_tac 1 *})
-lemma peirce_imp2: "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
+schematic_lemma peirce_imp2: "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
by (tactic {* IntPr.fast_tac 1 *})
-lemma mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q"
+schematic_lemma mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q"
by (tactic {* IntPr.fast_tac 1 *})
-lemma mints_solovev: "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
+schematic_lemma mints_solovev: "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
by (tactic {* IntPr.fast_tac 1 *})
-lemma tatsuta: "?p : (((P7 --> P1) --> P10) --> P4 --> P5)
+schematic_lemma tatsuta: "?p : (((P7 --> P1) --> P10) --> P4 --> P5)
--> (((P8 --> P2) --> P9) --> P3 --> P10)
--> (P1 --> P8) --> P6 --> P7
--> (((P3 --> P2) --> P9) --> P4)
--> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5"
by (tactic {* IntPr.fast_tac 1 *})
-lemma tatsuta1: "?p : (((P8 --> P2) --> P9) --> P3 --> P10)
+schematic_lemma tatsuta1: "?p : (((P8 --> P2) --> P9) --> P3 --> P10)
--> (((P3 --> P2) --> P9) --> P4)
--> (((P6 --> P1) --> P2) --> P9)
--> (((P7 --> P1) --> P10) --> P4 --> P5)
--- a/src/FOLP/ex/Quantifiers_Cla.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/FOLP/ex/Quantifiers_Cla.thy Fri Apr 23 23:35:43 2010 +0200
@@ -10,92 +10,92 @@
imports FOLP
begin
-lemma "?p : (ALL x y. P(x,y)) --> (ALL y x. P(x,y))"
+schematic_lemma "?p : (ALL x y. P(x,y)) --> (ALL y x. P(x,y))"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
-lemma "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))"
+schematic_lemma "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
(*Converse is false*)
-lemma "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
+schematic_lemma "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
-lemma "?p : (ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))"
+schematic_lemma "?p : (ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
-lemma "?p : (ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)"
+schematic_lemma "?p : (ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
text "Some harder ones"
-lemma "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
+schematic_lemma "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
(*Converse is false*)
-lemma "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x)) & (EX x. Q(x))"
+schematic_lemma "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x)) & (EX x. Q(x))"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
text "Basic test of quantifier reasoning"
(*TRUE*)
-lemma "?p : (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"
+schematic_lemma "?p : (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
-lemma "?p : (ALL x. Q(x)) --> (EX x. Q(x))"
+schematic_lemma "?p : (ALL x. Q(x)) --> (EX x. Q(x))"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
text "The following should fail, as they are false!"
-lemma "?p : (ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))"
+schematic_lemma "?p : (ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))"
apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
oops
-lemma "?p : (EX x. Q(x)) --> (ALL x. Q(x))"
+schematic_lemma "?p : (EX x. Q(x)) --> (ALL x. Q(x))"
apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
oops
-lemma "?p : P(?a) --> (ALL x. P(x))"
+schematic_lemma "?p : P(?a) --> (ALL x. P(x))"
apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
oops
-lemma "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
+schematic_lemma "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
oops
text "Back to things that are provable..."
-lemma "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
+schematic_lemma "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
(*An example of why exI should be delayed as long as possible*)
-lemma "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
+schematic_lemma "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
-lemma "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
+schematic_lemma "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
-lemma "?p : (ALL x. Q(x)) --> (EX x. Q(x))"
+schematic_lemma "?p : (ALL x. Q(x)) --> (EX x. Q(x))"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
text "Some slow ones"
(*Principia Mathematica *11.53 *)
-lemma "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
+schematic_lemma "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
(*Principia Mathematica *11.55 *)
-lemma "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
+schematic_lemma "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
(*Principia Mathematica *11.61 *)
-lemma "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
+schematic_lemma "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
by (tactic {* Cla.fast_tac FOLP_cs 1 *})
end
--- a/src/FOLP/ex/Quantifiers_Int.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/FOLP/ex/Quantifiers_Int.thy Fri Apr 23 23:35:43 2010 +0200
@@ -10,92 +10,92 @@
imports IFOLP
begin
-lemma "?p : (ALL x y. P(x,y)) --> (ALL y x. P(x,y))"
+schematic_lemma "?p : (ALL x y. P(x,y)) --> (ALL y x. P(x,y))"
by (tactic {* IntPr.fast_tac 1 *})
-lemma "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))"
+schematic_lemma "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))"
by (tactic {* IntPr.fast_tac 1 *})
(*Converse is false*)
-lemma "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
+schematic_lemma "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
by (tactic {* IntPr.fast_tac 1 *})
-lemma "?p : (ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))"
+schematic_lemma "?p : (ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))"
by (tactic {* IntPr.fast_tac 1 *})
-lemma "?p : (ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)"
+schematic_lemma "?p : (ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)"
by (tactic {* IntPr.fast_tac 1 *})
text "Some harder ones"
-lemma "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
+schematic_lemma "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
by (tactic {* IntPr.fast_tac 1 *})
(*Converse is false*)
-lemma "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x)) & (EX x. Q(x))"
+schematic_lemma "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x)) & (EX x. Q(x))"
by (tactic {* IntPr.fast_tac 1 *})
text "Basic test of quantifier reasoning"
(*TRUE*)
-lemma "?p : (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"
+schematic_lemma "?p : (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"
by (tactic {* IntPr.fast_tac 1 *})
-lemma "?p : (ALL x. Q(x)) --> (EX x. Q(x))"
+schematic_lemma "?p : (ALL x. Q(x)) --> (EX x. Q(x))"
by (tactic {* IntPr.fast_tac 1 *})
text "The following should fail, as they are false!"
-lemma "?p : (ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))"
+schematic_lemma "?p : (ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))"
apply (tactic {* IntPr.fast_tac 1 *})?
oops
-lemma "?p : (EX x. Q(x)) --> (ALL x. Q(x))"
+schematic_lemma "?p : (EX x. Q(x)) --> (ALL x. Q(x))"
apply (tactic {* IntPr.fast_tac 1 *})?
oops
-lemma "?p : P(?a) --> (ALL x. P(x))"
+schematic_lemma "?p : P(?a) --> (ALL x. P(x))"
apply (tactic {* IntPr.fast_tac 1 *})?
oops
-lemma "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
+schematic_lemma "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
apply (tactic {* IntPr.fast_tac 1 *})?
oops
text "Back to things that are provable..."
-lemma "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
+schematic_lemma "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
by (tactic {* IntPr.fast_tac 1 *})
(*An example of why exI should be delayed as long as possible*)
-lemma "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
+schematic_lemma "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
by (tactic {* IntPr.fast_tac 1 *})
-lemma "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
+schematic_lemma "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
by (tactic {* IntPr.fast_tac 1 *})
-lemma "?p : (ALL x. Q(x)) --> (EX x. Q(x))"
+schematic_lemma "?p : (ALL x. Q(x)) --> (EX x. Q(x))"
by (tactic {* IntPr.fast_tac 1 *})
text "Some slow ones"
(*Principia Mathematica *11.53 *)
-lemma "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
+schematic_lemma "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
by (tactic {* IntPr.fast_tac 1 *})
(*Principia Mathematica *11.55 *)
-lemma "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
+schematic_lemma "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
by (tactic {* IntPr.fast_tac 1 *})
(*Principia Mathematica *11.61 *)
-lemma "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
+schematic_lemma "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
by (tactic {* IntPr.fast_tac 1 *})
end
--- a/src/HOL/Bali/Example.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/HOL/Bali/Example.thy Fri Apr 23 23:35:43 2010 +0200
@@ -1070,7 +1070,7 @@
section "well-typedness"
-lemma wt_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
+schematic_lemma wt_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
apply (unfold test_def arr_viewed_from_def)
(* ?pTs = [Class Base] *)
apply (rule wtIs (* ;; *))
@@ -1122,7 +1122,7 @@
section "definite assignment"
-lemma da_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>
+schematic_lemma da_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>
\<turnstile>{} \<guillemotright>\<langle>test ?pTs\<rangle>\<guillemotright> \<lparr>nrm={VName e},brk=\<lambda> l. UNIV\<rparr>"
apply (unfold test_def arr_viewed_from_def)
apply (rule da.Comp)
@@ -1241,7 +1241,7 @@
declare Pair_eq [simp del]
-lemma exec_test:
+schematic_lemma exec_test:
"\<lbrakk>the (new_Addr (heap s1)) = a;
the (new_Addr (heap ?s2)) = b;
the (new_Addr (heap ?s3)) = c\<rbrakk> \<Longrightarrow>
--- a/src/HOL/Lambda/Type.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/HOL/Lambda/Type.thy Fri Apr 23 23:35:43 2010 +0200
@@ -83,10 +83,10 @@
subsection {* Some examples *}
-lemma "e \<turnstile> Abs (Abs (Abs (Var 1 \<degree> (Var 2 \<degree> Var 1 \<degree> Var 0)))) : ?T"
+schematic_lemma "e \<turnstile> Abs (Abs (Abs (Var 1 \<degree> (Var 2 \<degree> Var 1 \<degree> Var 0)))) : ?T"
by force
-lemma "e \<turnstile> Abs (Abs (Abs (Var 2 \<degree> Var 0 \<degree> (Var 1 \<degree> Var 0)))) : ?T"
+schematic_lemma "e \<turnstile> Abs (Abs (Abs (Var 2 \<degree> Var 0 \<degree> (Var 1 \<degree> Var 0)))) : ?T"
by force
--- a/src/HOL/MicroJava/J/Example.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/HOL/MicroJava/J/Example.thy Fri Apr 23 23:35:43 2010 +0200
@@ -371,7 +371,7 @@
done
ML {* val t = resolve_tac @{thms ty_expr_ty_exprs_wt_stmt.intros} 1 *}
-lemma wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile>
+schematic_lemma wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile>
Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\<surd>"
apply (tactic t) -- ";;"
apply (tactic t) -- "Expr"
@@ -400,7 +400,7 @@
declare split_if [split del]
declare init_vars_def [simp] c_hupd_def [simp] cast_ok_def [simp]
-lemma exec_test:
+schematic_lemma exec_test:
" [|new_Addr (heap (snd s0)) = (a, None)|] ==>
tprg\<turnstile>s0 -test-> ?s"
apply (unfold test_def)
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Fri Apr 23 23:35:43 2010 +0200
@@ -325,27 +325,27 @@
subsection {* Schematic Variables *}
-lemma "x = ?x"
+schematic_lemma "x = ?x"
nitpick [expect = none]
by auto
-lemma "\<forall>x. x = ?x"
+schematic_lemma "\<forall>x. x = ?x"
nitpick [expect = genuine]
oops
-lemma "\<exists>x. x = ?x"
+schematic_lemma "\<exists>x. x = ?x"
nitpick [expect = none]
by auto
-lemma "\<exists>x\<Colon>'a \<Rightarrow> 'b. x = ?x"
+schematic_lemma "\<exists>x\<Colon>'a \<Rightarrow> 'b. x = ?x"
nitpick [expect = none]
by auto
-lemma "\<forall>x. ?x = ?y"
+schematic_lemma "\<forall>x. ?x = ?y"
nitpick [expect = none]
by auto
-lemma "\<exists>x. ?x = ?y"
+schematic_lemma "\<exists>x. ?x = ?y"
nitpick [expect = none]
by auto
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Fri Apr 23 23:35:43 2010 +0200
@@ -340,12 +340,12 @@
subsubsection {* Schematic Variables *}
-lemma "?P"
+schematic_lemma "?P"
nitpick [expect = none]
apply auto
done
-lemma "x = ?y"
+schematic_lemma "x = ?y"
nitpick [expect = none]
apply auto
done
--- a/src/HOL/Prolog/Func.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/HOL/Prolog/Func.thy Fri Apr 23 23:35:43 2010 +0200
@@ -58,11 +58,11 @@
lemmas prog_Func = eval
-lemma "eval ((S (S Z)) + (S Z)) ?X"
+schematic_lemma "eval ((S (S Z)) + (S Z)) ?X"
apply (prolog prog_Func)
done
-lemma "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z)
+schematic_lemma "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z)
(n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X"
apply (prolog prog_Func)
done
--- a/src/HOL/Prolog/Test.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/HOL/Prolog/Test.thy Fri Apr 23 23:35:43 2010 +0200
@@ -81,7 +81,7 @@
lemmas prog_Test = append reverse mappred mapfun age eq bag_appl
-lemma "append ?x ?y [a,b,c,d]"
+schematic_lemma "append ?x ?y [a,b,c,d]"
apply (prolog prog_Test)
back
back
@@ -89,56 +89,56 @@
back
done
-lemma "append [a,b] y ?L"
+schematic_lemma "append [a,b] y ?L"
apply (prolog prog_Test)
done
-lemma "!y. append [a,b] y (?L y)"
+schematic_lemma "!y. append [a,b] y (?L y)"
apply (prolog prog_Test)
done
-lemma "reverse [] ?L"
+schematic_lemma "reverse [] ?L"
apply (prolog prog_Test)
done
-lemma "reverse [23] ?L"
+schematic_lemma "reverse [23] ?L"
apply (prolog prog_Test)
done
-lemma "reverse [23,24,?x] ?L"
+schematic_lemma "reverse [23,24,?x] ?L"
apply (prolog prog_Test)
done
-lemma "reverse ?L [23,24,?x]"
+schematic_lemma "reverse ?L [23,24,?x]"
apply (prolog prog_Test)
done
-lemma "mappred age ?x [23,24]"
+schematic_lemma "mappred age ?x [23,24]"
apply (prolog prog_Test)
back
done
-lemma "mappred (%x y. ? z. age z y) ?x [23,24]"
+schematic_lemma "mappred (%x y. ? z. age z y) ?x [23,24]"
apply (prolog prog_Test)
done
-lemma "mappred ?P [bob,sue] [24,23]"
+schematic_lemma "mappred ?P [bob,sue] [24,23]"
apply (prolog prog_Test)
done
-lemma "mapfun f [bob,bob,sue] [?x,?y,?z]"
+schematic_lemma "mapfun f [bob,bob,sue] [?x,?y,?z]"
apply (prolog prog_Test)
done
-lemma "mapfun (%x. h x 25) [bob,sue] ?L"
+schematic_lemma "mapfun (%x. h x 25) [bob,sue] ?L"
apply (prolog prog_Test)
done
-lemma "mapfun ?F [24,25] [h bob 24,h bob 25]"
+schematic_lemma "mapfun ?F [24,25] [h bob 24,h bob 25]"
apply (prolog prog_Test)
done
-lemma "mapfun ?F [24] [h 24 24]"
+schematic_lemma "mapfun ?F [24] [h 24 24]"
apply (prolog prog_Test)
back
back
@@ -149,12 +149,12 @@
apply (prolog prog_Test)
done
-lemma "age ?x 24 & age ?y 23"
+schematic_lemma "age ?x 24 & age ?y 23"
apply (prolog prog_Test)
back
done
-lemma "age ?x 24 | age ?x 23"
+schematic_lemma "age ?x 24 | age ?x 23"
apply (prolog prog_Test)
back
back
@@ -168,7 +168,7 @@
apply (prolog prog_Test)
done
-lemma "age sue 24 .. age bob 23 => age ?x ?y"
+schematic_lemma "age sue 24 .. age bob 23 => age ?x ?y"
apply (prolog prog_Test)
back
back
@@ -182,7 +182,7 @@
done
(*reset trace_DEPTH_FIRST;*)
-lemma "(!x. age x 25 :- age x 23) => age ?x 25 & age ?y 25"
+schematic_lemma "(!x. age x 25 :- age x 23) => age ?x 25 & age ?y 25"
apply (prolog prog_Test)
back
back
@@ -193,7 +193,7 @@
apply (prolog prog_Test)
done
-lemma "? P. P & eq P ?x"
+schematic_lemma "? P. P & eq P ?x"
apply (prolog prog_Test)
(*
back
@@ -248,14 +248,14 @@
by fast
*)
-lemma "!Emp Stk.(
+schematic_lemma "!Emp Stk.(
empty (Emp::'b) ..
(!(X::nat) S. add X (S::'b) (Stk X S)) ..
(!(X::nat) S. remove X ((Stk X S)::'b) S))
=> bag_appl 23 24 ?X ?Y"
oops
-lemma "!Qu. (
+schematic_lemma "!Qu. (
(!L. empty (Qu L L)) ..
(!(X::nat) L K. add X (Qu L (X#K)) (Qu L K)) ..
(!(X::nat) L K. remove X (Qu (X#L) K) (Qu L K)))
@@ -266,7 +266,7 @@
apply (prolog prog_Test)
done
-lemma "P x .. P y => P ?X"
+schematic_lemma "P x .. P y => P ?X"
apply (prolog prog_Test)
back
done
--- a/src/HOL/Prolog/Type.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/HOL/Prolog/Type.thy Fri Apr 23 23:35:43 2010 +0200
@@ -47,41 +47,41 @@
lemmas prog_Type = prog_Func good_typeof common_typeof
-lemma "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T"
+schematic_lemma "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T"
apply (prolog prog_Type)
done
-lemma "typeof (fix (%x. x)) ?T"
+schematic_lemma "typeof (fix (%x. x)) ?T"
apply (prolog prog_Type)
done
-lemma "typeof (fix (%fact. abs(%n. (app fact (n - Z))))) ?T"
+schematic_lemma "typeof (fix (%fact. abs(%n. (app fact (n - Z))))) ?T"
apply (prolog prog_Type)
done
-lemma "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z)
+schematic_lemma "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z)
(n * (app fact (n - (S Z))))))) ?T"
apply (prolog prog_Type)
done
-lemma "typeof (abs(%v. Z)) ?T" (*correct only solution (?A1 -> nat) *)
+schematic_lemma "typeof (abs(%v. Z)) ?T" (*correct only solution (?A1 -> nat) *)
apply (prolog prog_Type)
done
-lemma "typeof (abs(%v. Z)) ?T"
+schematic_lemma "typeof (abs(%v. Z)) ?T"
apply (prolog bad1_typeof common_typeof) (* 1st result ok*)
done
-lemma "typeof (abs(%v. Z)) ?T"
+schematic_lemma "typeof (abs(%v. Z)) ?T"
apply (prolog bad1_typeof common_typeof)
back (* 2nd result (?A1 -> ?A1) wrong *)
done
-lemma "typeof (abs(%v. abs(%v. app v v))) ?T"
+schematic_lemma "typeof (abs(%v. abs(%v. app v v))) ?T"
apply (prolog prog_Type)? (*correctly fails*)
oops
-lemma "typeof (abs(%v. abs(%v. app v v))) ?T"
+schematic_lemma "typeof (abs(%v. abs(%v. app v v))) ?T"
apply (prolog bad2_typeof common_typeof) (* wrong result ((?A3 -> ?B3) -> ?A3 -> ?B3)*)
done
--- a/src/HOL/ex/Classical.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/HOL/ex/Classical.thy Fri Apr 23 23:35:43 2010 +0200
@@ -348,7 +348,7 @@
text{*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
fast DISCOVERS who killed Agatha. *}
-lemma "lives(agatha) & lives(butler) & lives(charles) &
+schematic_lemma "lives(agatha) & lives(butler) & lives(charles) &
(killed agatha agatha | killed butler agatha | killed charles agatha) &
(\<forall>x y. killed x y --> hates x y & ~richer x y) &
(\<forall>x. hates agatha x --> ~hates charles x) &
--- a/src/HOL/ex/Groebner_Examples.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/HOL/ex/Groebner_Examples.thy Fri Apr 23 23:35:43 2010 +0200
@@ -10,13 +10,13 @@
subsection {* Basic examples *}
-lemma "3 ^ 3 == (?X::'a::{number_ring})"
+schematic_lemma "3 ^ 3 == (?X::'a::{number_ring})"
by sring_norm
-lemma "(x - (-2))^5 == ?X::int"
+schematic_lemma "(x - (-2))^5 == ?X::int"
by sring_norm
-lemma "(x - (-2))^5 * (y - 78) ^ 8 == ?X::int"
+schematic_lemma "(x - (-2))^5 * (y - 78) ^ 8 == ?X::int"
by sring_norm
lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring})"
--- a/src/HOL/ex/Refute_Examples.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/HOL/ex/Refute_Examples.thy Fri Apr 23 23:35:43 2010 +0200
@@ -347,12 +347,12 @@
subsubsection {* Schematic variables *}
-lemma "?P"
+schematic_lemma "?P"
refute
apply auto
done
-lemma "x = ?y"
+schematic_lemma "x = ?y"
refute
apply auto
done
--- a/src/HOL/ex/set.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/HOL/ex/set.thy Fri Apr 23 23:35:43 2010 +0200
@@ -26,7 +26,7 @@
Trivial example of term synthesis: apparently hard for some provers!
*}
-lemma "a \<noteq> b \<Longrightarrow> a \<in> ?X \<and> b \<notin> ?X"
+schematic_lemma "a \<noteq> b \<Longrightarrow> a \<in> ?X \<and> b \<notin> ?X"
by blast
@@ -60,15 +60,15 @@
-- {* Requires best-first search because it is undirectional. *}
by best
-lemma "\<forall>f:: 'a \<Rightarrow> 'a set. \<forall>x. f x \<noteq> ?S f"
+schematic_lemma "\<forall>f:: 'a \<Rightarrow> 'a set. \<forall>x. f x \<noteq> ?S f"
-- {*This form displays the diagonal term. *}
by best
-lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
+schematic_lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
-- {* This form exploits the set constructs. *}
by (rule notI, erule rangeE, best)
-lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
+schematic_lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
-- {* Or just this! *}
by best
--- a/src/Sequents/LK/Quantifiers.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/Sequents/LK/Quantifiers.thy Fri Apr 23 23:35:43 2010 +0200
@@ -90,13 +90,13 @@
oops
(*INVALID*)
-lemma "|- P(?a) --> (ALL x. P(x))"
+schematic_lemma "|- P(?a) --> (ALL x. P(x))"
apply fast?
apply (rule _)
oops
(*INVALID*)
-lemma "|- (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
+schematic_lemma "|- (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
apply fast?
apply (rule _)
oops
@@ -114,7 +114,7 @@
text "Solving for a Var"
-lemma "|- (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
+schematic_lemma "|- (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
by fast
--- a/src/ZF/AC/Cardinal_aux.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/ZF/AC/Cardinal_aux.thy Fri Apr 23 23:35:43 2010 +0200
@@ -71,7 +71,7 @@
apply (rule Un_upper1 [THEN subset_imp_lepoll])
done
-lemma paired_bij: "?f \<in> bij({{y,z}. y \<in> x}, x)"
+schematic_lemma paired_bij: "?f \<in> bij({{y,z}. y \<in> x}, x)"
apply (rule RepFun_bijective)
apply (simp add: doubleton_eq_iff, blast)
done
--- a/src/ZF/Constructible/Reflection.thy Fri Apr 23 23:33:48 2010 +0200
+++ b/src/ZF/Constructible/Reflection.thy Fri Apr 23 23:35:43 2010 +0200
@@ -268,7 +268,7 @@
text{*Example 1: reflecting a simple formula. The reflecting class is first
given as the variable @{text ?Cl} and later retrieved from the final
proof state.*}
-lemma (in reflection)
+schematic_lemma (in reflection)
"Reflects(?Cl,
\<lambda>x. \<exists>y. M(y) & x \<in> y,
\<lambda>a x. \<exists>y\<in>Mset(a). x \<in> y)"
@@ -285,7 +285,7 @@
text{*Example 2*}
-lemma (in reflection)
+schematic_lemma (in reflection)
"Reflects(?Cl,
\<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y),
\<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x --> z \<in> y)"
@@ -302,14 +302,14 @@
by fast
text{*Example 2''. We expand the subset relation.*}
-lemma (in reflection)
+schematic_lemma (in reflection)
"Reflects(?Cl,
\<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) --> (\<forall>w. M(w) --> w\<in>z --> w\<in>x) --> z\<in>y),
\<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)"
by fast
text{*Example 2'''. Single-step version, to reveal the reflecting class.*}
-lemma (in reflection)
+schematic_lemma (in reflection)
"Reflects(?Cl,
\<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y),
\<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x --> z \<in> y)"
@@ -329,21 +329,21 @@
text{*Example 3. Warning: the following examples make sense only
if @{term P} is quantifier-free, since it is not being relativized.*}
-lemma (in reflection)
+schematic_lemma (in reflection)
"Reflects(?Cl,
\<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) --> z \<in> y <-> z \<in> x & P(z)),
\<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<in> y <-> z \<in> x & P(z))"
by fast
text{*Example 3'*}
-lemma (in reflection)
+schematic_lemma (in reflection)
"Reflects(?Cl,
\<lambda>x. \<exists>y. M(y) & y = Collect(x,P),
\<lambda>a x. \<exists>y\<in>Mset(a). y = Collect(x,P))";
by fast
text{*Example 3''*}
-lemma (in reflection)
+schematic_lemma (in reflection)
"Reflects(?Cl,
\<lambda>x. \<exists>y. M(y) & y = Replace(x,P),
\<lambda>a x. \<exists>y\<in>Mset(a). y = Replace(x,P))";
@@ -351,7 +351,7 @@
text{*Example 4: Axiom of Choice. Possibly wrong, since @{text \<Pi>} needs
to be relativized.*}
-lemma (in reflection)
+schematic_lemma (in reflection)
"Reflects(?Cl,
\<lambda>A. 0\<notin>A --> (\<exists>f. M(f) & f \<in> (\<Pi> X \<in> A. X)),
\<lambda>a A. 0\<notin>A --> (\<exists>f\<in>Mset(a). f \<in> (\<Pi> X \<in> A. X)))"