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