--- 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)
--- 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)"
--- 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
--- 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*}
--- 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