# HG changeset patch
# User paulson
# Date 996076706 -7200
# Node ID 7514e5e21cb82170c91e4a9cfd2f64bd8623a346
# Parent  1b15f655da2c850736af63149795739b0fd90e3f
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice

diff -r 1b15f655da2c -r 7514e5e21cb8 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Wed Jul 25 13:44:32 2001 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Wed Jul 25 17:58:26 2001 +0200
@@ -29,6 +29,11 @@
   someI:        "P (x::'a) ==> P (SOME x. P x)"
 
 
+(*used in TFL*)
+lemma tfl_some: "\\<forall>P x. P x --> P (Eps P)"
+  by (blast intro: someI)
+
+
 constdefs  
   inv :: "('a => 'b) => ('b => 'a)"
     "inv(f::'a=>'b) == % y. @x. f(x)=y"
@@ -71,6 +76,38 @@
 apply (blast intro!: order_antisym) 
 done
 
+lemma wf_linord_ex_has_least:
+     "[|wf r;  ALL x y. ((x,y):r^+) = ((y,x)~:r^*);  P k|]  \
+\     ==> EX x. P x & (!y. P y --> (m x,m y):r^*)" 
+apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]])
+apply (drule_tac x = "m`Collect P" in spec)
+apply force
+done
+
+(* successor of obsolete nonempty_has_least *)
+lemma ex_has_least_nat:
+     "P k ==> EX x. P x & (ALL y. P y --> m x <= (m y::nat))"
+apply (simp only: pred_nat_trancl_eq_le [symmetric])
+apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
+apply (simp (no_asm) add: less_eq not_le_iff_less pred_nat_trancl_eq_le)
+apply assumption
+done
+
+lemma LeastM_nat_lemma: 
+  "P k ==> P (LeastM m P) & (ALL y. P y --> m (LeastM m P) <= (m y::nat))"
+apply (unfold LeastM_def)
+apply (rule someI_ex)
+apply (erule ex_has_least_nat)
+done
+
+lemmas LeastM_natI = LeastM_nat_lemma [THEN conjunct1, standard]
+
+lemma LeastM_nat_le: "P x ==> m (LeastM m P) <= (m x::nat)"
+apply (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp])
+apply assumption
+apply assumption
+done
+
 
 (** Greatest value operator **)
 
diff -r 1b15f655da2c -r 7514e5e21cb8 src/HOL/Hilbert_Choice_lemmas.ML
--- a/src/HOL/Hilbert_Choice_lemmas.ML	Wed Jul 25 13:44:32 2001 +0200
+++ b/src/HOL/Hilbert_Choice_lemmas.ML	Wed Jul 25 17:58:26 2001 +0200
@@ -1,5 +1,5 @@
 (*  Title:      HOL/Hilbert_Choice_lemmas
-    ID:         $Id$
+    ID: $Id$
     Author:     Lawrence C Paulson
     Copyright   2001  University of Cambridge
 
@@ -263,3 +263,36 @@
 by (Blast_tac 1);
 qed "Eps_split_eq";
 Addsimps [Eps_split_eq];
+
+
+(*---------------------------------------------------------------------------
+ * A relation is wellfounded iff it has no infinite descending chain
+ * Cannot go into WF because it needs type nat.
+ *---------------------------------------------------------------------------*)
+
+Goalw [wf_eq_minimal RS eq_reflection]
+  "wf r = (~(EX f. ALL i. (f(Suc i),f i) : r))";
+by (rtac iffI 1);
+ by (rtac notI 1);
+ by (etac exE 1);
+ by (eres_inst_tac [("x","{w. EX i. w=f i}")] allE 1);
+ by (Blast_tac 1);
+by (etac contrapos_np 1);
+by (Asm_full_simp_tac 1);
+by (Clarify_tac 1);
+by (subgoal_tac "ALL n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
+ by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1);
+ by (rtac allI 1);
+ by (Simp_tac 1);
+ by (rtac someI2_ex 1);
+  by (Blast_tac 1);
+ by (Blast_tac 1);
+by (rtac allI 1);
+by (induct_tac "n" 1);
+ by (Asm_simp_tac 1);
+by (Simp_tac 1);
+by (rtac someI2_ex 1);
+ by (Blast_tac 1);
+by (Blast_tac 1);
+qed "wf_iff_no_infinite_down_chain";
+
diff -r 1b15f655da2c -r 7514e5e21cb8 src/HOL/NatArith.thy
--- a/src/HOL/NatArith.thy	Wed Jul 25 13:44:32 2001 +0200
+++ b/src/HOL/NatArith.thy	Wed Jul 25 17:58:26 2001 +0200
@@ -9,6 +9,11 @@
 
 setup arith_setup
 
+lemma pred_nat_trancl_eq_le: "(m, n) : pred_nat^* = (m <= n)"
+apply (simp add: less_eq reflcl_trancl [THEN sym] 
+            del: reflcl_trancl)
+by arith
+
 (*elimination of `-' on nat*)
 lemma nat_diff_split:
     "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
diff -r 1b15f655da2c -r 7514e5e21cb8 src/HOL/Ord.thy
--- a/src/HOL/Ord.thy	Wed Jul 25 13:44:32 2001 +0200
+++ b/src/HOL/Ord.thy	Wed Jul 25 17:58:26 2001 +0200
@@ -173,6 +173,16 @@
   Least    :: "('a::ord => bool) => 'a"               (binder "LEAST " 10)
     "Least P == THE x. P x & (ALL y. P y --> x <= y)"
 
+lemma LeastI2:
+  "[| P (x::'a::order); 
+      !!y. P y ==> x <= y;
+      !!x. [| P x; \\<forall>y. P y --> x \\<le> y |] ==> Q x |]
+   ==> Q (Least P)";
+apply (unfold Least_def)
+apply (rule theI2)
+  apply (blast intro: order_antisym)+
+done
+
 lemma Least_equality:
   "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k";
 apply (simp add: Least_def)
@@ -180,7 +190,6 @@
 apply (auto intro!: order_antisym) 
 done
 
-
 section "Linear/Total Orders"
 
 axclass linorder < order
diff -r 1b15f655da2c -r 7514e5e21cb8 src/HOL/Recdef.thy
--- a/src/HOL/Recdef.thy	Wed Jul 25 13:44:32 2001 +0200
+++ b/src/HOL/Recdef.thy	Wed Jul 25 17:58:26 2001 +0200
@@ -17,9 +17,6 @@
   ("../TFL/post.ML")
   ("Tools/recdef_package.ML"):
 
-lemma tfl_some: "\\<forall>P x. P x --> P (Eps P)"
-  by (blast intro: someI)
-
 lemma tfl_eq_True: "(x = True) --> x"
   by blast
 
diff -r 1b15f655da2c -r 7514e5e21cb8 src/HOL/Wellfounded_Relations.ML
--- a/src/HOL/Wellfounded_Relations.ML	Wed Jul 25 13:44:32 2001 +0200
+++ b/src/HOL/Wellfounded_Relations.ML	Wed Jul 25 17:58:26 2001 +0200
@@ -123,37 +123,6 @@
 qed "wf_iff_acyclic_if_finite";
 
 
-(*---------------------------------------------------------------------------
- * A relation is wellfounded iff it has no infinite descending chain
- * Cannot go into WF because it needs type nat.
- *---------------------------------------------------------------------------*)
-
-Goalw [wf_eq_minimal RS eq_reflection]
-  "wf r = (~(EX f. ALL i. (f(Suc i),f i) : r))";
-by (rtac iffI 1);
- by (rtac notI 1);
- by (etac exE 1);
- by (eres_inst_tac [("x","{w. EX i. w=f i}")] allE 1);
- by (Blast_tac 1);
-by (etac contrapos_np 1);
-by (Asm_full_simp_tac 1);
-by (Clarify_tac 1);
-by (subgoal_tac "ALL n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
- by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1);
- by (rtac allI 1);
- by (Simp_tac 1);
- by (rtac someI2_ex 1);
-  by (Blast_tac 1);
- by (Blast_tac 1);
-by (rtac allI 1);
-by (induct_tac "n" 1);
- by (Asm_simp_tac 1);
-by (Simp_tac 1);
-by (rtac someI2_ex 1);
- by (Blast_tac 1);
-by (Blast_tac 1);
-qed "wf_iff_no_infinite_down_chain";
-
 (*----------------------------------------------------------------------------
  * Weakly decreasing sequences (w.r.t. some well-founded order) stabilize.
  *---------------------------------------------------------------------------*)
@@ -187,17 +156,10 @@
 by Auto_tac;
 qed "wf_weak_decr_stable";
 
-(* special case: <= *)
-
-Goal "(m, n) : pred_nat^* = (m <= n)";
-by (simp_tac (simpset() addsimps [less_eq, thm"reflcl_trancl" RS sym] 
-                        delsimps [thm"reflcl_trancl"]) 1);
-by (arith_tac 1);
-qed "le_eq";
-
+(* special case of the theorem above: <= *)
 Goal "ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i";
 by (res_inst_tac [("r","pred_nat")] wf_weak_decr_stable 1);
-by (asm_simp_tac (simpset() addsimps [le_eq]) 1);
+by (asm_simp_tac (simpset() addsimps [thm "pred_nat_trancl_eq_le"]) 1);
 by (REPEAT (resolve_tac [wf_trancl,wf_pred_nat] 1));
 qed "weak_decr_stable";
 
@@ -221,37 +183,3 @@
  by(Blast_tac 1);
 by(blast_tac (claset() addIs prems) 1);
 qed "wf_same_fst";
-
-
-
-(* ### see also LEAST and wellorderings in Wellfounded_Recursion.ML *)
-
-Goal "wf r ==> !x y. ((x,y):r^+) = ((y,x)~:r^*) ==> \
-\ P k ==> ? x. P x & (!y. P y --> (m x,m y):r^*)";
-by (dtac (wf_trancl RS (wf_eq_minimal RS iffD1)) 1);
-by (dres_inst_tac [("x","m`Collect P")] spec 1);
-by (Force_tac 1);
-qed "wf_linord_ex_has_least";
-
-(* successor of obsolete nonempty_has_least *)
-Goal "P k ==> ? x. P x & (!y. P y --> m x <= (m y::nat))";
-by (simp_tac (HOL_basic_ss addsimps [le_eq RS sym]) 1);
-by (rtac (wf_pred_nat RS wf_linord_ex_has_least) 1);
-by (simp_tac (simpset() addsimps [less_eq,not_le_iff_less,le_eq]) 1);
-by (atac 1);
-qed "ex_has_least_nat";
-
-Goalw [thm "LeastM_def"] 
-  "P k ==> P (LeastM m P) & (!y. P y --> m (LeastM m P) <= (m y::nat))";
-by (rtac someI_ex 1);
-by (etac ex_has_least_nat 1);
-qed "LeastM_nat_lemma";
-
-bind_thm ("LeastM_natI", LeastM_nat_lemma RS conjunct1);
-
-Goal "P x ==> m (LeastM m P) <= (m x::nat)";
-by (rtac (LeastM_nat_lemma RS conjunct2 RS spec RS mp) 1);
-by (atac 1);
-by (atac 1);
-qed "LeastM_nat_le";
-
diff -r 1b15f655da2c -r 7514e5e21cb8 src/HOL/Wellfounded_Relations.thy
--- a/src/HOL/Wellfounded_Relations.thy	Wed Jul 25 13:44:32 2001 +0200
+++ b/src/HOL/Wellfounded_Relations.thy	Wed Jul 25 17:58:26 2001 +0200
@@ -10,7 +10,7 @@
 separately.
 *)
 
-Wellfounded_Relations = Finite + Hilbert_Choice + 
+Wellfounded_Relations = Finite + 
 
 (* logically belongs in Finite.thy, but the theorems are proved in Finite.ML *)
 instance unit :: finite                  (finite_unit)
diff -r 1b15f655da2c -r 7514e5e21cb8 src/HOL/subset.thy
--- a/src/HOL/subset.thy	Wed Jul 25 13:44:32 2001 +0200
+++ b/src/HOL/subset.thy	Wed Jul 25 17:58:26 2001 +0200
@@ -9,10 +9,23 @@
 theory subset = Set
 files "Tools/induct_attrib.ML" ("Tools/typedef_package.ML"):
 
-(*belongs to theory Ord*)
+(** belongs to theory Ord **)
+  
 theorems linorder_cases [case_names less equal greater] =
   linorder_less_split
 
+(* Courtesy of Stephan Merz *)
+lemma Least_mono: 
+"[| mono (f::'a::order => 'b::order); EX x:S. ALL y:S. x <= y |]  
+   ==> (LEAST y. y : f`S) = f(LEAST x. x : S)"
+apply clarify
+apply (erule_tac P = "%x. x : S" in LeastI2)
+apply  fast
+apply (rule LeastI2)
+apply (auto elim: monoD intro!: order_antisym)
+done
+
+
 (*belongs to theory Set*)
 setup Rulify.setup
 
@@ -22,25 +35,25 @@
 constdefs
   type_definition :: "('a => 'b) => ('b => 'a) => 'b set => bool"
   "type_definition Rep Abs A ==
-    (\<forall>x. Rep x \<in> A) \<and>
-    (\<forall>x. Abs (Rep x) = x) \<and>
-    (\<forall>y \<in> A. Rep (Abs y) = y)"
+    (\\<forall>x. Rep x \\<in> A) \\<and>
+    (\\<forall>x. Abs (Rep x) = x) \\<and>
+    (\\<forall>y \\<in> A. Rep (Abs y) = y)"
   -- {* This will be stated as an axiom for each typedef! *}
 
 lemma type_definitionI [intro]:
-  "(!!x. Rep x \<in> A) ==>
+  "(!!x. Rep x \\<in> A) ==>
     (!!x. Abs (Rep x) = x) ==>
-    (!!y. y \<in> A ==> Rep (Abs y) = y) ==>
+    (!!y. y \\<in> A ==> Rep (Abs y) = y) ==>
     type_definition Rep Abs A"
   by (unfold type_definition_def) blast
 
-theorem Rep: "type_definition Rep Abs A ==> Rep x \<in> A"
+theorem Rep: "type_definition Rep Abs A ==> Rep x \\<in> A"
   by (unfold type_definition_def) blast
 
 theorem Rep_inverse: "type_definition Rep Abs A ==> Abs (Rep x) = x"
   by (unfold type_definition_def) blast
 
-theorem Abs_inverse: "type_definition Rep Abs A ==> y \<in> A ==> Rep (Abs y) = y"
+theorem Abs_inverse: "type_definition Rep Abs A ==> y \\<in> A ==> Rep (Abs y) = y"
   by (unfold type_definition_def) blast
 
 theorem Rep_inject: "type_definition Rep Abs A ==> (Rep x = Rep y) = (x = y)"
@@ -58,10 +71,10 @@
 qed
 
 theorem Abs_inject:
-  "type_definition Rep Abs A ==> x \<in> A ==> y \<in> A ==> (Abs x = Abs y) = (x = y)"
+  "type_definition Rep Abs A ==> x \\<in> A ==> y \\<in> A ==> (Abs x = Abs y) = (x = y)"
 proof -
   assume tydef: "type_definition Rep Abs A"
-  assume x: "x \<in> A" and y: "y \<in> A"
+  assume x: "x \\<in> A" and y: "y \\<in> A"
   show ?thesis
   proof
     assume "Abs x = Abs y"
@@ -76,10 +89,10 @@
 qed
 
 theorem Rep_cases:
-  "type_definition Rep Abs A ==> y \<in> A ==> (!!x. y = Rep x ==> P) ==> P"
+  "type_definition Rep Abs A ==> y \\<in> A ==> (!!x. y = Rep x ==> P) ==> P"
 proof -
   assume tydef: "type_definition Rep Abs A"
-  assume y: "y \<in> A" and r: "(!!x. y = Rep x ==> P)"
+  assume y: "y \\<in> A" and r: "(!!x. y = Rep x ==> P)"
   show P
   proof (rule r)
     from y have "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
@@ -88,33 +101,33 @@
 qed
 
 theorem Abs_cases:
-  "type_definition Rep Abs A ==> (!!y. x = Abs y ==> y \<in> A ==> P) ==> P"
+  "type_definition Rep Abs A ==> (!!y. x = Abs y ==> y \\<in> A ==> P) ==> P"
 proof -
   assume tydef: "type_definition Rep Abs A"
-  assume r: "!!y. x = Abs y ==> y \<in> A ==> P"
+  assume r: "!!y. x = Abs y ==> y \\<in> A ==> P"
   show P
   proof (rule r)
     have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef])
     thus "x = Abs (Rep x)" ..
-    show "Rep x \<in> A" by (rule Rep [OF tydef])
+    show "Rep x \\<in> A" by (rule Rep [OF tydef])
   qed
 qed
 
 theorem Rep_induct:
-  "type_definition Rep Abs A ==> y \<in> A ==> (!!x. P (Rep x)) ==> P y"
+  "type_definition Rep Abs A ==> y \\<in> A ==> (!!x. P (Rep x)) ==> P y"
 proof -
   assume tydef: "type_definition Rep Abs A"
   assume "!!x. P (Rep x)" hence "P (Rep (Abs y))" .
-  moreover assume "y \<in> A" hence "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
+  moreover assume "y \\<in> A" hence "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
   ultimately show "P y" by (simp only:)
 qed
 
 theorem Abs_induct:
-  "type_definition Rep Abs A ==> (!!y. y \<in> A ==> P (Abs y)) ==> P x"
+  "type_definition Rep Abs A ==> (!!y. y \\<in> A ==> P (Abs y)) ==> P x"
 proof -
   assume tydef: "type_definition Rep Abs A"
-  assume r: "!!y. y \<in> A ==> P (Abs y)"
-  have "Rep x \<in> A" by (rule Rep [OF tydef])
+  assume r: "!!y. y \\<in> A ==> P (Abs y)"
+  have "Rep x \\<in> A" by (rule Rep [OF tydef])
   hence "P (Abs (Rep x))" by (rule r)
   moreover have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef])
   ultimately show "P x" by (simp only:)