src/HOL/Orderings.thy
changeset 27823 52971512d1a2
parent 27689 268a7d02cf7a
child 28516 e6fdcaaadbd3
--- 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