--- a/NEWS Mon Sep 21 14:22:32 2009 +0200
+++ b/NEWS Mon Sep 21 14:23:12 2009 +0200
@@ -94,6 +94,8 @@
- mere abbreviations:
Set.empty (for bot)
Set.UNIV (for top)
+ Set.inter (for inf)
+ Set.union (for sup)
Complete_Lattice.Inter (for Inf)
Complete_Lattice.Union (for Sup)
Complete_Lattice.INTER (for INFI)
--- a/src/HOL/Finite_Set.thy Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/Finite_Set.thy Mon Sep 21 14:23:12 2009 +0200
@@ -1566,8 +1566,6 @@
prefer 2
apply assumption
apply auto
- apply (rule setsum_cong)
- apply auto
done
lemma setsum_right_distrib:
--- a/src/HOL/Hoare_Parallel/Gar_Coll.thy Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy Mon Sep 21 14:23:12 2009 +0200
@@ -253,7 +253,7 @@
\<and> ( \<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)}."
apply (unfold Propagate_Black_def PBInv_def Auxk_def collector_defs)
apply annhoare
-apply(simp_all add:Graph6 Graph7 Graph8 Graph12)
+apply(simp_all add: Graph6 Graph7 Graph8 Graph12)
apply force
apply force
apply force
@@ -297,8 +297,6 @@
apply(erule subset_psubset_trans)
apply(erule Graph11)
apply fast
---{* 3 subgoals left *}
-apply force
--{* 2 subgoals left *}
apply clarify
apply(simp add:Proper_Edges_def Graph6 Graph7 Graph8 Graph12)
--- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Mon Sep 21 14:23:12 2009 +0200
@@ -276,8 +276,6 @@
apply(force)
apply(force)
apply(rule disjI2, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
---{* 3 subgoals left *}
-apply force
--{* 2 subgoals left *}
apply clarify
apply(conjI_tac)
@@ -1235,9 +1233,9 @@
apply(unfold mul_modules mul_collector_defs mul_mutator_defs)
apply(tactic {* TRYALL (interfree_aux_tac) *})
--{* 76 subgoals left *}
-apply (clarify,simp add: nth_list_update)+
+apply (clarsimp simp add: nth_list_update)+
--{* 56 subgoals left *}
-apply(clarify,simp add:Mul_AppendInv_def Append_to_free0 nth_list_update)+
+apply (clarsimp simp add: Mul_AppendInv_def Append_to_free0 nth_list_update)+
done
subsubsection {* The Multi-Mutator Garbage Collection Algorithm *}
--- a/src/HOL/Hoare_Parallel/RG_Hoare.thy Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy Mon Sep 21 14:23:12 2009 +0200
@@ -4,8 +4,8 @@
subsection {* Proof System for Component Programs *}
-declare Un_subset_iff [iff del]
-declare Cons_eq_map_conv[iff]
+declare Un_subset_iff [simp del] le_sup_iff [simp del]
+declare Cons_eq_map_conv [iff]
constdefs
stable :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool"
--- a/src/HOL/Inductive.thy Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/Inductive.thy Mon Sep 21 14:23:12 2009 +0200
@@ -83,7 +83,7 @@
and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
shows "P(a)"
by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
- (auto simp: inf_set_eq intro: indhyp)
+ (auto simp: intro: indhyp)
lemma lfp_ordinal_induct:
fixes f :: "'a\<Colon>complete_lattice \<Rightarrow> 'a"
@@ -184,7 +184,7 @@
text{*strong version, thanks to Coen and Frost*}
lemma coinduct_set: "[| mono(f); a: X; X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)"
-by (blast intro: weak_coinduct [OF _ coinduct_lemma, simplified sup_set_eq])
+by (blast intro: weak_coinduct [OF _ coinduct_lemma])
lemma coinduct: "[| mono(f); X \<le> f (sup X (gfp f)) |] ==> X \<le> gfp(f)"
apply (rule order_trans)
--- a/src/HOL/Library/Euclidean_Space.thy Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy Mon Sep 21 14:23:12 2009 +0200
@@ -3649,10 +3649,7 @@
from setsum_restrict_set[OF fS, of "\<lambda>v. u v *s v" S', symmetric] SS'
have "setsum (\<lambda>v. ?u v *s v) S = setsum (\<lambda>v. u v *s v) S'"
unfolding cond_value_iff cond_application_beta
- apply (simp add: cond_value_iff cong del: if_weak_cong)
- apply (rule setsum_cong)
- apply auto
- done
+ by (simp add: cond_value_iff cong del: if_weak_cong)
hence "setsum (\<lambda>v. ?u v *s v) S = y" by (metis u)
hence "y \<in> ?rhs" by auto}
moreover
--- a/src/HOL/Library/Executable_Set.thy Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/Library/Executable_Set.thy Mon Sep 21 14:23:12 2009 +0200
@@ -12,6 +12,21 @@
declare member [code]
+definition empty :: "'a set" where
+ "empty = {}"
+
+declare empty_def [symmetric, code_unfold]
+
+definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+ "inter = op \<inter>"
+
+declare inter_def [symmetric, code_unfold]
+
+definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+ "union = op \<union>"
+
+declare union_def [symmetric, code_unfold]
+
definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
"subset = op \<le>"
@@ -69,7 +84,7 @@
Set ("\<module>Set")
consts_code
- "Set.empty" ("{*Fset.empty*}")
+ "empty" ("{*Fset.empty*}")
"List_Set.is_empty" ("{*Fset.is_empty*}")
"Set.insert" ("{*Fset.insert*}")
"List_Set.remove" ("{*Fset.remove*}")
@@ -77,8 +92,8 @@
"List_Set.project" ("{*Fset.filter*}")
"Ball" ("{*flip Fset.forall*}")
"Bex" ("{*flip Fset.exists*}")
- "op \<union>" ("{*Fset.union*}")
- "op \<inter>" ("{*Fset.inter*}")
+ "union" ("{*Fset.union*}")
+ "inter" ("{*Fset.inter*}")
"op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip Fset.subtract*}")
"Union" ("{*Fset.Union*}")
"Inter" ("{*Fset.Inter*}")
--- a/src/HOL/Library/Topology_Euclidean_Space.thy Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy Mon Sep 21 14:23:12 2009 +0200
@@ -99,11 +99,9 @@
lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B" by blast
lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U - S)"
- apply (auto simp add: closedin_def)
+ apply (auto simp add: closedin_def Diff_Diff_Int)
apply (metis openin_subset subset_eq)
- apply (auto simp add: Diff_Diff_Int)
- apply (subgoal_tac "topspace U \<inter> S = S")
- by auto
+ done
lemma openin_closedin: "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U - S))"
by (simp add: openin_closedin_eq)
--- a/src/HOL/MetisExamples/Message.thy Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/MetisExamples/Message.thy Mon Sep 21 14:23:12 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/MetisTest/Message.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Testing the metis method
@@ -711,17 +710,17 @@
proof (neg_clausify)
assume 0: "analz (synth H) \<noteq> analz H \<union> synth H"
have 1: "\<And>X1 X3. sup (analz (sup X3 X1)) (synth X3) = analz (sup (synth X3) X1)"
- by (metis analz_synth_Un sup_set_eq sup_set_eq sup_set_eq)
+ by (metis analz_synth_Un)
have 2: "sup (analz H) (synth H) \<noteq> analz (synth H)"
- by (metis 0 sup_set_eq)
+ by (metis 0)
have 3: "\<And>X1 X3. sup (synth X3) (analz (sup X3 X1)) = analz (sup (synth X3) X1)"
- by (metis 1 Un_commute sup_set_eq sup_set_eq)
+ by (metis 1 Un_commute)
have 4: "\<And>X3. sup (synth X3) (analz X3) = analz (sup (synth X3) {})"
- by (metis 3 Un_empty_right sup_set_eq)
+ by (metis 3 Un_empty_right)
have 5: "\<And>X3. sup (synth X3) (analz X3) = analz (synth X3)"
- by (metis 4 Un_empty_right sup_set_eq)
+ by (metis 4 Un_empty_right)
have 6: "\<And>X3. sup (analz X3) (synth X3) = analz (synth X3)"
- by (metis 5 Un_commute sup_set_eq sup_set_eq)
+ by (metis 5 Un_commute)
show "False"
by (metis 2 6)
qed
--- a/src/HOL/MetisExamples/set.thy Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/MetisExamples/set.thy Mon Sep 21 14:23:12 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/MetisExamples/set.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Testing the metis method
@@ -36,23 +35,23 @@
assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
have 6: "sup Y Z = X \<or> Y \<subseteq> X"
- by (metis 0 sup_set_eq)
+ by (metis 0)
have 7: "sup Y Z = X \<or> Z \<subseteq> X"
- by (metis 1 sup_set_eq)
+ by (metis 1)
have 8: "\<And>X3. sup Y Z = X \<or> X \<subseteq> X3 \<or> \<not> Y \<subseteq> X3 \<or> \<not> Z \<subseteq> X3"
- by (metis 5 sup_set_eq)
+ by (metis 5)
have 9: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
- by (metis 2 sup_set_eq)
+ by (metis 2)
have 10: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
- by (metis 3 sup_set_eq)
+ by (metis 3)
have 11: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
- by (metis 4 sup_set_eq)
+ by (metis 4)
have 12: "Z \<subseteq> X"
- by (metis Un_upper2 sup_set_eq 7)
+ by (metis Un_upper2 7)
have 13: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
- by (metis 8 Un_upper2 sup_set_eq)
+ by (metis 8 Un_upper2)
have 14: "Y \<subseteq> X"
- by (metis Un_upper1 sup_set_eq 6)
+ by (metis Un_upper1 6)
have 15: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
by (metis 10 12)
have 16: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
@@ -66,17 +65,17 @@
have 20: "Y \<subseteq> x \<or> sup Y Z \<noteq> X"
by (metis 16 14)
have 21: "sup Y Z = X \<or> X \<subseteq> sup Y Z"
- by (metis 13 Un_upper1 sup_set_eq)
+ by (metis 13 Un_upper1)
have 22: "sup Y Z = X \<or> \<not> sup Y Z \<subseteq> X"
by (metis equalityI 21)
have 23: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
- by (metis 22 Un_least sup_set_eq)
+ by (metis 22 Un_least)
have 24: "sup Y Z = X \<or> \<not> Y \<subseteq> X"
by (metis 23 12)
have 25: "sup Y Z = X"
by (metis 24 14)
have 26: "\<And>X3. X \<subseteq> X3 \<or> \<not> Z \<subseteq> X3 \<or> \<not> Y \<subseteq> X3"
- by (metis Un_least sup_set_eq 25)
+ by (metis Un_least 25)
have 27: "Y \<subseteq> x"
by (metis 20 25)
have 28: "Z \<subseteq> x"
@@ -105,31 +104,31 @@
assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
have 6: "sup Y Z = X \<or> Y \<subseteq> X"
- by (metis 0 sup_set_eq)
+ by (metis 0)
have 7: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
- by (metis 2 sup_set_eq)
+ by (metis 2)
have 8: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
- by (metis 4 sup_set_eq)
+ by (metis 4)
have 9: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
- by (metis 5 sup_set_eq Un_upper2 sup_set_eq)
+ by (metis 5 Un_upper2)
have 10: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
- by (metis 3 sup_set_eq Un_upper2 sup_set_eq sup_set_eq)
+ by (metis 3 Un_upper2)
have 11: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X"
- by (metis 8 Un_upper2 sup_set_eq sup_set_eq)
+ by (metis 8 Un_upper2)
have 12: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
- by (metis 10 Un_upper1 sup_set_eq)
+ by (metis 10 Un_upper1)
have 13: "sup Y Z = X \<or> X \<subseteq> sup Y Z"
- by (metis 9 Un_upper1 sup_set_eq)
+ by (metis 9 Un_upper1)
have 14: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
- by (metis equalityI 13 Un_least sup_set_eq)
+ by (metis equalityI 13 Un_least)
have 15: "sup Y Z = X"
- by (metis 14 sup_set_eq 1 sup_set_eq sup_set_eq 6)
+ by (metis 14 1 6)
have 16: "Y \<subseteq> x"
- by (metis 7 Un_upper2 sup_set_eq sup_set_eq Un_upper1 sup_set_eq 15)
+ by (metis 7 Un_upper2 Un_upper1 15)
have 17: "\<not> X \<subseteq> x"
- by (metis 11 Un_upper1 sup_set_eq 15)
+ by (metis 11 Un_upper1 15)
have 18: "X \<subseteq> x"
- by (metis Un_least sup_set_eq 15 12 15 16)
+ by (metis Un_least 15 12 15 16)
show "False"
by (metis 18 17)
qed
@@ -148,23 +147,23 @@
assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
have 6: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
- by (metis 3 sup_set_eq)
+ by (metis 3)
have 7: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
- by (metis 5 sup_set_eq Un_upper2 sup_set_eq)
+ by (metis 5 Un_upper2)
have 8: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
- by (metis 2 sup_set_eq Un_upper2 sup_set_eq sup_set_eq)
+ by (metis 2 Un_upper2)
have 9: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
- by (metis 6 Un_upper2 sup_set_eq sup_set_eq Un_upper1 sup_set_eq sup_set_eq)
+ by (metis 6 Un_upper2 Un_upper1)
have 10: "sup Y Z = X \<or> \<not> sup Y Z \<subseteq> X"
- by (metis equalityI 7 Un_upper1 sup_set_eq)
+ by (metis equalityI 7 Un_upper1)
have 11: "sup Y Z = X"
- by (metis 10 Un_least sup_set_eq sup_set_eq 1 sup_set_eq sup_set_eq 0 sup_set_eq)
+ by (metis 10 Un_least 1 0)
have 12: "Z \<subseteq> x"
by (metis 9 11)
have 13: "X \<subseteq> x"
- by (metis Un_least sup_set_eq 11 12 8 Un_upper1 sup_set_eq sup_set_eq 11)
+ by (metis Un_least 11 12 8 Un_upper1 11)
show "False"
- by (metis 13 4 sup_set_eq Un_upper2 sup_set_eq sup_set_eq Un_upper1 sup_set_eq sup_set_eq 11)
+ by (metis 13 4 Un_upper2 Un_upper1 11)
qed
(*Example included in TPHOLs paper*)
@@ -183,19 +182,19 @@
assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
have 6: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
- by (metis 4 sup_set_eq)
+ by (metis 4)
have 7: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
- by (metis 3 sup_set_eq Un_upper2 sup_set_eq sup_set_eq)
+ by (metis 3 Un_upper2)
have 8: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
- by (metis 7 Un_upper1 sup_set_eq sup_set_eq)
+ by (metis 7 Un_upper1)
have 9: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
- by (metis equalityI 5 sup_set_eq Un_upper2 sup_set_eq Un_upper1 sup_set_eq Un_least sup_set_eq)
+ by (metis equalityI 5 Un_upper2 Un_upper1 Un_least)
have 10: "Y \<subseteq> x"
- by (metis 2 sup_set_eq Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 9 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq)
+ by (metis 2 Un_upper2 1 Un_upper1 0 9 Un_upper2 1 Un_upper1 0)
have 11: "X \<subseteq> x"
- by (metis Un_least sup_set_eq 9 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 8 9 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 10)
+ by (metis Un_least 9 Un_upper2 1 Un_upper1 0 8 9 Un_upper2 1 Un_upper1 0 10)
show "False"
- by (metis 11 6 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 9 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq)
+ by (metis 11 6 Un_upper2 1 Un_upper1 0 9 Un_upper2 1 Un_upper1 0)
qed
ML {*AtpWrapper.problem_name := "set__equal_union"*}
@@ -238,7 +237,7 @@
lemma (*singleton_example_2:*)
"\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
-by (metis Set.subsetI Union_upper insert_code mem_def set_eq_subset)
+by (metis Set.subsetI Union_upper insert_iff set_eq_subset)
lemma singleton_example_2:
"\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
--- a/src/HOL/Set.thy Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/Set.thy Mon Sep 21 14:23:12 2009 +0200
@@ -652,8 +652,8 @@
subsubsection {* Binary union -- Un *}
-definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
- sup_set_eq [symmetric]: "A Un B = sup A B"
+abbreviation union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
+ "op Un \<equiv> sup"
notation (xsymbols)
union (infixl "\<union>" 65)
@@ -663,7 +663,7 @@
lemma Un_def:
"A \<union> B = {x. x \<in> A \<or> x \<in> B}"
- by (simp add: sup_fun_eq sup_bool_eq sup_set_eq [symmetric] Collect_def mem_def)
+ by (simp add: sup_fun_eq sup_bool_eq Collect_def mem_def)
lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"
by (unfold Un_def) blast
@@ -689,15 +689,13 @@
by (simp add: Collect_def mem_def insert_compr Un_def)
lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
- apply (fold sup_set_eq)
- apply (erule mono_sup)
- done
+ by (fact mono_sup)
subsubsection {* Binary intersection -- Int *}
-definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
- inf_set_eq [symmetric]: "A Int B = inf A B"
+abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
+ "op Int \<equiv> inf"
notation (xsymbols)
inter (infixl "\<inter>" 70)
@@ -707,7 +705,7 @@
lemma Int_def:
"A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
- by (simp add: inf_fun_eq inf_bool_eq inf_set_eq [symmetric] Collect_def mem_def)
+ by (simp add: inf_fun_eq inf_bool_eq Collect_def mem_def)
lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
by (unfold Int_def) blast
@@ -725,9 +723,7 @@
by simp
lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
- apply (fold inf_set_eq)
- apply (erule mono_inf)
- done
+ by (fact mono_inf)
subsubsection {* Set difference *}
--- a/src/HOL/Tools/Function/fundef_lib.ML Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_lib.ML Mon Sep 21 14:23:12 2009 +0200
@@ -170,7 +170,7 @@
end
(* instance for unions *)
-fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Set.union}
+fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Lattices.sup}
(map (fn t => t RS eq_reflection) (@{thms Un_ac} @
@{thms Un_empty_right} @
@{thms Un_empty_left})) t
--- a/src/HOL/Tools/Function/termination.ML Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/Tools/Function/termination.ML Mon Sep 21 14:23:12 2009 +0200
@@ -145,7 +145,7 @@
fun mk_sum_skel rel =
let
- val cs = FundefLib.dest_binop_list @{const_name Set.union} rel
+ val cs = FundefLib.dest_binop_list @{const_name Lattices.sup} rel
fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
let
val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
@@ -233,7 +233,7 @@
fun CALLS tac i st =
if Thm.no_prems st then all_tac st
else case Thm.term_of (Thm.cprem_of st i) of
- (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name Set.union} rel, i) st
+ (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name Lattices.sup} rel, i) st
|_ => no_tac st
type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
@@ -293,7 +293,7 @@
if null ineqs then
Const (@{const_name Set.empty}, fastype_of rel)
else
- foldr1 (HOLogic.mk_binop @{const_name Set.union}) (map mk_compr ineqs)
+ foldr1 (HOLogic.mk_binop @{const_name Lattices.sup}) (map mk_compr ineqs)
fun solve_membership_tac i =
(EVERY' (replicate (i - 2) (rtac @{thm UnI2})) (* pick the right component of the union *)
--- a/src/HOL/Tools/inductive_set.ML Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/Tools/inductive_set.ML Mon Sep 21 14:23:12 2009 +0200
@@ -74,8 +74,8 @@
in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
(p (fold (Logic.all o Var) vs t) f)
end;
- fun mkop "op &" T x = SOME (Const (@{const_name Set.inter}, T --> T --> T), x)
- | mkop "op |" T x = SOME (Const (@{const_name Set.union}, T --> T --> T), x)
+ fun mkop "op &" T x = SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x)
+ | mkop "op |" T x = SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x)
| mkop _ _ _ = NONE;
fun mk_collect p T t =
let val U = HOLogic.dest_setT T
--- a/src/HOL/UNITY/Follows.thy Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/UNITY/Follows.thy Mon Sep 21 14:23:12 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/UNITY/Follows
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
*)
@@ -160,7 +159,7 @@
lemma Follows_Un:
"[| F \<in> f' Fols f; F \<in> g' Fols g |]
==> F \<in> (%s. (f' s) \<union> (g' s)) Fols (%s. (f s) \<union> (g s))"
-apply (simp add: Follows_def Increasing_Un Always_Un del: Un_subset_iff, auto)
+apply (simp add: Follows_def Increasing_Un Always_Un del: Un_subset_iff le_sup_iff, auto)
apply (rule LeadsTo_Trans)
apply (blast intro: Follows_Un_lemma)
(*Weakening is used to exchange Un's arguments*)
--- a/src/HOL/UNITY/UNITY_Main.thy Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/UNITY/UNITY_Main.thy Mon Sep 21 14:23:12 2009 +0200
@@ -1,13 +1,14 @@
(* Title: HOL/UNITY/UNITY_Main.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 2003 University of Cambridge
*)
header{*Comprehensive UNITY Theory*}
-theory UNITY_Main imports Detects PPROD Follows ProgressSets
-uses "UNITY_tactics.ML" begin
+theory UNITY_Main
+imports Detects PPROD Follows ProgressSets
+uses "UNITY_tactics.ML"
+begin
method_setup safety = {*
Scan.succeed (fn ctxt =>
--- a/src/HOL/ex/predicate_compile.ML Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Mon Sep 21 14:23:12 2009 +0200
@@ -2152,7 +2152,7 @@
val (ts, _) = Predicate.yieldn k t;
val elemsT = HOLogic.mk_set T ts;
in if k = ~1 orelse length ts < k then elemsT
- else Const (@{const_name Set.union}, setT --> setT --> setT) $ elemsT $ t_compr
+ else Const (@{const_name Lattices.sup}, setT --> setT --> setT) $ elemsT $ t_compr
end;
fun values_cmd modes k raw_t state =