# HG changeset patch # User wenzelm # Date 1444137268 -7200 # Node ID 4645502c3c64bbf96a17ea3af2ba5b53e95d4801 # Parent fa4ebbd350ae0a10177b2eff2d117e5e0b1d62bc fewer aliases for toplevel theorem statements; diff -r fa4ebbd350ae -r 4645502c3c64 NEWS --- a/NEWS Tue Oct 06 13:31:44 2015 +0200 +++ b/NEWS Tue Oct 06 15:14:28 2015 +0200 @@ -7,6 +7,19 @@ New in this Isabelle version ---------------------------- +*** General *** + +* Toplevel theorem statements have been simplified as follows: + + theorems ~> lemmas + schematic_lemma ~> schematic_goal + schematic_theorem ~> schematic_goal + schematic_corollary ~> schematic_goal + +Command-line tool "isabelle update_theorems" updates theory sources +accordingly. + + *** Prover IDE -- Isabelle/Scala/jEdit *** * Improved scheduling for urgent print tasks (e.g. command state output, diff -r fa4ebbd350ae -r 4645502c3c64 lib/Tools/update_theorems --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/Tools/update_theorems Tue Oct 06 15:14:28 2015 +0200 @@ -0,0 +1,40 @@ +#!/usr/bin/env bash +# +# Author: Makarius +# +# DESCRIPTION: update toplevel theorem keywords + + +## diagnostics + +PRG="$(basename "$0")" + +function usage() +{ + echo + echo "Usage: isabelle $PRG [FILES|DIRS...]" + echo + echo " Recursively find .thy files and update toplevel theorem keywords:" + echo + echo " theorems ~> lemmas" + echo " schematic_theorem ~> schematic_goal" + echo " schematic_lemma ~> schematic_goal" + echo " schematic_corollary ~> schematic_goal" + echo + echo " Old versions of files are preserved by appending \"~~\"." + echo + exit 1 +} + + +## process command line + +[ "$#" -eq 0 -o "$1" = "-?" ] && usage + +SPECS="$@"; shift "$#" + + +## main + +find $SPECS -name \*.thy -print0 | \ + xargs -0 "$ISABELLE_TOOL" java isabelle.Update_Theorems diff -r fa4ebbd350ae -r 4645502c3c64 src/CCL/Fix.thy --- a/src/CCL/Fix.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/CCL/Fix.thy Tue Oct 06 15:14:28 2015 +0200 @@ -93,7 +93,7 @@ (* All fixed points are lam-expressions *) -schematic_lemma idgenfp_lam: "idgen(d) = d \ d = lam x. ?f(x)" +schematic_goal idgenfp_lam: "idgen(d) = d \ d = lam x. ?f(x)" apply (unfold idgen_def) apply (erule ssubst) apply (rule refl) @@ -125,7 +125,7 @@ apply simp done -schematic_lemma po_eta_lemma: "idgen(d) = d \ d = lam x. ?f(x)" +schematic_goal po_eta_lemma: "idgen(d) = d \ d = lam x. ?f(x)" apply (unfold idgen_def) apply (erule sym) done diff -r fa4ebbd350ae -r 4645502c3c64 src/CCL/Wfd.thy --- a/src/CCL/Wfd.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/CCL/Wfd.thy Tue Oct 06 15:14:28 2015 +0200 @@ -568,29 +568,29 @@ subsection \Factorial\ -schematic_lemma +schematic_goal "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 -schematic_lemma +schematic_goal "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\ -schematic_lemma +schematic_goal "letrec f p be split(p,\m n. ncase(m,true,\x. ncase(n,false,\y. f()))) in f() ---> ?a" by eval -schematic_lemma +schematic_goal "letrec f p be split(p,\m n. ncase(m,true,\x. ncase(n,false,\y. f()))) in f() ---> ?a" by eval -schematic_lemma +schematic_goal "letrec f p be split(p,\m n. ncase(m,true,\x. ncase(n,false,\y. f()))) in f() ---> ?a" by eval @@ -598,12 +598,12 @@ subsection \Reverse\ -schematic_lemma +schematic_goal "letrec id l be lcase(l,[],\x xs. x$id(xs)) in id(zero$succ(zero)$[]) ---> ?a" by eval -schematic_lemma +schematic_goal "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 fa4ebbd350ae -r 4645502c3c64 src/CTT/Arith.thy --- a/src/CTT/Arith.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/CTT/Arith.thy Tue Oct 06 15:14:28 2015 +0200 @@ -266,7 +266,7 @@ (*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.*) -schematic_lemma add_diff_inverse_lemma: +schematic_goal add_diff_inverse_lemma: "b:N \ ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)" apply (NE b) (*strip one "universal quantifier" but not the "implication"*) @@ -337,7 +337,7 @@ done (*If a+b=0 then a=0. Surprisingly tedious*) -schematic_lemma add_eq0_lemma: "\a:N; b:N\ \ ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)" +schematic_goal add_eq0_lemma: "\a:N; b:N\ \ ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)" apply (NE a) apply (rule_tac [3] replace_type) apply arith_rew @@ -357,7 +357,7 @@ done (*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *) -schematic_lemma absdiff_eq0_lem: +schematic_goal 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) apply intr diff -r fa4ebbd350ae -r 4645502c3c64 src/CTT/ex/Elimination.thy --- a/src/CTT/ex/Elimination.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/CTT/ex/Elimination.thy Tue Oct 06 15:14:28 2015 +0200 @@ -14,41 +14,41 @@ text "This finds the functions fst and snd!" -schematic_lemma [folded basic_defs]: "A type \ ?a : (A*A) --> A" +schematic_goal [folded basic_defs]: "A type \ ?a : (A*A) --> A" apply pc done -schematic_lemma [folded basic_defs]: "A type \ ?a : (A*A) --> A" +schematic_goal [folded basic_defs]: "A type \ ?a : (A*A) --> A" apply pc back done text "Double negation of the Excluded Middle" -schematic_lemma "A type \ ?a : ((A + (A-->F)) --> F) --> F" +schematic_goal "A type \ ?a : ((A + (A-->F)) --> F) --> F" apply intr apply (rule ProdE) apply assumption apply pc done -schematic_lemma "\A type; B type\ \ ?a : (A*B) \ (B*A)" +schematic_goal "\A type; B type\ \ ?a : (A*B) \ (B*A)" apply pc done (*The sequent version (ITT) could produce an interesting alternative by backtracking. No longer.*) text "Binary sums and products" -schematic_lemma "\A type; B type; C type\ \ ?a : (A+B --> C) --> (A-->C) * (B-->C)" +schematic_goal "\A type; B type; C type\ \ ?a : (A+B --> C) --> (A-->C) * (B-->C)" apply pc done (*A distributive law*) -schematic_lemma "\A type; B type; C type\ \ ?a : A * (B+C) --> (A*B + A*C)" +schematic_goal "\A type; B type; C type\ \ ?a : A * (B+C) --> (A*B + A*C)" apply pc done (*more general version, same proof*) -schematic_lemma +schematic_goal 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" -schematic_lemma "\A type; B type; C type\ \ ?a : (A*B --> C) --> (A--> (B-->C))" +schematic_goal "\A type; B type; C type\ \ ?a : (A*B --> C) --> (A--> (B-->C))" apply pc done (*more general goal with same proof*) -schematic_lemma +schematic_goal 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)" -schematic_lemma "\A type; B type; C type\ \ ?a : (A --> (B-->C)) --> (A*B --> C)" +schematic_goal "\A type; B type; C type\ \ ?a : (A --> (B-->C)) --> (A*B --> C)" apply pc done (*more general goal with same proof*) -schematic_lemma +schematic_goal 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" -schematic_lemma "\A type; B type\ \ ?a : ((A --> B) * A) --> B" +schematic_goal "\A type; B type\ \ ?a : ((A --> B) * A) --> B" apply pc done text "Basic test of quantifier reasoning" -schematic_lemma +schematic_goal 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" -schematic_lemma +schematic_goal 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" -schematic_lemma +schematic_goal assumes "A type" and "B type" and "\z. z: A+B \ C(z) type" @@ -123,7 +123,7 @@ done (*towards AXIOM OF CHOICE*) -schematic_lemma [folded basic_defs]: +schematic_goal [folded basic_defs]: "\A type; B type; C type\ \ ?a : (A --> B*C) --> (A-->B) * (A-->C)" apply pc done @@ -131,7 +131,7 @@ (*Martin-Lof (1984) page 50*) text "AXIOM OF CHOICE! Delicate use of elimination rules" -schematic_lemma +schematic_goal 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!" -schematic_lemma [folded basic_defs]: +schematic_goal [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" @@ -176,7 +176,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) *) -schematic_lemma +schematic_goal assumes "A type" and "B type" and "\z. z:A*B \ C(z) type" diff -r fa4ebbd350ae -r 4645502c3c64 src/CTT/ex/Synthesis.thy --- a/src/CTT/ex/Synthesis.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/CTT/ex/Synthesis.thy Tue Oct 06 15:14:28 2015 +0200 @@ -10,7 +10,7 @@ begin text "discovery of predecessor function" -schematic_lemma "?a : SUM pred:?A . Eq(N, pred`0, 0) +schematic_goal "?a : SUM pred:?A . Eq(N, pred`0, 0) * (PROD n:N. Eq(N, pred ` succ(n), n))" apply intr apply eqintr @@ -20,7 +20,7 @@ done text "the function fst as an element of a function type" -schematic_lemma [folded basic_defs]: +schematic_goal [folded basic_defs]: "A type \ ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` , i)" apply intr apply eqintr @@ -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.*) -schematic_lemma "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0 , i>) +schematic_goal "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0 , i>) * Eq(?A, ?b(inr(i)), )" apply intr apply eqintr @@ -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.*) -schematic_lemma "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0 , i>) +schematic_goal "?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*) -schematic_lemma [folded basic_defs]: +schematic_goal [folded basic_defs]: "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl()), i) * Eq(?A, ?b(inr()), j)" apply intr @@ -65,18 +65,18 @@ done (*similar but allows the type to depend on i and j*) -schematic_lemma "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl()), i) +schematic_goal "?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*) -schematic_lemma "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl()), i) +schematic_goal "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl()), i) * Eq(N, ?b(inr()), j)" oops text "Deriving the addition operator" -schematic_lemma [folded arith_defs]: +schematic_goal [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 intr @@ -86,7 +86,7 @@ done text "The addition function -- using explicit lambdas" -schematic_lemma [folded arith_defs]: +schematic_goal [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 fa4ebbd350ae -r 4645502c3c64 src/CTT/ex/Typechecking.thy --- a/src/CTT/ex/Typechecking.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/CTT/ex/Typechecking.thy Tue Oct 06 15:14:28 2015 +0200 @@ -11,18 +11,18 @@ subsection \Single-step proofs: verifying that a type is well-formed\ -schematic_lemma "?A type" +schematic_goal "?A type" apply (rule form_rls) done -schematic_lemma "?A type" +schematic_goal "?A type" apply (rule form_rls) back apply (rule form_rls) apply (rule form_rls) done -schematic_lemma "PROD z:?A . N + ?B(z) type" +schematic_goal "PROD z:?A . N + ?B(z) type" apply (rule form_rls) apply (rule form_rls) apply (rule form_rls) @@ -37,30 +37,30 @@ apply form done -schematic_lemma "<0, succ(0)> : ?A" +schematic_goal "<0, succ(0)> : ?A" apply intr done -schematic_lemma "PROD w:N . Eq(?A,w,w) type" +schematic_goal "PROD w:N . Eq(?A,w,w) type" apply typechk done -schematic_lemma "PROD x:N . PROD y:N . Eq(?A,x,y) type" +schematic_goal "PROD x:N . PROD y:N . Eq(?A,x,y) type" apply typechk done text "typechecking an application of fst" -schematic_lemma "(lam u. split(u, \v w. v)) ` <0, succ(0)> : ?A" +schematic_goal "(lam u. split(u, \v w. v)) ` <0, succ(0)> : ?A" apply typechk done text "typechecking the predecessor function" -schematic_lemma "lam n. rec(n, 0, \x y. x) : ?A" +schematic_goal "lam n. rec(n, 0, \x y. x) : ?A" apply typechk done text "typechecking the addition function" -schematic_lemma "lam n. lam m. rec(n, m, \x y. succ(y)) : ?A" +schematic_goal "lam n. lam m. rec(n, m, \x y. succ(y)) : ?A" apply typechk done @@ -69,18 +69,18 @@ method_setup N = \Scan.succeed (fn ctxt => SIMPLE_METHOD (TRYALL (resolve_tac ctxt @{thms NF})))\ -schematic_lemma "lam w. : ?A" +schematic_goal "lam w. : ?A" apply typechk apply N done -schematic_lemma "lam x. lam y. x : ?A" +schematic_goal "lam x. lam y. x : ?A" apply typechk apply N done text "typechecking fst (as a function object)" -schematic_lemma "lam i. split(i, \j k. j) : ?A" +schematic_goal "lam i. split(i, \j k. j) : ?A" apply typechk apply N done diff -r fa4ebbd350ae -r 4645502c3c64 src/Cube/Example.thy --- a/src/Cube/Example.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/Cube/Example.thy Tue Oct 06 15:14:28 2015 +0200 @@ -25,98 +25,98 @@ subsection \Simple types\ -schematic_lemma "A:* \ A\A : ?T" +schematic_goal "A:* \ A\A : ?T" by (depth_solve rules) -schematic_lemma "A:* \ \ a:A. a : ?T" +schematic_goal "A:* \ \ a:A. a : ?T" by (depth_solve rules) -schematic_lemma "A:* B:* b:B \ \ x:A. b : ?T" +schematic_goal "A:* B:* b:B \ \ x:A. b : ?T" by (depth_solve rules) -schematic_lemma "A:* b:A \ (\ a:A. a)^b: ?T" +schematic_goal "A:* b:A \ (\ a:A. a)^b: ?T" by (depth_solve rules) -schematic_lemma "A:* B:* c:A b:B \ (\ x:A. b)^ c: ?T" +schematic_goal "A:* B:* c:A b:B \ (\ x:A. b)^ c: ?T" by (depth_solve rules) -schematic_lemma "A:* B:* \ \ a:A. \ b:B. a : ?T" +schematic_goal "A:* B:* \ \ a:A. \ b:B. a : ?T" by (depth_solve rules) subsection \Second-order types\ -schematic_lemma (in L2) "\ \ A:*. \ a:A. a : ?T" +schematic_goal (in L2) "\ \ A:*. \ a:A. a : ?T" by (depth_solve rules) -schematic_lemma (in L2) "A:* \ (\ B:*.\ b:B. b)^A : ?T" +schematic_goal (in L2) "A:* \ (\ B:*.\ b:B. b)^A : ?T" by (depth_solve rules) -schematic_lemma (in L2) "A:* b:A \ (\ B:*.\ b:B. b) ^ A ^ b: ?T" +schematic_goal (in L2) "A:* b:A \ (\ B:*.\ b:B. b) ^ A ^ b: ?T" by (depth_solve rules) -schematic_lemma (in L2) "\ \ B:*.\ a:(\ A:*.A).a ^ ((\ A:*.A)\B) ^ a: ?T" +schematic_goal (in L2) "\ \ B:*.\ a:(\ A:*.A).a ^ ((\ A:*.A)\B) ^ a: ?T" by (depth_solve rules) subsection \Weakly higher-order propositional logic\ -schematic_lemma (in Lomega) "\ \ A:*.A\A : ?T" +schematic_goal (in Lomega) "\ \ A:*.A\A : ?T" by (depth_solve rules) -schematic_lemma (in Lomega) "B:* \ (\ A:*.A\A) ^ B : ?T" +schematic_goal (in Lomega) "B:* \ (\ A:*.A\A) ^ B : ?T" by (depth_solve rules) -schematic_lemma (in Lomega) "B:* b:B \ (\ y:B. b): ?T" +schematic_goal (in Lomega) "B:* b:B \ (\ y:B. b): ?T" by (depth_solve rules) -schematic_lemma (in Lomega) "A:* F:*\* \ F^(F^A): ?T" +schematic_goal (in Lomega) "A:* F:*\* \ F^(F^A): ?T" by (depth_solve rules) -schematic_lemma (in Lomega) "A:* \ \ F:*\*.F^(F^A): ?T" +schematic_goal (in Lomega) "A:* \ \ F:*\*.F^(F^A): ?T" by (depth_solve rules) subsection \LP\ -schematic_lemma (in LP) "A:* \ A \ * : ?T" +schematic_goal (in LP) "A:* \ A \ * : ?T" by (depth_solve rules) -schematic_lemma (in LP) "A:* P:A\* a:A \ P^a: ?T" +schematic_goal (in LP) "A:* P:A\* a:A \ P^a: ?T" by (depth_solve rules) -schematic_lemma (in LP) "A:* P:A\A\* a:A \ \ a:A. P^a^a: ?T" +schematic_goal (in LP) "A:* P:A\A\* a:A \ \ a:A. P^a^a: ?T" by (depth_solve rules) -schematic_lemma (in LP) "A:* P:A\* Q:A\* \ \ a:A. P^a \ Q^a: ?T" +schematic_goal (in LP) "A:* P:A\* Q:A\* \ \ a:A. P^a \ Q^a: ?T" by (depth_solve rules) -schematic_lemma (in LP) "A:* P:A\* \ \ a:A. P^a \ P^a: ?T" +schematic_goal (in LP) "A:* P:A\* \ \ a:A. P^a \ P^a: ?T" by (depth_solve rules) -schematic_lemma (in LP) "A:* P:A\* \ \ a:A. \ x:P^a. x: ?T" +schematic_goal (in LP) "A:* P:A\* \ \ a:A. \ x:P^a. x: ?T" by (depth_solve rules) -schematic_lemma (in LP) "A:* P:A\* Q:* \ (\ a:A. P^a\Q) \ (\ a:A. P^a) \ Q : ?T" +schematic_goal (in LP) "A:* P:A\* Q:* \ (\ a:A. P^a\Q) \ (\ a:A. P^a) \ Q : ?T" by (depth_solve rules) -schematic_lemma (in LP) "A:* P:A\* Q:* a0:A \ +schematic_goal (in LP) "A:* P:A\* Q:* a0:A \ \ x:\ a:A. P^a\Q. \ y:\ a:A. P^a. x^a0^(y^a0): ?T" by (depth_solve rules) subsection \Omega-order types\ -schematic_lemma (in L2) "A:* B:* \ \ C:*.(A\B\C)\C : ?T" +schematic_goal (in L2) "A:* B:* \ \ C:*.(A\B\C)\C : ?T" by (depth_solve rules) -schematic_lemma (in Lomega2) "\ \ A:*.\ B:*.\ C:*.(A\B\C)\C : ?T" +schematic_goal (in Lomega2) "\ \ A:*.\ B:*.\ C:*.(A\B\C)\C : ?T" by (depth_solve rules) -schematic_lemma (in Lomega2) "\ \ A:*.\ B:*.\ x:A. \ y:B. x : ?T" +schematic_goal (in Lomega2) "\ \ A:*.\ B:*.\ x:A. \ y:B. x : ?T" by (depth_solve rules) -schematic_lemma (in Lomega2) "A:* B:* \ ?p : (A\B) \ ((B\\ P:*.P)\(A\\ P:*.P))" +schematic_goal (in Lomega2) "A:* B:* \ ?p : (A\B) \ ((B\\ P:*.P)\(A\\ P:*.P))" apply (strip_asms rules) apply (rule lam_ss) apply (depth_solve1 rules) @@ -140,14 +140,14 @@ subsection \Second-order Predicate Logic\ -schematic_lemma (in LP2) "A:* P:A\* \ \ a:A. P^a\(\ A:*.A) : ?T" +schematic_goal (in LP2) "A:* P:A\* \ \ a:A. P^a\(\ A:*.A) : ?T" by (depth_solve rules) -schematic_lemma (in LP2) "A:* P:A\A\* \ +schematic_goal (in LP2) "A:* P:A\A\* \ (\ a:A. \ b:A. P^a^b\P^b^a\\ P:*.P) \ \ a:A. P^a^a\\ P:*.P : ?T" by (depth_solve rules) -schematic_lemma (in LP2) "A:* P:A\A\* \ +schematic_goal (in LP2) "A:* P:A\A\* \ ?p: (\ a:A. \ b:A. P^a^b\P^b^a\\ P:*.P) \ \ a:A. P^a^a\\ P:*.P" -- \Antisymmetry implies irreflexivity:\ apply (strip_asms rules) @@ -169,22 +169,22 @@ subsection \LPomega\ -schematic_lemma (in LPomega) "A:* \ \ P:A\A\*.\ a:A. P^a^a : ?T" +schematic_goal (in LPomega) "A:* \ \ P:A\A\*.\ a:A. P^a^a : ?T" by (depth_solve rules) -schematic_lemma (in LPomega) "\ \ A:*.\ P:A\A\*.\ a:A. P^a^a : ?T" +schematic_goal (in LPomega) "\ \ A:*.\ P:A\A\*.\ a:A. P^a^a : ?T" by (depth_solve rules) subsection \Constructions\ -schematic_lemma (in CC) "\ \ A:*.\ P:A\*.\ a:A. P^a\\ P:*.P: ?T" +schematic_goal (in CC) "\ \ A:*.\ P:A\*.\ a:A. P^a\\ P:*.P: ?T" by (depth_solve rules) -schematic_lemma (in CC) "\ \ A:*.\ P:A\*.\ a:A. P^a: ?T" +schematic_goal (in CC) "\ \ A:*.\ P:A\*.\ a:A. P^a: ?T" by (depth_solve rules) -schematic_lemma (in CC) "A:* P:A\* a:A \ ?p : (\ a:A. P^a)\P^a" +schematic_goal (in CC) "A:* P:A\* a:A \ ?p : (\ a:A. P^a)\P^a" apply (strip_asms rules) apply (rule lam_ss) apply (depth_solve1 rules) @@ -196,15 +196,15 @@ subsection \Some random examples\ -schematic_lemma (in LP2) "A:* c:A f:A\A \ +schematic_goal (in LP2) "A:* c:A f:A\A \ \ a:A. \ P:A\*.P^c \ (\ x:A. P^x\P^(f^x)) \ P^a : ?T" by (depth_solve rules) -schematic_lemma (in CC) "\ A:*.\ c:A. \ f:A\A. +schematic_goal (in CC) "\ A:*.\ c:A. \ f:A\A. \ a:A. \ P:A\*.P^c \ (\ x:A. P^x\P^(f^x)) \ P^a : ?T" by (depth_solve rules) -schematic_lemma (in LP2) +schematic_goal (in LP2) "A:* a:A b:A \ ?p: (\ P:A\*.P^a\P^b) \ (\ P:A\*.P^b\P^a)" -- \Symmetry of Leibnitz equality\ apply (strip_asms rules) diff -r fa4ebbd350ae -r 4645502c3c64 src/Doc/Codegen/Evaluation.thy --- a/src/Doc/Codegen/Evaluation.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/Doc/Codegen/Evaluation.thy Tue Oct 06 15:14:28 2015 +0200 @@ -228,7 +228,7 @@ \ ML (*<*) \\ -schematic_lemma "thm": fixes x y z :: "'a::order" shows "x < y \ x < z \ ?P" +schematic_goal "thm": fixes x y z :: "'a::order" shows "x < y \ x < z \ ?P" ML_prf (*>*) \val thm = Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \ x < z"}\ (*<*) diff -r fa4ebbd350ae -r 4645502c3c64 src/Doc/Isar_Ref/Proof.thy --- a/src/Doc/Isar_Ref/Proof.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/Doc/Isar_Ref/Proof.thy Tue Oct 06 15:14:28 2015 +0200 @@ -379,9 +379,7 @@ @{command_def "lemma"} & : & @{text "local_theory \ proof(prove)"} \\ @{command_def "theorem"} & : & @{text "local_theory \ proof(prove)"} \\ @{command_def "corollary"} & : & @{text "local_theory \ proof(prove)"} \\ - @{command_def "schematic_lemma"} & : & @{text "local_theory \ proof(prove)"} \\ - @{command_def "schematic_theorem"} & : & @{text "local_theory \ proof(prove)"} \\ - @{command_def "schematic_corollary"} & : & @{text "local_theory \ proof(prove)"} \\ + @{command_def "schematic_goal"} & : & @{text "local_theory \ proof(prove)"} \\ @{command_def "have"} & : & @{text "proof(state) | proof(chain) \ proof(prove)"} \\ @{command_def "show"} & : & @{text "proof(state) | proof(chain) \ proof(prove)"} \\ @{command_def "hence"} & : & @{text "proof(state) \ proof(prove)"} \\ @@ -423,8 +421,7 @@ @{rail \ (@@{command lemma} | @@{command theorem} | @@{command corollary} | - @@{command schematic_lemma} | @@{command schematic_theorem} | - @@{command schematic_corollary}) (stmt | statement) + @@{command schematic_goal}) (stmt | statement) ; (@@{command have} | @@{command show} | @@{command hence} | @@{command thus}) stmt cond_stmt @{syntax for_fixes} @@ -463,10 +460,8 @@ being of a different kind. This discrimination acts like a formal comment. - \item @{command "schematic_lemma"}, @{command "schematic_theorem"}, - @{command "schematic_corollary"} are similar to @{command "lemma"}, - @{command "theorem"}, @{command "corollary"}, respectively but allow - the statement to contain unbound schematic variables. + \item @{command "schematic_goal"} is similar to @{command "theorem"}, + but allows the statement to contain unbound schematic variables. Under normal circumstances, an Isar proof text needs to specify claims explicitly. Schematic goals are more like goals in Prolog, diff -r fa4ebbd350ae -r 4645502c3c64 src/Doc/Isar_Ref/Spec.thy --- a/src/Doc/Isar_Ref/Spec.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/Doc/Isar_Ref/Spec.thy Tue Oct 06 15:14:28 2015 +0200 @@ -446,9 +446,9 @@ \item @{command "declare"}~@{text thms} declares theorems to the current local theory context. No theorem binding is involved here, - unlike @{command "theorems"} or @{command "lemmas"} (cf.\ - \secref{sec:theorems}), so @{command "declare"} only has the effect - of applying attributes as included in the theorem specification. + unlike @{command "lemmas"} (cf.\ \secref{sec:theorems}), so + @{command "declare"} only has the effect of applying attributes as + included in the theorem specification. \end{description} \ @@ -1441,12 +1441,11 @@ text \ \begin{matharray}{rcll} @{command_def "lemmas"} & : & @{text "local_theory \ local_theory"} \\ - @{command_def "theorems"} & : & @{text "local_theory \ local_theory"} \\ @{command_def "named_theorems"} & : & @{text "local_theory \ local_theory"} \\ \end{matharray} @{rail \ - (@@{command lemmas} | @@{command theorems}) (@{syntax thmdef}? @{syntax thmrefs} + @'and') + @@{command lemmas} (@{syntax thmdef}? @{syntax thmrefs} + @'and') @{syntax for_fixes} ; @@{command named_theorems} (@{syntax name} @{syntax text}? + @'and') @@ -1460,9 +1459,6 @@ Results are standardized before being stored, i.e.\ schematic variables are renamed to enforce index @{text "0"} uniformly. - \item @{command "theorems"} is the same as @{command "lemmas"}, but - marks the result as a different kind of facts. - \item @{command "named_theorems"}~@{text "name description"} declares a dynamic fact within the context. The same @{text name} is used to define an attribute with the usual @{text add}/@{text del} syntax (e.g.\ see diff -r fa4ebbd350ae -r 4645502c3c64 src/FOL/ex/Classical.thy --- a/src/FOL/ex/Classical.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/FOL/ex/Classical.thy Tue Oct 06 15:14:28 2015 +0200 @@ -363,7 +363,7 @@ text\Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988). fast DISCOVERS who killed Agatha.\ -schematic_lemma "lives(agatha) & lives(butler) & lives(charles) & +schematic_goal "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 fa4ebbd350ae -r 4645502c3c64 src/FOL/ex/Prolog.thy --- a/src/FOL/ex/Prolog.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/FOL/ex/Prolog.thy Tue Oct 06 15:14:28 2015 +0200 @@ -23,18 +23,18 @@ revNil: "rev(Nil,Nil)" and revCons: "[| rev(xs,ys); app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)" -schematic_lemma "app(a:b:c:Nil, d:e:Nil, ?x)" +schematic_goal "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 -schematic_lemma "app(?x, c:d:Nil, a:b:c:d:Nil)" +schematic_goal "app(?x, c:d:Nil, a:b:c:d:Nil)" apply (rule appNil appCons)+ done -schematic_lemma "app(?x, ?y, a:b:c:d:Nil)" +schematic_goal "app(?x, ?y, a:b:c:d:Nil)" apply (rule appNil appCons)+ back back @@ -47,15 +47,15 @@ lemmas rules = appNil appCons revNil revCons -schematic_lemma "rev(a:b:c:d:Nil, ?x)" +schematic_goal "rev(a:b:c:d:Nil, ?x)" apply (rule rules)+ done -schematic_lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)" +schematic_goal "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)" apply (rule rules)+ done -schematic_lemma "rev(?x, a:b:c:Nil)" +schematic_goal "rev(?x, a:b:c:Nil)" apply (rule rules)+ -- \does not solve it directly!\ back back @@ -67,23 +67,23 @@ DEPTH_FIRST (has_fewer_prems 1) (resolve_tac ctxt @{thms rules} 1) \ -schematic_lemma "rev(?x, a:b:c:Nil)" +schematic_goal "rev(?x, a:b:c:Nil)" apply (tactic \prolog_tac @{context}\) done -schematic_lemma "rev(a:?x:c:?y:Nil, d:?z:b:?u)" +schematic_goal "rev(a:?x:c:?y:Nil, d:?z:b:?u)" apply (tactic \prolog_tac @{context}\) done (*rev([a..p], ?w) requires 153 inferences *) -schematic_lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)" +schematic_goal "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 @{context} ([@{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*) -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)" +schematic_goal "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 @{context} ([@{thm refl}, @{thm conjI}] @ @{thms rules}) 1)\) done diff -r fa4ebbd350ae -r 4645502c3c64 src/FOL/ex/Quantifiers_Cla.thy --- a/src/FOL/ex/Quantifiers_Cla.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/FOL/ex/Quantifiers_Cla.thy Tue Oct 06 15:14:28 2015 +0200 @@ -58,11 +58,11 @@ apply fast? oops -schematic_lemma "P(?a) --> (ALL x. P(x))" +schematic_goal "P(?a) --> (ALL x. P(x))" apply fast? oops -schematic_lemma "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))" +schematic_goal "(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 -schematic_lemma "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)" +schematic_goal "(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 fa4ebbd350ae -r 4645502c3c64 src/FOL/ex/Quantifiers_Int.thy --- a/src/FOL/ex/Quantifiers_Int.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/FOL/ex/Quantifiers_Int.thy Tue Oct 06 15:14:28 2015 +0200 @@ -58,11 +58,11 @@ apply (tactic "IntPr.fast_tac @{context} 1")? oops -schematic_lemma "P(?a) --> (ALL x. P(x))" +schematic_goal "P(?a) --> (ALL x. P(x))" apply (tactic "IntPr.fast_tac @{context} 1")? oops -schematic_lemma "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))" +schematic_goal "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))" apply (tactic "IntPr.fast_tac @{context} 1")? oops @@ -76,7 +76,7 @@ lemma "(P --> (EX x. Q(x))) & P --> (EX x. Q(x))" by (tactic "IntPr.fast_tac @{context} 1") -schematic_lemma "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)" +schematic_goal "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)" by (tactic "IntPr.fast_tac @{context} 1") lemma "(ALL x. Q(x)) --> (EX x. Q(x))" diff -r fa4ebbd350ae -r 4645502c3c64 src/FOLP/FOLP.thy --- a/src/FOLP/FOLP.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/FOLP/FOLP.thy Tue Oct 06 15:14:28 2015 +0200 @@ -15,7 +15,7 @@ (*** Classical introduction rules for | and EX ***) -schematic_lemma disjCI: +schematic_goal disjCI: assumes "!!x. x:~Q ==> f(x):P" shows "?p : P|Q" apply (rule classical) @@ -24,7 +24,7 @@ done (*introduction rule involving only EX*) -schematic_lemma ex_classical: +schematic_goal ex_classical: assumes "!!u. u:~(EX x. P(x)) ==> f(u):P(a)" shows "?p : EX x. P(x)" apply (rule classical) @@ -32,7 +32,7 @@ done (*version of above, simplifying ~EX to ALL~ *) -schematic_lemma exCI: +schematic_goal exCI: assumes "!!u. u:ALL x. ~P(x) ==> f(u):P(a)" shows "?p : EX x. P(x)" apply (rule ex_classical) @@ -41,7 +41,7 @@ apply (erule exI) done -schematic_lemma excluded_middle: "?p : ~P | P" +schematic_goal excluded_middle: "?p : ~P | P" apply (rule disjCI) apply assumption done @@ -50,7 +50,7 @@ (*** Special elimination rules *) (*Classical implies (-->) elimination. *) -schematic_lemma impCE: +schematic_goal impCE: assumes major: "p:P-->Q" and r1: "!!x. x:~P ==> f(x):R" and r2: "!!y. y:Q ==> g(y):R" @@ -61,7 +61,7 @@ done (*Double negation law*) -schematic_lemma notnotD: "p:~~P ==> ?p : P" +schematic_goal notnotD: "p:~~P ==> ?p : P" apply (rule classical) apply (erule notE) apply assumption @@ -72,7 +72,7 @@ (*Classical <-> elimination. Proof substitutes P=Q in ~P ==> ~Q and P ==> Q *) -schematic_lemma iffCE: +schematic_goal 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" @@ -88,7 +88,7 @@ (*Should be used as swap since ~P becomes redundant*) -schematic_lemma swap: +schematic_goal swap: assumes major: "p:~P" and r: "!!x. x:~Q ==> f(x):P" shows "?p : Q" @@ -130,7 +130,7 @@ addSEs [@{thm exE}, @{thm ex1E}] addEs [@{thm all_dupE}]; \ -schematic_lemma cla_rews: +schematic_goal cla_rews: "?p1 : P | ~P" "?p2 : ~P | P" "?p3 : ~ ~ P <-> P" diff -r fa4ebbd350ae -r 4645502c3c64 src/FOLP/IFOLP.thy --- a/src/FOLP/IFOLP.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/FOLP/IFOLP.thy Tue Oct 06 15:14:28 2015 +0200 @@ -171,7 +171,7 @@ (*** Sequent-style elimination rules for & --> and ALL ***) -schematic_lemma conjE: +schematic_goal conjE: assumes "p:P&Q" and "!!x y.[| x:P; y:Q |] ==> f(x,y):R" shows "?a:R" @@ -180,7 +180,7 @@ apply (rule conjunct2 [OF assms(1)]) done -schematic_lemma impE: +schematic_goal impE: assumes "p:P-->Q" and "q:P" and "!!x. x:Q ==> r(x):R" @@ -188,7 +188,7 @@ apply (rule assms mp)+ done -schematic_lemma allE: +schematic_goal allE: assumes "p:ALL x. P(x)" and "!!y. y:P(x) ==> q(y):R" shows "?p:R" @@ -196,7 +196,7 @@ done (*Duplicates the quantifier; for use with eresolve_tac*) -schematic_lemma all_dupE: +schematic_goal 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" @@ -206,21 +206,21 @@ (*** Negation rules, which translate between ~P and P-->False ***) -schematic_lemma notI: +schematic_goal notI: assumes "!!x. x:P ==> q(x):False" shows "?p:~P" unfolding not_def apply (assumption | rule assms impI)+ done -schematic_lemma notE: "p:~P \ q:P \ ?p:R" +schematic_goal 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. *) -schematic_lemma not_to_imp: +schematic_goal not_to_imp: assumes "p:~P" and "!!x. x:(P-->False) ==> q(x):Q" shows "?p:Q" @@ -229,13 +229,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.*) -schematic_lemma rev_mp: "[| p:P; q:P --> Q |] ==> ?p:Q" +schematic_goal rev_mp: "[| p:P; q:P --> Q |] ==> ?p:Q" apply (assumption | rule mp)+ done (*Contrapositive of an inference rule*) -schematic_lemma contrapos: +schematic_goal contrapos: assumes major: "p:~Q" and minor: "!!y. y:P==>q(y):Q" shows "?a:~P" @@ -286,7 +286,7 @@ (*** If-and-only-if ***) -schematic_lemma iffI: +schematic_goal iffI: assumes "!!x. x:P ==> q(x):Q" and "!!x. x:Q ==> r(x):P" shows "?p:P<->Q" @@ -295,7 +295,7 @@ done -schematic_lemma iffE: +schematic_goal iffE: assumes "p:P <-> Q" and "!!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R" shows "?p:R" @@ -307,28 +307,28 @@ (* Destruct rules for <-> similar to Modus Ponens *) -schematic_lemma iffD1: "[| p:P <-> Q; q:P |] ==> ?p:Q" +schematic_goal iffD1: "[| p:P <-> Q; q:P |] ==> ?p:Q" unfolding iff_def apply (rule conjunct1 [THEN mp], assumption+) done -schematic_lemma iffD2: "[| p:P <-> Q; q:Q |] ==> ?p:P" +schematic_goal iffD2: "[| p:P <-> Q; q:Q |] ==> ?p:P" unfolding iff_def apply (rule conjunct2 [THEN mp], assumption+) done -schematic_lemma iff_refl: "?p:P <-> P" +schematic_goal iff_refl: "?p:P <-> P" apply (rule iffI) apply assumption+ done -schematic_lemma iff_sym: "p:Q <-> P ==> ?p:P <-> Q" +schematic_goal iff_sym: "p:Q <-> P ==> ?p:P <-> Q" apply (erule iffE) apply (rule iffI) apply (erule (1) mp)+ done -schematic_lemma iff_trans: "[| p:P <-> Q; q:Q<-> R |] ==> ?p:P <-> R" +schematic_goal iff_trans: "[| p:P <-> Q; q:Q<-> R |] ==> ?p:P <-> R" apply (rule iffI) apply (assumption | erule iffE | erule (1) impE)+ done @@ -339,7 +339,7 @@ do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential. ***) -schematic_lemma ex1I: +schematic_goal ex1I: assumes "p:P(a)" and "!!x u. u:P(x) ==> f(u) : x=a" shows "?p:EX! x. P(x)" @@ -347,7 +347,7 @@ apply (assumption | rule assms exI conjI allI impI)+ done -schematic_lemma ex1E: +schematic_goal 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" @@ -369,7 +369,7 @@ method_setup iff = \Attrib.thms >> (fn prems => fn ctxt => SIMPLE_METHOD' (iff_tac ctxt prems))\ -schematic_lemma conj_cong: +schematic_goal conj_cong: assumes "p:P <-> P'" and "!!x. x:P' ==> q(x):Q <-> Q'" shows "?p:(P&Q) <-> (P'&Q')" @@ -377,12 +377,12 @@ apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+ done -schematic_lemma disj_cong: +schematic_goal disj_cong: "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P|Q) <-> (P'|Q')" apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | mp)+ done -schematic_lemma imp_cong: +schematic_goal imp_cong: assumes "p:P <-> P'" and "!!x. x:P' ==> q(x):Q <-> Q'" shows "?p:(P-->Q) <-> (P'-->Q')" @@ -390,23 +390,23 @@ apply (assumption | rule iffI impI | erule iffE | mp | iff assms)+ done -schematic_lemma iff_cong: +schematic_goal iff_cong: "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')" apply (erule iffE | assumption | rule iffI | mp)+ done -schematic_lemma not_cong: +schematic_goal not_cong: "p:P <-> P' ==> ?p:~P <-> ~P'" apply (assumption | rule iffI notI | mp | erule iffE notE)+ done -schematic_lemma all_cong: +schematic_goal 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 | mp | erule allE | iff assms)+ done -schematic_lemma ex_cong: +schematic_goal 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 | mp | iff assms)+ @@ -425,7 +425,7 @@ lemmas refl = ieqI -schematic_lemma subst: +schematic_goal subst: assumes prem1: "p:a=b" and prem2: "q:P(a)" shows "?p : P(b)" @@ -435,29 +435,29 @@ apply assumption done -schematic_lemma sym: "q:a=b ==> ?c:b=a" +schematic_goal sym: "q:a=b ==> ?c:b=a" apply (erule subst) apply (rule refl) done -schematic_lemma trans: "[| p:a=b; q:b=c |] ==> ?d:a=c" +schematic_goal trans: "[| p:a=b; q:b=c |] ==> ?d:a=c" apply (erule (1) subst) done (** ~ b=a ==> ~ a=b **) -schematic_lemma not_sym: "p:~ b=a ==> ?q:~ a=b" +schematic_goal not_sym: "p:~ b=a ==> ?q:~ a=b" apply (erule contrapos) apply (erule sym) done -schematic_lemma ssubst: "p:b=a \ q:P(a) \ ?p:P(b)" +schematic_goal ssubst: "p:b=a \ q:P(a) \ ?p:P(b)" apply (drule sym) apply (erule subst) apply assumption done (*A special case of ex1E that would otherwise need quantifier expansion*) -schematic_lemma ex1_equalsE: "[| p:EX! x. P(x); q:P(a); r:P(b) |] ==> ?d:a=b" +schematic_goal 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) @@ -466,17 +466,17 @@ (** Polymorphic congruence rules **) -schematic_lemma subst_context: "[| p:a=b |] ==> ?d:t(a)=t(b)" +schematic_goal subst_context: "[| p:a=b |] ==> ?d:t(a)=t(b)" apply (erule ssubst) apply (rule refl) done -schematic_lemma subst_context2: "[| p:a=b; q:c=d |] ==> ?p:t(a,c)=t(b,d)" +schematic_goal subst_context2: "[| p:a=b; q:c=d |] ==> ?p:t(a,c)=t(b,d)" apply (erule ssubst)+ apply (rule refl) done -schematic_lemma subst_context3: "[| p:a=b; q:c=d; r:e=f |] ==> ?p:t(a,c,e)=t(b,d,f)" +schematic_goal 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 @@ -485,7 +485,7 @@ a = b | | c = d *) -schematic_lemma box_equals: "[| p:a=b; q:a=c; r:b=d |] ==> ?p:c=d" +schematic_goal box_equals: "[| p:a=b; q:a=c; r:b=d |] ==> ?p:c=d" apply (rule trans) apply (rule trans) apply (rule sym) @@ -493,7 +493,7 @@ done (*Dual of box_equals: for proving equalities backwards*) -schematic_lemma simp_equals: "[| p:a=c; q:b=d; r:c=d |] ==> ?p:a=b" +schematic_goal simp_equals: "[| p:a=c; q:b=d; r:c=d |] ==> ?p:a=b" apply (rule trans) apply (rule trans) apply (assumption | rule sym)+ @@ -501,19 +501,19 @@ (** Congruence rules for predicate letters **) -schematic_lemma pred1_cong: "p:a=a' ==> ?p:P(a) <-> P(a')" +schematic_goal pred1_cong: "p:a=a' ==> ?p:P(a) <-> P(a')" apply (rule iffI) apply (tactic \ DEPTH_SOLVE (assume_tac @{context} 1 ORELSE eresolve_tac @{context} [@{thm subst}, @{thm ssubst}] 1)\) done -schematic_lemma pred2_cong: "[| p:a=a'; q:b=b' |] ==> ?p:P(a,b) <-> P(a',b')" +schematic_goal pred2_cong: "[| p:a=a'; q:b=b' |] ==> ?p:P(a,b) <-> P(a',b')" apply (rule iffI) apply (tactic \ DEPTH_SOLVE (assume_tac @{context} 1 ORELSE eresolve_tac @{context} [@{thm subst}, @{thm ssubst}] 1)\) done -schematic_lemma pred3_cong: "[| p:a=a'; q:b=b'; r:c=c' |] ==> ?p:P(a,b,c) <-> P(a',b',c')" +schematic_goal 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 (assume_tac @{context} 1 ORELSE eresolve_tac @{context} [@{thm subst}, @{thm ssubst}] 1)\) @@ -532,14 +532,14 @@ R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic (preprint, University of St Andrews, 1991) ***) -schematic_lemma conj_impE: +schematic_goal 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 -schematic_lemma disj_impE: +schematic_goal 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" @@ -550,7 +550,7 @@ (*Simplifies the implication. Classical version is stronger. Still UNSAFE since Q must be provable -- backtracking needed. *) -schematic_lemma imp_impE: +schematic_goal 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" @@ -560,7 +560,7 @@ (*Simplifies the implication. Classical version is stronger. Still UNSAFE since ~P must be provable -- backtracking needed. *) -schematic_lemma not_impE: +schematic_goal not_impE: assumes major: "p:~P --> S" and r1: "!!y. y:P ==> q(y):False" and r2: "!!y. y:S ==> r(y):R" @@ -569,7 +569,7 @@ done (*Simplifies the implication. UNSAFE. *) -schematic_lemma iff_impE: +schematic_goal 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" @@ -579,7 +579,7 @@ done (*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*) -schematic_lemma all_impE: +schematic_goal all_impE: assumes major: "p:(ALL x. P(x))-->S" and r1: "!!x. q:P(x)" and r2: "!!y. y:S ==> r(y):R" @@ -588,7 +588,7 @@ done (*Unsafe: (EX x.P(x))-->S is equivalent to ALL x.P(x)-->S. *) -schematic_lemma ex_impE: +schematic_goal ex_impE: assumes major: "p:(EX x. P(x))-->S" and r: "!!y. y:P(a)-->S ==> q(y):R" shows "?p:R" @@ -596,7 +596,7 @@ done -schematic_lemma rev_cut_eq: +schematic_goal rev_cut_eq: assumes "p:a=b" and "!!x. x:a=b ==> f(x):R" shows "?p:R" @@ -632,7 +632,7 @@ (*** Rewrite rules ***) -schematic_lemma conj_rews: +schematic_goal conj_rews: "?p1 : P & True <-> P" "?p2 : True & P <-> P" "?p3 : P & False <-> False" @@ -644,7 +644,7 @@ apply (tactic \fn st => IntPr.fast_tac @{context} 1 st\)+ done -schematic_lemma disj_rews: +schematic_goal disj_rews: "?p1 : P | True <-> True" "?p2 : True | P <-> True" "?p3 : P | False <-> P" @@ -654,13 +654,13 @@ apply (tactic \IntPr.fast_tac @{context} 1\)+ done -schematic_lemma not_rews: +schematic_goal not_rews: "?p1 : ~ False <-> True" "?p2 : ~ True <-> False" apply (tactic \IntPr.fast_tac @{context} 1\)+ done -schematic_lemma imp_rews: +schematic_goal imp_rews: "?p1 : (P --> False) <-> ~P" "?p2 : (P --> True) <-> True" "?p3 : (False --> P) <-> True" @@ -670,7 +670,7 @@ apply (tactic \IntPr.fast_tac @{context} 1\)+ done -schematic_lemma iff_rews: +schematic_goal iff_rews: "?p1 : (True <-> P) <-> P" "?p2 : (P <-> True) <-> P" "?p3 : (P <-> P) <-> True" @@ -679,14 +679,14 @@ apply (tactic \IntPr.fast_tac @{context} 1\)+ done -schematic_lemma quant_rews: +schematic_goal quant_rews: "?p1 : (ALL x. P) <-> P" "?p2 : (EX x. P) <-> P" apply (tactic \IntPr.fast_tac @{context} 1\)+ done (*These are NOT supplied by default!*) -schematic_lemma distrib_rews1: +schematic_goal distrib_rews1: "?p1 : ~(P|Q) <-> ~P & ~Q" "?p2 : P & (Q | R) <-> P&Q | P&R" "?p3 : (Q | R) & P <-> Q&P | R&P" @@ -694,7 +694,7 @@ apply (tactic \IntPr.fast_tac @{context} 1\)+ done -schematic_lemma distrib_rews2: +schematic_goal 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))" @@ -704,11 +704,11 @@ lemmas distrib_rews = distrib_rews1 distrib_rews2 -schematic_lemma P_Imp_P_iff_T: "p:P ==> ?p:(P <-> True)" +schematic_goal P_Imp_P_iff_T: "p:P ==> ?p:(P <-> True)" apply (tactic \IntPr.fast_tac @{context} 1\) done -schematic_lemma not_P_imp_P_iff_F: "p:~P ==> ?p:(P <-> False)" +schematic_goal not_P_imp_P_iff_F: "p:~P ==> ?p:(P <-> False)" apply (tactic \IntPr.fast_tac @{context} 1\) done diff -r fa4ebbd350ae -r 4645502c3c64 src/FOLP/ex/Classical.thy --- a/src/FOLP/ex/Classical.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/FOLP/ex/Classical.thy Tue Oct 06 15:14:28 2015 +0200 @@ -9,14 +9,14 @@ imports FOLP begin -schematic_lemma "?p : (P --> Q | R) --> (P-->Q) | (P-->R)" +schematic_goal "?p : (P --> Q | R) --> (P-->Q) | (P-->R)" by (tactic "fast_tac @{context} FOLP_cs 1") (*If and only if*) -schematic_lemma "?p : (P<->Q) <-> (Q<->P)" +schematic_goal "?p : (P<->Q) <-> (Q<->P)" by (tactic "fast_tac @{context} FOLP_cs 1") -schematic_lemma "?p : ~ (P <-> ~P)" +schematic_goal "?p : ~ (P <-> ~P)" by (tactic "fast_tac @{context} FOLP_cs 1") @@ -32,138 +32,138 @@ text "Pelletier's examples" (*1*) -schematic_lemma "?p : (P-->Q) <-> (~Q --> ~P)" +schematic_goal "?p : (P-->Q) <-> (~Q --> ~P)" by (tactic "fast_tac @{context} FOLP_cs 1") (*2*) -schematic_lemma "?p : ~ ~ P <-> P" +schematic_goal "?p : ~ ~ P <-> P" by (tactic "fast_tac @{context} FOLP_cs 1") (*3*) -schematic_lemma "?p : ~(P-->Q) --> (Q-->P)" +schematic_goal "?p : ~(P-->Q) --> (Q-->P)" by (tactic "fast_tac @{context} FOLP_cs 1") (*4*) -schematic_lemma "?p : (~P-->Q) <-> (~Q --> P)" +schematic_goal "?p : (~P-->Q) <-> (~Q --> P)" by (tactic "fast_tac @{context} FOLP_cs 1") (*5*) -schematic_lemma "?p : ((P|Q)-->(P|R)) --> (P|(Q-->R))" +schematic_goal "?p : ((P|Q)-->(P|R)) --> (P|(Q-->R))" by (tactic "fast_tac @{context} FOLP_cs 1") (*6*) -schematic_lemma "?p : P | ~ P" +schematic_goal "?p : P | ~ P" by (tactic "fast_tac @{context} FOLP_cs 1") (*7*) -schematic_lemma "?p : P | ~ ~ ~ P" +schematic_goal "?p : P | ~ ~ ~ P" by (tactic "fast_tac @{context} FOLP_cs 1") (*8. Peirce's law*) -schematic_lemma "?p : ((P-->Q) --> P) --> P" +schematic_goal "?p : ((P-->Q) --> P) --> P" by (tactic "fast_tac @{context} FOLP_cs 1") (*9*) -schematic_lemma "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)" +schematic_goal "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)" by (tactic "fast_tac @{context} FOLP_cs 1") (*10*) -schematic_lemma "?p : (Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)" +schematic_goal "?p : (Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)" by (tactic "fast_tac @{context} FOLP_cs 1") (*11. Proved in each direction (incorrectly, says Pelletier!!) *) -schematic_lemma "?p : P<->P" +schematic_goal "?p : P<->P" by (tactic "fast_tac @{context} FOLP_cs 1") (*12. "Dijkstra's law"*) -schematic_lemma "?p : ((P <-> Q) <-> R) <-> (P <-> (Q <-> R))" +schematic_goal "?p : ((P <-> Q) <-> R) <-> (P <-> (Q <-> R))" by (tactic "fast_tac @{context} FOLP_cs 1") (*13. Distributive law*) -schematic_lemma "?p : P | (Q & R) <-> (P | Q) & (P | R)" +schematic_goal "?p : P | (Q & R) <-> (P | Q) & (P | R)" by (tactic "fast_tac @{context} FOLP_cs 1") (*14*) -schematic_lemma "?p : (P <-> Q) <-> ((Q | ~P) & (~Q|P))" +schematic_goal "?p : (P <-> Q) <-> ((Q | ~P) & (~Q|P))" by (tactic "fast_tac @{context} FOLP_cs 1") (*15*) -schematic_lemma "?p : (P --> Q) <-> (~P | Q)" +schematic_goal "?p : (P --> Q) <-> (~P | Q)" by (tactic "fast_tac @{context} FOLP_cs 1") (*16*) -schematic_lemma "?p : (P-->Q) | (Q-->P)" +schematic_goal "?p : (P-->Q) | (Q-->P)" by (tactic "fast_tac @{context} FOLP_cs 1") (*17*) -schematic_lemma "?p : ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))" +schematic_goal "?p : ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))" by (tactic "fast_tac @{context} FOLP_cs 1") text "Classical Logic: examples with quantifiers" -schematic_lemma "?p : (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))" +schematic_goal "?p : (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))" by (tactic "fast_tac @{context} FOLP_cs 1") -schematic_lemma "?p : (EX x. P-->Q(x)) <-> (P --> (EX x. Q(x)))" +schematic_goal "?p : (EX x. P-->Q(x)) <-> (P --> (EX x. Q(x)))" by (tactic "fast_tac @{context} FOLP_cs 1") -schematic_lemma "?p : (EX x. P(x)-->Q) <-> (ALL x. P(x)) --> Q" +schematic_goal "?p : (EX x. P(x)-->Q) <-> (ALL x. P(x)) --> Q" by (tactic "fast_tac @{context} FOLP_cs 1") -schematic_lemma "?p : (ALL x. P(x)) | Q <-> (ALL x. P(x) | Q)" +schematic_goal "?p : (ALL x. P(x)) | Q <-> (ALL x. P(x) | Q)" by (tactic "fast_tac @{context} FOLP_cs 1") text "Problems requiring quantifier duplication" (*Needs multiple instantiation of ALL.*) -schematic_lemma "?p : (ALL x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))" +schematic_goal "?p : (ALL x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))" by (tactic "best_tac @{context} FOLP_dup_cs 1") (*Needs double instantiation of the quantifier*) -schematic_lemma "?p : EX x. P(x) --> P(a) & P(b)" +schematic_goal "?p : EX x. P(x) --> P(a) & P(b)" by (tactic "best_tac @{context} FOLP_dup_cs 1") -schematic_lemma "?p : EX z. P(z) --> (ALL x. P(x))" +schematic_goal "?p : EX z. P(z) --> (ALL x. P(x))" by (tactic "best_tac @{context} FOLP_dup_cs 1") text "Hard examples with quantifiers" text "Problem 18" -schematic_lemma "?p : EX y. ALL x. P(y)-->P(x)" +schematic_goal "?p : EX y. ALL x. P(y)-->P(x)" by (tactic "best_tac @{context} FOLP_dup_cs 1") text "Problem 19" -schematic_lemma "?p : EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))" +schematic_goal "?p : EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))" by (tactic "best_tac @{context} FOLP_dup_cs 1") text "Problem 20" -schematic_lemma "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w))) +schematic_goal "?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 @{context} FOLP_cs 1") text "Problem 21" -schematic_lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))" +schematic_goal "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))" by (tactic "best_tac @{context} FOLP_dup_cs 1") text "Problem 22" -schematic_lemma "?p : (ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))" +schematic_goal "?p : (ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))" by (tactic "fast_tac @{context} FOLP_cs 1") text "Problem 23" -schematic_lemma "?p : (ALL x. P | Q(x)) <-> (P | (ALL x. Q(x)))" +schematic_goal "?p : (ALL x. P | Q(x)) <-> (P | (ALL x. Q(x)))" by (tactic "best_tac @{context} FOLP_dup_cs 1") text "Problem 24" -schematic_lemma "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) & +schematic_goal "?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 @{context} FOLP_cs 1") text "Problem 25" -schematic_lemma "?p : (EX x. P(x)) & +schematic_goal "?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" -schematic_lemma "?u : ((EX x. p(x)) <-> (EX x. q(x))) & +schematic_goal "?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 @{context} FOLP_cs 1") text "Problem 27" -schematic_lemma "?p : (EX x. P(x) & ~Q(x)) & +schematic_goal "?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 @{context} FOLP_cs 1") text "Problem 28. AMENDED" -schematic_lemma "?p : (ALL x. P(x) --> (ALL x. Q(x))) & +schematic_goal "?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 @{context} FOLP_cs 1") text "Problem 29. Essentially the same as Principia Mathematica *11.71" -schematic_lemma "?p : (EX x. P(x)) & (EX y. Q(y)) +schematic_goal "?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 @{context} FOLP_cs 1") text "Problem 30" -schematic_lemma "?p : (ALL x. P(x) | Q(x) --> ~ R(x)) & +schematic_goal "?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 @{context} FOLP_cs 1") text "Problem 31" -schematic_lemma "?p : ~(EX x. P(x) & (Q(x) | R(x))) & +schematic_goal "?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 @{context} FOLP_cs 1") text "Problem 32" -schematic_lemma "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & +schematic_goal "?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 @{context} FOLP_dup_cs 1") text "Problem 33" -schematic_lemma "?p : (ALL x. P(a) & (P(x)-->P(b))-->P(c)) <-> +schematic_goal "?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 @{context} FOLP_dup_cs 1") text "Problem 35" -schematic_lemma "?p : EX x y. P(x,y) --> (ALL u v. P(u,v))" +schematic_goal "?p : EX x y. P(x,y) --> (ALL u v. P(u,v))" by (tactic "best_tac @{context} FOLP_dup_cs 1") text "Problem 36" -schematic_lemma +schematic_goal "?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 @{context} FOLP_cs 1") text "Problem 37" -schematic_lemma "?p : (ALL z. EX w. ALL x. EX y. +schematic_goal "?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 @{context} FOLP_cs 1") text "Problem 39" -schematic_lemma "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))" +schematic_goal "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))" by (tactic "fast_tac @{context} FOLP_cs 1") text "Problem 40. AMENDED" -schematic_lemma "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) --> +schematic_goal "?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 @{context} FOLP_cs 1") text "Problem 41" -schematic_lemma "?p : (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x)) +schematic_goal "?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 @{context} FOLP_dup_cs 1") text "Problem 44" -schematic_lemma "?p : (ALL x. f(x) --> +schematic_goal "?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,36 +266,36 @@ text "Problems (mainly) involving equality or functions" text "Problem 48" -schematic_lemma "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c" +schematic_goal "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c" by (tactic "fast_tac @{context} FOLP_cs 1") text "Problem 50" (*What has this to do with equality?*) -schematic_lemma "?p : (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))" +schematic_goal "?p : (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))" by (tactic "best_tac @{context} FOLP_dup_cs 1") text "Problem 56" -schematic_lemma +schematic_goal "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))" by (tactic "fast_tac @{context} FOLP_cs 1") text "Problem 57" -schematic_lemma +schematic_goal "?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 @{context} FOLP_cs 1") text "Problem 58 NOT PROVED AUTOMATICALLY" -schematic_lemma "?p : (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))" +schematic_goal "?p : (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))" supply f_cong = subst_context [where t = f] by (tactic \fast_tac @{context} (FOLP_cs addSIs [@{thm f_cong}]) 1\) text "Problem 59" -schematic_lemma "?p : (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))" +schematic_goal "?p : (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))" by (tactic "best_tac @{context} FOLP_dup_cs 1") text "Problem 60" -schematic_lemma "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))" +schematic_goal "?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 @{context} FOLP_cs 1") end diff -r fa4ebbd350ae -r 4645502c3c64 src/FOLP/ex/Foundation.thy --- a/src/FOLP/ex/Foundation.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/FOLP/ex/Foundation.thy Tue Oct 06 15:14:28 2015 +0200 @@ -9,7 +9,7 @@ imports IFOLP begin -schematic_lemma "?p : A&B --> (C-->A&C)" +schematic_goal "?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\ -schematic_lemma +schematic_goal assumes "p : A & B" and "!!x y. x : A ==> y : B ==> f(x, y) : C" shows "?p : C" @@ -30,7 +30,7 @@ apply (rule assms) done -schematic_lemma +schematic_goal assumes "!!A x. x : ~ ~A ==> cla(x) : A" shows "?p : B | ~B" apply (rule assms) @@ -48,7 +48,7 @@ apply assumption done -schematic_lemma +schematic_goal assumes "!!A x. x : ~ ~A ==> cla(x) : A" shows "?p : B | ~B" apply (rule assms) @@ -63,7 +63,7 @@ done -schematic_lemma +schematic_goal assumes "p : A | ~A" and "q : ~ ~A" shows "?p : A" @@ -79,7 +79,7 @@ subsection "Examples with quantifiers" -schematic_lemma +schematic_goal assumes "p : ALL z. G(z)" shows "?p : ALL z. G(z)|H(z)" apply (rule allI) @@ -87,20 +87,20 @@ apply (rule assms [THEN spec]) done -schematic_lemma "?p : ALL x. EX y. x=y" +schematic_goal "?p : ALL x. EX y. x=y" apply (rule allI) apply (rule exI) apply (rule refl) done -schematic_lemma "?p : EX y. ALL x. x=y" +schematic_goal "?p : EX y. ALL x. x=y" apply (rule exI) apply (rule allI) apply (rule refl)? oops text \Parallel lifting example.\ -schematic_lemma "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)" +schematic_goal "?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 -schematic_lemma +schematic_goal 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.\ -schematic_lemma "?p : (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))" +schematic_goal "?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 fa4ebbd350ae -r 4645502c3c64 src/FOLP/ex/If.thy --- a/src/FOLP/ex/If.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/FOLP/ex/If.thy Tue Oct 06 15:14:28 2015 +0200 @@ -5,14 +5,14 @@ definition "if" :: "[o,o,o]=>o" where "if(P,Q,R) == P&Q | ~P&R" -schematic_lemma ifI: +schematic_goal 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 @{context} (FOLP_cs addIs @{thms assms}) 1\) done -schematic_lemma ifE: +schematic_goal 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 @{context} (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1\) done -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))" +schematic_goal 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}]\ -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))" +schematic_goal 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 @{context} if_cs 1\) done -schematic_lemma nested_ifs: "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))" +schematic_goal nested_ifs: "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))" apply (tactic \fast_tac @{context} if_cs 1\) done diff -r fa4ebbd350ae -r 4645502c3c64 src/FOLP/ex/Intro.thy --- a/src/FOLP/ex/Intro.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/FOLP/ex/Intro.thy Tue Oct 06 15:14:28 2015 +0200 @@ -13,7 +13,7 @@ subsubsection \Some simple backward proofs\ -schematic_lemma mythm: "?p : P|P --> P" +schematic_goal mythm: "?p : P|P --> P" apply (rule impI) apply (rule disjE) prefer 3 apply (assumption) @@ -21,7 +21,7 @@ apply assumption done -schematic_lemma "?p : (P & Q) | R --> (P | R)" +schematic_goal "?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*) -schematic_lemma "?p : (ALL x y. P(x,y)) --> (ALL z w. P(w,z))" +schematic_goal "?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"}\ -schematic_lemma "?p : (EX y. ALL x. J(y,x) <-> ~J(x,x)) +schematic_goal "?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 @{context} FOLP_cs 1\) done -schematic_lemma "?p : ALL x. P(x,f(x)) <-> +schematic_goal "?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 @{context} FOLP_cs 1\) done @@ -57,7 +57,7 @@ subsubsection \Derivation of conjunction elimination rule\ -schematic_lemma +schematic_goal 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\ -schematic_lemma +schematic_goal assumes "!!x. x : P ==> f(x) : False" shows "?p : ~ P" apply (unfold not_def) @@ -80,7 +80,7 @@ apply assumption done -schematic_lemma +schematic_goal assumes major: "p : ~P" and minor: "q : P" shows "?p : R" @@ -91,7 +91,7 @@ done text \Alternative proof of the result above\ -schematic_lemma +schematic_goal assumes major: "p : ~P" and minor: "q : P" shows "?p : R" diff -r fa4ebbd350ae -r 4645502c3c64 src/FOLP/ex/Intuitionistic.thy --- a/src/FOLP/ex/Intuitionistic.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/FOLP/ex/Intuitionistic.thy Tue Oct 06 15:14:28 2015 +0200 @@ -30,39 +30,39 @@ imports IFOLP begin -schematic_lemma "?p : ~~(P&Q) <-> ~~P & ~~Q" +schematic_goal "?p : ~~(P&Q) <-> ~~P & ~~Q" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma "?p : ~~~P <-> ~P" +schematic_goal "?p : ~~~P <-> ~P" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma "?p : ~~((P --> Q | R) --> (P-->Q) | (P-->R))" +schematic_goal "?p : ~~((P --> Q | R) --> (P-->Q) | (P-->R))" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma "?p : (P<->Q) <-> (Q<->P)" +schematic_goal "?p : (P<->Q) <-> (Q<->P)" by (tactic \IntPr.fast_tac @{context} 1\) subsection \Lemmas for the propositional double-negation translation\ -schematic_lemma "?p : P --> ~~P" +schematic_goal "?p : P --> ~~P" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma "?p : ~~(~~P --> P)" +schematic_goal "?p : ~~(~~P --> P)" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma "?p : ~~P & ~~(P --> Q) --> ~~Q" +schematic_goal "?p : ~~P & ~~(P --> Q) --> ~~Q" by (tactic \IntPr.fast_tac @{context} 1\) subsection \The following are classically but not constructively valid\ (*The attempt to prove them terminates quickly!*) -schematic_lemma "?p : ((P-->Q) --> P) --> P" +schematic_goal "?p : ((P-->Q) --> P) --> P" apply (tactic \IntPr.fast_tac @{context} 1\)? oops -schematic_lemma "?p : (P&Q-->R) --> (P-->R) | (Q-->R)" +schematic_goal "?p : (P&Q-->R) --> (P-->R) | (Q-->R)" apply (tactic \IntPr.fast_tac @{context} 1\)? oops @@ -70,74 +70,74 @@ subsection \Intuitionistic FOL: propositional problems based on Pelletier\ text "Problem ~~1" -schematic_lemma "?p : ~~((P-->Q) <-> (~Q --> ~P))" +schematic_goal "?p : ~~((P-->Q) <-> (~Q --> ~P))" by (tactic \IntPr.fast_tac @{context} 1\) text "Problem ~~2" -schematic_lemma "?p : ~~(~~P <-> P)" +schematic_goal "?p : ~~(~~P <-> P)" by (tactic \IntPr.fast_tac @{context} 1\) text "Problem 3" -schematic_lemma "?p : ~(P-->Q) --> (Q-->P)" +schematic_goal "?p : ~(P-->Q) --> (Q-->P)" by (tactic \IntPr.fast_tac @{context} 1\) text "Problem ~~4" -schematic_lemma "?p : ~~((~P-->Q) <-> (~Q --> P))" +schematic_goal "?p : ~~((~P-->Q) <-> (~Q --> P))" by (tactic \IntPr.fast_tac @{context} 1\) text "Problem ~~5" -schematic_lemma "?p : ~~((P|Q-->P|R) --> P|(Q-->R))" +schematic_goal "?p : ~~((P|Q-->P|R) --> P|(Q-->R))" by (tactic \IntPr.fast_tac @{context} 1\) text "Problem ~~6" -schematic_lemma "?p : ~~(P | ~P)" +schematic_goal "?p : ~~(P | ~P)" by (tactic \IntPr.fast_tac @{context} 1\) text "Problem ~~7" -schematic_lemma "?p : ~~(P | ~~~P)" +schematic_goal "?p : ~~(P | ~~~P)" by (tactic \IntPr.fast_tac @{context} 1\) text "Problem ~~8. Peirce's law" -schematic_lemma "?p : ~~(((P-->Q) --> P) --> P)" +schematic_goal "?p : ~~(((P-->Q) --> P) --> P)" by (tactic \IntPr.fast_tac @{context} 1\) text "Problem 9" -schematic_lemma "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)" +schematic_goal "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)" by (tactic \IntPr.fast_tac @{context} 1\) text "Problem 10" -schematic_lemma "?p : (Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)" +schematic_goal "?p : (Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)" by (tactic \IntPr.fast_tac @{context} 1\) text "11. Proved in each direction (incorrectly, says Pelletier!!) " -schematic_lemma "?p : P<->P" +schematic_goal "?p : P<->P" by (tactic \IntPr.fast_tac @{context} 1\) text "Problem ~~12. Dijkstra's law " -schematic_lemma "?p : ~~(((P <-> Q) <-> R) <-> (P <-> (Q <-> R)))" +schematic_goal "?p : ~~(((P <-> Q) <-> R) <-> (P <-> (Q <-> R)))" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma "?p : ((P <-> Q) <-> R) --> ~~(P <-> (Q <-> R))" +schematic_goal "?p : ((P <-> Q) <-> R) --> ~~(P <-> (Q <-> R))" by (tactic \IntPr.fast_tac @{context} 1\) text "Problem 13. Distributive law" -schematic_lemma "?p : P | (Q & R) <-> (P | Q) & (P | R)" +schematic_goal "?p : P | (Q & R) <-> (P | Q) & (P | R)" by (tactic \IntPr.fast_tac @{context} 1\) text "Problem ~~14" -schematic_lemma "?p : ~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))" +schematic_goal "?p : ~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))" by (tactic \IntPr.fast_tac @{context} 1\) text "Problem ~~15" -schematic_lemma "?p : ~~((P --> Q) <-> (~P | Q))" +schematic_goal "?p : ~~((P --> Q) <-> (~P | Q))" by (tactic \IntPr.fast_tac @{context} 1\) text "Problem ~~16" -schematic_lemma "?p : ~~((P-->Q) | (Q-->P))" +schematic_goal "?p : ~~((P-->Q) | (Q-->P))" by (tactic \IntPr.fast_tac @{context} 1\) text "Problem ~~17" -schematic_lemma "?p : ~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))" +schematic_goal "?p : ~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))" by (tactic \IntPr.fast_tac @{context} 1\) -- slow @@ -145,43 +145,43 @@ text "The converse is classical in the following implications..." -schematic_lemma "?p : (EX x. P(x)-->Q) --> (ALL x. P(x)) --> Q" +schematic_goal "?p : (EX x. P(x)-->Q) --> (ALL x. P(x)) --> Q" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma "?p : ((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)" +schematic_goal "?p : ((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma "?p : ((ALL x. ~P(x))-->Q) --> ~ (ALL x. ~ (P(x)|Q))" +schematic_goal "?p : ((ALL x. ~P(x))-->Q) --> ~ (ALL x. ~ (P(x)|Q))" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma "?p : (ALL x. P(x)) | Q --> (ALL x. P(x) | Q)" +schematic_goal "?p : (ALL x. P(x)) | Q --> (ALL x. P(x) | Q)" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma "?p : (EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))" +schematic_goal "?p : (EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))" by (tactic \IntPr.fast_tac @{context} 1\) text "The following are not constructively valid!" text "The attempt to prove them terminates quickly!" -schematic_lemma "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)" +schematic_goal "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)" apply (tactic \IntPr.fast_tac @{context} 1\)? oops -schematic_lemma "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))" +schematic_goal "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))" apply (tactic \IntPr.fast_tac @{context} 1\)? oops -schematic_lemma "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)" +schematic_goal "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)" apply (tactic \IntPr.fast_tac @{context} 1\)? oops -schematic_lemma "?p : (ALL x. ~~P(x)) --> ~~(ALL x. P(x))" +schematic_goal "?p : (ALL x. ~~P(x)) --> ~~(ALL x. P(x))" apply (tactic \IntPr.fast_tac @{context} 1\)? oops (*Classically but not intuitionistically valid. Proved by a bug in 1986!*) -schematic_lemma "?p : EX x. Q(x) --> (ALL x. Q(x))" +schematic_goal "?p : EX x. Q(x) --> (ALL x. Q(x))" apply (tactic \IntPr.fast_tac @{context} 1\)? oops @@ -194,32 +194,32 @@ \ text "Problem ~~18" -schematic_lemma "?p : ~~(EX y. ALL x. P(y)-->P(x))" oops +schematic_goal "?p : ~~(EX y. ALL x. P(y)-->P(x))" oops (*NOT PROVED*) text "Problem ~~19" -schematic_lemma "?p : ~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))" oops +schematic_goal "?p : ~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))" oops (*NOT PROVED*) text "Problem 20" -schematic_lemma "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w))) +schematic_goal "?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 @{context} 1\) text "Problem 21" -schematic_lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))" oops +schematic_goal "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))" oops (*NOT PROVED*) text "Problem 22" -schematic_lemma "?p : (ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))" +schematic_goal "?p : (ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))" by (tactic \IntPr.fast_tac @{context} 1\) text "Problem ~~23" -schematic_lemma "?p : ~~ ((ALL x. P | Q(x)) <-> (P | (ALL x. Q(x))))" +schematic_goal "?p : ~~ ((ALL x. P | Q(x)) <-> (P | (ALL x. Q(x))))" by (tactic \IntPr.fast_tac @{context} 1\) text "Problem 24" -schematic_lemma "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) & +schematic_goal "?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" -schematic_lemma "?p : (EX x. P(x)) & +schematic_goal "?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 @{context} 1") text "Problem 29. Essentially the same as Principia Mathematica *11.71" -schematic_lemma "?p : (EX x. P(x)) & (EX y. Q(y)) +schematic_goal "?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 @{context} 1") text "Problem ~~30" -schematic_lemma "?p : (ALL x. (P(x) | Q(x)) --> ~ R(x)) & +schematic_goal "?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 @{context} 1") text "Problem 31" -schematic_lemma "?p : ~(EX x. P(x) & (Q(x) | R(x))) & +schematic_goal "?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 @{context} 1") text "Problem 32" -schematic_lemma "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & +schematic_goal "?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 @{context} 1") -- slow text "Problem 39" -schematic_lemma "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))" +schematic_goal "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))" by (tactic "IntPr.best_tac @{context} 1") text "Problem 40. AMENDED" -schematic_lemma "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) --> +schematic_goal "?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 @{context} 1") -- slow text "Problem 44" -schematic_lemma "?p : (ALL x. f(x) --> +schematic_goal "?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 @{context} 1") text "Problem 48" -schematic_lemma "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c" +schematic_goal "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c" by (tactic "IntPr.best_tac @{context} 1") text "Problem 51" -schematic_lemma +schematic_goal "?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 @{context} 1") -- \60 seconds\ text "Problem 56" -schematic_lemma "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))" +schematic_goal "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))" by (tactic "IntPr.best_tac @{context} 1") text "Problem 57" -schematic_lemma +schematic_goal "?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 @{context} 1") text "Problem 60" -schematic_lemma "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))" +schematic_goal "?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 @{context} 1") end diff -r fa4ebbd350ae -r 4645502c3c64 src/FOLP/ex/Nat.thy --- a/src/FOLP/ex/Nat.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/FOLP/ex/Nat.thy Tue Oct 06 15:14:28 2015 +0200 @@ -40,7 +40,7 @@ subsection \Proofs about the natural numbers\ -schematic_lemma Suc_n_not_n: "?p : ~ (Suc(k) = k)" +schematic_goal Suc_n_not_n: "?p : ~ (Suc(k) = k)" apply (rule_tac n = k in induct) apply (rule notI) apply (erule Suc_neq_0) @@ -49,7 +49,7 @@ apply (erule Suc_inject) done -schematic_lemma "?p : (k+m)+n = k+(m+n)" +schematic_goal "?p : (k+m)+n = k+(m+n)" apply (rule induct) back back @@ -59,23 +59,23 @@ back oops -schematic_lemma add_0 [simp]: "?p : 0+n = n" +schematic_goal add_0 [simp]: "?p : 0+n = n" apply (unfold add_def) apply (rule rec_0) done -schematic_lemma add_Suc [simp]: "?p : Suc(m)+n = Suc(m+n)" +schematic_goal add_Suc [simp]: "?p : Suc(m)+n = Suc(m+n)" apply (unfold add_def) apply (rule rec_Suc) done -schematic_lemma Suc_cong: "p : x = y \ ?p : Suc(x) = Suc(y)" +schematic_goal Suc_cong: "p : x = y \ ?p : Suc(x) = Suc(y)" apply (erule subst) apply (rule refl) done -schematic_lemma Plus_cong: "[| p : a = x; q: b = y |] ==> ?p : a + b = x + y" +schematic_goal Plus_cong: "[| p : a = x; q: b = y |] ==> ?p : a + b = x + y" apply (erule subst, erule subst, rule refl) done @@ -87,19 +87,19 @@ |> fold (addrew @{context}) @{thms add_0 add_Suc} \ -schematic_lemma add_assoc: "?p : (k+m)+n = k+(m+n)" +schematic_goal add_assoc: "?p : (k+m)+n = k+(m+n)" apply (rule_tac n = k in induct) apply (tactic \SIMP_TAC @{context} add_ss 1\) apply (tactic \ASM_SIMP_TAC @{context} add_ss 1\) done -schematic_lemma add_0_right: "?p : m+0 = m" +schematic_goal add_0_right: "?p : m+0 = m" apply (rule_tac n = m in induct) apply (tactic \SIMP_TAC @{context} add_ss 1\) apply (tactic \ASM_SIMP_TAC @{context} add_ss 1\) done -schematic_lemma add_Suc_right: "?p : m+Suc(n) = Suc(m+n)" +schematic_goal add_Suc_right: "?p : m+Suc(n) = Suc(m+n)" apply (rule_tac n = m in induct) apply (tactic \ALLGOALS (ASM_SIMP_TAC @{context} add_ss)\) done diff -r fa4ebbd350ae -r 4645502c3c64 src/FOLP/ex/Propositional_Cla.thy --- a/src/FOLP/ex/Propositional_Cla.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/FOLP/ex/Propositional_Cla.thy Tue Oct 06 15:14:28 2015 +0200 @@ -11,103 +11,103 @@ text "commutative laws of & and | " -schematic_lemma "?p : P & Q --> Q & P" +schematic_goal "?p : P & Q --> Q & P" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) -schematic_lemma "?p : P | Q --> Q | P" +schematic_goal "?p : P | Q --> Q | P" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) text "associative laws of & and | " -schematic_lemma "?p : (P & Q) & R --> P & (Q & R)" +schematic_goal "?p : (P & Q) & R --> P & (Q & R)" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) -schematic_lemma "?p : (P | Q) | R --> P | (Q | R)" +schematic_goal "?p : (P | Q) | R --> P | (Q | R)" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) text "distributive laws of & and | " -schematic_lemma "?p : (P & Q) | R --> (P | R) & (Q | R)" +schematic_goal "?p : (P & Q) | R --> (P | R) & (Q | R)" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) -schematic_lemma "?p : (P | R) & (Q | R) --> (P & Q) | R" +schematic_goal "?p : (P | R) & (Q | R) --> (P & Q) | R" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) -schematic_lemma "?p : (P | Q) & R --> (P & R) | (Q & R)" +schematic_goal "?p : (P | Q) & R --> (P & R) | (Q & R)" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) -schematic_lemma "?p : (P & R) | (Q & R) --> (P | Q) & R" +schematic_goal "?p : (P & R) | (Q & R) --> (P | Q) & R" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) text "Laws involving implication" -schematic_lemma "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)" +schematic_goal "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) -schematic_lemma "?p : (P & Q --> R) <-> (P--> (Q-->R))" +schematic_goal "?p : (P & Q --> R) <-> (P--> (Q-->R))" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) -schematic_lemma "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R" +schematic_goal "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) -schematic_lemma "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)" +schematic_goal "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) -schematic_lemma "?p : (P --> Q & R) <-> (P-->Q) & (P-->R)" +schematic_goal "?p : (P --> Q & R) <-> (P-->Q) & (P-->R)" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) text "Propositions-as-types" (*The combinator K*) -schematic_lemma "?p : P --> (Q --> P)" +schematic_goal "?p : P --> (Q --> P)" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) (*The combinator S*) -schematic_lemma "?p : (P-->Q-->R) --> (P-->Q) --> (P-->R)" +schematic_goal "?p : (P-->Q-->R) --> (P-->Q) --> (P-->R)" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) (*Converse is classical*) -schematic_lemma "?p : (P-->Q) | (P-->R) --> (P --> Q | R)" +schematic_goal "?p : (P-->Q) | (P-->R) --> (P --> Q | R)" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) -schematic_lemma "?p : (P-->Q) --> (~Q --> ~P)" +schematic_goal "?p : (P-->Q) --> (~Q --> ~P)" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) text "Schwichtenberg's examples (via T. Nipkow)" -schematic_lemma stab_imp: "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q" +schematic_goal stab_imp: "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) -schematic_lemma stab_to_peirce: "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q) +schematic_goal stab_to_peirce: "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q) --> ((P --> Q) --> P) --> P" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) -schematic_lemma peirce_imp1: "?p : (((Q --> R) --> Q) --> Q) +schematic_goal peirce_imp1: "?p : (((Q --> R) --> Q) --> Q) --> (((P --> Q) --> R) --> P --> Q) --> P --> Q" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) -schematic_lemma peirce_imp2: "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P" +schematic_goal peirce_imp2: "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) -schematic_lemma mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q" +schematic_goal mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) -schematic_lemma mints_solovev: "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R" +schematic_goal mints_solovev: "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) -schematic_lemma tatsuta: "?p : (((P7 --> P1) --> P10) --> P4 --> P5) +schematic_goal 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 @{context} FOLP_cs 1\) -schematic_lemma tatsuta1: "?p : (((P8 --> P2) --> P9) --> P3 --> P10) +schematic_goal tatsuta1: "?p : (((P8 --> P2) --> P9) --> P3 --> P10) --> (((P3 --> P2) --> P9) --> P4) --> (((P6 --> P1) --> P2) --> P9) --> (((P7 --> P1) --> P10) --> P4 --> P5) diff -r fa4ebbd350ae -r 4645502c3c64 src/FOLP/ex/Propositional_Int.thy --- a/src/FOLP/ex/Propositional_Int.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/FOLP/ex/Propositional_Int.thy Tue Oct 06 15:14:28 2015 +0200 @@ -11,103 +11,103 @@ text "commutative laws of & and | " -schematic_lemma "?p : P & Q --> Q & P" +schematic_goal "?p : P & Q --> Q & P" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma "?p : P | Q --> Q | P" +schematic_goal "?p : P | Q --> Q | P" by (tactic \IntPr.fast_tac @{context} 1\) text "associative laws of & and | " -schematic_lemma "?p : (P & Q) & R --> P & (Q & R)" +schematic_goal "?p : (P & Q) & R --> P & (Q & R)" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma "?p : (P | Q) | R --> P | (Q | R)" +schematic_goal "?p : (P | Q) | R --> P | (Q | R)" by (tactic \IntPr.fast_tac @{context} 1\) text "distributive laws of & and | " -schematic_lemma "?p : (P & Q) | R --> (P | R) & (Q | R)" +schematic_goal "?p : (P & Q) | R --> (P | R) & (Q | R)" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma "?p : (P | R) & (Q | R) --> (P & Q) | R" +schematic_goal "?p : (P | R) & (Q | R) --> (P & Q) | R" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma "?p : (P | Q) & R --> (P & R) | (Q & R)" +schematic_goal "?p : (P | Q) & R --> (P & R) | (Q & R)" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma "?p : (P & R) | (Q & R) --> (P | Q) & R" +schematic_goal "?p : (P & R) | (Q & R) --> (P | Q) & R" by (tactic \IntPr.fast_tac @{context} 1\) text "Laws involving implication" -schematic_lemma "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)" +schematic_goal "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma "?p : (P & Q --> R) <-> (P--> (Q-->R))" +schematic_goal "?p : (P & Q --> R) <-> (P--> (Q-->R))" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R" +schematic_goal "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)" +schematic_goal "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma "?p : (P --> Q & R) <-> (P-->Q) & (P-->R)" +schematic_goal "?p : (P --> Q & R) <-> (P-->Q) & (P-->R)" by (tactic \IntPr.fast_tac @{context} 1\) text "Propositions-as-types" (*The combinator K*) -schematic_lemma "?p : P --> (Q --> P)" +schematic_goal "?p : P --> (Q --> P)" by (tactic \IntPr.fast_tac @{context} 1\) (*The combinator S*) -schematic_lemma "?p : (P-->Q-->R) --> (P-->Q) --> (P-->R)" +schematic_goal "?p : (P-->Q-->R) --> (P-->Q) --> (P-->R)" by (tactic \IntPr.fast_tac @{context} 1\) (*Converse is classical*) -schematic_lemma "?p : (P-->Q) | (P-->R) --> (P --> Q | R)" +schematic_goal "?p : (P-->Q) | (P-->R) --> (P --> Q | R)" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma "?p : (P-->Q) --> (~Q --> ~P)" +schematic_goal "?p : (P-->Q) --> (~Q --> ~P)" by (tactic \IntPr.fast_tac @{context} 1\) text "Schwichtenberg's examples (via T. Nipkow)" -schematic_lemma stab_imp: "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q" +schematic_goal stab_imp: "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma stab_to_peirce: "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q) +schematic_goal stab_to_peirce: "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q) --> ((P --> Q) --> P) --> P" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma peirce_imp1: "?p : (((Q --> R) --> Q) --> Q) +schematic_goal peirce_imp1: "?p : (((Q --> R) --> Q) --> Q) --> (((P --> Q) --> R) --> P --> Q) --> P --> Q" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma peirce_imp2: "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P" +schematic_goal peirce_imp2: "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q" +schematic_goal mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma mints_solovev: "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R" +schematic_goal mints_solovev: "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma tatsuta: "?p : (((P7 --> P1) --> P10) --> P4 --> P5) +schematic_goal 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 @{context} 1\) -schematic_lemma tatsuta1: "?p : (((P8 --> P2) --> P9) --> P3 --> P10) +schematic_goal tatsuta1: "?p : (((P8 --> P2) --> P9) --> P3 --> P10) --> (((P3 --> P2) --> P9) --> P4) --> (((P6 --> P1) --> P2) --> P9) --> (((P7 --> P1) --> P10) --> P4 --> P5) diff -r fa4ebbd350ae -r 4645502c3c64 src/FOLP/ex/Quantifiers_Cla.thy --- a/src/FOLP/ex/Quantifiers_Cla.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/FOLP/ex/Quantifiers_Cla.thy Tue Oct 06 15:14:28 2015 +0200 @@ -10,92 +10,92 @@ imports FOLP begin -schematic_lemma "?p : (ALL x y. P(x,y)) --> (ALL y x. P(x,y))" +schematic_goal "?p : (ALL x y. P(x,y)) --> (ALL y x. P(x,y))" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) -schematic_lemma "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))" +schematic_goal "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) (*Converse is false*) -schematic_lemma "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))" +schematic_goal "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) -schematic_lemma "?p : (ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))" +schematic_goal "?p : (ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) -schematic_lemma "?p : (ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)" +schematic_goal "?p : (ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) text "Some harder ones" -schematic_lemma "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))" +schematic_goal "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) (*Converse is false*) -schematic_lemma "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x)) & (EX x. Q(x))" +schematic_goal "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x)) & (EX x. Q(x))" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) text "Basic test of quantifier reasoning" (*TRUE*) -schematic_lemma "?p : (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))" +schematic_goal "?p : (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) -schematic_lemma "?p : (ALL x. Q(x)) --> (EX x. Q(x))" +schematic_goal "?p : (ALL x. Q(x)) --> (EX x. Q(x))" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) text "The following should fail, as they are false!" -schematic_lemma "?p : (ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))" +schematic_goal "?p : (ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))" apply (tactic \Cla.fast_tac @{context} FOLP_cs 1\)? oops -schematic_lemma "?p : (EX x. Q(x)) --> (ALL x. Q(x))" +schematic_goal "?p : (EX x. Q(x)) --> (ALL x. Q(x))" apply (tactic \Cla.fast_tac @{context} FOLP_cs 1\)? oops -schematic_lemma "?p : P(?a) --> (ALL x. P(x))" +schematic_goal "?p : P(?a) --> (ALL x. P(x))" apply (tactic \Cla.fast_tac @{context} FOLP_cs 1\)? oops -schematic_lemma "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))" +schematic_goal "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))" apply (tactic \Cla.fast_tac @{context} FOLP_cs 1\)? oops text "Back to things that are provable..." -schematic_lemma "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))" +schematic_goal "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) (*An example of why exI should be delayed as long as possible*) -schematic_lemma "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))" +schematic_goal "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) -schematic_lemma "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)" +schematic_goal "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) -schematic_lemma "?p : (ALL x. Q(x)) --> (EX x. Q(x))" +schematic_goal "?p : (ALL x. Q(x)) --> (EX x. Q(x))" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) text "Some slow ones" (*Principia Mathematica *11.53 *) -schematic_lemma "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))" +schematic_goal "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) (*Principia Mathematica *11.55 *) -schematic_lemma "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))" +schematic_goal "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) (*Principia Mathematica *11.61 *) -schematic_lemma "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))" +schematic_goal "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))" by (tactic \Cla.fast_tac @{context} FOLP_cs 1\) end diff -r fa4ebbd350ae -r 4645502c3c64 src/FOLP/ex/Quantifiers_Int.thy --- a/src/FOLP/ex/Quantifiers_Int.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/FOLP/ex/Quantifiers_Int.thy Tue Oct 06 15:14:28 2015 +0200 @@ -10,92 +10,92 @@ imports IFOLP begin -schematic_lemma "?p : (ALL x y. P(x,y)) --> (ALL y x. P(x,y))" +schematic_goal "?p : (ALL x y. P(x,y)) --> (ALL y x. P(x,y))" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))" +schematic_goal "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))" by (tactic \IntPr.fast_tac @{context} 1\) (*Converse is false*) -schematic_lemma "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))" +schematic_goal "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma "?p : (ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))" +schematic_goal "?p : (ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma "?p : (ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)" +schematic_goal "?p : (ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)" by (tactic \IntPr.fast_tac @{context} 1\) text "Some harder ones" -schematic_lemma "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))" +schematic_goal "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))" by (tactic \IntPr.fast_tac @{context} 1\) (*Converse is false*) -schematic_lemma "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x)) & (EX x. Q(x))" +schematic_goal "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x)) & (EX x. Q(x))" by (tactic \IntPr.fast_tac @{context} 1\) text "Basic test of quantifier reasoning" (*TRUE*) -schematic_lemma "?p : (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))" +schematic_goal "?p : (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma "?p : (ALL x. Q(x)) --> (EX x. Q(x))" +schematic_goal "?p : (ALL x. Q(x)) --> (EX x. Q(x))" by (tactic \IntPr.fast_tac @{context} 1\) text "The following should fail, as they are false!" -schematic_lemma "?p : (ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))" +schematic_goal "?p : (ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))" apply (tactic \IntPr.fast_tac @{context} 1\)? oops -schematic_lemma "?p : (EX x. Q(x)) --> (ALL x. Q(x))" +schematic_goal "?p : (EX x. Q(x)) --> (ALL x. Q(x))" apply (tactic \IntPr.fast_tac @{context} 1\)? oops -schematic_lemma "?p : P(?a) --> (ALL x. P(x))" +schematic_goal "?p : P(?a) --> (ALL x. P(x))" apply (tactic \IntPr.fast_tac @{context} 1\)? oops -schematic_lemma "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))" +schematic_goal "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))" apply (tactic \IntPr.fast_tac @{context} 1\)? oops text "Back to things that are provable..." -schematic_lemma "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))" +schematic_goal "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))" by (tactic \IntPr.fast_tac @{context} 1\) (*An example of why exI should be delayed as long as possible*) -schematic_lemma "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))" +schematic_goal "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)" +schematic_goal "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)" by (tactic \IntPr.fast_tac @{context} 1\) -schematic_lemma "?p : (ALL x. Q(x)) --> (EX x. Q(x))" +schematic_goal "?p : (ALL x. Q(x)) --> (EX x. Q(x))" by (tactic \IntPr.fast_tac @{context} 1\) text "Some slow ones" (*Principia Mathematica *11.53 *) -schematic_lemma "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))" +schematic_goal "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))" by (tactic \IntPr.fast_tac @{context} 1\) (*Principia Mathematica *11.55 *) -schematic_lemma "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))" +schematic_goal "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))" by (tactic \IntPr.fast_tac @{context} 1\) (*Principia Mathematica *11.61 *) -schematic_lemma "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))" +schematic_goal "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))" by (tactic \IntPr.fast_tac @{context} 1\) end diff -r fa4ebbd350ae -r 4645502c3c64 src/HOL/Bali/Example.thy --- a/src/HOL/Bali/Example.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/HOL/Bali/Example.thy Tue Oct 06 15:14:28 2015 +0200 @@ -1078,7 +1078,7 @@ subsubsection "well-typedness" -schematic_lemma wt_test: "\prg=tprg,cls=Main,lcl=empty(VName e\Class Base)\\test ?pTs\\" +schematic_goal 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 (* ;; *)) @@ -1130,7 +1130,7 @@ subsubsection "definite assignment" -schematic_lemma da_test: "\prg=tprg,cls=Main,lcl=empty(VName e\Class Base)\ +schematic_goal 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) @@ -1248,7 +1248,7 @@ declare Pair_eq [simp del] -schematic_lemma exec_test: +schematic_goal exec_test: "\the (new_Addr (heap s1)) = a; the (new_Addr (heap ?s2)) = b; the (new_Addr (heap ?s3)) = c\ \ diff -r fa4ebbd350ae -r 4645502c3c64 src/HOL/Eisbach/Tests.thy --- a/src/HOL/Eisbach/Tests.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/HOL/Eisbach/Tests.thy Tue Oct 06 15:14:28 2015 +0200 @@ -224,7 +224,7 @@ by retrofitting. This needs to be done more carefully to avoid smashing legitimate pairs.*) -schematic_lemma "?A x \ A x" +schematic_goal "?A x \ A x" apply (match conclusion in "H" for H \ \match conclusion in Y for Y \ \print_term Y\\) apply assumption done diff -r fa4ebbd350ae -r 4645502c3c64 src/HOL/Groups.thy --- a/src/HOL/Groups.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/HOL/Groups.thy Tue Oct 06 15:14:28 2015 +0200 @@ -147,13 +147,13 @@ declare add.left_commute [algebra_simps, field_simps] -theorems add_ac = add.assoc add.commute add.left_commute +lemmas add_ac = add.assoc add.commute add.left_commute end hide_fact add_commute -theorems add_ac = add.assoc add.commute add.left_commute +lemmas add_ac = add.assoc add.commute add.left_commute class semigroup_mult = times + assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)" @@ -175,13 +175,13 @@ declare mult.left_commute [algebra_simps, field_simps] -theorems mult_ac = mult.assoc mult.commute mult.left_commute +lemmas mult_ac = mult.assoc mult.commute mult.left_commute end hide_fact mult_commute -theorems mult_ac = mult.assoc mult.commute mult.left_commute +lemmas mult_ac = mult.assoc mult.commute mult.left_commute class monoid_add = zero + semigroup_add + assumes add_0_left: "0 + a = a" diff -r fa4ebbd350ae -r 4645502c3c64 src/HOL/Hahn_Banach/Vector_Space.thy --- a/src/HOL/Hahn_Banach/Vector_Space.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/HOL/Hahn_Banach/Vector_Space.thy Tue Oct 06 15:14:28 2015 +0200 @@ -75,7 +75,7 @@ finally show ?thesis . qed -theorems add_ac = add_assoc add_commute add_left_commute +lemmas add_ac = add_assoc add_commute add_left_commute text \The existence of the zero element of a vector space diff -r fa4ebbd350ae -r 4645502c3c64 src/HOL/IMP/Big_Step.thy --- a/src/HOL/IMP/Big_Step.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/HOL/IMP/Big_Step.thy Tue Oct 06 15:14:28 2015 +0200 @@ -26,7 +26,7 @@ text_raw{*}%endsnip*} text_raw{*\snip{BigStepEx}{1}{2}{% *} -schematic_lemma ex: "(''x'' ::= N 5;; ''y'' ::= V ''x'', s) \ ?t" +schematic_goal ex: "(''x'' ::= N 5;; ''y'' ::= V ''x'', s) \ ?t" apply(rule Seq) apply(rule Assign) apply simp diff -r fa4ebbd350ae -r 4645502c3c64 src/HOL/Inductive.thy --- a/src/HOL/Inductive.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/HOL/Inductive.thy Tue Oct 06 15:14:28 2015 +0200 @@ -343,13 +343,13 @@ text \Package setup.\ -theorems basic_monos = +lemmas basic_monos = subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj Collect_mono in_mono vimage_mono ML_file "Tools/inductive.ML" -theorems [mono] = +lemmas [mono] = imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj imp_mono not_mono Ball_def Bex_def diff -r fa4ebbd350ae -r 4645502c3c64 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/HOL/Library/Multiset.thy Tue Oct 06 15:14:28 2015 +0200 @@ -2544,7 +2544,7 @@ using rel_mset_imp_rel_mset' rel_mset'_imp_rel_mset by auto text \The main end product for @{const rel_mset}: inductive characterization:\ -theorems rel_mset_induct[case_names empty add, induct pred: rel_mset] = +lemmas rel_mset_induct[case_names empty add, induct pred: rel_mset] = rel_mset'.induct[unfolded rel_mset_rel_mset'[symmetric]] diff -r fa4ebbd350ae -r 4645502c3c64 src/HOL/Library/Omega_Words_Fun.thy --- a/src/HOL/Library/Omega_Words_Fun.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/HOL/Library/Omega_Words_Fun.thy Tue Oct 06 15:14:28 2015 +0200 @@ -560,7 +560,7 @@ thus ?thesis .. qed -theorems limit_is_suffixE = limit_is_suffix[THEN exE] +lemmas limit_is_suffixE = limit_is_suffix[THEN exE] text \ diff -r fa4ebbd350ae -r 4645502c3c64 src/HOL/Library/Prefix_Order.thy --- a/src/HOL/Library/Prefix_Order.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/HOL/Library/Prefix_Order.thy Tue Oct 06 15:14:28 2015 +0200 @@ -25,15 +25,15 @@ lemmas strict_prefixE' [elim?] = prefixE' [folded less_list_def] lemmas strict_prefixI [intro?] = prefixI [folded less_list_def] lemmas strict_prefixE [elim?] = prefixE [folded less_list_def] -theorems Nil_prefix [iff] = Nil_prefixeq [folded less_eq_list_def] -theorems prefix_Nil [simp] = prefixeq_Nil [folded less_eq_list_def] +lemmas Nil_prefix [iff] = Nil_prefixeq [folded less_eq_list_def] +lemmas prefix_Nil [simp] = prefixeq_Nil [folded less_eq_list_def] lemmas prefix_snoc [simp] = prefixeq_snoc [folded less_eq_list_def] lemmas Cons_prefix_Cons [simp] = Cons_prefixeq_Cons [folded less_eq_list_def] lemmas same_prefix_prefix [simp] = same_prefixeq_prefixeq [folded less_eq_list_def] lemmas same_prefix_nil [iff] = same_prefixeq_nil [folded less_eq_list_def] lemmas prefix_prefix [simp] = prefixeq_prefixeq [folded less_eq_list_def] -theorems prefix_Cons = prefixeq_Cons [folded less_eq_list_def] -theorems prefix_length_le = prefixeq_length_le [folded less_eq_list_def] +lemmas prefix_Cons = prefixeq_Cons [folded less_eq_list_def] +lemmas prefix_length_le = prefixeq_length_le [folded less_eq_list_def] lemmas strict_prefix_simps [simp, code] = prefix_simps [folded less_list_def] lemmas not_prefix_induct [consumes 1, case_names Nil Neq Eq] = not_prefixeq_induct [folded less_eq_list_def] diff -r fa4ebbd350ae -r 4645502c3c64 src/HOL/Library/Set_Algebras.thy --- a/src/HOL/Library/Set_Algebras.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/HOL/Library/Set_Algebras.thy Tue Oct 06 15:14:28 2015 +0200 @@ -127,7 +127,7 @@ apply (auto simp add: ac_simps) done -theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2 +lemmas set_plus_rearranges = set_plus_rearrange set_plus_rearrange2 set_plus_rearrange3 set_plus_rearrange4 lemma set_plus_mono [intro!]: "C \ D \ a +o C \ a +o D" @@ -237,7 +237,7 @@ apply (auto simp add: ac_simps) done -theorems set_times_rearranges = set_times_rearrange set_times_rearrange2 +lemmas set_times_rearranges = set_times_rearrange set_times_rearrange2 set_times_rearrange3 set_times_rearrange4 lemma set_times_mono [intro]: "C \ D \ a *o C \ a *o D" @@ -303,7 +303,7 @@ apply auto done -theorems set_times_plus_distribs = +lemmas set_times_plus_distribs = set_times_plus_distrib set_times_plus_distrib2 diff -r fa4ebbd350ae -r 4645502c3c64 src/HOL/MicroJava/J/Example.thy --- a/src/HOL/MicroJava/J/Example.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/HOL/MicroJava/J/Example.thy Tue Oct 06 15:14:28 2015 +0200 @@ -373,7 +373,7 @@ done lemmas t = ty_expr_ty_exprs_wt_stmt.intros -schematic_lemma wt_test: "(tprg, empty(e\Class Base))\ +schematic_goal wt_test: "(tprg, empty(e\Class Base))\ Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\" apply (rule ty_expr_ty_exprs_wt_stmt.intros) -- ";;" apply (rule t) -- "Expr" @@ -402,7 +402,7 @@ lemmas e = NewCI eval_evals_exec.intros declare split_if [split del] declare init_vars_def [simp] c_hupd_def [simp] cast_ok_def [simp] -schematic_lemma exec_test: +schematic_goal exec_test: " [|new_Addr (heap (snd s0)) = (a, None)|] ==> tprg\s0 -test-> ?s" apply (unfold test_def) diff -r fa4ebbd350ae -r 4645502c3c64 src/HOL/Nitpick_Examples/Core_Nits.thy --- a/src/HOL/Nitpick_Examples/Core_Nits.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Tue Oct 06 15:14:28 2015 +0200 @@ -266,27 +266,27 @@ subsection {* Schematic Variables *} -schematic_lemma "x = ?x" +schematic_goal "x = ?x" nitpick [expect = none] by auto -schematic_lemma "\x. x = ?x" +schematic_goal "\x. x = ?x" nitpick [expect = genuine] oops -schematic_lemma "\x. x = ?x" +schematic_goal "\x. x = ?x" nitpick [expect = none] by auto -schematic_lemma "\x::'a \ 'b. x = ?x" +schematic_goal "\x::'a \ 'b. x = ?x" nitpick [expect = none] by auto -schematic_lemma "\x. ?x = ?y" +schematic_goal "\x. ?x = ?y" nitpick [expect = none] by auto -schematic_lemma "\x. ?x = ?y" +schematic_goal "\x. ?x = ?y" nitpick [expect = none] by auto diff -r fa4ebbd350ae -r 4645502c3c64 src/HOL/Nitpick_Examples/Refute_Nits.thy --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Tue Oct 06 15:14:28 2015 +0200 @@ -340,12 +340,12 @@ subsubsection {* Schematic Variables *} -schematic_lemma "?P" +schematic_goal "?P" nitpick [expect = none] apply auto done -schematic_lemma "x = ?y" +schematic_goal "x = ?y" nitpick [expect = none] apply auto done diff -r fa4ebbd350ae -r 4645502c3c64 src/HOL/Prolog/Func.thy --- a/src/HOL/Prolog/Func.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/HOL/Prolog/Func.thy Tue Oct 06 15:14:28 2015 +0200 @@ -58,11 +58,11 @@ lemmas prog_Func = eval -schematic_lemma "eval ((S (S Z)) + (S Z)) ?X" +schematic_goal "eval ((S (S Z)) + (S Z)) ?X" apply (prolog prog_Func) done -schematic_lemma "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z) +schematic_goal "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 fa4ebbd350ae -r 4645502c3c64 src/HOL/Prolog/Test.thy --- a/src/HOL/Prolog/Test.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/HOL/Prolog/Test.thy Tue Oct 06 15:14:28 2015 +0200 @@ -80,7 +80,7 @@ lemmas prog_Test = append reverse mappred mapfun age eq bag_appl -schematic_lemma "append ?x ?y [a,b,c,d]" +schematic_goal "append ?x ?y [a,b,c,d]" apply (prolog prog_Test) back back @@ -88,56 +88,56 @@ back done -schematic_lemma "append [a,b] y ?L" +schematic_goal "append [a,b] y ?L" apply (prolog prog_Test) done -schematic_lemma "!y. append [a,b] y (?L y)" +schematic_goal "!y. append [a,b] y (?L y)" apply (prolog prog_Test) done -schematic_lemma "reverse [] ?L" +schematic_goal "reverse [] ?L" apply (prolog prog_Test) done -schematic_lemma "reverse [23] ?L" +schematic_goal "reverse [23] ?L" apply (prolog prog_Test) done -schematic_lemma "reverse [23,24,?x] ?L" +schematic_goal "reverse [23,24,?x] ?L" apply (prolog prog_Test) done -schematic_lemma "reverse ?L [23,24,?x]" +schematic_goal "reverse ?L [23,24,?x]" apply (prolog prog_Test) done -schematic_lemma "mappred age ?x [23,24]" +schematic_goal "mappred age ?x [23,24]" apply (prolog prog_Test) back done -schematic_lemma "mappred (%x y. ? z. age z y) ?x [23,24]" +schematic_goal "mappred (%x y. ? z. age z y) ?x [23,24]" apply (prolog prog_Test) done -schematic_lemma "mappred ?P [bob,sue] [24,23]" +schematic_goal "mappred ?P [bob,sue] [24,23]" apply (prolog prog_Test) done -schematic_lemma "mapfun f [bob,bob,sue] [?x,?y,?z]" +schematic_goal "mapfun f [bob,bob,sue] [?x,?y,?z]" apply (prolog prog_Test) done -schematic_lemma "mapfun (%x. h x 25) [bob,sue] ?L" +schematic_goal "mapfun (%x. h x 25) [bob,sue] ?L" apply (prolog prog_Test) done -schematic_lemma "mapfun ?F [24,25] [h bob 24,h bob 25]" +schematic_goal "mapfun ?F [24,25] [h bob 24,h bob 25]" apply (prolog prog_Test) done -schematic_lemma "mapfun ?F [24] [h 24 24]" +schematic_goal "mapfun ?F [24] [h 24 24]" apply (prolog prog_Test) back back @@ -148,12 +148,12 @@ apply (prolog prog_Test) done -schematic_lemma "age ?x 24 & age ?y 23" +schematic_goal "age ?x 24 & age ?y 23" apply (prolog prog_Test) back done -schematic_lemma "age ?x 24 | age ?x 23" +schematic_goal "age ?x 24 | age ?x 23" apply (prolog prog_Test) back back @@ -167,7 +167,7 @@ apply (prolog prog_Test) done -schematic_lemma "age sue 24 .. age bob 23 => age ?x ?y" +schematic_goal "age sue 24 .. age bob 23 => age ?x ?y" apply (prolog prog_Test) back back @@ -181,7 +181,7 @@ done (*reset trace_DEPTH_FIRST;*) -schematic_lemma "(!x. age x 25 :- age x 23) => age ?x 25 & age ?y 25" +schematic_goal "(!x. age x 25 :- age x 23) => age ?x 25 & age ?y 25" apply (prolog prog_Test) back back @@ -192,7 +192,7 @@ apply (prolog prog_Test) done -schematic_lemma "? P. P & eq P ?x" +schematic_goal "? P. P & eq P ?x" apply (prolog prog_Test) (* back @@ -247,14 +247,14 @@ by fast *) -schematic_lemma "!Emp Stk.( +schematic_goal "!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 -schematic_lemma "!Qu. ( +schematic_goal "!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))) @@ -265,7 +265,7 @@ apply (prolog prog_Test) done -schematic_lemma "P x .. P y => P ?X" +schematic_goal "P x .. P y => P ?X" apply (prolog prog_Test) back done diff -r fa4ebbd350ae -r 4645502c3c64 src/HOL/Prolog/Type.thy --- a/src/HOL/Prolog/Type.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/HOL/Prolog/Type.thy Tue Oct 06 15:14:28 2015 +0200 @@ -46,41 +46,41 @@ lemmas prog_Type = prog_Func good_typeof common_typeof -schematic_lemma "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T" +schematic_goal "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T" apply (prolog prog_Type) done -schematic_lemma "typeof (fix (%x. x)) ?T" +schematic_goal "typeof (fix (%x. x)) ?T" apply (prolog prog_Type) done -schematic_lemma "typeof (fix (%fact. abs(%n. (app fact (n - Z))))) ?T" +schematic_goal "typeof (fix (%fact. abs(%n. (app fact (n - Z))))) ?T" apply (prolog prog_Type) done -schematic_lemma "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z) +schematic_goal "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z) (n * (app fact (n - (S Z))))))) ?T" apply (prolog prog_Type) done -schematic_lemma "typeof (abs(%v. Z)) ?T" (*correct only solution (?A1 -> nat) *) +schematic_goal "typeof (abs(%v. Z)) ?T" (*correct only solution (?A1 -> nat) *) apply (prolog prog_Type) done -schematic_lemma "typeof (abs(%v. Z)) ?T" +schematic_goal "typeof (abs(%v. Z)) ?T" apply (prolog bad1_typeof common_typeof) (* 1st result ok*) done -schematic_lemma "typeof (abs(%v. Z)) ?T" +schematic_goal "typeof (abs(%v. Z)) ?T" apply (prolog bad1_typeof common_typeof) back (* 2nd result (?A1 -> ?A1) wrong *) done -schematic_lemma "typeof (abs(%v. abs(%v. app v v))) ?T" +schematic_goal "typeof (abs(%v. abs(%v. app v v))) ?T" apply (prolog prog_Type)? (*correctly fails*) oops -schematic_lemma "typeof (abs(%v. abs(%v. app v v))) ?T" +schematic_goal "typeof (abs(%v. abs(%v. app v v))) ?T" apply (prolog bad2_typeof common_typeof) (* wrong result ((?A3 -> ?B3) -> ?A3 -> ?B3)*) done diff -r fa4ebbd350ae -r 4645502c3c64 src/HOL/Proofs/Lambda/LambdaType.thy --- a/src/HOL/Proofs/Lambda/LambdaType.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/HOL/Proofs/Lambda/LambdaType.thy Tue Oct 06 15:14:28 2015 +0200 @@ -77,10 +77,10 @@ subsection {* Some examples *} -schematic_lemma "e \ Abs (Abs (Abs (Var 1 \ (Var 2 \ Var 1 \ Var 0)))) : ?T" +schematic_goal "e \ Abs (Abs (Abs (Var 1 \ (Var 2 \ Var 1 \ Var 0)))) : ?T" by force -schematic_lemma "e \ Abs (Abs (Abs (Var 2 \ Var 0 \ (Var 1 \ Var 0)))) : ?T" +schematic_goal "e \ Abs (Abs (Abs (Var 2 \ Var 0 \ (Var 1 \ Var 0)))) : ?T" by force diff -r fa4ebbd350ae -r 4645502c3c64 src/HOL/Wellfounded.thy --- a/src/HOL/Wellfounded.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/HOL/Wellfounded.thy Tue Oct 06 15:14:28 2015 +0200 @@ -558,7 +558,7 @@ apply fast done -theorems accp_induct_rule = accp_induct [rule_format, induct set: accp] +lemmas accp_induct_rule = accp_induct [rule_format, induct set: accp] theorem accp_downward: "accp r b ==> r a b ==> accp r a" apply (erule accp.cases) diff -r fa4ebbd350ae -r 4645502c3c64 src/HOL/ex/Classical.thy --- a/src/HOL/ex/Classical.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/HOL/ex/Classical.thy Tue Oct 06 15:14:28 2015 +0200 @@ -348,7 +348,7 @@ text{*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988). fast DISCOVERS who killed Agatha. *} -schematic_lemma "lives(agatha) & lives(butler) & lives(charles) & +schematic_goal "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 fa4ebbd350ae -r 4645502c3c64 src/HOL/ex/Groebner_Examples.thy --- a/src/HOL/ex/Groebner_Examples.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/HOL/ex/Groebner_Examples.thy Tue Oct 06 15:14:28 2015 +0200 @@ -24,7 +24,7 @@ (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv @{context})))) *}) by (rule refl) -schematic_lemma +schematic_goal fixes x :: int shows "(x - (-2))^5 * (y - 78) ^ 8 = ?X" apply (tactic {* ALLGOALS (CONVERSION diff -r fa4ebbd350ae -r 4645502c3c64 src/HOL/ex/Refute_Examples.thy --- a/src/HOL/ex/Refute_Examples.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/HOL/ex/Refute_Examples.thy Tue Oct 06 15:14:28 2015 +0200 @@ -332,11 +332,11 @@ subsubsection {* Schematic variables *} -schematic_lemma "?P" +schematic_goal "?P" refute [expect = none] by auto -schematic_lemma "x = ?y" +schematic_goal "x = ?y" refute [expect = none] by auto diff -r fa4ebbd350ae -r 4645502c3c64 src/HOL/ex/Set_Comprehension_Pointfree_Examples.thy --- a/src/HOL/ex/Set_Comprehension_Pointfree_Examples.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/HOL/ex/Set_Comprehension_Pointfree_Examples.thy Tue Oct 06 15:14:28 2015 +0200 @@ -111,7 +111,7 @@ using assms by (auto intro!: finite_vimageI simp add: inj_on_def) (* injectivity to be automated with further rules and automation *) -schematic_lemma (* check interaction with schematics *) +schematic_goal (* check interaction with schematics *) "finite {x :: ?'A \ ?'B \ bool. \a b. x = Pair_Rep a b} = finite ((\(b :: ?'B, a:: ?'A). Pair_Rep a b) ` (UNIV \ UNIV))" by simp diff -r fa4ebbd350ae -r 4645502c3c64 src/HOL/ex/Set_Theory.thy --- a/src/HOL/ex/Set_Theory.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/HOL/ex/Set_Theory.thy Tue Oct 06 15:14:28 2015 +0200 @@ -27,7 +27,7 @@ Trivial example of term synthesis: apparently hard for some provers! *} -schematic_lemma "a \ b \ a \ ?X \ b \ ?X" +schematic_goal "a \ b \ a \ ?X \ b \ ?X" by blast @@ -61,15 +61,15 @@ -- {* Requires best-first search because it is undirectional. *} by best -schematic_lemma "\f:: 'a \ 'a set. \x. f x \ ?S f" +schematic_goal "\f:: 'a \ 'a set. \x. f x \ ?S f" -- {*This form displays the diagonal term. *} by best -schematic_lemma "?S \ range (f :: 'a \ 'a set)" +schematic_goal "?S \ range (f :: 'a \ 'a set)" -- {* This form exploits the set constructs. *} by (rule notI, erule rangeE, best) -schematic_lemma "?S \ range (f :: 'a \ 'a set)" +schematic_goal "?S \ range (f :: 'a \ 'a set)" -- {* Or just this! *} by best diff -r fa4ebbd350ae -r 4645502c3c64 src/HOL/ex/Simproc_Tests.thy --- a/src/HOL/ex/Simproc_Tests.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/HOL/ex/Simproc_Tests.thy Tue Oct 06 15:14:28 2015 +0200 @@ -41,7 +41,7 @@ } end -schematic_lemma "\(y::?'b::size). size (?x::?'a::size) \ size y + size ?x" +schematic_goal "\(y::?'b::size). size (?x::?'a::size) \ size y + size ?x" by (tactic {* test @{context} [@{simproc natle_cancel_sums}] *}) (rule le0) (* TODO: test more simprocs with schematic variables *) diff -r fa4ebbd350ae -r 4645502c3c64 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Tue Oct 06 13:31:44 2015 +0200 +++ b/src/Pure/Isar/isar_syn.ML Tue Oct 06 15:14:28 2015 +0200 @@ -152,15 +152,10 @@ (* theorems *) -val theorems = - Parse_Spec.name_facts -- Parse.for_fixes - >> (fn (facts, fixes) => #2 oo Specification.theorems_cmd Thm.theoremK facts fixes); - val _ = - Outer_Syntax.local_theory' @{command_keyword theorems} "define theorems" theorems; - -val _ = - Outer_Syntax.local_theory' @{command_keyword lemmas} "define lemmas" theorems; + Outer_Syntax.local_theory' @{command_keyword lemmas} "define theorems" + (Parse_Spec.name_facts -- Parse.for_fixes >> + (fn (facts, fixes) => #2 oo Specification.theorems_cmd Thm.theoremK facts fixes)); val _ = Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems" @@ -507,9 +502,7 @@ val _ = theorem @{command_keyword theorem} false "theorem"; val _ = theorem @{command_keyword lemma} false "lemma"; val _ = theorem @{command_keyword corollary} false "corollary"; -val _ = theorem @{command_keyword schematic_theorem} true "schematic goal"; -val _ = theorem @{command_keyword schematic_lemma} true "schematic goal"; -val _ = theorem @{command_keyword schematic_corollary} true "schematic goal"; +val _ = theorem @{command_keyword schematic_goal} true "schematic goal"; val structured_statement = diff -r fa4ebbd350ae -r 4645502c3c64 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/Pure/Pure.thy Tue Oct 06 15:14:28 2015 +0200 @@ -19,7 +19,7 @@ and "typedecl" "type_synonym" "nonterminal" "judgment" "consts" "syntax" "no_syntax" "translations" "no_translations" "defs" "definition" "abbreviation" "type_notation" "no_type_notation" "notation" - "no_notation" "axiomatization" "theorems" "lemmas" "declare" + "no_notation" "axiomatization" "lemmas" "declare" "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML" and "SML_import" "SML_export" :: thy_decl % "ML" @@ -44,7 +44,7 @@ and "overloading" :: thy_decl_block and "code_datatype" :: thy_decl and "theorem" "lemma" "corollary" :: thy_goal - and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_goal + and "schematic_goal" :: thy_goal and "notepad" :: thy_decl_block and "have" :: prf_goal % "proof" and "hence" :: prf_goal % "proof" == "then have" diff -r fa4ebbd350ae -r 4645502c3c64 src/Pure/Tools/update_theorems.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Tools/update_theorems.scala Tue Oct 06 15:14:28 2015 +0200 @@ -0,0 +1,40 @@ +/* Title: Pure/Tools/update_theorems.scala + Author: Makarius + +Update toplevel theorem keywords. +*/ + +package isabelle + + +object Update_Theorems +{ + def update_theorems(path: Path) + { + val text0 = File.read(path) + val text1 = + (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator) + yield { + tok.source match { + case "theorems" => "lemmas" + case "schematic_theorem" | "schematic_lemma" | "schematic_corollary" => + "schematic_goal" + case s => s + } }).mkString + + if (text0 != text1) { + Output.writeln("changing " + path) + File.write_backup2(path, text1) + } + } + + + /* command line entry point */ + + def main(args: Array[String]) + { + Command_Line.tool0 { + args.foreach(arg => update_theorems(Path.explode(arg))) + } + } +} diff -r fa4ebbd350ae -r 4645502c3c64 src/Pure/build-jars --- a/src/Pure/build-jars Tue Oct 06 13:31:44 2015 +0200 +++ b/src/Pure/build-jars Tue Oct 06 15:14:28 2015 +0200 @@ -107,6 +107,7 @@ Tools/update_header.scala Tools/update_semicolons.scala Tools/update_then.scala + Tools/update_theorems.scala library.scala term.scala term_xml.scala diff -r fa4ebbd350ae -r 4645502c3c64 src/Sequents/LK/Quantifiers.thy --- a/src/Sequents/LK/Quantifiers.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/Sequents/LK/Quantifiers.thy Tue Oct 06 15:14:28 2015 +0200 @@ -90,13 +90,13 @@ oops (*INVALID*) -schematic_lemma "|- P(?a) --> (ALL x. P(x))" +schematic_goal "|- P(?a) --> (ALL x. P(x))" apply fast? apply (rule _) oops (*INVALID*) -schematic_lemma "|- (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))" +schematic_goal "|- (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" -schematic_lemma "|- (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)" +schematic_goal "|- (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)" by fast diff -r fa4ebbd350ae -r 4645502c3c64 src/ZF/AC/Cardinal_aux.thy --- a/src/ZF/AC/Cardinal_aux.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/ZF/AC/Cardinal_aux.thy Tue Oct 06 15:14:28 2015 +0200 @@ -57,7 +57,7 @@ finally show "i \ A \ B" . qed -schematic_lemma paired_bij: "?f \ bij({{y,z}. y \ x}, x)" +schematic_goal paired_bij: "?f \ bij({{y,z}. y \ x}, x)" apply (rule RepFun_bijective) apply (simp add: doubleton_eq_iff, blast) done diff -r fa4ebbd350ae -r 4645502c3c64 src/ZF/Bin.thy --- a/src/ZF/Bin.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/ZF/Bin.thy Tue Oct 06 15:14:28 2015 +0200 @@ -700,7 +700,7 @@ text \@{text combine_numerals_prod} (products of separate literals)\ lemma "#5 $* x $* #3 = y" apply simp oops -schematic_lemma "y2 $+ ?x42 = y $+ y2" apply simp oops +schematic_goal "y2 $+ ?x42 = y $+ y2" apply simp oops lemma "oo : int ==> l $+ (l $+ #2) $+ oo = oo" apply simp oops diff -r fa4ebbd350ae -r 4645502c3c64 src/ZF/Constructible/Reflection.thy --- a/src/ZF/Constructible/Reflection.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/ZF/Constructible/Reflection.thy Tue Oct 06 15:14:28 2015 +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.\ -schematic_lemma (in reflection) +schematic_goal (in reflection) "Reflects(?Cl, \x. \y. M(y) & x \ y, \a x. \y\Mset(a). x \ y)" @@ -285,7 +285,7 @@ text\Example 2\ -schematic_lemma (in reflection) +schematic_goal (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.\ -schematic_lemma (in reflection) +schematic_goal (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.\ -schematic_lemma (in reflection) +schematic_goal (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.\ -schematic_lemma (in reflection) +schematic_goal (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'\ -schematic_lemma (in reflection) +schematic_goal (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''\ -schematic_lemma (in reflection) +schematic_goal (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.\ -schematic_lemma (in reflection) +schematic_goal (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)))" diff -r fa4ebbd350ae -r 4645502c3c64 src/ZF/ex/misc.thy --- a/src/ZF/ex/misc.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/ZF/ex/misc.thy Tue Oct 06 15:14:28 2015 +0200 @@ -44,7 +44,7 @@ by (blast intro!: equalityI) text\trivial example of term synthesis: apparently hard for some provers!\ -schematic_lemma "a \ b ==> a:?X & b \ ?X" +schematic_goal "a \ b ==> a:?X & b \ ?X" by blast text\Nice blast benchmark. Proved in 0.3s; old tactics can't manage it!\