author noschinl Thu, 26 May 2011 23:21:00 +0200 changeset 42993 da014b00d7a4 parent 42992 4fc15e3217eb child 42994 fe291ab75eb5
instance inat for complete_lattice
```--- a/src/HOL/Library/Nat_Infinity.thy	Thu May 26 22:02:40 2011 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy	Thu May 26 23:21:00 2011 +0200
@@ -453,6 +453,18 @@

end

+lemma finite_Fin_bounded:
+  assumes le_fin: "\<And>y. y \<in> A \<Longrightarrow> y \<le> Fin n"
+  shows "finite A"
+proof (rule finite_subset)
+  show "finite (Fin ` {..n})" by blast
+
+  have "A \<subseteq> {..Fin n}" using le_fin by fastsimp
+  also have "\<dots> \<subseteq> Fin ` {..n}"
+    by (rule subsetI) (case_tac x, auto)
+  finally show "A \<subseteq> Fin ` {..n}" .
+qed
+

subsection {* Well-ordering *}

@@ -492,6 +504,38 @@
show "P n" by (blast intro: inat_less_induct hyp)
qed

+subsection {* Complete Lattice *}
+
+instantiation inat :: complete_lattice
+begin
+
+definition inf_inat :: "inat \<Rightarrow> inat \<Rightarrow> inat" where
+  "inf_inat \<equiv> min"
+
+definition sup_inat :: "inat \<Rightarrow> inat \<Rightarrow> inat" where
+  "sup_inat \<equiv> max"
+
+definition Inf_inat :: "inat set \<Rightarrow> inat" where
+  "Inf_inat A \<equiv> if A = {} then \<infinity> else (LEAST x. x \<in> A)"
+
+definition Sup_inat :: "inat set \<Rightarrow> inat" where
+  "Sup_inat A \<equiv> if A = {} then 0
+    else if finite A then Max A
+                     else \<infinity>"
+instance proof
+  fix x :: "inat" and A :: "inat set"
+  { assume "x \<in> A" then show "Inf A \<le> x"
+      unfolding Inf_inat_def by (auto intro: Least_le) }
+  { assume "\<And>y. y \<in> A \<Longrightarrow> x \<le> y" then show "x \<le> Inf A"
+      unfolding Inf_inat_def
+      by (cases "A = {}") (auto intro: LeastI2_ex) }
+  { assume "x \<in> A" then show "x \<le> Sup A"
+      unfolding Sup_inat_def by (cases "finite A") auto }
+  { assume "\<And>y. y \<in> A \<Longrightarrow> y \<le> x" then show "Sup A \<le> x"
+      unfolding Sup_inat_def using finite_Fin_bounded by auto }