Sup now explicit parameter of complete_lattice
authorhaftmann
Mon Aug 20 18:07:29 2007 +0200 (2007-08-20)
changeset 2434586a3557a9ebb
parent 24344 a0fd8c2db293
child 24346 4f6b71b84ee7
Sup now explicit parameter of complete_lattice
src/HOL/Lattices.thy
src/HOL/Library/Graphs.thy
src/HOL/Predicate.thy
src/HOL/UNITY/Transformers.thy
src/HOL/ex/CTL.thy
     1.1 --- a/src/HOL/Lattices.thy	Mon Aug 20 18:07:28 2007 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Mon Aug 20 18:07:29 2007 +0200
     1.3 @@ -327,26 +327,21 @@
     1.4  
     1.5  class complete_lattice = lattice +
     1.6    fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
     1.7 +    and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
     1.8    assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
     1.9 -  assumes Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
    1.10 +     and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
    1.11 +  assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
    1.12 +     and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
    1.13  begin
    1.14  
    1.15 -definition
    1.16 -  Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
    1.17 -where
    1.18 -  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<^loc>\<le> b}"
    1.19 -
    1.20  lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<^loc>\<le> a}"
    1.21 -  unfolding Sup_def by (auto intro: Inf_greatest Inf_lower)
    1.22 +  by (auto intro: Inf_lower Inf_greatest Sup_upper Sup_least)
    1.23  
    1.24 -lemma Sup_upper: "x \<in> A \<Longrightarrow> x \<^loc>\<le> \<Squnion>A"
    1.25 -  by (auto simp: Sup_def intro: Inf_greatest)
    1.26 -
    1.27 -lemma Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<^loc>\<le> z) \<Longrightarrow> \<Squnion>A \<^loc>\<le> z"
    1.28 -  by (auto simp: Sup_def intro: Inf_lower)
    1.29 +lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<^loc>\<le> b}"
    1.30 +  by (auto intro: Inf_lower Inf_greatest Sup_upper Sup_least)
    1.31  
    1.32  lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}"
    1.33 -  unfolding Sup_def by auto
    1.34 +  unfolding Sup_Inf by auto
    1.35  
    1.36  lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}"
    1.37    unfolding Inf_Sup by auto
    1.38 @@ -367,7 +362,7 @@
    1.39    apply (erule Inf_lower)
    1.40    done
    1.41  
    1.42 -lemma Sup_insert [code func]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
    1.43 +lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
    1.44    apply (rule antisym)
    1.45    apply (rule Sup_least)
    1.46    apply (erule insertE)
    1.47 @@ -387,7 +382,7 @@
    1.48    "\<Sqinter>{a} = a"
    1.49    by (auto intro: antisym Inf_lower Inf_greatest)
    1.50  
    1.51 -lemma Sup_singleton [simp, code func]:
    1.52 +lemma Sup_singleton [simp]:
    1.53    "\<Squnion>{a} = a"
    1.54    by (auto intro: antisym Sup_upper Sup_least)
    1.55  
    1.56 @@ -491,23 +486,8 @@
    1.57  
    1.58  instance bool :: complete_lattice
    1.59    Inf_bool_def: "Inf A \<equiv> \<forall>x\<in>A. x"
    1.60 -  apply intro_classes
    1.61 -  apply (unfold Inf_bool_def)
    1.62 -  apply (iprover intro!: le_boolI elim: ballE)
    1.63 -  apply (iprover intro!: ballI le_boolI elim: ballE le_boolE)
    1.64 -  done
    1.65 -
    1.66 -theorem Sup_bool_eq: "Sup A \<longleftrightarrow> (\<exists>x\<in>A. x)"
    1.67 -  apply (rule order_antisym)
    1.68 -  apply (rule Sup_least)
    1.69 -  apply (rule le_boolI)
    1.70 -  apply (erule bexI, assumption)
    1.71 -  apply (rule le_boolI)
    1.72 -  apply (erule bexE)
    1.73 -  apply (rule le_boolE)
    1.74 -  apply (rule Sup_upper)
    1.75 -  apply assumption+
    1.76 -  done
    1.77 +  Sup_bool_def: "Sup A \<equiv> \<exists>x\<in>A. x"
    1.78 +  by intro_classes (auto simp add: Inf_bool_def Sup_bool_def le_bool_def)
    1.79  
    1.80  lemma Inf_empty_bool [simp]:
    1.81    "Inf {}"
    1.82 @@ -515,7 +495,7 @@
    1.83  
    1.84  lemma not_Sup_empty_bool [simp]:
    1.85    "\<not> Sup {}"
    1.86 -  unfolding Sup_def Inf_bool_def by auto
    1.87 +  unfolding Sup_bool_def by auto
    1.88  
    1.89  lemma top_bool_eq: "top = True"
    1.90    by (iprover intro!: order_antisym le_boolI top_greatest)
    1.91 @@ -541,17 +521,10 @@
    1.92  
    1.93  instance set :: (type) complete_lattice
    1.94    Inf_set_def: "Inf S \<equiv> \<Inter>S"
    1.95 -  by intro_classes (auto simp add: Inf_set_def)
    1.96 -
    1.97 -lemmas [code func del] = Inf_set_def
    1.98 +  Sup_set_def: "Sup S \<equiv> \<Union>S"
    1.99 +  by intro_classes (auto simp add: Inf_set_def Sup_set_def)
   1.100  
   1.101 -theorem Sup_set_eq: "Sup S = \<Union>S"
   1.102 -  apply (rule subset_antisym)
   1.103 -  apply (rule Sup_least)
   1.104 -  apply (erule Union_upper)
   1.105 -  apply (rule Union_least)
   1.106 -  apply (erule Sup_upper)
   1.107 -  done
   1.108 +lemmas [code func del] = Inf_set_def Sup_set_def
   1.109  
   1.110  lemma top_set_eq: "top = UNIV"
   1.111    by (iprover intro!: subset_antisym subset_UNIV top_greatest)
   1.112 @@ -581,36 +554,12 @@
   1.113  
   1.114  instance "fun" :: (type, complete_lattice) complete_lattice
   1.115    Inf_fun_def: "Inf A \<equiv> (\<lambda>x. Inf {y. \<exists>f\<in>A. y = f x})"
   1.116 -  apply intro_classes
   1.117 -  apply (unfold Inf_fun_def)
   1.118 -  apply (rule le_funI)
   1.119 -  apply (rule Inf_lower)
   1.120 -  apply (rule CollectI)
   1.121 -  apply (rule bexI)
   1.122 -  apply (rule refl)
   1.123 -  apply assumption
   1.124 -  apply (rule le_funI)
   1.125 -  apply (rule Inf_greatest)
   1.126 -  apply (erule CollectE)
   1.127 -  apply (erule bexE)
   1.128 -  apply (iprover elim: le_funE)
   1.129 -  done
   1.130 +  Sup_fun_def: "Sup A \<equiv> (\<lambda>x. Sup {y. \<exists>f\<in>A. y = f x})"
   1.131 +  by intro_classes
   1.132 +    (auto simp add: Inf_fun_def Sup_fun_def le_fun_def
   1.133 +      intro: Inf_lower Sup_upper Inf_greatest Sup_least)
   1.134  
   1.135 -lemmas [code func del] = Inf_fun_def
   1.136 -
   1.137 -theorem Sup_fun_eq: "Sup A = (\<lambda>x. Sup {y. \<exists>f\<in>A. y = f x})"
   1.138 -  apply (rule order_antisym)
   1.139 -  apply (rule Sup_least)
   1.140 -  apply (rule le_funI)
   1.141 -  apply (rule Sup_upper)
   1.142 -  apply fast
   1.143 -  apply (rule le_funI)
   1.144 -  apply (rule Sup_least)
   1.145 -  apply (erule CollectE)
   1.146 -  apply (erule bexE)
   1.147 -  apply (drule le_funD [OF Sup_upper])
   1.148 -  apply simp
   1.149 -  done
   1.150 +lemmas [code func del] = Inf_fun_def Sup_fun_def
   1.151  
   1.152  lemma Inf_empty_fun:
   1.153    "Inf {} = (\<lambda>_. Inf {})"
   1.154 @@ -618,11 +567,7 @@
   1.155  
   1.156  lemma Sup_empty_fun:
   1.157    "Sup {} = (\<lambda>_. Sup {})"
   1.158 -proof -
   1.159 -  have aux: "\<And>x. {y. \<exists>f. y = f x} = UNIV" by auto
   1.160 -  show ?thesis
   1.161 -  by (auto simp add: Sup_def Inf_fun_def Inf_binary inf_bool_eq aux)
   1.162 -qed
   1.163 +  by rule (auto simp add: Sup_fun_def)
   1.164  
   1.165  lemma top_fun_eq: "top = (\<lambda>x. top)"
   1.166    by (iprover intro!: order_antisym le_funI top_greatest)
     2.1 --- a/src/HOL/Library/Graphs.thy	Mon Aug 20 18:07:28 2007 +0200
     2.2 +++ b/src/HOL/Library/Graphs.thy	Mon Aug 20 18:07:29 2007 +0200
     2.3 @@ -81,6 +81,7 @@
     2.4    "inf G H \<equiv> Graph (dest_graph G \<inter> dest_graph H)"
     2.5    "sup G H \<equiv> G + H"
     2.6    Inf_graph_def: "Inf \<equiv> \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
     2.7 +  Sup_graph_def: "Sup \<equiv> \<lambda>Gs. Graph (\<Union>(dest_graph ` Gs))"
     2.8  proof
     2.9    fix x y z :: "('a,'b) graph"
    2.10    fix A :: "('a, 'b) graph set"
    2.11 @@ -121,10 +122,16 @@
    2.12  
    2.13    { assume "\<And>x. x \<in> A \<Longrightarrow> z \<le> x" thus "z \<le> Inf A"
    2.14      unfolding Inf_graph_def graph_leq_def by auto }
    2.15 +
    2.16 +  { assume "x \<in> A" thus "x \<le> Sup A" 
    2.17 +      unfolding Sup_graph_def graph_leq_def by auto }
    2.18 +
    2.19 +  { assume "\<And>x. x \<in> A \<Longrightarrow> x \<le> z" thus "Sup A \<le> z"
    2.20 +    unfolding Sup_graph_def graph_leq_def by auto }
    2.21  qed
    2.22  
    2.23  lemmas [code func del] = graph_leq_def graph_less_def
    2.24 -  inf_graph_def sup_graph_def Inf_graph_def
    2.25 +  inf_graph_def sup_graph_def Inf_graph_def Sup_graph_def
    2.26  
    2.27  lemma in_grplus:
    2.28    "has_edge (G + H) p b q = (has_edge G p b q \<or> has_edge H p b q)"
     3.1 --- a/src/HOL/Predicate.thy	Mon Aug 20 18:07:28 2007 +0200
     3.2 +++ b/src/HOL/Predicate.thy	Mon Aug 20 18:07:29 2007 +0200
     3.3 @@ -134,10 +134,10 @@
     3.4  subsection {* Unions of families *}
     3.5  
     3.6  lemma SUP1_iff [simp]: "(SUP x:A. B x) b = (EX x:A. B x b)"
     3.7 -  by (simp add: SUPR_def Sup_fun_eq Sup_bool_eq) blast
     3.8 +  by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast
     3.9  
    3.10  lemma SUP2_iff [simp]: "(SUP x:A. B x) b c = (EX x:A. B x b c)"
    3.11 -  by (simp add: SUPR_def Sup_fun_eq Sup_bool_eq) blast
    3.12 +  by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast
    3.13  
    3.14  lemma SUP1_I [intro]: "a : A ==> B a b ==> (SUP x:A. B x) b"
    3.15    by auto
     4.1 --- a/src/HOL/UNITY/Transformers.thy	Mon Aug 20 18:07:28 2007 +0200
     4.2 +++ b/src/HOL/UNITY/Transformers.thy	Mon Aug 20 18:07:29 2007 +0200
     4.3 @@ -88,7 +88,7 @@
     4.4  done
     4.5  
     4.6  lemma wens_Id [simp]: "wens F Id B = B"
     4.7 -by (simp add: wens_def gfp_def wp_def awp_def Sup_set_eq, blast)
     4.8 +by (simp add: wens_def gfp_def wp_def awp_def Sup_set_def, blast)
     4.9  
    4.10  text{*These two theorems justify the claim that @{term wens} returns the
    4.11  weakest assertion satisfying the ensures property*}
    4.12 @@ -101,7 +101,7 @@
    4.13  
    4.14  lemma wens_ensures: "act \<in> Acts F ==> F \<in> (wens F act B) ensures B"
    4.15  by (simp add: wens_def gfp_def constrains_def awp_def wp_def
    4.16 -              ensures_def transient_def Sup_set_eq, blast)
    4.17 +              ensures_def transient_def Sup_set_def, blast)
    4.18  
    4.19  text{*These two results constitute assertion (4.13) of the thesis*}
    4.20  lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B"
    4.21 @@ -110,7 +110,7 @@
    4.22  done
    4.23  
    4.24  lemma wens_weakening: "B \<subseteq> wens F act B"
    4.25 -by (simp add: wens_def gfp_def Sup_set_eq, blast)
    4.26 +by (simp add: wens_def gfp_def Sup_set_def, blast)
    4.27  
    4.28  text{*Assertion (6), or 4.16 in the thesis*}
    4.29  lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B" 
    4.30 @@ -120,7 +120,7 @@
    4.31  
    4.32  text{*Assertion 4.17 in the thesis*}
    4.33  lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A"
    4.34 -by (simp add: wens_def gfp_def wp_def awp_def constrains_def Sup_set_eq, blast)
    4.35 +by (simp add: wens_def gfp_def wp_def awp_def constrains_def Sup_set_def, blast)
    4.36    --{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff}
    4.37        is declared as an iff-rule, then it's almost impossible to prove. 
    4.38        One proof is via @{text meson} after expanding all definitions, but it's
    4.39 @@ -331,7 +331,7 @@
    4.40  
    4.41  lemma wens_single_eq:
    4.42       "wens (mk_program (init, {act}, allowed)) act B = B \<union> wp act B"
    4.43 -by (simp add: wens_def gfp_def wp_def Sup_set_eq, blast)
    4.44 +by (simp add: wens_def gfp_def wp_def Sup_set_def, blast)
    4.45  
    4.46  
    4.47  text{*Next, we express the @{term "wens_set"} for single-assignment programs*}
     5.1 --- a/src/HOL/ex/CTL.thy	Mon Aug 20 18:07:28 2007 +0200
     5.2 +++ b/src/HOL/ex/CTL.thy	Mon Aug 20 18:07:29 2007 +0200
     5.3 @@ -95,7 +95,7 @@
     5.4      proof
     5.5        assume "x \<in> gfp (\<lambda>s. - f (- s))"
     5.6        then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)"
     5.7 -	by (auto simp add: gfp_def Sup_set_eq)
     5.8 +	by (auto simp add: gfp_def Sup_set_def)
     5.9        then have "f (- u) \<subseteq> - u" by auto
    5.10        then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)
    5.11        from l and this have "x \<notin> u" by auto