# HG changeset patch
# User paulson
# Date 997094481 -7200
# Node ID e5fb885bfe3aafbade9274f67924e24287e56efa
# Parent  1b6258b288ba2180b0640d9f1b429d127670bfe7
tidying and moving the theorem "choice"

diff -r 1b6258b288ba -r e5fb885bfe3a src/HOL/Hilbert_Choice_lemmas.ML
--- a/src/HOL/Hilbert_Choice_lemmas.ML	Mon Aug 06 12:40:39 2001 +0200
+++ b/src/HOL/Hilbert_Choice_lemmas.ML	Mon Aug 06 12:41:21 2001 +0200
@@ -17,6 +17,7 @@
 by (etac exE 1);
 by (etac someI 1);
 qed "someI_ex";
+AddXEs [someI_ex];
 
 (*Easier to apply than someI: conclusion has only one occurrence of P*)
 val prems = Goal "[| P a;  !!x. P x ==> Q x |] ==> Q (SOME x. P x)";
@@ -68,29 +69,26 @@
 by (rtac refl 1);
 by (etac sym 1);
 qed "some_sym_eq_trivial";
-
-
-AddXEs [someI_ex];
-AddIs [some_equality];
-
 Addsimps [some_eq_trivial, some_sym_eq_trivial];
 
 
 (** "Axiom" of Choice, proved using the description operator **)
 
-(*"choice" is now proved in Tools/meson.ML*)
+(*Used in Tools/meson.ML*)
+Goal "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";
+by (fast_tac (claset() addEs [someI]) 1);
+qed "choice";
 
 Goal "ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)";
 by (fast_tac (claset() addEs [someI]) 1);
 qed "bchoice";
 
 
-(**** Function Inverse ****)
+section "Function Inverse";
 
 val inv_def = thm "inv_def";
 val Inv_def = thm "Inv_def";
 
-
 Goal "inv id = id";
 by (simp_tac (simpset() addsimps [inv_def,id_def]) 1);
 qed "inv_id";
@@ -212,7 +210,8 @@
 by (blast_tac (claset() addIs [bij_is_inj RS inv_f_f RS sym]) 1);
 qed "bij_vimage_eq_inv_image";
 
-(*** Inverse ***)
+
+section "Inverse of a PI-function (restricted domain)";
 
 Goalw [Inv_def] "f ` A = B ==> (lam x: B. (Inv A f) x) : B funcset A";
 by (fast_tac (claset() addIs [restrict_in_funcset, someI2]) 1);
@@ -248,7 +247,8 @@
 qed "compose_Inv_id";
 
 
-(**** split ****)
+
+section "split and SOME";
 
 (*Can't be added to simpset: loops!*)
 Goal "(SOME x. P x) = (SOME (a,b). P(a,b))";
@@ -265,10 +265,7 @@
 Addsimps [Eps_split_eq];
 
 
-(*---------------------------------------------------------------------------
- * A relation is wellfounded iff it has no infinite descending chain
- * Cannot go into WF because it needs type nat.
- *---------------------------------------------------------------------------*)
+section "A relation is wellfounded iff it has no infinite descending chain";
 
 Goalw [wf_eq_minimal RS eq_reflection]
   "wf r = (~(EX f. ALL i. (f(Suc i),f i) : r))";
diff -r 1b6258b288ba -r e5fb885bfe3a src/HOL/meson_lemmas.ML
--- a/src/HOL/meson_lemmas.ML	Mon Aug 06 12:40:39 2001 +0200
+++ b/src/HOL/meson_lemmas.ML	Mon Aug 06 12:41:21 2001 +0200
@@ -6,13 +6,6 @@
 Lemmas for Meson.
 *)
 
-(* "Axiom" of Choice, proved using the description operator *)
-
-Goal "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";
-by (fast_tac (claset() addEs [someI]) 1);
-qed "choice";
-
-
 (* Generation of contrapositives *)
 
 (*Inserts negated disjunct after removing the negation; P is a literal*)