# HG changeset patch
# User haftmann
# Date 1187626049 -7200
# Node ID 86a3557a9ebbd9a9cb3f9f95e4ee7b6ef4a56ebb
# Parent  a0fd8c2db29364c9b398bb8db089bcc581b82b3a
Sup now explicit parameter of complete_lattice

diff -r a0fd8c2db293 -r 86a3557a9ebb src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Mon Aug 20 18:07:28 2007 +0200
+++ b/src/HOL/Lattices.thy	Mon Aug 20 18:07:29 2007 +0200
@@ -327,26 +327,21 @@
 
 class complete_lattice = lattice +
   fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
+    and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
   assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
-  assumes Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
+     and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
+  assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
+     and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
 begin
 
-definition
-  Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
-where
-  "\<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)
+  by (auto intro: Inf_lower Inf_greatest Sup_upper Sup_least)
 
-lemma Sup_upper: "x \<in> A \<Longrightarrow> x \<^loc>\<le> \<Squnion>A"
-  by (auto simp: Sup_def intro: Inf_greatest)
-
-lemma Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<^loc>\<le> z) \<Longrightarrow> \<Squnion>A \<^loc>\<le> z"
-  by (auto simp: Sup_def intro: Inf_lower)
+lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<^loc>\<le> b}"
+  by (auto intro: Inf_lower Inf_greatest Sup_upper Sup_least)
 
 lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}"
-  unfolding Sup_def by auto
+  unfolding Sup_Inf by auto
 
 lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}"
   unfolding Inf_Sup by auto
@@ -367,7 +362,7 @@
   apply (erule Inf_lower)
   done
 
-lemma Sup_insert [code func]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
+lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
   apply (rule antisym)
   apply (rule Sup_least)
   apply (erule insertE)
@@ -387,7 +382,7 @@
   "\<Sqinter>{a} = a"
   by (auto intro: antisym Inf_lower Inf_greatest)
 
-lemma Sup_singleton [simp, code func]:
+lemma Sup_singleton [simp]:
   "\<Squnion>{a} = a"
   by (auto intro: antisym Sup_upper Sup_least)
 
@@ -491,23 +486,8 @@
 
 instance bool :: complete_lattice
   Inf_bool_def: "Inf A \<equiv> \<forall>x\<in>A. x"
-  apply intro_classes
-  apply (unfold Inf_bool_def)
-  apply (iprover intro!: le_boolI elim: ballE)
-  apply (iprover intro!: ballI le_boolI elim: ballE le_boolE)
-  done
-
-theorem Sup_bool_eq: "Sup A \<longleftrightarrow> (\<exists>x\<in>A. x)"
-  apply (rule order_antisym)
-  apply (rule Sup_least)
-  apply (rule le_boolI)
-  apply (erule bexI, assumption)
-  apply (rule le_boolI)
-  apply (erule bexE)
-  apply (rule le_boolE)
-  apply (rule Sup_upper)
-  apply assumption+
-  done
+  Sup_bool_def: "Sup A \<equiv> \<exists>x\<in>A. x"
+  by intro_classes (auto simp add: Inf_bool_def Sup_bool_def le_bool_def)
 
 lemma Inf_empty_bool [simp]:
   "Inf {}"
@@ -515,7 +495,7 @@
 
 lemma not_Sup_empty_bool [simp]:
   "\<not> Sup {}"
-  unfolding Sup_def Inf_bool_def by auto
+  unfolding Sup_bool_def by auto
 
 lemma top_bool_eq: "top = True"
   by (iprover intro!: order_antisym le_boolI top_greatest)
@@ -541,17 +521,10 @@
 
 instance set :: (type) complete_lattice
   Inf_set_def: "Inf S \<equiv> \<Inter>S"
-  by intro_classes (auto simp add: Inf_set_def)
-
-lemmas [code func del] = Inf_set_def
+  Sup_set_def: "Sup S \<equiv> \<Union>S"
+  by intro_classes (auto simp add: Inf_set_def Sup_set_def)
 
-theorem Sup_set_eq: "Sup S = \<Union>S"
-  apply (rule subset_antisym)
-  apply (rule Sup_least)
-  apply (erule Union_upper)
-  apply (rule Union_least)
-  apply (erule Sup_upper)
-  done
+lemmas [code func del] = Inf_set_def Sup_set_def
 
 lemma top_set_eq: "top = UNIV"
   by (iprover intro!: subset_antisym subset_UNIV top_greatest)
@@ -581,36 +554,12 @@
 
 instance "fun" :: (type, complete_lattice) complete_lattice
   Inf_fun_def: "Inf A \<equiv> (\<lambda>x. Inf {y. \<exists>f\<in>A. y = f x})"
-  apply intro_classes
-  apply (unfold Inf_fun_def)
-  apply (rule le_funI)
-  apply (rule Inf_lower)
-  apply (rule CollectI)
-  apply (rule bexI)
-  apply (rule refl)
-  apply assumption
-  apply (rule le_funI)
-  apply (rule Inf_greatest)
-  apply (erule CollectE)
-  apply (erule bexE)
-  apply (iprover elim: le_funE)
-  done
+  Sup_fun_def: "Sup A \<equiv> (\<lambda>x. Sup {y. \<exists>f\<in>A. y = f x})"
+  by intro_classes
+    (auto simp add: Inf_fun_def Sup_fun_def le_fun_def
+      intro: Inf_lower Sup_upper Inf_greatest Sup_least)
 
-lemmas [code func del] = Inf_fun_def
-
-theorem Sup_fun_eq: "Sup A = (\<lambda>x. Sup {y. \<exists>f\<in>A. y = f x})"
-  apply (rule order_antisym)
-  apply (rule Sup_least)
-  apply (rule le_funI)
-  apply (rule Sup_upper)
-  apply fast
-  apply (rule le_funI)
-  apply (rule Sup_least)
-  apply (erule CollectE)
-  apply (erule bexE)
-  apply (drule le_funD [OF Sup_upper])
-  apply simp
-  done
+lemmas [code func del] = Inf_fun_def Sup_fun_def
 
 lemma Inf_empty_fun:
   "Inf {} = (\<lambda>_. Inf {})"
@@ -618,11 +567,7 @@
 
 lemma Sup_empty_fun:
   "Sup {} = (\<lambda>_. Sup {})"
-proof -
-  have aux: "\<And>x. {y. \<exists>f. y = f x} = UNIV" by auto
-  show ?thesis
-  by (auto simp add: Sup_def Inf_fun_def Inf_binary inf_bool_eq aux)
-qed
+  by rule (auto simp add: Sup_fun_def)
 
 lemma top_fun_eq: "top = (\<lambda>x. top)"
   by (iprover intro!: order_antisym le_funI top_greatest)
diff -r a0fd8c2db293 -r 86a3557a9ebb src/HOL/Library/Graphs.thy
--- a/src/HOL/Library/Graphs.thy	Mon Aug 20 18:07:28 2007 +0200
+++ b/src/HOL/Library/Graphs.thy	Mon Aug 20 18:07:29 2007 +0200
@@ -81,6 +81,7 @@
   "inf G H \<equiv> Graph (dest_graph G \<inter> dest_graph H)"
   "sup G H \<equiv> G + H"
   Inf_graph_def: "Inf \<equiv> \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
+  Sup_graph_def: "Sup \<equiv> \<lambda>Gs. Graph (\<Union>(dest_graph ` Gs))"
 proof
   fix x y z :: "('a,'b) graph"
   fix A :: "('a, 'b) graph set"
@@ -121,10 +122,16 @@
 
   { assume "\<And>x. x \<in> A \<Longrightarrow> z \<le> x" thus "z \<le> Inf A"
     unfolding Inf_graph_def graph_leq_def by auto }
+
+  { assume "x \<in> A" thus "x \<le> Sup A" 
+      unfolding Sup_graph_def graph_leq_def by auto }
+
+  { assume "\<And>x. x \<in> A \<Longrightarrow> x \<le> z" thus "Sup A \<le> z"
+    unfolding Sup_graph_def graph_leq_def by auto }
 qed
 
 lemmas [code func del] = graph_leq_def graph_less_def
-  inf_graph_def sup_graph_def Inf_graph_def
+  inf_graph_def sup_graph_def Inf_graph_def Sup_graph_def
 
 lemma in_grplus:
   "has_edge (G + H) p b q = (has_edge G p b q \<or> has_edge H p b q)"
diff -r a0fd8c2db293 -r 86a3557a9ebb src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Mon Aug 20 18:07:28 2007 +0200
+++ b/src/HOL/Predicate.thy	Mon Aug 20 18:07:29 2007 +0200
@@ -134,10 +134,10 @@
 subsection {* Unions of families *}
 
 lemma SUP1_iff [simp]: "(SUP x:A. B x) b = (EX x:A. B x b)"
-  by (simp add: SUPR_def Sup_fun_eq Sup_bool_eq) blast
+  by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast
 
 lemma SUP2_iff [simp]: "(SUP x:A. B x) b c = (EX x:A. B x b c)"
-  by (simp add: SUPR_def Sup_fun_eq Sup_bool_eq) blast
+  by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast
 
 lemma SUP1_I [intro]: "a : A ==> B a b ==> (SUP x:A. B x) b"
   by auto
diff -r a0fd8c2db293 -r 86a3557a9ebb src/HOL/UNITY/Transformers.thy
--- a/src/HOL/UNITY/Transformers.thy	Mon Aug 20 18:07:28 2007 +0200
+++ b/src/HOL/UNITY/Transformers.thy	Mon Aug 20 18:07:29 2007 +0200
@@ -88,7 +88,7 @@
 done
 
 lemma wens_Id [simp]: "wens F Id B = B"
-by (simp add: wens_def gfp_def wp_def awp_def Sup_set_eq, blast)
+by (simp add: wens_def gfp_def wp_def awp_def Sup_set_def, blast)
 
 text{*These two theorems justify the claim that @{term wens} returns the
 weakest assertion satisfying the ensures property*}
@@ -101,7 +101,7 @@
 
 lemma wens_ensures: "act \<in> Acts F ==> F \<in> (wens F act B) ensures B"
 by (simp add: wens_def gfp_def constrains_def awp_def wp_def
-              ensures_def transient_def Sup_set_eq, blast)
+              ensures_def transient_def Sup_set_def, blast)
 
 text{*These two results constitute assertion (4.13) of the thesis*}
 lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B"
@@ -110,7 +110,7 @@
 done
 
 lemma wens_weakening: "B \<subseteq> wens F act B"
-by (simp add: wens_def gfp_def Sup_set_eq, blast)
+by (simp add: wens_def gfp_def Sup_set_def, blast)
 
 text{*Assertion (6), or 4.16 in the thesis*}
 lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B" 
@@ -120,7 +120,7 @@
 
 text{*Assertion 4.17 in the thesis*}
 lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A"
-by (simp add: wens_def gfp_def wp_def awp_def constrains_def Sup_set_eq, blast)
+by (simp add: wens_def gfp_def wp_def awp_def constrains_def Sup_set_def, blast)
   --{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff}
       is declared as an iff-rule, then it's almost impossible to prove. 
       One proof is via @{text meson} after expanding all definitions, but it's
@@ -331,7 +331,7 @@
 
 lemma wens_single_eq:
      "wens (mk_program (init, {act}, allowed)) act B = B \<union> wp act B"
-by (simp add: wens_def gfp_def wp_def Sup_set_eq, blast)
+by (simp add: wens_def gfp_def wp_def Sup_set_def, blast)
 
 
 text{*Next, we express the @{term "wens_set"} for single-assignment programs*}
diff -r a0fd8c2db293 -r 86a3557a9ebb src/HOL/ex/CTL.thy
--- a/src/HOL/ex/CTL.thy	Mon Aug 20 18:07:28 2007 +0200
+++ b/src/HOL/ex/CTL.thy	Mon Aug 20 18:07:29 2007 +0200
@@ -95,7 +95,7 @@
     proof
       assume "x \<in> gfp (\<lambda>s. - f (- s))"
       then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)"
-	by (auto simp add: gfp_def Sup_set_eq)
+	by (auto simp add: gfp_def Sup_set_def)
       then have "f (- u) \<subseteq> - u" by auto
       then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)
       from l and this have "x \<notin> u" by auto