# HG changeset patch
# User haftmann
# Date 1180120132 -7200
# Node ID 7cb68a8708c11aec6476a3ab49193d8254d246b8
# Parent  0c3c55b7c98fac9fc5981c9926f64faacbd96e14
using rudimentary class target mechanism

diff -r 0c3c55b7c98f -r 7cb68a8708c1 src/HOL/FixedPoint.thy
--- a/src/HOL/FixedPoint.thy	Fri May 25 21:08:46 2007 +0200
+++ b/src/HOL/FixedPoint.thy	Fri May 25 21:08:52 2007 +0200
@@ -22,7 +22,10 @@
 definition
   Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
 where
-  "Sup A = \<Sqinter>{b. \<forall>a \<in> A. a \<^loc>\<le> b}"
+  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<^loc>\<le> b}"
+
+lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<^loc>\<le> a}"
+  unfolding Sup_def by (auto intro: Inf_greatest Inf_lower)
 
 lemma Sup_upper: "x \<in> A \<Longrightarrow> x \<^loc>\<le> \<Squnion>A"
   by (auto simp: Sup_def intro: Inf_greatest)
@@ -36,6 +39,12 @@
 lemma bot_least [simp]: "\<Squnion>{} \<^loc>\<le> x"
   by (rule Sup_least) simp
 
+lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}"
+  unfolding Sup_def by auto
+
+lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}"
+  unfolding Inf_Sup by auto
+
 lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
   apply (rule antisym)
   apply (rule le_infI)
@@ -94,34 +103,15 @@
 
 end
 
-hide const Sup
-
-definition
-  Sup :: "'a\<Colon>complete_lattice set \<Rightarrow> 'a"
-where
-  [code func del]: "Sup A = Inf {b. \<forall>a \<in> A. a \<le> b}"
+lemmas Sup_def = Sup_def [folded complete_lattice_class.Sup]
+lemmas Sup_upper = Sup_upper [folded complete_lattice_class.Sup]
+lemmas Sup_least = Sup_least [folded complete_lattice_class.Sup]
 
-lemma complete_lattice_class_Sup:
-  "complete_lattice.Sup (op \<le>) Inf = Sup"
-proof
-  fix A
-  show "complete_lattice.Sup (op \<le>) Inf A = Sup A"
-  by (auto simp add: Sup_def complete_lattice.Sup_def [OF complete_lattice_class.axioms])
-qed
-
-lemmas Sup_upper = complete_lattice_class.Sup_upper [unfolded complete_lattice_class_Sup]
-lemmas Sup_least = complete_lattice_class.Sup_least [unfolded complete_lattice_class_Sup]
-
-lemmas top_greatest [simp] = complete_lattice_class.top_greatest
-lemmas bot_least [simp] = complete_lattice_class.bot_least [unfolded complete_lattice_class_Sup]
-lemmas Inf_insert = complete_lattice_class.Inf_insert
-lemmas Sup_insert [code func] = complete_lattice_class.Sup_insert [unfolded complete_lattice_class_Sup]
-lemmas Inf_singleton [simp] = complete_lattice_class.Inf_singleton
-lemmas Sup_singleton [simp, code func] = complete_lattice_class.Sup_singleton [unfolded complete_lattice_class_Sup]
-lemmas Inf_insert_simp = complete_lattice_class.Inf_insert_simp
-lemmas Sup_insert_simp = complete_lattice_class.Sup_insert_simp [unfolded complete_lattice_class_Sup]
-lemmas Inf_binary = complete_lattice_class.Inf_binary
-lemmas Sup_binary = complete_lattice_class.Sup_binary [unfolded complete_lattice_class_Sup]
+lemmas bot_least [simp] = bot_least [folded complete_lattice_class.Sup]
+lemmas Sup_insert [code func] = Sup_insert [folded complete_lattice_class.Sup]
+lemmas Sup_singleton [simp, code func] = Sup_singleton [folded complete_lattice_class.Sup]
+lemmas Sup_insert_simp = Sup_insert_simp [folded complete_lattice_class.Sup]
+lemmas Sup_binary = Sup_binary [folded complete_lattice_class.Sup]
 
 definition
   SUPR :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> 'b" where
@@ -208,6 +198,13 @@
   apply assumption+
   done
 
+lemma Inf_empty_bool [simp]:
+  "Inf {}"
+  unfolding Inf_bool_def by auto
+
+lemma not_Sup_empty_bool [simp]:
+  "\<not> Sup {}"
+  unfolding Sup_def Inf_bool_def by auto
 
 subsubsection {* Functions *}
 
@@ -244,6 +241,19 @@
   apply simp
   done
 
+lemma Inf_empty_fun_True:
+  "Inf {} = (\<lambda>_. True)"
+  by rule (auto simp add: Inf_fun_def)
+
+lemma Sup_empty_fun_False:
+  "Sup {} = (\<lambda>_. False)"
+proof
+  fix x
+  have aux: "{y\<Colon>bool. \<exists>f\<Colon>'a \<Rightarrow> bool. y = f x} = {True, False}" by auto
+  show "Sup {} x = False"
+  unfolding Sup_def Inf_fun_def by (auto simp add: aux Inf_binary inf_bool_eq)
+qed 
+
 
 subsubsection {* Sets *}