--- a/NEWS Wed Sep 16 13:03:03 2009 +0200
+++ b/NEWS Wed Sep 16 13:43:15 2009 +0200
@@ -41,14 +41,6 @@
semidefinite programming solvers. For more information and examples
see src/HOL/Library/Sum_Of_Squares.
-* Set.UNIV and Set.empty are mere abbreviations for top and bot.
-INCOMPATIBILITY.
-
-* More convenient names for set intersection and union.
-INCOMPATIBILITY:
- Set.Int ~> Set.inter
- Set.Un ~> Set.union
-
* Code generator attributes follow the usual underscore convention:
code_unfold replaces code unfold
code_post replaces code post
@@ -57,16 +49,14 @@
* New class "boolean_algebra".
-* Refinements to lattices classes:
- - added boolean_algebra type class
+* Refinements to lattice classes and sets:
- less default intro/elim rules in locale variant, more default
intro/elim rules in class variant: more uniformity
- lemma ge_sup_conv renamed to le_sup_iff, in accordance with le_inf_iff
- dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and sup_aci)
- renamed ACI to inf_sup_aci
- class "complete_lattice" moved to separate theory "complete_lattice";
- corresponding constants renamed:
-
+ corresponding constants (and abbreviations) renamed:
Set.Inf ~> Complete_Lattice.Inf
Set.Sup ~> Complete_Lattice.Sup
Set.INFI ~> Complete_Lattice.INFI
@@ -75,6 +65,14 @@
Set.Union ~> Complete_Lattice.Union
Set.INTER ~> Complete_Lattice.INTER
Set.UNION ~> Complete_Lattice.UNION
+ - more convenient names for set intersection and union:
+ Set.Int ~> Set.inter
+ Set.Un ~> Set.union
+ - mere abbreviations:
+ Set.empty (for bot)
+ Set.UNIV (for top)
+ Complete_Lattice.Inter (for Inf)
+ Complete_Lattice.Union (for Sup)
INCOMPATIBILITY.
@@ -87,7 +85,7 @@
INCOMPATIBILITY.
* Power operations on relations and functions are now one dedicate
-constant compow with infix syntax "^^". Power operations on
+constant "compow" with infix syntax "^^". Power operations on
multiplicative monoids retains syntax "^" and is now defined generic
in class power. INCOMPATIBILITY.
--- a/src/HOL/Complete_Lattice.thy Wed Sep 16 13:03:03 2009 +0200
+++ b/src/HOL/Complete_Lattice.thy Wed Sep 16 13:43:15 2009 +0200
@@ -203,8 +203,8 @@
subsection {* Union *}
-definition Union :: "'a set set \<Rightarrow> 'a set" where
- Sup_set_eq [symmetric]: "Union S = \<Squnion>S"
+abbreviation Union :: "'a set set \<Rightarrow> 'a set" where
+ "Union S \<equiv> \<Squnion>S"
notation (xsymbols)
Union ("\<Union>_" [90] 90)
@@ -216,7 +216,7 @@
have "(\<exists>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<exists>B\<in>A. x \<in> B)"
by auto
then show "x \<in> \<Union>A \<longleftrightarrow> x \<in> {x. \<exists>B\<in>A. x \<in> B}"
- by (simp add: Sup_set_eq [symmetric] Sup_fun_def Sup_bool_def) (simp add: mem_def)
+ by (simp add: Sup_fun_def Sup_bool_def) (simp add: mem_def)
qed
lemma Union_iff [simp, noatp]:
@@ -314,7 +314,7 @@
lemma UNION_eq_Union_image:
"(\<Union>x\<in>A. B x) = \<Union>(B`A)"
- by (simp add: SUPR_def SUPR_set_eq [symmetric] Sup_set_eq)
+ by (simp add: SUPR_def SUPR_set_eq [symmetric])
lemma Union_def:
"\<Union>S = (\<Union>x\<in>S. x)"
@@ -439,8 +439,8 @@
subsection {* Inter *}
-definition Inter :: "'a set set \<Rightarrow> 'a set" where
- Inf_set_eq [symmetric]: "Inter S = \<Sqinter>S"
+abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where
+ "Inter S \<equiv> \<Sqinter>S"
notation (xsymbols)
Inter ("\<Inter>_" [90] 90)
@@ -452,7 +452,7 @@
have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)"
by auto
then show "x \<in> \<Inter>A \<longleftrightarrow> x \<in> {x. \<forall>B \<in> A. x \<in> B}"
- by (simp add: Inf_fun_def Inf_bool_def Inf_set_eq [symmetric]) (simp add: mem_def)
+ by (simp add: Inf_fun_def Inf_bool_def) (simp add: mem_def)
qed
lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
@@ -541,7 +541,7 @@
lemma INTER_eq_Inter_image:
"(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
- by (simp add: INFI_def INFI_set_eq [symmetric] Inf_set_eq)
+ by (simp add: INFI_def INFI_set_eq [symmetric])
lemma Inter_def:
"\<Inter>S = (\<Inter>x\<in>S. x)"
--- a/src/HOL/Inductive.thy Wed Sep 16 13:03:03 2009 +0200
+++ b/src/HOL/Inductive.thy Wed Sep 16 13:43:15 2009 +0200
@@ -111,8 +111,7 @@
and P_f: "!!S. P S ==> P(f S)"
and P_Union: "!!M. !S:M. P S ==> P(Union M)"
shows "P(lfp f)"
- using assms unfolding Sup_set_eq [symmetric]
- by (rule lfp_ordinal_induct [where P=P])
+ using assms by (rule lfp_ordinal_induct [where P=P])
text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct},
--- a/src/HOL/Library/Executable_Set.thy Wed Sep 16 13:03:03 2009 +0200
+++ b/src/HOL/Library/Executable_Set.thy Wed Sep 16 13:43:15 2009 +0200
@@ -8,7 +8,7 @@
imports Main Fset
begin
-subsection {* Derived set operations *}
+subsection {* Preprocessor setup *}
declare member [code]
@@ -24,9 +24,7 @@
definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
[code del]: "eq_set = op ="
-(* FIXME allow for Stefan's code generator:
-declare set_eq_subset[code_unfold]
-*)
+(*declare eq_set_def [symmetric, code_unfold]*)
lemma [code]:
"eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
@@ -37,13 +35,20 @@
declare Inter_image_eq [symmetric, code]
declare Union_image_eq [symmetric, code]
-
-subsection {* Rewrites for primitive operations *}
-
declare List_Set.project_def [symmetric, code_unfold]
+definition Inter :: "'a set set \<Rightarrow> 'a set" where
+ "Inter = Complete_Lattice.Inter"
-subsection {* code generator setup *}
+declare Inter_def [symmetric, code_unfold]
+
+definition Union :: "'a set set \<Rightarrow> 'a set" where
+ "Union = Complete_Lattice.Union"
+
+declare Union_def [symmetric, code_unfold]
+
+
+subsection {* Code generator setup *}
ML {*
nonfix inter;
@@ -75,8 +80,8 @@
"op \<union>" ("{*Fset.union*}")
"op \<inter>" ("{*Fset.inter*}")
"op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip Fset.subtract*}")
- "Complete_Lattice.Union" ("{*Fset.Union*}")
- "Complete_Lattice.Inter" ("{*Fset.Inter*}")
+ "Union" ("{*Fset.Union*}")
+ "Inter" ("{*Fset.Inter*}")
card ("{*Fset.card*}")
fold ("{*foldl o flip*}")
--- a/src/HOL/Nominal/Examples/Class.thy Wed Sep 16 13:03:03 2009 +0200
+++ b/src/HOL/Nominal/Examples/Class.thy Wed Sep 16 13:43:15 2009 +0200
@@ -11134,7 +11134,6 @@
shows "pi1\<bullet>(lfp f) = lfp (pi1\<bullet>f)"
and "pi2\<bullet>(lfp g) = lfp (pi2\<bullet>g)"
apply(simp add: lfp_def)
-apply(simp add: Inf_set_eq)
apply(simp add: big_inter_eqvt)
apply(simp add: pt_Collect_eqvt[OF pt_name_inst, OF at_name_inst])
apply(subgoal_tac "{u. (pi1\<bullet>f) u \<subseteq> u} = {u. ((rev pi1)\<bullet>((pi1\<bullet>f) u)) \<subseteq> ((rev pi1)\<bullet>u)}")
@@ -11146,7 +11145,6 @@
apply(drule subseteq_eqvt(1)[THEN iffD2])
apply(simp add: perm_bool)
apply(simp add: lfp_def)
-apply(simp add: Inf_set_eq)
apply(simp add: big_inter_eqvt)
apply(simp add: pt_Collect_eqvt[OF pt_coname_inst, OF at_coname_inst])
apply(subgoal_tac "{u. (pi2\<bullet>g) u \<subseteq> u} = {u. ((rev pi2)\<bullet>((pi2\<bullet>g) u)) \<subseteq> ((rev pi2)\<bullet>u)}")
--- a/src/HOL/UNITY/Transformers.thy Wed Sep 16 13:03:03 2009 +0200
+++ b/src/HOL/UNITY/Transformers.thy Wed Sep 16 13:43:15 2009 +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, 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, 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, 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, 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, blast)
text{*Next, we express the @{term "wens_set"} for single-assignment programs*}
--- a/src/HOL/ex/CTL.thy Wed Sep 16 13:03:03 2009 +0200
+++ b/src/HOL/ex/CTL.thy Wed Sep 16 13:43:15 2009 +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)
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