1.1 --- a/src/HOL/Orderings.thy	Sun Aug 10 12:38:26 2008 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Mon Aug 11 14:49:53 2008 +0200
     1.3 @@ -1109,4 +1109,71 @@
     1.4  apply (blast intro: order_antisym)
     1.5  done
     1.6  
     1.7 +
     1.8 +subsection {* Dense orders *}
     1.9 +
    1.10 +class dense_linear_order = linorder + 
    1.11 +  assumes gt_ex: "\<exists>y. x < y" 
    1.12 +  and lt_ex: "\<exists>y. y < x"
    1.13 +  and dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
    1.14 +  (*see further theory Dense_Linear_Order*)
    1.15 +
    1.16 +
    1.17 +subsection {* Wellorders *}
    1.18 +
    1.19 +class wellorder = linorder +
    1.20 +  assumes less_induct [case_names less]: "(\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P a"
    1.21 +begin
    1.22 +
    1.23 +lemma wellorder_Least_lemma:
    1.24 +  fixes k :: 'a
    1.25 +  assumes "P k"
    1.26 +  shows "P (LEAST x. P x)" and "(LEAST x. P x) \<le> k"
    1.27 +proof -
    1.28 +  have "P (LEAST x. P x) \<and> (LEAST x. P x) \<le> k"
    1.29 +  using assms proof (induct k rule: less_induct)
    1.30 +    case (less x) then have "P x" by simp
    1.31 +    show ?case proof (rule classical)
    1.32 +      assume assm: "\<not> (P (LEAST a. P a) \<and> (LEAST a. P a) \<le> x)"
    1.33 +      have "\<And>y. P y \<Longrightarrow> x \<le> y"
    1.34 +      proof (rule classical)
    1.35 +        fix y
    1.36 +        assume "P y" and "\<not> x \<le> y" 
    1.37 +        with less have "P (LEAST a. P a)" and "(LEAST a. P a) \<le> y"
    1.38 +          by (auto simp add: not_le)
    1.39 +        with assm have "x < (LEAST a. P a)" and "(LEAST a. P a) \<le> y"
    1.40 +          by auto
    1.41 +        then show "x \<le> y" by auto
    1.42 +      qed
    1.43 +      with `P x` have Least: "(LEAST a. P a) = x"
    1.44 +        by (rule Least_equality)
    1.45 +      with `P x` show ?thesis by simp
    1.46 +    qed
    1.47 +  qed
    1.48 +  then show "P (LEAST x. P x)" and "(LEAST x. P x) \<le> k" by auto
    1.49 +qed
    1.50 +
    1.51 +lemmas LeastI   = wellorder_Least_lemma(1)
    1.52 +lemmas Least_le = wellorder_Least_lemma(2)
    1.53 +
    1.54 +-- "The following 3 lemmas are due to Brian Huffman"
    1.55 +lemma LeastI_ex: "\<exists>x. P x \<Longrightarrow> P (Least P)"
    1.56 +  by (erule exE) (erule LeastI)
    1.57 +
    1.58 +lemma LeastI2:
    1.59 +  "P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (Least P)"
    1.60 +  by (blast intro: LeastI)
    1.61 +
    1.62 +lemma LeastI2_ex:
    1.63 +  "\<exists>a. P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (Least P)"
    1.64 +  by (blast intro: LeastI_ex)
    1.65 +
    1.66 +lemma not_less_Least: "k < (LEAST x. P x) \<Longrightarrow> \<not> P k"
    1.67 +apply (simp (no_asm_use) add: not_le [symmetric])
    1.68 +apply (erule contrapos_nn)
    1.69 +apply (erule Least_le)
    1.70 +done
    1.71 +
    1.72 +end  
    1.73 +
    1.74  end