# HG changeset patch
# User paulson
# Date 1103102341 -3600
# Node ID 1d195de594970784c8789003bcdedd90bf98f909
# Parent  18914688a5fd6578f3f580a2f23462c94d70e1d7
removal of HOL_Lemmas

diff -r 18914688a5fd -r 1d195de59497 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Dec 14 14:53:02 2004 +0100
+++ b/src/HOL/HOL.thy	Wed Dec 15 10:19:01 2004 +0100
@@ -7,8 +7,7 @@
 
 theory HOL
 imports CPure
-files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
-      ("antisym_setup.ML")
+files ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("antisym_setup.ML")
 begin
 
 subsection {* Primitive logic *}
@@ -217,11 +216,568 @@
   abs :: "'a::minus => 'a"    ("\<bar>_\<bar>")
 
 
+subsection {*Equality*}
+
+lemma sym: "s=t ==> t=s"
+apply (erule subst)
+apply (rule refl)
+done
+
+(*calling "standard" reduces maxidx to 0*)
+lemmas ssubst = sym [THEN subst, standard]
+
+lemma trans: "[| r=s; s=t |] ==> r=t"
+apply (erule subst , assumption)
+done
+
+lemma def_imp_eq:  assumes meq: "A == B" shows "A = B"
+apply (unfold meq)
+apply (rule refl)
+done
+
+(*Useful with eresolve_tac for proving equalties from known equalities.
+        a = b
+        |   |
+        c = d   *)
+lemma box_equals: "[| a=b;  a=c;  b=d |] ==> c=d"
+apply (rule trans)
+apply (rule trans)
+apply (rule sym)
+apply assumption+
+done
+
+
+subsection {*Congruence rules for application*}
+
+(*similar to AP_THM in Gordon's HOL*)
+lemma fun_cong: "(f::'a=>'b) = g ==> f(x)=g(x)"
+apply (erule subst)
+apply (rule refl)
+done
+
+(*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)
+lemma arg_cong: "x=y ==> f(x)=f(y)"
+apply (erule subst)
+apply (rule refl)
+done
+
+lemma cong: "[| f = g; (x::'a) = y |] ==> f(x) = g(y)"
+apply (erule subst)+
+apply (rule refl)
+done
+
+
+subsection {*Equality of booleans -- iff*}
+
+lemma iffI: assumes prems: "P ==> Q" "Q ==> P" shows "P=Q"
+apply (rules intro: iff [THEN mp, THEN mp] impI prems)
+done
+
+lemma iffD2: "[| P=Q; Q |] ==> P"
+apply (erule ssubst)
+apply assumption
+done
+
+lemma rev_iffD2: "[| Q; P=Q |] ==> P"
+apply (erule iffD2)
+apply assumption
+done
+
+lemmas iffD1 = sym [THEN iffD2, standard]
+lemmas rev_iffD1 = sym [THEN [2] rev_iffD2, standard]
+
+lemma iffE:
+  assumes major: "P=Q"
+      and minor: "[| P --> Q; Q --> P |] ==> R"
+  shows "R"
+by (rules intro: minor impI major [THEN iffD2] major [THEN iffD1])
+
+
+subsection {*True*}
+
+lemma TrueI: "True"
+apply (unfold True_def)
+apply (rule refl)
+done
+
+lemma eqTrueI: "P ==> P=True"
+by (rules intro: iffI TrueI)
+
+lemma eqTrueE: "P=True ==> P"
+apply (erule iffD2)
+apply (rule TrueI)
+done
+
+
+subsection {*Universal quantifier*}
+
+lemma allI: assumes p: "!!x::'a. P(x)" shows "ALL x. P(x)"
+apply (unfold All_def)
+apply (rules intro: ext eqTrueI p)
+done
+
+lemma spec: "ALL x::'a. P(x) ==> P(x)"
+apply (unfold All_def)
+apply (rule eqTrueE)
+apply (erule fun_cong)
+done
+
+lemma allE:
+  assumes major: "ALL x. P(x)"
+      and minor: "P(x) ==> R"
+  shows "R"
+by (rules intro: minor major [THEN spec])
+
+lemma all_dupE:
+  assumes major: "ALL x. P(x)"
+      and minor: "[| P(x); ALL x. P(x) |] ==> R"
+  shows "R"
+by (rules intro: minor major major [THEN spec])
+
+
+subsection {*False*}
+(*Depends upon spec; it is impossible to do propositional logic before quantifiers!*)
+
+lemma FalseE: "False ==> P"
+apply (unfold False_def)
+apply (erule spec)
+done
+
+lemma False_neq_True: "False=True ==> P"
+by (erule eqTrueE [THEN FalseE])
+
+
+subsection {*Negation*}
+
+lemma notI:
+  assumes p: "P ==> False"
+  shows "~P"
+apply (unfold not_def)
+apply (rules intro: impI p)
+done
+
+lemma False_not_True: "False ~= True"
+apply (rule notI)
+apply (erule False_neq_True)
+done
+
+lemma True_not_False: "True ~= False"
+apply (rule notI)
+apply (drule sym)
+apply (erule False_neq_True)
+done
+
+lemma notE: "[| ~P;  P |] ==> R"
+apply (unfold not_def)
+apply (erule mp [THEN FalseE])
+apply assumption
+done
+
+(* Alternative ~ introduction rule: [| P ==> ~ Pa; P ==> Pa |] ==> ~ P *)
+lemmas notI2 = notE [THEN notI, standard]
+
+
+subsection {*Implication*}
+
+lemma impE:
+  assumes "P-->Q" "P" "Q ==> R"
+  shows "R"
+by (rules intro: prems mp)
+
+(* Reduces Q to P-->Q, allowing substitution in P. *)
+lemma rev_mp: "[| P;  P --> Q |] ==> Q"
+by (rules intro: mp)
+
+lemma contrapos_nn:
+  assumes major: "~Q"
+      and minor: "P==>Q"
+  shows "~P"
+by (rules intro: notI minor major [THEN notE])
+
+(*not used at all, but we already have the other 3 combinations *)
+lemma contrapos_pn:
+  assumes major: "Q"
+      and minor: "P ==> ~Q"
+  shows "~P"
+by (rules intro: notI minor major notE)
+
+lemma not_sym: "t ~= s ==> s ~= t"
+apply (erule contrapos_nn)
+apply (erule sym)
+done
+
+(*still used in HOLCF*)
+lemma rev_contrapos:
+  assumes pq: "P ==> Q"
+      and nq: "~Q"
+  shows "~P"
+apply (rule nq [THEN contrapos_nn])
+apply (erule pq)
+done
+
+subsection {*Existential quantifier*}
+
+lemma exI: "P x ==> EX x::'a. P x"
+apply (unfold Ex_def)
+apply (rules intro: allI allE impI mp)
+done
+
+lemma exE:
+  assumes major: "EX x::'a. P(x)"
+      and minor: "!!x. P(x) ==> Q"
+  shows "Q"
+apply (rule major [unfolded Ex_def, THEN spec, THEN mp])
+apply (rules intro: impI [THEN allI] minor)
+done
+
+
+subsection {*Conjunction*}
+
+lemma conjI: "[| P; Q |] ==> P&Q"
+apply (unfold and_def)
+apply (rules intro: impI [THEN allI] mp)
+done
+
+lemma conjunct1: "[| P & Q |] ==> P"
+apply (unfold and_def)
+apply (rules intro: impI dest: spec mp)
+done
+
+lemma conjunct2: "[| P & Q |] ==> Q"
+apply (unfold and_def)
+apply (rules intro: impI dest: spec mp)
+done
+
+lemma conjE:
+  assumes major: "P&Q"
+      and minor: "[| P; Q |] ==> R"
+  shows "R"
+apply (rule minor)
+apply (rule major [THEN conjunct1])
+apply (rule major [THEN conjunct2])
+done
+
+lemma context_conjI:
+  assumes prems: "P" "P ==> Q" shows "P & Q"
+by (rules intro: conjI prems)
+
+
+subsection {*Disjunction*}
+
+lemma disjI1: "P ==> P|Q"
+apply (unfold or_def)
+apply (rules intro: allI impI mp)
+done
+
+lemma disjI2: "Q ==> P|Q"
+apply (unfold or_def)
+apply (rules intro: allI impI mp)
+done
+
+lemma disjE:
+  assumes major: "P|Q"
+      and minorP: "P ==> R"
+      and minorQ: "Q ==> R"
+  shows "R"
+by (rules intro: minorP minorQ impI
+                 major [unfolded or_def, THEN spec, THEN mp, THEN mp])
+
+
+subsection {*Classical logic*}
+
+
+lemma classical:
+  assumes prem: "~P ==> P"
+  shows "P"
+apply (rule True_or_False [THEN disjE, THEN eqTrueE])
+apply assumption
+apply (rule notI [THEN prem, THEN eqTrueI])
+apply (erule subst)
+apply assumption
+done
+
+lemmas ccontr = FalseE [THEN classical, standard]
+
+(*notE with premises exchanged; it discharges ~R so that it can be used to
+  make elimination rules*)
+lemma rev_notE:
+  assumes premp: "P"
+      and premnot: "~R ==> ~P"
+  shows "R"
+apply (rule ccontr)
+apply (erule notE [OF premnot premp])
+done
+
+(*Double negation law*)
+lemma notnotD: "~~P ==> P"
+apply (rule classical)
+apply (erule notE)
+apply assumption
+done
+
+lemma contrapos_pp:
+  assumes p1: "Q"
+      and p2: "~P ==> ~Q"
+  shows "P"
+by (rules intro: classical p1 p2 notE)
+
+
+subsection {*Unique existence*}
+
+lemma ex1I:
+  assumes prems: "P a" "!!x. P(x) ==> x=a"
+  shows "EX! x. P(x)"
+by (unfold Ex1_def, rules intro: prems exI conjI allI impI)
+
+text{*Sometimes easier to use: the premises have no shared variables.  Safe!*}
+lemma ex_ex1I:
+  assumes ex_prem: "EX x. P(x)"
+      and eq: "!!x y. [| P(x); P(y) |] ==> x=y"
+  shows "EX! x. P(x)"
+by (rules intro: ex_prem [THEN exE] ex1I eq)
+
+lemma ex1E:
+  assumes major: "EX! x. P(x)"
+      and minor: "!!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R"
+  shows "R"
+apply (rule major [unfolded Ex1_def, THEN exE])
+apply (erule conjE)
+apply (rules intro: minor)
+done
+
+lemma ex1_implies_ex: "EX! x. P x ==> EX x. P x"
+apply (erule ex1E)
+apply (rule exI)
+apply assumption
+done
+
+
+subsection {*THE: definite description operator*}
+
+lemma the_equality:
+  assumes prema: "P a"
+      and premx: "!!x. P x ==> x=a"
+  shows "(THE x. P x) = a"
+apply (rule trans [OF _ the_eq_trivial])
+apply (rule_tac f = "The" in arg_cong)
+apply (rule ext)
+apply (rule iffI)
+ apply (erule premx)
+apply (erule ssubst, rule prema)
+done
+
+lemma theI:
+  assumes "P a" and "!!x. P x ==> x=a"
+  shows "P (THE x. P x)"
+by (rules intro: prems the_equality [THEN ssubst])
+
+lemma theI': "EX! x. P x ==> P (THE x. P x)"
+apply (erule ex1E)
+apply (erule theI)
+apply (erule allE)
+apply (erule mp)
+apply assumption
+done
+
+(*Easier to apply than theI: only one occurrence of P*)
+lemma theI2:
+  assumes "P a" "!!x. P x ==> x=a" "!!x. P x ==> Q x"
+  shows "Q (THE x. P x)"
+by (rules intro: prems theI)
+
+lemma the1_equality: "[| EX!x. P x; P a |] ==> (THE x. P x) = a"
+apply (rule the_equality)
+apply  assumption
+apply (erule ex1E)
+apply (erule all_dupE)
+apply (drule mp)
+apply  assumption
+apply (erule ssubst)
+apply (erule allE)
+apply (erule mp)
+apply assumption
+done
+
+lemma the_sym_eq_trivial: "(THE y. x=y) = x"
+apply (rule the_equality)
+apply (rule refl)
+apply (erule sym)
+done
+
+
+subsection {*Classical intro rules for disjunction and existential quantifiers*}
+
+lemma disjCI:
+  assumes "~Q ==> P" shows "P|Q"
+apply (rule classical)
+apply (rules intro: prems disjI1 disjI2 notI elim: notE)
+done
+
+lemma excluded_middle: "~P | P"
+by (rules intro: disjCI)
+
+text{*case distinction as a natural deduction rule. Note that @{term "~P"}
+   is the second case, not the first.*}
+lemma case_split_thm:
+  assumes prem1: "P ==> Q"
+      and prem2: "~P ==> Q"
+  shows "Q"
+apply (rule excluded_middle [THEN disjE])
+apply (erule prem2)
+apply (erule prem1)
+done
+
+(*Classical implies (-->) elimination. *)
+lemma impCE:
+  assumes major: "P-->Q"
+      and minor: "~P ==> R" "Q ==> R"
+  shows "R"
+apply (rule excluded_middle [of P, THEN disjE])
+apply (rules intro: minor major [THEN mp])+
+done
+
+(*This version of --> elimination works on Q before P.  It works best for
+  those cases in which P holds "almost everywhere".  Can't install as
+  default: would break old proofs.*)
+lemma impCE':
+  assumes major: "P-->Q"
+      and minor: "Q ==> R" "~P ==> R"
+  shows "R"
+apply (rule excluded_middle [of P, THEN disjE])
+apply (rules intro: minor major [THEN mp])+
+done
+
+(*Classical <-> elimination. *)
+lemma iffCE:
+  assumes major: "P=Q"
+      and minor: "[| P; Q |] ==> R"  "[| ~P; ~Q |] ==> R"
+  shows "R"
+apply (rule major [THEN iffE])
+apply (rules intro: minor elim: impCE notE)
+done
+
+lemma exCI:
+  assumes "ALL x. ~P(x) ==> P(a)"
+  shows "EX x. P(x)"
+apply (rule ccontr)
+apply (rules intro: prems exI allI notI notE [of "\<exists>x. P x"])
+done
+
+
+
 subsection {* Theory and package setup *}
 
-subsubsection {* Basic lemmas *}
+ML
+{*
+val plusI = thm "plusI"
+val minusI = thm "minusI"
+val timesI = thm "timesI"
+val eq_reflection = thm "eq_reflection"
+val refl = thm "refl"
+val subst = thm "subst"
+val ext = thm "ext"
+val impI = thm "impI"
+val mp = thm "mp"
+val True_def = thm "True_def"
+val All_def = thm "All_def"
+val Ex_def = thm "Ex_def"
+val False_def = thm "False_def"
+val not_def = thm "not_def"
+val and_def = thm "and_def"
+val or_def = thm "or_def"
+val Ex1_def = thm "Ex1_def"
+val iff = thm "iff"
+val True_or_False = thm "True_or_False"
+val Let_def = thm "Let_def"
+val if_def = thm "if_def"
+val sym = thm "sym"
+val ssubst = thm "ssubst"
+val trans = thm "trans"
+val def_imp_eq = thm "def_imp_eq"
+val box_equals = thm "box_equals"
+val fun_cong = thm "fun_cong"
+val arg_cong = thm "arg_cong"
+val cong = thm "cong"
+val iffI = thm "iffI"
+val iffD2 = thm "iffD2"
+val rev_iffD2 = thm "rev_iffD2"
+val iffD1 = thm "iffD1"
+val rev_iffD1 = thm "rev_iffD1"
+val iffE = thm "iffE"
+val TrueI = thm "TrueI"
+val eqTrueI = thm "eqTrueI"
+val eqTrueE = thm "eqTrueE"
+val allI = thm "allI"
+val spec = thm "spec"
+val allE = thm "allE"
+val all_dupE = thm "all_dupE"
+val FalseE = thm "FalseE"
+val False_neq_True = thm "False_neq_True"
+val notI = thm "notI"
+val False_not_True = thm "False_not_True"
+val True_not_False = thm "True_not_False"
+val notE = thm "notE"
+val notI2 = thm "notI2"
+val impE = thm "impE"
+val rev_mp = thm "rev_mp"
+val contrapos_nn = thm "contrapos_nn"
+val contrapos_pn = thm "contrapos_pn"
+val not_sym = thm "not_sym"
+val rev_contrapos = thm "rev_contrapos"
+val exI = thm "exI"
+val exE = thm "exE"
+val conjI = thm "conjI"
+val conjunct1 = thm "conjunct1"
+val conjunct2 = thm "conjunct2"
+val conjE = thm "conjE"
+val context_conjI = thm "context_conjI"
+val disjI1 = thm "disjI1"
+val disjI2 = thm "disjI2"
+val disjE = thm "disjE"
+val classical = thm "classical"
+val ccontr = thm "ccontr"
+val rev_notE = thm "rev_notE"
+val notnotD = thm "notnotD"
+val contrapos_pp = thm "contrapos_pp"
+val ex1I = thm "ex1I"
+val ex_ex1I = thm "ex_ex1I"
+val ex1E = thm "ex1E"
+val ex1_implies_ex = thm "ex1_implies_ex"
+val the_equality = thm "the_equality"
+val theI = thm "theI"
+val theI' = thm "theI'"
+val theI2 = thm "theI2"
+val the1_equality = thm "the1_equality"
+val the_sym_eq_trivial = thm "the_sym_eq_trivial"
+val disjCI = thm "disjCI"
+val excluded_middle = thm "excluded_middle"
+val case_split_thm = thm "case_split_thm"
+val impCE = thm "impCE"
+val impCE = thm "impCE"
+val iffCE = thm "iffCE"
+val exCI = thm "exCI"
 
-use "HOL_lemmas.ML"
+(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
+local
+  fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t
+  |   wrong_prem (Bound _) = true
+  |   wrong_prem _ = false
+  val filter_right = filter (fn t => not (wrong_prem (HOLogic.dest_Trueprop (hd (Thm.prems_of t)))))
+in
+  fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp])
+  fun smp_tac j = EVERY'[dresolve_tac (smp j), atac]
+end
+
+
+fun strip_tac i = REPEAT(resolve_tac [impI,allI] i)
+
+(*Obsolete form of disjunctive case analysis*)
+fun excluded_middle_tac sP =
+    res_inst_tac [("Q",sP)] (excluded_middle RS disjE)
+
+fun case_tac a = res_inst_tac [("P",a)] case_split_thm
+*}
+
 theorems case_split = case_split_thm [case_names True False]
 
 
@@ -549,7 +1105,7 @@
 setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
 setup Splitter.setup setup Clasimp.setup
 
-declare disj_absorb [simp] conj_absorb [simp] 
+declare disj_absorb [simp] conj_absorb [simp]
 
 lemma ex1_eq[iff]: "EX! x. x = t" "EX! x. t = x"
 by blast+
@@ -632,14 +1188,14 @@
 ML {*
   structure InductMethod = InductMethodFun
   (struct
-    val dest_concls = HOLogic.dest_concls;
-    val cases_default = thm "case_split";
-    val local_impI = thm "induct_impliesI";
-    val conjI = thm "conjI";
-    val atomize = thms "induct_atomize";
-    val rulify1 = thms "induct_rulify1";
-    val rulify2 = thms "induct_rulify2";
-    val localize = [Thm.symmetric (thm "induct_implies_def")];
+    val dest_concls = HOLogic.dest_concls
+    val cases_default = thm "case_split"
+    val local_impI = thm "induct_impliesI"
+    val conjI = thm "conjI"
+    val atomize = thms "induct_atomize"
+    val rulify1 = thms "induct_rulify1"
+    val rulify2 = thms "induct_rulify2"
+    val localize = [Thm.symmetric (thm "induct_implies_def")]
   end);
 *}
 
@@ -758,7 +1314,7 @@
   apply (erule contrapos_np, simp)
   done
 
-lemma order_eq_iff: "!!x::'a::order. (x = y) = (x \<le> y & y \<le> x)"  
+lemma order_eq_iff: "!!x::'a::order. (x = y) = (x \<le> y & y \<le> x)"
 by (blast intro: order_antisym)
 
 lemma order_antisym_conv: "(y::'a::order) <= x ==> (x <= y) = (x = y)"
@@ -1030,15 +1586,15 @@
 	  case dec t of
 	    None => None
 	  | Some (t1, rel, t2) => Some (t1, "~" ^ rel, t2))
-	| dec (Const ("op =",  _) $ t1 $ t2) = 
+	| dec (Const ("op =",  _) $ t1 $ t2) =
 	    if of_sort t1
 	    then Some (t1, "=", t2)
 	    else None
-	| dec (Const ("op <=",  _) $ t1 $ t2) = 
+	| dec (Const ("op <=",  _) $ t1 $ t2) =
 	    if of_sort t1
 	    then Some (t1, "<=", t2)
 	    else None
-	| dec (Const ("op <",  _) $ t1 $ t2) = 
+	| dec (Const ("op <",  _) $ t1 $ t2) =
 	    if of_sort t1
 	    then Some (t1, "<", t2)
 	    else None
@@ -1100,7 +1656,7 @@
 (*
 method_setup trans_partial =
   {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (Order_Tac.partial_tac)) *}
-  {* transitivity reasoner for partial orders *}	    
+  {* transitivity reasoner for partial orders *}	
 method_setup trans_linear =
   {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (Order_Tac.linear_tac)) *}
   {* transitivity reasoner for linear orders *}
@@ -1168,36 +1724,36 @@
   fun mk v v' q n P =
     if v=v' andalso not(v  mem (map fst (Term.add_frees([],n))))
     then Syntax.const q $ Syntax.mark_bound v' $ n $ P else raise Match;
-  fun all_tr' [Const ("_bound",_) $ Free (v,_), 
-               Const("op -->",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
+  fun all_tr' [Const ("_bound",_) $ Free (v,_),
+               Const("op -->",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
     mk v v' "_lessAll" n P
 
-  | all_tr' [Const ("_bound",_) $ Free (v,_), 
-               Const("op -->",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
+  | all_tr' [Const ("_bound",_) $ Free (v,_),
+               Const("op -->",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
     mk v v' "_leAll" n P
 
-  | all_tr' [Const ("_bound",_) $ Free (v,_), 
-               Const("op -->",_) $ (Const ("op <",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = 
+  | all_tr' [Const ("_bound",_) $ Free (v,_),
+               Const("op -->",_) $ (Const ("op <",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
     mk v v' "_gtAll" n P
 
-  | all_tr' [Const ("_bound",_) $ Free (v,_), 
-               Const("op -->",_) $ (Const ("op <=",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = 
+  | all_tr' [Const ("_bound",_) $ Free (v,_),
+               Const("op -->",_) $ (Const ("op <=",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
     mk v v' "_geAll" n P;
 
-  fun ex_tr' [Const ("_bound",_) $ Free (v,_), 
-               Const("op &",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
+  fun ex_tr' [Const ("_bound",_) $ Free (v,_),
+               Const("op &",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
     mk v v' "_lessEx" n P
 
-  | ex_tr' [Const ("_bound",_) $ Free (v,_), 
-               Const("op &",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
+  | ex_tr' [Const ("_bound",_) $ Free (v,_),
+               Const("op &",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
     mk v v' "_leEx" n P
 
-  | ex_tr' [Const ("_bound",_) $ Free (v,_), 
-               Const("op &",_) $ (Const ("op <",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = 
+  | ex_tr' [Const ("_bound",_) $ Free (v,_),
+               Const("op &",_) $ (Const ("op <",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
     mk v v' "_gtEx" n P
 
-  | ex_tr' [Const ("_bound",_) $ Free (v,_), 
-               Const("op &",_) $ (Const ("op <=",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = 
+  | ex_tr' [Const ("_bound",_) $ Free (v,_),
+               Const("op &",_) $ (Const ("op <=",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
     mk v v' "_geEx" n P
 in
 [("ALL ", all_tr'), ("EX ", ex_tr')]
@@ -1205,3 +1761,4 @@
 *}
 
 end
+
diff -r 18914688a5fd -r 1d195de59497 src/HOL/HOL_lemmas.ML
--- a/src/HOL/HOL_lemmas.ML	Tue Dec 14 14:53:02 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,475 +0,0 @@
-(*  Title:      HOL/HOL_lemmas.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1991  University of Cambridge
-
-Derived rules from Appendix of Mike Gordons HOL Report, Cambridge TR 68.
-*)
-
-(* legacy ML bindings *)
-
-val plusI = thm "plusI";
-val minusI = thm "minusI";
-val timesI = thm "timesI";
-val eq_reflection = thm "eq_reflection";
-val refl = thm "refl";
-val subst = thm "subst";
-val ext = thm "ext";
-val impI = thm "impI";
-val mp = thm "mp";
-val True_def = thm "True_def";
-val All_def = thm "All_def";
-val Ex_def = thm "Ex_def";
-val False_def = thm "False_def";
-val not_def = thm "not_def";
-val and_def = thm "and_def";
-val or_def = thm "or_def";
-val Ex1_def = thm "Ex1_def";
-val iff = thm "iff";
-val True_or_False = thm "True_or_False";
-val Let_def = thm "Let_def";
-val if_def = thm "if_def";
-
-
-section "Equality";
-
-Goal "s=t ==> t=s";
-by (etac subst 1);
-by (rtac refl 1);
-qed "sym";
-
-(*calling "standard" reduces maxidx to 0*)
-bind_thm ("ssubst", sym RS subst);
-
-Goal "[| r=s; s=t |] ==> r=t";
-by (etac subst 1 THEN assume_tac 1);
-qed "trans";
-
-val prems = goal (the_context()) "(A == B) ==> A = B";
-by (rewrite_goals_tac prems);
-by (rtac refl 1);
-qed "def_imp_eq";
-
-(*Useful with eresolve_tac for proving equalties from known equalities.
-        a = b
-        |   |
-        c = d   *)
-Goal "[| a=b;  a=c;  b=d |] ==> c=d";
-by (rtac trans 1);
-by (rtac trans 1);
-by (rtac sym 1);
-by (REPEAT (assume_tac 1)) ;
-qed "box_equals";
-
-
-section "Congruence rules for application";
-
-(*similar to AP_THM in Gordon's HOL*)
-Goal "(f::'a=>'b) = g ==> f(x)=g(x)";
-by (etac subst 1);
-by (rtac refl 1);
-qed "fun_cong";
-
-(*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)
-Goal "x=y ==> f(x)=f(y)";
-by (etac subst 1);
-by (rtac refl 1);
-qed "arg_cong";
-
-Goal "[| f = g; (x::'a) = y |] ==> f(x) = g(y)";
-by (etac subst 1);
-by (etac subst 1);
-by (rtac refl 1);
-qed "cong";
-
-
-section "Equality of booleans -- iff";
-
-val prems = Goal "[| P ==> Q;  Q ==> P |] ==> P=Q";
-by (REPEAT (ares_tac (prems@[impI, iff RS mp RS mp]) 1));
-qed "iffI";
-
-Goal "[| P=Q; Q |] ==> P";
-by (etac ssubst 1);
-by (assume_tac 1);
-qed "iffD2";
-
-Goal "[| Q; P=Q |] ==> P";
-by (etac iffD2 1);
-by (assume_tac 1);
-qed "rev_iffD2";
-
-bind_thm ("iffD1", sym RS iffD2);
-bind_thm ("rev_iffD1", sym RSN (2, rev_iffD2));
-
-val [p1,p2] = Goal "[| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R";
-by (REPEAT (ares_tac [p1 RS iffD2, p1 RS iffD1, p2, impI] 1));
-qed "iffE";
-
-
-section "True";
-
-Goalw [True_def] "True";
-by (rtac refl 1);
-qed "TrueI";
-
-Goal "P ==> P=True";
-by (REPEAT (ares_tac [iffI,TrueI] 1));
-qed "eqTrueI";
-
-Goal "P=True ==> P";
-by (etac iffD2 1);
-by (rtac TrueI 1);
-qed "eqTrueE";
-
-
-section "Universal quantifier";
-
-val prems = Goalw [All_def] "(!!x::'a. P(x)) ==> ALL x. P(x)";
-by (resolve_tac (prems RL [eqTrueI RS ext]) 1);
-qed "allI";
-
-Goalw [All_def] "ALL x::'a. P(x) ==> P(x)";
-by (rtac eqTrueE 1);
-by (etac fun_cong 1);
-qed "spec";
-
-val major::prems = Goal "[| ALL x. P(x);  P(x) ==> R |] ==> R";
-by (REPEAT (resolve_tac (prems @ [major RS spec]) 1)) ;
-qed "allE";
-
-val prems = Goal
-    "[| ALL x. P(x);  [| P(x); ALL x. P(x) |] ==> R |] ==> R";
-by (REPEAT (resolve_tac (prems @ (prems RL [spec])) 1)) ;
-qed "all_dupE";
-
-
-section "False";
-(*Depends upon spec; it is impossible to do propositional logic before quantifiers!*)
-
-Goalw [False_def] "False ==> P";
-by (etac spec 1);
-qed "FalseE";
-
-Goal "False=True ==> P";
-by (etac (eqTrueE RS FalseE) 1);
-qed "False_neq_True";
-
-
-section "Negation";
-
-val prems = Goalw [not_def] "(P ==> False) ==> ~P";
-by (rtac impI 1);
-by (eresolve_tac prems 1);
-qed "notI";
-
-Goal "False ~= True";
-by (rtac notI 1);
-by (etac False_neq_True 1);
-qed "False_not_True";
-
-Goal "True ~= False";
-by (rtac notI 1);
-by (dtac sym 1);
-by (etac False_neq_True 1);
-qed "True_not_False";
-
-Goalw [not_def] "[| ~P;  P |] ==> R";
-by (etac (mp RS FalseE) 1);
-by (assume_tac 1);
-qed "notE";
-
-(* Alternative ~ introduction rule: [| P ==> ~ Pa; P ==> Pa |] ==> ~ P *)
-bind_thm ("notI2", notE RS notI);
-
-
-section "Implication";
-
-val prems = Goal "[| P-->Q;  P;  Q ==> R |] ==> R";
-by (REPEAT (resolve_tac (prems@[mp]) 1));
-qed "impE";
-
-(* Reduces Q to P-->Q, allowing substitution in P. *)
-Goal "[| P;  P --> Q |] ==> Q";
-by (REPEAT (ares_tac [mp] 1)) ;
-qed "rev_mp";
-
-val [major,minor] = Goal "[| ~Q;  P==>Q |] ==> ~P";
-by (rtac (major RS notE RS notI) 1);
-by (etac minor 1) ;
-qed "contrapos_nn";
-
-(*not used at all, but we already have the other 3 combinations *)
-val [major,minor] = Goal "[| Q;  P ==> ~Q |] ==> ~P";
-by (rtac (minor RS notE RS notI) 1);
-by (assume_tac 1);
-by (rtac major 1) ;
-qed "contrapos_pn";
-
-Goal "t ~= s ==> s ~= t";
-by (etac contrapos_nn 1); 
-by (etac sym 1); 
-qed "not_sym";
-
-(*still used in HOLCF*)
-val [major,minor] = Goal "[| P==>Q; ~Q |] ==> ~P";
-by (rtac (minor RS contrapos_nn) 1);
-by (etac major 1) ;
-qed "rev_contrapos";
-
-section "Existential quantifier";
-
-Goalw [Ex_def] "P x ==> EX x::'a. P x";
-by (rtac allI 1); 
-by (rtac impI 1); 
-by (etac allE 1); 
-by (etac mp 1) ;
-by (assume_tac 1); 
-qed "exI";
-
-val [major,minor] =
-Goalw [Ex_def] "[| EX x::'a. P(x); !!x. P(x) ==> Q |] ==> Q";
-by (rtac (major RS spec RS mp) 1); 
-by (rtac (impI RS allI) 1); 
-by (etac minor 1); 
-qed "exE";
-
-
-section "Conjunction";
-
-Goalw [and_def] "[| P; Q |] ==> P&Q";
-by (rtac (impI RS allI) 1);
-by (etac (mp RS mp) 1);
-by (REPEAT (assume_tac 1));
-qed "conjI";
-
-Goalw [and_def] "[| P & Q |] ==> P";
-by (dtac spec 1) ;
-by (etac mp 1);
-by (REPEAT (ares_tac [impI] 1));
-qed "conjunct1";
-
-Goalw [and_def] "[| P & Q |] ==> Q";
-by (dtac spec 1) ;
-by (etac mp 1);
-by (REPEAT (ares_tac [impI] 1));
-qed "conjunct2";
-
-val [major,minor] =
-Goal "[| P&Q;  [| P; Q |] ==> R |] ==> R";
-by (rtac minor 1);
-by (rtac (major RS conjunct1) 1);
-by (rtac (major RS conjunct2) 1);
-qed "conjE";
-
-val prems =
-Goal "[| P; P ==> Q |] ==> P & Q";
-by (REPEAT (resolve_tac (conjI::prems) 1));
-qed "context_conjI";
-
-
-section "Disjunction";
-
-Goalw [or_def] "P ==> P|Q";
-by (REPEAT (resolve_tac [allI,impI] 1));
-by (etac mp 1 THEN assume_tac 1);
-qed "disjI1";
-
-Goalw [or_def] "Q ==> P|Q";
-by (REPEAT (resolve_tac [allI,impI] 1));
-by (etac mp 1 THEN assume_tac 1);
-qed "disjI2";
-
-val [major,minorP,minorQ] =
-Goalw [or_def]  "[| P | Q; P ==> R; Q ==> R |] ==> R";
-by (rtac (major RS spec RS mp RS mp) 1);
-by (DEPTH_SOLVE (ares_tac [impI,minorP,minorQ] 1));
-qed "disjE";
-
-
-section "Classical logic";
-(*CCONTR -- classical logic*)
-
-val [prem] = Goal  "(~P ==> P) ==> P";
-by (rtac (True_or_False RS disjE RS eqTrueE) 1);
-by (assume_tac 1);
-by (rtac (notI RS prem RS eqTrueI) 1);
-by (etac subst 1);
-by (assume_tac 1);
-qed "classical";
-
-bind_thm ("ccontr", FalseE RS classical);
-
-(*notE with premises exchanged; it discharges ~R so that it can be used to
-  make elimination rules*)
-val [premp,premnot] = Goal "[| P; ~R ==> ~P |] ==> R";
-by (rtac ccontr 1);
-by (etac ([premnot,premp] MRS notE) 1);
-qed "rev_notE";
-
-(*Double negation law*)
-Goal "~~P ==> P";
-by (rtac classical 1);
-by (etac notE 1);
-by (assume_tac 1);
-qed "notnotD";
-
-val [p1,p2] = Goal "[| Q; ~ P ==> ~ Q |] ==> P";
-by (rtac classical 1);
-by (dtac p2 1);
-by (etac notE 1);
-by (rtac p1 1);
-qed "contrapos_pp";
-
-
-section "Unique existence";
-
-val prems = Goalw [Ex1_def] "[| P(a);  !!x. P(x) ==> x=a |] ==> EX! x. P(x)";
-by (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1));
-qed "ex1I";
-
-(*Sometimes easier to use: the premises have no shared variables.  Safe!*)
-val [ex_prem,eq] = Goal
-    "[| EX x. P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)";
-by (rtac (ex_prem RS exE) 1);
-by (REPEAT (ares_tac [ex1I,eq] 1)) ;
-qed "ex_ex1I";
-
-val major::prems = Goalw [Ex1_def]
-    "[| EX! x. P(x);  !!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R |] ==> R";
-by (rtac (major RS exE) 1);
-by (REPEAT (etac conjE 1 ORELSE ares_tac prems 1));
-qed "ex1E";
-
-Goal "EX! x. P x ==> EX x. P x";
-by (etac ex1E 1);
-by (rtac exI 1);
-by (assume_tac 1);
-qed "ex1_implies_ex";
-
-
-section "THE: definite description operator";
-
-val [prema,premx] = Goal "[| P a;  !!x. P x ==> x=a |] ==> (THE x. P x) = a";
-by (rtac trans 1); 
- by (rtac (thm "the_eq_trivial") 2);
-by (res_inst_tac [("f","The")] arg_cong 1); 
-by (rtac ext 1); 
- by (rtac iffI 1); 
-by (etac premx 1); 
-by (etac ssubst 1 THEN rtac prema 1);
-qed "the_equality";
-
-val [prema,premx] = Goal "[| P a;  !!x. P x ==> x=a |] ==> P (THE x. P x)";
-by (rtac (the_equality RS ssubst) 1);
-by (REPEAT (ares_tac [prema,premx] 1));
-qed "theI";
-
-Goal "EX! x. P x ==> P (THE x. P x)";
-by (etac ex1E 1);
-by (etac theI 1);
-by (etac allE 1);
-by (etac mp 1);
-by (atac 1);
-qed "theI'";
-
-(*Easier to apply than theI: only one occurrence of P*)
-val [prema,premx,premq] = Goal
-     "[| P a;  !!x. P x ==> x=a;  !!x. P x ==> Q x |] \
-\     ==> Q (THE x. P x)";
-by (rtac premq 1); 
-by (rtac theI 1); 
-by (REPEAT (ares_tac [prema,premx] 1));
-qed "theI2";
-
-Goal "[| EX!x. P x; P a |] ==> (THE x. P x) = a";
-by (rtac the_equality 1);
-by  (atac 1);
-by (etac ex1E 1);
-by (etac all_dupE 1);
-by (dtac mp 1);
-by  (atac 1);
-by (etac ssubst 1);
-by (etac allE 1);
-by (etac mp 1);
-by (atac 1);
-qed "the1_equality";
-
-Goal "(THE y. x=y) = x";
-by (rtac the_equality 1);
-by (rtac refl 1);
-by (etac sym 1);
-qed "the_sym_eq_trivial";
-
-
-section "Classical intro rules for disjunction and existential quantifiers";
-
-val prems = Goal "(~Q ==> P) ==> P|Q";
-by (rtac classical 1);
-by (REPEAT (ares_tac (prems@[disjI1,notI]) 1));
-by (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ;
-qed "disjCI";
-
-Goal "~P | P";
-by (REPEAT (ares_tac [disjCI] 1)) ;
-qed "excluded_middle";
-
-(*For disjunctive case analysis*)
-fun excluded_middle_tac sP =
-    res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
-
-(*Classical implies (-->) elimination. *)
-val major::prems = Goal "[| P-->Q; ~P ==> R; Q ==> R |] ==> R";
-by (rtac (excluded_middle RS disjE) 1);
-by (REPEAT (DEPTH_SOLVE_1 (ares_tac (prems @ [major RS mp]) 1)));
-qed "impCE";
-
-(*This version of --> elimination works on Q before P.  It works best for
-  those cases in which P holds "almost everywhere".  Can't install as
-  default: would break old proofs.*)
-val major::prems = Goal
-    "[| P-->Q;  Q ==> R;  ~P ==> R |] ==> R";
-by (resolve_tac [excluded_middle RS disjE] 1);
-by (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ;
-qed "impCE'";
-
-(*Classical <-> elimination. *)
-val major::prems = Goal
-    "[| P=Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R";
-by (rtac (major RS iffE) 1);
-by (REPEAT (DEPTH_SOLVE_1
-            (eresolve_tac ([asm_rl,impCE,notE]@prems) 1)));
-qed "iffCE";
-
-val prems = Goal "(ALL x. ~P(x) ==> P(a)) ==> EX x. P(x)";
-by (rtac ccontr 1);
-by (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1))  ;
-qed "exCI";
-
-(* case distinction *)
-
-val [prem1,prem2] = Goal "[| P ==> Q; ~P ==> Q |] ==> Q";
-by (rtac (excluded_middle RS disjE) 1);
-by (etac prem2 1);
-by (etac prem1 1);
-qed "case_split_thm";
-
-fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
-
-
-(** Standard abbreviations **)
-
-(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
-local
-  fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t
-  |   wrong_prem (Bound _) = true
-  |   wrong_prem _ = false;
-  val filter_right = filter (fn t => not (wrong_prem (HOLogic.dest_Trueprop (hd (Thm.prems_of t)))));
-in
-  fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
-  fun smp_tac j = EVERY'[dresolve_tac (smp j), atac]
-end;
-
-
-fun strip_tac i = REPEAT(resolve_tac [impI,allI] i);
-
diff -r 18914688a5fd -r 1d195de59497 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Dec 14 14:53:02 2004 +0100
+++ b/src/HOL/IsaMakefile	Wed Dec 15 10:19:01 2004 +0100
@@ -84,7 +84,7 @@
   Datatype.thy Datatype_Universe.thy \
   Divides.thy Equiv_Relations.thy Extraction.thy Finite_Set.ML Finite_Set.thy \
   Fun.thy Gfp.thy Hilbert_Choice.thy HOL.ML \
-  HOL.thy HOL_lemmas.ML Inductive.thy Infinite_Set.thy Integ/Numeral.thy \
+  HOL.thy Inductive.thy Infinite_Set.thy Integ/Numeral.thy \
   Integ/cooper_dec.ML Integ/cooper_proof.ML \
   Integ/IntArith.thy Integ/IntDef.thy \
   Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Parity.thy \