
diff -r 09e794384323 -r 6a56bf1b3a64 src/HOL/FixedPoint.thy
--- a/src/HOL/FixedPoint.thy	Sat Mar 10 16:13:08 2007 +0100
+++ b/src/HOL/FixedPoint.thy	Sat Mar 10 16:23:28 2007 +0100
@@ -20,15 +20,6 @@
   Sup :: "'a::order set \<Rightarrow> 'a" where
   "Sup A = Inf {b. \<forall>a \<in> A. a \<le> b}"
 
-definition
-  SUP :: "('a \<Rightarrow> 'b::order) \<Rightarrow> 'b"  (binder "SUP " 10) where
-  "(SUP x. f x) = Sup (f ` UNIV)"
-
-(*
-abbreviation
-  bot :: "'a::order" where
-  "bot == Sup {}"
-*)
 class comp_lat = order +
   assumes Inf_lower: "x \<in> A \<Longrightarrow> Inf A \<sqsubseteq> x"
   assumes Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> Inf A"
@@ -39,6 +30,54 @@
 theorem Sup_least: "(\<And>x::'a::comp_lat. x \<in> A \<Longrightarrow> x <= z) \<Longrightarrow> Sup A <= z"
   by (auto simp: Sup_def intro: Inf_lower)
 
+definition
+  SUPR :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::comp_lat) \<Rightarrow> 'b" where
+  "SUPR A f == Sup (f ` A)"
+
+definition
+  INFI :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::comp_lat) \<Rightarrow> 'b" where
+  "INFI A f == Inf (f ` A)"
+
+syntax
+  "_SUP1"     :: "pttrns => 'b => 'b"           ("(3SUP _./ _)" 10)
+  "_SUP"      :: "pttrn => 'a set => 'b => 'b"  ("(3SUP _:_./ _)" 10)
+  "_INF1"     :: "pttrns => 'b => 'b"           ("(3INF _./ _)" 10)
+  "_INF"      :: "pttrn => 'a set => 'b => 'b"  ("(3INF _:_./ _)" 10)
+
+translations
+  "SUP x y. B"   == "SUP x. SUP y. B"
+  "SUP x. B"     == "CONST SUPR UNIV (%x. B)"
+  "SUP x. B"     == "SUP x:UNIV. B"
+  "SUP x:A. B"   == "CONST SUPR A (%x. B)"
+  "INF x y. B"   == "INF x. INF y. B"
+  "INF x. B"     == "CONST INFI UNIV (%x. B)"
+  "INF x. B"     == "INF x:UNIV. B"
+  "INF x:A. B"   == "CONST INFI A (%x. B)"
+
+(* To avoid eta-contraction of body: *)
+print_translation {*
+let
+  fun btr' syn (A :: Abs abs :: ts) =
+    let val (x,t) = atomic_abs_tr' abs
+    in list_comb (Syntax.const syn $ x $ A $ t, ts) end
+  val const_syntax_name = Sign.const_syntax_name @{theory} o fst o dest_Const
+in
+[(const_syntax_name @{term SUPR}, btr' "_SUP"),(const_syntax_name @{term "INFI"}, btr' "_INF")]
+end
+*}
+
+lemma le_SUPI: "i : A \<Longrightarrow> M i \<le> (SUP i:A. M i)"
+  by (auto simp add: SUPR_def intro: Sup_upper)
+
+lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<le> u) \<Longrightarrow> (SUP i:A. M i) \<le> u"
+  by (auto simp add: SUPR_def intro: Sup_least)
+
+lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<le> M i"
+  by (auto simp add: INFI_def intro: Inf_lower)
+
+lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<le> M i) \<Longrightarrow> u \<le> (INF i:A. M i)"
+  by (auto simp add: INFI_def intro: Inf_greatest)
+
 text {* A complete lattice is a lattice *}
 
 lemma is_meet_Inf: "is_meet (\<lambda>(x::'a::comp_lat) y. Inf {x, y})"
@@ -62,59 +101,48 @@
   by (auto simp add: mono_def)
 
 lemma Sup_insert[simp]: "Sup (insert (a::'a::comp_lat) A) = sup a (Sup A)"
-apply(simp add:Sup_def)
-apply(rule order_antisym)
- apply(rule Inf_lower)
- apply(clarsimp)
- apply(rule le_supI2)
- apply(rule Inf_greatest)
- apply blast
-apply simp
-apply rule
- apply(rule Inf_greatest)apply blast
-apply(rule Inf_greatest)
-apply(rule Inf_lower)
-apply blast
-done
+  apply (rule order_antisym)
+  apply (rule Sup_least)
+  apply (erule insertE)
+  apply (rule le_supI1)
+  apply simp
+  apply (rule le_supI2)
+  apply (erule Sup_upper)
+  apply (rule le_supI)
+  apply (rule Sup_upper)
+  apply simp
+  apply (rule Sup_least)
+  apply (rule Sup_upper)
+  apply simp
+  done
+
+lemma Inf_insert[simp]: "Inf (insert (a::'a::comp_lat) A) = inf a (Inf A)"
+  apply (rule order_antisym)
+  apply (rule le_infI)
+  apply (rule Inf_lower)
+  apply simp
+  apply (rule Inf_greatest)
+  apply (rule Inf_lower)
+  apply simp
+  apply (rule Inf_greatest)
+  apply (erule insertE)
+  apply (rule le_infI1)
+  apply simp
+  apply (rule le_infI2)
+  apply (erule Inf_lower)
+  done
 
 lemma bot_least[simp]: "Sup{} \<le> (x::'a::comp_lat)"
-apply(simp add: Sup_def)
-apply(rule Inf_lower)
-apply blast
-done
-(*
-lemma Inf_singleton[simp]: "Inf{a} = (a::'a::comp_lat)"
-apply(rule order_antisym)
- apply(simp add: Inf_lower)
-apply(rule Inf_greatest)
-apply(simp)
-done
-*)
-lemma le_SupI: "(l::'a::comp_lat) : M \<Longrightarrow> l \<le> Sup M"
-apply(simp add:Sup_def)
-apply(rule Inf_greatest)
-apply(simp)
-done
+  by (rule Sup_least) simp
+
+lemma top_greatest[simp]: "(x::'a::comp_lat) \<le> Inf{}"
+  by (rule Inf_greatest) simp
 
-lemma le_SUPI: "(l::'a::comp_lat) = M i \<Longrightarrow> l \<le> (SUP i. M i)"
-apply(simp add:SUP_def)
-apply(blast intro:le_SupI)
-done
+lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
+  by (auto intro: order_antisym SUP_leI le_SUPI)
 
-lemma Sup_leI: "(!!x. x:M \<Longrightarrow> x \<le> u) \<Longrightarrow> Sup M \<le> (u::'a::comp_lat)"
-apply(simp add:Sup_def)
-apply(rule Inf_lower)
-apply(blast)
-done
-
-
-lemma SUP_leI: "(!!i. M i \<le> u) \<Longrightarrow> (SUP i. M i) \<le> (u::'a::comp_lat)"
-apply(simp add:SUP_def)
-apply(blast intro!:Sup_leI)
-done
-
-lemma SUP_const[simp]: "(SUP i. M) = (M::'a::comp_lat)"
-by(simp add:SUP_def image_constant_conv sup_absorb1)
+lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (INF i:A. M) = M"
+  by (auto intro: order_antisym INF_leI le_INFI)
 
 
 subsection {* Some instances of the type class of complete lattices *}




