partial restructuring to reduce dependence on Axiom of Choice
authorpaulson
Wed Jul 25 13:13:01 2001 +0200 (2001-07-25)
changeset 114518abfb4f7bd02
parent 11450 1b02a6c4032f
child 11452 f3fbbaeb4fb8
partial restructuring to reduce dependence on Axiom of Choice
src/HOL/Datatype_Universe.thy
src/HOL/Finite.ML
src/HOL/Finite.thy
src/HOL/Fun.ML
src/HOL/Fun.thy
src/HOL/GroupTheory/Bij.thy
src/HOL/GroupTheory/Ring.thy
src/HOL/HOL.ML
src/HOL/HOL.thy
src/HOL/HOL_lemmas.ML
src/HOL/Hilbert_Choice.thy
src/HOL/Integ/Int.thy
src/HOL/Integ/IntDef.thy
src/HOL/IsaMakefile
src/HOL/Nat.thy
src/HOL/NatArith.ML
src/HOL/Ord.thy
src/HOL/Product_Type.thy
src/HOL/Product_Type_lemmas.ML
src/HOL/Relation.ML
src/HOL/Wellfounded_Recursion.ML
src/HOL/Wellfounded_Recursion.thy
src/HOL/Wellfounded_Relations.thy
src/HOL/cladata.ML
src/HOL/ex/Tarski.ML
src/HOL/ex/mesontest.ML
src/HOL/ex/mesontest2.ML
src/HOL/mono.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/Datatype_Universe.thy	Tue Jul 24 11:25:54 2001 +0200
     1.2 +++ b/src/HOL/Datatype_Universe.thy	Wed Jul 25 13:13:01 2001 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  Could <*> be generalized to a general summation (Sigma)?
     1.5  *)
     1.6  
     1.7 -Datatype_Universe = NatArith + Sum_Type +
     1.8 +Datatype_Universe = NatArith + Sum_Type + Hilbert_Choice +
     1.9  
    1.10  
    1.11  (** lists, trees will be sets of nodes **)
    1.12 @@ -86,10 +86,10 @@
    1.13    usum_def   "usum A B == In0`A Un In1`B"
    1.14  
    1.15    (*the corresponding eliminators*)
    1.16 -  Split_def  "Split c M == @u. ? x y. M = Scons x y & u = c x y"
    1.17 +  Split_def  "Split c M == THE u. EX x y. M = Scons x y & u = c x y"
    1.18  
    1.19 -  Case_def   "Case c d M == @u.  (? x . M = In0(x) & u = c(x)) 
    1.20 -                               | (? y . M = In1(y) & u = d(y))"
    1.21 +  Case_def   "Case c d M == THE u.  (EX x . M = In0(x) & u = c(x)) 
    1.22 +                                  | (EX y . M = In1(y) & u = d(y))"
    1.23  
    1.24  
    1.25    (** equality for the "universe" **)
     2.1 --- a/src/HOL/Finite.ML	Tue Jul 24 11:25:54 2001 +0200
     2.2 +++ b/src/HOL/Finite.ML	Wed Jul 25 13:13:01 2001 +0200
     2.3 @@ -333,9 +333,8 @@
     2.4  qed "card_empty";
     2.5  Addsimps [card_empty];
     2.6  
     2.7 -Goal "x ~: A ==> \
     2.8 -\     ((insert x A, n) : cardR) =  \
     2.9 -\     (EX m. (A, m) : cardR & n = Suc m)";
    2.10 +Goal "x ~: A \
    2.11 +\     ==> ((insert x A, n) : cardR)  =  (EX m. (A, m) : cardR & n = Suc m)";
    2.12  by Auto_tac;
    2.13  by (res_inst_tac [("A1", "A")] (finite_imp_cardR RS exE) 1);
    2.14  by (force_tac (claset() addDs [cardR_imp_finite], simpset()) 1);
    2.15 @@ -345,7 +344,7 @@
    2.16  Goalw [card_def]
    2.17       "[| finite A; x ~: A |] ==> card (insert x A) = Suc(card A)";
    2.18  by (asm_simp_tac (simpset() addsimps [lemma]) 1);
    2.19 -by (rtac some_equality 1);
    2.20 +by (rtac the_equality 1);
    2.21  by (auto_tac (claset() addIs [finite_imp_cardR],
    2.22  	      simpset() addcongs [conj_cong]
    2.23  		        addsimps [symmetric card_def,
    2.24 @@ -624,7 +623,7 @@
    2.25  Goalw [fold_def]
    2.26       "[| finite A; x ~: A |] ==> fold f e (insert x A) = f x (fold f e A)";
    2.27  by (asm_simp_tac (simpset() addsimps [lemma]) 1);
    2.28 -by (rtac some_equality 1);
    2.29 +by (rtac the_equality 1);
    2.30  by (auto_tac (claset() addIs [finite_imp_foldSet],
    2.31  	      simpset() addcongs [conj_cong]
    2.32  		        addsimps [symmetric fold_def,
     3.1 --- a/src/HOL/Finite.thy	Tue Jul 24 11:25:54 2001 +0200
     3.2 +++ b/src/HOL/Finite.thy	Wed Jul 25 13:13:01 2001 +0200
     3.3 @@ -37,7 +37,7 @@
     3.4  
     3.5  constdefs
     3.6    card :: 'a set => nat
     3.7 - "card A == @n. (A,n) : cardR"
     3.8 + "card A == THE n. (A,n) : cardR"
     3.9  
    3.10  (*
    3.11  A "fold" functional for finite sets.  For n non-negative we have
    3.12 @@ -56,7 +56,7 @@
    3.13  
    3.14  constdefs
    3.15     fold :: "[['b,'a] => 'a, 'a, 'b set] => 'a"
    3.16 -  "fold f e A == @x. (A,x) : foldSet f e"
    3.17 +  "fold f e A == THE x. (A,x) : foldSet f e"
    3.18  
    3.19     setsum :: "('a => 'b) => 'a set => ('b::{plus, zero})"
    3.20    "setsum f A == if finite A then fold (op+ o f) 0 A else 0"
     4.1 --- a/src/HOL/Fun.ML	Tue Jul 24 11:25:54 2001 +0200
     4.2 +++ b/src/HOL/Fun.ML	Wed Jul 25 13:13:01 2001 +0200
     4.3 @@ -19,15 +19,6 @@
     4.4  qed "apply_inverse";
     4.5  
     4.6  
     4.7 -(** "Axiom" of Choice, proved using the description operator **)
     4.8 -
     4.9 -(*"choice" is now proved in Tools/meson.ML*)
    4.10 -
    4.11 -Goal "!!S. ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)";
    4.12 -by (fast_tac (claset() addEs [someI]) 1);
    4.13 -qed "bchoice";
    4.14 -
    4.15 -
    4.16  section "id";
    4.17  
    4.18  Goalw [id_def] "id x = x";
    4.19 @@ -35,11 +26,6 @@
    4.20  qed "id_apply";
    4.21  Addsimps [id_apply];
    4.22  
    4.23 -Goal "inv id = id";
    4.24 -by (simp_tac (simpset() addsimps [inv_def,id_def]) 1);
    4.25 -qed "inv_id";
    4.26 -Addsimps [inv_id];
    4.27 -
    4.28  
    4.29  section "o";
    4.30  
    4.31 @@ -113,28 +99,6 @@
    4.32  by (assume_tac 1);
    4.33  qed "inj_eq";
    4.34  
    4.35 -(*A one-to-one function has an inverse (given using select).*)
    4.36 -Goalw [inv_def] "inj(f) ==> inv f (f x) = x";
    4.37 -by (asm_simp_tac (simpset() addsimps [inj_eq]) 1); 
    4.38 -qed "inv_f_f";
    4.39 -Addsimps [inv_f_f];
    4.40 -
    4.41 -Goal "[| inj(f);  f x = y |] ==> inv f y = x";
    4.42 -by (etac subst 1);
    4.43 -by (etac inv_f_f 1);
    4.44 -qed "inv_f_eq";
    4.45 -
    4.46 -Goal "[| inj f; ALL x. f(g x) = x |] ==> inv f = g";
    4.47 -by (blast_tac (claset() addIs [ext, inv_f_eq]) 1); 
    4.48 -qed "inj_imp_inv_eq";
    4.49 -
    4.50 -(* Useful??? *)
    4.51 -val [oneone,minor] = Goal
    4.52 -    "[| inj(f); !!y. y: range(f) ==> P(inv f y) |] ==> P(x)";
    4.53 -by (res_inst_tac [("t", "x")] (oneone RS (inv_f_f RS subst)) 1);
    4.54 -by (rtac (rangeI RS minor) 1);
    4.55 -qed "inj_transfer";
    4.56 -
    4.57  Goalw [o_def] "[| inj f; f o g = f o h |] ==> g = h";
    4.58  by (rtac ext 1);
    4.59  by (etac injD 1);
    4.60 @@ -157,11 +121,6 @@
    4.61  qed "inj_on_inverseI";
    4.62  bind_thm ("inj_inverseI", inj_on_inverseI);   (*for compatibility*)
    4.63  
    4.64 -Goal "(inj f) = (inv f o f = id)";
    4.65 -by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1);
    4.66 -by (blast_tac (claset() addIs [inj_inverseI, inv_f_f]) 1);
    4.67 -qed "inj_iff";
    4.68 -
    4.69  Goalw [inj_on_def] "[| inj_on f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
    4.70  by (Blast_tac 1);
    4.71  qed "inj_onD";
    4.72 @@ -170,6 +129,10 @@
    4.73  by (blast_tac (claset() addSDs [inj_onD]) 1);
    4.74  qed "inj_on_iff";
    4.75  
    4.76 +Goalw [o_def] "[| inj_on f A;  inj_on g (f`A) |] ==> inj_on (g o f) A";
    4.77 +by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1);
    4.78 +qed "comp_inj_on";
    4.79 +
    4.80  Goalw [inj_on_def] "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
    4.81  by (Blast_tac 1);
    4.82  qed "inj_on_contraD";
    4.83 @@ -198,49 +161,6 @@
    4.84  by (Blast_tac 1);
    4.85  qed "surjD";
    4.86  
    4.87 -Goal "inj f ==> surj (inv f)";
    4.88 -by (blast_tac (claset() addIs [surjI, inv_f_f]) 1);
    4.89 -qed "inj_imp_surj_inv";
    4.90 -
    4.91 -
    4.92 -(*** Lemmas about injective functions and inv ***)
    4.93 -
    4.94 -Goalw [o_def] "[| inj_on f A;  inj_on g (f`A) |] ==> inj_on (g o f) A";
    4.95 -by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1);
    4.96 -qed "comp_inj_on";
    4.97 -
    4.98 -Goalw [inv_def] "y : range(f) ==> f(inv f y) = y";
    4.99 -by (fast_tac (claset() addIs [someI]) 1);
   4.100 -qed "f_inv_f";
   4.101 -
   4.102 -Goal "surj f ==> f(inv f y) = y";
   4.103 -by (asm_simp_tac (simpset() addsimps [f_inv_f, surj_range]) 1);
   4.104 -qed "surj_f_inv_f";
   4.105 -
   4.106 -Goal "[| inv f x = inv f y;  x: range(f);  y: range(f) |] ==> x=y";
   4.107 -by (rtac (arg_cong RS box_equals) 1);
   4.108 -by (REPEAT (ares_tac [f_inv_f] 1));
   4.109 -qed "inv_injective";
   4.110 -
   4.111 -Goal "A <= range(f) ==> inj_on (inv f) A";
   4.112 -by (fast_tac (claset() addIs [inj_onI] 
   4.113 -                       addEs [inv_injective, injD]) 1);
   4.114 -qed "inj_on_inv";
   4.115 -
   4.116 -Goal "surj f ==> inj (inv f)";
   4.117 -by (asm_simp_tac (simpset() addsimps [inj_on_inv, surj_range]) 1);
   4.118 -qed "surj_imp_inj_inv";
   4.119 -
   4.120 -Goal "(surj f) = (f o inv f = id)";
   4.121 -by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1);
   4.122 -by (blast_tac (claset() addIs [surjI, surj_f_inv_f]) 1);
   4.123 -qed "surj_iff";
   4.124 -
   4.125 -Goal "[| surj f; ALL x. g(f x) = x |] ==> inv f = g";
   4.126 -by (rtac ext 1);
   4.127 -by (dres_inst_tac [("x","inv f x")] spec 1); 
   4.128 -by (asm_full_simp_tac (simpset() addsimps [surj_f_inv_f]) 1); 
   4.129 -qed "surj_imp_inv_eq";
   4.130  
   4.131  
   4.132  (** Bijections **)
   4.133 @@ -257,33 +177,6 @@
   4.134  by (Blast_tac 1);
   4.135  qed "bij_is_surj";
   4.136  
   4.137 -Goalw [bij_def] "bij f ==> bij (inv f)";
   4.138 -by (asm_simp_tac (simpset() addsimps [inj_imp_surj_inv, surj_imp_inj_inv]) 1);
   4.139 -qed "bij_imp_bij_inv";
   4.140 -
   4.141 -val prems = 
   4.142 -Goalw [inv_def] "[| !! x. g (f x) = x;  !! y. f (g y) = y |] ==> inv f = g";
   4.143 -by (rtac ext 1);
   4.144 -by (auto_tac (claset(), simpset() addsimps prems));
   4.145 -qed "inv_equality";
   4.146 -
   4.147 -Goalw [bij_def] "bij f ==> inv (inv f) = f";
   4.148 -by (rtac inv_equality 1);
   4.149 -by (auto_tac (claset(), simpset() addsimps [surj_f_inv_f]));
   4.150 -qed "inv_inv_eq";
   4.151 -
   4.152 -(** bij(inv f) implies little about f.  Consider f::bool=>bool such that
   4.153 -    f(True)=f(False)=True.  Then it's consistent with axiom someI that
   4.154 -    inv(f) could be any function at all, including the identity function.
   4.155 -    If inv(f)=id then inv(f) is a bijection, but inj(f), surj(f) and
   4.156 -    inv(inv(f))=f all fail.
   4.157 -**)
   4.158 -
   4.159 -Goalw [bij_def] "[| bij f; bij g |] ==> inv (f o g) = inv g o inv f";
   4.160 -by (rtac (inv_equality) 1);
   4.161 -by (auto_tac (claset(), simpset() addsimps [surj_f_inv_f]));
   4.162 -qed "o_inv_distrib";
   4.163 -
   4.164  
   4.165  (** We seem to need both the id-forms and the (%x. x) forms; the latter can
   4.166      arise by rewriting, while id may be used explicitly. **)
   4.167 @@ -323,18 +216,10 @@
   4.168  by (asm_simp_tac (simpset() addsimps [surj_range]) 1);
   4.169  qed "surj_image_vimage_eq";
   4.170  
   4.171 -Goal "surj f ==> f ` (inv f ` A) = A";
   4.172 -by (asm_simp_tac (simpset() addsimps [image_eq_UN, surj_f_inv_f]) 1);
   4.173 -qed "image_surj_f_inv_f";
   4.174 -
   4.175  Goalw [inj_on_def] "inj f ==> f -` (f ` A) = A";
   4.176  by (Blast_tac 1);
   4.177  qed "inj_vimage_image_eq";
   4.178  
   4.179 -Goal "inj f ==> (inv f) ` (f ` A) = A";
   4.180 -by (asm_simp_tac (simpset() addsimps [image_eq_UN]) 1);
   4.181 -qed "image_inv_f_f";
   4.182 -
   4.183  Goalw [surj_def] "surj f ==> f -` B <= A ==> B <= f ` A";
   4.184  by (blast_tac (claset() addIs [sym]) 1);
   4.185  qed "vimage_subsetD";
   4.186 @@ -374,10 +259,6 @@
   4.187  by (Blast_tac 1);
   4.188  qed "image_set_diff";
   4.189  
   4.190 -Goalw [image_def] "inj(f) ==> inv(f)`(f`X) = X";
   4.191 -by Auto_tac;
   4.192 -qed "inv_image_comp";
   4.193 -
   4.194  Goal "inj f ==> (f a : f`A) = (a : A)";
   4.195  by (blast_tac (claset() addDs [injD]) 1);
   4.196  qed "inj_image_mem_iff";
   4.197 @@ -404,22 +285,10 @@
   4.198  (*Compare with image_INT: no use of inj_on, and if f is surjective then
   4.199    it doesn't matter whether A is empty*)
   4.200  Goalw [bij_def] "bij f ==> f ` (INTER A B) = (INT x:A. f ` B x)";
   4.201 -by (force_tac (claset() addSIs [surj_f_inv_f RS sym RS image_eqI], 
   4.202 -	       simpset()) 1);
   4.203 +by (asm_full_simp_tac (simpset() addsimps [inj_on_def, surj_def]) 1);
   4.204 +by (Blast_tac 1);  
   4.205  qed "bij_image_INT";
   4.206  
   4.207 -Goal "bij f ==> f ` Collect P = {y. P (inv f y)}";
   4.208 -by Auto_tac;
   4.209 -by (force_tac (claset(), simpset() addsimps [bij_is_inj]) 1);
   4.210 -by (blast_tac (claset() addIs [bij_is_surj RS surj_f_inv_f RS sym]) 1);
   4.211 -qed "bij_image_Collect_eq";
   4.212 -
   4.213 -Goal "bij f ==> f -` A = inv f ` A";
   4.214 -by Safe_tac;
   4.215 -by (asm_simp_tac (simpset() addsimps [bij_is_surj RS surj_f_inv_f]) 2);
   4.216 -by (blast_tac (claset() addIs [bij_is_inj RS inv_f_f RS sym]) 1);
   4.217 -qed "bij_vimage_eq_inv_image";
   4.218 -
   4.219  Goal "surj f ==> -(f`A) <= f`(-A)";
   4.220  by (auto_tac (claset(), simpset() addsimps [surj_def]));  
   4.221  qed "surj_Compl_image_subset";
   4.222 @@ -504,13 +373,13 @@
   4.223  (*** -> and Pi, by Florian Kammueller and LCP ***)
   4.224  
   4.225  val prems = Goalw [Pi_def]
   4.226 -"[| !!x. x: A ==> f x: B x; !!x. x ~: A  ==> f(x) = (@ y. True)|] \
   4.227 +"[| !!x. x: A ==> f x: B x; !!x. x ~: A  ==> f(x) = arbitrary|] \
   4.228  \    ==> f: Pi A B";
   4.229  by (auto_tac (claset(), simpset() addsimps prems));
   4.230  qed "Pi_I";
   4.231  
   4.232  val prems = Goal 
   4.233 -"[| !!x. x: A ==> f x: B; !!x. x ~: A  ==> f(x) = (@ y. True)|] ==> f: A funcset B";
   4.234 +"[| !!x. x: A ==> f x: B; !!x. x ~: A  ==> f(x) = arbitrary|] ==> f: A funcset B";
   4.235  by (blast_tac (claset() addIs Pi_I::prems) 1);
   4.236  qed "funcsetI";
   4.237  
   4.238 @@ -522,7 +391,7 @@
   4.239  by Auto_tac;
   4.240  qed "funcset_mem";
   4.241  
   4.242 -Goalw [Pi_def] "[|f: Pi A B; x~: A|] ==> f x = (@ y. True)";
   4.243 +Goalw [Pi_def] "[|f: Pi A B; x~: A|] ==> f x = arbitrary";
   4.244  by Auto_tac;
   4.245  qed "apply_arb";
   4.246  
   4.247 @@ -573,7 +442,7 @@
   4.248  by (asm_simp_tac (simpset() addsimps prems) 1);
   4.249  qed "restrictI";
   4.250  
   4.251 -Goal "(lam y: A. f y) x = (if x : A then f x else (@ y. True))";
   4.252 +Goal "(lam y: A. f y) x = (if x : A then f x else arbitrary)";
   4.253  by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
   4.254  qed "restrict_apply";
   4.255  Addsimps [restrict_apply];
   4.256 @@ -590,32 +459,6 @@
   4.257  qed "inj_on_restrict_eq";
   4.258  
   4.259  
   4.260 -(*** Inverse ***)
   4.261 -
   4.262 -Goalw [Inv_def] "f ` A = B ==> (lam x: B. (Inv A f) x) : B funcset A";
   4.263 -by (fast_tac (claset() addIs [restrict_in_funcset, someI2]) 1);
   4.264 -qed "Inv_funcset";
   4.265 -
   4.266 -Goal "[| inj_on f A;  x : A |] ==> Inv A f (f x) = x";
   4.267 -by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);
   4.268 -by (blast_tac (claset() addIs [someI2]) 1); 
   4.269 -qed "Inv_f_f";
   4.270 -
   4.271 -Goal "y : f`A  ==> f (Inv A f y) = y";
   4.272 -by (asm_simp_tac (simpset() addsimps [Inv_def]) 1);
   4.273 -by (fast_tac (claset() addIs [someI2]) 1);
   4.274 -qed "f_Inv_f";
   4.275 -
   4.276 -Goal "[| Inv A f x = Inv A f y;  x : f`A;  y : f`A |] ==> x=y";
   4.277 -by (rtac (arg_cong RS box_equals) 1);
   4.278 -by (REPEAT (ares_tac [f_Inv_f] 1));
   4.279 -qed "Inv_injective";
   4.280 -
   4.281 -Goal "B <= f`A ==> inj_on (Inv A f) B";
   4.282 -by (rtac inj_onI 1);
   4.283 -by (blast_tac (claset() addIs [inj_onI] addDs [Inv_injective, injD]) 1);
   4.284 -qed "inj_on_Inv";
   4.285 -
   4.286  Goal "f : A funcset B ==> compose A (lam y:B. y) f = f";
   4.287  by (rtac ext 1); 
   4.288  by (auto_tac (claset(), simpset() addsimps [compose_def, Pi_def])); 
   4.289 @@ -626,15 +469,6 @@
   4.290  by (auto_tac (claset(), simpset() addsimps [compose_def, Pi_def])); 
   4.291  qed "compose_Id";
   4.292  
   4.293 -Goal "[| inj_on f A;  f ` A = B |] \
   4.294 -\     ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)";
   4.295 -by (asm_simp_tac (simpset() addsimps [compose_def]) 1);
   4.296 -by (rtac restrict_ext 1); 
   4.297 -by Auto_tac; 
   4.298 -by (etac subst 1); 
   4.299 -by (asm_full_simp_tac (simpset() addsimps [Inv_f_f]) 1);
   4.300 -qed "compose_Inv_id";
   4.301 -
   4.302  
   4.303  (*** Pi ***)
   4.304  
   4.305 @@ -646,7 +480,7 @@
   4.306  by (blast_tac (HOL_cs addIs [Pi_eq_empty]) 1);
   4.307  qed "Pi_total1";
   4.308  
   4.309 -Goal "Pi {} B = { %x. @y. True }";
   4.310 +Goal "Pi {} B = { %x. arbitrary }";
   4.311  by (auto_tac (claset() addIs [ext], simpset() addsimps [Pi_def]));
   4.312  qed "Pi_empty";
   4.313  
     5.1 --- a/src/HOL/Fun.thy	Tue Jul 24 11:25:54 2001 +0200
     5.2 +++ b/src/HOL/Fun.thy	Wed Jul 25 13:13:01 2001 +0200
     5.3 @@ -43,9 +43,6 @@
     5.4    o  :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl 55)
     5.5      "f o g == %x. f(g(x))"
     5.6  
     5.7 -  inv :: ('a => 'b) => ('b => 'a)
     5.8 -    "inv(f::'a=>'b) == % y. @x. f(x)=y"
     5.9 -
    5.10    inj_on :: ['a => 'b, 'a set] => bool
    5.11      "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    5.12  
    5.13 @@ -70,17 +67,20 @@
    5.14    
    5.15  constdefs
    5.16    Pi      :: "['a set, 'a => 'b set] => ('a => 'b) set"
    5.17 -    "Pi A B == {f. ! x. if x:A then f(x) : B(x) else f(x) = (@ y. True)}"
    5.18 +    "Pi A B == {f. ! x. if x:A then f(x) : B(x) else f(x) = arbitrary}"
    5.19  
    5.20    restrict :: "['a => 'b, 'a set] => ('a => 'b)"
    5.21 -    "restrict f A == (%x. if x : A then f x else (@ y. True))"
    5.22 +    "restrict f A == (%x. if x : A then f x else arbitrary)"
    5.23  
    5.24  syntax
    5.25 -  "@Pi"  :: "[idt, 'a set, 'b set] => ('a => 'b) set"  ("(3PI _:_./ _)" 10)
    5.26 +  "@Pi"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PI _:_./ _)" 10)
    5.27    funcset :: "['a set, 'b set] => ('a => 'b) set"      (infixr 60) 
    5.28    "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)"  ("(3lam _:_./ _)" 10)
    5.29  
    5.30 -  (*Giving funcset the nice arrow syntax -> clashes with existing theories*)
    5.31 +  (*Giving funcset the arrow syntax (namely ->) clashes with other theories*)
    5.32 +
    5.33 +syntax (symbols)
    5.34 +  "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\\<Pi> _\\<in>_./ _)"   10)
    5.35  
    5.36  translations
    5.37    "PI x:A. B" => "Pi A (%x. B)"
    5.38 @@ -91,8 +91,6 @@
    5.39    compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
    5.40      "compose A g f == lam x : A. g(f x)"
    5.41  
    5.42 -  Inv    :: "['a set, 'a => 'b] => ('b => 'a)"
    5.43 -    "Inv A f == (% x. (@ y. y : A & f y = x))"
    5.44  
    5.45    
    5.46  end
     6.1 --- a/src/HOL/GroupTheory/Bij.thy	Tue Jul 24 11:25:54 2001 +0200
     6.2 +++ b/src/HOL/GroupTheory/Bij.thy	Wed Jul 25 13:13:01 2001 +0200
     6.3 @@ -1,4 +1,4 @@
     6.4 -(*  Title:      HOL/GroupTheory/Coset
     6.5 +(*  Title:      HOL/GroupTheory/Bij
     6.6      ID:         $Id$
     6.7      Author:     Florian Kammueller, with new proofs by L C Paulson
     6.8      Copyright   1998-2001  University of Cambridge
     7.1 --- a/src/HOL/GroupTheory/Ring.thy	Tue Jul 24 11:25:54 2001 +0200
     7.2 +++ b/src/HOL/GroupTheory/Ring.thy	Wed Jul 25 13:13:01 2001 +0200
     7.3 @@ -1,4 +1,4 @@
     7.4 -(*  Title:      HOL/GroupTheory/Bij
     7.5 +(*  Title:      HOL/GroupTheory/Ring
     7.6      ID:         $Id$
     7.7      Author:     Florian Kammueller, with new proofs by L C Paulson
     7.8      Copyright   1998-2001  University of Cambridge
     8.1 --- a/src/HOL/HOL.ML	Tue Jul 24 11:25:54 2001 +0200
     8.2 +++ b/src/HOL/HOL.ML	Wed Jul 25 13:13:01 2001 +0200
     8.3 @@ -12,7 +12,6 @@
     8.4    val refl = refl;
     8.5    val subst = subst;
     8.6    val ext = ext;
     8.7 -  val someI = someI;
     8.8    val impI = impI;
     8.9    val mp = mp;
    8.10    val True_def = True_def;
    8.11 @@ -31,6 +30,6 @@
    8.12  end;
    8.13  
    8.14  AddXIs [equal_intr_rule, disjI1, disjI2, ext];
    8.15 -AddXEs [ex1_implies_ex, someI_ex, sym];
    8.16 +AddXEs [ex1_implies_ex, sym];
    8.17  
    8.18  open HOL;
     9.1 --- a/src/HOL/HOL.thy	Tue Jul 24 11:25:54 2001 +0200
     9.2 +++ b/src/HOL/HOL.thy	Wed Jul 25 13:13:01 2001 +0200
     9.3 @@ -7,8 +7,7 @@
     9.4  *)
     9.5  
     9.6  theory HOL = CPure
     9.7 -files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
     9.8 -  ("meson_lemmas.ML") ("Tools/meson.ML"):
     9.9 +files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML"):
    9.10  
    9.11  
    9.12  (** Core syntax **)
    9.13 @@ -37,7 +36,6 @@
    9.14  
    9.15    (* Binders *)
    9.16  
    9.17 -  Eps           :: "('a => bool) => 'a"
    9.18    The           :: "('a => bool) => 'a"
    9.19    All           :: "('a => bool) => bool"           (binder "ALL " 10)
    9.20    Ex            :: "('a => bool) => bool"           (binder "EX " 10)
    9.21 @@ -79,9 +77,9 @@
    9.22    divide        :: "['a::inverse, 'a] => 'a"        (infixl "'/" 70)
    9.23  
    9.24  syntax (xsymbols)
    9.25 -  abs :: "'a::minus => 'a"    ("\<bar>_\<bar>")
    9.26 +  abs :: "'a::minus => 'a"    ("\\<bar>_\\<bar>")
    9.27  syntax (HTML output)
    9.28 -  abs :: "'a::minus => 'a"    ("\<bar>_\<bar>")
    9.29 +  abs :: "'a::minus => 'a"    ("\\<bar>_\\<bar>")
    9.30  
    9.31  axclass plus_ac0 < plus, zero
    9.32    commute: "x + y = y + x"
    9.33 @@ -97,7 +95,6 @@
    9.34  
    9.35  syntax
    9.36    ~=            :: "['a, 'a] => bool"                    (infixl 50)
    9.37 -  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3SOME _./ _)" [0, 10] 10)
    9.38    "_The"        :: "[pttrn, bool] => 'a"                 ("(3THE _./ _)" [0, 10] 10)
    9.39  
    9.40    (* Let expressions *)
    9.41 @@ -116,7 +113,6 @@
    9.42  
    9.43  translations
    9.44    "x ~= y"                == "~ (x = y)"
    9.45 -  "SOME x. P"             == "Eps (%x. P)"
    9.46    "THE x. P"              == "The (%x. P)"
    9.47    "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
    9.48    "let x = a in e"        == "Let a (%x. e)"
    9.49 @@ -126,31 +122,27 @@
    9.50    "op ~="       :: "['a, 'a] => bool"                    ("(_ ~=/ _)" [51, 51] 50)
    9.51  
    9.52  syntax (symbols)
    9.53 -  Not           :: "bool => bool"                        ("\<not> _" [40] 40)
    9.54 -  "op &"        :: "[bool, bool] => bool"                (infixr "\<and>" 35)
    9.55 -  "op |"        :: "[bool, bool] => bool"                (infixr "\<or>" 30)
    9.56 -  "op -->"      :: "[bool, bool] => bool"                (infixr "\<midarrow>\<rightarrow>" 25)
    9.57 -  "op ~="       :: "['a, 'a] => bool"                    (infixl "\<noteq>" 50)
    9.58 -  "ALL "        :: "[idts, bool] => bool"                ("(3\<forall>_./ _)" [0, 10] 10)
    9.59 -  "EX "         :: "[idts, bool] => bool"                ("(3\<exists>_./ _)" [0, 10] 10)
    9.60 -  "EX! "        :: "[idts, bool] => bool"                ("(3\<exists>!_./ _)" [0, 10] 10)
    9.61 -  "_case1"      :: "['a, 'b] => case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
    9.62 +  Not           :: "bool => bool"                        ("\\<not> _" [40] 40)
    9.63 +  "op &"        :: "[bool, bool] => bool"                (infixr "\\<and>" 35)
    9.64 +  "op |"        :: "[bool, bool] => bool"                (infixr "\\<or>" 30)
    9.65 +  "op -->"      :: "[bool, bool] => bool"                (infixr "\\<midarrow>\\<rightarrow>" 25)
    9.66 +  "op ~="       :: "['a, 'a] => bool"                    (infixl "\\<noteq>" 50)
    9.67 +  "ALL "        :: "[idts, bool] => bool"                ("(3\\<forall>_./ _)" [0, 10] 10)
    9.68 +  "EX "         :: "[idts, bool] => bool"                ("(3\\<exists>_./ _)" [0, 10] 10)
    9.69 +  "EX! "        :: "[idts, bool] => bool"                ("(3\\<exists>!_./ _)" [0, 10] 10)
    9.70 +  "_case1"      :: "['a, 'b] => case_syn"                ("(2_ \\<Rightarrow>/ _)" 10)
    9.71  (*"_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ \\<orelse> _")*)
    9.72  
    9.73 -syntax (input)
    9.74 -  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3\<epsilon>_./ _)" [0, 10] 10)
    9.75 -
    9.76  syntax (symbols output)
    9.77 -  "op ~="       :: "['a, 'a] => bool"                    ("(_ \<noteq>/ _)" [51, 51] 50)
    9.78 +  "op ~="       :: "['a, 'a] => bool"                    ("(_ \\<noteq>/ _)" [51, 51] 50)
    9.79  
    9.80  syntax (xsymbols)
    9.81 -  "op -->"      :: "[bool, bool] => bool"                (infixr "\<longrightarrow>" 25)
    9.82 +  "op -->"      :: "[bool, bool] => bool"                (infixr "\\<longrightarrow>" 25)
    9.83  
    9.84  syntax (HTML output)
    9.85 -  Not           :: "bool => bool"                        ("\<not> _" [40] 40)
    9.86 +  Not           :: "bool => bool"                        ("\\<not> _" [40] 40)
    9.87  
    9.88  syntax (HOL)
    9.89 -  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3@ _./ _)" [0, 10] 10)
    9.90    "ALL "        :: "[idts, bool] => bool"                ("(3! _./ _)" [0, 10] 10)
    9.91    "EX "         :: "[idts, bool] => bool"                ("(3? _./ _)" [0, 10] 10)
    9.92    "EX! "        :: "[idts, bool] => bool"                ("(3?! _./ _)" [0, 10] 10)
    9.93 @@ -173,7 +165,6 @@
    9.94      rule, and similar to the ABS rule of HOL.*)
    9.95    ext:          "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
    9.96  
    9.97 -  someI:        "P (x::'a) ==> P (SOME x. P x)"
    9.98    the_eq_trivial: "(THE x. x = a) = (a::'a)"
    9.99  
   9.100    impI:         "(P ==> Q) ==> P-->Q"
   9.101 @@ -183,7 +174,7 @@
   9.102  
   9.103    True_def:     "True      == ((%x::bool. x) = (%x. x))"
   9.104    All_def:      "All(P)    == (P = (%x. True))"
   9.105 -  Ex_def:       "Ex(P)     == P (SOME x. P x)"
   9.106 +  Ex_def:       "Ex(P)     == !Q. (!x. P x --> Q) --> Q"
   9.107    False_def:    "False     == (!P. P)"
   9.108    not_def:      "~ P       == P-->False"
   9.109    and_def:      "P & Q     == !R. (P-->Q-->R) --> R"
   9.110 @@ -199,11 +190,11 @@
   9.111  defs
   9.112    (*misc definitions*)
   9.113    Let_def:      "Let s f == f(s)"
   9.114 -  if_def:       "If P x y == SOME z::'a. (P=True --> z=x) & (P=False --> z=y)"
   9.115 +  if_def:       "If P x y == THE z::'a. (P=True --> z=x) & (P=False --> z=y)"
   9.116  
   9.117    (*arbitrary is completely unspecified, but is made to appear as a
   9.118      definition syntactically*)
   9.119 -  arbitrary_def:  "False ==> arbitrary == (SOME x. False)"
   9.120 +  arbitrary_def:  "False ==> arbitrary == (THE x. False)"
   9.121  
   9.122  
   9.123  
   9.124 @@ -256,8 +247,4 @@
   9.125  setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
   9.126  setup Splitter.setup setup Clasimp.setup
   9.127  
   9.128 -use "meson_lemmas.ML"
   9.129 -use "Tools/meson.ML"
   9.130 -setup meson_setup
   9.131 -
   9.132  end
    10.1 --- a/src/HOL/HOL_lemmas.ML	Tue Jul 24 11:25:54 2001 +0200
    10.2 +++ b/src/HOL/HOL_lemmas.ML	Wed Jul 25 13:13:01 2001 +0200
    10.3 @@ -15,7 +15,6 @@
    10.4  val refl = thm "refl";
    10.5  val subst = thm "subst";
    10.6  val ext = thm "ext";
    10.7 -val someI = thm "someI";
    10.8  val impI = thm "impI";
    10.9  val mp = thm "mp";
   10.10  val True_def = thm "True_def";
   10.11 @@ -222,12 +221,18 @@
   10.12  section "Existential quantifier";
   10.13  
   10.14  Goalw [Ex_def] "P x ==> EX x::'a. P x";
   10.15 -by (etac someI 1) ;
   10.16 +by (rtac allI 1); 
   10.17 +by (rtac impI 1); 
   10.18 +by (etac allE 1); 
   10.19 +by (etac mp 1) ;
   10.20 +by (assume_tac 1); 
   10.21  qed "exI";
   10.22  
   10.23  val [major,minor] =
   10.24  Goalw [Ex_def] "[| EX x::'a. P(x); !!x. P(x) ==> Q |] ==> Q";
   10.25 -by (rtac (major RS minor) 1);
   10.26 +by (rtac (major RS spec RS mp) 1); 
   10.27 +by (rtac (impI RS allI) 1); 
   10.28 +by (etac minor 1); 
   10.29  qed "exE";
   10.30  
   10.31  
   10.32 @@ -344,66 +349,6 @@
   10.33  qed "ex1_implies_ex";
   10.34  
   10.35  
   10.36 -section "SOME: Hilbert's Epsilon-operator";
   10.37 -
   10.38 -(*Easier to apply than someI if witness ?a comes from an EX-formula*)
   10.39 -Goal "EX x. P x ==> P (SOME x. P x)";
   10.40 -by (etac exE 1);
   10.41 -by (etac someI 1);
   10.42 -qed "someI_ex";
   10.43 -
   10.44 -(*Easier to apply than someI: conclusion has only one occurrence of P*)
   10.45 -val prems = Goal "[| P a;  !!x. P x ==> Q x |] ==> Q (SOME x. P x)";
   10.46 -by (resolve_tac prems 1);
   10.47 -by (rtac someI 1);
   10.48 -by (resolve_tac prems 1) ;
   10.49 -qed "someI2";
   10.50 -
   10.51 -(*Easier to apply than someI2 if witness ?a comes from an EX-formula*)
   10.52 -val [major,minor] = Goal "[| EX a. P a; !!x. P x ==> Q x |] ==> Q (SOME x. P x)";
   10.53 -by (rtac (major RS exE) 1);
   10.54 -by (etac someI2 1 THEN etac minor 1);
   10.55 -qed "someI2_ex";
   10.56 -
   10.57 -val prems = Goal "[| P a;  !!x. P x ==> x=a |] ==> (SOME x. P x) = a";
   10.58 -by (rtac someI2 1);
   10.59 -by (REPEAT (ares_tac prems 1)) ;
   10.60 -qed "some_equality";
   10.61 -
   10.62 -Goal "[| EX!x. P x; P a |] ==> (SOME x. P x) = a";
   10.63 -by (rtac some_equality 1);
   10.64 -by  (atac 1);
   10.65 -by (etac ex1E 1);
   10.66 -by (etac all_dupE 1);
   10.67 -by (dtac mp 1);
   10.68 -by  (atac 1);
   10.69 -by (etac ssubst 1);
   10.70 -by (etac allE 1);
   10.71 -by (etac mp 1);
   10.72 -by (atac 1);
   10.73 -qed "some1_equality";
   10.74 -
   10.75 -Goal "P (SOME x. P x) =  (EX x. P x)";
   10.76 -by (rtac iffI 1);
   10.77 -by (etac exI 1);
   10.78 -by (etac exE 1);
   10.79 -by (etac someI 1);
   10.80 -qed "some_eq_ex";
   10.81 -
   10.82 -Goal "(SOME y. y=x) = x";
   10.83 -by (rtac some_equality 1);
   10.84 -by (rtac refl 1);
   10.85 -by (atac 1);
   10.86 -qed "some_eq_trivial";
   10.87 -
   10.88 -Goal "(SOME y. x=y) = x";
   10.89 -by (rtac some_equality 1);
   10.90 -by (rtac refl 1);
   10.91 -by (etac sym 1);
   10.92 -qed "some_sym_eq_trivial";
   10.93 -
   10.94 -
   10.95 -
   10.96  section "THE: definite description operator";
   10.97  
   10.98  val [prema,premx] = Goal "[| P a;  !!x. P x ==> x=a |] ==> (THE x. P x) = a";
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Hilbert_Choice.thy	Wed Jul 25 13:13:01 2001 +0200
    11.3 @@ -0,0 +1,187 @@
    11.4 +(*  Title:      HOL/Hilbert_Choice.thy
    11.5 +    ID:         $Id$
    11.6 +    Author:     Lawrence C Paulson
    11.7 +    Copyright   2001  University of Cambridge
    11.8 +
    11.9 +Hilbert's epsilon-operator and everything to do with the Axiom of Choice
   11.10 +*)
   11.11 +
   11.12 +theory Hilbert_Choice = NatArith
   11.13 +files ("Hilbert_Choice_lemmas.ML") ("meson_lemmas.ML") ("Tools/meson.ML"):
   11.14 +
   11.15 +consts
   11.16 +  Eps           :: "('a => bool) => 'a"
   11.17 +
   11.18 +
   11.19 +syntax (input)
   11.20 +  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3\\<epsilon>_./ _)" [0, 10] 10)
   11.21 +
   11.22 +syntax (HOL)
   11.23 +  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3@ _./ _)" [0, 10] 10)
   11.24 +
   11.25 +syntax
   11.26 +  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3SOME _./ _)" [0, 10] 10)
   11.27 +
   11.28 +translations
   11.29 +  "SOME x. P"             == "Eps (%x. P)"
   11.30 +
   11.31 +axioms  
   11.32 +  someI:        "P (x::'a) ==> P (SOME x. P x)"
   11.33 +
   11.34 +
   11.35 +constdefs  
   11.36 +  inv :: "('a => 'b) => ('b => 'a)"
   11.37 +    "inv(f::'a=>'b) == % y. @x. f(x)=y"
   11.38 +
   11.39 +  Inv :: "['a set, 'a => 'b] => ('b => 'a)"
   11.40 +    "Inv A f == (% x. (@ y. y : A & f y = x))"
   11.41 +
   11.42 +
   11.43 +use "Hilbert_Choice_lemmas.ML"
   11.44 +
   11.45 +
   11.46 +(** Least value operator **)
   11.47 +
   11.48 +constdefs
   11.49 +  LeastM   :: "['a => 'b::ord, 'a => bool] => 'a"
   11.50 +              "LeastM m P == @x. P x & (ALL y. P y --> m x <= m y)"
   11.51 +
   11.52 +syntax
   11.53 + "@LeastM" :: "[pttrn, 'a=>'b::ord, bool] => 'a" ("LEAST _ WRT _. _" [0,4,10]10)
   11.54 +
   11.55 +translations
   11.56 +                "LEAST x WRT m. P" == "LeastM m (%x. P)"
   11.57 +
   11.58 +lemma LeastMI2:
   11.59 +  "[| P x; !!y. P y ==> m x <= m y;
   11.60 +           !!x. [| P x; \\<forall>y. P y --> m x \\<le> m y |] ==> Q x |]
   11.61 +   ==> Q (LeastM m P)";
   11.62 +apply (unfold LeastM_def)
   11.63 +apply (rule someI2_ex)
   11.64 +apply  blast
   11.65 +apply blast
   11.66 +done
   11.67 +
   11.68 +lemma LeastM_equality:
   11.69 + "[| P k; !!x. P x ==> m k <= m x |] ==> m (LEAST x WRT m. P x) = 
   11.70 +     (m k::'a::order)";
   11.71 +apply (rule LeastMI2)
   11.72 +apply   assumption
   11.73 +apply  blast
   11.74 +apply (blast intro!: order_antisym) 
   11.75 +done
   11.76 +
   11.77 +
   11.78 +(** Greatest value operator **)
   11.79 +
   11.80 +constdefs
   11.81 +  GreatestM   :: "['a => 'b::ord, 'a => bool] => 'a"
   11.82 +              "GreatestM m P == @x. P x & (ALL y. P y --> m y <= m x)"
   11.83 +  
   11.84 +  Greatest    :: "('a::ord => bool) => 'a"         (binder "GREATEST " 10)
   11.85 +              "Greatest     == GreatestM (%x. x)"
   11.86 +
   11.87 +syntax
   11.88 + "@GreatestM" :: "[pttrn, 'a=>'b::ord, bool] => 'a"
   11.89 +                                        ("GREATEST _ WRT _. _" [0,4,10]10)
   11.90 +
   11.91 +translations
   11.92 +              "GREATEST x WRT m. P" == "GreatestM m (%x. P)"
   11.93 +
   11.94 +lemma GreatestMI2:
   11.95 +     "[| P x;
   11.96 +	 !!y. P y ==> m y <= m x;
   11.97 +         !!x. [| P x; \\<forall>y. P y --> m y \\<le> m x |] ==> Q x |]
   11.98 +      ==> Q (GreatestM m P)";
   11.99 +apply (unfold GreatestM_def)
  11.100 +apply (rule someI2_ex)
  11.101 +apply  blast
  11.102 +apply blast
  11.103 +done
  11.104 +
  11.105 +lemma GreatestM_equality:
  11.106 + "[| P k;  !!x. P x ==> m x <= m k |]
  11.107 +  ==> m (GREATEST x WRT m. P x) = (m k::'a::order)";
  11.108 +apply (rule_tac m=m in GreatestMI2)
  11.109 +apply   assumption
  11.110 +apply  blast
  11.111 +apply (blast intro!: order_antisym) 
  11.112 +done
  11.113 +
  11.114 +lemma Greatest_equality:
  11.115 +  "[| P (k::'a::order); !!x. P x ==> x <= k |] ==> (GREATEST x. P x) = k";
  11.116 +apply (unfold Greatest_def)
  11.117 +apply (erule GreatestM_equality)
  11.118 +apply blast
  11.119 +done
  11.120 +
  11.121 +lemma ex_has_greatest_nat_lemma:
  11.122 +     "[|P k;  ALL x. P x --> (EX y. P y & ~ ((m y::nat) <= m x))|]  
  11.123 +      ==> EX y. P y & ~ (m y < m k + n)"
  11.124 +apply (induct_tac "n")
  11.125 +apply force
  11.126 +(*ind step*)
  11.127 +apply (force simp add: le_Suc_eq)
  11.128 +done
  11.129 +
  11.130 +lemma ex_has_greatest_nat: "[|P k;  ! y. P y --> m y < b|]  
  11.131 +      ==> ? x. P x & (! y. P y --> (m y::nat) <= m x)"
  11.132 +apply (rule ccontr)
  11.133 +apply (cut_tac P = "P" and n = "b - m k" in ex_has_greatest_nat_lemma)
  11.134 +apply (subgoal_tac [3] "m k <= b")
  11.135 +apply auto
  11.136 +done
  11.137 +
  11.138 +lemma GreatestM_nat_lemma: 
  11.139 +     "[|P k;  ! y. P y --> m y < b|]  
  11.140 +      ==> P (GreatestM m P) & (!y. P y --> (m y::nat) <= m (GreatestM m P))"
  11.141 +apply (unfold GreatestM_def)
  11.142 +apply (rule someI_ex)
  11.143 +apply (erule ex_has_greatest_nat)
  11.144 +apply assumption
  11.145 +done
  11.146 +
  11.147 +lemmas GreatestM_natI = GreatestM_nat_lemma [THEN conjunct1, standard]
  11.148 +
  11.149 +lemma GreatestM_nat_le: "[|P x;  ! y. P y --> m y < b|]  
  11.150 +      ==> (m x::nat) <= m (GreatestM m P)"
  11.151 +apply (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec]) 
  11.152 +done
  11.153 +
  11.154 +(** Specialization to GREATEST **)
  11.155 +
  11.156 +lemma GreatestI: 
  11.157 +     "[|P (k::nat);  ! y. P y --> y < b|] ==> P (GREATEST x. P x)"
  11.158 +
  11.159 +apply (unfold Greatest_def)
  11.160 +apply (rule GreatestM_natI)
  11.161 +apply auto
  11.162 +done
  11.163 +
  11.164 +lemma Greatest_le: 
  11.165 +     "[|P x;  ! y. P y --> y < b|] ==> (x::nat) <= (GREATEST x. P x)"
  11.166 +apply (unfold Greatest_def)
  11.167 +apply (rule GreatestM_nat_le)
  11.168 +apply auto
  11.169 +done
  11.170 +
  11.171 +
  11.172 +ML {*
  11.173 +val LeastMI2 = thm "LeastMI2";
  11.174 +val LeastM_equality = thm "LeastM_equality";
  11.175 +val GreatestM_def = thm "GreatestM_def";
  11.176 +val GreatestMI2 = thm "GreatestMI2";
  11.177 +val GreatestM_equality = thm "GreatestM_equality";
  11.178 +val Greatest_def = thm "Greatest_def";
  11.179 +val Greatest_equality = thm "Greatest_equality";
  11.180 +val GreatestM_natI = thm "GreatestM_natI";
  11.181 +val GreatestM_nat_le = thm "GreatestM_nat_le";
  11.182 +val GreatestI = thm "GreatestI";
  11.183 +val Greatest_le = thm "Greatest_le";
  11.184 +*}
  11.185 +
  11.186 +use "meson_lemmas.ML"
  11.187 +use "Tools/meson.ML"
  11.188 +setup meson_setup
  11.189 +
  11.190 +end
    12.1 --- a/src/HOL/Integ/Int.thy	Tue Jul 24 11:25:54 2001 +0200
    12.2 +++ b/src/HOL/Integ/Int.thy	Wed Jul 25 13:13:01 2001 +0200
    12.3 @@ -6,7 +6,7 @@
    12.4  Type "int" is a linear order
    12.5  *)
    12.6  
    12.7 -Int = IntDef +
    12.8 +Int = IntDef + 
    12.9  
   12.10  instance int :: order (zle_refl,zle_trans,zle_anti_sym,int_less_le)
   12.11  instance int :: plus_ac0 (zadd_commute,zadd_assoc,zadd_zero)
   12.12 @@ -14,7 +14,7 @@
   12.13  
   12.14  constdefs
   12.15    nat  :: int => nat
   12.16 -  "nat(Z) == if neg Z then 0 else (@ m. Z = int m)"
   12.17 +  "nat(Z) == if neg Z then 0 else (THE m. Z = int m)"
   12.18  
   12.19  defs
   12.20    zabs_def  "abs(i::int) == if i < 0 then -i else i"
    13.1 --- a/src/HOL/Integ/IntDef.thy	Tue Jul 24 11:25:54 2001 +0200
    13.2 +++ b/src/HOL/Integ/IntDef.thy	Wed Jul 25 13:13:01 2001 +0200
    13.3 @@ -6,7 +6,7 @@
    13.4  The integers as equivalence classes over nat*nat.
    13.5  *)
    13.6  
    13.7 -IntDef = Equiv + NatArith +
    13.8 +IntDef = Equiv + NatArith + 
    13.9  constdefs
   13.10    intrel      :: "((nat * nat) * (nat * nat)) set"
   13.11    "intrel == {p. EX x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}"
    14.1 --- a/src/HOL/IsaMakefile	Tue Jul 24 11:25:54 2001 +0200
    14.2 +++ b/src/HOL/IsaMakefile	Wed Jul 25 13:13:01 2001 +0200
    14.3 @@ -78,7 +78,8 @@
    14.4    $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
    14.5    $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML Calculation.thy \
    14.6    Datatype.thy Datatype_Universe.ML Datatype_Universe.thy Divides.ML \
    14.7 -  Divides.thy Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML \
    14.8 +  Divides.thy Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy \
    14.9 +  Hilbert_Choice.thy Hilbert_Choice_lemmas.ML HOL.ML \
   14.10    HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \
   14.11    Integ/Equiv.ML Integ/Equiv.thy Integ/Int.ML Integ/Int.thy \
   14.12    Integ/IntArith.ML Integ/IntArith.thy Integ/IntDef.ML Integ/IntDef.thy \
    15.1 --- a/src/HOL/Nat.thy	Tue Jul 24 11:25:54 2001 +0200
    15.2 +++ b/src/HOL/Nat.thy	Wed Jul 25 13:13:01 2001 +0200
    15.3 @@ -6,7 +6,7 @@
    15.4  and * (for div, mod and dvd, see theory Divides).
    15.5  *)
    15.6  
    15.7 -Nat = NatDef +
    15.8 +Nat = NatDef + 
    15.9  
   15.10  (* type "nat" is a wellfounded linear order, and a datatype *)
   15.11  
    16.1 --- a/src/HOL/NatArith.ML	Tue Jul 24 11:25:54 2001 +0200
    16.2 +++ b/src/HOL/NatArith.ML	Wed Jul 25 13:13:01 2001 +0200
    16.3 @@ -135,54 +135,5 @@
    16.4  
    16.5  
    16.6  
    16.7 -(** GREATEST theorems for type "nat": not dual to LEAST, since there is
    16.8 -    no greatest natural number.  [The LEAST proofs are in Nat.ML, but the
    16.9 -    GREATEST proofs require more infrastructure.] **)
   16.10 -
   16.11 -Goal "[|P k;  ALL x. P x --> (EX y. P y & ~ ((m y::nat) <= m x))|] \
   16.12 -\     ==> EX y. P y & ~ (m y < m k + n)";
   16.13 -by (induct_tac "n" 1);
   16.14 -by (Force_tac 1); 
   16.15 -(*ind step*)
   16.16 -by (force_tac (claset(), simpset() addsimps [le_Suc_eq]) 1); 
   16.17 -qed "ex_has_greatest_nat_lemma";
   16.18 -
   16.19 -Goal "[|P k;  ! y. P y --> m y < b|] \
   16.20 -\     ==> ? x. P x & (! y. P y --> (m y::nat) <= m x)";
   16.21 -by (rtac ccontr 1); 
   16.22 -by (cut_inst_tac [("P","P"),("n","b - m k")] ex_has_greatest_nat_lemma 1);
   16.23 -by (subgoal_tac "m k <= b" 3);
   16.24 -by Auto_tac;  
   16.25 -qed "ex_has_greatest_nat";
   16.26 -
   16.27 -Goalw [GreatestM_def]
   16.28 -     "[|P k;  ! y. P y --> m y < b|] \
   16.29 -\     ==> P (GreatestM m P) & (!y. P y --> (m y::nat) <= m (GreatestM m P))";
   16.30 -by (rtac someI_ex 1);
   16.31 -by (etac ex_has_greatest_nat 1);
   16.32 -by (assume_tac 1); 
   16.33 -qed "GreatestM_nat_lemma";
   16.34 -
   16.35 -bind_thm ("GreatestM_natI", GreatestM_nat_lemma RS conjunct1);
   16.36 -
   16.37 -Goal "[|P x;  ! y. P y --> m y < b|] \
   16.38 -\     ==> (m x::nat) <= m (GreatestM m P)";
   16.39 -by (blast_tac (claset() addDs [GreatestM_nat_lemma RS conjunct2 RS spec]) 1);
   16.40 -qed "GreatestM_nat_le";
   16.41 -
   16.42 -(** Specialization to GREATEST **)
   16.43 -
   16.44 -Goalw [Greatest_def]
   16.45 -     "[|P (k::nat);  ! y. P y --> y < b|] ==> P (GREATEST x. P x)";
   16.46 -by (rtac GreatestM_natI 1); 
   16.47 -by Auto_tac;  
   16.48 -qed "GreatestI";
   16.49 -
   16.50 -Goalw [Greatest_def]
   16.51 -     "[|P x;  ! y. P y --> y < b|] ==> (x::nat) <= (GREATEST x. P x)";
   16.52 -by (rtac GreatestM_nat_le 1); 
   16.53 -by Auto_tac;  
   16.54 -qed "Greatest_le";
   16.55 -
   16.56  (*No analogue of not_less_Least or Least_Suc yet, since it isn't used much*)
   16.57  
    17.1 --- a/src/HOL/Ord.thy	Tue Jul 24 11:25:54 2001 +0200
    17.2 +++ b/src/HOL/Ord.thy	Wed Jul 25 13:13:01 2001 +0200
    17.3 @@ -25,8 +25,8 @@
    17.4  local
    17.5  
    17.6  syntax (symbols)
    17.7 -  "op <="       :: "['a::ord, 'a] => bool"             ("op \<le>")
    17.8 -  "op <="       :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
    17.9 +  "op <="       :: "['a::ord, 'a] => bool"             ("op \\<le>")
   17.10 +  "op <="       :: "['a::ord, 'a] => bool"             ("(_/ \\<le> _)"  [50, 51] 50)
   17.11  
   17.12  (*Tell Blast_tac about overloading of < and <= to reduce the risk of
   17.13    its applying a rule for the wrong type*)
   17.14 @@ -76,57 +76,6 @@
   17.15  done
   17.16  
   17.17  
   17.18 -(** Least value operator **)
   17.19 -
   17.20 -constdefs
   17.21 -  LeastM   :: "['a => 'b::ord, 'a => bool] => 'a"
   17.22 -              "LeastM m P == @x. P x & (!y. P y --> m x <= m y)"
   17.23 -  Least    :: "('a::ord => bool) => 'a"               (binder "LEAST " 10)
   17.24 -              "Least     == LeastM (%x. x)"
   17.25 -
   17.26 -syntax
   17.27 - "@LeastM" :: "[pttrn, 'a=>'b::ord, bool] => 'a" ("LEAST _ WRT _. _" [0,4,10]10)
   17.28 -translations
   17.29 -                "LEAST x WRT m. P" == "LeastM m (%x. P)"
   17.30 -
   17.31 -lemma LeastMI2: "[| P x; !!y. P y ==> m x <= m y;
   17.32 - !!x. [| P x; \<forall>y. P y --> m x \<le> m y |] ==> Q x
   17.33 -		 |] ==> Q (LeastM m P)";
   17.34 -apply (unfold LeastM_def)
   17.35 -apply (rule someI2_ex)
   17.36 -apply  blast
   17.37 -apply blast
   17.38 -done
   17.39 -
   17.40 -
   17.41 -(** Greatest value operator **)
   17.42 -
   17.43 -constdefs
   17.44 -  GreatestM   :: "['a => 'b::ord, 'a => bool] => 'a"
   17.45 -              "GreatestM m P == @x. P x & (!y. P y --> m y <= m x)"
   17.46 -  
   17.47 -  Greatest    :: "('a::ord => bool) => 'a"         (binder "GREATEST " 10)
   17.48 -              "Greatest     == GreatestM (%x. x)"
   17.49 -
   17.50 -syntax
   17.51 - "@GreatestM" :: "[pttrn, 'a=>'b::ord, bool] => 'a"
   17.52 -                                        ("GREATEST _ WRT _. _" [0,4,10]10)
   17.53 -
   17.54 -translations
   17.55 -              "GREATEST x WRT m. P" == "GreatestM m (%x. P)"
   17.56 -
   17.57 -lemma GreatestMI2:
   17.58 -     "[| P x;
   17.59 -	 !!y. P y ==> m y <= m x;
   17.60 -         !!x. [| P x; \<forall>y. P y --> m y \<le> m x |] ==> Q x |]
   17.61 -      ==> Q (GreatestM m P)";
   17.62 -apply (unfold GreatestM_def)
   17.63 -apply (rule someI2_ex)
   17.64 -apply  blast
   17.65 -apply blast
   17.66 -done
   17.67 -
   17.68 -
   17.69  section "Orders"
   17.70  
   17.71  axclass order < ord
   17.72 @@ -216,36 +165,19 @@
   17.73  apply (blast intro: order_antisym)
   17.74  done
   17.75  
   17.76 -lemma LeastM_equality:
   17.77 - "[| P k; !!x. P x ==> m k <= m x |] ==> m (LEAST x WRT m. P x) = 
   17.78 -     (m k::'a::order)";
   17.79 -apply (rule LeastMI2)
   17.80 -apply   assumption
   17.81 -apply  blast
   17.82 -apply (blast intro!: order_antisym) 
   17.83 -done
   17.84 +
   17.85 +(** Least value operator **)
   17.86 +
   17.87 +(*We can no longer use LeastM because the latter requires Hilbert-AC*)
   17.88 +constdefs
   17.89 +  Least    :: "('a::ord => bool) => 'a"               (binder "LEAST " 10)
   17.90 +    "Least P == THE x. P x & (ALL y. P y --> x <= y)"
   17.91  
   17.92  lemma Least_equality:
   17.93    "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k";
   17.94 -apply (unfold Least_def)
   17.95 -apply (erule LeastM_equality)
   17.96 -apply blast
   17.97 -done
   17.98 -
   17.99 -lemma GreatestM_equality:
  17.100 - "[| P k;  !!x. P x ==> m x <= m k |]
  17.101 -  ==> m (GREATEST x WRT m. P x) = (m k::'a::order)";
  17.102 -apply (rule_tac m=m in GreatestMI2)
  17.103 -apply   assumption
  17.104 -apply  blast
  17.105 -apply (blast intro!: order_antisym) 
  17.106 -done
  17.107 -
  17.108 -lemma Greatest_equality:
  17.109 -  "[| P (k::'a::order); !!x. P x ==> x <= k |] ==> (GREATEST x. P x) = k";
  17.110 -apply (unfold Greatest_def)
  17.111 -apply (erule GreatestM_equality)
  17.112 -apply blast
  17.113 +apply (simp add: Least_def)
  17.114 +apply (rule the_equality)
  17.115 +apply (auto intro!: order_antisym) 
  17.116  done
  17.117  
  17.118  
  17.119 @@ -381,10 +313,10 @@
  17.120    "_leEx"    :: "[idt, 'a, bool] => bool"  ("(3EX _<=_./ _)" [0, 0, 10] 10)
  17.121  
  17.122  syntax (symbols)
  17.123 -  "_lessAll" :: "[idt, 'a, bool] => bool"  ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
  17.124 -  "_lessEx"  :: "[idt, 'a, bool] => bool"  ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
  17.125 -  "_leAll"   :: "[idt, 'a, bool] => bool"  ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
  17.126 -  "_leEx"    :: "[idt, 'a, bool] => bool"  ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
  17.127 +  "_lessAll" :: "[idt, 'a, bool] => bool"  ("(3\\<forall>_<_./ _)"  [0, 0, 10] 10)
  17.128 +  "_lessEx"  :: "[idt, 'a, bool] => bool"  ("(3\\<exists>_<_./ _)"  [0, 0, 10] 10)
  17.129 +  "_leAll"   :: "[idt, 'a, bool] => bool"  ("(3\\<forall>_\\<le>_./ _)" [0, 0, 10] 10)
  17.130 +  "_leEx"    :: "[idt, 'a, bool] => bool"  ("(3\\<exists>_\\<le>_./ _)" [0, 0, 10] 10)
  17.131  
  17.132  syntax (HOL)
  17.133    "_lessAll" :: "[idt, 'a, bool] => bool"  ("(3! _<_./ _)"  [0, 0, 10] 10)
  17.134 @@ -401,6 +333,8 @@
  17.135  
  17.136  ML
  17.137  {*
  17.138 +val Least_def = thm "Least_def";
  17.139 +val Least_equality = thm "Least_equality";
  17.140  val mono_def = thm "mono_def";
  17.141  val monoI = thm "monoI";
  17.142  val monoD = thm "monoD";
  17.143 @@ -410,15 +344,6 @@
  17.144  val max_of_mono = thm "max_of_mono";
  17.145  val min_leastL = thm "min_leastL";
  17.146  val max_leastL = thm "max_leastL";
  17.147 -val LeastMI2 = thm "LeastMI2";
  17.148 -val LeastM_equality = thm "LeastM_equality";
  17.149 -val Least_def = thm "Least_def";
  17.150 -val Least_equality = thm "Least_equality";
  17.151 -val GreatestM_def = thm "GreatestM_def";
  17.152 -val GreatestMI2 = thm "GreatestMI2";
  17.153 -val GreatestM_equality = thm "GreatestM_equality";
  17.154 -val Greatest_def = thm "Greatest_def";
  17.155 -val Greatest_equality = thm "Greatest_equality";
  17.156  val min_leastR = thm "min_leastR";
  17.157  val max_leastR = thm "max_leastR";
  17.158  val order_eq_refl = thm "order_eq_refl";
    18.1 --- a/src/HOL/Product_Type.thy	Tue Jul 24 11:25:54 2001 +0200
    18.2 +++ b/src/HOL/Product_Type.thy	Wed Jul 25 13:13:01 2001 +0200
    18.3 @@ -30,9 +30,9 @@
    18.4  qed
    18.5  
    18.6  syntax (symbols)
    18.7 -  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
    18.8 +  "*"      :: "[type, type] => type"         ("(_ \\<times>/ _)" [21, 20] 20)
    18.9  syntax (HTML output)
   18.10 -  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
   18.11 +  "*"      :: "[type, type] => type"         ("(_ \\<times>/ _)" [21, 20] 20)
   18.12  
   18.13  
   18.14  (* abstract constants and syntax *)
   18.15 @@ -74,8 +74,8 @@
   18.16    "A <*> B"      => "Sigma A (_K B)"
   18.17  
   18.18  syntax (symbols)
   18.19 -  "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\<Sigma> _\<in>_./ _)"   10)
   18.20 -  "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
   18.21 +  "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\\<Sigma> _\\<in>_./ _)"   10)
   18.22 +  "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \\<times> _" [81, 80] 80)
   18.23  
   18.24  print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *}
   18.25  
   18.26 @@ -86,8 +86,8 @@
   18.27  
   18.28  defs
   18.29    Pair_def:     "Pair a b == Abs_Prod(Pair_Rep a b)"
   18.30 -  fst_def:      "fst p == SOME a. EX b. p = (a, b)"
   18.31 -  snd_def:      "snd p == SOME b. EX a. p = (a, b)"
   18.32 +  fst_def:      "fst p == THE a. EX b. p = (a, b)"
   18.33 +  snd_def:      "snd p == THE b. EX a. p = (a, b)"
   18.34    split_def:    "split == (%c p. c (fst p) (snd p))"
   18.35    prod_fun_def: "prod_fun f g == split(%x y.(f(x), g(y)))"
   18.36    Sigma_def:    "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
    19.1 --- a/src/HOL/Product_Type_lemmas.ML	Tue Jul 24 11:25:54 2001 +0200
    19.2 +++ b/src/HOL/Product_Type_lemmas.ML	Wed Jul 25 13:13:01 2001 +0200
    19.3 @@ -192,13 +192,13 @@
    19.4  qed "split_Pair_apply";
    19.5  
    19.6  (*Can't be added to simpset: loops!*)
    19.7 -Goal "(SOME x. P x) = (SOME (a,b). P(a,b))";
    19.8 +Goal "(THE x. P x) = (THE (a,b). P(a,b))";
    19.9  by (simp_tac (simpset() addsimps [split_Pair_apply]) 1);
   19.10 -qed "split_paired_Eps";
   19.11 +qed "split_paired_The";
   19.12  
   19.13 -Goalw [split_def] "Eps (split P) = (SOME xy. P (fst xy) (snd xy))";
   19.14 +Goalw [split_def] "The (split P) = (THE xy. P (fst xy) (snd xy))";
   19.15  by (rtac refl 1);
   19.16 -qed "Eps_split";
   19.17 +qed "The_split";
   19.18  
   19.19  Goal "!!s t. (s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
   19.20  by (split_all_tac 1);
   19.21 @@ -385,10 +385,10 @@
   19.22  qed "split_part";
   19.23  Addsimps [split_part];
   19.24  
   19.25 -Goal "(@(x',y'). x = x' & y = y') = (x,y)";
   19.26 +Goal "(THE (x',y'). x = x' & y = y') = (x,y)";
   19.27  by (Blast_tac 1);
   19.28 -qed "Eps_split_eq";
   19.29 -Addsimps [Eps_split_eq];
   19.30 +qed "The_split_eq";
   19.31 +Addsimps [The_split_eq];
   19.32  (*
   19.33  the following  would be slightly more general,
   19.34  but cannot be used as rewrite rule:
   19.35 @@ -399,7 +399,7 @@
   19.36  by ( Simp_tac 1);
   19.37  by (split_all_tac 1);
   19.38  by (Asm_full_simp_tac 1);
   19.39 -qed "Eps_split_eq";
   19.40 +qed "The_split_eq";
   19.41  *)
   19.42  
   19.43  Goal "!!x y. [|fst x = fst y; snd x = snd y|] ==> x = y";
    20.1 --- a/src/HOL/Relation.ML	Tue Jul 24 11:25:54 2001 +0200
    20.2 +++ b/src/HOL/Relation.ML	Wed Jul 25 13:13:01 2001 +0200
    20.3 @@ -333,7 +333,7 @@
    20.4  
    20.5  overload_1st_set "Relation.Image";
    20.6  
    20.7 -Goalw [Image_def] "b : r``A = (? x:A. (x,b):r)";
    20.8 +Goalw [Image_def] "b : r``A = (EX x:A. (x,b):r)";
    20.9  by (Blast_tac 1);
   20.10  qed "Image_iff";
   20.11  
   20.12 @@ -422,7 +422,7 @@
   20.13  section "single_valued";
   20.14  
   20.15  Goalw [single_valued_def]
   20.16 -     "!x y. (x,y):r --> (!z. (x,z):r --> y=z) ==> single_valued r";
   20.17 +     "ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z) ==> single_valued r";
   20.18  by (assume_tac 1);
   20.19  qed "single_valuedI";
   20.20  
   20.21 @@ -454,26 +454,18 @@
   20.22  by (Fast_tac 1);
   20.23  qed "fun_rel_comp_mono";
   20.24  
   20.25 -Goalw [fun_rel_comp_def] "! x. ?! y. (f x, y) : R ==> ?! g. g : fun_rel_comp f R";
   20.26 -by (res_inst_tac [("a","%x. @y. (f x, y) : R")] ex1I 1);
   20.27 -by (rtac CollectI 1);
   20.28 -by (rtac allI 1);
   20.29 -by (etac allE 1);
   20.30 -by (rtac (some_eq_ex RS iffD2) 1);
   20.31 -by (etac ex1_implies_ex 1);
   20.32 -by (rtac ext 1);
   20.33 -by (etac CollectE 1);
   20.34 -by (REPEAT (etac allE 1));
   20.35 -by (rtac (some1_equality RS sym) 1);
   20.36 -by (atac 1);
   20.37 -by (atac 1);
   20.38 +Goalw [fun_rel_comp_def]
   20.39 +     "ALL x. EX! y. (f x, y) : R ==> EX! g. g : fun_rel_comp f R";
   20.40 +by (res_inst_tac [("a","%x. THE y. (f x, y) : R")] ex1I 1);
   20.41 +by (fast_tac (claset() addSDs [theI']) 1); 
   20.42 +by (fast_tac (claset() addIs [ext, the1_equality RS sym]) 1);
   20.43  qed "fun_rel_comp_unique";
   20.44  
   20.45  
   20.46  section "inverse image";
   20.47  
   20.48  Goalw [trans_def,inv_image_def]
   20.49 -    "!!r. trans r ==> trans (inv_image r f)";
   20.50 +    "trans r ==> trans (inv_image r f)";
   20.51  by (Simp_tac 1);
   20.52  by (Blast_tac 1);
   20.53  qed "trans_inv_image";
    21.1 --- a/src/HOL/Wellfounded_Recursion.ML	Tue Jul 24 11:25:54 2001 +0200
    21.2 +++ b/src/HOL/Wellfounded_Recursion.ML	Wed Jul 25 13:13:01 2001 +0200
    21.3 @@ -253,20 +253,15 @@
    21.4  (*** John Harrison, "Inductive definitions: automation and application" ***)
    21.5  
    21.6  Goalw [adm_wf_def]
    21.7 -  "[| wf R; adm_wf R F |] ==> EX! y. (x, y) : wfrec_rel R F";
    21.8 +  "[| adm_wf R F; wf R |] ==> EX! y. (x, y) : wfrec_rel R F";
    21.9  by (wf_ind_tac "x" [] 1);
   21.10  by (rtac ex1I 1);
   21.11 -by (res_inst_tac [("g","%x. @y. (x, y) : wfrec_rel R F")] wfrec_rel.wfrecI 1);
   21.12 -by (strip_tac 1);
   21.13 -byev [etac allE 1, etac impE 1, atac 1];
   21.14 -by (rtac (some_eq_ex RS ssubst) 1);
   21.15 -by (etac ex1_implies_ex 1);
   21.16 +by (res_inst_tac [("g","%x. THE y. (x, y) : wfrec_rel R F")] wfrec_rel.wfrecI 1);
   21.17 +by (fast_tac (claset() addSDs [theI']) 1); 
   21.18  by (etac wfrec_rel.elim 1);
   21.19  by (Asm_full_simp_tac 1);
   21.20  byev [etac allE 1, etac allE 1, etac allE 1, etac mp 1];
   21.21 -by (strip_tac 1);
   21.22 -by (rtac (some_equality RS ssubst) 1);
   21.23 -by (ALLGOALS Blast_tac);
   21.24 +by (fast_tac (claset() addIs [the_equality RS sym]) 1);
   21.25  qed "wfrec_unique";
   21.26  
   21.27  Goalw [adm_wf_def] "adm_wf R (%f x. F (cut f R x) x)";
   21.28 @@ -278,15 +273,14 @@
   21.29  
   21.30  Goalw [wfrec_def]
   21.31      "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a";
   21.32 -by (rtac (adm_lemma RSN (2, wfrec_unique) RS some1_equality) 1);
   21.33 +by (rtac (adm_lemma RS wfrec_unique RS the1_equality) 1);
   21.34  by (atac 1);
   21.35  by (rtac wfrec_rel.wfrecI 1);
   21.36  by (strip_tac 1);
   21.37 -by (rtac (some_eq_ex RS iffD2) 1);
   21.38 -by (rtac (adm_lemma RSN (2, wfrec_unique) RS ex1_implies_ex) 1);
   21.39 -by (atac 1);
   21.40 +by (etac (adm_lemma RS wfrec_unique RS theI') 1);
   21.41  qed "wfrec";
   21.42  
   21.43 +
   21.44  (*---------------------------------------------------------------------------
   21.45   * This form avoids giant explosions in proofs.  NOTE USE OF == 
   21.46   *---------------------------------------------------------------------------*)
    22.1 --- a/src/HOL/Wellfounded_Recursion.thy	Tue Jul 24 11:25:54 2001 +0200
    22.2 +++ b/src/HOL/Wellfounded_Recursion.thy	Wed Jul 25 13:13:01 2001 +0200
    22.3 @@ -6,7 +6,7 @@
    22.4  Well-founded Recursion
    22.5  *)
    22.6  
    22.7 -Wellfounded_Recursion = Transitive_Closure +
    22.8 +Wellfounded_Recursion = Transitive_Closure + 
    22.9  
   22.10  consts
   22.11    wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => ('a * 'b) set"
   22.12 @@ -31,7 +31,7 @@
   22.13       (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
   22.14  
   22.15    wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
   22.16 -  "wfrec R F == %x. @y. (x, y) : wfrec_rel R (%f x. F (cut f R x) x)"
   22.17 +  "wfrec R F == %x. THE y. (x, y) : wfrec_rel R (%f x. F (cut f R x) x)"
   22.18  
   22.19  axclass
   22.20    wellorder < linorder
    23.1 --- a/src/HOL/Wellfounded_Relations.thy	Tue Jul 24 11:25:54 2001 +0200
    23.2 +++ b/src/HOL/Wellfounded_Relations.thy	Wed Jul 25 13:13:01 2001 +0200
    23.3 @@ -10,9 +10,9 @@
    23.4  separately.
    23.5  *)
    23.6  
    23.7 -Wellfounded_Relations = Finite +
    23.8 +Wellfounded_Relations = Finite + Hilbert_Choice + 
    23.9  
   23.10 -(* actually belongs to theory Finite *)
   23.11 +(* logically belongs in Finite.thy, but the theorems are proved in Finite.ML *)
   23.12  instance unit :: finite                  (finite_unit)
   23.13  instance "*" :: (finite,finite) finite   (finite_Prod)
   23.14  
    24.1 --- a/src/HOL/cladata.ML	Tue Jul 24 11:25:54 2001 +0200
    24.2 +++ b/src/HOL/cladata.ML	Wed Jul 25 13:13:01 2001 +0200
    24.3 @@ -66,7 +66,7 @@
    24.4                         addSEs [conjE,disjE,impCE,FalseE,iffCE];
    24.5  
    24.6  (*Quantifier rules*)
    24.7 -val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI, some_equality, the_equality] 
    24.8 +val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI, the_equality] 
    24.9                       addSEs [exE] addEs [allE];
   24.10  
   24.11  val clasetup = [fn thy => (claset_ref_of thy := HOL_cs; thy)];
    25.1 --- a/src/HOL/ex/Tarski.ML	Tue Jul 24 11:25:54 2001 +0200
    25.2 +++ b/src/HOL/ex/Tarski.ML	Wed Jul 25 13:13:01 2001 +0200
    25.3 @@ -84,12 +84,14 @@
    25.4                         (thm "cl_co");
    25.5  Addsimps [simp_CL, thm "cl_co"];
    25.6  
    25.7 -Goalw [Ex_def] "(EX L. islub S cl L) = islub S cl (lub S cl)";
    25.8 -by (simp_tac (simpset() addsimps [lub_def, least_def, islub_def]) 1);
    25.9 +Goal "(EX L. islub S cl L) = islub S cl (lub S cl)";
   25.10 +by (simp_tac (simpset() addsimps [lub_def, least_def, islub_def, 
   25.11 +                                  some_eq_ex RS sym]) 1);
   25.12  qed "islub_lub";
   25.13  
   25.14 -Goalw [Ex_def] "(EX G. isglb S cl G) = isglb S cl (glb S cl)";
   25.15 -by (simp_tac (simpset() addsimps [glb_def, greatest_def, isglb_def]) 1);
   25.16 +Goal "(EX G. isglb S cl G) = isglb S cl (glb S cl)";
   25.17 +by (simp_tac (simpset() addsimps [glb_def, greatest_def, isglb_def, 
   25.18 +                                  some_eq_ex RS sym]) 1);
   25.19  qed "isglb_glb";
   25.20  
   25.21  Goal "isglb S cl = islub S (dual cl)";
    26.1 --- a/src/HOL/ex/mesontest.ML	Tue Jul 24 11:25:54 2001 +0200
    26.2 +++ b/src/HOL/ex/mesontest.ML	Wed Jul 25 13:13:01 2001 +0200
    26.3 @@ -33,7 +33,7 @@
    26.4  
    26.5  writeln"File HOL/ex/meson-test.";
    26.6  
    26.7 -context Fun.thy;
    26.8 +context Main.thy;
    26.9  
   26.10  (*Deep unifications can be required, esp. during transformation to clauses*)
   26.11  val orig_trace_bound = !Unify.trace_bound
    27.1 --- a/src/HOL/ex/mesontest2.ML	Tue Jul 24 11:25:54 2001 +0200
    27.2 +++ b/src/HOL/ex/mesontest2.ML	Wed Jul 25 13:13:01 2001 +0200
    27.3 @@ -6,6 +6,9 @@
    27.4  MORE and MUCH HARDER test data for the MESON proof procedure
    27.5  
    27.6  Courtesy John Harrison 
    27.7 +
    27.8 +WARNING: there are many potential conflicts between variables used below
    27.9 +and constants declared in HOL!
   27.10  *)
   27.11  
   27.12  (*All but the fastest are ignored to reduce build time*)
   27.13 @@ -17,6 +20,8 @@
   27.14  
   27.15  set timing;
   27.16  
   27.17 +context Main.thy;
   27.18 +
   27.19  (* ========================================================================= *)
   27.20  (* 100 problems selected from the TPTP library                               *)
   27.21  (* ========================================================================= *)
   27.22 @@ -155,10 +160,10 @@
   27.23  \  (! Y Z V1 V2 X V3 V4. sum(X::'a,Y,V1) & sum(X::'a,Z,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(X::'a,V3,V4)) &    \
   27.24  \  (! Y Z V3 X V1 V2 V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & sum(V3::'a,X,V4) --> product(V1::'a,V2,V4)) &    \
   27.25  \  (! Y Z V1 V2 V3 X V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(V3::'a,X,V4)) &    \
   27.26 -\  (! X. sum(inverse(X),X,multiplicative_identity)) &   \
   27.27 -\  (! X. sum(X::'a,inverse(X),multiplicative_identity)) &   \
   27.28 -\  (! X. product(inverse(X),X,additive_identity)) &     \
   27.29 -\  (! X. product(X::'a,inverse(X),additive_identity)) &     \
   27.30 +\  (! X. sum(INVERSE(X),X,multiplicative_identity)) &   \
   27.31 +\  (! X. sum(X::'a,INVERSE(X),multiplicative_identity)) &   \
   27.32 +\  (! X. product(INVERSE(X),X,additive_identity)) &     \
   27.33 +\  (! X. product(X::'a,INVERSE(X),additive_identity)) &     \
   27.34  \  (! X Y U V. sum(X::'a,Y,U) & sum(X::'a,Y,V) --> equal(U::'a,V)) &        \
   27.35  \  (! X Y U V. product(X::'a,Y,U) & product(X::'a,Y,V) --> equal(U::'a,V)) &        \
   27.36  \  (! X Y W Z. equal(X::'a,Y) & sum(X::'a,W,Z) --> sum(Y::'a,W,Z)) &        \
   27.37 @@ -171,7 +176,7 @@
   27.38  \  (! X W Y. equal(X::'a,Y) --> equal(add(W::'a,X),add(W::'a,Y))) & \
   27.39  \  (! X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) &       \
   27.40  \  (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) &       \
   27.41 -\  (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) &       \
   27.42 +\  (! X Y. equal(X::'a,Y) --> equal(INVERSE(X),INVERSE(Y))) &       \
   27.43  \  (~product(x::'a,x,x)) --> False",
   27.44    meson_tac 1);
   27.45  
   27.46 @@ -198,10 +203,10 @@
   27.47  \  (! Y Z V1 V2 X V3 V4. sum(X::'a,Y,V1) & sum(X::'a,Z,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(X::'a,V3,V4)) &    \
   27.48  \  (! Y Z V3 X V1 V2 V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & sum(V3::'a,X,V4) --> product(V1::'a,V2,V4)) &    \
   27.49  \  (! Y Z V1 V2 V3 X V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(V3::'a,X,V4)) &    \
   27.50 -\  (! X. sum(inverse(X),X,multiplicative_identity)) &   \
   27.51 -\  (! X. sum(X::'a,inverse(X),multiplicative_identity)) &   \
   27.52 -\  (! X. product(inverse(X),X,additive_identity)) &     \
   27.53 -\  (! X. product(X::'a,inverse(X),additive_identity)) &     \
   27.54 +\  (! X. sum(INVERSE(X),X,multiplicative_identity)) &   \
   27.55 +\  (! X. sum(X::'a,INVERSE(X),multiplicative_identity)) &   \
   27.56 +\  (! X. product(INVERSE(X),X,additive_identity)) &     \
   27.57 +\  (! X. product(X::'a,INVERSE(X),additive_identity)) &     \
   27.58  \  (! X Y U V. sum(X::'a,Y,U) & sum(X::'a,Y,V) --> equal(U::'a,V)) &        \
   27.59  \  (! X Y U V. product(X::'a,Y,U) & product(X::'a,Y,V) --> equal(U::'a,V)) &        \
   27.60  \  (! X Y W Z. equal(X::'a,Y) & sum(X::'a,W,Z) --> sum(Y::'a,W,Z)) &        \
   27.61 @@ -214,7 +219,7 @@
   27.62  \  (! X W Y. equal(X::'a,Y) --> equal(add(W::'a,X),add(W::'a,Y))) & \
   27.63  \  (! X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) &       \
   27.64  \  (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) &       \
   27.65 -\  (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) &       \
   27.66 +\  (! X Y. equal(X::'a,Y) --> equal(INVERSE(X),INVERSE(Y))) &       \
   27.67  \  (~sum(x::'a,x,x)) --> False",
   27.68    meson_tac 1);
   27.69  
   27.70 @@ -239,10 +244,10 @@
   27.71  \  (! Y Z V1 V2 X V3 V4. sum(X::'a,Y,V1) & sum(X::'a,Z,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(X::'a,V3,V4)) &    \
   27.72  \  (! Y Z V3 X V1 V2 V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & sum(V3::'a,X,V4) --> product(V1::'a,V2,V4)) &    \
   27.73  \  (! Y Z V1 V2 V3 X V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(V3::'a,X,V4)) &    \
   27.74 -\  (! X. sum(inverse(X),X,multiplicative_identity)) &   \
   27.75 -\  (! X. sum(X::'a,inverse(X),multiplicative_identity)) &   \
   27.76 -\  (! X. product(inverse(X),X,additive_identity)) &     \
   27.77 -\  (! X. product(X::'a,inverse(X),additive_identity)) &     \
   27.78 +\  (! X. sum(INVERSE(X),X,multiplicative_identity)) &   \
   27.79 +\  (! X. sum(X::'a,INVERSE(X),multiplicative_identity)) &   \
   27.80 +\  (! X. product(INVERSE(X),X,additive_identity)) &     \
   27.81 +\  (! X. product(X::'a,INVERSE(X),additive_identity)) &     \
   27.82  \  (! X Y U V. sum(X::'a,Y,U) & sum(X::'a,Y,V) --> equal(U::'a,V)) &        \
   27.83  \  (! X Y U V. product(X::'a,Y,U) & product(X::'a,Y,V) --> equal(U::'a,V)) &        \
   27.84  \  (! X Y W Z. equal(X::'a,Y) & sum(X::'a,W,Z) --> sum(Y::'a,W,Z)) &        \
   27.85 @@ -255,7 +260,7 @@
   27.86  \  (! X W Y. equal(X::'a,Y) --> equal(add(W::'a,X),add(W::'a,Y))) & \
   27.87  \  (! X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) &       \
   27.88  \  (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) &       \
   27.89 -\  (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) &       \
   27.90 +\  (! X Y. equal(X::'a,Y) --> equal(INVERSE(X),INVERSE(Y))) &       \
   27.91  \  (~sum(x::'a,multiplicative_identity,multiplicative_identity)) --> False",
   27.92    meson_tac 1);
   27.93  
   27.94 @@ -280,10 +285,10 @@
   27.95  \  (! Y Z V1 V2 X V3 V4. sum(X::'a,Y,V1) & sum(X::'a,Z,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(X::'a,V3,V4)) &    \
   27.96  \  (! Y Z V3 X V1 V2 V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & sum(V3::'a,X,V4) --> product(V1::'a,V2,V4)) &    \
   27.97  \  (! Y Z V1 V2 V3 X V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(V3::'a,X,V4)) &    \
   27.98 -\  (! X. sum(inverse(X),X,multiplicative_identity)) &   \
   27.99 -\  (! X. sum(X::'a,inverse(X),multiplicative_identity)) &   \
  27.100 -\  (! X. product(inverse(X),X,additive_identity)) &     \
  27.101 -\  (! X. product(X::'a,inverse(X),additive_identity)) &     \
  27.102 +\  (! X. sum(INVERSE(X),X,multiplicative_identity)) &   \
  27.103 +\  (! X. sum(X::'a,INVERSE(X),multiplicative_identity)) &   \
  27.104 +\  (! X. product(INVERSE(X),X,additive_identity)) &     \
  27.105 +\  (! X. product(X::'a,INVERSE(X),additive_identity)) &     \
  27.106  \  (! X Y U V. sum(X::'a,Y,U) & sum(X::'a,Y,V) --> equal(U::'a,V)) &        \
  27.107  \  (! X Y U V. product(X::'a,Y,U) & product(X::'a,Y,V) --> equal(U::'a,V)) &        \
  27.108  \  (! X Y W Z. equal(X::'a,Y) & sum(X::'a,W,Z) --> sum(Y::'a,W,Z)) &        \
  27.109 @@ -296,7 +301,7 @@
  27.110  \  (! X W Y. equal(X::'a,Y) --> equal(add(W::'a,X),add(W::'a,Y))) & \
  27.111  \  (! X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) &       \
  27.112  \  (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) &       \
  27.113 -\  (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) &       \
  27.114 +\  (! X Y. equal(X::'a,Y) --> equal(INVERSE(X),INVERSE(Y))) &       \
  27.115  \  (~product(x::'a,additive_identity,additive_identity)) --> False",
  27.116    meson_tac 1);
  27.117  
  27.118 @@ -321,10 +326,10 @@
  27.119  \  (! Y Z V1 V2 X V3 V4. sum(X::'a,Y,V1) & sum(X::'a,Z,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(X::'a,V3,V4)) &    \
  27.120  \  (! Y Z V3 X V1 V2 V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & sum(V3::'a,X,V4) --> product(V1::'a,V2,V4)) &    \
  27.121  \  (! Y Z V1 V2 V3 X V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(V3::'a,X,V4)) &    \
  27.122 -\  (! X. sum(inverse(X),X,multiplicative_identity)) &   \
  27.123 -\  (! X. sum(X::'a,inverse(X),multiplicative_identity)) &   \
  27.124 -\  (! X. product(inverse(X),X,additive_identity)) &     \
  27.125 -\  (! X. product(X::'a,inverse(X),additive_identity)) &     \
  27.126 +\  (! X. sum(INVERSE(X),X,multiplicative_identity)) &   \
  27.127 +\  (! X. sum(X::'a,INVERSE(X),multiplicative_identity)) &   \
  27.128 +\  (! X. product(INVERSE(X),X,additive_identity)) &     \
  27.129 +\  (! X. product(X::'a,INVERSE(X),additive_identity)) &     \
  27.130  \  (! X Y U V. sum(X::'a,Y,U) & sum(X::'a,Y,V) --> equal(U::'a,V)) &        \
  27.131  \  (! X Y U V. product(X::'a,Y,U) & product(X::'a,Y,V) --> equal(U::'a,V)) &        \
  27.132  \  (! X Y W Z. equal(X::'a,Y) & sum(X::'a,W,Z) --> sum(Y::'a,W,Z)) &        \
  27.133 @@ -337,8 +342,8 @@
  27.134  \  (! X W Y. equal(X::'a,Y) --> equal(add(W::'a,X),add(W::'a,Y))) & \
  27.135  \  (! X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) &       \
  27.136  \  (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) &       \
  27.137 -\  (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) &       \
  27.138 -\  (~equal(inverse(additive_identity),multiplicative_identity)) --> False",
  27.139 +\  (! X Y. equal(X::'a,Y) --> equal(INVERSE(X),INVERSE(Y))) &       \
  27.140 +\  (~equal(INVERSE(additive_identity),multiplicative_identity)) --> False",
  27.141    meson_tac 1);
  27.142  
  27.143  (*4007 inferences so far.  Searching to depth 9.  13 secs*)
  27.144 @@ -736,11 +741,11 @@
  27.145  \  (! E1 G1 F1. equal(E1::'a,F1) & failure_node(G1::'a,E1) --> failure_node(G1::'a,F1)) &   \
  27.146  \  (! H1 I1 J1. equal(H1::'a,I1) & siblings(H1::'a,J1) --> siblings(I1::'a,J1)) &   \
  27.147  \  (! K1 M1 L1. equal(K1::'a,L1) & siblings(M1::'a,K1) --> siblings(M1::'a,L1)) &   \
  27.148 -\  (failure_node(n_left::'a,or(empty::'a,atom))) &      \
  27.149 -\  (failure_node(n_right::'a,or(empty::'a,negate(atom)))) &     \
  27.150 +\  (failure_node(n_left::'a,or(EMPTY::'a,atom))) &      \
  27.151 +\  (failure_node(n_right::'a,or(EMPTY::'a,negate(atom)))) &     \
  27.152  \  (equal(n_left::'a,left_child_of(n))) &   \
  27.153  \  (equal(n_right::'a,right_child_of(n))) & \
  27.154 -\  (! Z. ~failure_node(Z::'a,or(empty::'a,empty))) --> False",
  27.155 +\  (! Z. ~failure_node(Z::'a,or(EMPTY::'a,EMPTY))) --> False",
  27.156    meson_tac 1);
  27.157  ****************)
  27.158  
  27.159 @@ -1012,7 +1017,7 @@
  27.160  (*0 inferences so far.  Searching to depth 0.  0.2 secs*)
  27.161  val GEO079_1 = prove
  27.162   ("(! U V W X Y Z. right_angle(U::'a,V,W) & right_angle(X::'a,Y,Z) --> eq(U::'a,V,W,X,Y,Z)) &       \
  27.163 -\  (! U V W X Y Z. congruent(U::'a,V,W,X,Y,Z) --> eq(U::'a,V,W,X,Y,Z)) &        \
  27.164 +\  (! U V W X Y Z. CONGRUENT(U::'a,V,W,X,Y,Z) --> eq(U::'a,V,W,X,Y,Z)) &        \
  27.165  \  (! V W U X. trapezoid(U::'a,V,W,X) --> parallel(V::'a,W,U,X)) &      \
  27.166  \  (! U V X Y. parallel(U::'a,V,X,Y) --> eq(X::'a,V,U,V,X,Y)) & \
  27.167  \  (trapezoid(a::'a,b,c,d)) &       \
  27.168 @@ -1027,13 +1032,13 @@
  27.169  \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
  27.170  \  (! X. product(identity::'a,X,X)) &       \
  27.171  \  (! X. product(X::'a,identity,X)) &       \
  27.172 -\  (! X. product(inverse(X),X,identity)) &      \
  27.173 -\  (! X. product(X::'a,inverse(X),identity)) &      \
  27.174 +\  (! X. product(INVERSE(X),X,identity)) &      \
  27.175 +\  (! X. product(X::'a,INVERSE(X),identity)) &      \
  27.176  \  (! X Y. product(X::'a,Y,multiply(X::'a,Y))) &        \
  27.177  \  (! X Y Z W. product(X::'a,Y,Z) & product(X::'a,Y,W) --> equal(Z::'a,W)) &        \
  27.178  \  (! Y U Z X V W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(U::'a,Z,W) --> product(X::'a,V,W)) &       \
  27.179  \  (! Y X V U Z W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(X::'a,V,W) --> product(U::'a,Z,W)) &       \
  27.180 -\  (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) &       \
  27.181 +\  (! X Y. equal(X::'a,Y) --> equal(INVERSE(X),INVERSE(Y))) &       \
  27.182  \  (! X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) &       \
  27.183  \  (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) &       \
  27.184  \  (! X Y W Z. equal(X::'a,Y) & product(X::'a,W,Z) --> product(Y::'a,W,Z)) &        \
  27.185 @@ -1052,13 +1057,13 @@
  27.186  \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
  27.187  \  (! X. product(identity::'a,X,X)) &       \
  27.188  \  (! X. product(X::'a,identity,X)) &       \
  27.189 -\  (! X. product(inverse(X),X,identity)) &      \
  27.190 -\  (! X. product(X::'a,inverse(X),identity)) &      \
  27.191 +\  (! X. product(INVERSE(X),X,identity)) &      \
  27.192 +\  (! X. product(X::'a,INVERSE(X),identity)) &      \
  27.193  \  (! X Y. product(X::'a,Y,multiply(X::'a,Y))) &        \
  27.194  \  (! X Y Z W. product(X::'a,Y,Z) & product(X::'a,Y,W) --> equal(Z::'a,W)) &        \
  27.195  \  (! Y U Z X V W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(U::'a,Z,W) --> product(X::'a,V,W)) &       \
  27.196  \  (! Y X V U Z W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(X::'a,V,W) --> product(U::'a,Z,W)) &       \
  27.197 -\  (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) &       \
  27.198 +\  (! X Y. equal(X::'a,Y) --> equal(INVERSE(X),INVERSE(Y))) &       \
  27.199  \  (! X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) &       \
  27.200  \  (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) &       \
  27.201  \  (! X Y W Z. equal(X::'a,Y) & product(X::'a,W,Z) --> product(Y::'a,W,Z)) &        \
  27.202 @@ -1080,13 +1085,13 @@
  27.203  \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
  27.204  \  (! X. product(identity::'a,X,X)) &       \
  27.205  \  (! X. product(X::'a,identity,X)) &       \
  27.206 -\  (! X. product(inverse(X),X,identity)) &      \
  27.207 -\  (! X. product(X::'a,inverse(X),identity)) &      \
  27.208 +\  (! X. product(INVERSE(X),X,identity)) &      \
  27.209 +\  (! X. product(X::'a,INVERSE(X),identity)) &      \
  27.210  \  (! X Y. product(X::'a,Y,multiply(X::'a,Y))) &        \
  27.211  \  (! X Y Z W. product(X::'a,Y,Z) & product(X::'a,Y,W) --> equal(Z::'a,W)) &        \
  27.212  \  (! Y U Z X V W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(U::'a,Z,W) --> product(X::'a,V,W)) &       \
  27.213  \  (! Y X V U Z W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(X::'a,V,W) --> product(U::'a,Z,W)) &       \
  27.214 -\  (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) &       \
  27.215 +\  (! X Y. equal(X::'a,Y) --> equal(INVERSE(X),INVERSE(Y))) &       \
  27.216  \  (! X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) &       \
  27.217  \  (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) &       \
  27.218  \  (! X Y W Z. equal(X::'a,Y) & product(X::'a,W,Z) --> product(Y::'a,W,Z)) &        \
  27.219 @@ -1094,8 +1099,8 @@
  27.220  \  (! X W Z Y. equal(X::'a,Y) & product(W::'a,Z,X) --> product(W::'a,Z,Y)) &        \
  27.221  \  (! A. product(A::'a,A,identity)) &       \
  27.222  \  (product(a::'a,b,c)) &   \
  27.223 -\  (product(inverse(a),inverse(b),d)) & \
  27.224 -\  (! A C B. product(inverse(A),inverse(B),C) --> product(A::'a,C,B)) &     \
  27.225 +\  (product(INVERSE(a),INVERSE(b),d)) & \
  27.226 +\  (! A C B. product(INVERSE(A),INVERSE(B),C) --> product(A::'a,C,B)) &     \
  27.227  \  (~product(c::'a,d,identity)) --> False",
  27.228    meson_tac 1);
  27.229  
  27.230 @@ -1106,19 +1111,19 @@
  27.231  \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
  27.232  \  (! X. product(identity::'a,X,X)) &       \
  27.233  \  (! X. product(X::'a,identity,X)) &       \
  27.234 -\  (! X. product(inverse(X),X,identity)) &      \
  27.235 -\  (! X. product(X::'a,inverse(X),identity)) &      \
  27.236 +\  (! X. product(INVERSE(X),X,identity)) &      \
  27.237 +\  (! X. product(X::'a,INVERSE(X),identity)) &      \
  27.238  \  (! X Y. product(X::'a,Y,multiply(X::'a,Y))) &        \
  27.239  \  (! X Y Z W. product(X::'a,Y,Z) & product(X::'a,Y,W) --> equal(Z::'a,W)) &        \
  27.240  \  (! Y U Z X V W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(U::'a,Z,W) --> product(X::'a,V,W)) &       \
  27.241  \  (! Y X V U Z W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(X::'a,V,W) --> product(U::'a,Z,W)) &       \
  27.242 -\  (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) &       \
  27.243 +\  (! X Y. equal(X::'a,Y) --> equal(INVERSE(X),INVERSE(Y))) &       \
  27.244  \  (! X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) &       \
  27.245  \  (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) &       \
  27.246  \  (! X Y W Z. equal(X::'a,Y) & product(X::'a,W,Z) --> product(Y::'a,W,Z)) &        \
  27.247  \  (! X W Y Z. equal(X::'a,Y) & product(W::'a,X,Z) --> product(W::'a,Y,Z)) &        \
  27.248  \  (! X W Z Y. equal(X::'a,Y) & product(W::'a,Z,X) --> product(W::'a,Z,Y)) &        \
  27.249 -\  (! A B C. subgroup_member(A) & subgroup_member(B) & product(A::'a,inverse(B),C) --> subgroup_member(C)) &        \
  27.250 +\  (! A B C. subgroup_member(A) & subgroup_member(B) & product(A::'a,INVERSE(B),C) --> subgroup_member(C)) &        \
  27.251  \  (! A B. equal(A::'a,B) & subgroup_member(A) --> subgroup_member(B)) &    \
  27.252  \  (! A. subgroup_member(A) --> product(another_identity::'a,A,A)) &        \
  27.253  \  (! A. subgroup_member(A) --> product(A::'a,another_identity,A)) &        \
  27.254 @@ -1130,7 +1135,7 @@
  27.255  \  (! B C D A. product(A::'a,B,C) & product(D::'a,B,C) --> equal(D::'a,A)) &        \
  27.256  \  (subgroup_member(a)) &       \
  27.257  \  (subgroup_member(another_identity)) &        \
  27.258 -\  (~equal(inverse(a),another_inverse(a))) --> False",
  27.259 +\  (~equal(INVERSE(a),another_inverse(a))) --> False",
  27.260    meson_tac 1);
  27.261  
  27.262  (*163 inferences so far.  Searching to depth 11.  0.3 secs*)
  27.263 @@ -1139,7 +1144,7 @@
  27.264  \  (! X Y Z W. product(X::'a,Y,Z) & product(X::'a,Y,W) --> equal(Z::'a,W)) &        \
  27.265  \  (! Y U Z X V W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(U::'a,Z,W) --> product(X::'a,V,W)) &       \
  27.266  \  (! Y X V U Z W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(X::'a,V,W) --> product(U::'a,Z,W)) &       \
  27.267 -\  (! A. product(A::'a,inverse(A),identity)) &      \
  27.268 +\  (! A. product(A::'a,INVERSE(A),identity)) &      \
  27.269  \  (! A. product(A::'a,identity,A)) &       \
  27.270  \  (! A. ~product(A::'a,a,identity)) --> False",
  27.271    meson_tac 1);
  27.272 @@ -1149,18 +1154,18 @@
  27.273   ("(! X Y. product(X::'a,Y,multiply(X::'a,Y))) &        \
  27.274  \  (! X. product(identity::'a,X,X)) &       \
  27.275  \  (! X. product(X::'a,identity,X)) &       \
  27.276 -\  (! X. product(X::'a,inverse(X),identity)) &      \
  27.277 +\  (! X. product(X::'a,INVERSE(X),identity)) &      \
  27.278  \  (! Y U Z X V W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(U::'a,Z,W) --> product(X::'a,V,W)) &       \
  27.279  \  (! Y X V U Z W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(X::'a,V,W) --> product(U::'a,Z,W)) &       \
  27.280 -\  (! B A C. subgroup_member(A) & subgroup_member(B) & product(B::'a,inverse(A),C) --> subgroup_member(C)) &        \
  27.281 +\  (! B A C. subgroup_member(A) & subgroup_member(B) & product(B::'a,INVERSE(A),C) --> subgroup_member(C)) &        \
  27.282  \  (subgroup_member(a)) &       \
  27.283 -\  (~subgroup_member(inverse(a))) --> False",
  27.284 +\  (~subgroup_member(INVERSE(a))) --> False",
  27.285    meson_tac 1);
  27.286  
  27.287  (*3287 inferences so far.  Searching to depth 14.  3.5 secs*)
  27.288  val GRP047_2 = prove_hard
  27.289   ("(! X. product(identity::'a,X,X)) &       \
  27.290 -\  (! X. product(inverse(X),X,identity)) &      \
  27.291 +\  (! X. product(INVERSE(X),X,identity)) &      \
  27.292  \  (! X Y. product(X::'a,Y,multiply(X::'a,Y))) &        \
  27.293  \  (! X Y Z W. product(X::'a,Y,Z) & product(X::'a,Y,W) --> equal(Z::'a,W)) &        \
  27.294  \  (! Y U Z X V W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(U::'a,Z,W) --> product(X::'a,V,W)) &       \
  27.295 @@ -1189,9 +1194,9 @@
  27.296  \  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
  27.297  \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
  27.298  \  (! X. equal(multiply(identity::'a,X),X)) &       \
  27.299 -\  (! X. equal(multiply(inverse(X),X),identity)) &      \
  27.300 +\  (! X. equal(multiply(INVERSE(X),X),identity)) &      \
  27.301  \  (! X Y Z. equal(multiply(multiply(X::'a,Y),Z),multiply(X::'a,multiply(Y::'a,Z)))) &      \
  27.302 -\  (! A B. equal(A::'a,B) --> equal(inverse(A),inverse(B))) &       \
  27.303 +\  (! A B. equal(A::'a,B) --> equal(INVERSE(A),INVERSE(B))) &       \
  27.304  \  (! C D E. equal(C::'a,D) --> equal(multiply(C::'a,E),multiply(D::'a,E))) &       \
  27.305  \  (! F' H G. equal(F'::'a,G) --> equal(multiply(H::'a,F'),multiply(H::'a,G))) &    \
  27.306  \  (! Y X. equal(greatest_lower_bound(X::'a,Y),greatest_lower_bound(Y::'a,X))) &        \
  27.307 @@ -1222,9 +1227,9 @@
  27.308  \  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
  27.309  \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
  27.310  \  (! X. equal(multiply(identity::'a,X),X)) &       \
  27.311 -\  (! X. equal(multiply(inverse(X),X),identity)) &      \
  27.312 +\  (! X. equal(multiply(INVERSE(X),X),identity)) &      \
  27.313  \  (! X Y Z. equal(multiply(multiply(X::'a,Y),Z),multiply(X::'a,multiply(Y::'a,Z)))) &      \
  27.314 -\  (! A B. equal(A::'a,B) --> equal(inverse(A),inverse(B))) &       \
  27.315 +\  (! A B. equal(A::'a,B) --> equal(INVERSE(A),INVERSE(B))) &       \
  27.316  \  (! C D E. equal(C::'a,D) --> equal(multiply(C::'a,E),multiply(D::'a,E))) &       \
  27.317  \  (! F' H G. equal(F'::'a,G) --> equal(multiply(H::'a,F'),multiply(H::'a,G))) &    \
  27.318  \  (! Y X. equal(greatest_lower_bound(X::'a,Y),greatest_lower_bound(Y::'a,X))) &        \
  27.319 @@ -1246,7 +1251,7 @@
  27.320  \  (! A B C. equal(A::'a,B) --> equal(multiply(A::'a,C),multiply(B::'a,C))) &       \
  27.321  \  (! A C B. equal(A::'a,B) --> equal(multiply(C::'a,A),multiply(C::'a,B))) &       \
  27.322  \  (equal(least_upper_bound(a::'a,b),b)) &  \
  27.323 -\  (~equal(least_upper_bound(multiply(inverse(c),multiply(a::'a,c)),multiply(inverse(c),multiply(b::'a,c))),multiply(inverse(c),multiply(b::'a,c)))) --> False",
  27.324 +\  (~equal(least_upper_bound(multiply(INVERSE(c),multiply(a::'a,c)),multiply(INVERSE(c),multiply(b::'a,c))),multiply(INVERSE(c),multiply(b::'a,c)))) --> False",
  27.325    meson_tac 1);
  27.326  
  27.327  (*250258 inferences so far.  Searching to depth 16.  406.2 secs*)
  27.328 @@ -1664,8 +1669,8 @@
  27.329  \  (! X. subclass(flip(X),cross_product(cross_product(universal_class::'a,universal_class),universal_class))) &     \
  27.330  \  (! V U W X. member(ordered_pair(ordered_pair(U::'a,V),W),flip(X)) --> member(ordered_pair(ordered_pair(V::'a,U),W),X)) &     \
  27.331  \  (! U V W X. member(ordered_pair(ordered_pair(V::'a,U),W),X) & member(ordered_pair(ordered_pair(U::'a,V),W),cross_product(cross_product(universal_class::'a,universal_class),universal_class)) --> member(ordered_pair(ordered_pair(U::'a,V),W),flip(X))) &   \
  27.332 -\  (! Y. equal(domain_of(flip(cross_product(Y::'a,universal_class))),inverse(Y))) & \
  27.333 -\  (! Z. equal(domain_of(inverse(Z)),range_of(Z))) &    \
  27.334 +\  (! Y. equal(domain_of(flip(cross_product(Y::'a,universal_class))),INVERSE(Y))) & \
  27.335 +\  (! Z. equal(domain_of(INVERSE(Z)),range_of(Z))) &    \
  27.336  \  (! Z X Y. equal(first(not_subclass_element(restrct(Z::'a,X,singleton(Y)),null_class)),domain(Z::'a,X,Y))) & \
  27.337  \  (! Z X Y. equal(second(not_subclass_element(restrct(Z::'a,singleton(X),Y),null_class)),rng(Z::'a,X,Y))) & \
  27.338  \  (! Xr X. equal(range_of(restrct(Xr::'a,X,universal_class)),image_(Xr::'a,X))) &      \
  27.339 @@ -1686,11 +1691,11 @@
  27.340  \  (! Yr Xr. subclass(compos(Yr::'a,Xr),cross_product(universal_class::'a,universal_class))) & \
  27.341  \  (! Z Yr Xr Y. member(ordered_pair(Y::'a,Z),compos(Yr::'a,Xr)) --> member(Z::'a,image_(Yr::'a,image_(Xr::'a,singleton(Y))))) &     \
  27.342  \  (! Y Z Yr Xr. member(Z::'a,image_(Yr::'a,image_(Xr::'a,singleton(Y)))) & member(ordered_pair(Y::'a,Z),cross_product(universal_class::'a,universal_class)) --> member(ordered_pair(Y::'a,Z),compos(Yr::'a,Xr))) &  \
  27.343 -\  (! X. single_valued_class(X) --> subclass(compos(X::'a,inverse(X)),identity_relation)) &        \
  27.344 -\  (! X. subclass(compos(X::'a,inverse(X)),identity_relation) --> single_valued_class(X)) &        \
  27.345 +\  (! X. single_valued_class(X) --> subclass(compos(X::'a,INVERSE(X)),identity_relation)) &        \
  27.346 +\  (! X. subclass(compos(X::'a,INVERSE(X)),identity_relation) --> single_valued_class(X)) &        \
  27.347  \  (! Xf. function(Xf) --> subclass(Xf::'a,cross_product(universal_class::'a,universal_class))) &       \
  27.348 -\  (! Xf. function(Xf) --> subclass(compos(Xf::'a,inverse(Xf)),identity_relation)) &       \
  27.349 -\  (! Xf. subclass(Xf::'a,cross_product(universal_class::'a,universal_class)) & subclass(compos(Xf::'a,inverse(Xf)),identity_relation) --> function(Xf)) & \
  27.350 +\  (! Xf. function(Xf) --> subclass(compos(Xf::'a,INVERSE(Xf)),identity_relation)) &       \
  27.351 +\  (! Xf. subclass(Xf::'a,cross_product(universal_class::'a,universal_class)) & subclass(compos(Xf::'a,INVERSE(Xf)),identity_relation) --> function(Xf)) & \
  27.352  \  (! Xf X. function(Xf) & member(X::'a,universal_class) --> member(image_(Xf::'a,X),universal_class)) & \
  27.353  \  (! X. equal(X::'a,null_class) | member(regular(X),X)) & \
  27.354  \  (! X. equal(X::'a,null_class) | equal(intersection(X::'a,regular(X)),null_class)) & \
  27.355 @@ -1698,12 +1703,12 @@
  27.356  \  (function(choice)) & \
  27.357  \  (! Y. member(Y::'a,universal_class) --> equal(Y::'a,null_class) | member(apply(choice::'a,Y),Y)) &      \
  27.358  \  (! Xf. one_to_one(Xf) --> function(Xf)) &    \
  27.359 -\  (! Xf. one_to_one(Xf) --> function(inverse(Xf))) &   \
  27.360 -\  (! Xf. function(inverse(Xf)) & function(Xf) --> one_to_one(Xf)) &    \
  27.361 -\  (equal(intersection(cross_product(universal_class::'a,universal_class),intersection(cross_product(universal_class::'a,universal_class),complement(compos(complement(element_relation),inverse(element_relation))))),subset_relation)) &     \
  27.362 -\  (equal(intersection(inverse(subset_relation),subset_relation),identity_relation)) &  \
  27.363 +\  (! Xf. one_to_one(Xf) --> function(INVERSE(Xf))) &   \
  27.364 +\  (! Xf. function(INVERSE(Xf)) & function(Xf) --> one_to_one(Xf)) &    \
  27.365 +\  (equal(intersection(cross_product(universal_class::'a,universal_class),intersection(cross_product(universal_class::'a,universal_class),complement(compos(complement(element_relation),INVERSE(element_relation))))),subset_relation)) &     \
  27.366 +\  (equal(intersection(INVERSE(subset_relation),subset_relation),identity_relation)) &  \
  27.367  \  (! Xr. equal(complement(domain_of(intersection(Xr::'a,identity_relation))),diagonalise(Xr))) &   \
  27.368 -\  (! X. equal(intersection(domain_of(X),diagonalise(compos(inverse(element_relation),X))),cantor(X))) &       \
  27.369 +\  (! X. equal(intersection(domain_of(X),diagonalise(compos(INVERSE(element_relation),X))),cantor(X))) &       \
  27.370  \  (! Xf. operation(Xf) --> function(Xf)) &     \
  27.371  \  (! Xf. operation(Xf) --> equal(cross_product(domain_of(domain_of(Xf)),domain_of(domain_of(Xf))),domain_of(Xf))) &    \
  27.372  \  (! Xf. operation(Xf) --> subclass(range_of(Xf),domain_of(domain_of(Xf)))) &  \
  27.373 @@ -1739,7 +1744,7 @@
  27.374  \  (! C2 E2 D2. equal(C2::'a,D2) --> equal(image_(E2::'a,C2),image_(E2::'a,D2))) &    \
  27.375  \  (! F2 G2 H2. equal(F2::'a,G2) --> equal(intersection(F2::'a,H2),intersection(G2::'a,H2))) &      \
  27.376  \  (! I2 K2 J2. equal(I2::'a,J2) --> equal(intersection(K2::'a,I2),intersection(K2::'a,J2))) &      \
  27.377 -\  (! L2 M2. equal(L2::'a,M2) --> equal(inverse(L2),inverse(M2))) & \
  27.378 +\  (! L2 M2. equal(L2::'a,M2) --> equal(INVERSE(L2),INVERSE(M2))) & \
  27.379  \  (! N2 O2 P2 Q2. equal(N2::'a,O2) --> equal(not_homomorphism1(N2::'a,P2,Q2),not_homomorphism1(O2::'a,P2,Q2))) &   \
  27.380  \  (! R2 T2 S2 U2. equal(R2::'a,S2) --> equal(not_homomorphism1(T2::'a,R2,U2),not_homomorphism1(T2::'a,S2,U2))) &   \
  27.381  \  (! V2 X2 Y2 W2. equal(V2::'a,W2) --> equal(not_homomorphism1(X2::'a,Y2,V2),not_homomorphism1(X2::'a,Y2,W2))) &   \
  27.382 @@ -1792,9 +1797,9 @@
  27.383  \  (subclass(domain_relation::'a,cross_product(universal_class::'a,universal_class))) & \
  27.384  \  (! X Y. member(ordered_pair(X::'a,Y),domain_relation) --> equal(domain_of(X),Y)) &       \
  27.385  \  (! X. member(X::'a,universal_class) --> member(ordered_pair(X::'a,domain_of(X)),domain_relation)) &  \
  27.386 -\  (! X. equal(first(not_subclass_element(compos(X::'a,inverse(X)),identity_relation)),single_valued1(X))) &       \
  27.387 -\  (! X. equal(second(not_subclass_element(compos(X::'a,inverse(X)),identity_relation)),single_valued2(X))) &      \
  27.388 -\  (! X. equal(domain(X::'a,image_(inverse(X),singleton(single_valued1(X))),single_valued2(X)),single_valued3(X))) & \
  27.389 +\  (! X. equal(first(not_subclass_element(compos(X::'a,INVERSE(X)),identity_relation)),single_valued1(X))) &       \
  27.390 +\  (! X. equal(second(not_subclass_element(compos(X::'a,INVERSE(X)),identity_relation)),single_valued2(X))) &      \
  27.391 +\  (! X. equal(domain(X::'a,image_(INVERSE(X),singleton(single_valued1(X))),single_valued2(X)),single_valued3(X))) & \
  27.392  \  (equal(intersection(complement(compos(element_relation::'a,complement(identity_relation))),element_relation),singleton_relation)) &     \
  27.393  \  (subclass(application_function::'a,cross_product(universal_class::'a,cross_product(universal_class::'a,universal_class)))) &     \
  27.394  \  (! Z Y X. member(ordered_pair(X::'a,ordered_pair(Y::'a,Z)),application_function) --> member(Y::'a,domain_of(X))) &       \
  27.395 @@ -1811,15 +1816,15 @@
  27.396  \  (! X2 Y2 Z2 A3. equal(X2::'a,Y2) & maps(X2::'a,Z2,A3) --> maps(Y2::'a,Z2,A3)) &  \
  27.397  \  (! B3 D3 C3 E3. equal(B3::'a,C3) & maps(D3::'a,B3,E3) --> maps(D3::'a,C3,E3)) &  \
  27.398  \  (! F3 H3 I3 G3. equal(F3::'a,G3) & maps(H3::'a,I3,F3) --> maps(H3::'a,I3,G3)) &  \
  27.399 -\  (! X. equal(union(X::'a,inverse(X)),symmetrization_of(X))) &     \
  27.400 +\  (! X. equal(union(X::'a,INVERSE(X)),symmetrization_of(X))) &     \
  27.401  \  (! X Y. irreflexive(X::'a,Y) --> subclass(restrct(X::'a,Y,Y),complement(identity_relation))) &      \
  27.402  \  (! X Y. subclass(restrct(X::'a,Y,Y),complement(identity_relation)) --> irreflexive(X::'a,Y)) &      \
  27.403  \  (! Y X. connected(X::'a,Y) --> subclass(cross_product(Y::'a,Y),union(identity_relation::'a,symmetrization_of(X)))) &     \
  27.404  \  (! X Y. subclass(cross_product(Y::'a,Y),union(identity_relation::'a,symmetrization_of(X))) --> connected(X::'a,Y)) &     \
  27.405  \  (! Xr Y. transitive(Xr::'a,Y) --> subclass(compos(restrct(Xr::'a,Y,Y),restrct(Xr::'a,Y,Y)),restrct(Xr::'a,Y,Y))) &       \
  27.406  \  (! Xr Y. subclass(compos(restrct(Xr::'a,Y,Y),restrct(Xr::'a,Y,Y)),restrct(Xr::'a,Y,Y)) --> transitive(Xr::'a,Y)) &       \
  27.407 -\  (! Xr Y. asymmetric(Xr::'a,Y) --> equal(restrct(intersection(Xr::'a,inverse(Xr)),Y,Y),null_class)) &        \
  27.408 -\  (! Xr Y. equal(restrct(intersection(Xr::'a,inverse(Xr)),Y,Y),null_class) --> asymmetric(Xr::'a,Y)) &        \
  27.409 +\  (! Xr Y. asymmetric(Xr::'a,Y) --> equal(restrct(intersection(Xr::'a,INVERSE(Xr)),Y,Y),null_class)) &        \
  27.410 +\  (! Xr Y. equal(restrct(intersection(Xr::'a,INVERSE(Xr)),Y,Y),null_class) --> asymmetric(Xr::'a,Y)) &        \
  27.411  \  (! Xr Y Z. equal(segment(Xr::'a,Y,Z),domain_of(restrct(Xr::'a,Y,singleton(Z))))) &  \
  27.412  \  (! X Y. well_ordering(X::'a,Y) --> connected(X::'a,Y)) &     \
  27.413  \  (! Y Xr U. well_ordering(Xr::'a,Y) & subclass(U::'a,Y) --> equal(U::'a,null_class) | member(least(Xr::'a,U),U)) &   \
  27.414 @@ -1934,8 +1939,8 @@
  27.415  \  (! X. subclass(flip(X),cross_product(cross_product(universal_class::'a,universal_class),universal_class))) &     \
  27.416  \  (! V U W X. member(ordered_pair(ordered_pair(U::'a,V),W),flip(X)) --> member(ordered_pair(ordered_pair(V::'a,U),W),X)) &     \
  27.417  \  (! U V W X. member(ordered_pair(ordered_pair(V::'a,U),W),X) & member(ordered_pair(ordered_pair(U::'a,V),W),cross_product(cross_product(universal_class::'a,universal_class),universal_class)) --> member(ordered_pair(ordered_pair(U::'a,V),W),flip(X))) &   \
  27.418 -\  (! Y. equal(domain_of(flip(cross_product(Y::'a,universal_class))),inverse(Y))) & \
  27.419 -\  (! Z. equal(domain_of(inverse(Z)),range_of(Z))) &    \
  27.420 +\  (! Y. equal(domain_of(flip(cross_product(Y::'a,universal_class))),INVERSE(Y))) & \
  27.421 +\  (! Z. equal(domain_of(INVERSE(Z)),range_of(Z))) &    \
  27.422  \  (! Z X Y. equal(first(not_subclass_element(restrct(Z::'a,X,singleton(Y)),null_class)),domain(Z::'a,X,Y))) & \
  27.423  \  (! Z X Y. equal(second(not_subclass_element(restrct(Z::'a,singleton(X),Y),null_class)),rng(Z::'a,X,Y))) & \
  27.424  \  (! Xr X. equal(range_of(restrct(Xr::'a,X,universal_class)),image_(Xr::'a,X))) &      \
  27.425 @@ -1956,11 +1961,11 @@
  27.426  \  (! Yr Xr. subclass(compos(Yr::'a,Xr),cross_product(universal_class::'a,universal_class))) & \
  27.427  \  (! Z Yr Xr Y. member(ordered_pair(Y::'a,Z),compos(Yr::'a,Xr)) --> member(Z::'a,image_(Yr::'a,image_(Xr::'a,singleton(Y))))) &     \
  27.428  \  (! Y Z Yr Xr. member(Z::'a,image_(Yr::'a,image_(Xr::'a,singleton(Y)))) & member(ordered_pair(Y::'a,Z),cross_product(universal_class::'a,universal_class)) --> member(ordered_pair(Y::'a,Z),compos(Yr::'a,Xr))) &  \
  27.429 -\  (! X. single_valued_class(X) --> subclass(compos(X::'a,inverse(X)),identity_relation)) &        \
  27.430 -\  (! X. subclass(compos(X::'a,inverse(X)),identity_relation) --> single_valued_class(X)) &        \
  27.431 +\  (! X. single_valued_class(X) --> subclass(compos(X::'a,INVERSE(X)),identity_relation)) &        \
  27.432 +\  (! X. subclass(compos(X::'a,INVERSE(X)),identity_relation) --> single_valued_class(X)) &        \
  27.433  \  (! Xf. function(Xf) --> subclass(Xf::'a,cross_product(universal_class::'a,universal_class))) &       \
  27.434 -\  (! Xf. function(Xf) --> subclass(compos(Xf::'a,inverse(Xf)),identity_relation)) &       \
  27.435 -\  (! Xf. subclass(Xf::'a,cross_product(universal_class::'a,universal_class)) & subclass(compos(Xf::'a,inverse(Xf)),identity_relation) --> function(Xf)) & \
  27.436 +\  (! Xf. function(Xf) --> subclass(compos(Xf::'a,INVERSE(Xf)),identity_relation)) &       \
  27.437 +\  (! Xf. subclass(Xf::'a,cross_product(universal_class::'a,universal_class)) & subclass(compos(Xf::'a,INVERSE(Xf)),identity_relation) --> function(Xf)) & \
  27.438  \  (! Xf X. function(Xf) & member(X::'a,universal_class) --> member(image_(Xf::'a,X),universal_class)) & \
  27.439  \  (! X. equal(X::'a,null_class) | member(regular(X),X)) & \
  27.440  \  (! X. equal(X::'a,null_class) | equal(intersection(X::'a,regular(X)),null_class)) & \
  27.441 @@ -1968,12 +1973,12 @@
  27.442  \  (function(choice)) & \
  27.443  \  (! Y. member(Y::'a,universal_class) --> equal(Y::'a,null_class) | member(apply(choice::'a,Y),Y)) &      \
  27.444  \  (! Xf. one_to_one(Xf) --> function(Xf)) &    \
  27.445 -\  (! Xf. one_to_one(Xf) --> function(inverse(Xf))) &   \
  27.446 -\  (! Xf. function(inverse(Xf)) & function(Xf) --> one_to_one(Xf)) &    \
  27.447 -\  (equal(intersection(cross_product(universal_class::'a,universal_class),intersection(cross_product(universal_class::'a,universal_class),complement(compos(complement(element_relation),inverse(element_relation))))),subset_relation)) &     \
  27.448 -\  (equal(intersection(inverse(subset_relation),subset_relation),identity_relation)) &  \
  27.449 +\  (! Xf. one_to_one(Xf) --> function(INVERSE(Xf))) &   \
  27.450 +\  (! Xf. function(INVERSE(Xf)) & function(Xf) --> one_to_one(Xf)) &    \
  27.451 +\  (equal(intersection(cross_product(universal_class::'a,universal_class),intersection(cross_product(universal_class::'a,universal_class),complement(compos(complement(element_relation),INVERSE(element_relation))))),subset_relation)) &     \
  27.452 +\  (equal(intersection(INVERSE(subset_relation),subset_relation),identity_relation)) &  \
  27.453  \  (! Xr. equal(complement(domain_of(intersection(Xr::'a,identity_relation))),diagonalise(Xr))) &   \
  27.454 -\  (! X. equal(intersection(domain_of(X),diagonalise(compos(inverse(element_relation),X))),cantor(X))) &       \
  27.455 +\  (! X. equal(intersection(domain_of(X),diagonalise(compos(INVERSE(element_relation),X))),cantor(X))) &       \
  27.456  \  (! Xf. operation(Xf) --> function(Xf)) &     \
  27.457  \  (! Xf. operation(Xf) --> equal(cross_product(domain_of(domain_of(Xf)),domain_of(domain_of(Xf))),domain_of(Xf))) &    \
  27.458  \  (! Xf. operation(Xf) --> subclass(range_of(Xf),domain_of(domain_of(Xf)))) &  \
  27.459 @@ -2009,7 +2014,7 @@
  27.460  \  (! C2 E2 D2. equal(C2::'a,D2) --> equal(image_(E2::'a,C2),image_(E2::'a,D2))) &    \
  27.461  \  (! F2 G2 H2. equal(F2::'a,G2) --> equal(intersection(F2::'a,H2),intersection(G2::'a,H2))) &      \
  27.462  \  (! I2 K2 J2. equal(I2::'a,J2) --> equal(intersection(K2::'a,I2),intersection(K2::'a,J2))) &      \
  27.463 -\  (! L2 M2. equal(L2::'a,M2) --> equal(inverse(L2),inverse(M2))) & \
  27.464 +\  (! L2 M2. equal(L2::'a,M2) --> equal(INVERSE(L2),INVERSE(M2))) & \
  27.465  \  (! N2 O2 P2 Q2. equal(N2::'a,O2) --> equal(not_homomorphism1(N2::'a,P2,Q2),not_homomorphism1(O2::'a,P2,Q2))) &   \
  27.466  \  (! R2 T2 S2 U2. equal(R2::'a,S2) --> equal(not_homomorphism1(T2::'a,R2,U2),not_homomorphism1(T2::'a,S2,U2))) &   \
  27.467  \  (! V2 X2 Y2 W2. equal(V2::'a,W2) --> equal(not_homomorphism1(X2::'a,Y2,V2),not_homomorphism1(X2::'a,Y2,W2))) &   \
  27.468 @@ -2062,9 +2067,9 @@
  27.469  \  (subclass(domain_relation::'a,cross_product(universal_class::'a,universal_class))) & \
  27.470  \  (! X Y. member(ordered_pair(X::'a,Y),domain_relation) --> equal(domain_of(X),Y)) &       \
  27.471  \  (! X. member(X::'a,universal_class) --> member(ordered_pair(X::'a,domain_of(X)),domain_relation)) &  \
  27.472 -\  (! X. equal(first(not_subclass_element(compos(X::'a,inverse(X)),identity_relation)),single_valued1(X))) &       \
  27.473 -\  (! X. equal(second(not_subclass_element(compos(X::'a,inverse(X)),identity_relation)),single_valued2(X))) &      \
  27.474 -\  (! X. equal(domain(X::'a,image_(inverse(X),singleton(single_valued1(X))),single_valued2(X)),single_valued3(X))) & \
  27.475 +\  (! X. equal(first(not_subclass_element(compos(X::'a,INVERSE(X)),identity_relation)),single_valued1(X))) &       \
  27.476 +\  (! X. equal(second(not_subclass_element(compos(X::'a,INVERSE(X)),identity_relation)),single_valued2(X))) &      \
  27.477 +\  (! X. equal(domain(X::'a,image_(INVERSE(X),singleton(single_valued1(X))),single_valued2(X)),single_valued3(X))) & \
  27.478  \  (equal(intersection(complement(compos(element_relation::'a,complement(identity_relation))),element_relation),singleton_relation)) &     \
  27.479  \  (subclass(application_function::'a,cross_product(universal_class::'a,cross_product(universal_class::'a,universal_class)))) &     \
  27.480  \  (! Z Y X. member(ordered_pair(X::'a,ordered_pair(Y::'a,Z)),application_function) --> member(Y::'a,domain_of(X))) &       \
  27.481 @@ -2081,15 +2086,15 @@
  27.482  \  (! X2 Y2 Z2 A3. equal(X2::'a,Y2) & maps(X2::'a,Z2,A3) --> maps(Y2::'a,Z2,A3)) &  \
  27.483  \  (! B3 D3 C3 E3. equal(B3::'a,C3) & maps(D3::'a,B3,E3) --> maps(D3::'a,C3,E3)) &  \
  27.484  \  (! F3 H3 I3 G3. equal(F3::'a,G3) & maps(H3::'a,I3,F3) --> maps(H3::'a,I3,G3)) &  \
  27.485 -\  (! X. equal(union(X::'a,inverse(X)),symmetrization_of(X))) &     \
  27.486 +\  (! X. equal(union(X::'a,INVERSE(X)),symmetrization_of(X))) &     \
  27.487  \  (! X Y. irreflexive(X::'a,Y) --> subclass(restrct(X::'a,Y,Y),complement(identity_relation))) &      \
  27.488  \  (! X Y. subclass(restrct(X::'a,Y,Y),complement(identity_relation)) --> irreflexive(X::'a,Y)) &      \
  27.489  \  (! Y X. connected(X::'a,Y) --> subclass(cross_product(Y::'a,Y),union(identity_relation::'a,symmetrization_of(X)))) &     \
  27.490  \  (! X Y. subclass(cross_product(Y::'a,Y),union(identity_relation::'a,symmetrization_of(X))) --> connected(X::'a,Y)) &     \
  27.491  \  (! Xr Y. transitive(Xr::'a,Y) --> subclass(compos(restrct(Xr::'a,Y,Y),restrct(Xr::'a,Y,Y)),restrct(Xr::'a,Y,Y))) &       \
  27.492  \  (! Xr Y. subclass(compos(restrct(Xr::'a,Y,Y),restrct(Xr::'a,Y,Y)),restrct(Xr::'a,Y,Y)) --> transitive(Xr::'a,Y)) &       \
  27.493 -\  (! Xr Y. asymmetric(Xr::'a,Y) --> equal(restrct(intersection(Xr::'a,inverse(Xr)),Y,Y),null_class)) &        \
  27.494 -\  (! Xr Y. equal(restrct(intersection(Xr::'a,inverse(Xr)),Y,Y),null_class) --> asymmetric(Xr::'a,Y)) &        \
  27.495 +\  (! Xr Y. asymmetric(Xr::'a,Y) --> equal(restrct(intersection(Xr::'a,INVERSE(Xr)),Y,Y),null_class)) &        \
  27.496 +\  (! Xr Y. equal(restrct(intersection(Xr::'a,INVERSE(Xr)),Y,Y),null_class) --> asymmetric(Xr::'a,Y)) &        \
  27.497  \  (! Xr Y Z. equal(segment(Xr::'a,Y,Z),domain_of(restrct(Xr::'a,Y,singleton(Z))))) &  \
  27.498  \  (! X Y. well_ordering(X::'a,Y) --> connected(X::'a,Y)) &     \
  27.499  \  (! Y Xr U. well_ordering(Xr::'a,Y) & subclass(U::'a,Y) --> equal(U::'a,null_class) | member(least(Xr::'a,U),U)) &   \
  27.500 @@ -2187,11 +2192,11 @@
  27.501  (*190 inferences so far.  Searching to depth 10.  0.6 secs*)
  27.502  val PLA006_1 = prove
  27.503   ("(! X Y State. holds(X::'a,State) & holds(Y::'a,State) --> holds(and'(X::'a,Y),State)) &  \
  27.504 -\  (! State X. holds(empty::'a,State) & holds(clear(X),State) & differ(X::'a,table) --> holds(holding(X),do(pickup(X),State))) &        \
  27.505 -\  (! Y X State. holds(on(X::'a,Y),State) & holds(clear(X),State) & holds(empty::'a,State) --> holds(clear(Y),do(pickup(X),State))) &   \
  27.506 +\  (! State X. holds(EMPTY::'a,State) & holds(clear(X),State) & differ(X::'a,table) --> holds(holding(X),do(pickup(X),State))) &        \
  27.507 +\  (! Y X State. holds(on(X::'a,Y),State) & holds(clear(X),State) & holds(EMPTY::'a,State) --> holds(clear(Y),do(pickup(X),State))) &   \
  27.508  \  (! Y State X Z. holds(on(X::'a,Y),State) & differ(X::'a,Z) --> holds(on(X::'a,Y),do(pickup(Z),State))) & \
  27.509  \  (! State X Z. holds(clear(X),State) & differ(X::'a,Z) --> holds(clear(X),do(pickup(Z),State))) & \
  27.510 -\  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(empty::'a,do(putdown(X::'a,Y),State))) &     \
  27.511 +\  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(EMPTY::'a,do(putdown(X::'a,Y),State))) &     \
  27.512  \  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(on(X::'a,Y),do(putdown(X::'a,Y),State))) &   \
  27.513  \  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(clear(X),do(putdown(X::'a,Y),State))) &  \
  27.514  \  (! Z W X Y State. holds(on(X::'a,Y),State) --> holds(on(X::'a,Y),do(putdown(Z::'a,W),State))) &  \
  27.515 @@ -2214,7 +2219,7 @@
  27.516  \  (holds(clear(a),s0)) &       \
  27.517  \  (holds(clear(b),s0)) &       \
  27.518  \  (holds(clear(c),s0)) &       \
  27.519 -\  (holds(empty::'a,s0)) &  \
  27.520 +\  (holds(EMPTY::'a,s0)) &  \
  27.521  \  (! State. holds(clear(table),State)) &       \
  27.522  \  (! State. ~holds(on(c::'a,table),State)) --> False",
  27.523    meson_tac 1);
  27.524 @@ -2222,11 +2227,11 @@
  27.525  (*190 inferences so far.  Searching to depth 10.  0.5 secs*)
  27.526  val PLA017_1 = prove
  27.527   ("(! X Y State. holds(X::'a,State) & holds(Y::'a,State) --> holds(and'(X::'a,Y),State)) &  \
  27.528 -\  (! State X. holds(empty::'a,State) & holds(clear(X),State) & differ(X::'a,table) --> holds(holding(X),do(pickup(X),State))) &        \
  27.529 -\  (! Y X State. holds(on(X::'a,Y),State) & holds(clear(X),State) & holds(empty::'a,State) --> holds(clear(Y),do(pickup(X),State))) &   \
  27.530 +\  (! State X. holds(EMPTY::'a,State) & holds(clear(X),State) & differ(X::'a,table) --> holds(holding(X),do(pickup(X),State))) &        \
  27.531 +\  (! Y X State. holds(on(X::'a,Y),State) & holds(clear(X),State) & holds(EMPTY::'a,State) --> holds(clear(Y),do(pickup(X),State))) &   \
  27.532  \  (! Y State X Z. holds(on(X::'a,Y),State) & differ(X::'a,Z) --> holds(on(X::'a,Y),do(pickup(Z),State))) & \
  27.533  \  (! State X Z. holds(clear(X),State) & differ(X::'a,Z) --> holds(clear(X),do(pickup(Z),State))) & \
  27.534 -\  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(empty::'a,do(putdown(X::'a,Y),State))) &     \
  27.535 +\  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(EMPTY::'a,do(putdown(X::'a,Y),State))) &     \
  27.536  \  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(on(X::'a,Y),do(putdown(X::'a,Y),State))) &   \
  27.537  \  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(clear(X),do(putdown(X::'a,Y),State))) &  \
  27.538  \  (! Z W X Y State. holds(on(X::'a,Y),State) --> holds(on(X::'a,Y),do(putdown(Z::'a,W),State))) &  \
  27.539 @@ -2249,7 +2254,7 @@
  27.540  \  (holds(clear(a),s0)) &       \
  27.541  \  (holds(clear(b),s0)) &       \
  27.542  \  (holds(clear(c),s0)) &       \
  27.543 -\  (holds(empty::'a,s0)) &  \
  27.544 +\  (holds(EMPTY::'a,s0)) &  \
  27.545  \  (! State. holds(clear(table),State)) &       \
  27.546  \  (! State. ~holds(on(a::'a,c),State)) --> False",
  27.547    meson_tac 1);
  27.548 @@ -2257,11 +2262,11 @@
  27.549  (*13732 inferences so far.  Searching to depth 16.  9.8 secs*)
  27.550  val PLA022_1 = prove_hard
  27.551   ("(! X Y State. holds(X::'a,State) & holds(Y::'a,State) --> holds(and'(X::'a,Y),State)) &  \
  27.552 -\  (! State X. holds(empty::'a,State) & holds(clear(X),State) & differ(X::'a,table) --> holds(holding(X),do(pickup(X),State))) &        \
  27.553 -\  (! Y X State. holds(on(X::'a,Y),State) & holds(clear(X),State) & holds(empty::'a,State) --> holds(clear(Y),do(pickup(X),State))) &   \
  27.554 +\  (! State X. holds(EMPTY::'a,State) & holds(clear(X),State) & differ(X::'a,table) --> holds(holding(X),do(pickup(X),State))) &        \
  27.555 +\  (! Y X State. holds(on(X::'a,Y),State) & holds(clear(X),State) & holds(EMPTY::'a,State) --> holds(clear(Y),do(pickup(X),State))) &   \
  27.556  \  (! Y State X Z. holds(on(X::'a,Y),State) & differ(X::'a,Z) --> holds(on(X::'a,Y),do(pickup(Z),State))) & \
  27.557  \  (! State X Z. holds(clear(X),State) & differ(X::'a,Z) --> holds(clear(X),do(pickup(Z),State))) & \
  27.558 -\  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(empty::'a,do(putdown(X::'a,Y),State))) &     \
  27.559 +\  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(EMPTY::'a,do(putdown(X::'a,Y),State))) &     \
  27.560  \  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(on(X::'a,Y),do(putdown(X::'a,Y),State))) &   \
  27.561  \  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(clear(X),do(putdown(X::'a,Y),State))) &  \
  27.562  \  (! Z W X Y State. holds(on(X::'a,Y),State) --> holds(on(X::'a,Y),do(putdown(Z::'a,W),State))) &  \
  27.563 @@ -2284,7 +2289,7 @@
  27.564  \  (holds(clear(a),s0)) &       \
  27.565  \  (holds(clear(b),s0)) &       \
  27.566  \  (holds(clear(c),s0)) &       \
  27.567 -\  (holds(empty::'a,s0)) &  \
  27.568 +\  (holds(EMPTY::'a,s0)) &  \
  27.569  \  (! State. holds(clear(table),State)) &       \
  27.570  \  (! State. ~holds(and'(on(c::'a,d),on(a::'a,c)),State)) --> False",
  27.571    meson_tac 1);
  27.572 @@ -2292,11 +2297,11 @@
  27.573  (*217 inferences so far.  Searching to depth 13.  0.7 secs*)
  27.574  val PLA022_2 = prove
  27.575   ("(! X Y State. holds(X::'a,State) & holds(Y::'a,State) --> holds(and'(X::'a,Y),State)) &  \
  27.576 -\  (! State X. holds(empty::'a,State) & holds(clear(X),State) & differ(X::'a,table) --> holds(holding(X),do(pickup(X),State))) &        \
  27.577 -\  (! Y X State. holds(on(X::'a,Y),State) & holds(clear(X),State) & holds(empty::'a,State) --> holds(clear(Y),do(pickup(X),State))) &   \
  27.578 +\  (! State X. holds(EMPTY::'a,State) & holds(clear(X),State) & differ(X::'a,table) --> holds(holding(X),do(pickup(X),State))) &        \
  27.579 +\  (! Y X State. holds(on(X::'a,Y),State) & holds(clear(X),State) & holds(EMPTY::'a,State) --> holds(clear(Y),do(pickup(X),State))) &   \
  27.580  \  (! Y State X Z. holds(on(X::'a,Y),State) & differ(X::'a,Z) --> holds(on(X::'a,Y),do(pickup(Z),State))) & \
  27.581  \  (! State X Z. holds(clear(X),State) & differ(X::'a,Z) --> holds(clear(X),do(pickup(Z),State))) & \
  27.582 -\  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(empty::'a,do(putdown(X::'a,Y),State))) &     \
  27.583 +\  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(EMPTY::'a,do(putdown(X::'a,Y),State))) &     \
  27.584  \  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(on(X::'a,Y),do(putdown(X::'a,Y),State))) &   \
  27.585  \  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(clear(X),do(putdown(X::'a,Y),State))) &  \
  27.586  \  (! Z W X Y State. holds(on(X::'a,Y),State) --> holds(on(X::'a,Y),do(putdown(Z::'a,W),State))) &  \
  27.587 @@ -2319,7 +2324,7 @@
  27.588  \  (holds(clear(a),s0)) &       \
  27.589  \  (holds(clear(b),s0)) &       \
  27.590  \  (holds(clear(c),s0)) &       \
  27.591 -\  (holds(empty::'a,s0)) &  \
  27.592 +\  (holds(EMPTY::'a,s0)) &  \
  27.593  \  (! State. holds(clear(table),State)) &       \
  27.594  \  (! State. ~holds(and'(on(a::'a,c),on(c::'a,d)),State)) --> False",
  27.595    meson_tac 1);
  27.596 @@ -2351,26 +2356,26 @@
  27.597  \  (! X. equal(successor(predecessor(X)),X)) &  \
  27.598  \  (! X Y. equal(predecessor(X),predecessor(Y)) --> equal(X::'a,Y)) &       \
  27.599  \  (! X Y. equal(successor(X),successor(Y)) --> equal(X::'a,Y)) &   \
  27.600 -\  (! X. less_than(predecessor(X),X)) & \
  27.601 -\  (! X. less_than(X::'a,successor(X))) &   \
  27.602 -\  (! X Y Z. less_than(X::'a,Y) & less_than(Y::'a,Z) --> less_than(X::'a,Z)) &      \
  27.603 -\  (! X Y. less_than(X::'a,Y) | less_than(Y::'a,X) | equal(X::'a,Y)) &    \
  27.604 -\  (! X. ~less_than(X::'a,X)) &     \
  27.605 -\  (! Y X. ~(less_than(X::'a,Y) & less_than(Y::'a,X))) &        \
  27.606 -\  (! Y X Z. equal(X::'a,Y) & less_than(X::'a,Z) --> less_than(Y::'a,Z)) &  \
  27.607 -\  (! Y Z X. equal(X::'a,Y) & less_than(Z::'a,X) --> less_than(Z::'a,Y)) &  \
  27.608 +\  (! X. LESS_THAN(predecessor(X),X)) & \
  27.609 +\  (! X. LESS_THAN(X::'a,successor(X))) &   \
  27.610 +\  (! X Y Z. LESS_THAN(X::'a,Y) & LESS_THAN(Y::'a,Z) --> LESS_THAN(X::'a,Z)) &      \
  27.611 +\  (! X Y. LESS_THAN(X::'a,Y) | LESS_THAN(Y::'a,X) | equal(X::'a,Y)) &    \
  27.612 +\  (! X. ~LESS_THAN(X::'a,X)) &     \
  27.613 +\  (! Y X. ~(LESS_THAN(X::'a,Y) & LESS_THAN(Y::'a,X))) &        \
  27.614 +\  (! Y X Z. equal(X::'a,Y) & LESS_THAN(X::'a,Z) --> LESS_THAN(Y::'a,Z)) &  \
  27.615 +\  (! Y Z X. equal(X::'a,Y) & LESS_THAN(Z::'a,X) --> LESS_THAN(Z::'a,Y)) &  \
  27.616  \  (! X Y. equal(X::'a,Y) --> equal(predecessor(X),predecessor(Y))) &       \
  27.617  \  (! X Y. equal(X::'a,Y) --> equal(successor(X),successor(Y))) &   \
  27.618  \  (! X Y. equal(X::'a,Y) --> equal(a(X),a(Y))) &   \
  27.619 -\  (~less_than(n::'a,j)) &  \
  27.620 -\  (less_than(k::'a,j)) &   \
  27.621 -\  (~less_than(k::'a,i)) &  \
  27.622 -\  (less_than(i::'a,n)) &   \
  27.623 -\  (less_than(a(j),a(k))) &     \
  27.624 -\  (! X. less_than(X::'a,j) & less_than(a(X),a(k)) --> less_than(X::'a,i)) &    \
  27.625 -\  (! X. less_than(one::'a,i) & less_than(a(X),a(predecessor(i))) --> less_than(X::'a,i) | less_than(n::'a,X)) &   \
  27.626 -\  (! X. ~(less_than(one::'a,X) & less_than(X::'a,i) & less_than(a(X),a(predecessor(X))))) &    \
  27.627 -\  (less_than(j::'a,i)) --> False",
  27.628 +\  (~LESS_THAN(n::'a,j)) &  \
  27.629 +\  (LESS_THAN(k::'a,j)) &   \
  27.630 +\  (~LESS_THAN(k::'a,i)) &  \
  27.631 +\  (LESS_THAN(i::'a,n)) &   \
  27.632 +\  (LESS_THAN(a(j),a(k))) &     \
  27.633 +\  (! X. LESS_THAN(X::'a,j) & LESS_THAN(a(X),a(k)) --> LESS_THAN(X::'a,i)) &    \
  27.634 +\  (! X. LESS_THAN(one::'a,i) & LESS_THAN(a(X),a(predecessor(i))) --> LESS_THAN(X::'a,i) | LESS_THAN(n::'a,X)) &   \
  27.635 +\  (! X. ~(LESS_THAN(one::'a,X) & LESS_THAN(X::'a,i) & LESS_THAN(a(X),a(predecessor(X))))) &    \
  27.636 +\  (LESS_THAN(j::'a,i)) --> False",
  27.637    meson_tac 1);
  27.638  
  27.639  (*584 inferences so far.  Searching to depth 7.  1.1 secs*)
  27.640 @@ -2382,26 +2387,26 @@
  27.641  \  (! X. equal(successor(predecessor(X)),X)) &  \
  27.642  \  (! X Y. equal(predecessor(X),predecessor(Y)) --> equal(X::'a,Y)) &       \
  27.643  \  (! X Y. equal(successor(X),successor(Y)) --> equal(X::'a,Y)) &   \
  27.644 -\  (! X. less_than(predecessor(X),X)) & \
  27.645 -\  (! X. less_than(X::'a,successor(X))) &   \
  27.646 -\  (! X Y Z. less_than(X::'a,Y) & less_than(Y::'a,Z) --> less_than(X::'a,Z)) &      \
  27.647 -\  (! X Y. less_than(X::'a,Y) | less_than(Y::'a,X) | equal(X::'a,Y)) &    \
  27.648 -\  (! X. ~less_than(X::'a,X)) &     \
  27.649 -\  (! Y X. ~(less_than(X::'a,Y) & less_than(Y::'a,X))) &        \
  27.650 -\  (! Y X Z. equal(X::'a,Y) & less_than(X::'a,Z) --> less_than(Y::'a,Z)) &  \
  27.651 -\  (! Y Z X. equal(X::'a,Y) & less_than(Z::'a,X) --> less_than(Z::'a,Y)) &  \
  27.652 +\  (! X. LESS_THAN(predecessor(X),X)) & \
  27.653 +\  (! X. LESS_THAN(X::'a,successor(X))) &   \
  27.654 +\  (! X Y Z. LESS_THAN(X::'a,Y) & LESS_THAN(Y::'a,Z) --> LESS_THAN(X::'a,Z)) &      \
  27.655 +\  (! X Y. LESS_THAN(X::'a,Y) | LESS_THAN(Y::'a,X) | equal(X::'a,Y)) &    \
  27.656 +\  (! X. ~LESS_THAN(X::'a,X)) &     \
  27.657 +\  (! Y X. ~(LESS_THAN(X::'a,Y) & LESS_THAN(Y::'a,X))) &        \
  27.658 +\  (! Y X Z. equal(X::'a,Y) & LESS_THAN(X::'a,Z) --> LESS_THAN(Y::'a,Z)) &  \
  27.659 +\  (! Y Z X. equal(X::'a,Y) & LESS_THAN(Z::'a,X) --> LESS_THAN(Z::'a,Y)) &  \
  27.660  \  (! X Y. equal(X::'a,Y) --> equal(predecessor(X),predecessor(Y))) &       \
  27.661  \  (! X Y. equal(X::'a,Y) --> equal(successor(X),successor(Y))) &   \
  27.662  \  (! X Y. equal(X::'a,Y) --> equal(a(X),a(Y))) &   \
  27.663 -\  (~less_than(n::'a,k)) &  \
  27.664 -\  (~less_than(k::'a,l)) &  \
  27.665 -\  (~less_than(k::'a,i)) &  \
  27.666 -\  (less_than(l::'a,n)) &   \
  27.667 -\  (less_than(one::'a,l)) & \
  27.668 -\  (less_than(a(k),a(predecessor(l)))) &        \
  27.669 -\  (! X. less_than(X::'a,successor(n)) & less_than(a(X),a(k)) --> less_than(X::'a,l)) & \
  27.670 -\  (! X. less_than(one::'a,l) & less_than(a(X),a(predecessor(l))) --> less_than(X::'a,l) | less_than(n::'a,X)) &   \
  27.671 -\  (! X. ~(less_than(one::'a,X) & less_than(X::'a,l) & less_than(a(X),a(predecessor(X))))) --> False",
  27.672 +\  (~LESS_THAN(n::'a,k)) &  \
  27.673 +\  (~LESS_THAN(k::'a,l)) &  \
  27.674 +\  (~LESS_THAN(k::'a,i)) &  \
  27.675 +\  (LESS_THAN(l::'a,n)) &   \
  27.676 +\  (LESS_THAN(one::'a,l)) & \
  27.677 +\  (LESS_THAN(a(k),a(predecessor(l)))) &        \
  27.678 +\  (! X. LESS_THAN(X::'a,successor(n)) & LESS_THAN(a(X),a(k)) --> LESS_THAN(X::'a,l)) & \
  27.679 +\  (! X. LESS_THAN(one::'a,l) & LESS_THAN(a(X),a(predecessor(l))) --> LESS_THAN(X::'a,l) | LESS_THAN(n::'a,X)) &   \
  27.680 +\  (! X. ~(LESS_THAN(one::'a,X) & LESS_THAN(X::'a,l) & LESS_THAN(a(X),a(predecessor(X))))) --> False",
  27.681    meson_tac 1);
  27.682  
  27.683  (*2343 inferences so far.  Searching to depth 8.  3.5 secs*)
  27.684 @@ -2413,25 +2418,25 @@
  27.685  \  (! X. equal(successor(predecessor(X)),X)) &  \
  27.686  \  (! X Y. equal(predecessor(X),predecessor(Y)) --> equal(X::'a,Y)) &       \
  27.687  \  (! X Y. equal(successor(X),successor(Y)) --> equal(X::'a,Y)) &   \
  27.688 -\  (! X. less_than(predecessor(X),X)) & \
  27.689 -\  (! X. less_than(X::'a,successor(X))) &   \
  27.690 -\  (! X Y Z. less_than(X::'a,Y) & less_than(Y::'a,Z) --> less_than(X::'a,Z)) &      \
  27.691 -\  (! X Y. less_than(X::'a,Y) | less_than(Y::'a,X) | equal(X::'a,Y)) &    \
  27.692 -\  (! X. ~less_than(X::'a,X)) &     \
  27.693 -\  (! Y X. ~(less_than(X::'a,Y) & less_than(Y::'a,X))) &        \
  27.694 -\  (! Y X Z. equal(X::'a,Y) & less_than(X::'a,Z) --> less_than(Y::'a,Z)) &  \
  27.695 -\  (! Y Z X. equal(X::'a,Y) & less_than(Z::'a,X) --> less_than(Z::'a,Y)) &  \
  27.696 +\  (! X. LESS_THAN(predecessor(X),X)) & \
  27.697 +\  (! X. LESS_THAN(X::'a,successor(X))) &   \
  27.698 +\  (! X Y Z. LESS_THAN(X::'a,Y) & LESS_THAN(Y::'a,Z) --> LESS_THAN(X::'a,Z)) &      \
  27.699 +\  (! X Y. LESS_THAN(X::'a,Y) | LESS_THAN(Y::'a,X) | equal(X::'a,Y)) &    \
  27.700 +\  (! X. ~LESS_THAN(X::'a,X)) &     \
  27.701 +\  (! Y X. ~(LESS_THAN(X::'a,Y) & LESS_THAN(Y::'a,X))) &        \
  27.702 +\  (! Y X Z. equal(X::'a,Y) & LESS_THAN(X::'a,Z) --> LESS_THAN(Y::'a,Z)) &  \
  27.703 +\  (! Y Z X. equal(X::'a,Y) & LESS_THAN(Z::'a,X) --> LESS_THAN(Z::'a,Y)) &  \
  27.704  \  (! X Y. equal(X::'a,Y) --> equal(predecessor(X),predecessor(Y))) &       \
  27.705  \  (! X Y. equal(X::'a,Y) --> equal(successor(X),successor(Y))) &   \
  27.706  \  (! X Y. equal(X::'a,Y) --> equal(a(X),a(Y))) &   \
  27.707 -\  (~less_than(n::'a,m)) &  \
  27.708 -\  (less_than(i::'a,m)) &   \
  27.709 -\  (less_than(i::'a,n)) &   \
  27.710 -\  (~less_than(i::'a,one)) &        \
  27.711 -\  (less_than(a(i),a(m))) &     \
  27.712 -\  (! X. less_than(X::'a,successor(n)) & less_than(a(X),a(m)) --> less_than(X::'a,i)) & \
  27.713 -\  (! X. less_than(one::'a,i) & less_than(a(X),a(predecessor(i))) --> less_than(X::'a,i) | less_than(n::'a,X)) &   \
  27.714 -\  (! X. ~(less_than(one::'a,X) & less_than(X::'a,i) & less_than(a(X),a(predecessor(X))))) --> False",
  27.715 +\  (~LESS_THAN(n::'a,m)) &  \
  27.716 +\  (LESS_THAN(i::'a,m)) &   \
  27.717 +\  (LESS_THAN(i::'a,n)) &   \
  27.718 +\  (~LESS_THAN(i::'a,one)) &        \
  27.719 +\  (LESS_THAN(a(i),a(m))) &     \
  27.720 +\  (! X. LESS_THAN(X::'a,successor(n)) & LESS_THAN(a(X),a(m)) --> LESS_THAN(X::'a,i)) & \
  27.721 +\  (! X. LESS_THAN(one::'a,i) & LESS_THAN(a(X),a(predecessor(i))) --> LESS_THAN(X::'a,i) | LESS_THAN(n::'a,X)) &   \
  27.722 +\  (! X. ~(LESS_THAN(one::'a,X) & LESS_THAN(X::'a,i) & LESS_THAN(a(X),a(predecessor(X))))) --> False",
  27.723    meson_tac 1);
  27.724  
  27.725  (*86 inferences so far.  Searching to depth 14.  0.1 secs*)
    28.1 --- a/src/HOL/mono.ML	Tue Jul 24 11:25:54 2001 +0200
    28.2 +++ b/src/HOL/mono.ML	Wed Jul 25 13:13:01 2001 +0200
    28.3 @@ -104,17 +104,6 @@
    28.4  val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, 
    28.5                     ex_mono, Collect_mono, in_mono];
    28.6  
    28.7 -(* Courtesy of Stephan Merz *)
    28.8 -Goalw [Least_def] 
    28.9 -"[| mono (f::'a::order => 'b::order); ? x:S. ! y:S. x <= y |] \
   28.10 -\  ==> (LEAST y. y : f`S) = f(LEAST x. x : S)";
   28.11 -by (Clarify_tac 1);
   28.12 -by (eres_inst_tac [("P","%x. x : S")] LeastMI2 1);
   28.13 -by  (Fast_tac 1);
   28.14 -by (rtac LeastMI2 1);
   28.15 -by (auto_tac (claset() addEs [monoD] addSIs [thm "order_antisym"], simpset()));
   28.16 -qed "Least_mono";
   28.17 -
   28.18  Goal "[| a = b; c = d; b --> d |] ==> a --> c";
   28.19  by (Fast_tac 1);
   28.20  qed "eq_to_mono";
    29.1 --- a/src/HOL/simpdata.ML	Tue Jul 24 11:25:54 2001 +0200
    29.2 +++ b/src/HOL/simpdata.ML	Wed Jul 25 13:13:01 2001 +0200
    29.3 @@ -96,17 +96,6 @@
    29.4                   "(ALL x. P --> Q x) = (P --> (ALL x. Q x))"];
    29.5  
    29.6  
    29.7 -(* elimination of existential quantifiers in assumptions *)
    29.8 -
    29.9 -val ex_all_equiv =
   29.10 -  let val lemma1 = prove_goal (the_context ())
   29.11 -        "(? x. P(x) ==> PROP Q) ==> (!!x. P(x) ==> PROP Q)"
   29.12 -        (fn prems => [resolve_tac prems 1, etac exI 1]);
   29.13 -      val lemma2 = prove_goalw (the_context ()) [Ex_def]
   29.14 -        "(!!x. P(x) ==> PROP Q) ==> (? x. P(x) ==> PROP Q)"
   29.15 -        (fn prems => [(REPEAT(resolve_tac prems 1))])
   29.16 -  in equal_intr lemma1 lemma2 end;
   29.17 -
   29.18  end;
   29.19  
   29.20  bind_thms ("ex_simps", ex_simps);
   29.21 @@ -391,7 +380,7 @@
   29.22         if_True, if_False, if_cancel, if_eq_cancel,
   29.23         imp_disjL, conj_assoc, disj_assoc,
   29.24         de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
   29.25 -       disj_not1, not_all, not_ex, cases_simp, some_eq_trivial, some_sym_eq_trivial,
   29.26 +       disj_not1, not_all, not_ex, cases_simp,
   29.27         thm "the_eq_trivial", the_sym_eq_trivial, thm "plus_ac0.zero", thm "plus_ac0_zero_right"]
   29.28       @ ex_simps @ all_simps @ simp_thms)
   29.29       addsimprocs [defALL_regroup,defEX_regroup]