# HG changeset patch # User wenzelm # Date 1272058543 -7200 # Node ID 8feb2c4bef1a060ab08a6dbf432e9189d0411ada # Parent 3567d0571932ec816fb97cacbc2fd7b9b9b1280d mark schematic statements explicitly; diff -r 3567d0571932 -r 8feb2c4bef1a src/CCL/Fix.thy --- 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 diff -r 3567d0571932 -r 8feb2c4bef1a src/CCL/Wfd.thy --- 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()))) in f() ---> ?a" by eval -lemma +schematic_lemma "letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f()))) in f() ---> ?a" by eval -lemma +schematic_lemma "letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f()))) in f() ---> ?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 diff -r 3567d0571932 -r 8feb2c4bef1a src/CTT/Arith.thy --- 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) diff -r 3567d0571932 -r 8feb2c4bef1a src/CTT/ex/Elimination.thy --- 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. >) ` w) *) -lemma +schematic_lemma assumes "A type" and "B type" and "!!z. z:A*B ==> C(z) type" diff -r 3567d0571932 -r 8feb2c4bef1a src/CTT/ex/Synthesis.thy --- 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)" 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)), )" 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)), )" 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) * Eq(?A, ?b(inr()), 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) +schematic_lemma "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl()), i) * Eq(?A(i,j), ?b(inr()), 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) +schematic_lemma "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl()), i) * Eq(N, ?b(inr()), 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)))" diff -r 3567d0571932 -r 8feb2c4bef1a src/CTT/ex/Typechecking.thy --- 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. : ?A" +schematic_lemma "lam 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 diff -r 3567d0571932 -r 8feb2c4bef1a src/Cube/Example.thy --- 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) diff -r 3567d0571932 -r 8feb2c4bef1a src/FOL/ex/Classical.thy --- 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)) & (\x y. killed(x,y) --> hates(x,y) & ~richer(x,y)) & (\x. hates(agatha,x) --> ~hates(charles,x)) & diff -r 3567d0571932 -r 8feb2c4bef1a src/FOL/ex/Prolog.thy --- 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 diff -r 3567d0571932 -r 8feb2c4bef1a src/FOL/ex/Quantifiers_Cla.thy --- 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))" diff -r 3567d0571932 -r 8feb2c4bef1a src/FOL/ex/Quantifiers_Int.thy --- 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))" diff -r 3567d0571932 -r 8feb2c4bef1a src/FOLP/FOLP.thy --- 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" diff -r 3567d0571932 -r 8feb2c4bef1a src/FOLP/IFOLP.thy --- 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 \ q:P \ ?p:R" +schematic_lemma notE: "p:~P \ q:P \ ?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 diff -r 3567d0571932 -r 8feb2c4bef1a src/FOLP/ex/Classical.thy --- 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 diff -r 3567d0571932 -r 8feb2c4bef1a src/FOLP/ex/Foundation.thy --- 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) diff -r 3567d0571932 -r 8feb2c4bef1a src/FOLP/ex/If.thy --- 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 diff -r 3567d0571932 -r 8feb2c4bef1a src/FOLP/ex/Intro.thy --- 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" diff -r 3567d0571932 -r 8feb2c4bef1a src/FOLP/ex/Intuitionistic.thy --- 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 diff -r 3567d0571932 -r 8feb2c4bef1a src/FOLP/ex/Nat.thy --- 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 \ ?p : Suc(x) = Suc(y)" +schematic_lemma Suc_cong: "p : x = y \ ?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 diff -r 3567d0571932 -r 8feb2c4bef1a src/FOLP/ex/Propositional_Cla.thy --- 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) diff -r 3567d0571932 -r 8feb2c4bef1a src/FOLP/ex/Propositional_Int.thy --- 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) diff -r 3567d0571932 -r 8feb2c4bef1a src/FOLP/ex/Quantifiers_Cla.thy --- 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 diff -r 3567d0571932 -r 8feb2c4bef1a src/FOLP/ex/Quantifiers_Int.thy --- 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 diff -r 3567d0571932 -r 8feb2c4bef1a src/HOL/Bali/Example.thy --- 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: "\prg=tprg,cls=Main,lcl=empty(VName e\Class Base)\\test ?pTs\\" +schematic_lemma wt_test: "\prg=tprg,cls=Main,lcl=empty(VName e\Class Base)\\test ?pTs\\" apply (unfold test_def arr_viewed_from_def) (* ?pTs = [Class Base] *) apply (rule wtIs (* ;; *)) @@ -1122,7 +1122,7 @@ section "definite assignment" -lemma da_test: "\prg=tprg,cls=Main,lcl=empty(VName e\Class Base)\ +schematic_lemma da_test: "\prg=tprg,cls=Main,lcl=empty(VName e\Class Base)\ \{} \\test ?pTs\\ \nrm={VName e},brk=\ l. UNIV\" 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: "\the (new_Addr (heap s1)) = a; the (new_Addr (heap ?s2)) = b; the (new_Addr (heap ?s3)) = c\ \ diff -r 3567d0571932 -r 8feb2c4bef1a src/HOL/Lambda/Type.thy --- 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 \ Abs (Abs (Abs (Var 1 \ (Var 2 \ Var 1 \ Var 0)))) : ?T" +schematic_lemma "e \ Abs (Abs (Abs (Var 1 \ (Var 2 \ Var 1 \ Var 0)))) : ?T" by force -lemma "e \ Abs (Abs (Abs (Var 2 \ Var 0 \ (Var 1 \ Var 0)))) : ?T" +schematic_lemma "e \ Abs (Abs (Abs (Var 2 \ Var 0 \ (Var 1 \ Var 0)))) : ?T" by force diff -r 3567d0571932 -r 8feb2c4bef1a src/HOL/MicroJava/J/Example.thy --- 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\Class Base))\ +schematic_lemma wt_test: "(tprg, empty(e\Class Base))\ Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\" 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\s0 -test-> ?s" apply (unfold test_def) diff -r 3567d0571932 -r 8feb2c4bef1a src/HOL/Nitpick_Examples/Core_Nits.thy --- 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 "\x. x = ?x" +schematic_lemma "\x. x = ?x" nitpick [expect = genuine] oops -lemma "\x. x = ?x" +schematic_lemma "\x. x = ?x" nitpick [expect = none] by auto -lemma "\x\'a \ 'b. x = ?x" +schematic_lemma "\x\'a \ 'b. x = ?x" nitpick [expect = none] by auto -lemma "\x. ?x = ?y" +schematic_lemma "\x. ?x = ?y" nitpick [expect = none] by auto -lemma "\x. ?x = ?y" +schematic_lemma "\x. ?x = ?y" nitpick [expect = none] by auto diff -r 3567d0571932 -r 8feb2c4bef1a src/HOL/Nitpick_Examples/Refute_Nits.thy --- 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 diff -r 3567d0571932 -r 8feb2c4bef1a src/HOL/Prolog/Func.thy --- 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 diff -r 3567d0571932 -r 8feb2c4bef1a src/HOL/Prolog/Test.thy --- 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 diff -r 3567d0571932 -r 8feb2c4bef1a src/HOL/Prolog/Type.thy --- 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 diff -r 3567d0571932 -r 8feb2c4bef1a src/HOL/ex/Classical.thy --- 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) & (\x y. killed x y --> hates x y & ~richer x y) & (\x. hates agatha x --> ~hates charles x) & diff -r 3567d0571932 -r 8feb2c4bef1a src/HOL/ex/Groebner_Examples.thy --- 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})" diff -r 3567d0571932 -r 8feb2c4bef1a src/HOL/ex/Refute_Examples.thy --- 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 diff -r 3567d0571932 -r 8feb2c4bef1a src/HOL/ex/set.thy --- 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 \ b \ a \ ?X \ b \ ?X" +schematic_lemma "a \ b \ a \ ?X \ b \ ?X" by blast @@ -60,15 +60,15 @@ -- {* Requires best-first search because it is undirectional. *} by best -lemma "\f:: 'a \ 'a set. \x. f x \ ?S f" +schematic_lemma "\f:: 'a \ 'a set. \x. f x \ ?S f" -- {*This form displays the diagonal term. *} by best -lemma "?S \ range (f :: 'a \ 'a set)" +schematic_lemma "?S \ range (f :: 'a \ 'a set)" -- {* This form exploits the set constructs. *} by (rule notI, erule rangeE, best) -lemma "?S \ range (f :: 'a \ 'a set)" +schematic_lemma "?S \ range (f :: 'a \ 'a set)" -- {* Or just this! *} by best diff -r 3567d0571932 -r 8feb2c4bef1a src/Sequents/LK/Quantifiers.thy --- 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 diff -r 3567d0571932 -r 8feb2c4bef1a src/ZF/AC/Cardinal_aux.thy --- 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 \ bij({{y,z}. y \ x}, x)" +schematic_lemma paired_bij: "?f \ bij({{y,z}. y \ x}, x)" apply (rule RepFun_bijective) apply (simp add: doubleton_eq_iff, blast) done diff -r 3567d0571932 -r 8feb2c4bef1a src/ZF/Constructible/Reflection.thy --- 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, \x. \y. M(y) & x \ y, \a x. \y\Mset(a). x \ y)" @@ -285,7 +285,7 @@ text{*Example 2*} -lemma (in reflection) +schematic_lemma (in reflection) "Reflects(?Cl, \x. \y. M(y) & (\z. M(z) --> z \ x --> z \ y), \a x. \y\Mset(a). \z\Mset(a). z \ x --> z \ y)" @@ -302,14 +302,14 @@ by fast text{*Example 2''. We expand the subset relation.*} -lemma (in reflection) +schematic_lemma (in reflection) "Reflects(?Cl, \x. \y. M(y) & (\z. M(z) --> (\w. M(w) --> w\z --> w\x) --> z\y), \a x. \y\Mset(a). \z\Mset(a). (\w\Mset(a). w\z --> w\x) --> z\y)" by fast text{*Example 2'''. Single-step version, to reveal the reflecting class.*} -lemma (in reflection) +schematic_lemma (in reflection) "Reflects(?Cl, \x. \y. M(y) & (\z. M(z) --> z \ x --> z \ y), \a x. \y\Mset(a). \z\Mset(a). z \ x --> z \ 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, \x. \y. M(y) & (\z. M(z) --> z \ y <-> z \ x & P(z)), \a x. \y\Mset(a). \z\Mset(a). z \ y <-> z \ x & P(z))" by fast text{*Example 3'*} -lemma (in reflection) +schematic_lemma (in reflection) "Reflects(?Cl, \x. \y. M(y) & y = Collect(x,P), \a x. \y\Mset(a). y = Collect(x,P))"; by fast text{*Example 3''*} -lemma (in reflection) +schematic_lemma (in reflection) "Reflects(?Cl, \x. \y. M(y) & y = Replace(x,P), \a x. \y\Mset(a). y = Replace(x,P))"; @@ -351,7 +351,7 @@ text{*Example 4: Axiom of Choice. Possibly wrong, since @{text \} needs to be relativized.*} -lemma (in reflection) +schematic_lemma (in reflection) "Reflects(?Cl, \A. 0\A --> (\f. M(f) & f \ (\ X \ A. X)), \a A. 0\A --> (\f\Mset(a). f \ (\ X \ A. X)))"