fewer aliases for toplevel theorem statements;
authorwenzelm
Tue Oct 06 15:14:28 2015 +0200 (2015-10-06)
changeset 613374645502c3c64
parent 61336 fa4ebbd350ae
child 61338 de610e8df459
fewer aliases for toplevel theorem statements;
NEWS
lib/Tools/update_theorems
src/CCL/Fix.thy
src/CCL/Wfd.thy
src/CTT/Arith.thy
src/CTT/ex/Elimination.thy
src/CTT/ex/Synthesis.thy
src/CTT/ex/Typechecking.thy
src/Cube/Example.thy
src/Doc/Codegen/Evaluation.thy
src/Doc/Isar_Ref/Proof.thy
src/Doc/Isar_Ref/Spec.thy
src/FOL/ex/Classical.thy
src/FOL/ex/Prolog.thy
src/FOL/ex/Quantifiers_Cla.thy
src/FOL/ex/Quantifiers_Int.thy
src/FOLP/FOLP.thy
src/FOLP/IFOLP.thy
src/FOLP/ex/Classical.thy
src/FOLP/ex/Foundation.thy
src/FOLP/ex/If.thy
src/FOLP/ex/Intro.thy
src/FOLP/ex/Intuitionistic.thy
src/FOLP/ex/Nat.thy
src/FOLP/ex/Propositional_Cla.thy
src/FOLP/ex/Propositional_Int.thy
src/FOLP/ex/Quantifiers_Cla.thy
src/FOLP/ex/Quantifiers_Int.thy
src/HOL/Bali/Example.thy
src/HOL/Eisbach/Tests.thy
src/HOL/Groups.thy
src/HOL/Hahn_Banach/Vector_Space.thy
src/HOL/IMP/Big_Step.thy
src/HOL/Inductive.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Omega_Words_Fun.thy
src/HOL/Library/Prefix_Order.thy
src/HOL/Library/Set_Algebras.thy
src/HOL/MicroJava/J/Example.thy
src/HOL/Nitpick_Examples/Core_Nits.thy
src/HOL/Nitpick_Examples/Refute_Nits.thy
src/HOL/Prolog/Func.thy
src/HOL/Prolog/Test.thy
src/HOL/Prolog/Type.thy
src/HOL/Proofs/Lambda/LambdaType.thy
src/HOL/Wellfounded.thy
src/HOL/ex/Classical.thy
src/HOL/ex/Groebner_Examples.thy
src/HOL/ex/Refute_Examples.thy
src/HOL/ex/Set_Comprehension_Pointfree_Examples.thy
src/HOL/ex/Set_Theory.thy
src/HOL/ex/Simproc_Tests.thy
src/Pure/Isar/isar_syn.ML
src/Pure/Pure.thy
src/Pure/Tools/update_theorems.scala
src/Pure/build-jars
src/Sequents/LK/Quantifiers.thy
src/ZF/AC/Cardinal_aux.thy
src/ZF/Bin.thy
src/ZF/Constructible/Reflection.thy
src/ZF/ex/misc.thy
     1.1 --- a/NEWS	Tue Oct 06 13:31:44 2015 +0200
     1.2 +++ b/NEWS	Tue Oct 06 15:14:28 2015 +0200
     1.3 @@ -7,6 +7,19 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** General ***
     1.8 +
     1.9 +* Toplevel theorem statements have been simplified as follows:
    1.10 +
    1.11 +  theorems             ~>  lemmas
    1.12 +  schematic_lemma      ~>  schematic_goal
    1.13 +  schematic_theorem    ~>  schematic_goal
    1.14 +  schematic_corollary  ~>  schematic_goal
    1.15 +
    1.16 +Command-line tool "isabelle update_theorems" updates theory sources
    1.17 +accordingly.
    1.18 +
    1.19 +
    1.20  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.21  
    1.22  * Improved scheduling for urgent print tasks (e.g. command state output,
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/lib/Tools/update_theorems	Tue Oct 06 15:14:28 2015 +0200
     2.3 @@ -0,0 +1,40 @@
     2.4 +#!/usr/bin/env bash
     2.5 +#
     2.6 +# Author: Makarius
     2.7 +#
     2.8 +# DESCRIPTION: update toplevel theorem keywords
     2.9 +
    2.10 +
    2.11 +## diagnostics
    2.12 +
    2.13 +PRG="$(basename "$0")"
    2.14 +
    2.15 +function usage()
    2.16 +{
    2.17 +  echo
    2.18 +  echo "Usage: isabelle $PRG [FILES|DIRS...]"
    2.19 +  echo
    2.20 +  echo "  Recursively find .thy files and update toplevel theorem keywords:"
    2.21 +  echo
    2.22 +  echo "    theorems             ~>  lemmas"
    2.23 +  echo "    schematic_theorem    ~>  schematic_goal"
    2.24 +  echo "    schematic_lemma      ~>  schematic_goal"
    2.25 +  echo "    schematic_corollary  ~>  schematic_goal"
    2.26 +  echo
    2.27 +  echo "  Old versions of files are preserved by appending \"~~\"."
    2.28 +  echo
    2.29 +  exit 1
    2.30 +}
    2.31 +
    2.32 +
    2.33 +## process command line
    2.34 +
    2.35 +[ "$#" -eq 0 -o "$1" = "-?" ] && usage
    2.36 +
    2.37 +SPECS="$@"; shift "$#"
    2.38 +
    2.39 +
    2.40 +## main
    2.41 +
    2.42 +find $SPECS -name \*.thy -print0 | \
    2.43 +  xargs -0 "$ISABELLE_TOOL" java isabelle.Update_Theorems
     3.1 --- a/src/CCL/Fix.thy	Tue Oct 06 13:31:44 2015 +0200
     3.2 +++ b/src/CCL/Fix.thy	Tue Oct 06 15:14:28 2015 +0200
     3.3 @@ -93,7 +93,7 @@
     3.4  
     3.5  (* All fixed points are lam-expressions *)
     3.6  
     3.7 -schematic_lemma idgenfp_lam: "idgen(d) = d \<Longrightarrow> d = lam x. ?f(x)"
     3.8 +schematic_goal idgenfp_lam: "idgen(d) = d \<Longrightarrow> d = lam x. ?f(x)"
     3.9    apply (unfold idgen_def)
    3.10    apply (erule ssubst)
    3.11    apply (rule refl)
    3.12 @@ -125,7 +125,7 @@
    3.13    apply simp
    3.14    done
    3.15  
    3.16 -schematic_lemma po_eta_lemma: "idgen(d) = d \<Longrightarrow> d = lam x. ?f(x)"
    3.17 +schematic_goal po_eta_lemma: "idgen(d) = d \<Longrightarrow> d = lam x. ?f(x)"
    3.18    apply (unfold idgen_def)
    3.19    apply (erule sym)
    3.20    done
     4.1 --- a/src/CCL/Wfd.thy	Tue Oct 06 13:31:44 2015 +0200
     4.2 +++ b/src/CCL/Wfd.thy	Tue Oct 06 15:14:28 2015 +0200
     4.3 @@ -568,29 +568,29 @@
     4.4  
     4.5  subsection \<open>Factorial\<close>
     4.6  
     4.7 -schematic_lemma
     4.8 +schematic_goal
     4.9    "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))))  
    4.10     in f(succ(succ(zero))) ---> ?a"
    4.11    by eval
    4.12  
    4.13 -schematic_lemma
    4.14 +schematic_goal
    4.15    "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))))  
    4.16     in f(succ(succ(succ(zero)))) ---> ?a"
    4.17    by eval
    4.18  
    4.19  subsection \<open>Less Than Or Equal\<close>
    4.20  
    4.21 -schematic_lemma
    4.22 +schematic_goal
    4.23    "letrec f p be split(p,\<lambda>m n. ncase(m,true,\<lambda>x. ncase(n,false,\<lambda>y. f(<x,y>))))
    4.24     in f(<succ(zero), succ(zero)>) ---> ?a"
    4.25    by eval
    4.26  
    4.27 -schematic_lemma
    4.28 +schematic_goal
    4.29    "letrec f p be split(p,\<lambda>m n. ncase(m,true,\<lambda>x. ncase(n,false,\<lambda>y. f(<x,y>))))
    4.30     in f(<succ(zero), succ(succ(succ(succ(zero))))>) ---> ?a"
    4.31    by eval
    4.32  
    4.33 -schematic_lemma
    4.34 +schematic_goal
    4.35    "letrec f p be split(p,\<lambda>m n. ncase(m,true,\<lambda>x. ncase(n,false,\<lambda>y. f(<x,y>))))
    4.36     in f(<succ(succ(succ(succ(succ(zero))))), succ(succ(succ(succ(zero))))>) ---> ?a"
    4.37    by eval
    4.38 @@ -598,12 +598,12 @@
    4.39  
    4.40  subsection \<open>Reverse\<close>
    4.41  
    4.42 -schematic_lemma
    4.43 +schematic_goal
    4.44    "letrec id l be lcase(l,[],\<lambda>x xs. x$id(xs))  
    4.45     in id(zero$succ(zero)$[]) ---> ?a"
    4.46    by eval
    4.47  
    4.48 -schematic_lemma
    4.49 +schematic_goal
    4.50    "letrec rev l be lcase(l,[],\<lambda>x xs. lrec(rev(xs),x$[],\<lambda>y ys g. y$g))  
    4.51     in rev(zero$succ(zero)$(succ((lam x. x)`succ(zero)))$([])) ---> ?a"
    4.52    by eval
     5.1 --- a/src/CTT/Arith.thy	Tue Oct 06 13:31:44 2015 +0200
     5.2 +++ b/src/CTT/Arith.thy	Tue Oct 06 15:14:28 2015 +0200
     5.3 @@ -266,7 +266,7 @@
     5.4  (*Addition is the inverse of subtraction: if b<=x then b#+(x-b) = x.
     5.5    An example of induction over a quantified formula (a product).
     5.6    Uses rewriting with a quantified, implicative inductive hypothesis.*)
     5.7 -schematic_lemma add_diff_inverse_lemma:
     5.8 +schematic_goal add_diff_inverse_lemma:
     5.9    "b:N \<Longrightarrow> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)"
    5.10  apply (NE b)
    5.11  (*strip one "universal quantifier" but not the "implication"*)
    5.12 @@ -337,7 +337,7 @@
    5.13  done
    5.14  
    5.15  (*If a+b=0 then a=0.   Surprisingly tedious*)
    5.16 -schematic_lemma add_eq0_lemma: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> ?c : PROD u: Eq(N,a#+b,0) .  Eq(N,a,0)"
    5.17 +schematic_goal add_eq0_lemma: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> ?c : PROD u: Eq(N,a#+b,0) .  Eq(N,a,0)"
    5.18  apply (NE a)
    5.19  apply (rule_tac [3] replace_type)
    5.20  apply arith_rew
    5.21 @@ -357,7 +357,7 @@
    5.22  done
    5.23  
    5.24  (*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *)
    5.25 -schematic_lemma absdiff_eq0_lem:
    5.26 +schematic_goal absdiff_eq0_lem:
    5.27    "\<lbrakk>a:N; b:N; a |-| b = 0 : N\<rbrakk> \<Longrightarrow> ?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)"
    5.28  apply (unfold absdiff_def)
    5.29  apply intr
     6.1 --- a/src/CTT/ex/Elimination.thy	Tue Oct 06 13:31:44 2015 +0200
     6.2 +++ b/src/CTT/ex/Elimination.thy	Tue Oct 06 15:14:28 2015 +0200
     6.3 @@ -14,41 +14,41 @@
     6.4  
     6.5  text "This finds the functions fst and snd!"
     6.6  
     6.7 -schematic_lemma [folded basic_defs]: "A type \<Longrightarrow> ?a : (A*A) --> A"
     6.8 +schematic_goal [folded basic_defs]: "A type \<Longrightarrow> ?a : (A*A) --> A"
     6.9  apply pc
    6.10  done
    6.11  
    6.12 -schematic_lemma [folded basic_defs]: "A type \<Longrightarrow> ?a : (A*A) --> A"
    6.13 +schematic_goal [folded basic_defs]: "A type \<Longrightarrow> ?a : (A*A) --> A"
    6.14  apply pc
    6.15  back
    6.16  done
    6.17  
    6.18  text "Double negation of the Excluded Middle"
    6.19 -schematic_lemma "A type \<Longrightarrow> ?a : ((A + (A-->F)) --> F) --> F"
    6.20 +schematic_goal "A type \<Longrightarrow> ?a : ((A + (A-->F)) --> F) --> F"
    6.21  apply intr
    6.22  apply (rule ProdE)
    6.23  apply assumption
    6.24  apply pc
    6.25  done
    6.26  
    6.27 -schematic_lemma "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : (A*B) \<longrightarrow> (B*A)"
    6.28 +schematic_goal "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : (A*B) \<longrightarrow> (B*A)"
    6.29  apply pc
    6.30  done
    6.31  (*The sequent version (ITT) could produce an interesting alternative
    6.32    by backtracking.  No longer.*)
    6.33  
    6.34  text "Binary sums and products"
    6.35 -schematic_lemma "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A+B --> C) --> (A-->C) * (B-->C)"
    6.36 +schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A+B --> C) --> (A-->C) * (B-->C)"
    6.37  apply pc
    6.38  done
    6.39  
    6.40  (*A distributive law*)
    6.41 -schematic_lemma "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : A * (B+C)  -->  (A*B + A*C)"
    6.42 +schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : A * (B+C)  -->  (A*B + A*C)"
    6.43  apply pc
    6.44  done
    6.45  
    6.46  (*more general version, same proof*)
    6.47 -schematic_lemma
    6.48 +schematic_goal
    6.49    assumes "A type"
    6.50      and "\<And>x. x:A \<Longrightarrow> B(x) type"
    6.51      and "\<And>x. x:A \<Longrightarrow> C(x) type"
    6.52 @@ -57,12 +57,12 @@
    6.53  done
    6.54  
    6.55  text "Construction of the currying functional"
    6.56 -schematic_lemma "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A*B --> C) --> (A--> (B-->C))"
    6.57 +schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A*B --> C) --> (A--> (B-->C))"
    6.58  apply pc
    6.59  done
    6.60  
    6.61  (*more general goal with same proof*)
    6.62 -schematic_lemma
    6.63 +schematic_goal
    6.64    assumes "A type"
    6.65      and "\<And>x. x:A \<Longrightarrow> B(x) type"
    6.66      and "\<And>z. z: (SUM x:A. B(x)) \<Longrightarrow> C(z) type"
    6.67 @@ -72,12 +72,12 @@
    6.68  done
    6.69  
    6.70  text "Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)"
    6.71 -schematic_lemma "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A --> (B-->C)) --> (A*B --> C)"
    6.72 +schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A --> (B-->C)) --> (A*B --> C)"
    6.73  apply pc
    6.74  done
    6.75  
    6.76  (*more general goal with same proof*)
    6.77 -schematic_lemma
    6.78 +schematic_goal
    6.79    assumes "A type"
    6.80      and "\<And>x. x:A \<Longrightarrow> B(x) type"
    6.81      and "\<And>z. z: (SUM x:A . B(x)) \<Longrightarrow> C(z) type"
    6.82 @@ -87,12 +87,12 @@
    6.83  done
    6.84  
    6.85  text "Function application"
    6.86 -schematic_lemma "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : ((A --> B) * A) --> B"
    6.87 +schematic_goal "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : ((A --> B) * A) --> B"
    6.88  apply pc
    6.89  done
    6.90  
    6.91  text "Basic test of quantifier reasoning"
    6.92 -schematic_lemma
    6.93 +schematic_goal
    6.94    assumes "A type"
    6.95      and "B type"
    6.96      and "\<And>x y. \<lbrakk>x:A; y:B\<rbrakk> \<Longrightarrow> C(x,y) type"
    6.97 @@ -103,7 +103,7 @@
    6.98  done
    6.99  
   6.100  text "Martin-Lof (1984) pages 36-7: the combinator S"
   6.101 -schematic_lemma
   6.102 +schematic_goal
   6.103    assumes "A type"
   6.104      and "\<And>x. x:A \<Longrightarrow> B(x) type"
   6.105      and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type"
   6.106 @@ -113,7 +113,7 @@
   6.107  done
   6.108  
   6.109  text "Martin-Lof (1984) page 58: the axiom of disjunction elimination"
   6.110 -schematic_lemma
   6.111 +schematic_goal
   6.112    assumes "A type"
   6.113      and "B type"
   6.114      and "\<And>z. z: A+B \<Longrightarrow> C(z) type"
   6.115 @@ -123,7 +123,7 @@
   6.116  done
   6.117  
   6.118  (*towards AXIOM OF CHOICE*)
   6.119 -schematic_lemma [folded basic_defs]:
   6.120 +schematic_goal [folded basic_defs]:
   6.121    "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A --> B*C) --> (A-->B) * (A-->C)"
   6.122  apply pc
   6.123  done
   6.124 @@ -131,7 +131,7 @@
   6.125  
   6.126  (*Martin-Lof (1984) page 50*)
   6.127  text "AXIOM OF CHOICE!  Delicate use of elimination rules"
   6.128 -schematic_lemma
   6.129 +schematic_goal
   6.130    assumes "A type"
   6.131      and "\<And>x. x:A \<Longrightarrow> B(x) type"
   6.132      and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type"
   6.133 @@ -149,7 +149,7 @@
   6.134  done
   6.135  
   6.136  text "Axiom of choice.  Proof without fst, snd.  Harder still!"
   6.137 -schematic_lemma [folded basic_defs]:
   6.138 +schematic_goal [folded basic_defs]:
   6.139    assumes "A type"
   6.140      and "\<And>x. x:A \<Longrightarrow> B(x) type"
   6.141      and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type"
   6.142 @@ -176,7 +176,7 @@
   6.143  text "Example of sequent_style deduction"
   6.144  (*When splitting z:A*B, the assumption C(z) is affected;  ?a becomes
   6.145      lam u. split(u,\<lambda>v w.split(v,\<lambda>x y.lam z. <x,<y,z>>) ` w)     *)
   6.146 -schematic_lemma
   6.147 +schematic_goal
   6.148    assumes "A type"
   6.149      and "B type"
   6.150      and "\<And>z. z:A*B \<Longrightarrow> C(z) type"
     7.1 --- a/src/CTT/ex/Synthesis.thy	Tue Oct 06 13:31:44 2015 +0200
     7.2 +++ b/src/CTT/ex/Synthesis.thy	Tue Oct 06 15:14:28 2015 +0200
     7.3 @@ -10,7 +10,7 @@
     7.4  begin
     7.5  
     7.6  text "discovery of predecessor function"
     7.7 -schematic_lemma "?a : SUM pred:?A . Eq(N, pred`0, 0)
     7.8 +schematic_goal "?a : SUM pred:?A . Eq(N, pred`0, 0)
     7.9                    *  (PROD n:N. Eq(N, pred ` succ(n), n))"
    7.10  apply intr
    7.11  apply eqintr
    7.12 @@ -20,7 +20,7 @@
    7.13  done
    7.14  
    7.15  text "the function fst as an element of a function type"
    7.16 -schematic_lemma [folded basic_defs]:
    7.17 +schematic_goal [folded basic_defs]:
    7.18    "A type \<Longrightarrow> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` <i,j>, i)"
    7.19  apply intr
    7.20  apply eqintr
    7.21 @@ -34,7 +34,7 @@
    7.22  text "An interesting use of the eliminator, when"
    7.23  (*The early implementation of unification caused non-rigid path in occur check
    7.24    See following example.*)
    7.25 -schematic_lemma "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0    ,   i>)
    7.26 +schematic_goal "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0    ,   i>)
    7.27                     * Eq(?A, ?b(inr(i)), <succ(0), i>)"
    7.28  apply intr
    7.29  apply eqintr
    7.30 @@ -46,13 +46,13 @@
    7.31   This prevents the cycle in the first unification (no longer needed).
    7.32   Requires flex-flex to preserve the dependence.
    7.33   Simpler still: make ?A into a constant type N*N.*)
    7.34 -schematic_lemma "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0   ,   i>)
    7.35 +schematic_goal "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0   ,   i>)
    7.36                    *  Eq(?A(i), ?b(inr(i)), <succ(0),i>)"
    7.37  oops
    7.38  
    7.39  text "A tricky combination of when and split"
    7.40  (*Now handled easily, but caused great problems once*)
    7.41 -schematic_lemma [folded basic_defs]:
    7.42 +schematic_goal [folded basic_defs]:
    7.43    "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i)
    7.44                             *  Eq(?A, ?b(inr(<i,j>)), j)"
    7.45  apply intr
    7.46 @@ -65,18 +65,18 @@
    7.47  done
    7.48  
    7.49  (*similar but allows the type to depend on i and j*)
    7.50 -schematic_lemma "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i)
    7.51 +schematic_goal "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i)
    7.52                            *   Eq(?A(i,j), ?b(inr(<i,j>)), j)"
    7.53  oops
    7.54  
    7.55  (*similar but specifying the type N simplifies the unification problems*)
    7.56 -schematic_lemma "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)
    7.57 +schematic_goal "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)
    7.58                            *   Eq(N, ?b(inr(<i,j>)), j)"
    7.59  oops
    7.60  
    7.61  
    7.62  text "Deriving the addition operator"
    7.63 -schematic_lemma [folded arith_defs]:
    7.64 +schematic_goal [folded arith_defs]:
    7.65    "?c : PROD n:N. Eq(N, ?f(0,n), n)
    7.66                    *  (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))"
    7.67  apply intr
    7.68 @@ -86,7 +86,7 @@
    7.69  done
    7.70  
    7.71  text "The addition function -- using explicit lambdas"
    7.72 -schematic_lemma [folded arith_defs]:
    7.73 +schematic_goal [folded arith_defs]:
    7.74    "?c : SUM plus : ?A .
    7.75           PROD x:N. Eq(N, plus`0`x, x)
    7.76                  *  (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))"
     8.1 --- a/src/CTT/ex/Typechecking.thy	Tue Oct 06 13:31:44 2015 +0200
     8.2 +++ b/src/CTT/ex/Typechecking.thy	Tue Oct 06 15:14:28 2015 +0200
     8.3 @@ -11,18 +11,18 @@
     8.4  
     8.5  subsection \<open>Single-step proofs: verifying that a type is well-formed\<close>
     8.6  
     8.7 -schematic_lemma "?A type"
     8.8 +schematic_goal "?A type"
     8.9  apply (rule form_rls)
    8.10  done
    8.11  
    8.12 -schematic_lemma "?A type"
    8.13 +schematic_goal "?A type"
    8.14  apply (rule form_rls)
    8.15  back
    8.16  apply (rule form_rls)
    8.17  apply (rule form_rls)
    8.18  done
    8.19  
    8.20 -schematic_lemma "PROD z:?A . N + ?B(z) type"
    8.21 +schematic_goal "PROD z:?A . N + ?B(z) type"
    8.22  apply (rule form_rls)
    8.23  apply (rule form_rls)
    8.24  apply (rule form_rls)
    8.25 @@ -37,30 +37,30 @@
    8.26  apply form
    8.27  done
    8.28  
    8.29 -schematic_lemma "<0, succ(0)> : ?A"
    8.30 +schematic_goal "<0, succ(0)> : ?A"
    8.31  apply intr
    8.32  done
    8.33  
    8.34 -schematic_lemma "PROD w:N . Eq(?A,w,w) type"
    8.35 +schematic_goal "PROD w:N . Eq(?A,w,w) type"
    8.36  apply typechk
    8.37  done
    8.38  
    8.39 -schematic_lemma "PROD x:N . PROD y:N . Eq(?A,x,y) type"
    8.40 +schematic_goal "PROD x:N . PROD y:N . Eq(?A,x,y) type"
    8.41  apply typechk
    8.42  done
    8.43  
    8.44  text "typechecking an application of fst"
    8.45 -schematic_lemma "(lam u. split(u, \<lambda>v w. v)) ` <0, succ(0)> : ?A"
    8.46 +schematic_goal "(lam u. split(u, \<lambda>v w. v)) ` <0, succ(0)> : ?A"
    8.47  apply typechk
    8.48  done
    8.49  
    8.50  text "typechecking the predecessor function"
    8.51 -schematic_lemma "lam n. rec(n, 0, \<lambda>x y. x) : ?A"
    8.52 +schematic_goal "lam n. rec(n, 0, \<lambda>x y. x) : ?A"
    8.53  apply typechk
    8.54  done
    8.55  
    8.56  text "typechecking the addition function"
    8.57 -schematic_lemma "lam n. lam m. rec(n, m, \<lambda>x y. succ(y)) : ?A"
    8.58 +schematic_goal "lam n. lam m. rec(n, m, \<lambda>x y. succ(y)) : ?A"
    8.59  apply typechk
    8.60  done
    8.61  
    8.62 @@ -69,18 +69,18 @@
    8.63  method_setup N =
    8.64    \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (TRYALL (resolve_tac ctxt @{thms NF})))\<close>
    8.65  
    8.66 -schematic_lemma "lam w. <w,w> : ?A"
    8.67 +schematic_goal "lam w. <w,w> : ?A"
    8.68  apply typechk
    8.69  apply N
    8.70  done
    8.71  
    8.72 -schematic_lemma "lam x. lam y. x : ?A"
    8.73 +schematic_goal "lam x. lam y. x : ?A"
    8.74  apply typechk
    8.75  apply N
    8.76  done
    8.77  
    8.78  text "typechecking fst (as a function object)"
    8.79 -schematic_lemma "lam i. split(i, \<lambda>j k. j) : ?A"
    8.80 +schematic_goal "lam i. split(i, \<lambda>j k. j) : ?A"
    8.81  apply typechk
    8.82  apply N
    8.83  done
     9.1 --- a/src/Cube/Example.thy	Tue Oct 06 13:31:44 2015 +0200
     9.2 +++ b/src/Cube/Example.thy	Tue Oct 06 15:14:28 2015 +0200
     9.3 @@ -25,98 +25,98 @@
     9.4  
     9.5  subsection \<open>Simple types\<close>
     9.6  
     9.7 -schematic_lemma "A:* \<turnstile> A\<rightarrow>A : ?T"
     9.8 +schematic_goal "A:* \<turnstile> A\<rightarrow>A : ?T"
     9.9    by (depth_solve rules)
    9.10  
    9.11 -schematic_lemma "A:* \<turnstile> \<Lambda> a:A. a : ?T"
    9.12 +schematic_goal "A:* \<turnstile> \<Lambda> a:A. a : ?T"
    9.13    by (depth_solve rules)
    9.14  
    9.15 -schematic_lemma "A:* B:* b:B \<turnstile> \<Lambda> x:A. b : ?T"
    9.16 +schematic_goal "A:* B:* b:B \<turnstile> \<Lambda> x:A. b : ?T"
    9.17    by (depth_solve rules)
    9.18  
    9.19 -schematic_lemma "A:* b:A \<turnstile> (\<Lambda> a:A. a)^b: ?T"
    9.20 +schematic_goal "A:* b:A \<turnstile> (\<Lambda> a:A. a)^b: ?T"
    9.21    by (depth_solve rules)
    9.22  
    9.23 -schematic_lemma "A:* B:* c:A b:B \<turnstile> (\<Lambda> x:A. b)^ c: ?T"
    9.24 +schematic_goal "A:* B:* c:A b:B \<turnstile> (\<Lambda> x:A. b)^ c: ?T"
    9.25    by (depth_solve rules)
    9.26  
    9.27 -schematic_lemma "A:* B:* \<turnstile> \<Lambda> a:A. \<Lambda> b:B. a : ?T"
    9.28 +schematic_goal "A:* B:* \<turnstile> \<Lambda> a:A. \<Lambda> b:B. a : ?T"
    9.29    by (depth_solve rules)
    9.30  
    9.31  
    9.32  subsection \<open>Second-order types\<close>
    9.33  
    9.34 -schematic_lemma (in L2) "\<turnstile> \<Lambda> A:*. \<Lambda> a:A. a : ?T"
    9.35 +schematic_goal (in L2) "\<turnstile> \<Lambda> A:*. \<Lambda> a:A. a : ?T"
    9.36    by (depth_solve rules)
    9.37  
    9.38 -schematic_lemma (in L2) "A:* \<turnstile> (\<Lambda> B:*.\<Lambda> b:B. b)^A : ?T"
    9.39 +schematic_goal (in L2) "A:* \<turnstile> (\<Lambda> B:*.\<Lambda> b:B. b)^A : ?T"
    9.40    by (depth_solve rules)
    9.41  
    9.42 -schematic_lemma (in L2) "A:* b:A \<turnstile> (\<Lambda> B:*.\<Lambda> b:B. b) ^ A ^ b: ?T"
    9.43 +schematic_goal (in L2) "A:* b:A \<turnstile> (\<Lambda> B:*.\<Lambda> b:B. b) ^ A ^ b: ?T"
    9.44    by (depth_solve rules)
    9.45  
    9.46 -schematic_lemma (in L2) "\<turnstile> \<Lambda> B:*.\<Lambda> a:(\<Pi> A:*.A).a ^ ((\<Pi> A:*.A)\<rightarrow>B) ^ a: ?T"
    9.47 +schematic_goal (in L2) "\<turnstile> \<Lambda> B:*.\<Lambda> a:(\<Pi> A:*.A).a ^ ((\<Pi> A:*.A)\<rightarrow>B) ^ a: ?T"
    9.48    by (depth_solve rules)
    9.49  
    9.50  
    9.51  subsection \<open>Weakly higher-order propositional logic\<close>
    9.52  
    9.53 -schematic_lemma (in Lomega) "\<turnstile> \<Lambda> A:*.A\<rightarrow>A : ?T"
    9.54 +schematic_goal (in Lomega) "\<turnstile> \<Lambda> A:*.A\<rightarrow>A : ?T"
    9.55    by (depth_solve rules)
    9.56  
    9.57 -schematic_lemma (in Lomega) "B:* \<turnstile> (\<Lambda> A:*.A\<rightarrow>A) ^ B : ?T"
    9.58 +schematic_goal (in Lomega) "B:* \<turnstile> (\<Lambda> A:*.A\<rightarrow>A) ^ B : ?T"
    9.59    by (depth_solve rules)
    9.60  
    9.61 -schematic_lemma (in Lomega) "B:* b:B \<turnstile> (\<Lambda> y:B. b): ?T"
    9.62 +schematic_goal (in Lomega) "B:* b:B \<turnstile> (\<Lambda> y:B. b): ?T"
    9.63    by (depth_solve rules)
    9.64  
    9.65 -schematic_lemma (in Lomega) "A:* F:*\<rightarrow>* \<turnstile> F^(F^A): ?T"
    9.66 +schematic_goal (in Lomega) "A:* F:*\<rightarrow>* \<turnstile> F^(F^A): ?T"
    9.67    by (depth_solve rules)
    9.68  
    9.69 -schematic_lemma (in Lomega) "A:* \<turnstile> \<Lambda> F:*\<rightarrow>*.F^(F^A): ?T"
    9.70 +schematic_goal (in Lomega) "A:* \<turnstile> \<Lambda> F:*\<rightarrow>*.F^(F^A): ?T"
    9.71    by (depth_solve rules)
    9.72  
    9.73  
    9.74  subsection \<open>LP\<close>
    9.75  
    9.76 -schematic_lemma (in LP) "A:* \<turnstile> A \<rightarrow> * : ?T"
    9.77 +schematic_goal (in LP) "A:* \<turnstile> A \<rightarrow> * : ?T"
    9.78    by (depth_solve rules)
    9.79  
    9.80 -schematic_lemma (in LP) "A:* P:A\<rightarrow>* a:A \<turnstile> P^a: ?T"
    9.81 +schematic_goal (in LP) "A:* P:A\<rightarrow>* a:A \<turnstile> P^a: ?T"
    9.82    by (depth_solve rules)
    9.83  
    9.84 -schematic_lemma (in LP) "A:* P:A\<rightarrow>A\<rightarrow>* a:A \<turnstile> \<Pi> a:A. P^a^a: ?T"
    9.85 +schematic_goal (in LP) "A:* P:A\<rightarrow>A\<rightarrow>* a:A \<turnstile> \<Pi> a:A. P^a^a: ?T"
    9.86    by (depth_solve rules)
    9.87  
    9.88 -schematic_lemma (in LP) "A:* P:A\<rightarrow>* Q:A\<rightarrow>* \<turnstile> \<Pi> a:A. P^a \<rightarrow> Q^a: ?T"
    9.89 +schematic_goal (in LP) "A:* P:A\<rightarrow>* Q:A\<rightarrow>* \<turnstile> \<Pi> a:A. P^a \<rightarrow> Q^a: ?T"
    9.90    by (depth_solve rules)
    9.91  
    9.92 -schematic_lemma (in LP) "A:* P:A\<rightarrow>* \<turnstile> \<Pi> a:A. P^a \<rightarrow> P^a: ?T"
    9.93 +schematic_goal (in LP) "A:* P:A\<rightarrow>* \<turnstile> \<Pi> a:A. P^a \<rightarrow> P^a: ?T"
    9.94    by (depth_solve rules)
    9.95  
    9.96 -schematic_lemma (in LP) "A:* P:A\<rightarrow>* \<turnstile> \<Lambda> a:A. \<Lambda> x:P^a. x: ?T"
    9.97 +schematic_goal (in LP) "A:* P:A\<rightarrow>* \<turnstile> \<Lambda> a:A. \<Lambda> x:P^a. x: ?T"
    9.98    by (depth_solve rules)
    9.99  
   9.100 -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"
   9.101 +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"
   9.102    by (depth_solve rules)
   9.103  
   9.104 -schematic_lemma (in LP) "A:* P:A\<rightarrow>* Q:* a0:A \<turnstile>
   9.105 +schematic_goal (in LP) "A:* P:A\<rightarrow>* Q:* a0:A \<turnstile>
   9.106          \<Lambda> x:\<Pi> a:A. P^a\<rightarrow>Q. \<Lambda> y:\<Pi> a:A. P^a. x^a0^(y^a0): ?T"
   9.107    by (depth_solve rules)
   9.108  
   9.109  
   9.110  subsection \<open>Omega-order types\<close>
   9.111  
   9.112 -schematic_lemma (in L2) "A:* B:* \<turnstile> \<Pi> C:*.(A\<rightarrow>B\<rightarrow>C)\<rightarrow>C : ?T"
   9.113 +schematic_goal (in L2) "A:* B:* \<turnstile> \<Pi> C:*.(A\<rightarrow>B\<rightarrow>C)\<rightarrow>C : ?T"
   9.114    by (depth_solve rules)
   9.115  
   9.116 -schematic_lemma (in Lomega2) "\<turnstile> \<Lambda> A:*.\<Lambda> B:*.\<Pi> C:*.(A\<rightarrow>B\<rightarrow>C)\<rightarrow>C : ?T"
   9.117 +schematic_goal (in Lomega2) "\<turnstile> \<Lambda> A:*.\<Lambda> B:*.\<Pi> C:*.(A\<rightarrow>B\<rightarrow>C)\<rightarrow>C : ?T"
   9.118    by (depth_solve rules)
   9.119  
   9.120 -schematic_lemma (in Lomega2) "\<turnstile> \<Lambda> A:*.\<Lambda> B:*.\<Lambda> x:A. \<Lambda> y:B. x : ?T"
   9.121 +schematic_goal (in Lomega2) "\<turnstile> \<Lambda> A:*.\<Lambda> B:*.\<Lambda> x:A. \<Lambda> y:B. x : ?T"
   9.122    by (depth_solve rules)
   9.123  
   9.124 -schematic_lemma (in Lomega2) "A:* B:* \<turnstile> ?p : (A\<rightarrow>B) \<rightarrow> ((B\<rightarrow>\<Pi> P:*.P)\<rightarrow>(A\<rightarrow>\<Pi> P:*.P))"
   9.125 +schematic_goal (in Lomega2) "A:* B:* \<turnstile> ?p : (A\<rightarrow>B) \<rightarrow> ((B\<rightarrow>\<Pi> P:*.P)\<rightarrow>(A\<rightarrow>\<Pi> P:*.P))"
   9.126    apply (strip_asms rules)
   9.127    apply (rule lam_ss)
   9.128      apply (depth_solve1 rules)
   9.129 @@ -140,14 +140,14 @@
   9.130  
   9.131  subsection \<open>Second-order Predicate Logic\<close>
   9.132  
   9.133 -schematic_lemma (in LP2) "A:* P:A\<rightarrow>* \<turnstile> \<Lambda> a:A. P^a\<rightarrow>(\<Pi> A:*.A) : ?T"
   9.134 +schematic_goal (in LP2) "A:* P:A\<rightarrow>* \<turnstile> \<Lambda> a:A. P^a\<rightarrow>(\<Pi> A:*.A) : ?T"
   9.135    by (depth_solve rules)
   9.136  
   9.137 -schematic_lemma (in LP2) "A:* P:A\<rightarrow>A\<rightarrow>* \<turnstile>
   9.138 +schematic_goal (in LP2) "A:* P:A\<rightarrow>A\<rightarrow>* \<turnstile>
   9.139      (\<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"
   9.140    by (depth_solve rules)
   9.141  
   9.142 -schematic_lemma (in LP2) "A:* P:A\<rightarrow>A\<rightarrow>* \<turnstile>
   9.143 +schematic_goal (in LP2) "A:* P:A\<rightarrow>A\<rightarrow>* \<turnstile>
   9.144      ?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"
   9.145    -- \<open>Antisymmetry implies irreflexivity:\<close>
   9.146    apply (strip_asms rules)
   9.147 @@ -169,22 +169,22 @@
   9.148  
   9.149  subsection \<open>LPomega\<close>
   9.150  
   9.151 -schematic_lemma (in LPomega) "A:* \<turnstile> \<Lambda> P:A\<rightarrow>A\<rightarrow>*.\<Lambda> a:A. P^a^a : ?T"
   9.152 +schematic_goal (in LPomega) "A:* \<turnstile> \<Lambda> P:A\<rightarrow>A\<rightarrow>*.\<Lambda> a:A. P^a^a : ?T"
   9.153    by (depth_solve rules)
   9.154  
   9.155 -schematic_lemma (in LPomega) "\<turnstile> \<Lambda> A:*.\<Lambda> P:A\<rightarrow>A\<rightarrow>*.\<Lambda> a:A. P^a^a : ?T"
   9.156 +schematic_goal (in LPomega) "\<turnstile> \<Lambda> A:*.\<Lambda> P:A\<rightarrow>A\<rightarrow>*.\<Lambda> a:A. P^a^a : ?T"
   9.157    by (depth_solve rules)
   9.158  
   9.159  
   9.160  subsection \<open>Constructions\<close>
   9.161  
   9.162 -schematic_lemma (in CC) "\<turnstile> \<Lambda> A:*.\<Lambda> P:A\<rightarrow>*.\<Lambda> a:A. P^a\<rightarrow>\<Pi> P:*.P: ?T"
   9.163 +schematic_goal (in CC) "\<turnstile> \<Lambda> A:*.\<Lambda> P:A\<rightarrow>*.\<Lambda> a:A. P^a\<rightarrow>\<Pi> P:*.P: ?T"
   9.164    by (depth_solve rules)
   9.165  
   9.166 -schematic_lemma (in CC) "\<turnstile> \<Lambda> A:*.\<Lambda> P:A\<rightarrow>*.\<Pi> a:A. P^a: ?T"
   9.167 +schematic_goal (in CC) "\<turnstile> \<Lambda> A:*.\<Lambda> P:A\<rightarrow>*.\<Pi> a:A. P^a: ?T"
   9.168    by (depth_solve rules)
   9.169  
   9.170 -schematic_lemma (in CC) "A:* P:A\<rightarrow>* a:A \<turnstile> ?p : (\<Pi> a:A. P^a)\<rightarrow>P^a"
   9.171 +schematic_goal (in CC) "A:* P:A\<rightarrow>* a:A \<turnstile> ?p : (\<Pi> a:A. P^a)\<rightarrow>P^a"
   9.172    apply (strip_asms rules)
   9.173    apply (rule lam_ss)
   9.174      apply (depth_solve1 rules)
   9.175 @@ -196,15 +196,15 @@
   9.176  
   9.177  subsection \<open>Some random examples\<close>
   9.178  
   9.179 -schematic_lemma (in LP2) "A:* c:A f:A\<rightarrow>A \<turnstile>
   9.180 +schematic_goal (in LP2) "A:* c:A f:A\<rightarrow>A \<turnstile>
   9.181      \<Lambda> a:A. \<Pi> P:A\<rightarrow>*.P^c \<rightarrow> (\<Pi> x:A. P^x\<rightarrow>P^(f^x)) \<rightarrow> P^a : ?T"
   9.182    by (depth_solve rules)
   9.183  
   9.184 -schematic_lemma (in CC) "\<Lambda> A:*.\<Lambda> c:A. \<Lambda> f:A\<rightarrow>A.
   9.185 +schematic_goal (in CC) "\<Lambda> A:*.\<Lambda> c:A. \<Lambda> f:A\<rightarrow>A.
   9.186      \<Lambda> a:A. \<Pi> P:A\<rightarrow>*.P^c \<rightarrow> (\<Pi> x:A. P^x\<rightarrow>P^(f^x)) \<rightarrow> P^a : ?T"
   9.187    by (depth_solve rules)
   9.188  
   9.189 -schematic_lemma (in LP2)
   9.190 +schematic_goal (in LP2)
   9.191    "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)"
   9.192    -- \<open>Symmetry of Leibnitz equality\<close>
   9.193    apply (strip_asms rules)
    10.1 --- a/src/Doc/Codegen/Evaluation.thy	Tue Oct 06 13:31:44 2015 +0200
    10.2 +++ b/src/Doc/Codegen/Evaluation.thy	Tue Oct 06 15:14:28 2015 +0200
    10.3 @@ -228,7 +228,7 @@
    10.4  \<close>
    10.5  
    10.6  ML (*<*) \<open>\<close>
    10.7 -schematic_lemma "thm": fixes x y z :: "'a::order" shows "x < y \<and> x < z \<equiv> ?P"
    10.8 +schematic_goal "thm": fixes x y z :: "'a::order" shows "x < y \<and> x < z \<equiv> ?P"
    10.9  ML_prf 
   10.10  (*>*) \<open>val thm =
   10.11    Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"}\<close> (*<*)
    11.1 --- a/src/Doc/Isar_Ref/Proof.thy	Tue Oct 06 13:31:44 2015 +0200
    11.2 +++ b/src/Doc/Isar_Ref/Proof.thy	Tue Oct 06 15:14:28 2015 +0200
    11.3 @@ -379,9 +379,7 @@
    11.4      @{command_def "lemma"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
    11.5      @{command_def "theorem"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
    11.6      @{command_def "corollary"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
    11.7 -    @{command_def "schematic_lemma"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
    11.8 -    @{command_def "schematic_theorem"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
    11.9 -    @{command_def "schematic_corollary"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
   11.10 +    @{command_def "schematic_goal"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
   11.11      @{command_def "have"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
   11.12      @{command_def "show"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
   11.13      @{command_def "hence"} & : & @{text "proof(state) \<rightarrow> proof(prove)"} \\
   11.14 @@ -423,8 +421,7 @@
   11.15  
   11.16    @{rail \<open>
   11.17      (@@{command lemma} | @@{command theorem} | @@{command corollary} |
   11.18 -     @@{command schematic_lemma} | @@{command schematic_theorem} |
   11.19 -     @@{command schematic_corollary}) (stmt | statement)
   11.20 +     @@{command schematic_goal}) (stmt | statement)
   11.21      ;
   11.22      (@@{command have} | @@{command show} | @@{command hence} | @@{command thus})
   11.23        stmt cond_stmt @{syntax for_fixes}
   11.24 @@ -463,10 +460,8 @@
   11.25    being of a different kind.  This discrimination acts like a formal
   11.26    comment.
   11.27  
   11.28 -  \item @{command "schematic_lemma"}, @{command "schematic_theorem"},
   11.29 -  @{command "schematic_corollary"} are similar to @{command "lemma"},
   11.30 -  @{command "theorem"}, @{command "corollary"}, respectively but allow
   11.31 -  the statement to contain unbound schematic variables.
   11.32 +  \item @{command "schematic_goal"} is similar to @{command "theorem"},
   11.33 +  but allows the statement to contain unbound schematic variables.
   11.34  
   11.35    Under normal circumstances, an Isar proof text needs to specify
   11.36    claims explicitly.  Schematic goals are more like goals in Prolog,
    12.1 --- a/src/Doc/Isar_Ref/Spec.thy	Tue Oct 06 13:31:44 2015 +0200
    12.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Tue Oct 06 15:14:28 2015 +0200
    12.3 @@ -446,9 +446,9 @@
    12.4  
    12.5    \item @{command "declare"}~@{text thms} declares theorems to the
    12.6    current local theory context.  No theorem binding is involved here,
    12.7 -  unlike @{command "theorems"} or @{command "lemmas"} (cf.\
    12.8 -  \secref{sec:theorems}), so @{command "declare"} only has the effect
    12.9 -  of applying attributes as included in the theorem specification.
   12.10 +  unlike @{command "lemmas"} (cf.\ \secref{sec:theorems}), so
   12.11 +  @{command "declare"} only has the effect of applying attributes as
   12.12 +  included in the theorem specification.
   12.13  
   12.14    \end{description}
   12.15  \<close>
   12.16 @@ -1441,12 +1441,11 @@
   12.17  text \<open>
   12.18    \begin{matharray}{rcll}
   12.19      @{command_def "lemmas"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   12.20 -    @{command_def "theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   12.21      @{command_def "named_theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   12.22    \end{matharray}
   12.23  
   12.24    @{rail \<open>
   12.25 -    (@@{command lemmas} | @@{command theorems}) (@{syntax thmdef}? @{syntax thmrefs} + @'and')
   12.26 +    @@{command lemmas} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
   12.27        @{syntax for_fixes}
   12.28      ;
   12.29      @@{command named_theorems} (@{syntax name} @{syntax text}? + @'and')
   12.30 @@ -1460,9 +1459,6 @@
   12.31    Results are standardized before being stored, i.e.\ schematic
   12.32    variables are renamed to enforce index @{text "0"} uniformly.
   12.33  
   12.34 -  \item @{command "theorems"} is the same as @{command "lemmas"}, but
   12.35 -  marks the result as a different kind of facts.
   12.36 -
   12.37    \item @{command "named_theorems"}~@{text "name description"} declares a
   12.38    dynamic fact within the context. The same @{text name} is used to define
   12.39    an attribute with the usual @{text add}/@{text del} syntax (e.g.\ see
    13.1 --- a/src/FOL/ex/Classical.thy	Tue Oct 06 13:31:44 2015 +0200
    13.2 +++ b/src/FOL/ex/Classical.thy	Tue Oct 06 15:14:28 2015 +0200
    13.3 @@ -363,7 +363,7 @@
    13.4  
    13.5  text\<open>Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
    13.6    fast DISCOVERS who killed Agatha.\<close>
    13.7 -schematic_lemma "lives(agatha) & lives(butler) & lives(charles) &  
    13.8 +schematic_goal "lives(agatha) & lives(butler) & lives(charles) &  
    13.9     (killed(agatha,agatha) | killed(butler,agatha) | killed(charles,agatha)) &  
   13.10     (\<forall>x y. killed(x,y) --> hates(x,y) & ~richer(x,y)) &  
   13.11     (\<forall>x. hates(agatha,x) --> ~hates(charles,x)) &  
    14.1 --- a/src/FOL/ex/Prolog.thy	Tue Oct 06 13:31:44 2015 +0200
    14.2 +++ b/src/FOL/ex/Prolog.thy	Tue Oct 06 15:14:28 2015 +0200
    14.3 @@ -23,18 +23,18 @@
    14.4    revNil:  "rev(Nil,Nil)" and
    14.5    revCons: "[| rev(xs,ys);  app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)"
    14.6  
    14.7 -schematic_lemma "app(a:b:c:Nil, d:e:Nil, ?x)"
    14.8 +schematic_goal "app(a:b:c:Nil, d:e:Nil, ?x)"
    14.9  apply (rule appNil appCons)
   14.10  apply (rule appNil appCons)
   14.11  apply (rule appNil appCons)
   14.12  apply (rule appNil appCons)
   14.13  done
   14.14  
   14.15 -schematic_lemma "app(?x, c:d:Nil, a:b:c:d:Nil)"
   14.16 +schematic_goal "app(?x, c:d:Nil, a:b:c:d:Nil)"
   14.17  apply (rule appNil appCons)+
   14.18  done
   14.19  
   14.20 -schematic_lemma "app(?x, ?y, a:b:c:d:Nil)"
   14.21 +schematic_goal "app(?x, ?y, a:b:c:d:Nil)"
   14.22  apply (rule appNil appCons)+
   14.23  back
   14.24  back
   14.25 @@ -47,15 +47,15 @@
   14.26  
   14.27  lemmas rules = appNil appCons revNil revCons
   14.28  
   14.29 -schematic_lemma "rev(a:b:c:d:Nil, ?x)"
   14.30 +schematic_goal "rev(a:b:c:d:Nil, ?x)"
   14.31  apply (rule rules)+
   14.32  done
   14.33  
   14.34 -schematic_lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)"
   14.35 +schematic_goal "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)"
   14.36  apply (rule rules)+
   14.37  done
   14.38  
   14.39 -schematic_lemma "rev(?x, a:b:c:Nil)"
   14.40 +schematic_goal "rev(?x, a:b:c:Nil)"
   14.41  apply (rule rules)+  -- \<open>does not solve it directly!\<close>
   14.42  back
   14.43  back
   14.44 @@ -67,23 +67,23 @@
   14.45    DEPTH_FIRST (has_fewer_prems 1) (resolve_tac ctxt @{thms rules} 1)
   14.46  \<close>
   14.47  
   14.48 -schematic_lemma "rev(?x, a:b:c:Nil)"
   14.49 +schematic_goal "rev(?x, a:b:c:Nil)"
   14.50  apply (tactic \<open>prolog_tac @{context}\<close>)
   14.51  done
   14.52  
   14.53 -schematic_lemma "rev(a:?x:c:?y:Nil, d:?z:b:?u)"
   14.54 +schematic_goal "rev(a:?x:c:?y:Nil, d:?z:b:?u)"
   14.55  apply (tactic \<open>prolog_tac @{context}\<close>)
   14.56  done
   14.57  
   14.58  (*rev([a..p], ?w) requires 153 inferences *)
   14.59 -schematic_lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)"
   14.60 +schematic_goal "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)"
   14.61  apply (tactic \<open>
   14.62    DEPTH_SOLVE (resolve_tac @{context} ([@{thm refl}, @{thm conjI}] @ @{thms rules}) 1)\<close>)
   14.63  done
   14.64  
   14.65  (*?x has 16, ?y has 32;  rev(?y,?w) requires 561 (rather large) inferences
   14.66    total inferences = 2 + 1 + 17 + 561 = 581*)
   14.67 -schematic_lemma "a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil = ?x & app(?x,?x,?y) & rev(?y,?w)"
   14.68 +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)"
   14.69  apply (tactic \<open>
   14.70    DEPTH_SOLVE (resolve_tac @{context} ([@{thm refl}, @{thm conjI}] @ @{thms rules}) 1)\<close>)
   14.71  done
    15.1 --- a/src/FOL/ex/Quantifiers_Cla.thy	Tue Oct 06 13:31:44 2015 +0200
    15.2 +++ b/src/FOL/ex/Quantifiers_Cla.thy	Tue Oct 06 15:14:28 2015 +0200
    15.3 @@ -58,11 +58,11 @@
    15.4    apply fast?
    15.5    oops
    15.6  
    15.7 -schematic_lemma "P(?a) --> (ALL x. P(x))"
    15.8 +schematic_goal "P(?a) --> (ALL x. P(x))"
    15.9    apply fast?
   15.10    oops
   15.11  
   15.12 -schematic_lemma "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
   15.13 +schematic_goal "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
   15.14    apply fast?
   15.15    oops
   15.16  
   15.17 @@ -76,7 +76,7 @@
   15.18  lemma "(P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
   15.19    by fast
   15.20  
   15.21 -schematic_lemma "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
   15.22 +schematic_goal "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
   15.23    by fast
   15.24  
   15.25  lemma "(ALL x. Q(x))  -->  (EX x. Q(x))"
    16.1 --- a/src/FOL/ex/Quantifiers_Int.thy	Tue Oct 06 13:31:44 2015 +0200
    16.2 +++ b/src/FOL/ex/Quantifiers_Int.thy	Tue Oct 06 15:14:28 2015 +0200
    16.3 @@ -58,11 +58,11 @@
    16.4    apply (tactic "IntPr.fast_tac @{context} 1")?
    16.5    oops
    16.6  
    16.7 -schematic_lemma "P(?a) --> (ALL x. P(x))"
    16.8 +schematic_goal "P(?a) --> (ALL x. P(x))"
    16.9    apply (tactic "IntPr.fast_tac @{context} 1")?
   16.10    oops
   16.11  
   16.12 -schematic_lemma "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
   16.13 +schematic_goal "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
   16.14    apply (tactic "IntPr.fast_tac @{context} 1")?
   16.15    oops
   16.16  
   16.17 @@ -76,7 +76,7 @@
   16.18  lemma "(P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
   16.19    by (tactic "IntPr.fast_tac @{context} 1")
   16.20  
   16.21 -schematic_lemma "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
   16.22 +schematic_goal "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
   16.23    by (tactic "IntPr.fast_tac @{context} 1")
   16.24  
   16.25  lemma "(ALL x. Q(x))  -->  (EX x. Q(x))"
    17.1 --- a/src/FOLP/FOLP.thy	Tue Oct 06 13:31:44 2015 +0200
    17.2 +++ b/src/FOLP/FOLP.thy	Tue Oct 06 15:14:28 2015 +0200
    17.3 @@ -15,7 +15,7 @@
    17.4  
    17.5  (*** Classical introduction rules for | and EX ***)
    17.6  
    17.7 -schematic_lemma disjCI:
    17.8 +schematic_goal disjCI:
    17.9    assumes "!!x. x:~Q ==> f(x):P"
   17.10    shows "?p : P|Q"
   17.11    apply (rule classical)
   17.12 @@ -24,7 +24,7 @@
   17.13    done
   17.14  
   17.15  (*introduction rule involving only EX*)
   17.16 -schematic_lemma ex_classical:
   17.17 +schematic_goal ex_classical:
   17.18    assumes "!!u. u:~(EX x. P(x)) ==> f(u):P(a)"
   17.19    shows "?p : EX x. P(x)"
   17.20    apply (rule classical)
   17.21 @@ -32,7 +32,7 @@
   17.22    done
   17.23  
   17.24  (*version of above, simplifying ~EX to ALL~ *)
   17.25 -schematic_lemma exCI:
   17.26 +schematic_goal exCI:
   17.27    assumes "!!u. u:ALL x. ~P(x) ==> f(u):P(a)"
   17.28    shows "?p : EX x. P(x)"
   17.29    apply (rule ex_classical)
   17.30 @@ -41,7 +41,7 @@
   17.31    apply (erule exI)
   17.32    done
   17.33  
   17.34 -schematic_lemma excluded_middle: "?p : ~P | P"
   17.35 +schematic_goal excluded_middle: "?p : ~P | P"
   17.36    apply (rule disjCI)
   17.37    apply assumption
   17.38    done
   17.39 @@ -50,7 +50,7 @@
   17.40  (*** Special elimination rules *)
   17.41  
   17.42  (*Classical implies (-->) elimination. *)
   17.43 -schematic_lemma impCE:
   17.44 +schematic_goal impCE:
   17.45    assumes major: "p:P-->Q"
   17.46      and r1: "!!x. x:~P ==> f(x):R"
   17.47      and r2: "!!y. y:Q ==> g(y):R"
   17.48 @@ -61,7 +61,7 @@
   17.49    done
   17.50  
   17.51  (*Double negation law*)
   17.52 -schematic_lemma notnotD: "p:~~P ==> ?p : P"
   17.53 +schematic_goal notnotD: "p:~~P ==> ?p : P"
   17.54    apply (rule classical)
   17.55    apply (erule notE)
   17.56    apply assumption
   17.57 @@ -72,7 +72,7 @@
   17.58  
   17.59  (*Classical <-> elimination.  Proof substitutes P=Q in
   17.60      ~P ==> ~Q    and    P ==> Q  *)
   17.61 -schematic_lemma iffCE:
   17.62 +schematic_goal iffCE:
   17.63    assumes major: "p:P<->Q"
   17.64      and r1: "!!x y.[| x:P; y:Q |] ==> f(x,y):R"
   17.65      and r2: "!!x y.[| x:~P; y:~Q |] ==> g(x,y):R"
   17.66 @@ -88,7 +88,7 @@
   17.67  
   17.68  
   17.69  (*Should be used as swap since ~P becomes redundant*)
   17.70 -schematic_lemma swap:
   17.71 +schematic_goal swap:
   17.72    assumes major: "p:~P"
   17.73      and r: "!!x. x:~Q ==> f(x):P"
   17.74    shows "?p : Q"
   17.75 @@ -130,7 +130,7 @@
   17.76      addSEs [@{thm exE}, @{thm ex1E}] addEs [@{thm all_dupE}];
   17.77  \<close>
   17.78  
   17.79 -schematic_lemma cla_rews:
   17.80 +schematic_goal cla_rews:
   17.81    "?p1 : P | ~P"
   17.82    "?p2 : ~P | P"
   17.83    "?p3 : ~ ~ P <-> P"
    18.1 --- a/src/FOLP/IFOLP.thy	Tue Oct 06 13:31:44 2015 +0200
    18.2 +++ b/src/FOLP/IFOLP.thy	Tue Oct 06 15:14:28 2015 +0200
    18.3 @@ -171,7 +171,7 @@
    18.4  
    18.5  (*** Sequent-style elimination rules for & --> and ALL ***)
    18.6  
    18.7 -schematic_lemma conjE:
    18.8 +schematic_goal conjE:
    18.9    assumes "p:P&Q"
   18.10      and "!!x y.[| x:P; y:Q |] ==> f(x,y):R"
   18.11    shows "?a:R"
   18.12 @@ -180,7 +180,7 @@
   18.13    apply (rule conjunct2 [OF assms(1)])
   18.14    done
   18.15  
   18.16 -schematic_lemma impE:
   18.17 +schematic_goal impE:
   18.18    assumes "p:P-->Q"
   18.19      and "q:P"
   18.20      and "!!x. x:Q ==> r(x):R"
   18.21 @@ -188,7 +188,7 @@
   18.22    apply (rule assms mp)+
   18.23    done
   18.24  
   18.25 -schematic_lemma allE:
   18.26 +schematic_goal allE:
   18.27    assumes "p:ALL x. P(x)"
   18.28      and "!!y. y:P(x) ==> q(y):R"
   18.29    shows "?p:R"
   18.30 @@ -196,7 +196,7 @@
   18.31    done
   18.32  
   18.33  (*Duplicates the quantifier; for use with eresolve_tac*)
   18.34 -schematic_lemma all_dupE:
   18.35 +schematic_goal all_dupE:
   18.36    assumes "p:ALL x. P(x)"
   18.37      and "!!y z.[| y:P(x); z:ALL x. P(x) |] ==> q(y,z):R"
   18.38    shows "?p:R"
   18.39 @@ -206,21 +206,21 @@
   18.40  
   18.41  (*** Negation rules, which translate between ~P and P-->False ***)
   18.42  
   18.43 -schematic_lemma notI:
   18.44 +schematic_goal notI:
   18.45    assumes "!!x. x:P ==> q(x):False"
   18.46    shows "?p:~P"
   18.47    unfolding not_def
   18.48    apply (assumption | rule assms impI)+
   18.49    done
   18.50  
   18.51 -schematic_lemma notE: "p:~P \<Longrightarrow> q:P \<Longrightarrow> ?p:R"
   18.52 +schematic_goal notE: "p:~P \<Longrightarrow> q:P \<Longrightarrow> ?p:R"
   18.53    unfolding not_def
   18.54    apply (drule (1) mp)
   18.55    apply (erule FalseE)
   18.56    done
   18.57  
   18.58  (*This is useful with the special implication rules for each kind of P. *)
   18.59 -schematic_lemma not_to_imp:
   18.60 +schematic_goal not_to_imp:
   18.61    assumes "p:~P"
   18.62      and "!!x. x:(P-->False) ==> q(x):Q"
   18.63    shows "?p:Q"
   18.64 @@ -229,13 +229,13 @@
   18.65  
   18.66  (* For substitution int an assumption P, reduce Q to P-->Q, substitute into
   18.67     this implication, then apply impI to move P back into the assumptions.*)
   18.68 -schematic_lemma rev_mp: "[| p:P;  q:P --> Q |] ==> ?p:Q"
   18.69 +schematic_goal rev_mp: "[| p:P;  q:P --> Q |] ==> ?p:Q"
   18.70    apply (assumption | rule mp)+
   18.71    done
   18.72  
   18.73  
   18.74  (*Contrapositive of an inference rule*)
   18.75 -schematic_lemma contrapos:
   18.76 +schematic_goal contrapos:
   18.77    assumes major: "p:~Q"
   18.78      and minor: "!!y. y:P==>q(y):Q"
   18.79    shows "?a:~P"
   18.80 @@ -286,7 +286,7 @@
   18.81  
   18.82  (*** If-and-only-if ***)
   18.83  
   18.84 -schematic_lemma iffI:
   18.85 +schematic_goal iffI:
   18.86    assumes "!!x. x:P ==> q(x):Q"
   18.87      and "!!x. x:Q ==> r(x):P"
   18.88    shows "?p:P<->Q"
   18.89 @@ -295,7 +295,7 @@
   18.90    done
   18.91  
   18.92  
   18.93 -schematic_lemma iffE:
   18.94 +schematic_goal iffE:
   18.95    assumes "p:P <-> Q"
   18.96      and "!!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R"
   18.97    shows "?p:R"
   18.98 @@ -307,28 +307,28 @@
   18.99  
  18.100  (* Destruct rules for <-> similar to Modus Ponens *)
  18.101  
  18.102 -schematic_lemma iffD1: "[| p:P <-> Q; q:P |] ==> ?p:Q"
  18.103 +schematic_goal iffD1: "[| p:P <-> Q; q:P |] ==> ?p:Q"
  18.104    unfolding iff_def
  18.105    apply (rule conjunct1 [THEN mp], assumption+)
  18.106    done
  18.107  
  18.108 -schematic_lemma iffD2: "[| p:P <-> Q; q:Q |] ==> ?p:P"
  18.109 +schematic_goal iffD2: "[| p:P <-> Q; q:Q |] ==> ?p:P"
  18.110    unfolding iff_def
  18.111    apply (rule conjunct2 [THEN mp], assumption+)
  18.112    done
  18.113  
  18.114 -schematic_lemma iff_refl: "?p:P <-> P"
  18.115 +schematic_goal iff_refl: "?p:P <-> P"
  18.116    apply (rule iffI)
  18.117     apply assumption+
  18.118    done
  18.119  
  18.120 -schematic_lemma iff_sym: "p:Q <-> P ==> ?p:P <-> Q"
  18.121 +schematic_goal iff_sym: "p:Q <-> P ==> ?p:P <-> Q"
  18.122    apply (erule iffE)
  18.123    apply (rule iffI)
  18.124     apply (erule (1) mp)+
  18.125    done
  18.126  
  18.127 -schematic_lemma iff_trans: "[| p:P <-> Q; q:Q<-> R |] ==> ?p:P <-> R"
  18.128 +schematic_goal iff_trans: "[| p:P <-> Q; q:Q<-> R |] ==> ?p:P <-> R"
  18.129    apply (rule iffI)
  18.130     apply (assumption | erule iffE | erule (1) impE)+
  18.131    done
  18.132 @@ -339,7 +339,7 @@
  18.133   do NOT mean the same thing.  The parser treats EX!x y.P(x,y) as sequential.
  18.134  ***)
  18.135  
  18.136 -schematic_lemma ex1I:
  18.137 +schematic_goal ex1I:
  18.138    assumes "p:P(a)"
  18.139      and "!!x u. u:P(x) ==> f(u) : x=a"
  18.140    shows "?p:EX! x. P(x)"
  18.141 @@ -347,7 +347,7 @@
  18.142    apply (assumption | rule assms exI conjI allI impI)+
  18.143    done
  18.144  
  18.145 -schematic_lemma ex1E:
  18.146 +schematic_goal ex1E:
  18.147    assumes "p:EX! x. P(x)"
  18.148      and "!!x u v. [| u:P(x);  v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R"
  18.149    shows "?a : R"
  18.150 @@ -369,7 +369,7 @@
  18.151  method_setup iff =
  18.152    \<open>Attrib.thms >> (fn prems => fn ctxt => SIMPLE_METHOD' (iff_tac ctxt prems))\<close>
  18.153  
  18.154 -schematic_lemma conj_cong:
  18.155 +schematic_goal conj_cong:
  18.156    assumes "p:P <-> P'"
  18.157      and "!!x. x:P' ==> q(x):Q <-> Q'"
  18.158    shows "?p:(P&Q) <-> (P'&Q')"
  18.159 @@ -377,12 +377,12 @@
  18.160    apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+
  18.161    done
  18.162  
  18.163 -schematic_lemma disj_cong:
  18.164 +schematic_goal disj_cong:
  18.165    "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P|Q) <-> (P'|Q')"
  18.166    apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | mp)+
  18.167    done
  18.168  
  18.169 -schematic_lemma imp_cong:
  18.170 +schematic_goal imp_cong:
  18.171    assumes "p:P <-> P'"
  18.172      and "!!x. x:P' ==> q(x):Q <-> Q'"
  18.173    shows "?p:(P-->Q) <-> (P'-->Q')"
  18.174 @@ -390,23 +390,23 @@
  18.175    apply (assumption | rule iffI impI | erule iffE | mp | iff assms)+
  18.176    done
  18.177  
  18.178 -schematic_lemma iff_cong:
  18.179 +schematic_goal iff_cong:
  18.180    "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')"
  18.181    apply (erule iffE | assumption | rule iffI | mp)+
  18.182    done
  18.183  
  18.184 -schematic_lemma not_cong:
  18.185 +schematic_goal not_cong:
  18.186    "p:P <-> P' ==> ?p:~P <-> ~P'"
  18.187    apply (assumption | rule iffI notI | mp | erule iffE notE)+
  18.188    done
  18.189  
  18.190 -schematic_lemma all_cong:
  18.191 +schematic_goal all_cong:
  18.192    assumes "!!x. f(x):P(x) <-> Q(x)"
  18.193    shows "?p:(ALL x. P(x)) <-> (ALL x. Q(x))"
  18.194    apply (assumption | rule iffI allI | mp | erule allE | iff assms)+
  18.195    done
  18.196  
  18.197 -schematic_lemma ex_cong:
  18.198 +schematic_goal ex_cong:
  18.199    assumes "!!x. f(x):P(x) <-> Q(x)"
  18.200    shows "?p:(EX x. P(x)) <-> (EX x. Q(x))"
  18.201    apply (erule exE | assumption | rule iffI exI | mp | iff assms)+
  18.202 @@ -425,7 +425,7 @@
  18.203  
  18.204  lemmas refl = ieqI
  18.205  
  18.206 -schematic_lemma subst:
  18.207 +schematic_goal subst:
  18.208    assumes prem1: "p:a=b"
  18.209      and prem2: "q:P(a)"
  18.210    shows "?p : P(b)"
  18.211 @@ -435,29 +435,29 @@
  18.212    apply assumption
  18.213    done
  18.214  
  18.215 -schematic_lemma sym: "q:a=b ==> ?c:b=a"
  18.216 +schematic_goal sym: "q:a=b ==> ?c:b=a"
  18.217    apply (erule subst)
  18.218    apply (rule refl)
  18.219    done
  18.220  
  18.221 -schematic_lemma trans: "[| p:a=b;  q:b=c |] ==> ?d:a=c"
  18.222 +schematic_goal trans: "[| p:a=b;  q:b=c |] ==> ?d:a=c"
  18.223    apply (erule (1) subst)
  18.224    done
  18.225  
  18.226  (** ~ b=a ==> ~ a=b **)
  18.227 -schematic_lemma not_sym: "p:~ b=a ==> ?q:~ a=b"
  18.228 +schematic_goal not_sym: "p:~ b=a ==> ?q:~ a=b"
  18.229    apply (erule contrapos)
  18.230    apply (erule sym)
  18.231    done
  18.232  
  18.233 -schematic_lemma ssubst: "p:b=a \<Longrightarrow> q:P(a) \<Longrightarrow> ?p:P(b)"
  18.234 +schematic_goal ssubst: "p:b=a \<Longrightarrow> q:P(a) \<Longrightarrow> ?p:P(b)"
  18.235    apply (drule sym)
  18.236    apply (erule subst)
  18.237    apply assumption
  18.238    done
  18.239  
  18.240  (*A special case of ex1E that would otherwise need quantifier expansion*)
  18.241 -schematic_lemma ex1_equalsE: "[| p:EX! x. P(x);  q:P(a);  r:P(b) |] ==> ?d:a=b"
  18.242 +schematic_goal ex1_equalsE: "[| p:EX! x. P(x);  q:P(a);  r:P(b) |] ==> ?d:a=b"
  18.243    apply (erule ex1E)
  18.244    apply (rule trans)
  18.245     apply (rule_tac [2] sym)
  18.246 @@ -466,17 +466,17 @@
  18.247  
  18.248  (** Polymorphic congruence rules **)
  18.249  
  18.250 -schematic_lemma subst_context: "[| p:a=b |]  ==>  ?d:t(a)=t(b)"
  18.251 +schematic_goal subst_context: "[| p:a=b |]  ==>  ?d:t(a)=t(b)"
  18.252    apply (erule ssubst)
  18.253    apply (rule refl)
  18.254    done
  18.255  
  18.256 -schematic_lemma subst_context2: "[| p:a=b;  q:c=d |]  ==>  ?p:t(a,c)=t(b,d)"
  18.257 +schematic_goal subst_context2: "[| p:a=b;  q:c=d |]  ==>  ?p:t(a,c)=t(b,d)"
  18.258    apply (erule ssubst)+
  18.259    apply (rule refl)
  18.260    done
  18.261  
  18.262 -schematic_lemma subst_context3: "[| p:a=b;  q:c=d;  r:e=f |]  ==>  ?p:t(a,c,e)=t(b,d,f)"
  18.263 +schematic_goal subst_context3: "[| p:a=b;  q:c=d;  r:e=f |]  ==>  ?p:t(a,c,e)=t(b,d,f)"
  18.264    apply (erule ssubst)+
  18.265    apply (rule refl)
  18.266    done
  18.267 @@ -485,7 +485,7 @@
  18.268          a = b
  18.269          |   |
  18.270          c = d   *)
  18.271 -schematic_lemma box_equals: "[| p:a=b;  q:a=c;  r:b=d |] ==> ?p:c=d"
  18.272 +schematic_goal box_equals: "[| p:a=b;  q:a=c;  r:b=d |] ==> ?p:c=d"
  18.273    apply (rule trans)
  18.274     apply (rule trans)
  18.275      apply (rule sym)
  18.276 @@ -493,7 +493,7 @@
  18.277    done
  18.278  
  18.279  (*Dual of box_equals: for proving equalities backwards*)
  18.280 -schematic_lemma simp_equals: "[| p:a=c;  q:b=d;  r:c=d |] ==> ?p:a=b"
  18.281 +schematic_goal simp_equals: "[| p:a=c;  q:b=d;  r:c=d |] ==> ?p:a=b"
  18.282    apply (rule trans)
  18.283     apply (rule trans)
  18.284      apply (assumption | rule sym)+
  18.285 @@ -501,19 +501,19 @@
  18.286  
  18.287  (** Congruence rules for predicate letters **)
  18.288  
  18.289 -schematic_lemma pred1_cong: "p:a=a' ==> ?p:P(a) <-> P(a')"
  18.290 +schematic_goal pred1_cong: "p:a=a' ==> ?p:P(a) <-> P(a')"
  18.291    apply (rule iffI)
  18.292     apply (tactic \<open>
  18.293       DEPTH_SOLVE (assume_tac @{context} 1 ORELSE eresolve_tac @{context} [@{thm subst}, @{thm ssubst}] 1)\<close>)
  18.294    done
  18.295  
  18.296 -schematic_lemma pred2_cong: "[| p:a=a';  q:b=b' |] ==> ?p:P(a,b) <-> P(a',b')"
  18.297 +schematic_goal pred2_cong: "[| p:a=a';  q:b=b' |] ==> ?p:P(a,b) <-> P(a',b')"
  18.298    apply (rule iffI)
  18.299     apply (tactic \<open>
  18.300       DEPTH_SOLVE (assume_tac @{context} 1 ORELSE eresolve_tac @{context} [@{thm subst}, @{thm ssubst}] 1)\<close>)
  18.301    done
  18.302  
  18.303 -schematic_lemma pred3_cong: "[| p:a=a';  q:b=b';  r:c=c' |] ==> ?p:P(a,b,c) <-> P(a',b',c')"
  18.304 +schematic_goal pred3_cong: "[| p:a=a';  q:b=b';  r:c=c' |] ==> ?p:P(a,b,c) <-> P(a',b',c')"
  18.305    apply (rule iffI)
  18.306     apply (tactic \<open>
  18.307       DEPTH_SOLVE (assume_tac @{context} 1 ORELSE eresolve_tac @{context} [@{thm subst}, @{thm ssubst}] 1)\<close>)
  18.308 @@ -532,14 +532,14 @@
  18.309     R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
  18.310      (preprint, University of St Andrews, 1991)  ***)
  18.311  
  18.312 -schematic_lemma conj_impE:
  18.313 +schematic_goal conj_impE:
  18.314    assumes major: "p:(P&Q)-->S"
  18.315      and minor: "!!x. x:P-->(Q-->S) ==> q(x):R"
  18.316    shows "?p:R"
  18.317    apply (assumption | rule conjI impI major [THEN mp] minor)+
  18.318    done
  18.319  
  18.320 -schematic_lemma disj_impE:
  18.321 +schematic_goal disj_impE:
  18.322    assumes major: "p:(P|Q)-->S"
  18.323      and minor: "!!x y.[| x:P-->S; y:Q-->S |] ==> q(x,y):R"
  18.324    shows "?p:R"
  18.325 @@ -550,7 +550,7 @@
  18.326  
  18.327  (*Simplifies the implication.  Classical version is stronger.
  18.328    Still UNSAFE since Q must be provable -- backtracking needed.  *)
  18.329 -schematic_lemma imp_impE:
  18.330 +schematic_goal imp_impE:
  18.331    assumes major: "p:(P-->Q)-->S"
  18.332      and r1: "!!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q"
  18.333      and r2: "!!x. x:S ==> r(x):R"
  18.334 @@ -560,7 +560,7 @@
  18.335  
  18.336  (*Simplifies the implication.  Classical version is stronger.
  18.337    Still UNSAFE since ~P must be provable -- backtracking needed.  *)
  18.338 -schematic_lemma not_impE:
  18.339 +schematic_goal not_impE:
  18.340    assumes major: "p:~P --> S"
  18.341      and r1: "!!y. y:P ==> q(y):False"
  18.342      and r2: "!!y. y:S ==> r(y):R"
  18.343 @@ -569,7 +569,7 @@
  18.344    done
  18.345  
  18.346  (*Simplifies the implication.   UNSAFE.  *)
  18.347 -schematic_lemma iff_impE:
  18.348 +schematic_goal iff_impE:
  18.349    assumes major: "p:(P<->Q)-->S"
  18.350      and r1: "!!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q"
  18.351      and r2: "!!x y.[| x:Q; y:P-->S |] ==> r(x,y):P"
  18.352 @@ -579,7 +579,7 @@
  18.353    done
  18.354  
  18.355  (*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
  18.356 -schematic_lemma all_impE:
  18.357 +schematic_goal all_impE:
  18.358    assumes major: "p:(ALL x. P(x))-->S"
  18.359      and r1: "!!x. q:P(x)"
  18.360      and r2: "!!y. y:S ==> r(y):R"
  18.361 @@ -588,7 +588,7 @@
  18.362    done
  18.363  
  18.364  (*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
  18.365 -schematic_lemma ex_impE:
  18.366 +schematic_goal ex_impE:
  18.367    assumes major: "p:(EX x. P(x))-->S"
  18.368      and r: "!!y. y:P(a)-->S ==> q(y):R"
  18.369    shows "?p:R"
  18.370 @@ -596,7 +596,7 @@
  18.371    done
  18.372  
  18.373  
  18.374 -schematic_lemma rev_cut_eq:
  18.375 +schematic_goal rev_cut_eq:
  18.376    assumes "p:a=b"
  18.377      and "!!x. x:a=b ==> f(x):R"
  18.378    shows "?p:R"
  18.379 @@ -632,7 +632,7 @@
  18.380  
  18.381  (*** Rewrite rules ***)
  18.382  
  18.383 -schematic_lemma conj_rews:
  18.384 +schematic_goal conj_rews:
  18.385    "?p1 : P & True <-> P"
  18.386    "?p2 : True & P <-> P"
  18.387    "?p3 : P & False <-> False"
  18.388 @@ -644,7 +644,7 @@
  18.389    apply (tactic \<open>fn st => IntPr.fast_tac @{context} 1 st\<close>)+
  18.390    done
  18.391  
  18.392 -schematic_lemma disj_rews:
  18.393 +schematic_goal disj_rews:
  18.394    "?p1 : P | True <-> True"
  18.395    "?p2 : True | P <-> True"
  18.396    "?p3 : P | False <-> P"
  18.397 @@ -654,13 +654,13 @@
  18.398    apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)+
  18.399    done
  18.400  
  18.401 -schematic_lemma not_rews:
  18.402 +schematic_goal not_rews:
  18.403    "?p1 : ~ False <-> True"
  18.404    "?p2 : ~ True <-> False"
  18.405    apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)+
  18.406    done
  18.407  
  18.408 -schematic_lemma imp_rews:
  18.409 +schematic_goal imp_rews:
  18.410    "?p1 : (P --> False) <-> ~P"
  18.411    "?p2 : (P --> True) <-> True"
  18.412    "?p3 : (False --> P) <-> True"
  18.413 @@ -670,7 +670,7 @@
  18.414    apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)+
  18.415    done
  18.416  
  18.417 -schematic_lemma iff_rews:
  18.418 +schematic_goal iff_rews:
  18.419    "?p1 : (True <-> P) <-> P"
  18.420    "?p2 : (P <-> True) <-> P"
  18.421    "?p3 : (P <-> P) <-> True"
  18.422 @@ -679,14 +679,14 @@
  18.423    apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)+
  18.424    done
  18.425  
  18.426 -schematic_lemma quant_rews:
  18.427 +schematic_goal quant_rews:
  18.428    "?p1 : (ALL x. P) <-> P"
  18.429    "?p2 : (EX x. P) <-> P"
  18.430    apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)+
  18.431    done
  18.432  
  18.433  (*These are NOT supplied by default!*)
  18.434 -schematic_lemma distrib_rews1:
  18.435 +schematic_goal distrib_rews1:
  18.436    "?p1 : ~(P|Q) <-> ~P & ~Q"
  18.437    "?p2 : P & (Q | R) <-> P&Q | P&R"
  18.438    "?p3 : (Q | R) & P <-> Q&P | R&P"
  18.439 @@ -694,7 +694,7 @@
  18.440    apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)+
  18.441    done
  18.442  
  18.443 -schematic_lemma distrib_rews2:
  18.444 +schematic_goal distrib_rews2:
  18.445    "?p1 : ~(EX x. NORM(P(x))) <-> (ALL x. ~NORM(P(x)))"
  18.446    "?p2 : ((EX x. NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)"
  18.447    "?p3 : (EX x. NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))"
  18.448 @@ -704,11 +704,11 @@
  18.449  
  18.450  lemmas distrib_rews = distrib_rews1 distrib_rews2
  18.451  
  18.452 -schematic_lemma P_Imp_P_iff_T: "p:P ==> ?p:(P <-> True)"
  18.453 +schematic_goal P_Imp_P_iff_T: "p:P ==> ?p:(P <-> True)"
  18.454    apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
  18.455    done
  18.456  
  18.457 -schematic_lemma not_P_imp_P_iff_F: "p:~P ==> ?p:(P <-> False)"
  18.458 +schematic_goal not_P_imp_P_iff_F: "p:~P ==> ?p:(P <-> False)"
  18.459    apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
  18.460    done
  18.461  
    19.1 --- a/src/FOLP/ex/Classical.thy	Tue Oct 06 13:31:44 2015 +0200
    19.2 +++ b/src/FOLP/ex/Classical.thy	Tue Oct 06 15:14:28 2015 +0200
    19.3 @@ -9,14 +9,14 @@
    19.4  imports FOLP
    19.5  begin
    19.6  
    19.7 -schematic_lemma "?p : (P --> Q | R) --> (P-->Q) | (P-->R)"
    19.8 +schematic_goal "?p : (P --> Q | R) --> (P-->Q) | (P-->R)"
    19.9    by (tactic "fast_tac @{context} FOLP_cs 1")
   19.10  
   19.11  (*If and only if*)
   19.12 -schematic_lemma "?p : (P<->Q) <-> (Q<->P)"
   19.13 +schematic_goal "?p : (P<->Q) <-> (Q<->P)"
   19.14    by (tactic "fast_tac @{context} FOLP_cs 1")
   19.15  
   19.16 -schematic_lemma "?p : ~ (P <-> ~P)"
   19.17 +schematic_goal "?p : ~ (P <-> ~P)"
   19.18    by (tactic "fast_tac @{context} FOLP_cs 1")
   19.19  
   19.20  
   19.21 @@ -32,138 +32,138 @@
   19.22  
   19.23  text "Pelletier's examples"
   19.24  (*1*)
   19.25 -schematic_lemma "?p : (P-->Q)  <->  (~Q --> ~P)"
   19.26 +schematic_goal "?p : (P-->Q)  <->  (~Q --> ~P)"
   19.27    by (tactic "fast_tac @{context} FOLP_cs 1")
   19.28  
   19.29  (*2*)
   19.30 -schematic_lemma "?p : ~ ~ P  <->  P"
   19.31 +schematic_goal "?p : ~ ~ P  <->  P"
   19.32    by (tactic "fast_tac @{context} FOLP_cs 1")
   19.33  
   19.34  (*3*)
   19.35 -schematic_lemma "?p : ~(P-->Q) --> (Q-->P)"
   19.36 +schematic_goal "?p : ~(P-->Q) --> (Q-->P)"
   19.37    by (tactic "fast_tac @{context} FOLP_cs 1")
   19.38  
   19.39  (*4*)
   19.40 -schematic_lemma "?p : (~P-->Q)  <->  (~Q --> P)"
   19.41 +schematic_goal "?p : (~P-->Q)  <->  (~Q --> P)"
   19.42    by (tactic "fast_tac @{context} FOLP_cs 1")
   19.43  
   19.44  (*5*)
   19.45 -schematic_lemma "?p : ((P|Q)-->(P|R)) --> (P|(Q-->R))"
   19.46 +schematic_goal "?p : ((P|Q)-->(P|R)) --> (P|(Q-->R))"
   19.47    by (tactic "fast_tac @{context} FOLP_cs 1")
   19.48  
   19.49  (*6*)
   19.50 -schematic_lemma "?p : P | ~ P"
   19.51 +schematic_goal "?p : P | ~ P"
   19.52    by (tactic "fast_tac @{context} FOLP_cs 1")
   19.53  
   19.54  (*7*)
   19.55 -schematic_lemma "?p : P | ~ ~ ~ P"
   19.56 +schematic_goal "?p : P | ~ ~ ~ P"
   19.57    by (tactic "fast_tac @{context} FOLP_cs 1")
   19.58  
   19.59  (*8.  Peirce's law*)
   19.60 -schematic_lemma "?p : ((P-->Q) --> P)  -->  P"
   19.61 +schematic_goal "?p : ((P-->Q) --> P)  -->  P"
   19.62    by (tactic "fast_tac @{context} FOLP_cs 1")
   19.63  
   19.64  (*9*)
   19.65 -schematic_lemma "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
   19.66 +schematic_goal "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
   19.67    by (tactic "fast_tac @{context} FOLP_cs 1")
   19.68  
   19.69  (*10*)
   19.70 -schematic_lemma "?p : (Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)"
   19.71 +schematic_goal "?p : (Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)"
   19.72    by (tactic "fast_tac @{context} FOLP_cs 1")
   19.73  
   19.74  (*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
   19.75 -schematic_lemma "?p : P<->P"
   19.76 +schematic_goal "?p : P<->P"
   19.77    by (tactic "fast_tac @{context} FOLP_cs 1")
   19.78  
   19.79  (*12.  "Dijkstra's law"*)
   19.80 -schematic_lemma "?p : ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))"
   19.81 +schematic_goal "?p : ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))"
   19.82    by (tactic "fast_tac @{context} FOLP_cs 1")
   19.83  
   19.84  (*13.  Distributive law*)
   19.85 -schematic_lemma "?p : P | (Q & R)  <-> (P | Q) & (P | R)"
   19.86 +schematic_goal "?p : P | (Q & R)  <-> (P | Q) & (P | R)"
   19.87    by (tactic "fast_tac @{context} FOLP_cs 1")
   19.88  
   19.89  (*14*)
   19.90 -schematic_lemma "?p : (P <-> Q) <-> ((Q | ~P) & (~Q|P))"
   19.91 +schematic_goal "?p : (P <-> Q) <-> ((Q | ~P) & (~Q|P))"
   19.92    by (tactic "fast_tac @{context} FOLP_cs 1")
   19.93  
   19.94  (*15*)
   19.95 -schematic_lemma "?p : (P --> Q) <-> (~P | Q)"
   19.96 +schematic_goal "?p : (P --> Q) <-> (~P | Q)"
   19.97    by (tactic "fast_tac @{context} FOLP_cs 1")
   19.98  
   19.99  (*16*)
  19.100 -schematic_lemma "?p : (P-->Q) | (Q-->P)"
  19.101 +schematic_goal "?p : (P-->Q) | (Q-->P)"
  19.102    by (tactic "fast_tac @{context} FOLP_cs 1")
  19.103  
  19.104  (*17*)
  19.105 -schematic_lemma "?p : ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))"
  19.106 +schematic_goal "?p : ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))"
  19.107    by (tactic "fast_tac @{context} FOLP_cs 1")
  19.108  
  19.109  
  19.110  text "Classical Logic: examples with quantifiers"
  19.111  
  19.112 -schematic_lemma "?p : (ALL x. P(x) & Q(x)) <-> (ALL x. P(x))  &  (ALL x. Q(x))"
  19.113 +schematic_goal "?p : (ALL x. P(x) & Q(x)) <-> (ALL x. P(x))  &  (ALL x. Q(x))"
  19.114    by (tactic "fast_tac @{context} FOLP_cs 1")
  19.115  
  19.116 -schematic_lemma "?p : (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))"
  19.117 +schematic_goal "?p : (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))"
  19.118    by (tactic "fast_tac @{context} FOLP_cs 1")
  19.119  
  19.120 -schematic_lemma "?p : (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q"
  19.121 +schematic_goal "?p : (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q"
  19.122    by (tactic "fast_tac @{context} FOLP_cs 1")
  19.123  
  19.124 -schematic_lemma "?p : (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)"
  19.125 +schematic_goal "?p : (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)"
  19.126    by (tactic "fast_tac @{context} FOLP_cs 1")
  19.127  
  19.128  
  19.129  text "Problems requiring quantifier duplication"
  19.130  
  19.131  (*Needs multiple instantiation of ALL.*)
  19.132 -schematic_lemma "?p : (ALL x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))"
  19.133 +schematic_goal "?p : (ALL x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))"
  19.134    by (tactic "best_tac @{context} FOLP_dup_cs 1")
  19.135  
  19.136  (*Needs double instantiation of the quantifier*)
  19.137 -schematic_lemma "?p : EX x. P(x) --> P(a) & P(b)"
  19.138 +schematic_goal "?p : EX x. P(x) --> P(a) & P(b)"
  19.139    by (tactic "best_tac @{context} FOLP_dup_cs 1")
  19.140  
  19.141 -schematic_lemma "?p : EX z. P(z) --> (ALL x. P(x))"
  19.142 +schematic_goal "?p : EX z. P(z) --> (ALL x. P(x))"
  19.143    by (tactic "best_tac @{context} FOLP_dup_cs 1")
  19.144  
  19.145  
  19.146  text "Hard examples with quantifiers"
  19.147  
  19.148  text "Problem 18"
  19.149 -schematic_lemma "?p : EX y. ALL x. P(y)-->P(x)"
  19.150 +schematic_goal "?p : EX y. ALL x. P(y)-->P(x)"
  19.151    by (tactic "best_tac @{context} FOLP_dup_cs 1")
  19.152  
  19.153  text "Problem 19"
  19.154 -schematic_lemma "?p : EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
  19.155 +schematic_goal "?p : EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
  19.156    by (tactic "best_tac @{context} FOLP_dup_cs 1")
  19.157  
  19.158  text "Problem 20"
  19.159 -schematic_lemma "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))      
  19.160 +schematic_goal "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))      
  19.161      --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"
  19.162    by (tactic "fast_tac @{context} FOLP_cs 1")
  19.163  
  19.164  text "Problem 21"
  19.165 -schematic_lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))"
  19.166 +schematic_goal "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))"
  19.167    by (tactic "best_tac @{context} FOLP_dup_cs 1")
  19.168  
  19.169  text "Problem 22"
  19.170 -schematic_lemma "?p : (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))"
  19.171 +schematic_goal "?p : (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))"
  19.172    by (tactic "fast_tac @{context} FOLP_cs 1")
  19.173  
  19.174  text "Problem 23"
  19.175 -schematic_lemma "?p : (ALL x. P | Q(x))  <->  (P | (ALL x. Q(x)))"
  19.176 +schematic_goal "?p : (ALL x. P | Q(x))  <->  (P | (ALL x. Q(x)))"
  19.177    by (tactic "best_tac @{context} FOLP_dup_cs 1")
  19.178  
  19.179  text "Problem 24"
  19.180 -schematic_lemma "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &   
  19.181 +schematic_goal "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &   
  19.182       (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))   
  19.183      --> (EX x. P(x)&R(x))"
  19.184    by (tactic "fast_tac @{context} FOLP_cs 1")
  19.185  
  19.186  text "Problem 25"
  19.187 -schematic_lemma "?p : (EX x. P(x)) &  
  19.188 +schematic_goal "?p : (EX x. P(x)) &  
  19.189         (ALL x. L(x) --> ~ (M(x) & R(x))) &  
  19.190         (ALL x. P(x) --> (M(x) & L(x))) &   
  19.191         ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))  
  19.192 @@ -171,13 +171,13 @@
  19.193    oops
  19.194  
  19.195  text "Problem 26"
  19.196 -schematic_lemma "?u : ((EX x. p(x)) <-> (EX x. q(x))) &   
  19.197 +schematic_goal "?u : ((EX x. p(x)) <-> (EX x. q(x))) &   
  19.198       (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))   
  19.199    --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))"
  19.200    by (tactic "fast_tac @{context} FOLP_cs 1")
  19.201  
  19.202  text "Problem 27"
  19.203 -schematic_lemma "?p : (EX x. P(x) & ~Q(x)) &    
  19.204 +schematic_goal "?p : (EX x. P(x) & ~Q(x)) &    
  19.205                (ALL x. P(x) --> R(x)) &    
  19.206                (ALL x. M(x) & L(x) --> P(x)) &    
  19.207                ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))   
  19.208 @@ -185,49 +185,49 @@
  19.209    by (tactic "fast_tac @{context} FOLP_cs 1")
  19.210  
  19.211  text "Problem 28.  AMENDED"
  19.212 -schematic_lemma "?p : (ALL x. P(x) --> (ALL x. Q(x))) &    
  19.213 +schematic_goal "?p : (ALL x. P(x) --> (ALL x. Q(x))) &    
  19.214          ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &   
  19.215          ((EX x. S(x)) --> (ALL x. L(x) --> M(x)))   
  19.216      --> (ALL x. P(x) & L(x) --> M(x))"
  19.217    by (tactic "fast_tac @{context} FOLP_cs 1")
  19.218  
  19.219  text "Problem 29.  Essentially the same as Principia Mathematica *11.71"
  19.220 -schematic_lemma "?p : (EX x. P(x)) & (EX y. Q(y))   
  19.221 +schematic_goal "?p : (EX x. P(x)) & (EX y. Q(y))   
  19.222      --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->      
  19.223           (ALL x y. P(x) & Q(y) --> R(x) & S(y)))"
  19.224    by (tactic "fast_tac @{context} FOLP_cs 1")
  19.225  
  19.226  text "Problem 30"
  19.227 -schematic_lemma "?p : (ALL x. P(x) | Q(x) --> ~ R(x)) &  
  19.228 +schematic_goal "?p : (ALL x. P(x) | Q(x) --> ~ R(x)) &  
  19.229          (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))   
  19.230      --> (ALL x. S(x))"
  19.231    by (tactic "fast_tac @{context} FOLP_cs 1")
  19.232  
  19.233  text "Problem 31"
  19.234 -schematic_lemma "?p : ~(EX x. P(x) & (Q(x) | R(x))) &  
  19.235 +schematic_goal "?p : ~(EX x. P(x) & (Q(x) | R(x))) &  
  19.236          (EX x. L(x) & P(x)) &  
  19.237          (ALL x. ~ R(x) --> M(x))   
  19.238      --> (EX x. L(x) & M(x))"
  19.239    by (tactic "fast_tac @{context} FOLP_cs 1")
  19.240  
  19.241  text "Problem 32"
  19.242 -schematic_lemma "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) &  
  19.243 +schematic_goal "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) &  
  19.244          (ALL x. S(x) & R(x) --> L(x)) &  
  19.245          (ALL x. M(x) --> R(x))   
  19.246      --> (ALL x. P(x) & M(x) --> L(x))"
  19.247    by (tactic "best_tac @{context} FOLP_dup_cs 1")
  19.248  
  19.249  text "Problem 33"
  19.250 -schematic_lemma "?p : (ALL x. P(a) & (P(x)-->P(b))-->P(c))  <->     
  19.251 +schematic_goal "?p : (ALL x. P(a) & (P(x)-->P(b))-->P(c))  <->     
  19.252       (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"
  19.253    by (tactic "best_tac @{context} FOLP_dup_cs 1")
  19.254  
  19.255  text "Problem 35"
  19.256 -schematic_lemma "?p : EX x y. P(x,y) -->  (ALL u v. P(u,v))"
  19.257 +schematic_goal "?p : EX x y. P(x,y) -->  (ALL u v. P(u,v))"
  19.258    by (tactic "best_tac @{context} FOLP_dup_cs 1")
  19.259  
  19.260  text "Problem 36"
  19.261 -schematic_lemma
  19.262 +schematic_goal
  19.263  "?p : (ALL x. EX y. J(x,y)) &  
  19.264        (ALL x. EX y. G(x,y)) &  
  19.265        (ALL x y. J(x,y) | G(x,y) --> (ALL z. J(y,z) | G(y,z) --> H(x,z)))    
  19.266 @@ -235,7 +235,7 @@
  19.267    by (tactic "fast_tac @{context} FOLP_cs 1")
  19.268  
  19.269  text "Problem 37"
  19.270 -schematic_lemma "?p : (ALL z. EX w. ALL x. EX y.  
  19.271 +schematic_goal "?p : (ALL z. EX w. ALL x. EX y.  
  19.272             (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) &  
  19.273          (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) &  
  19.274          ((EX x y. Q(x,y)) --> (ALL x. R(x,x)))   
  19.275 @@ -243,21 +243,21 @@
  19.276    by (tactic "fast_tac @{context} FOLP_cs 1")
  19.277  
  19.278  text "Problem 39"
  19.279 -schematic_lemma "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
  19.280 +schematic_goal "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
  19.281    by (tactic "fast_tac @{context} FOLP_cs 1")
  19.282  
  19.283  text "Problem 40.  AMENDED"
  19.284 -schematic_lemma "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->   
  19.285 +schematic_goal "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->   
  19.286                ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"
  19.287    by (tactic "fast_tac @{context} FOLP_cs 1")
  19.288  
  19.289  text "Problem 41"
  19.290 -schematic_lemma "?p : (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))   
  19.291 +schematic_goal "?p : (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))   
  19.292            --> ~ (EX z. ALL x. f(x,z))"
  19.293    by (tactic "best_tac @{context} FOLP_dup_cs 1")
  19.294  
  19.295  text "Problem 44"
  19.296 -schematic_lemma "?p : (ALL x. f(x) -->                                     
  19.297 +schematic_goal "?p : (ALL x. f(x) -->                                     
  19.298                (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &        
  19.299                (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                    
  19.300                --> (EX x. j(x) & ~f(x))"
  19.301 @@ -266,36 +266,36 @@
  19.302  text "Problems (mainly) involving equality or functions"
  19.303  
  19.304  text "Problem 48"
  19.305 -schematic_lemma "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c"
  19.306 +schematic_goal "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c"
  19.307    by (tactic "fast_tac @{context} FOLP_cs 1")
  19.308  
  19.309  text "Problem 50"
  19.310  (*What has this to do with equality?*)
  19.311 -schematic_lemma "?p : (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))"
  19.312 +schematic_goal "?p : (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))"
  19.313    by (tactic "best_tac @{context} FOLP_dup_cs 1")
  19.314  
  19.315  text "Problem 56"
  19.316 -schematic_lemma
  19.317 +schematic_goal
  19.318   "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
  19.319    by (tactic "fast_tac @{context} FOLP_cs 1")
  19.320  
  19.321  text "Problem 57"
  19.322 -schematic_lemma
  19.323 +schematic_goal
  19.324  "?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &  
  19.325        (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))"
  19.326    by (tactic "fast_tac @{context} FOLP_cs 1")
  19.327  
  19.328  text "Problem 58  NOT PROVED AUTOMATICALLY"
  19.329 -schematic_lemma "?p : (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))"
  19.330 +schematic_goal "?p : (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))"
  19.331    supply f_cong = subst_context [where t = f]
  19.332    by (tactic \<open>fast_tac @{context} (FOLP_cs addSIs [@{thm f_cong}]) 1\<close>)
  19.333  
  19.334  text "Problem 59"
  19.335 -schematic_lemma "?p : (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))"
  19.336 +schematic_goal "?p : (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))"
  19.337    by (tactic "best_tac @{context} FOLP_dup_cs 1")
  19.338  
  19.339  text "Problem 60"
  19.340 -schematic_lemma "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
  19.341 +schematic_goal "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
  19.342    by (tactic "fast_tac @{context} FOLP_cs 1")
  19.343  
  19.344  end
    20.1 --- a/src/FOLP/ex/Foundation.thy	Tue Oct 06 13:31:44 2015 +0200
    20.2 +++ b/src/FOLP/ex/Foundation.thy	Tue Oct 06 15:14:28 2015 +0200
    20.3 @@ -9,7 +9,7 @@
    20.4  imports IFOLP
    20.5  begin
    20.6  
    20.7 -schematic_lemma "?p : A&B  --> (C-->A&C)"
    20.8 +schematic_goal "?p : A&B  --> (C-->A&C)"
    20.9  apply (rule impI)
   20.10  apply (rule impI)
   20.11  apply (rule conjI)
   20.12 @@ -19,7 +19,7 @@
   20.13  done
   20.14  
   20.15  text \<open>A form of conj-elimination\<close>
   20.16 -schematic_lemma
   20.17 +schematic_goal
   20.18    assumes "p : A & B"
   20.19      and "!!x y. x : A ==> y : B ==> f(x, y) : C"
   20.20    shows "?p : C"
   20.21 @@ -30,7 +30,7 @@
   20.22  apply (rule assms)
   20.23  done
   20.24  
   20.25 -schematic_lemma
   20.26 +schematic_goal
   20.27    assumes "!!A x. x : ~ ~A ==> cla(x) : A"
   20.28    shows "?p : B | ~B"
   20.29  apply (rule assms)
   20.30 @@ -48,7 +48,7 @@
   20.31  apply assumption
   20.32  done
   20.33  
   20.34 -schematic_lemma
   20.35 +schematic_goal
   20.36    assumes "!!A x. x : ~ ~A ==> cla(x) : A"
   20.37    shows "?p : B | ~B"
   20.38  apply (rule assms)
   20.39 @@ -63,7 +63,7 @@
   20.40  done
   20.41  
   20.42  
   20.43 -schematic_lemma
   20.44 +schematic_goal
   20.45    assumes "p : A | ~A"
   20.46      and "q : ~ ~A"
   20.47    shows "?p : A"
   20.48 @@ -79,7 +79,7 @@
   20.49  
   20.50  subsection "Examples with quantifiers"
   20.51  
   20.52 -schematic_lemma
   20.53 +schematic_goal
   20.54    assumes "p : ALL z. G(z)"
   20.55    shows "?p : ALL z. G(z)|H(z)"
   20.56  apply (rule allI)
   20.57 @@ -87,20 +87,20 @@
   20.58  apply (rule assms [THEN spec])
   20.59  done
   20.60  
   20.61 -schematic_lemma "?p : ALL x. EX y. x=y"
   20.62 +schematic_goal "?p : ALL x. EX y. x=y"
   20.63  apply (rule allI)
   20.64  apply (rule exI)
   20.65  apply (rule refl)
   20.66  done
   20.67  
   20.68 -schematic_lemma "?p : EX y. ALL x. x=y"
   20.69 +schematic_goal "?p : EX y. ALL x. x=y"
   20.70  apply (rule exI)
   20.71  apply (rule allI)
   20.72  apply (rule refl)?
   20.73  oops
   20.74  
   20.75  text \<open>Parallel lifting example.\<close>
   20.76 -schematic_lemma "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)"
   20.77 +schematic_goal "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)"
   20.78  apply (rule exI allI)
   20.79  apply (rule exI allI)
   20.80  apply (rule exI allI)
   20.81 @@ -108,7 +108,7 @@
   20.82  apply (rule exI allI)
   20.83  oops
   20.84  
   20.85 -schematic_lemma
   20.86 +schematic_goal
   20.87    assumes "p : (EX z. F(z)) & B"
   20.88    shows "?p : EX z. F(z) & B"
   20.89  apply (rule conjE)
   20.90 @@ -122,7 +122,7 @@
   20.91  done
   20.92  
   20.93  text \<open>A bigger demonstration of quantifiers -- not in the paper.\<close>
   20.94 -schematic_lemma "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
   20.95 +schematic_goal "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
   20.96  apply (rule impI)
   20.97  apply (rule allI)
   20.98  apply (rule exE, assumption)
    21.1 --- a/src/FOLP/ex/If.thy	Tue Oct 06 13:31:44 2015 +0200
    21.2 +++ b/src/FOLP/ex/If.thy	Tue Oct 06 15:14:28 2015 +0200
    21.3 @@ -5,14 +5,14 @@
    21.4  definition "if" :: "[o,o,o]=>o" where
    21.5    "if(P,Q,R) == P&Q | ~P&R"
    21.6  
    21.7 -schematic_lemma ifI:
    21.8 +schematic_goal ifI:
    21.9    assumes "!!x. x : P ==> f(x) : Q"  "!!x. x : ~P ==> g(x) : R"
   21.10    shows "?p : if(P,Q,R)"
   21.11  apply (unfold if_def)
   21.12  apply (tactic \<open>fast_tac @{context} (FOLP_cs addIs @{thms assms}) 1\<close>)
   21.13  done
   21.14  
   21.15 -schematic_lemma ifE:
   21.16 +schematic_goal ifE:
   21.17    assumes 1: "p : if(P,Q,R)" and
   21.18      2: "!!x y. [| x : P; y : Q |] ==> f(x, y) : S" and
   21.19      3: "!!x y. [| x : ~P; y : R |] ==> g(x, y) : S"
   21.20 @@ -22,7 +22,7 @@
   21.21  apply (tactic \<open>fast_tac @{context} (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1\<close>)
   21.22  done
   21.23  
   21.24 -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))"
   21.25 +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))"
   21.26  apply (rule iffI)
   21.27  apply (erule ifE)
   21.28  apply (erule ifE)
   21.29 @@ -32,11 +32,11 @@
   21.30  
   21.31  ML \<open>val if_cs = FOLP_cs addSIs [@{thm ifI}] addSEs [@{thm ifE}]\<close>
   21.32  
   21.33 -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))"
   21.34 +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))"
   21.35  apply (tactic \<open>fast_tac @{context} if_cs 1\<close>)
   21.36  done
   21.37  
   21.38 -schematic_lemma nested_ifs: "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
   21.39 +schematic_goal nested_ifs: "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
   21.40  apply (tactic \<open>fast_tac @{context} if_cs 1\<close>)
   21.41  done
   21.42  
    22.1 --- a/src/FOLP/ex/Intro.thy	Tue Oct 06 13:31:44 2015 +0200
    22.2 +++ b/src/FOLP/ex/Intro.thy	Tue Oct 06 15:14:28 2015 +0200
    22.3 @@ -13,7 +13,7 @@
    22.4  
    22.5  subsubsection \<open>Some simple backward proofs\<close>
    22.6  
    22.7 -schematic_lemma mythm: "?p : P|P --> P"
    22.8 +schematic_goal mythm: "?p : P|P --> P"
    22.9  apply (rule impI)
   22.10  apply (rule disjE)
   22.11  prefer 3 apply (assumption)
   22.12 @@ -21,7 +21,7 @@
   22.13  apply assumption
   22.14  done
   22.15  
   22.16 -schematic_lemma "?p : (P & Q) | R --> (P | R)"
   22.17 +schematic_goal "?p : (P & Q) | R --> (P | R)"
   22.18  apply (rule impI)
   22.19  apply (erule disjE)
   22.20  apply (drule conjunct1)
   22.21 @@ -31,7 +31,7 @@
   22.22  done
   22.23  
   22.24  (*Correct version, delaying use of "spec" until last*)
   22.25 -schematic_lemma "?p : (ALL x y. P(x,y)) --> (ALL z w. P(w,z))"
   22.26 +schematic_goal "?p : (ALL x y. P(x,y)) --> (ALL z w. P(w,z))"
   22.27  apply (rule impI)
   22.28  apply (rule allI)
   22.29  apply (rule allI)
   22.30 @@ -43,13 +43,13 @@
   22.31  
   22.32  subsubsection \<open>Demonstration of @{text "fast"}\<close>
   22.33  
   22.34 -schematic_lemma "?p : (EX y. ALL x. J(y,x) <-> ~J(x,x))
   22.35 +schematic_goal "?p : (EX y. ALL x. J(y,x) <-> ~J(x,x))
   22.36          -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))"
   22.37  apply (tactic \<open>fast_tac @{context} FOLP_cs 1\<close>)
   22.38  done
   22.39  
   22.40  
   22.41 -schematic_lemma "?p : ALL x. P(x,f(x)) <->
   22.42 +schematic_goal "?p : ALL x. P(x,f(x)) <->
   22.43          (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
   22.44  apply (tactic \<open>fast_tac @{context} FOLP_cs 1\<close>)
   22.45  done
   22.46 @@ -57,7 +57,7 @@
   22.47  
   22.48  subsubsection \<open>Derivation of conjunction elimination rule\<close>
   22.49  
   22.50 -schematic_lemma
   22.51 +schematic_goal
   22.52    assumes major: "p : P&Q"
   22.53      and minor: "!!x y. [| x : P; y : Q |] ==> f(x, y) : R"
   22.54    shows "?p : R"
   22.55 @@ -71,7 +71,7 @@
   22.56  
   22.57  text \<open>Derivation of negation introduction\<close>
   22.58  
   22.59 -schematic_lemma
   22.60 +schematic_goal
   22.61    assumes "!!x. x : P ==> f(x) : False"
   22.62    shows "?p : ~ P"
   22.63  apply (unfold not_def)
   22.64 @@ -80,7 +80,7 @@
   22.65  apply assumption
   22.66  done
   22.67  
   22.68 -schematic_lemma
   22.69 +schematic_goal
   22.70    assumes major: "p : ~P"
   22.71      and minor: "q : P"
   22.72    shows "?p : R"
   22.73 @@ -91,7 +91,7 @@
   22.74  done
   22.75  
   22.76  text \<open>Alternative proof of the result above\<close>
   22.77 -schematic_lemma
   22.78 +schematic_goal
   22.79    assumes major: "p : ~P"
   22.80      and minor: "q : P"
   22.81    shows "?p : R"
    23.1 --- a/src/FOLP/ex/Intuitionistic.thy	Tue Oct 06 13:31:44 2015 +0200
    23.2 +++ b/src/FOLP/ex/Intuitionistic.thy	Tue Oct 06 15:14:28 2015 +0200
    23.3 @@ -30,39 +30,39 @@
    23.4  imports IFOLP
    23.5  begin
    23.6  
    23.7 -schematic_lemma "?p : ~~(P&Q) <-> ~~P & ~~Q"
    23.8 +schematic_goal "?p : ~~(P&Q) <-> ~~P & ~~Q"
    23.9    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   23.10  
   23.11 -schematic_lemma "?p : ~~~P <-> ~P"
   23.12 +schematic_goal "?p : ~~~P <-> ~P"
   23.13    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   23.14  
   23.15 -schematic_lemma "?p : ~~((P --> Q | R)  -->  (P-->Q) | (P-->R))"
   23.16 +schematic_goal "?p : ~~((P --> Q | R)  -->  (P-->Q) | (P-->R))"
   23.17    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   23.18  
   23.19 -schematic_lemma "?p : (P<->Q) <-> (Q<->P)"
   23.20 +schematic_goal "?p : (P<->Q) <-> (Q<->P)"
   23.21    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   23.22  
   23.23  
   23.24  subsection \<open>Lemmas for the propositional double-negation translation\<close>
   23.25  
   23.26 -schematic_lemma "?p : P --> ~~P"
   23.27 +schematic_goal "?p : P --> ~~P"
   23.28    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   23.29  
   23.30 -schematic_lemma "?p : ~~(~~P --> P)"
   23.31 +schematic_goal "?p : ~~(~~P --> P)"
   23.32    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   23.33  
   23.34 -schematic_lemma "?p : ~~P & ~~(P --> Q) --> ~~Q"
   23.35 +schematic_goal "?p : ~~P & ~~(P --> Q) --> ~~Q"
   23.36    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   23.37  
   23.38  
   23.39  subsection \<open>The following are classically but not constructively valid\<close>
   23.40  
   23.41  (*The attempt to prove them terminates quickly!*)
   23.42 -schematic_lemma "?p : ((P-->Q) --> P)  -->  P"
   23.43 +schematic_goal "?p : ((P-->Q) --> P)  -->  P"
   23.44    apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
   23.45    oops
   23.46  
   23.47 -schematic_lemma "?p : (P&Q-->R)  -->  (P-->R) | (Q-->R)"
   23.48 +schematic_goal "?p : (P&Q-->R)  -->  (P-->R) | (Q-->R)"
   23.49    apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
   23.50    oops
   23.51  
   23.52 @@ -70,74 +70,74 @@
   23.53  subsection \<open>Intuitionistic FOL: propositional problems based on Pelletier\<close>
   23.54  
   23.55  text "Problem ~~1"
   23.56 -schematic_lemma "?p : ~~((P-->Q)  <->  (~Q --> ~P))"
   23.57 +schematic_goal "?p : ~~((P-->Q)  <->  (~Q --> ~P))"
   23.58    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   23.59  
   23.60  text "Problem ~~2"
   23.61 -schematic_lemma "?p : ~~(~~P  <->  P)"
   23.62 +schematic_goal "?p : ~~(~~P  <->  P)"
   23.63    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   23.64  
   23.65  text "Problem 3"
   23.66 -schematic_lemma "?p : ~(P-->Q) --> (Q-->P)"
   23.67 +schematic_goal "?p : ~(P-->Q) --> (Q-->P)"
   23.68    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   23.69  
   23.70  text "Problem ~~4"
   23.71 -schematic_lemma "?p : ~~((~P-->Q)  <->  (~Q --> P))"
   23.72 +schematic_goal "?p : ~~((~P-->Q)  <->  (~Q --> P))"
   23.73    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   23.74  
   23.75  text "Problem ~~5"
   23.76 -schematic_lemma "?p : ~~((P|Q-->P|R) --> P|(Q-->R))"
   23.77 +schematic_goal "?p : ~~((P|Q-->P|R) --> P|(Q-->R))"
   23.78    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   23.79  
   23.80  text "Problem ~~6"
   23.81 -schematic_lemma "?p : ~~(P | ~P)"
   23.82 +schematic_goal "?p : ~~(P | ~P)"
   23.83    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   23.84  
   23.85  text "Problem ~~7"
   23.86 -schematic_lemma "?p : ~~(P | ~~~P)"
   23.87 +schematic_goal "?p : ~~(P | ~~~P)"
   23.88    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   23.89  
   23.90  text "Problem ~~8.  Peirce's law"
   23.91 -schematic_lemma "?p : ~~(((P-->Q) --> P)  -->  P)"
   23.92 +schematic_goal "?p : ~~(((P-->Q) --> P)  -->  P)"
   23.93    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   23.94  
   23.95  text "Problem 9"
   23.96 -schematic_lemma "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
   23.97 +schematic_goal "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
   23.98    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   23.99  
  23.100  text "Problem 10"
  23.101 -schematic_lemma "?p : (Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)"
  23.102 +schematic_goal "?p : (Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)"
  23.103    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
  23.104  
  23.105  text "11.  Proved in each direction (incorrectly, says Pelletier!!) "
  23.106 -schematic_lemma "?p : P<->P"
  23.107 +schematic_goal "?p : P<->P"
  23.108    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
  23.109  
  23.110  text "Problem ~~12.  Dijkstra's law  "
  23.111 -schematic_lemma "?p : ~~(((P <-> Q) <-> R)  <->  (P <-> (Q <-> R)))"
  23.112 +schematic_goal "?p : ~~(((P <-> Q) <-> R)  <->  (P <-> (Q <-> R)))"
  23.113    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
  23.114  
  23.115 -schematic_lemma "?p : ((P <-> Q) <-> R)  -->  ~~(P <-> (Q <-> R))"
  23.116 +schematic_goal "?p : ((P <-> Q) <-> R)  -->  ~~(P <-> (Q <-> R))"
  23.117    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
  23.118  
  23.119  text "Problem 13.  Distributive law"
  23.120 -schematic_lemma "?p : P | (Q & R)  <-> (P | Q) & (P | R)"
  23.121 +schematic_goal "?p : P | (Q & R)  <-> (P | Q) & (P | R)"
  23.122    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
  23.123  
  23.124  text "Problem ~~14"
  23.125 -schematic_lemma "?p : ~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))"
  23.126 +schematic_goal "?p : ~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))"
  23.127    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
  23.128  
  23.129  text "Problem ~~15"
  23.130 -schematic_lemma "?p : ~~((P --> Q) <-> (~P | Q))"
  23.131 +schematic_goal "?p : ~~((P --> Q) <-> (~P | Q))"
  23.132    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
  23.133  
  23.134  text "Problem ~~16"
  23.135 -schematic_lemma "?p : ~~((P-->Q) | (Q-->P))"
  23.136 +schematic_goal "?p : ~~((P-->Q) | (Q-->P))"
  23.137    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
  23.138  
  23.139  text "Problem ~~17"
  23.140 -schematic_lemma "?p : ~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))"
  23.141 +schematic_goal "?p : ~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))"
  23.142    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)  -- slow
  23.143  
  23.144  
  23.145 @@ -145,43 +145,43 @@
  23.146  
  23.147  text "The converse is classical in the following implications..."
  23.148  
  23.149 -schematic_lemma "?p : (EX x. P(x)-->Q)  -->  (ALL x. P(x)) --> Q"
  23.150 +schematic_goal "?p : (EX x. P(x)-->Q)  -->  (ALL x. P(x)) --> Q"
  23.151    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
  23.152  
  23.153 -schematic_lemma "?p : ((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)"
  23.154 +schematic_goal "?p : ((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)"
  23.155    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
  23.156  
  23.157 -schematic_lemma "?p : ((ALL x. ~P(x))-->Q)  -->  ~ (ALL x. ~ (P(x)|Q))"
  23.158 +schematic_goal "?p : ((ALL x. ~P(x))-->Q)  -->  ~ (ALL x. ~ (P(x)|Q))"
  23.159    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
  23.160  
  23.161 -schematic_lemma "?p : (ALL x. P(x)) | Q  -->  (ALL x. P(x) | Q)"
  23.162 +schematic_goal "?p : (ALL x. P(x)) | Q  -->  (ALL x. P(x) | Q)"
  23.163    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
  23.164  
  23.165 -schematic_lemma "?p : (EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))"
  23.166 +schematic_goal "?p : (EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))"
  23.167    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
  23.168  
  23.169  
  23.170  text "The following are not constructively valid!"
  23.171  text "The attempt to prove them terminates quickly!"
  23.172  
  23.173 -schematic_lemma "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)"
  23.174 +schematic_goal "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)"
  23.175    apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
  23.176    oops
  23.177  
  23.178 -schematic_lemma "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))"
  23.179 +schematic_goal "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))"
  23.180    apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
  23.181    oops
  23.182  
  23.183 -schematic_lemma "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)"
  23.184 +schematic_goal "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)"
  23.185    apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
  23.186    oops
  23.187  
  23.188 -schematic_lemma "?p : (ALL x. ~~P(x)) --> ~~(ALL x. P(x))"
  23.189 +schematic_goal "?p : (ALL x. ~~P(x)) --> ~~(ALL x. P(x))"
  23.190    apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
  23.191    oops
  23.192  
  23.193  (*Classically but not intuitionistically valid.  Proved by a bug in 1986!*)
  23.194 -schematic_lemma "?p : EX x. Q(x) --> (ALL x. Q(x))"
  23.195 +schematic_goal "?p : EX x. Q(x) --> (ALL x. Q(x))"
  23.196    apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
  23.197    oops
  23.198  
  23.199 @@ -194,32 +194,32 @@
  23.200  \<close>
  23.201  
  23.202  text "Problem ~~18"
  23.203 -schematic_lemma "?p : ~~(EX y. ALL x. P(y)-->P(x))" oops
  23.204 +schematic_goal "?p : ~~(EX y. ALL x. P(y)-->P(x))" oops
  23.205  (*NOT PROVED*)
  23.206  
  23.207  text "Problem ~~19"
  23.208 -schematic_lemma "?p : ~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))" oops
  23.209 +schematic_goal "?p : ~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))" oops
  23.210  (*NOT PROVED*)
  23.211  
  23.212  text "Problem 20"
  23.213 -schematic_lemma "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))      
  23.214 +schematic_goal "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))      
  23.215      --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"
  23.216    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
  23.217  
  23.218  text "Problem 21"
  23.219 -schematic_lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))" oops
  23.220 +schematic_goal "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))" oops
  23.221  (*NOT PROVED*)
  23.222  
  23.223  text "Problem 22"
  23.224 -schematic_lemma "?p : (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))"
  23.225 +schematic_goal "?p : (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))"
  23.226    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
  23.227  
  23.228  text "Problem ~~23"
  23.229 -schematic_lemma "?p : ~~ ((ALL x. P | Q(x))  <->  (P | (ALL x. Q(x))))"
  23.230 +schematic_goal "?p : ~~ ((ALL x. P | Q(x))  <->  (P | (ALL x. Q(x))))"
  23.231    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
  23.232  
  23.233  text "Problem 24"
  23.234 -schematic_lemma "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &   
  23.235 +schematic_goal "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &   
  23.236       (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))   
  23.237      --> ~~(EX x. P(x)&R(x))"
  23.238  (*Not clear why fast_tac, best_tac, ASTAR and ITER_DEEPEN all take forever*)
  23.239 @@ -230,7 +230,7 @@
  23.240    done
  23.241  
  23.242  text "Problem 25"
  23.243 -schematic_lemma "?p : (EX x. P(x)) &   
  23.244 +schematic_goal "?p : (EX x. P(x)) &   
  23.245          (ALL x. L(x) --> ~ (M(x) & R(x))) &   
  23.246          (ALL x. P(x) --> (M(x) & L(x))) &    
  23.247          ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))   
  23.248 @@ -238,69 +238,69 @@
  23.249    by (tactic "IntPr.best_tac @{context} 1")
  23.250  
  23.251  text "Problem 29.  Essentially the same as Principia Mathematica *11.71"
  23.252 -schematic_lemma "?p : (EX x. P(x)) & (EX y. Q(y))   
  23.253 +schematic_goal "?p : (EX x. P(x)) & (EX y. Q(y))   
  23.254      --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->      
  23.255           (ALL x y. P(x) & Q(y) --> R(x) & S(y)))"
  23.256    by (tactic "IntPr.fast_tac @{context} 1")
  23.257  
  23.258  text "Problem ~~30"
  23.259 -schematic_lemma "?p : (ALL x. (P(x) | Q(x)) --> ~ R(x)) &  
  23.260 +schematic_goal "?p : (ALL x. (P(x) | Q(x)) --> ~ R(x)) &  
  23.261          (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))   
  23.262      --> (ALL x. ~~S(x))"
  23.263    by (tactic "IntPr.fast_tac @{context} 1")
  23.264  
  23.265  text "Problem 31"
  23.266 -schematic_lemma "?p : ~(EX x. P(x) & (Q(x) | R(x))) &  
  23.267 +schematic_goal "?p : ~(EX x. P(x) & (Q(x) | R(x))) &  
  23.268          (EX x. L(x) & P(x)) &  
  23.269          (ALL x. ~ R(x) --> M(x))   
  23.270      --> (EX x. L(x) & M(x))"
  23.271    by (tactic "IntPr.fast_tac @{context} 1")
  23.272  
  23.273  text "Problem 32"
  23.274 -schematic_lemma "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) &  
  23.275 +schematic_goal "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) &  
  23.276          (ALL x. S(x) & R(x) --> L(x)) &  
  23.277          (ALL x. M(x) --> R(x))   
  23.278      --> (ALL x. P(x) & M(x) --> L(x))"
  23.279    by (tactic "IntPr.best_tac @{context} 1") -- slow
  23.280  
  23.281  text "Problem 39"
  23.282 -schematic_lemma "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
  23.283 +schematic_goal "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
  23.284    by (tactic "IntPr.best_tac @{context} 1")
  23.285  
  23.286  text "Problem 40.  AMENDED"
  23.287 -schematic_lemma "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->   
  23.288 +schematic_goal "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->   
  23.289                ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"
  23.290    by (tactic "IntPr.best_tac @{context} 1") -- slow
  23.291  
  23.292  text "Problem 44"
  23.293 -schematic_lemma "?p : (ALL x. f(x) -->                                    
  23.294 +schematic_goal "?p : (ALL x. f(x) -->                                    
  23.295                (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &        
  23.296                (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                    
  23.297                --> (EX x. j(x) & ~f(x))"
  23.298    by (tactic "IntPr.best_tac @{context} 1")
  23.299  
  23.300  text "Problem 48"
  23.301 -schematic_lemma "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c"
  23.302 +schematic_goal "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c"
  23.303    by (tactic "IntPr.best_tac @{context} 1")
  23.304  
  23.305  text "Problem 51"
  23.306 -schematic_lemma
  23.307 +schematic_goal
  23.308      "?p : (EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->   
  23.309       (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)"
  23.310    by (tactic "IntPr.best_tac @{context} 1") -- \<open>60 seconds\<close>
  23.311  
  23.312  text "Problem 56"
  23.313 -schematic_lemma "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
  23.314 +schematic_goal "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
  23.315    by (tactic "IntPr.best_tac @{context} 1")
  23.316  
  23.317  text "Problem 57"
  23.318 -schematic_lemma
  23.319 +schematic_goal
  23.320      "?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &  
  23.321       (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))"
  23.322    by (tactic "IntPr.best_tac @{context} 1")
  23.323  
  23.324  text "Problem 60"
  23.325 -schematic_lemma "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
  23.326 +schematic_goal "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
  23.327    by (tactic "IntPr.best_tac @{context} 1")
  23.328  
  23.329  end
    24.1 --- a/src/FOLP/ex/Nat.thy	Tue Oct 06 13:31:44 2015 +0200
    24.2 +++ b/src/FOLP/ex/Nat.thy	Tue Oct 06 15:14:28 2015 +0200
    24.3 @@ -40,7 +40,7 @@
    24.4  
    24.5  subsection \<open>Proofs about the natural numbers\<close>
    24.6  
    24.7 -schematic_lemma Suc_n_not_n: "?p : ~ (Suc(k) = k)"
    24.8 +schematic_goal Suc_n_not_n: "?p : ~ (Suc(k) = k)"
    24.9  apply (rule_tac n = k in induct)
   24.10  apply (rule notI)
   24.11  apply (erule Suc_neq_0)
   24.12 @@ -49,7 +49,7 @@
   24.13  apply (erule Suc_inject)
   24.14  done
   24.15  
   24.16 -schematic_lemma "?p : (k+m)+n = k+(m+n)"
   24.17 +schematic_goal "?p : (k+m)+n = k+(m+n)"
   24.18  apply (rule induct)
   24.19  back
   24.20  back
   24.21 @@ -59,23 +59,23 @@
   24.22  back
   24.23  oops
   24.24  
   24.25 -schematic_lemma add_0 [simp]: "?p : 0+n = n"
   24.26 +schematic_goal add_0 [simp]: "?p : 0+n = n"
   24.27  apply (unfold add_def)
   24.28  apply (rule rec_0)
   24.29  done
   24.30  
   24.31 -schematic_lemma add_Suc [simp]: "?p : Suc(m)+n = Suc(m+n)"
   24.32 +schematic_goal add_Suc [simp]: "?p : Suc(m)+n = Suc(m+n)"
   24.33  apply (unfold add_def)
   24.34  apply (rule rec_Suc)
   24.35  done
   24.36  
   24.37  
   24.38 -schematic_lemma Suc_cong: "p : x = y \<Longrightarrow> ?p : Suc(x) = Suc(y)"
   24.39 +schematic_goal Suc_cong: "p : x = y \<Longrightarrow> ?p : Suc(x) = Suc(y)"
   24.40    apply (erule subst)
   24.41    apply (rule refl)
   24.42    done
   24.43  
   24.44 -schematic_lemma Plus_cong: "[| p : a = x;  q: b = y |] ==> ?p : a + b = x + y"
   24.45 +schematic_goal Plus_cong: "[| p : a = x;  q: b = y |] ==> ?p : a + b = x + y"
   24.46    apply (erule subst, erule subst, rule refl)
   24.47    done
   24.48  
   24.49 @@ -87,19 +87,19 @@
   24.50      |> fold (addrew @{context}) @{thms add_0 add_Suc}
   24.51  \<close>
   24.52  
   24.53 -schematic_lemma add_assoc: "?p : (k+m)+n = k+(m+n)"
   24.54 +schematic_goal add_assoc: "?p : (k+m)+n = k+(m+n)"
   24.55  apply (rule_tac n = k in induct)
   24.56  apply (tactic \<open>SIMP_TAC @{context} add_ss 1\<close>)
   24.57  apply (tactic \<open>ASM_SIMP_TAC @{context} add_ss 1\<close>)
   24.58  done
   24.59  
   24.60 -schematic_lemma add_0_right: "?p : m+0 = m"
   24.61 +schematic_goal add_0_right: "?p : m+0 = m"
   24.62  apply (rule_tac n = m in induct)
   24.63  apply (tactic \<open>SIMP_TAC @{context} add_ss 1\<close>)
   24.64  apply (tactic \<open>ASM_SIMP_TAC @{context} add_ss 1\<close>)
   24.65  done
   24.66  
   24.67 -schematic_lemma add_Suc_right: "?p : m+Suc(n) = Suc(m+n)"
   24.68 +schematic_goal add_Suc_right: "?p : m+Suc(n) = Suc(m+n)"
   24.69  apply (rule_tac n = m in induct)
   24.70  apply (tactic \<open>ALLGOALS (ASM_SIMP_TAC @{context} add_ss)\<close>)
   24.71  done
    25.1 --- a/src/FOLP/ex/Propositional_Cla.thy	Tue Oct 06 13:31:44 2015 +0200
    25.2 +++ b/src/FOLP/ex/Propositional_Cla.thy	Tue Oct 06 15:14:28 2015 +0200
    25.3 @@ -11,103 +11,103 @@
    25.4  
    25.5  
    25.6  text "commutative laws of & and | "
    25.7 -schematic_lemma "?p : P & Q  -->  Q & P"
    25.8 +schematic_goal "?p : P & Q  -->  Q & P"
    25.9    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   25.10  
   25.11 -schematic_lemma "?p : P | Q  -->  Q | P"
   25.12 +schematic_goal "?p : P | Q  -->  Q | P"
   25.13    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   25.14  
   25.15  
   25.16  text "associative laws of & and | "
   25.17 -schematic_lemma "?p : (P & Q) & R  -->  P & (Q & R)"
   25.18 +schematic_goal "?p : (P & Q) & R  -->  P & (Q & R)"
   25.19    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   25.20  
   25.21 -schematic_lemma "?p : (P | Q) | R  -->  P | (Q | R)"
   25.22 +schematic_goal "?p : (P | Q) | R  -->  P | (Q | R)"
   25.23    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   25.24  
   25.25  
   25.26  text "distributive laws of & and | "
   25.27 -schematic_lemma "?p : (P & Q) | R  --> (P | R) & (Q | R)"
   25.28 +schematic_goal "?p : (P & Q) | R  --> (P | R) & (Q | R)"
   25.29    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   25.30  
   25.31 -schematic_lemma "?p : (P | R) & (Q | R)  --> (P & Q) | R"
   25.32 +schematic_goal "?p : (P | R) & (Q | R)  --> (P & Q) | R"
   25.33    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   25.34  
   25.35 -schematic_lemma "?p : (P | Q) & R  --> (P & R) | (Q & R)"
   25.36 +schematic_goal "?p : (P | Q) & R  --> (P & R) | (Q & R)"
   25.37    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   25.38  
   25.39  
   25.40 -schematic_lemma "?p : (P & R) | (Q & R)  --> (P | Q) & R"
   25.41 +schematic_goal "?p : (P & R) | (Q & R)  --> (P | Q) & R"
   25.42    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   25.43  
   25.44  
   25.45  text "Laws involving implication"
   25.46  
   25.47 -schematic_lemma "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)"
   25.48 +schematic_goal "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)"
   25.49    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   25.50  
   25.51 -schematic_lemma "?p : (P & Q --> R) <-> (P--> (Q-->R))"
   25.52 +schematic_goal "?p : (P & Q --> R) <-> (P--> (Q-->R))"
   25.53    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   25.54  
   25.55 -schematic_lemma "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
   25.56 +schematic_goal "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
   25.57    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   25.58  
   25.59 -schematic_lemma "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
   25.60 +schematic_goal "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
   25.61    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   25.62  
   25.63 -schematic_lemma "?p : (P --> Q & R) <-> (P-->Q)  &  (P-->R)"
   25.64 +schematic_goal "?p : (P --> Q & R) <-> (P-->Q)  &  (P-->R)"
   25.65    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   25.66  
   25.67  
   25.68  text "Propositions-as-types"
   25.69  
   25.70  (*The combinator K*)
   25.71 -schematic_lemma "?p : P --> (Q --> P)"
   25.72 +schematic_goal "?p : P --> (Q --> P)"
   25.73    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   25.74  
   25.75  (*The combinator S*)
   25.76 -schematic_lemma "?p : (P-->Q-->R)  --> (P-->Q) --> (P-->R)"
   25.77 +schematic_goal "?p : (P-->Q-->R)  --> (P-->Q) --> (P-->R)"
   25.78    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   25.79  
   25.80  
   25.81  (*Converse is classical*)
   25.82 -schematic_lemma "?p : (P-->Q) | (P-->R)  -->  (P --> Q | R)"
   25.83 +schematic_goal "?p : (P-->Q) | (P-->R)  -->  (P --> Q | R)"
   25.84    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   25.85  
   25.86 -schematic_lemma "?p : (P-->Q)  -->  (~Q --> ~P)"
   25.87 +schematic_goal "?p : (P-->Q)  -->  (~Q --> ~P)"
   25.88    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   25.89  
   25.90  
   25.91  text "Schwichtenberg's examples (via T. Nipkow)"
   25.92  
   25.93 -schematic_lemma stab_imp: "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
   25.94 +schematic_goal stab_imp: "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
   25.95    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   25.96  
   25.97 -schematic_lemma stab_to_peirce: "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)  
   25.98 +schematic_goal stab_to_peirce: "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)  
   25.99                --> ((P --> Q) --> P) --> P"
  25.100    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
  25.101  
  25.102 -schematic_lemma peirce_imp1: "?p : (((Q --> R) --> Q) --> Q)  
  25.103 +schematic_goal peirce_imp1: "?p : (((Q --> R) --> Q) --> Q)  
  25.104                 --> (((P --> Q) --> R) --> P --> Q) --> P --> Q"
  25.105    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
  25.106    
  25.107 -schematic_lemma peirce_imp2: "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
  25.108 +schematic_goal peirce_imp2: "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
  25.109    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
  25.110  
  25.111 -schematic_lemma mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q"
  25.112 +schematic_goal mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q"
  25.113    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
  25.114  
  25.115 -schematic_lemma mints_solovev: "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
  25.116 +schematic_goal mints_solovev: "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
  25.117    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
  25.118  
  25.119 -schematic_lemma tatsuta: "?p : (((P7 --> P1) --> P10) --> P4 --> P5)  
  25.120 +schematic_goal tatsuta: "?p : (((P7 --> P1) --> P10) --> P4 --> P5)  
  25.121            --> (((P8 --> P2) --> P9) --> P3 --> P10)  
  25.122            --> (P1 --> P8) --> P6 --> P7  
  25.123            --> (((P3 --> P2) --> P9) --> P4)  
  25.124            --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5"
  25.125    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
  25.126  
  25.127 -schematic_lemma tatsuta1: "?p : (((P8 --> P2) --> P9) --> P3 --> P10)  
  25.128 +schematic_goal tatsuta1: "?p : (((P8 --> P2) --> P9) --> P3 --> P10)  
  25.129       --> (((P3 --> P2) --> P9) --> P4)  
  25.130       --> (((P6 --> P1) --> P2) --> P9)  
  25.131       --> (((P7 --> P1) --> P10) --> P4 --> P5)  
    26.1 --- a/src/FOLP/ex/Propositional_Int.thy	Tue Oct 06 13:31:44 2015 +0200
    26.2 +++ b/src/FOLP/ex/Propositional_Int.thy	Tue Oct 06 15:14:28 2015 +0200
    26.3 @@ -11,103 +11,103 @@
    26.4  
    26.5  
    26.6  text "commutative laws of & and | "
    26.7 -schematic_lemma "?p : P & Q  -->  Q & P"
    26.8 +schematic_goal "?p : P & Q  -->  Q & P"
    26.9    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   26.10  
   26.11 -schematic_lemma "?p : P | Q  -->  Q | P"
   26.12 +schematic_goal "?p : P | Q  -->  Q | P"
   26.13    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   26.14  
   26.15  
   26.16  text "associative laws of & and | "
   26.17 -schematic_lemma "?p : (P & Q) & R  -->  P & (Q & R)"
   26.18 +schematic_goal "?p : (P & Q) & R  -->  P & (Q & R)"
   26.19    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   26.20  
   26.21 -schematic_lemma "?p : (P | Q) | R  -->  P | (Q | R)"
   26.22 +schematic_goal "?p : (P | Q) | R  -->  P | (Q | R)"
   26.23    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   26.24  
   26.25  
   26.26  text "distributive laws of & and | "
   26.27 -schematic_lemma "?p : (P & Q) | R  --> (P | R) & (Q | R)"
   26.28 +schematic_goal "?p : (P & Q) | R  --> (P | R) & (Q | R)"
   26.29    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   26.30  
   26.31 -schematic_lemma "?p : (P | R) & (Q | R)  --> (P & Q) | R"
   26.32 +schematic_goal "?p : (P | R) & (Q | R)  --> (P & Q) | R"
   26.33    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   26.34  
   26.35 -schematic_lemma "?p : (P | Q) & R  --> (P & R) | (Q & R)"
   26.36 +schematic_goal "?p : (P | Q) & R  --> (P & R) | (Q & R)"
   26.37    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   26.38  
   26.39  
   26.40 -schematic_lemma "?p : (P & R) | (Q & R)  --> (P | Q) & R"
   26.41 +schematic_goal "?p : (P & R) | (Q & R)  --> (P | Q) & R"
   26.42    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   26.43  
   26.44  
   26.45  text "Laws involving implication"
   26.46  
   26.47 -schematic_lemma "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)"
   26.48 +schematic_goal "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)"
   26.49    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   26.50  
   26.51 -schematic_lemma "?p : (P & Q --> R) <-> (P--> (Q-->R))"
   26.52 +schematic_goal "?p : (P & Q --> R) <-> (P--> (Q-->R))"
   26.53    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   26.54  
   26.55 -schematic_lemma "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
   26.56 +schematic_goal "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
   26.57    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   26.58  
   26.59 -schematic_lemma "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
   26.60 +schematic_goal "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
   26.61    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   26.62  
   26.63 -schematic_lemma "?p : (P --> Q & R) <-> (P-->Q)  &  (P-->R)"
   26.64 +schematic_goal "?p : (P --> Q & R) <-> (P-->Q)  &  (P-->R)"
   26.65    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   26.66  
   26.67  
   26.68  text "Propositions-as-types"
   26.69  
   26.70  (*The combinator K*)
   26.71 -schematic_lemma "?p : P --> (Q --> P)"
   26.72 +schematic_goal "?p : P --> (Q --> P)"
   26.73    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   26.74  
   26.75  (*The combinator S*)
   26.76 -schematic_lemma "?p : (P-->Q-->R)  --> (P-->Q) --> (P-->R)"
   26.77 +schematic_goal "?p : (P-->Q-->R)  --> (P-->Q) --> (P-->R)"
   26.78    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   26.79  
   26.80  
   26.81  (*Converse is classical*)
   26.82 -schematic_lemma "?p : (P-->Q) | (P-->R)  -->  (P --> Q | R)"
   26.83 +schematic_goal "?p : (P-->Q) | (P-->R)  -->  (P --> Q | R)"
   26.84    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   26.85  
   26.86 -schematic_lemma "?p : (P-->Q)  -->  (~Q --> ~P)"
   26.87 +schematic_goal "?p : (P-->Q)  -->  (~Q --> ~P)"
   26.88    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   26.89  
   26.90  
   26.91  text "Schwichtenberg's examples (via T. Nipkow)"
   26.92  
   26.93 -schematic_lemma stab_imp: "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
   26.94 +schematic_goal stab_imp: "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
   26.95    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   26.96  
   26.97 -schematic_lemma stab_to_peirce: "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)  
   26.98 +schematic_goal stab_to_peirce: "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)  
   26.99                --> ((P --> Q) --> P) --> P"
  26.100    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
  26.101  
  26.102 -schematic_lemma peirce_imp1: "?p : (((Q --> R) --> Q) --> Q)  
  26.103 +schematic_goal peirce_imp1: "?p : (((Q --> R) --> Q) --> Q)  
  26.104                 --> (((P --> Q) --> R) --> P --> Q) --> P --> Q"
  26.105    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
  26.106    
  26.107 -schematic_lemma peirce_imp2: "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
  26.108 +schematic_goal peirce_imp2: "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
  26.109    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
  26.110  
  26.111 -schematic_lemma mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q"
  26.112 +schematic_goal mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q"
  26.113    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
  26.114  
  26.115 -schematic_lemma mints_solovev: "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
  26.116 +schematic_goal mints_solovev: "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
  26.117    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
  26.118  
  26.119 -schematic_lemma tatsuta: "?p : (((P7 --> P1) --> P10) --> P4 --> P5)  
  26.120 +schematic_goal tatsuta: "?p : (((P7 --> P1) --> P10) --> P4 --> P5)  
  26.121            --> (((P8 --> P2) --> P9) --> P3 --> P10)  
  26.122            --> (P1 --> P8) --> P6 --> P7  
  26.123            --> (((P3 --> P2) --> P9) --> P4)  
  26.124            --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5"
  26.125    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
  26.126  
  26.127 -schematic_lemma tatsuta1: "?p : (((P8 --> P2) --> P9) --> P3 --> P10)  
  26.128 +schematic_goal tatsuta1: "?p : (((P8 --> P2) --> P9) --> P3 --> P10)  
  26.129       --> (((P3 --> P2) --> P9) --> P4)  
  26.130       --> (((P6 --> P1) --> P2) --> P9)  
  26.131       --> (((P7 --> P1) --> P10) --> P4 --> P5)  
    27.1 --- a/src/FOLP/ex/Quantifiers_Cla.thy	Tue Oct 06 13:31:44 2015 +0200
    27.2 +++ b/src/FOLP/ex/Quantifiers_Cla.thy	Tue Oct 06 15:14:28 2015 +0200
    27.3 @@ -10,92 +10,92 @@
    27.4  imports FOLP
    27.5  begin
    27.6  
    27.7 -schematic_lemma "?p : (ALL x y. P(x,y))  -->  (ALL y x. P(x,y))"
    27.8 +schematic_goal "?p : (ALL x y. P(x,y))  -->  (ALL y x. P(x,y))"
    27.9    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   27.10  
   27.11 -schematic_lemma "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))"
   27.12 +schematic_goal "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))"
   27.13    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   27.14  
   27.15  
   27.16  (*Converse is false*)
   27.17 -schematic_lemma "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
   27.18 +schematic_goal "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
   27.19    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   27.20  
   27.21 -schematic_lemma "?p : (ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))"
   27.22 +schematic_goal "?p : (ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))"
   27.23    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   27.24  
   27.25  
   27.26 -schematic_lemma "?p : (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)"
   27.27 +schematic_goal "?p : (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)"
   27.28    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   27.29  
   27.30  
   27.31  text "Some harder ones"
   27.32  
   27.33 -schematic_lemma "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
   27.34 +schematic_goal "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
   27.35    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   27.36  
   27.37  (*Converse is false*)
   27.38 -schematic_lemma "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))"
   27.39 +schematic_goal "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))"
   27.40    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   27.41  
   27.42  
   27.43  text "Basic test of quantifier reasoning"
   27.44  (*TRUE*)
   27.45 -schematic_lemma "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
   27.46 +schematic_goal "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
   27.47    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   27.48  
   27.49 -schematic_lemma "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
   27.50 +schematic_goal "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
   27.51    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   27.52  
   27.53  
   27.54  text "The following should fail, as they are false!"
   27.55  
   27.56 -schematic_lemma "?p : (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))"
   27.57 +schematic_goal "?p : (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))"
   27.58    apply (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)?
   27.59    oops
   27.60  
   27.61 -schematic_lemma "?p : (EX x. Q(x))  -->  (ALL x. Q(x))"
   27.62 +schematic_goal "?p : (EX x. Q(x))  -->  (ALL x. Q(x))"
   27.63    apply (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)?
   27.64    oops
   27.65  
   27.66 -schematic_lemma "?p : P(?a) --> (ALL x. P(x))"
   27.67 +schematic_goal "?p : P(?a) --> (ALL x. P(x))"
   27.68    apply (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)?
   27.69    oops
   27.70  
   27.71 -schematic_lemma "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
   27.72 +schematic_goal "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
   27.73    apply (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)?
   27.74    oops
   27.75  
   27.76  
   27.77  text "Back to things that are provable..."
   27.78  
   27.79 -schematic_lemma "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
   27.80 +schematic_goal "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
   27.81    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   27.82  
   27.83  
   27.84  (*An example of why exI should be delayed as long as possible*)
   27.85 -schematic_lemma "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
   27.86 +schematic_goal "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
   27.87    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   27.88  
   27.89 -schematic_lemma "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
   27.90 +schematic_goal "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
   27.91    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   27.92  
   27.93 -schematic_lemma "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
   27.94 +schematic_goal "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
   27.95    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
   27.96  
   27.97  
   27.98  text "Some slow ones"
   27.99  
  27.100  (*Principia Mathematica *11.53  *)
  27.101 -schematic_lemma "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
  27.102 +schematic_goal "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
  27.103    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
  27.104  
  27.105  (*Principia Mathematica *11.55  *)
  27.106 -schematic_lemma "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
  27.107 +schematic_goal "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
  27.108    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
  27.109  
  27.110  (*Principia Mathematica *11.61  *)
  27.111 -schematic_lemma "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
  27.112 +schematic_goal "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
  27.113    by (tactic \<open>Cla.fast_tac @{context} FOLP_cs 1\<close>)
  27.114  
  27.115  end
    28.1 --- a/src/FOLP/ex/Quantifiers_Int.thy	Tue Oct 06 13:31:44 2015 +0200
    28.2 +++ b/src/FOLP/ex/Quantifiers_Int.thy	Tue Oct 06 15:14:28 2015 +0200
    28.3 @@ -10,92 +10,92 @@
    28.4  imports IFOLP
    28.5  begin
    28.6  
    28.7 -schematic_lemma "?p : (ALL x y. P(x,y))  -->  (ALL y x. P(x,y))"
    28.8 +schematic_goal "?p : (ALL x y. P(x,y))  -->  (ALL y x. P(x,y))"
    28.9    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   28.10  
   28.11 -schematic_lemma "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))"
   28.12 +schematic_goal "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))"
   28.13    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   28.14  
   28.15  
   28.16  (*Converse is false*)
   28.17 -schematic_lemma "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
   28.18 +schematic_goal "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
   28.19    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   28.20  
   28.21 -schematic_lemma "?p : (ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))"
   28.22 +schematic_goal "?p : (ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))"
   28.23    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   28.24  
   28.25  
   28.26 -schematic_lemma "?p : (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)"
   28.27 +schematic_goal "?p : (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)"
   28.28    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   28.29  
   28.30  
   28.31  text "Some harder ones"
   28.32  
   28.33 -schematic_lemma "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
   28.34 +schematic_goal "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
   28.35    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   28.36  
   28.37  (*Converse is false*)
   28.38 -schematic_lemma "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))"
   28.39 +schematic_goal "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))"
   28.40    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   28.41  
   28.42  
   28.43  text "Basic test of quantifier reasoning"
   28.44  (*TRUE*)
   28.45 -schematic_lemma "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
   28.46 +schematic_goal "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
   28.47    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   28.48  
   28.49 -schematic_lemma "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
   28.50 +schematic_goal "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
   28.51    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   28.52  
   28.53  
   28.54  text "The following should fail, as they are false!"
   28.55  
   28.56 -schematic_lemma "?p : (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))"
   28.57 +schematic_goal "?p : (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))"
   28.58    apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
   28.59    oops
   28.60  
   28.61 -schematic_lemma "?p : (EX x. Q(x))  -->  (ALL x. Q(x))"
   28.62 +schematic_goal "?p : (EX x. Q(x))  -->  (ALL x. Q(x))"
   28.63    apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
   28.64    oops
   28.65  
   28.66 -schematic_lemma "?p : P(?a) --> (ALL x. P(x))"
   28.67 +schematic_goal "?p : P(?a) --> (ALL x. P(x))"
   28.68    apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
   28.69    oops
   28.70  
   28.71 -schematic_lemma "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
   28.72 +schematic_goal "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
   28.73    apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
   28.74    oops
   28.75  
   28.76  
   28.77  text "Back to things that are provable..."
   28.78  
   28.79 -schematic_lemma "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
   28.80 +schematic_goal "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
   28.81    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   28.82  
   28.83  
   28.84  (*An example of why exI should be delayed as long as possible*)
   28.85 -schematic_lemma "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
   28.86 +schematic_goal "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
   28.87    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   28.88  
   28.89 -schematic_lemma "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
   28.90 +schematic_goal "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
   28.91    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   28.92  
   28.93 -schematic_lemma "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
   28.94 +schematic_goal "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
   28.95    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
   28.96  
   28.97  
   28.98  text "Some slow ones"
   28.99  
  28.100  (*Principia Mathematica *11.53  *)
  28.101 -schematic_lemma "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
  28.102 +schematic_goal "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
  28.103    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
  28.104  
  28.105  (*Principia Mathematica *11.55  *)
  28.106 -schematic_lemma "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
  28.107 +schematic_goal "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
  28.108    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
  28.109  
  28.110  (*Principia Mathematica *11.61  *)
  28.111 -schematic_lemma "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
  28.112 +schematic_goal "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
  28.113    by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
  28.114  
  28.115  end
    29.1 --- a/src/HOL/Bali/Example.thy	Tue Oct 06 13:31:44 2015 +0200
    29.2 +++ b/src/HOL/Bali/Example.thy	Tue Oct 06 15:14:28 2015 +0200
    29.3 @@ -1078,7 +1078,7 @@
    29.4  
    29.5  subsubsection "well-typedness"
    29.6  
    29.7 -schematic_lemma wt_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
    29.8 +schematic_goal wt_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
    29.9  apply (unfold test_def arr_viewed_from_def)
   29.10  (* ?pTs = [Class Base] *)
   29.11  apply (rule wtIs (* ;; *))
   29.12 @@ -1130,7 +1130,7 @@
   29.13  
   29.14  subsubsection "definite assignment"
   29.15  
   29.16 -schematic_lemma da_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>
   29.17 +schematic_goal da_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>
   29.18                    \<turnstile>{} \<guillemotright>\<langle>test ?pTs\<rangle>\<guillemotright> \<lparr>nrm={VName e},brk=\<lambda> l. UNIV\<rparr>"
   29.19  apply (unfold test_def arr_viewed_from_def)
   29.20  apply (rule da.Comp)
   29.21 @@ -1248,7 +1248,7 @@
   29.22  
   29.23  
   29.24  declare Pair_eq [simp del]
   29.25 -schematic_lemma exec_test: 
   29.26 +schematic_goal exec_test: 
   29.27  "\<lbrakk>the (new_Addr (heap  s1)) = a;  
   29.28    the (new_Addr (heap ?s2)) = b;  
   29.29    the (new_Addr (heap ?s3)) = c\<rbrakk> \<Longrightarrow>  
    30.1 --- a/src/HOL/Eisbach/Tests.thy	Tue Oct 06 13:31:44 2015 +0200
    30.2 +++ b/src/HOL/Eisbach/Tests.thy	Tue Oct 06 15:14:28 2015 +0200
    30.3 @@ -224,7 +224,7 @@
    30.4     by retrofitting. This needs to be done more carefully to avoid smashing
    30.5     legitimate pairs.*)
    30.6  
    30.7 -schematic_lemma "?A x \<Longrightarrow> A x"
    30.8 +schematic_goal "?A x \<Longrightarrow> A x"
    30.9    apply (match conclusion in "H" for H \<Rightarrow> \<open>match conclusion in Y for Y \<Rightarrow> \<open>print_term Y\<close>\<close>)
   30.10    apply assumption
   30.11    done
    31.1 --- a/src/HOL/Groups.thy	Tue Oct 06 13:31:44 2015 +0200
    31.2 +++ b/src/HOL/Groups.thy	Tue Oct 06 15:14:28 2015 +0200
    31.3 @@ -147,13 +147,13 @@
    31.4  
    31.5  declare add.left_commute [algebra_simps, field_simps]
    31.6  
    31.7 -theorems add_ac = add.assoc add.commute add.left_commute
    31.8 +lemmas add_ac = add.assoc add.commute add.left_commute
    31.9  
   31.10  end
   31.11  
   31.12  hide_fact add_commute
   31.13  
   31.14 -theorems add_ac = add.assoc add.commute add.left_commute
   31.15 +lemmas add_ac = add.assoc add.commute add.left_commute
   31.16  
   31.17  class semigroup_mult = times +
   31.18    assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"
   31.19 @@ -175,13 +175,13 @@
   31.20  
   31.21  declare mult.left_commute [algebra_simps, field_simps]
   31.22  
   31.23 -theorems mult_ac = mult.assoc mult.commute mult.left_commute
   31.24 +lemmas mult_ac = mult.assoc mult.commute mult.left_commute
   31.25  
   31.26  end
   31.27  
   31.28  hide_fact mult_commute
   31.29  
   31.30 -theorems mult_ac = mult.assoc mult.commute mult.left_commute
   31.31 +lemmas mult_ac = mult.assoc mult.commute mult.left_commute
   31.32  
   31.33  class monoid_add = zero + semigroup_add +
   31.34    assumes add_0_left: "0 + a = a"
    32.1 --- a/src/HOL/Hahn_Banach/Vector_Space.thy	Tue Oct 06 13:31:44 2015 +0200
    32.2 +++ b/src/HOL/Hahn_Banach/Vector_Space.thy	Tue Oct 06 15:14:28 2015 +0200
    32.3 @@ -75,7 +75,7 @@
    32.4    finally show ?thesis .
    32.5  qed
    32.6  
    32.7 -theorems add_ac = add_assoc add_commute add_left_commute
    32.8 +lemmas add_ac = add_assoc add_commute add_left_commute
    32.9  
   32.10  
   32.11  text \<open>The existence of the zero element of a vector space
    33.1 --- a/src/HOL/IMP/Big_Step.thy	Tue Oct 06 13:31:44 2015 +0200
    33.2 +++ b/src/HOL/IMP/Big_Step.thy	Tue Oct 06 15:14:28 2015 +0200
    33.3 @@ -26,7 +26,7 @@
    33.4  text_raw{*}%endsnip*}
    33.5  
    33.6  text_raw{*\snip{BigStepEx}{1}{2}{% *}
    33.7 -schematic_lemma ex: "(''x'' ::= N 5;; ''y'' ::= V ''x'', s) \<Rightarrow> ?t"
    33.8 +schematic_goal ex: "(''x'' ::= N 5;; ''y'' ::= V ''x'', s) \<Rightarrow> ?t"
    33.9  apply(rule Seq)
   33.10  apply(rule Assign)
   33.11  apply simp
    34.1 --- a/src/HOL/Inductive.thy	Tue Oct 06 13:31:44 2015 +0200
    34.2 +++ b/src/HOL/Inductive.thy	Tue Oct 06 15:14:28 2015 +0200
    34.3 @@ -343,13 +343,13 @@
    34.4  
    34.5  text \<open>Package setup.\<close>
    34.6  
    34.7 -theorems basic_monos =
    34.8 +lemmas basic_monos =
    34.9    subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
   34.10    Collect_mono in_mono vimage_mono
   34.11  
   34.12  ML_file "Tools/inductive.ML"
   34.13  
   34.14 -theorems [mono] =
   34.15 +lemmas [mono] =
   34.16    imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
   34.17    imp_mono not_mono
   34.18    Ball_def Bex_def
    35.1 --- a/src/HOL/Library/Multiset.thy	Tue Oct 06 13:31:44 2015 +0200
    35.2 +++ b/src/HOL/Library/Multiset.thy	Tue Oct 06 15:14:28 2015 +0200
    35.3 @@ -2544,7 +2544,7 @@
    35.4    using rel_mset_imp_rel_mset' rel_mset'_imp_rel_mset by auto
    35.5  
    35.6  text \<open>The main end product for @{const rel_mset}: inductive characterization:\<close>
    35.7 -theorems rel_mset_induct[case_names empty add, induct pred: rel_mset] =
    35.8 +lemmas rel_mset_induct[case_names empty add, induct pred: rel_mset] =
    35.9    rel_mset'.induct[unfolded rel_mset_rel_mset'[symmetric]]
   35.10  
   35.11  
    36.1 --- a/src/HOL/Library/Omega_Words_Fun.thy	Tue Oct 06 13:31:44 2015 +0200
    36.2 +++ b/src/HOL/Library/Omega_Words_Fun.thy	Tue Oct 06 15:14:28 2015 +0200
    36.3 @@ -560,7 +560,7 @@
    36.4    thus ?thesis ..
    36.5  qed
    36.6  
    36.7 -theorems limit_is_suffixE = limit_is_suffix[THEN exE]
    36.8 +lemmas limit_is_suffixE = limit_is_suffix[THEN exE]
    36.9  
   36.10  
   36.11  text \<open>
    37.1 --- a/src/HOL/Library/Prefix_Order.thy	Tue Oct 06 13:31:44 2015 +0200
    37.2 +++ b/src/HOL/Library/Prefix_Order.thy	Tue Oct 06 15:14:28 2015 +0200
    37.3 @@ -25,15 +25,15 @@
    37.4  lemmas strict_prefixE' [elim?] = prefixE' [folded less_list_def]
    37.5  lemmas strict_prefixI [intro?] = prefixI [folded less_list_def]
    37.6  lemmas strict_prefixE [elim?] = prefixE [folded less_list_def]
    37.7 -theorems Nil_prefix [iff] = Nil_prefixeq [folded less_eq_list_def]
    37.8 -theorems prefix_Nil [simp] = prefixeq_Nil [folded less_eq_list_def]
    37.9 +lemmas Nil_prefix [iff] = Nil_prefixeq [folded less_eq_list_def]
   37.10 +lemmas prefix_Nil [simp] = prefixeq_Nil [folded less_eq_list_def]
   37.11  lemmas prefix_snoc [simp] = prefixeq_snoc [folded less_eq_list_def]
   37.12  lemmas Cons_prefix_Cons [simp] = Cons_prefixeq_Cons [folded less_eq_list_def]
   37.13  lemmas same_prefix_prefix [simp] = same_prefixeq_prefixeq [folded less_eq_list_def]
   37.14  lemmas same_prefix_nil [iff] = same_prefixeq_nil [folded less_eq_list_def]
   37.15  lemmas prefix_prefix [simp] = prefixeq_prefixeq [folded less_eq_list_def]
   37.16 -theorems prefix_Cons = prefixeq_Cons [folded less_eq_list_def]
   37.17 -theorems prefix_length_le = prefixeq_length_le [folded less_eq_list_def]
   37.18 +lemmas prefix_Cons = prefixeq_Cons [folded less_eq_list_def]
   37.19 +lemmas prefix_length_le = prefixeq_length_le [folded less_eq_list_def]
   37.20  lemmas strict_prefix_simps [simp, code] = prefix_simps [folded less_list_def]
   37.21  lemmas not_prefix_induct [consumes 1, case_names Nil Neq Eq] =
   37.22    not_prefixeq_induct [folded less_eq_list_def]
    38.1 --- a/src/HOL/Library/Set_Algebras.thy	Tue Oct 06 13:31:44 2015 +0200
    38.2 +++ b/src/HOL/Library/Set_Algebras.thy	Tue Oct 06 15:14:28 2015 +0200
    38.3 @@ -127,7 +127,7 @@
    38.4     apply (auto simp add: ac_simps)
    38.5    done
    38.6  
    38.7 -theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
    38.8 +lemmas set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
    38.9    set_plus_rearrange3 set_plus_rearrange4
   38.10  
   38.11  lemma set_plus_mono [intro!]: "C \<subseteq> D \<Longrightarrow> a +o C \<subseteq> a +o D"
   38.12 @@ -237,7 +237,7 @@
   38.13     apply (auto simp add: ac_simps)
   38.14    done
   38.15  
   38.16 -theorems set_times_rearranges = set_times_rearrange set_times_rearrange2
   38.17 +lemmas set_times_rearranges = set_times_rearrange set_times_rearrange2
   38.18    set_times_rearrange3 set_times_rearrange4
   38.19  
   38.20  lemma set_times_mono [intro]: "C \<subseteq> D \<Longrightarrow> a *o C \<subseteq> a *o D"
   38.21 @@ -303,7 +303,7 @@
   38.22    apply auto
   38.23    done
   38.24  
   38.25 -theorems set_times_plus_distribs =
   38.26 +lemmas set_times_plus_distribs =
   38.27    set_times_plus_distrib
   38.28    set_times_plus_distrib2
   38.29  
    39.1 --- a/src/HOL/MicroJava/J/Example.thy	Tue Oct 06 13:31:44 2015 +0200
    39.2 +++ b/src/HOL/MicroJava/J/Example.thy	Tue Oct 06 15:14:28 2015 +0200
    39.3 @@ -373,7 +373,7 @@
    39.4  done
    39.5  
    39.6  lemmas t = ty_expr_ty_exprs_wt_stmt.intros
    39.7 -schematic_lemma wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile>  
    39.8 +schematic_goal wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile>  
    39.9    Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\<surd>"
   39.10  apply (rule ty_expr_ty_exprs_wt_stmt.intros) -- ";;"
   39.11  apply  (rule t) -- "Expr"
   39.12 @@ -402,7 +402,7 @@
   39.13  lemmas e = NewCI eval_evals_exec.intros
   39.14  declare split_if [split del]
   39.15  declare init_vars_def [simp] c_hupd_def [simp] cast_ok_def [simp]
   39.16 -schematic_lemma exec_test: 
   39.17 +schematic_goal exec_test: 
   39.18  " [|new_Addr (heap (snd s0)) = (a, None)|] ==>  
   39.19    tprg\<turnstile>s0 -test-> ?s"
   39.20  apply (unfold test_def)
    40.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Oct 06 13:31:44 2015 +0200
    40.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Oct 06 15:14:28 2015 +0200
    40.3 @@ -266,27 +266,27 @@
    40.4  
    40.5  subsection {* Schematic Variables *}
    40.6  
    40.7 -schematic_lemma "x = ?x"
    40.8 +schematic_goal "x = ?x"
    40.9  nitpick [expect = none]
   40.10  by auto
   40.11  
   40.12 -schematic_lemma "\<forall>x. x = ?x"
   40.13 +schematic_goal "\<forall>x. x = ?x"
   40.14  nitpick [expect = genuine]
   40.15  oops
   40.16  
   40.17 -schematic_lemma "\<exists>x. x = ?x"
   40.18 +schematic_goal "\<exists>x. x = ?x"
   40.19  nitpick [expect = none]
   40.20  by auto
   40.21  
   40.22 -schematic_lemma "\<exists>x::'a \<Rightarrow> 'b. x = ?x"
   40.23 +schematic_goal "\<exists>x::'a \<Rightarrow> 'b. x = ?x"
   40.24  nitpick [expect = none]
   40.25  by auto
   40.26  
   40.27 -schematic_lemma "\<forall>x. ?x = ?y"
   40.28 +schematic_goal "\<forall>x. ?x = ?y"
   40.29  nitpick [expect = none]
   40.30  by auto
   40.31  
   40.32 -schematic_lemma "\<exists>x. ?x = ?y"
   40.33 +schematic_goal "\<exists>x. ?x = ?y"
   40.34  nitpick [expect = none]
   40.35  by auto
   40.36  
    41.1 --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Tue Oct 06 13:31:44 2015 +0200
    41.2 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Tue Oct 06 15:14:28 2015 +0200
    41.3 @@ -340,12 +340,12 @@
    41.4  
    41.5  subsubsection {* Schematic Variables *}
    41.6  
    41.7 -schematic_lemma "?P"
    41.8 +schematic_goal "?P"
    41.9  nitpick [expect = none]
   41.10  apply auto
   41.11  done
   41.12  
   41.13 -schematic_lemma "x = ?y"
   41.14 +schematic_goal "x = ?y"
   41.15  nitpick [expect = none]
   41.16  apply auto
   41.17  done
    42.1 --- a/src/HOL/Prolog/Func.thy	Tue Oct 06 13:31:44 2015 +0200
    42.2 +++ b/src/HOL/Prolog/Func.thy	Tue Oct 06 15:14:28 2015 +0200
    42.3 @@ -58,11 +58,11 @@
    42.4  
    42.5  lemmas prog_Func = eval
    42.6  
    42.7 -schematic_lemma "eval ((S (S Z)) + (S Z)) ?X"
    42.8 +schematic_goal "eval ((S (S Z)) + (S Z)) ?X"
    42.9    apply (prolog prog_Func)
   42.10    done
   42.11  
   42.12 -schematic_lemma "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z)
   42.13 +schematic_goal "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z)
   42.14                          (n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X"
   42.15    apply (prolog prog_Func)
   42.16    done
    43.1 --- a/src/HOL/Prolog/Test.thy	Tue Oct 06 13:31:44 2015 +0200
    43.2 +++ b/src/HOL/Prolog/Test.thy	Tue Oct 06 15:14:28 2015 +0200
    43.3 @@ -80,7 +80,7 @@
    43.4  
    43.5  lemmas prog_Test = append reverse mappred mapfun age eq bag_appl
    43.6  
    43.7 -schematic_lemma "append ?x ?y [a,b,c,d]"
    43.8 +schematic_goal "append ?x ?y [a,b,c,d]"
    43.9    apply (prolog prog_Test)
   43.10    back
   43.11    back
   43.12 @@ -88,56 +88,56 @@
   43.13    back
   43.14    done
   43.15  
   43.16 -schematic_lemma "append [a,b] y ?L"
   43.17 +schematic_goal "append [a,b] y ?L"
   43.18    apply (prolog prog_Test)
   43.19    done
   43.20  
   43.21 -schematic_lemma "!y. append [a,b] y (?L y)"
   43.22 +schematic_goal "!y. append [a,b] y (?L y)"
   43.23    apply (prolog prog_Test)
   43.24    done
   43.25  
   43.26 -schematic_lemma "reverse [] ?L"
   43.27 +schematic_goal "reverse [] ?L"
   43.28    apply (prolog prog_Test)
   43.29    done
   43.30  
   43.31 -schematic_lemma "reverse [23] ?L"
   43.32 +schematic_goal "reverse [23] ?L"
   43.33    apply (prolog prog_Test)
   43.34    done
   43.35  
   43.36 -schematic_lemma "reverse [23,24,?x] ?L"
   43.37 +schematic_goal "reverse [23,24,?x] ?L"
   43.38    apply (prolog prog_Test)
   43.39    done
   43.40  
   43.41 -schematic_lemma "reverse ?L [23,24,?x]"
   43.42 +schematic_goal "reverse ?L [23,24,?x]"
   43.43    apply (prolog prog_Test)
   43.44    done
   43.45  
   43.46 -schematic_lemma "mappred age ?x [23,24]"
   43.47 +schematic_goal "mappred age ?x [23,24]"
   43.48    apply (prolog prog_Test)
   43.49    back
   43.50    done
   43.51  
   43.52 -schematic_lemma "mappred (%x y. ? z. age z y) ?x [23,24]"
   43.53 +schematic_goal "mappred (%x y. ? z. age z y) ?x [23,24]"
   43.54    apply (prolog prog_Test)
   43.55    done
   43.56  
   43.57 -schematic_lemma "mappred ?P [bob,sue] [24,23]"
   43.58 +schematic_goal "mappred ?P [bob,sue] [24,23]"
   43.59    apply (prolog prog_Test)
   43.60    done
   43.61  
   43.62 -schematic_lemma "mapfun f [bob,bob,sue] [?x,?y,?z]"
   43.63 +schematic_goal "mapfun f [bob,bob,sue] [?x,?y,?z]"
   43.64    apply (prolog prog_Test)
   43.65    done
   43.66  
   43.67 -schematic_lemma "mapfun (%x. h x 25) [bob,sue] ?L"
   43.68 +schematic_goal "mapfun (%x. h x 25) [bob,sue] ?L"
   43.69    apply (prolog prog_Test)
   43.70    done
   43.71  
   43.72 -schematic_lemma "mapfun ?F [24,25] [h bob 24,h bob 25]"
   43.73 +schematic_goal "mapfun ?F [24,25] [h bob 24,h bob 25]"
   43.74    apply (prolog prog_Test)
   43.75    done
   43.76  
   43.77 -schematic_lemma "mapfun ?F [24] [h 24 24]"
   43.78 +schematic_goal "mapfun ?F [24] [h 24 24]"
   43.79    apply (prolog prog_Test)
   43.80    back
   43.81    back
   43.82 @@ -148,12 +148,12 @@
   43.83    apply (prolog prog_Test)
   43.84    done
   43.85  
   43.86 -schematic_lemma "age ?x 24 & age ?y 23"
   43.87 +schematic_goal "age ?x 24 & age ?y 23"
   43.88    apply (prolog prog_Test)
   43.89    back
   43.90    done
   43.91  
   43.92 -schematic_lemma "age ?x 24 | age ?x 23"
   43.93 +schematic_goal "age ?x 24 | age ?x 23"
   43.94    apply (prolog prog_Test)
   43.95    back
   43.96    back
   43.97 @@ -167,7 +167,7 @@
   43.98    apply (prolog prog_Test)
   43.99    done
  43.100  
  43.101 -schematic_lemma "age sue 24 .. age bob 23 => age ?x ?y"
  43.102 +schematic_goal "age sue 24 .. age bob 23 => age ?x ?y"
  43.103    apply (prolog prog_Test)
  43.104    back
  43.105    back
  43.106 @@ -181,7 +181,7 @@
  43.107    done
  43.108  (*reset trace_DEPTH_FIRST;*)
  43.109  
  43.110 -schematic_lemma "(!x. age x 25 :- age x 23) => age ?x 25 & age ?y 25"
  43.111 +schematic_goal "(!x. age x 25 :- age x 23) => age ?x 25 & age ?y 25"
  43.112    apply (prolog prog_Test)
  43.113    back
  43.114    back
  43.115 @@ -192,7 +192,7 @@
  43.116    apply (prolog prog_Test)
  43.117    done
  43.118  
  43.119 -schematic_lemma "? P. P & eq P ?x"
  43.120 +schematic_goal "? P. P & eq P ?x"
  43.121    apply (prolog prog_Test)
  43.122  (*
  43.123    back
  43.124 @@ -247,14 +247,14 @@
  43.125    by fast
  43.126  *)
  43.127  
  43.128 -schematic_lemma "!Emp Stk.(
  43.129 +schematic_goal "!Emp Stk.(
  43.130                         empty    (Emp::'b) .. 
  43.131           (!(X::nat) S. add    X (S::'b)         (Stk X S)) .. 
  43.132           (!(X::nat) S. remove X ((Stk X S)::'b) S))
  43.133   => bag_appl 23 24 ?X ?Y"
  43.134    oops
  43.135  
  43.136 -schematic_lemma "!Qu. ( 
  43.137 +schematic_goal "!Qu. ( 
  43.138            (!L.            empty    (Qu L L)) .. 
  43.139            (!(X::nat) L K. add    X (Qu L (X#K)) (Qu L K)) ..
  43.140            (!(X::nat) L K. remove X (Qu (X#L) K) (Qu L K)))
  43.141 @@ -265,7 +265,7 @@
  43.142    apply (prolog prog_Test)
  43.143    done
  43.144  
  43.145 -schematic_lemma "P x .. P y => P ?X"
  43.146 +schematic_goal "P x .. P y => P ?X"
  43.147    apply (prolog prog_Test)
  43.148    back
  43.149    done
    44.1 --- a/src/HOL/Prolog/Type.thy	Tue Oct 06 13:31:44 2015 +0200
    44.2 +++ b/src/HOL/Prolog/Type.thy	Tue Oct 06 15:14:28 2015 +0200
    44.3 @@ -46,41 +46,41 @@
    44.4  
    44.5  lemmas prog_Type = prog_Func good_typeof common_typeof
    44.6  
    44.7 -schematic_lemma "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T"
    44.8 +schematic_goal "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T"
    44.9    apply (prolog prog_Type)
   44.10    done
   44.11  
   44.12 -schematic_lemma "typeof (fix (%x. x)) ?T"
   44.13 +schematic_goal "typeof (fix (%x. x)) ?T"
   44.14    apply (prolog prog_Type)
   44.15    done
   44.16  
   44.17 -schematic_lemma "typeof (fix (%fact. abs(%n. (app fact (n - Z))))) ?T"
   44.18 +schematic_goal "typeof (fix (%fact. abs(%n. (app fact (n - Z))))) ?T"
   44.19    apply (prolog prog_Type)
   44.20    done
   44.21  
   44.22 -schematic_lemma "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z)
   44.23 +schematic_goal "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z)
   44.24    (n * (app fact (n - (S Z))))))) ?T"
   44.25    apply (prolog prog_Type)
   44.26    done
   44.27  
   44.28 -schematic_lemma "typeof (abs(%v. Z)) ?T" (*correct only solution (?A1 -> nat) *)
   44.29 +schematic_goal "typeof (abs(%v. Z)) ?T" (*correct only solution (?A1 -> nat) *)
   44.30    apply (prolog prog_Type)
   44.31    done
   44.32  
   44.33 -schematic_lemma "typeof (abs(%v. Z)) ?T"
   44.34 +schematic_goal "typeof (abs(%v. Z)) ?T"
   44.35    apply (prolog bad1_typeof common_typeof) (* 1st result ok*)
   44.36    done
   44.37  
   44.38 -schematic_lemma "typeof (abs(%v. Z)) ?T"
   44.39 +schematic_goal "typeof (abs(%v. Z)) ?T"
   44.40    apply (prolog bad1_typeof common_typeof)
   44.41    back (* 2nd result (?A1 -> ?A1) wrong *)
   44.42    done
   44.43  
   44.44 -schematic_lemma "typeof (abs(%v. abs(%v. app v v))) ?T"
   44.45 +schematic_goal "typeof (abs(%v. abs(%v. app v v))) ?T"
   44.46    apply (prolog prog_Type)?  (*correctly fails*)
   44.47    oops
   44.48  
   44.49 -schematic_lemma "typeof (abs(%v. abs(%v. app v v))) ?T"
   44.50 +schematic_goal "typeof (abs(%v. abs(%v. app v v))) ?T"
   44.51    apply (prolog bad2_typeof common_typeof) (* wrong result ((?A3 -> ?B3) -> ?A3 -> ?B3)*)
   44.52    done
   44.53  
    45.1 --- a/src/HOL/Proofs/Lambda/LambdaType.thy	Tue Oct 06 13:31:44 2015 +0200
    45.2 +++ b/src/HOL/Proofs/Lambda/LambdaType.thy	Tue Oct 06 15:14:28 2015 +0200
    45.3 @@ -77,10 +77,10 @@
    45.4  
    45.5  subsection {* Some examples *}
    45.6  
    45.7 -schematic_lemma "e \<turnstile> Abs (Abs (Abs (Var 1 \<degree> (Var 2 \<degree> Var 1 \<degree> Var 0)))) : ?T"
    45.8 +schematic_goal "e \<turnstile> Abs (Abs (Abs (Var 1 \<degree> (Var 2 \<degree> Var 1 \<degree> Var 0)))) : ?T"
    45.9    by force
   45.10  
   45.11 -schematic_lemma "e \<turnstile> Abs (Abs (Abs (Var 2 \<degree> Var 0 \<degree> (Var 1 \<degree> Var 0)))) : ?T"
   45.12 +schematic_goal "e \<turnstile> Abs (Abs (Abs (Var 2 \<degree> Var 0 \<degree> (Var 1 \<degree> Var 0)))) : ?T"
   45.13    by force
   45.14  
   45.15  
    46.1 --- a/src/HOL/Wellfounded.thy	Tue Oct 06 13:31:44 2015 +0200
    46.2 +++ b/src/HOL/Wellfounded.thy	Tue Oct 06 15:14:28 2015 +0200
    46.3 @@ -558,7 +558,7 @@
    46.4    apply fast
    46.5    done
    46.6  
    46.7 -theorems accp_induct_rule = accp_induct [rule_format, induct set: accp]
    46.8 +lemmas accp_induct_rule = accp_induct [rule_format, induct set: accp]
    46.9  
   46.10  theorem accp_downward: "accp r b ==> r a b ==> accp r a"
   46.11    apply (erule accp.cases)
    47.1 --- a/src/HOL/ex/Classical.thy	Tue Oct 06 13:31:44 2015 +0200
    47.2 +++ b/src/HOL/ex/Classical.thy	Tue Oct 06 15:14:28 2015 +0200
    47.3 @@ -348,7 +348,7 @@
    47.4  
    47.5  text{*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
    47.6    fast DISCOVERS who killed Agatha. *}
    47.7 -schematic_lemma "lives(agatha) & lives(butler) & lives(charles) &
    47.8 +schematic_goal "lives(agatha) & lives(butler) & lives(charles) &
    47.9     (killed agatha agatha | killed butler agatha | killed charles agatha) &
   47.10     (\<forall>x y. killed x y --> hates x y & ~richer x y) &
   47.11     (\<forall>x. hates agatha x --> ~hates charles x) &
    48.1 --- a/src/HOL/ex/Groebner_Examples.thy	Tue Oct 06 13:31:44 2015 +0200
    48.2 +++ b/src/HOL/ex/Groebner_Examples.thy	Tue Oct 06 15:14:28 2015 +0200
    48.3 @@ -24,7 +24,7 @@
    48.4      (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv @{context})))) *})
    48.5    by (rule refl)
    48.6  
    48.7 -schematic_lemma
    48.8 +schematic_goal
    48.9    fixes x :: int
   48.10    shows "(x - (-2))^5  * (y - 78) ^ 8 = ?X" 
   48.11    apply (tactic {* ALLGOALS (CONVERSION
    49.1 --- a/src/HOL/ex/Refute_Examples.thy	Tue Oct 06 13:31:44 2015 +0200
    49.2 +++ b/src/HOL/ex/Refute_Examples.thy	Tue Oct 06 15:14:28 2015 +0200
    49.3 @@ -332,11 +332,11 @@
    49.4  
    49.5  subsubsection {* Schematic variables *}
    49.6  
    49.7 -schematic_lemma "?P"
    49.8 +schematic_goal "?P"
    49.9  refute [expect = none]
   49.10  by auto
   49.11  
   49.12 -schematic_lemma "x = ?y"
   49.13 +schematic_goal "x = ?y"
   49.14  refute [expect = none]
   49.15  by auto
   49.16  
    50.1 --- a/src/HOL/ex/Set_Comprehension_Pointfree_Examples.thy	Tue Oct 06 13:31:44 2015 +0200
    50.2 +++ b/src/HOL/ex/Set_Comprehension_Pointfree_Examples.thy	Tue Oct 06 15:14:28 2015 +0200
    50.3 @@ -111,7 +111,7 @@
    50.4  using assms by (auto intro!: finite_vimageI simp add: inj_on_def)
    50.5    (* injectivity to be automated with further rules and automation *)
    50.6  
    50.7 -schematic_lemma (* check interaction with schematics *)
    50.8 +schematic_goal (* check interaction with schematics *)
    50.9    "finite {x :: ?'A \<Rightarrow> ?'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b}
   50.10     = finite ((\<lambda>(b :: ?'B, a:: ?'A). Pair_Rep a b) ` (UNIV \<times> UNIV))"
   50.11    by simp
    51.1 --- a/src/HOL/ex/Set_Theory.thy	Tue Oct 06 13:31:44 2015 +0200
    51.2 +++ b/src/HOL/ex/Set_Theory.thy	Tue Oct 06 15:14:28 2015 +0200
    51.3 @@ -27,7 +27,7 @@
    51.4    Trivial example of term synthesis: apparently hard for some provers!
    51.5  *}
    51.6  
    51.7 -schematic_lemma "a \<noteq> b \<Longrightarrow> a \<in> ?X \<and> b \<notin> ?X"
    51.8 +schematic_goal "a \<noteq> b \<Longrightarrow> a \<in> ?X \<and> b \<notin> ?X"
    51.9    by blast
   51.10  
   51.11  
   51.12 @@ -61,15 +61,15 @@
   51.13    -- {* Requires best-first search because it is undirectional. *}
   51.14    by best
   51.15  
   51.16 -schematic_lemma "\<forall>f:: 'a \<Rightarrow> 'a set. \<forall>x. f x \<noteq> ?S f"
   51.17 +schematic_goal "\<forall>f:: 'a \<Rightarrow> 'a set. \<forall>x. f x \<noteq> ?S f"
   51.18    -- {*This form displays the diagonal term. *}
   51.19    by best
   51.20  
   51.21 -schematic_lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
   51.22 +schematic_goal "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
   51.23    -- {* This form exploits the set constructs. *}
   51.24    by (rule notI, erule rangeE, best)
   51.25  
   51.26 -schematic_lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
   51.27 +schematic_goal "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
   51.28    -- {* Or just this! *}
   51.29    by best
   51.30  
    52.1 --- a/src/HOL/ex/Simproc_Tests.thy	Tue Oct 06 13:31:44 2015 +0200
    52.2 +++ b/src/HOL/ex/Simproc_Tests.thy	Tue Oct 06 15:14:28 2015 +0200
    52.3 @@ -41,7 +41,7 @@
    52.4    }
    52.5  end
    52.6  
    52.7 -schematic_lemma "\<And>(y::?'b::size). size (?x::?'a::size) \<le> size y + size ?x"
    52.8 +schematic_goal "\<And>(y::?'b::size). size (?x::?'a::size) \<le> size y + size ?x"
    52.9    by (tactic {* test @{context} [@{simproc natle_cancel_sums}] *}) (rule le0)
   52.10  (* TODO: test more simprocs with schematic variables *)
   52.11  
    53.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Oct 06 13:31:44 2015 +0200
    53.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Oct 06 15:14:28 2015 +0200
    53.3 @@ -152,15 +152,10 @@
    53.4  
    53.5  (* theorems *)
    53.6  
    53.7 -val theorems =
    53.8 -  Parse_Spec.name_facts -- Parse.for_fixes
    53.9 -    >> (fn (facts, fixes) => #2 oo Specification.theorems_cmd Thm.theoremK facts fixes);
   53.10 -
   53.11  val _ =
   53.12 -  Outer_Syntax.local_theory' @{command_keyword theorems} "define theorems" theorems;
   53.13 -
   53.14 -val _ =
   53.15 -  Outer_Syntax.local_theory' @{command_keyword lemmas} "define lemmas" theorems;
   53.16 +  Outer_Syntax.local_theory' @{command_keyword lemmas} "define theorems"
   53.17 +    (Parse_Spec.name_facts -- Parse.for_fixes >>
   53.18 +      (fn (facts, fixes) => #2 oo Specification.theorems_cmd Thm.theoremK facts fixes));
   53.19  
   53.20  val _ =
   53.21    Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems"
   53.22 @@ -507,9 +502,7 @@
   53.23  val _ = theorem @{command_keyword theorem} false "theorem";
   53.24  val _ = theorem @{command_keyword lemma} false "lemma";
   53.25  val _ = theorem @{command_keyword corollary} false "corollary";
   53.26 -val _ = theorem @{command_keyword schematic_theorem} true "schematic goal";
   53.27 -val _ = theorem @{command_keyword schematic_lemma} true "schematic goal";
   53.28 -val _ = theorem @{command_keyword schematic_corollary} true "schematic goal";
   53.29 +val _ = theorem @{command_keyword schematic_goal} true "schematic goal";
   53.30  
   53.31  
   53.32  val structured_statement =
    54.1 --- a/src/Pure/Pure.thy	Tue Oct 06 13:31:44 2015 +0200
    54.2 +++ b/src/Pure/Pure.thy	Tue Oct 06 15:14:28 2015 +0200
    54.3 @@ -19,7 +19,7 @@
    54.4    and "typedecl" "type_synonym" "nonterminal" "judgment"
    54.5      "consts" "syntax" "no_syntax" "translations" "no_translations" "defs"
    54.6      "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
    54.7 -    "no_notation" "axiomatization" "theorems" "lemmas" "declare"
    54.8 +    "no_notation" "axiomatization" "lemmas" "declare"
    54.9      "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
   54.10    and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML"
   54.11    and "SML_import" "SML_export" :: thy_decl % "ML"
   54.12 @@ -44,7 +44,7 @@
   54.13    and "overloading" :: thy_decl_block
   54.14    and "code_datatype" :: thy_decl
   54.15    and "theorem" "lemma" "corollary" :: thy_goal
   54.16 -  and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_goal
   54.17 +  and "schematic_goal" :: thy_goal
   54.18    and "notepad" :: thy_decl_block
   54.19    and "have" :: prf_goal % "proof"
   54.20    and "hence" :: prf_goal % "proof" == "then have"
    55.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    55.2 +++ b/src/Pure/Tools/update_theorems.scala	Tue Oct 06 15:14:28 2015 +0200
    55.3 @@ -0,0 +1,40 @@
    55.4 +/*  Title:      Pure/Tools/update_theorems.scala
    55.5 +    Author:     Makarius
    55.6 +
    55.7 +Update toplevel theorem keywords.
    55.8 +*/
    55.9 +
   55.10 +package isabelle
   55.11 +
   55.12 +
   55.13 +object Update_Theorems
   55.14 +{
   55.15 +  def update_theorems(path: Path)
   55.16 +  {
   55.17 +    val text0 = File.read(path)
   55.18 +    val text1 =
   55.19 +      (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator)
   55.20 +        yield {
   55.21 +          tok.source match {
   55.22 +            case "theorems" => "lemmas"
   55.23 +            case "schematic_theorem" | "schematic_lemma" | "schematic_corollary" =>
   55.24 +              "schematic_goal"
   55.25 +            case s => s
   55.26 +        } }).mkString
   55.27 +
   55.28 +    if (text0 != text1) {
   55.29 +      Output.writeln("changing " + path)
   55.30 +      File.write_backup2(path, text1)
   55.31 +    }
   55.32 +  }
   55.33 +
   55.34 +
   55.35 +  /* command line entry point */
   55.36 +
   55.37 +  def main(args: Array[String])
   55.38 +  {
   55.39 +    Command_Line.tool0 {
   55.40 +      args.foreach(arg => update_theorems(Path.explode(arg)))
   55.41 +    }
   55.42 +  }
   55.43 +}
    56.1 --- a/src/Pure/build-jars	Tue Oct 06 13:31:44 2015 +0200
    56.2 +++ b/src/Pure/build-jars	Tue Oct 06 15:14:28 2015 +0200
    56.3 @@ -107,6 +107,7 @@
    56.4    Tools/update_header.scala
    56.5    Tools/update_semicolons.scala
    56.6    Tools/update_then.scala
    56.7 +  Tools/update_theorems.scala
    56.8    library.scala
    56.9    term.scala
   56.10    term_xml.scala
    57.1 --- a/src/Sequents/LK/Quantifiers.thy	Tue Oct 06 13:31:44 2015 +0200
    57.2 +++ b/src/Sequents/LK/Quantifiers.thy	Tue Oct 06 15:14:28 2015 +0200
    57.3 @@ -90,13 +90,13 @@
    57.4    oops
    57.5  
    57.6  (*INVALID*)
    57.7 -schematic_lemma "|- P(?a) --> (ALL x. P(x))"
    57.8 +schematic_goal "|- P(?a) --> (ALL x. P(x))"
    57.9    apply fast?
   57.10    apply (rule _)
   57.11    oops
   57.12  
   57.13  (*INVALID*)
   57.14 -schematic_lemma "|- (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
   57.15 +schematic_goal "|- (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
   57.16    apply fast?
   57.17    apply (rule _)
   57.18    oops
   57.19 @@ -114,7 +114,7 @@
   57.20  
   57.21  text "Solving for a Var"
   57.22  
   57.23 -schematic_lemma "|- (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
   57.24 +schematic_goal "|- (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
   57.25    by fast
   57.26  
   57.27  
    58.1 --- a/src/ZF/AC/Cardinal_aux.thy	Tue Oct 06 13:31:44 2015 +0200
    58.2 +++ b/src/ZF/AC/Cardinal_aux.thy	Tue Oct 06 15:14:28 2015 +0200
    58.3 @@ -57,7 +57,7 @@
    58.4    finally show "i \<lesssim> A \<union> B" .
    58.5  qed
    58.6  
    58.7 -schematic_lemma paired_bij: "?f \<in> bij({{y,z}. y \<in> x}, x)"
    58.8 +schematic_goal paired_bij: "?f \<in> bij({{y,z}. y \<in> x}, x)"
    58.9  apply (rule RepFun_bijective)
   58.10  apply (simp add: doubleton_eq_iff, blast)
   58.11  done
    59.1 --- a/src/ZF/Bin.thy	Tue Oct 06 13:31:44 2015 +0200
    59.2 +++ b/src/ZF/Bin.thy	Tue Oct 06 15:14:28 2015 +0200
    59.3 @@ -700,7 +700,7 @@
    59.4  text \<open>@{text combine_numerals_prod} (products of separate literals)\<close>
    59.5  lemma "#5 $* x $* #3 = y" apply simp oops
    59.6  
    59.7 -schematic_lemma "y2 $+ ?x42 = y $+ y2" apply simp oops
    59.8 +schematic_goal "y2 $+ ?x42 = y $+ y2" apply simp oops
    59.9  
   59.10  lemma "oo : int ==> l $+ (l $+ #2) $+ oo = oo" apply simp oops
   59.11  
    60.1 --- a/src/ZF/Constructible/Reflection.thy	Tue Oct 06 13:31:44 2015 +0200
    60.2 +++ b/src/ZF/Constructible/Reflection.thy	Tue Oct 06 15:14:28 2015 +0200
    60.3 @@ -268,7 +268,7 @@
    60.4  text\<open>Example 1: reflecting a simple formula.  The reflecting class is first
    60.5  given as the variable @{text ?Cl} and later retrieved from the final
    60.6  proof state.\<close>
    60.7 -schematic_lemma (in reflection)
    60.8 +schematic_goal (in reflection)
    60.9       "Reflects(?Cl,
   60.10                 \<lambda>x. \<exists>y. M(y) & x \<in> y,
   60.11                 \<lambda>a x. \<exists>y\<in>Mset(a). x \<in> y)"
   60.12 @@ -285,7 +285,7 @@
   60.13  
   60.14  
   60.15  text\<open>Example 2\<close>
   60.16 -schematic_lemma (in reflection)
   60.17 +schematic_goal (in reflection)
   60.18       "Reflects(?Cl,
   60.19                 \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) \<longrightarrow> z \<subseteq> x \<longrightarrow> z \<in> y),
   60.20                 \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x \<longrightarrow> z \<in> y)"
   60.21 @@ -302,14 +302,14 @@
   60.22  by fast
   60.23  
   60.24  text\<open>Example 2''.  We expand the subset relation.\<close>
   60.25 -schematic_lemma (in reflection)
   60.26 +schematic_goal (in reflection)
   60.27    "Reflects(?Cl,
   60.28          \<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),
   60.29          \<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)"
   60.30  by fast
   60.31  
   60.32  text\<open>Example 2'''.  Single-step version, to reveal the reflecting class.\<close>
   60.33 -schematic_lemma (in reflection)
   60.34 +schematic_goal (in reflection)
   60.35       "Reflects(?Cl,
   60.36                 \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) \<longrightarrow> z \<subseteq> x \<longrightarrow> z \<in> y),
   60.37                 \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x \<longrightarrow> z \<in> y)"
   60.38 @@ -329,21 +329,21 @@
   60.39  
   60.40  text\<open>Example 3.  Warning: the following examples make sense only
   60.41  if @{term P} is quantifier-free, since it is not being relativized.\<close>
   60.42 -schematic_lemma (in reflection)
   60.43 +schematic_goal (in reflection)
   60.44       "Reflects(?Cl,
   60.45                 \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) \<longrightarrow> z \<in> y \<longleftrightarrow> z \<in> x & P(z)),
   60.46                 \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<in> y \<longleftrightarrow> z \<in> x & P(z))"
   60.47  by fast
   60.48  
   60.49  text\<open>Example 3'\<close>
   60.50 -schematic_lemma (in reflection)
   60.51 +schematic_goal (in reflection)
   60.52       "Reflects(?Cl,
   60.53                 \<lambda>x. \<exists>y. M(y) & y = Collect(x,P),
   60.54                 \<lambda>a x. \<exists>y\<in>Mset(a). y = Collect(x,P))"
   60.55  by fast
   60.56  
   60.57  text\<open>Example 3''\<close>
   60.58 -schematic_lemma (in reflection)
   60.59 +schematic_goal (in reflection)
   60.60       "Reflects(?Cl,
   60.61                 \<lambda>x. \<exists>y. M(y) & y = Replace(x,P),
   60.62                 \<lambda>a x. \<exists>y\<in>Mset(a). y = Replace(x,P))"
   60.63 @@ -351,7 +351,7 @@
   60.64  
   60.65  text\<open>Example 4: Axiom of Choice.  Possibly wrong, since @{text \<Pi>} needs
   60.66  to be relativized.\<close>
   60.67 -schematic_lemma (in reflection)
   60.68 +schematic_goal (in reflection)
   60.69       "Reflects(?Cl,
   60.70                 \<lambda>A. 0\<notin>A \<longrightarrow> (\<exists>f. M(f) & f \<in> (\<Pi> X \<in> A. X)),
   60.71                 \<lambda>a A. 0\<notin>A \<longrightarrow> (\<exists>f\<in>Mset(a). f \<in> (\<Pi> X \<in> A. X)))"
    61.1 --- a/src/ZF/ex/misc.thy	Tue Oct 06 13:31:44 2015 +0200
    61.2 +++ b/src/ZF/ex/misc.thy	Tue Oct 06 15:14:28 2015 +0200
    61.3 @@ -44,7 +44,7 @@
    61.4  by (blast intro!: equalityI)
    61.5  
    61.6  text\<open>trivial example of term synthesis: apparently hard for some provers!\<close>
    61.7 -schematic_lemma "a \<noteq> b ==> a:?X & b \<notin> ?X"
    61.8 +schematic_goal "a \<noteq> b ==> a:?X & b \<notin> ?X"
    61.9  by blast
   61.10  
   61.11  text\<open>Nice blast benchmark.  Proved in 0.3s; old tactics can't manage it!\<close>