--- 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,
--- /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
--- 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 \<Longrightarrow> d = lam x. ?f(x)"
+schematic_goal idgenfp_lam: "idgen(d) = d \<Longrightarrow> 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 \<Longrightarrow> d = lam x. ?f(x)"
+schematic_goal po_eta_lemma: "idgen(d) = d \<Longrightarrow> d = lam x. ?f(x)"
apply (unfold idgen_def)
apply (erule sym)
done
--- 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 \<open>Factorial\<close>
-schematic_lemma
+schematic_goal
"letrec f n be ncase(n,succ(zero),\<lambda>x. nrec(n,zero,\<lambda>y g. nrec(f(x),g,\<lambda>z h. succ(h))))
in f(succ(succ(zero))) ---> ?a"
by eval
-schematic_lemma
+schematic_goal
"letrec f n be ncase(n,succ(zero),\<lambda>x. nrec(n,zero,\<lambda>y g. nrec(f(x),g,\<lambda>z h. succ(h))))
in f(succ(succ(succ(zero)))) ---> ?a"
by eval
subsection \<open>Less Than Or Equal\<close>
-schematic_lemma
+schematic_goal
"letrec f p be split(p,\<lambda>m n. ncase(m,true,\<lambda>x. ncase(n,false,\<lambda>y. f(<x,y>))))
in f(<succ(zero), succ(zero)>) ---> ?a"
by eval
-schematic_lemma
+schematic_goal
"letrec f p be split(p,\<lambda>m n. ncase(m,true,\<lambda>x. ncase(n,false,\<lambda>y. f(<x,y>))))
in f(<succ(zero), succ(succ(succ(succ(zero))))>) ---> ?a"
by eval
-schematic_lemma
+schematic_goal
"letrec f p be split(p,\<lambda>m n. ncase(m,true,\<lambda>x. ncase(n,false,\<lambda>y. f(<x,y>))))
in f(<succ(succ(succ(succ(succ(zero))))), succ(succ(succ(succ(zero))))>) ---> ?a"
by eval
@@ -598,12 +598,12 @@
subsection \<open>Reverse\<close>
-schematic_lemma
+schematic_goal
"letrec id l be lcase(l,[],\<lambda>x xs. x$id(xs))
in id(zero$succ(zero)$[]) ---> ?a"
by eval
-schematic_lemma
+schematic_goal
"letrec rev l be lcase(l,[],\<lambda>x xs. lrec(rev(xs),x$[],\<lambda>y ys g. y$g))
in rev(zero$succ(zero)$(succ((lam x. x)`succ(zero)))$([])) ---> ?a"
by eval
--- 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 \<Longrightarrow> ?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: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)"
+schematic_goal add_eq0_lemma: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> ?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:
"\<lbrakk>a:N; b:N; a |-| b = 0 : N\<rbrakk> \<Longrightarrow> ?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)"
apply (unfold absdiff_def)
apply intr
--- 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 \<Longrightarrow> ?a : (A*A) --> A"
+schematic_goal [folded basic_defs]: "A type \<Longrightarrow> ?a : (A*A) --> A"
apply pc
done
-schematic_lemma [folded basic_defs]: "A type \<Longrightarrow> ?a : (A*A) --> A"
+schematic_goal [folded basic_defs]: "A type \<Longrightarrow> ?a : (A*A) --> A"
apply pc
back
done
text "Double negation of the Excluded Middle"
-schematic_lemma "A type \<Longrightarrow> ?a : ((A + (A-->F)) --> F) --> F"
+schematic_goal "A type \<Longrightarrow> ?a : ((A + (A-->F)) --> F) --> F"
apply intr
apply (rule ProdE)
apply assumption
apply pc
done
-schematic_lemma "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : (A*B) \<longrightarrow> (B*A)"
+schematic_goal "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : (A*B) \<longrightarrow> (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 "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A+B --> C) --> (A-->C) * (B-->C)"
+schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A+B --> C) --> (A-->C) * (B-->C)"
apply pc
done
(*A distributive law*)
-schematic_lemma "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : A * (B+C) --> (A*B + A*C)"
+schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : A * (B+C) --> (A*B + A*C)"
apply pc
done
(*more general version, same proof*)
-schematic_lemma
+schematic_goal
assumes "A type"
and "\<And>x. x:A \<Longrightarrow> B(x) type"
and "\<And>x. x:A \<Longrightarrow> C(x) type"
@@ -57,12 +57,12 @@
done
text "Construction of the currying functional"
-schematic_lemma "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A*B --> C) --> (A--> (B-->C))"
+schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A*B --> C) --> (A--> (B-->C))"
apply pc
done
(*more general goal with same proof*)
-schematic_lemma
+schematic_goal
assumes "A type"
and "\<And>x. x:A \<Longrightarrow> B(x) type"
and "\<And>z. z: (SUM x:A. B(x)) \<Longrightarrow> C(z) type"
@@ -72,12 +72,12 @@
done
text "Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)"
-schematic_lemma "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A --> (B-->C)) --> (A*B --> C)"
+schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A --> (B-->C)) --> (A*B --> C)"
apply pc
done
(*more general goal with same proof*)
-schematic_lemma
+schematic_goal
assumes "A type"
and "\<And>x. x:A \<Longrightarrow> B(x) type"
and "\<And>z. z: (SUM x:A . B(x)) \<Longrightarrow> C(z) type"
@@ -87,12 +87,12 @@
done
text "Function application"
-schematic_lemma "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : ((A --> B) * A) --> B"
+schematic_goal "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?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 "\<And>x y. \<lbrakk>x:A; y:B\<rbrakk> \<Longrightarrow> 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 "\<And>x. x:A \<Longrightarrow> B(x) type"
and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> 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 "\<And>z. z: A+B \<Longrightarrow> C(z) type"
@@ -123,7 +123,7 @@
done
(*towards AXIOM OF CHOICE*)
-schematic_lemma [folded basic_defs]:
+schematic_goal [folded basic_defs]:
"\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?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 "\<And>x. x:A \<Longrightarrow> B(x) type"
and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> 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 "\<And>x. x:A \<Longrightarrow> B(x) type"
and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> 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,\<lambda>v w.split(v,\<lambda>x y.lam z. <x,<y,z>>) ` w) *)
-schematic_lemma
+schematic_goal
assumes "A type"
and "B type"
and "\<And>z. z:A*B \<Longrightarrow> C(z) type"
--- 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 \<Longrightarrow> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` <i,j>, 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)), <succ(0), 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)), <succ(0),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,j>)), i)
* Eq(?A, ?b(inr(<i,j>)), 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,j>)), i)
+schematic_goal "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i)
* Eq(?A(i,j), ?b(inr(<i,j>)), j)"
oops
(*similar but specifying the type N simplifies the unification problems*)
-schematic_lemma "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)
+schematic_goal "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)
* Eq(N, ?b(inr(<i,j>)), j)"
oops
text "Deriving the addition operator"
-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)))"
--- 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 \<open>Single-step proofs: verifying that a type is well-formed\<close>
-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, \<lambda>v w. v)) ` <0, succ(0)> : ?A"
+schematic_goal "(lam u. split(u, \<lambda>v w. v)) ` <0, succ(0)> : ?A"
apply typechk
done
text "typechecking the predecessor function"
-schematic_lemma "lam n. rec(n, 0, \<lambda>x y. x) : ?A"
+schematic_goal "lam n. rec(n, 0, \<lambda>x y. x) : ?A"
apply typechk
done
text "typechecking the addition function"
-schematic_lemma "lam n. lam m. rec(n, m, \<lambda>x y. succ(y)) : ?A"
+schematic_goal "lam n. lam m. rec(n, m, \<lambda>x y. succ(y)) : ?A"
apply typechk
done
@@ -69,18 +69,18 @@
method_setup N =
\<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (TRYALL (resolve_tac ctxt @{thms NF})))\<close>
-schematic_lemma "lam w. <w,w> : ?A"
+schematic_goal "lam w. <w,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, \<lambda>j k. j) : ?A"
+schematic_goal "lam i. split(i, \<lambda>j k. j) : ?A"
apply typechk
apply N
done
--- 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 \<open>Simple types\<close>
-schematic_lemma "A:* \<turnstile> A\<rightarrow>A : ?T"
+schematic_goal "A:* \<turnstile> A\<rightarrow>A : ?T"
by (depth_solve rules)
-schematic_lemma "A:* \<turnstile> \<Lambda> a:A. a : ?T"
+schematic_goal "A:* \<turnstile> \<Lambda> a:A. a : ?T"
by (depth_solve rules)
-schematic_lemma "A:* B:* b:B \<turnstile> \<Lambda> x:A. b : ?T"
+schematic_goal "A:* B:* b:B \<turnstile> \<Lambda> x:A. b : ?T"
by (depth_solve rules)
-schematic_lemma "A:* b:A \<turnstile> (\<Lambda> a:A. a)^b: ?T"
+schematic_goal "A:* b:A \<turnstile> (\<Lambda> a:A. a)^b: ?T"
by (depth_solve rules)
-schematic_lemma "A:* B:* c:A b:B \<turnstile> (\<Lambda> x:A. b)^ c: ?T"
+schematic_goal "A:* B:* c:A b:B \<turnstile> (\<Lambda> x:A. b)^ c: ?T"
by (depth_solve rules)
-schematic_lemma "A:* B:* \<turnstile> \<Lambda> a:A. \<Lambda> b:B. a : ?T"
+schematic_goal "A:* B:* \<turnstile> \<Lambda> a:A. \<Lambda> b:B. a : ?T"
by (depth_solve rules)
subsection \<open>Second-order types\<close>
-schematic_lemma (in L2) "\<turnstile> \<Lambda> A:*. \<Lambda> a:A. a : ?T"
+schematic_goal (in L2) "\<turnstile> \<Lambda> A:*. \<Lambda> a:A. a : ?T"
by (depth_solve rules)
-schematic_lemma (in L2) "A:* \<turnstile> (\<Lambda> B:*.\<Lambda> b:B. b)^A : ?T"
+schematic_goal (in L2) "A:* \<turnstile> (\<Lambda> B:*.\<Lambda> b:B. b)^A : ?T"
by (depth_solve rules)
-schematic_lemma (in L2) "A:* b:A \<turnstile> (\<Lambda> B:*.\<Lambda> b:B. b) ^ A ^ b: ?T"
+schematic_goal (in L2) "A:* b:A \<turnstile> (\<Lambda> B:*.\<Lambda> b:B. b) ^ A ^ b: ?T"
by (depth_solve rules)
-schematic_lemma (in L2) "\<turnstile> \<Lambda> B:*.\<Lambda> a:(\<Pi> A:*.A).a ^ ((\<Pi> A:*.A)\<rightarrow>B) ^ a: ?T"
+schematic_goal (in L2) "\<turnstile> \<Lambda> B:*.\<Lambda> a:(\<Pi> A:*.A).a ^ ((\<Pi> A:*.A)\<rightarrow>B) ^ a: ?T"
by (depth_solve rules)
subsection \<open>Weakly higher-order propositional logic\<close>
-schematic_lemma (in Lomega) "\<turnstile> \<Lambda> A:*.A\<rightarrow>A : ?T"
+schematic_goal (in Lomega) "\<turnstile> \<Lambda> A:*.A\<rightarrow>A : ?T"
by (depth_solve rules)
-schematic_lemma (in Lomega) "B:* \<turnstile> (\<Lambda> A:*.A\<rightarrow>A) ^ B : ?T"
+schematic_goal (in Lomega) "B:* \<turnstile> (\<Lambda> A:*.A\<rightarrow>A) ^ B : ?T"
by (depth_solve rules)
-schematic_lemma (in Lomega) "B:* b:B \<turnstile> (\<Lambda> y:B. b): ?T"
+schematic_goal (in Lomega) "B:* b:B \<turnstile> (\<Lambda> y:B. b): ?T"
by (depth_solve rules)
-schematic_lemma (in Lomega) "A:* F:*\<rightarrow>* \<turnstile> F^(F^A): ?T"
+schematic_goal (in Lomega) "A:* F:*\<rightarrow>* \<turnstile> F^(F^A): ?T"
by (depth_solve rules)
-schematic_lemma (in Lomega) "A:* \<turnstile> \<Lambda> F:*\<rightarrow>*.F^(F^A): ?T"
+schematic_goal (in Lomega) "A:* \<turnstile> \<Lambda> F:*\<rightarrow>*.F^(F^A): ?T"
by (depth_solve rules)
subsection \<open>LP\<close>
-schematic_lemma (in LP) "A:* \<turnstile> A \<rightarrow> * : ?T"
+schematic_goal (in LP) "A:* \<turnstile> A \<rightarrow> * : ?T"
by (depth_solve rules)
-schematic_lemma (in LP) "A:* P:A\<rightarrow>* a:A \<turnstile> P^a: ?T"
+schematic_goal (in LP) "A:* P:A\<rightarrow>* a:A \<turnstile> P^a: ?T"
by (depth_solve rules)
-schematic_lemma (in LP) "A:* P:A\<rightarrow>A\<rightarrow>* a:A \<turnstile> \<Pi> a:A. P^a^a: ?T"
+schematic_goal (in LP) "A:* P:A\<rightarrow>A\<rightarrow>* a:A \<turnstile> \<Pi> a:A. P^a^a: ?T"
by (depth_solve rules)
-schematic_lemma (in LP) "A:* P:A\<rightarrow>* Q:A\<rightarrow>* \<turnstile> \<Pi> a:A. P^a \<rightarrow> Q^a: ?T"
+schematic_goal (in LP) "A:* P:A\<rightarrow>* Q:A\<rightarrow>* \<turnstile> \<Pi> a:A. P^a \<rightarrow> Q^a: ?T"
by (depth_solve rules)
-schematic_lemma (in LP) "A:* P:A\<rightarrow>* \<turnstile> \<Pi> a:A. P^a \<rightarrow> P^a: ?T"
+schematic_goal (in LP) "A:* P:A\<rightarrow>* \<turnstile> \<Pi> a:A. P^a \<rightarrow> P^a: ?T"
by (depth_solve rules)
-schematic_lemma (in LP) "A:* P:A\<rightarrow>* \<turnstile> \<Lambda> a:A. \<Lambda> x:P^a. x: ?T"
+schematic_goal (in LP) "A:* P:A\<rightarrow>* \<turnstile> \<Lambda> a:A. \<Lambda> x:P^a. x: ?T"
by (depth_solve rules)
-schematic_lemma (in LP) "A:* P:A\<rightarrow>* Q:* \<turnstile> (\<Pi> a:A. P^a\<rightarrow>Q) \<rightarrow> (\<Pi> a:A. P^a) \<rightarrow> Q : ?T"
+schematic_goal (in LP) "A:* P:A\<rightarrow>* Q:* \<turnstile> (\<Pi> a:A. P^a\<rightarrow>Q) \<rightarrow> (\<Pi> a:A. P^a) \<rightarrow> Q : ?T"
by (depth_solve rules)
-schematic_lemma (in LP) "A:* P:A\<rightarrow>* Q:* a0:A \<turnstile>
+schematic_goal (in LP) "A:* P:A\<rightarrow>* Q:* a0:A \<turnstile>
\<Lambda> x:\<Pi> a:A. P^a\<rightarrow>Q. \<Lambda> y:\<Pi> a:A. P^a. x^a0^(y^a0): ?T"
by (depth_solve rules)
subsection \<open>Omega-order types\<close>
-schematic_lemma (in L2) "A:* B:* \<turnstile> \<Pi> C:*.(A\<rightarrow>B\<rightarrow>C)\<rightarrow>C : ?T"
+schematic_goal (in L2) "A:* B:* \<turnstile> \<Pi> C:*.(A\<rightarrow>B\<rightarrow>C)\<rightarrow>C : ?T"
by (depth_solve rules)
-schematic_lemma (in Lomega2) "\<turnstile> \<Lambda> A:*.\<Lambda> B:*.\<Pi> C:*.(A\<rightarrow>B\<rightarrow>C)\<rightarrow>C : ?T"
+schematic_goal (in Lomega2) "\<turnstile> \<Lambda> A:*.\<Lambda> B:*.\<Pi> C:*.(A\<rightarrow>B\<rightarrow>C)\<rightarrow>C : ?T"
by (depth_solve rules)
-schematic_lemma (in Lomega2) "\<turnstile> \<Lambda> A:*.\<Lambda> B:*.\<Lambda> x:A. \<Lambda> y:B. x : ?T"
+schematic_goal (in Lomega2) "\<turnstile> \<Lambda> A:*.\<Lambda> B:*.\<Lambda> x:A. \<Lambda> y:B. x : ?T"
by (depth_solve rules)
-schematic_lemma (in Lomega2) "A:* B:* \<turnstile> ?p : (A\<rightarrow>B) \<rightarrow> ((B\<rightarrow>\<Pi> P:*.P)\<rightarrow>(A\<rightarrow>\<Pi> P:*.P))"
+schematic_goal (in Lomega2) "A:* B:* \<turnstile> ?p : (A\<rightarrow>B) \<rightarrow> ((B\<rightarrow>\<Pi> P:*.P)\<rightarrow>(A\<rightarrow>\<Pi> P:*.P))"
apply (strip_asms rules)
apply (rule lam_ss)
apply (depth_solve1 rules)
@@ -140,14 +140,14 @@
subsection \<open>Second-order Predicate Logic\<close>
-schematic_lemma (in LP2) "A:* P:A\<rightarrow>* \<turnstile> \<Lambda> a:A. P^a\<rightarrow>(\<Pi> A:*.A) : ?T"
+schematic_goal (in LP2) "A:* P:A\<rightarrow>* \<turnstile> \<Lambda> a:A. P^a\<rightarrow>(\<Pi> A:*.A) : ?T"
by (depth_solve rules)
-schematic_lemma (in LP2) "A:* P:A\<rightarrow>A\<rightarrow>* \<turnstile>
+schematic_goal (in LP2) "A:* P:A\<rightarrow>A\<rightarrow>* \<turnstile>
(\<Pi> a:A. \<Pi> b:A. P^a^b\<rightarrow>P^b^a\<rightarrow>\<Pi> P:*.P) \<rightarrow> \<Pi> a:A. P^a^a\<rightarrow>\<Pi> P:*.P : ?T"
by (depth_solve rules)
-schematic_lemma (in LP2) "A:* P:A\<rightarrow>A\<rightarrow>* \<turnstile>
+schematic_goal (in LP2) "A:* P:A\<rightarrow>A\<rightarrow>* \<turnstile>
?p: (\<Pi> a:A. \<Pi> b:A. P^a^b\<rightarrow>P^b^a\<rightarrow>\<Pi> P:*.P) \<rightarrow> \<Pi> a:A. P^a^a\<rightarrow>\<Pi> P:*.P"
-- \<open>Antisymmetry implies irreflexivity:\<close>
apply (strip_asms rules)
@@ -169,22 +169,22 @@
subsection \<open>LPomega\<close>
-schematic_lemma (in LPomega) "A:* \<turnstile> \<Lambda> P:A\<rightarrow>A\<rightarrow>*.\<Lambda> a:A. P^a^a : ?T"
+schematic_goal (in LPomega) "A:* \<turnstile> \<Lambda> P:A\<rightarrow>A\<rightarrow>*.\<Lambda> a:A. P^a^a : ?T"
by (depth_solve rules)
-schematic_lemma (in LPomega) "\<turnstile> \<Lambda> A:*.\<Lambda> P:A\<rightarrow>A\<rightarrow>*.\<Lambda> a:A. P^a^a : ?T"
+schematic_goal (in LPomega) "\<turnstile> \<Lambda> A:*.\<Lambda> P:A\<rightarrow>A\<rightarrow>*.\<Lambda> a:A. P^a^a : ?T"
by (depth_solve rules)
subsection \<open>Constructions\<close>
-schematic_lemma (in CC) "\<turnstile> \<Lambda> A:*.\<Lambda> P:A\<rightarrow>*.\<Lambda> a:A. P^a\<rightarrow>\<Pi> P:*.P: ?T"
+schematic_goal (in CC) "\<turnstile> \<Lambda> A:*.\<Lambda> P:A\<rightarrow>*.\<Lambda> a:A. P^a\<rightarrow>\<Pi> P:*.P: ?T"
by (depth_solve rules)
-schematic_lemma (in CC) "\<turnstile> \<Lambda> A:*.\<Lambda> P:A\<rightarrow>*.\<Pi> a:A. P^a: ?T"
+schematic_goal (in CC) "\<turnstile> \<Lambda> A:*.\<Lambda> P:A\<rightarrow>*.\<Pi> a:A. P^a: ?T"
by (depth_solve rules)
-schematic_lemma (in CC) "A:* P:A\<rightarrow>* a:A \<turnstile> ?p : (\<Pi> a:A. P^a)\<rightarrow>P^a"
+schematic_goal (in CC) "A:* P:A\<rightarrow>* a:A \<turnstile> ?p : (\<Pi> a:A. P^a)\<rightarrow>P^a"
apply (strip_asms rules)
apply (rule lam_ss)
apply (depth_solve1 rules)
@@ -196,15 +196,15 @@
subsection \<open>Some random examples\<close>
-schematic_lemma (in LP2) "A:* c:A f:A\<rightarrow>A \<turnstile>
+schematic_goal (in LP2) "A:* c:A f:A\<rightarrow>A \<turnstile>
\<Lambda> a:A. \<Pi> P:A\<rightarrow>*.P^c \<rightarrow> (\<Pi> x:A. P^x\<rightarrow>P^(f^x)) \<rightarrow> P^a : ?T"
by (depth_solve rules)
-schematic_lemma (in CC) "\<Lambda> A:*.\<Lambda> c:A. \<Lambda> f:A\<rightarrow>A.
+schematic_goal (in CC) "\<Lambda> A:*.\<Lambda> c:A. \<Lambda> f:A\<rightarrow>A.
\<Lambda> a:A. \<Pi> P:A\<rightarrow>*.P^c \<rightarrow> (\<Pi> x:A. P^x\<rightarrow>P^(f^x)) \<rightarrow> P^a : ?T"
by (depth_solve rules)
-schematic_lemma (in LP2)
+schematic_goal (in LP2)
"A:* a:A b:A \<turnstile> ?p: (\<Pi> P:A\<rightarrow>*.P^a\<rightarrow>P^b) \<rightarrow> (\<Pi> P:A\<rightarrow>*.P^b\<rightarrow>P^a)"
-- \<open>Symmetry of Leibnitz equality\<close>
apply (strip_asms rules)
--- 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 @@
\<close>
ML (*<*) \<open>\<close>
-schematic_lemma "thm": fixes x y z :: "'a::order" shows "x < y \<and> x < z \<equiv> ?P"
+schematic_goal "thm": fixes x y z :: "'a::order" shows "x < y \<and> x < z \<equiv> ?P"
ML_prf
(*>*) \<open>val thm =
Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"}\<close> (*<*)
--- 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 \<rightarrow> proof(prove)"} \\
@{command_def "theorem"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
@{command_def "corollary"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
- @{command_def "schematic_lemma"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
- @{command_def "schematic_theorem"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
- @{command_def "schematic_corollary"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
+ @{command_def "schematic_goal"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
@{command_def "have"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
@{command_def "show"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
@{command_def "hence"} & : & @{text "proof(state) \<rightarrow> proof(prove)"} \\
@@ -423,8 +421,7 @@
@{rail \<open>
(@@{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,
--- 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}
\<close>
@@ -1441,12 +1441,11 @@
text \<open>
\begin{matharray}{rcll}
@{command_def "lemmas"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def "theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
@{command_def "named_theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
\end{matharray}
@{rail \<open>
- (@@{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
--- 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\<open>Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
fast DISCOVERS who killed Agatha.\<close>
-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)) &
(\<forall>x y. killed(x,y) --> hates(x,y) & ~richer(x,y)) &
(\<forall>x. hates(agatha,x) --> ~hates(charles,x)) &
--- a/src/FOL/ex/Prolog.thy 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)+ -- \<open>does not solve it directly!\<close>
back
back
@@ -67,23 +67,23 @@
DEPTH_FIRST (has_fewer_prems 1) (resolve_tac ctxt @{thms rules} 1)
\<close>
-schematic_lemma "rev(?x, a:b:c:Nil)"
+schematic_goal "rev(?x, a:b:c:Nil)"
apply (tactic \<open>prolog_tac @{context}\<close>)
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 \<open>prolog_tac @{context}\<close>)
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 \<open>
DEPTH_SOLVE (resolve_tac @{context} ([@{thm refl}, @{thm conjI}] @ @{thms rules}) 1)\<close>)
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 \<open>
DEPTH_SOLVE (resolve_tac @{context} ([@{thm refl}, @{thm conjI}] @ @{thms rules}) 1)\<close>)
done
--- 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))"
--- 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))"
--- 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}];
\<close>
-schematic_lemma cla_rews:
+schematic_goal cla_rews:
"?p1 : P | ~P"
"?p2 : ~P | P"
"?p3 : ~ ~ P <-> P"
--- 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 \<Longrightarrow> q:P \<Longrightarrow> ?p:R"
+schematic_goal notE: "p:~P \<Longrightarrow> q:P \<Longrightarrow> ?p:R"
unfolding not_def
apply (drule (1) mp)
apply (erule FalseE)
done
(*This is useful with the special implication rules for each kind of P. *)
-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 =
\<open>Attrib.thms >> (fn prems => fn ctxt => SIMPLE_METHOD' (iff_tac ctxt prems))\<close>
-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 \<Longrightarrow> q:P(a) \<Longrightarrow> ?p:P(b)"
+schematic_goal ssubst: "p:b=a \<Longrightarrow> q:P(a) \<Longrightarrow> ?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 \<open>
DEPTH_SOLVE (assume_tac @{context} 1 ORELSE eresolve_tac @{context} [@{thm subst}, @{thm ssubst}] 1)\<close>)
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 \<open>
DEPTH_SOLVE (assume_tac @{context} 1 ORELSE eresolve_tac @{context} [@{thm subst}, @{thm ssubst}] 1)\<close>)
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 \<open>
DEPTH_SOLVE (assume_tac @{context} 1 ORELSE eresolve_tac @{context} [@{thm subst}, @{thm ssubst}] 1)\<close>)
@@ -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 \<open>fn st => IntPr.fast_tac @{context} 1 st\<close>)+
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 \<open>IntPr.fast_tac @{context} 1\<close>)+
done
-schematic_lemma not_rews:
+schematic_goal not_rews:
"?p1 : ~ False <-> True"
"?p2 : ~ True <-> False"
apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)+
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 \<open>IntPr.fast_tac @{context} 1\<close>)+
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 \<open>IntPr.fast_tac @{context} 1\<close>)+
done
-schematic_lemma quant_rews:
+schematic_goal quant_rews:
"?p1 : (ALL x. P) <-> P"
"?p2 : (EX x. P) <-> P"
apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)+
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 \<open>IntPr.fast_tac @{context} 1\<close>)+
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 \<open>IntPr.fast_tac @{context} 1\<close>)
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 \<open>IntPr.fast_tac @{context} 1\<close>)
done
--- 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 \<open>fast_tac @{context} (FOLP_cs addSIs [@{thm f_cong}]) 1\<close>)
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
--- 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 \<open>A form of conj-elimination\<close>
-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 \<open>Parallel lifting example.\<close>
-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 \<open>A bigger demonstration of quantifiers -- not in the paper.\<close>
-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)
--- 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 \<open>fast_tac @{context} (FOLP_cs addIs @{thms assms}) 1\<close>)
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 \<open>fast_tac @{context} (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1\<close>)
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 \<open>val if_cs = FOLP_cs addSIs [@{thm ifI}] addSEs [@{thm ifE}]\<close>
-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 \<open>fast_tac @{context} if_cs 1\<close>)
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 \<open>fast_tac @{context} if_cs 1\<close>)
done
--- 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 \<open>Some simple backward proofs\<close>
-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 \<open>Demonstration of @{text "fast"}\<close>
-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 \<open>fast_tac @{context} FOLP_cs 1\<close>)
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 \<open>fast_tac @{context} FOLP_cs 1\<close>)
done
@@ -57,7 +57,7 @@
subsubsection \<open>Derivation of conjunction elimination rule\<close>
-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 \<open>Derivation of negation introduction\<close>
-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 \<open>Alternative proof of the result above\<close>
-schematic_lemma
+schematic_goal
assumes major: "p : ~P"
and minor: "q : P"
shows "?p : R"
--- 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 \<open>IntPr.fast_tac @{context} 1\<close>)
-schematic_lemma "?p : ~~~P <-> ~P"
+schematic_goal "?p : ~~~P <-> ~P"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-schematic_lemma "?p : ~~((P --> Q | R) --> (P-->Q) | (P-->R))"
+schematic_goal "?p : ~~((P --> Q | R) --> (P-->Q) | (P-->R))"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-schematic_lemma "?p : (P<->Q) <-> (Q<->P)"
+schematic_goal "?p : (P<->Q) <-> (Q<->P)"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
subsection \<open>Lemmas for the propositional double-negation translation\<close>
-schematic_lemma "?p : P --> ~~P"
+schematic_goal "?p : P --> ~~P"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-schematic_lemma "?p : ~~(~~P --> P)"
+schematic_goal "?p : ~~(~~P --> P)"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-schematic_lemma "?p : ~~P & ~~(P --> Q) --> ~~Q"
+schematic_goal "?p : ~~P & ~~(P --> Q) --> ~~Q"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
subsection \<open>The following are classically but not constructively valid\<close>
(*The attempt to prove them terminates quickly!*)
-schematic_lemma "?p : ((P-->Q) --> P) --> P"
+schematic_goal "?p : ((P-->Q) --> P) --> P"
apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
oops
-schematic_lemma "?p : (P&Q-->R) --> (P-->R) | (Q-->R)"
+schematic_goal "?p : (P&Q-->R) --> (P-->R) | (Q-->R)"
apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
oops
@@ -70,74 +70,74 @@
subsection \<open>Intuitionistic FOL: propositional problems based on Pelletier\<close>
text "Problem ~~1"
-schematic_lemma "?p : ~~((P-->Q) <-> (~Q --> ~P))"
+schematic_goal "?p : ~~((P-->Q) <-> (~Q --> ~P))"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
text "Problem ~~2"
-schematic_lemma "?p : ~~(~~P <-> P)"
+schematic_goal "?p : ~~(~~P <-> P)"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
text "Problem 3"
-schematic_lemma "?p : ~(P-->Q) --> (Q-->P)"
+schematic_goal "?p : ~(P-->Q) --> (Q-->P)"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
text "Problem ~~4"
-schematic_lemma "?p : ~~((~P-->Q) <-> (~Q --> P))"
+schematic_goal "?p : ~~((~P-->Q) <-> (~Q --> P))"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
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 \<open>IntPr.fast_tac @{context} 1\<close>)
text "Problem ~~6"
-schematic_lemma "?p : ~~(P | ~P)"
+schematic_goal "?p : ~~(P | ~P)"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
text "Problem ~~7"
-schematic_lemma "?p : ~~(P | ~~~P)"
+schematic_goal "?p : ~~(P | ~~~P)"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
text "Problem ~~8. Peirce's law"
-schematic_lemma "?p : ~~(((P-->Q) --> P) --> P)"
+schematic_goal "?p : ~~(((P-->Q) --> P) --> P)"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
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 \<open>IntPr.fast_tac @{context} 1\<close>)
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 \<open>IntPr.fast_tac @{context} 1\<close>)
text "11. Proved in each direction (incorrectly, says Pelletier!!) "
-schematic_lemma "?p : P<->P"
+schematic_goal "?p : P<->P"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
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 \<open>IntPr.fast_tac @{context} 1\<close>)
-schematic_lemma "?p : ((P <-> Q) <-> R) --> ~~(P <-> (Q <-> R))"
+schematic_goal "?p : ((P <-> Q) <-> R) --> ~~(P <-> (Q <-> R))"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
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 \<open>IntPr.fast_tac @{context} 1\<close>)
text "Problem ~~14"
-schematic_lemma "?p : ~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))"
+schematic_goal "?p : ~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
text "Problem ~~15"
-schematic_lemma "?p : ~~((P --> Q) <-> (~P | Q))"
+schematic_goal "?p : ~~((P --> Q) <-> (~P | Q))"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
text "Problem ~~16"
-schematic_lemma "?p : ~~((P-->Q) | (Q-->P))"
+schematic_goal "?p : ~~((P-->Q) | (Q-->P))"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
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 \<open>IntPr.fast_tac @{context} 1\<close>) -- 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 \<open>IntPr.fast_tac @{context} 1\<close>)
-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 \<open>IntPr.fast_tac @{context} 1\<close>)
-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 \<open>IntPr.fast_tac @{context} 1\<close>)
-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 \<open>IntPr.fast_tac @{context} 1\<close>)
-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 \<open>IntPr.fast_tac @{context} 1\<close>)
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 \<open>IntPr.fast_tac @{context} 1\<close>)?
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 \<open>IntPr.fast_tac @{context} 1\<close>)?
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 \<open>IntPr.fast_tac @{context} 1\<close>)?
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 \<open>IntPr.fast_tac @{context} 1\<close>)?
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 \<open>IntPr.fast_tac @{context} 1\<close>)?
oops
@@ -194,32 +194,32 @@
\<close>
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 \<open>IntPr.fast_tac @{context} 1\<close>)
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 \<open>IntPr.fast_tac @{context} 1\<close>)
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 \<open>IntPr.fast_tac @{context} 1\<close>)
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") -- \<open>60 seconds\<close>
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
--- 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 \<open>Proofs about the natural numbers\<close>
-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 \<Longrightarrow> ?p : Suc(x) = Suc(y)"
+schematic_goal Suc_cong: "p : x = y \<Longrightarrow> ?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}
\<close>
-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 \<open>SIMP_TAC @{context} add_ss 1\<close>)
apply (tactic \<open>ASM_SIMP_TAC @{context} add_ss 1\<close>)
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 \<open>SIMP_TAC @{context} add_ss 1\<close>)
apply (tactic \<open>ASM_SIMP_TAC @{context} add_ss 1\<close>)
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 \<open>ALLGOALS (ASM_SIMP_TAC @{context} add_ss)\<close>)
done
--- 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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
-schematic_lemma "?p : P | Q --> Q | P"
+schematic_goal "?p : P | Q --> Q | P"
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
-schematic_lemma "?p : (P | Q) | R --> P | (Q | R)"
+schematic_goal "?p : (P | Q) | R --> P | (Q | R)"
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
-schematic_lemma "?p : (P | R) & (Q | R) --> (P & Q) | R"
+schematic_goal "?p : (P | R) & (Q | R) --> (P & Q) | R"
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
-schematic_lemma "?p : (P | Q) & R --> (P & R) | (Q & R)"
+schematic_goal "?p : (P | Q) & R --> (P & R) | (Q & R)"
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
-schematic_lemma "?p : (P & R) | (Q & R) --> (P | Q) & R"
+schematic_goal "?p : (P & R) | (Q & R) --> (P | Q) & R"
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
-schematic_lemma "?p : (P & Q --> R) <-> (P--> (Q-->R))"
+schematic_goal "?p : (P & Q --> R) <-> (P--> (Q-->R))"
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
-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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
-schematic_lemma "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
+schematic_goal "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
-schematic_lemma "?p : (P --> Q & R) <-> (P-->Q) & (P-->R)"
+schematic_goal "?p : (P --> Q & R) <-> (P-->Q) & (P-->R)"
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
text "Propositions-as-types"
(*The combinator K*)
-schematic_lemma "?p : P --> (Q --> P)"
+schematic_goal "?p : P --> (Q --> P)"
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
(*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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
(*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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
-schematic_lemma "?p : (P-->Q) --> (~Q --> ~P)"
+schematic_goal "?p : (P-->Q) --> (~Q --> ~P)"
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
-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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
-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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
-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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
-schematic_lemma mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q"
+schematic_goal mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q"
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
-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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
-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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
-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)
--- 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 \<open>IntPr.fast_tac @{context} 1\<close>)
-schematic_lemma "?p : P | Q --> Q | P"
+schematic_goal "?p : P | Q --> Q | P"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
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 \<open>IntPr.fast_tac @{context} 1\<close>)
-schematic_lemma "?p : (P | Q) | R --> P | (Q | R)"
+schematic_goal "?p : (P | Q) | R --> P | (Q | R)"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
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 \<open>IntPr.fast_tac @{context} 1\<close>)
-schematic_lemma "?p : (P | R) & (Q | R) --> (P & Q) | R"
+schematic_goal "?p : (P | R) & (Q | R) --> (P & Q) | R"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-schematic_lemma "?p : (P | Q) & R --> (P & R) | (Q & R)"
+schematic_goal "?p : (P | Q) & R --> (P & R) | (Q & R)"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-schematic_lemma "?p : (P & R) | (Q & R) --> (P | Q) & R"
+schematic_goal "?p : (P & R) | (Q & R) --> (P | Q) & R"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
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 \<open>IntPr.fast_tac @{context} 1\<close>)
-schematic_lemma "?p : (P & Q --> R) <-> (P--> (Q-->R))"
+schematic_goal "?p : (P & Q --> R) <-> (P--> (Q-->R))"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-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 \<open>IntPr.fast_tac @{context} 1\<close>)
-schematic_lemma "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
+schematic_goal "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-schematic_lemma "?p : (P --> Q & R) <-> (P-->Q) & (P-->R)"
+schematic_goal "?p : (P --> Q & R) <-> (P-->Q) & (P-->R)"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
text "Propositions-as-types"
(*The combinator K*)
-schematic_lemma "?p : P --> (Q --> P)"
+schematic_goal "?p : P --> (Q --> P)"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
(*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 \<open>IntPr.fast_tac @{context} 1\<close>)
(*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 \<open>IntPr.fast_tac @{context} 1\<close>)
-schematic_lemma "?p : (P-->Q) --> (~Q --> ~P)"
+schematic_goal "?p : (P-->Q) --> (~Q --> ~P)"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
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 \<open>IntPr.fast_tac @{context} 1\<close>)
-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 \<open>IntPr.fast_tac @{context} 1\<close>)
-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 \<open>IntPr.fast_tac @{context} 1\<close>)
-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 \<open>IntPr.fast_tac @{context} 1\<close>)
-schematic_lemma mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q"
+schematic_goal mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-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 \<open>IntPr.fast_tac @{context} 1\<close>)
-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 \<open>IntPr.fast_tac @{context} 1\<close>)
-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)
--- 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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
-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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
(*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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
-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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
-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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
(*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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
-schematic_lemma "?p : (ALL x. Q(x)) --> (EX x. Q(x))"
+schematic_goal "?p : (ALL x. Q(x)) --> (EX x. Q(x))"
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)?
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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)?
oops
-schematic_lemma "?p : P(?a) --> (ALL x. P(x))"
+schematic_goal "?p : P(?a) --> (ALL x. P(x))"
apply (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)?
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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)?
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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
(*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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
-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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
-schematic_lemma "?p : (ALL x. Q(x)) --> (EX x. Q(x))"
+schematic_goal "?p : (ALL x. Q(x)) --> (EX x. Q(x))"
by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
(*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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
(*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 \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
end
--- 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 \<open>IntPr.fast_tac @{context} 1\<close>)
-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 \<open>IntPr.fast_tac @{context} 1\<close>)
(*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 \<open>IntPr.fast_tac @{context} 1\<close>)
-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 \<open>IntPr.fast_tac @{context} 1\<close>)
-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 \<open>IntPr.fast_tac @{context} 1\<close>)
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 \<open>IntPr.fast_tac @{context} 1\<close>)
(*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 \<open>IntPr.fast_tac @{context} 1\<close>)
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 \<open>IntPr.fast_tac @{context} 1\<close>)
-schematic_lemma "?p : (ALL x. Q(x)) --> (EX x. Q(x))"
+schematic_goal "?p : (ALL x. Q(x)) --> (EX x. Q(x))"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
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 \<open>IntPr.fast_tac @{context} 1\<close>)?
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 \<open>IntPr.fast_tac @{context} 1\<close>)?
oops
-schematic_lemma "?p : P(?a) --> (ALL x. P(x))"
+schematic_goal "?p : P(?a) --> (ALL x. P(x))"
apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
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 \<open>IntPr.fast_tac @{context} 1\<close>)?
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 \<open>IntPr.fast_tac @{context} 1\<close>)
(*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 \<open>IntPr.fast_tac @{context} 1\<close>)
-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 \<open>IntPr.fast_tac @{context} 1\<close>)
-schematic_lemma "?p : (ALL x. Q(x)) --> (EX x. Q(x))"
+schematic_goal "?p : (ALL x. Q(x)) --> (EX x. Q(x))"
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
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 \<open>IntPr.fast_tac @{context} 1\<close>)
(*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 \<open>IntPr.fast_tac @{context} 1\<close>)
(*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 \<open>IntPr.fast_tac @{context} 1\<close>)
end
--- 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: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
+schematic_goal wt_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
apply (unfold test_def arr_viewed_from_def)
(* ?pTs = [Class Base] *)
apply (rule wtIs (* ;; *))
@@ -1130,7 +1130,7 @@
subsubsection "definite assignment"
-schematic_lemma da_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>
+schematic_goal da_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>
\<turnstile>{} \<guillemotright>\<langle>test ?pTs\<rangle>\<guillemotright> \<lparr>nrm={VName e},brk=\<lambda> l. UNIV\<rparr>"
apply (unfold test_def arr_viewed_from_def)
apply (rule da.Comp)
@@ -1248,7 +1248,7 @@
declare Pair_eq [simp del]
-schematic_lemma exec_test:
+schematic_goal exec_test:
"\<lbrakk>the (new_Addr (heap s1)) = a;
the (new_Addr (heap ?s2)) = b;
the (new_Addr (heap ?s3)) = c\<rbrakk> \<Longrightarrow>
--- a/src/HOL/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 \<Longrightarrow> A x"
+schematic_goal "?A x \<Longrightarrow> A x"
apply (match conclusion in "H" for H \<Rightarrow> \<open>match conclusion in Y for Y \<Rightarrow> \<open>print_term Y\<close>\<close>)
apply assumption
done
--- 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"
--- 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 \<open>The existence of the zero element of a vector space
--- 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) \<Rightarrow> ?t"
+schematic_goal ex: "(''x'' ::= N 5;; ''y'' ::= V ''x'', s) \<Rightarrow> ?t"
apply(rule Seq)
apply(rule Assign)
apply simp
--- 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 \<open>Package setup.\<close>
-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
--- 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 \<open>The main end product for @{const rel_mset}: inductive characterization:\<close>
-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]]
--- 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 \<open>
--- 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]
--- 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 \<subseteq> D \<Longrightarrow> a +o C \<subseteq> 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 \<subseteq> D \<Longrightarrow> a *o C \<subseteq> 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
--- 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\<mapsto>Class Base))\<turnstile>
+schematic_goal wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile>
Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\<surd>"
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\<turnstile>s0 -test-> ?s"
apply (unfold test_def)
--- 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 "\<forall>x. x = ?x"
+schematic_goal "\<forall>x. x = ?x"
nitpick [expect = genuine]
oops
-schematic_lemma "\<exists>x. x = ?x"
+schematic_goal "\<exists>x. x = ?x"
nitpick [expect = none]
by auto
-schematic_lemma "\<exists>x::'a \<Rightarrow> 'b. x = ?x"
+schematic_goal "\<exists>x::'a \<Rightarrow> 'b. x = ?x"
nitpick [expect = none]
by auto
-schematic_lemma "\<forall>x. ?x = ?y"
+schematic_goal "\<forall>x. ?x = ?y"
nitpick [expect = none]
by auto
-schematic_lemma "\<exists>x. ?x = ?y"
+schematic_goal "\<exists>x. ?x = ?y"
nitpick [expect = none]
by auto
--- 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
--- 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
--- 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
--- 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
--- 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 \<turnstile> Abs (Abs (Abs (Var 1 \<degree> (Var 2 \<degree> Var 1 \<degree> Var 0)))) : ?T"
+schematic_goal "e \<turnstile> Abs (Abs (Abs (Var 1 \<degree> (Var 2 \<degree> Var 1 \<degree> Var 0)))) : ?T"
by force
-schematic_lemma "e \<turnstile> Abs (Abs (Abs (Var 2 \<degree> Var 0 \<degree> (Var 1 \<degree> Var 0)))) : ?T"
+schematic_goal "e \<turnstile> Abs (Abs (Abs (Var 2 \<degree> Var 0 \<degree> (Var 1 \<degree> Var 0)))) : ?T"
by force
--- 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)
--- 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) &
(\<forall>x y. killed x y --> hates x y & ~richer x y) &
(\<forall>x. hates agatha x --> ~hates charles x) &
--- a/src/HOL/ex/Groebner_Examples.thy 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
--- 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
--- 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 \<Rightarrow> ?'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b}
= finite ((\<lambda>(b :: ?'B, a:: ?'A). Pair_Rep a b) ` (UNIV \<times> UNIV))"
by simp
--- 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 \<noteq> b \<Longrightarrow> a \<in> ?X \<and> b \<notin> ?X"
+schematic_goal "a \<noteq> b \<Longrightarrow> a \<in> ?X \<and> b \<notin> ?X"
by blast
@@ -61,15 +61,15 @@
-- {* Requires best-first search because it is undirectional. *}
by best
-schematic_lemma "\<forall>f:: 'a \<Rightarrow> 'a set. \<forall>x. f x \<noteq> ?S f"
+schematic_goal "\<forall>f:: 'a \<Rightarrow> 'a set. \<forall>x. f x \<noteq> ?S f"
-- {*This form displays the diagonal term. *}
by best
-schematic_lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
+schematic_goal "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
-- {* This form exploits the set constructs. *}
by (rule notI, erule rangeE, best)
-schematic_lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
+schematic_goal "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
-- {* Or just this! *}
by best
--- 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 "\<And>(y::?'b::size). size (?x::?'a::size) \<le> size y + size ?x"
+schematic_goal "\<And>(y::?'b::size). size (?x::?'a::size) \<le> size y + size ?x"
by (tactic {* test @{context} [@{simproc natle_cancel_sums}] *}) (rule le0)
(* TODO: test more simprocs with schematic variables *)
--- 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 =
--- 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"
--- /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)))
+ }
+ }
+}
--- 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
--- 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
--- 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 \<lesssim> A \<union> B" .
qed
-schematic_lemma paired_bij: "?f \<in> bij({{y,z}. y \<in> x}, x)"
+schematic_goal paired_bij: "?f \<in> bij({{y,z}. y \<in> x}, x)"
apply (rule RepFun_bijective)
apply (simp add: doubleton_eq_iff, blast)
done
--- a/src/ZF/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 \<open>@{text combine_numerals_prod} (products of separate literals)\<close>
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
--- 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\<open>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.\<close>
-schematic_lemma (in reflection)
+schematic_goal (in reflection)
"Reflects(?Cl,
\<lambda>x. \<exists>y. M(y) & x \<in> y,
\<lambda>a x. \<exists>y\<in>Mset(a). x \<in> y)"
@@ -285,7 +285,7 @@
text\<open>Example 2\<close>
-schematic_lemma (in reflection)
+schematic_goal (in reflection)
"Reflects(?Cl,
\<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) \<longrightarrow> z \<subseteq> x \<longrightarrow> z \<in> y),
\<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x \<longrightarrow> z \<in> y)"
@@ -302,14 +302,14 @@
by fast
text\<open>Example 2''. We expand the subset relation.\<close>
-schematic_lemma (in reflection)
+schematic_goal (in reflection)
"Reflects(?Cl,
\<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) \<longrightarrow> (\<forall>w. M(w) \<longrightarrow> w\<in>z \<longrightarrow> w\<in>x) \<longrightarrow> z\<in>y),
\<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). (\<forall>w\<in>Mset(a). w\<in>z \<longrightarrow> w\<in>x) \<longrightarrow> z\<in>y)"
by fast
text\<open>Example 2'''. Single-step version, to reveal the reflecting class.\<close>
-schematic_lemma (in reflection)
+schematic_goal (in reflection)
"Reflects(?Cl,
\<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) \<longrightarrow> z \<subseteq> x \<longrightarrow> z \<in> y),
\<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x \<longrightarrow> z \<in> y)"
@@ -329,21 +329,21 @@
text\<open>Example 3. Warning: the following examples make sense only
if @{term P} is quantifier-free, since it is not being relativized.\<close>
-schematic_lemma (in reflection)
+schematic_goal (in reflection)
"Reflects(?Cl,
\<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) \<longrightarrow> z \<in> y \<longleftrightarrow> z \<in> x & P(z)),
\<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<in> y \<longleftrightarrow> z \<in> x & P(z))"
by fast
text\<open>Example 3'\<close>
-schematic_lemma (in reflection)
+schematic_goal (in reflection)
"Reflects(?Cl,
\<lambda>x. \<exists>y. M(y) & y = Collect(x,P),
\<lambda>a x. \<exists>y\<in>Mset(a). y = Collect(x,P))"
by fast
text\<open>Example 3''\<close>
-schematic_lemma (in reflection)
+schematic_goal (in reflection)
"Reflects(?Cl,
\<lambda>x. \<exists>y. M(y) & y = Replace(x,P),
\<lambda>a x. \<exists>y\<in>Mset(a). y = Replace(x,P))"
@@ -351,7 +351,7 @@
text\<open>Example 4: Axiom of Choice. Possibly wrong, since @{text \<Pi>} needs
to be relativized.\<close>
-schematic_lemma (in reflection)
+schematic_goal (in reflection)
"Reflects(?Cl,
\<lambda>A. 0\<notin>A \<longrightarrow> (\<exists>f. M(f) & f \<in> (\<Pi> X \<in> A. X)),
\<lambda>a A. 0\<notin>A \<longrightarrow> (\<exists>f\<in>Mset(a). f \<in> (\<Pi> X \<in> A. X)))"
--- 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\<open>trivial example of term synthesis: apparently hard for some provers!\<close>
-schematic_lemma "a \<noteq> b ==> a:?X & b \<notin> ?X"
+schematic_goal "a \<noteq> b ==> a:?X & b \<notin> ?X"
by blast
text\<open>Nice blast benchmark. Proved in 0.3s; old tactics can't manage it!\<close>