# HG changeset patch
# User haftmann
# Date 1218458993 -7200
# Node ID 52971512d1a226421a5663ad2e046f55804c3107
# Parent  a6319699e517c1de99c191349750656fe00fa566
moved class wellorder to theory Orderings

diff -r a6319699e517 -r 52971512d1a2 NEWS
--- a/NEWS	Sun Aug 10 12:38:26 2008 +0200
+++ b/NEWS	Mon Aug 11 14:49:53 2008 +0200
@@ -40,6 +40,10 @@
 
 *** HOL ***
 
+* HOL/Orderings: class "wellorder" moved here, with explicit induction rule
+"less_induct" as assumption.  For instantiation of "wellorder" by means
+of predicate "wf", use rule wf_wellorderI.  INCOMPATIBILITY.
+
 * HOL/Orderings: added class "preorder" as superclass of "order".
 INCOMPATIBILITY: Instantiation proofs for order, linorder
 etc. slightly changed.  Some theorems named order_class.* now named
@@ -5671,4 +5675,5 @@
 
 :mode=text:wrap=hard:maxLineLen=72:
 
+
 $Id$
diff -r a6319699e517 -r 52971512d1a2 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Sun Aug 10 12:38:26 2008 +0200
+++ b/src/HOL/Datatype.thy	Mon Aug 11 14:49:53 2008 +0200
@@ -9,14 +9,9 @@
 header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *}
 
 theory Datatype
-imports Finite_Set Wellfounded
+imports Finite_Set
 begin
 
-lemma size_bool [code func]:
-  "size (b\<Colon>bool) = 0" by (cases b) auto
-
-declare "prod.size" [noatp]
-
 typedef (Node)
   ('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}"
     --{*it is a subtype of @{text "(nat=>'b+nat) * ('a+nat)"}*}
diff -r a6319699e517 -r 52971512d1a2 src/HOL/Library/Nat_Infinity.thy
--- a/src/HOL/Library/Nat_Infinity.thy	Sun Aug 10 12:38:26 2008 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy	Mon Aug 11 14:49:53 2008 +0200
@@ -317,13 +317,9 @@
 
 instance inat :: wellorder
 proof
-  show "wf {(x::inat, y::inat). x < y}"
-  proof (rule wfUNIVI)
-    fix P and x :: inat
-    assume "\<forall>x::inat. (\<forall>y. (y, x) \<in> {(x, y). x < y} \<longrightarrow> P y) \<longrightarrow> P x"
-    hence 1: "!!x::inat. ALL y. y < x --> P y ==> P x" by fast
-    thus "P x" by (rule inat_less_induct)
-  qed
+  fix P and n
+  assume hyp: "(\<And>n\<Colon>inat. (\<And>m\<Colon>inat. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)"
+  show "P n" by (blast intro: inat_less_induct hyp)
 qed
 
 
diff -r a6319699e517 -r 52971512d1a2 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sun Aug 10 12:38:26 2008 +0200
+++ b/src/HOL/Nat.thy	Mon Aug 11 14:49:53 2008 +0200
@@ -733,31 +733,66 @@
 
 text {* Complete induction, aka course-of-values induction *}
 
-lemma less_induct [case_names less]:
-  fixes P :: "nat \<Rightarrow> bool"
-  assumes step: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
-  shows "P a"
-proof - 
-  have "\<And>z. z\<le>a \<Longrightarrow> P z"
-  proof (induct a)
-    case (0 z)
+instance nat :: wellorder proof
+  fix P and n :: nat
+  assume step: "\<And>n::nat. (\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n"
+  have "\<And>q. q \<le> n \<Longrightarrow> P q"
+  proof (induct n)
+    case (0 n)
     have "P 0" by (rule step) auto
     thus ?case using 0 by auto
   next
-    case (Suc x z)
-    then have "z \<le> x \<or> z = Suc x" by (simp add: le_Suc_eq)
+    case (Suc m n)
+    then have "n \<le> m \<or> n = Suc m" by (simp add: le_Suc_eq)
     thus ?case
     proof
-      assume "z \<le> x" thus "P z" by (rule Suc(1))
+      assume "n \<le> m" thus "P n" by (rule Suc(1))
     next
-      assume z: "z = Suc x"
-      show "P z"
-        by (rule step) (rule Suc(1), simp add: z le_simps)
+      assume n: "n = Suc m"
+      show "P n"
+        by (rule step) (rule Suc(1), simp add: n le_simps)
     qed
   qed
-  thus ?thesis by auto
+  then show "P n" by auto
 qed
 
+lemma Least_Suc:
+     "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
+  apply (case_tac "n", auto)
+  apply (frule LeastI)
+  apply (drule_tac P = "%x. P (Suc x) " in LeastI)
+  apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
+  apply (erule_tac [2] Least_le)
+  apply (case_tac "LEAST x. P x", auto)
+  apply (drule_tac P = "%x. P (Suc x) " in Least_le)
+  apply (blast intro: order_antisym)
+  done
+
+lemma Least_Suc2:
+   "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
+  apply (erule (1) Least_Suc [THEN ssubst])
+  apply simp
+  done
+
+lemma ex_least_nat_le: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k\<le>n. (\<forall>i<k. \<not>P i) & P(k)"
+  apply (cases n)
+   apply blast
+  apply (rule_tac x="LEAST k. P(k)" in exI)
+  apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex)
+  done
+
+lemma ex_least_nat_less: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k<n. (\<forall>i\<le>k. \<not>P i) & P(k+1)"
+  apply (cases n)
+   apply blast
+  apply (frule (1) ex_least_nat_le)
+  apply (erule exE)
+  apply (case_tac k)
+   apply simp
+  apply (rename_tac k1)
+  apply (rule_tac x=k1 in exI)
+  apply (auto simp add: less_eq_Suc_le)
+  done
+
 lemma nat_less_induct:
   assumes "!!n. \<forall>m::nat. m < n --> P m ==> P n" shows "P n"
   using assms less_induct by blast
diff -r a6319699e517 -r 52971512d1a2 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Sun Aug 10 12:38:26 2008 +0200
+++ b/src/HOL/Orderings.thy	Mon Aug 11 14:49:53 2008 +0200
@@ -1109,4 +1109,71 @@
 apply (blast intro: order_antisym)
 done
 
+
+subsection {* Dense orders *}
+
+class dense_linear_order = linorder + 
+  assumes gt_ex: "\<exists>y. x < y" 
+  and lt_ex: "\<exists>y. y < x"
+  and dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
+  (*see further theory Dense_Linear_Order*)
+
+
+subsection {* Wellorders *}
+
+class wellorder = linorder +
+  assumes less_induct [case_names less]: "(\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P a"
+begin
+
+lemma wellorder_Least_lemma:
+  fixes k :: 'a
+  assumes "P k"
+  shows "P (LEAST x. P x)" and "(LEAST x. P x) \<le> k"
+proof -
+  have "P (LEAST x. P x) \<and> (LEAST x. P x) \<le> k"
+  using assms proof (induct k rule: less_induct)
+    case (less x) then have "P x" by simp
+    show ?case proof (rule classical)
+      assume assm: "\<not> (P (LEAST a. P a) \<and> (LEAST a. P a) \<le> x)"
+      have "\<And>y. P y \<Longrightarrow> x \<le> y"
+      proof (rule classical)
+        fix y
+        assume "P y" and "\<not> x \<le> y" 
+        with less have "P (LEAST a. P a)" and "(LEAST a. P a) \<le> y"
+          by (auto simp add: not_le)
+        with assm have "x < (LEAST a. P a)" and "(LEAST a. P a) \<le> y"
+          by auto
+        then show "x \<le> y" by auto
+      qed
+      with `P x` have Least: "(LEAST a. P a) = x"
+        by (rule Least_equality)
+      with `P x` show ?thesis by simp
+    qed
+  qed
+  then show "P (LEAST x. P x)" and "(LEAST x. P x) \<le> k" by auto
+qed
+
+lemmas LeastI   = wellorder_Least_lemma(1)
+lemmas Least_le = wellorder_Least_lemma(2)
+
+-- "The following 3 lemmas are due to Brian Huffman"
+lemma LeastI_ex: "\<exists>x. P x \<Longrightarrow> P (Least P)"
+  by (erule exE) (erule LeastI)
+
+lemma LeastI2:
+  "P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (Least P)"
+  by (blast intro: LeastI)
+
+lemma LeastI2_ex:
+  "\<exists>a. P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (Least P)"
+  by (blast intro: LeastI_ex)
+
+lemma not_less_Least: "k < (LEAST x. P x) \<Longrightarrow> \<not> P k"
+apply (simp (no_asm_use) add: not_le [symmetric])
+apply (erule contrapos_nn)
+apply (erule Least_le)
+done
+
+end  
+
 end
diff -r a6319699e517 -r 52971512d1a2 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Sun Aug 10 12:38:26 2008 +0200
+++ b/src/HOL/Wellfounded.thy	Mon Aug 11 14:49:53 2008 +0200
@@ -45,10 +45,6 @@
 abbreviation acyclicP :: "('a => 'a => bool) => bool" where
   "acyclicP r == acyclic {(x, y). r x y}"
 
-class wellorder = linorder +
-  assumes wf: "wf {(x, y). x < y}"
-
-
 lemma wfP_wf_eq [pred_set_conv]: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r"
   by (simp add: wfP_def)
 
@@ -90,6 +86,18 @@
 (* [| wf r;  (a,a) ~: r ==> PROP W |] ==> PROP W *)
 lemmas wf_irrefl = wf_not_refl [elim_format]
 
+lemma wf_wellorderI:
+  assumes wf: "wf {(x::'a::ord, y). x < y}"
+  assumes lin: "OFCLASS('a::ord, linorder_class)"
+  shows "OFCLASS('a::ord, wellorder_class)"
+using lin by (rule wellorder_class.intro)
+  (blast intro: wellorder_axioms.intro wf_induct_rule [OF wf])
+
+lemma (in wellorder) wf:
+  "wf {(x, y). x < y}"
+unfolding wf_def by (blast intro: less_induct)
+
+
 subsection {* Basic Results *}
 
 text{*transitive closure of a well-founded relation is well-founded! *}
@@ -460,43 +468,6 @@
 *}
 
 
-subsection {*LEAST and wellorderings*}
-
-text{* See also @{text wf_linord_ex_has_least} and its consequences in
- @{text Wellfounded_Relations.ML}*}
-
-lemma wellorder_Least_lemma [rule_format]:
-     "P (k::'a::wellorder) --> P (LEAST x. P(x)) & (LEAST x. P(x)) <= k"
-apply (rule_tac a = k in wf [THEN wf_induct])
-apply (rule impI)
-apply (rule classical)
-apply (rule_tac s = x in Least_equality [THEN ssubst], auto)
-apply (auto simp add: linorder_not_less [symmetric])
-done
-
-lemmas LeastI   = wellorder_Least_lemma [THEN conjunct1, standard]
-lemmas Least_le = wellorder_Least_lemma [THEN conjunct2, standard]
-
--- "The following 3 lemmas are due to Brian Huffman"
-lemma LeastI_ex: "EX x::'a::wellorder. P x ==> P (Least P)"
-apply (erule exE)
-apply (erule LeastI)
-done
-
-lemma LeastI2:
-  "[| P (a::'a::wellorder); !!x. P x ==> Q x |] ==> Q (Least P)"
-by (blast intro: LeastI)
-
-lemma LeastI2_ex:
-  "[| EX a::'a::wellorder. P a; !!x. P x ==> Q x |] ==> Q (Least P)"
-by (blast intro: LeastI_ex)
-
-lemma not_less_Least: "[| k < (LEAST x. P x) |] ==> ~P (k::'a::wellorder)"
-apply (simp (no_asm_use) add: linorder_not_le [symmetric])
-apply (erule contrapos_nn)
-apply (erule Least_le)
-done
-
 subsection {* @{typ nat} is well-founded *}
 
 lemma less_nat_rel: "op < = (\<lambda>m n. n = Suc m)^++"
@@ -550,52 +521,6 @@
 lemma wf_less: "wf {(x, y::nat). x < y}"
   using wf_less_than by (simp add: less_than_def less_eq [symmetric])
 
-text {* Type @{typ nat} is a wellfounded order *}
-
-instance nat :: wellorder
-  by intro_classes
-    (assumption |
-      rule le_refl le_trans le_anti_sym nat_less_le nat_le_linear wf_less)+
-
-text {* @{text LEAST} theorems for type @{typ nat}*}
-
-lemma Least_Suc:
-     "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
-  apply (case_tac "n", auto)
-  apply (frule LeastI)
-  apply (drule_tac P = "%x. P (Suc x) " in LeastI)
-  apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
-  apply (erule_tac [2] Least_le)
-  apply (case_tac "LEAST x. P x", auto)
-  apply (drule_tac P = "%x. P (Suc x) " in Least_le)
-  apply (blast intro: order_antisym)
-  done
-
-lemma Least_Suc2:
-   "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
-  apply (erule (1) Least_Suc [THEN ssubst])
-  apply simp
-  done
-
-lemma ex_least_nat_le: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k\<le>n. (\<forall>i<k. \<not>P i) & P(k)"
-  apply (cases n)
-   apply blast
-  apply (rule_tac x="LEAST k. P(k)" in exI)
-  apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex)
-  done
-
-lemma ex_least_nat_less: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k<n. (\<forall>i\<le>k. \<not>P i) & P(k+1)"
-  apply (cases n)
-   apply blast
-  apply (frule (1) ex_least_nat_le)
-  apply (erule exE)
-  apply (case_tac k)
-   apply simp
-  apply (rename_tac k1)
-  apply (rule_tac x=k1 in exI)
-  apply fastsimp
-  done
-
 
 subsection {* Accessible Part *}
 
@@ -914,8 +839,12 @@
 
 setup Size.setup
 
+lemma size_bool [code func]:
+  "size (b\<Colon>bool) = 0" by (cases b) auto
+
 lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n"
   by (induct n) simp_all
 
+declare "prod.size" [noatp]
 
 end