--- a/NEWS Mon Sep 21 15:33:40 2009 +0200
+++ b/NEWS Mon Sep 21 15:35:24 2009 +0200
@@ -94,13 +94,18 @@
- 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)
Complete_Lattice.UNION (for SUPR)
- object-logic definitions as far as appropriate
- INCOMPATIBILITY.
+INCOMPATIBILITY. Care is required when theorems Int_subset_iff or
+Un_subset_iff are explicitly deleted as default simp rules; then
+also their lattice counterparts le_inf_iff and le_sup_iff have to be
+deleted to achieve the desired effect.
* Power operations on relations and functions are now one dedicate
constant "compow" with infix syntax "^^". Power operations on
--- a/src/HOL/Algebra/FiniteProduct.thy Mon Sep 21 15:33:40 2009 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy Mon Sep 21 15:35:24 2009 +0200
@@ -212,7 +212,7 @@
apply (induct set: finite)
apply simp
apply (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb
- Int_mono2 Un_subset_iff)
+ Int_mono2)
done
lemma (in LCD) foldD_nest_Un_disjoint:
@@ -274,14 +274,14 @@
apply (simp add: AC insert_absorb Int_insert_left
LCD.foldD_insert [OF LCD.intro [of D]]
LCD.foldD_closed [OF LCD.intro [of D]]
- Int_mono2 Un_subset_iff)
+ Int_mono2)
done
lemma (in ACeD) foldD_Un_disjoint:
"[| finite A; finite B; A Int B = {}; A \<subseteq> D; B \<subseteq> D |] ==>
foldD D f e (A Un B) = foldD D f e A \<cdot> foldD D f e B"
by (simp add: foldD_Un_Int
- left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff)
+ left_commute LCD.foldD_closed [OF LCD.intro [of D]])
subsubsection {* Products over Finite Sets *}
@@ -377,7 +377,7 @@
from insert have A: "g \<in> A -> carrier G" by fast
from insert A a show ?case
by (simp add: m_ac Int_insert_left insert_absorb finprod_closed
- Int_mono2 Un_subset_iff)
+ Int_mono2)
qed
lemma finprod_Un_disjoint:
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy Mon Sep 21 15:33:40 2009 +0200
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy Mon Sep 21 15:35:24 2009 +0200
@@ -1747,7 +1747,7 @@
have "assigns (In1l e2) \<subseteq> dom (locals (store s2))"
by (simp add: need_second_arg_def)
with s2
- show ?thesis using False by (simp add: Un_subset_iff)
+ show ?thesis using False by simp
qed
next
case Super thus ?case by simp
--- a/src/HOL/Bali/TypeSafe.thy Mon Sep 21 15:33:40 2009 +0200
+++ b/src/HOL/Bali/TypeSafe.thy Mon Sep 21 15:35:24 2009 +0200
@@ -2953,7 +2953,7 @@
by simp
from da_e1 s0_s1 True obtain E1' where
"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e1\<guillemotright> E1'"
- by - (rule da_weakenE, auto iff del: Un_subset_iff)
+ by - (rule da_weakenE, auto iff del: Un_subset_iff le_sup_iff)
with conf_s1 wt_e1
obtain
"s2\<Colon>\<preceq>(G, L)"
@@ -2972,7 +2972,7 @@
by simp
from da_e2 s0_s1 False obtain E2' where
"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e2\<guillemotright> E2'"
- by - (rule da_weakenE, auto iff del: Un_subset_iff)
+ by - (rule da_weakenE, auto iff del: Un_subset_iff le_sup_iff)
with conf_s1 wt_e2
obtain
"s2\<Colon>\<preceq>(G, L)"
--- a/src/HOL/Finite_Set.thy Mon Sep 21 15:33:40 2009 +0200
+++ b/src/HOL/Finite_Set.thy Mon Sep 21 15:35:24 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 15:33:40 2009 +0200
+++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy Mon Sep 21 15:35:24 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 15:33:40 2009 +0200
+++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Mon Sep 21 15:35:24 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 15:33:40 2009 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy Mon Sep 21 15:35:24 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 15:33:40 2009 +0200
+++ b/src/HOL/Inductive.thy Mon Sep 21 15:35:24 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 15:33:40 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy Mon Sep 21 15:35:24 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 15:33:40 2009 +0200
+++ b/src/HOL/Library/Executable_Set.thy Mon Sep 21 15:35:24 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 15:33:40 2009 +0200
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy Mon Sep 21 15:35:24 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 15:33:40 2009 +0200
+++ b/src/HOL/MetisExamples/Message.thy Mon Sep 21 15:35:24 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 15:33:40 2009 +0200
+++ b/src/HOL/MetisExamples/set.thy Mon Sep 21 15:35:24 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/MicroJava/BV/Typing_Framework_JVM.thy Mon Sep 21 15:33:40 2009 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Mon Sep 21 15:35:24 2009 +0200
@@ -140,7 +140,7 @@
apply fastsimp
apply (erule disjE)
- apply (clarsimp simp add: Un_subset_iff)
+ apply clarsimp
apply (drule method_wf_mdecl, assumption+)
apply (clarsimp simp add: wf_mdecl_def wf_mhead_def)
apply fastsimp
--- a/src/HOL/Set.thy Mon Sep 21 15:33:40 2009 +0200
+++ b/src/HOL/Set.thy Mon Sep 21 15:35:24 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 15:33:40 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_lib.ML Mon Sep 21 15:35:24 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 15:33:40 2009 +0200
+++ b/src/HOL/Tools/Function/termination.ML Mon Sep 21 15:35:24 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 15:33:40 2009 +0200
+++ b/src/HOL/Tools/inductive_set.ML Mon Sep 21 15:35:24 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 15:33:40 2009 +0200
+++ b/src/HOL/UNITY/Follows.thy Mon Sep 21 15:35:24 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/ProgressSets.thy Mon Sep 21 15:33:40 2009 +0200
+++ b/src/HOL/UNITY/ProgressSets.thy Mon Sep 21 15:35:24 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/UNITY/ProgressSets
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 2003 University of Cambridge
@@ -245,7 +244,7 @@
then have "cl C (T\<inter>?r) \<subseteq> ?r"
by (blast intro!: subset_wens)
then have cl_subset: "cl C (T\<inter>?r) \<subseteq> T\<inter>?r"
- by (simp add: Int_subset_iff cl_ident TC
+ by (simp add: cl_ident TC
subset_trans [OF cl_mono [OF Int_lower1]])
show ?thesis
by (rule cl_subset_in_lattice [OF cl_subset latt])
@@ -486,7 +485,7 @@
shows "closed F T B L"
apply (simp add: closed_def, clarify)
apply (rule ProgressSets.cl_subset_in_lattice [OF _ lattice])
-apply (simp add: Int_Un_distrib cl_Un [OF lattice] Un_subset_iff
+apply (simp add: Int_Un_distrib cl_Un [OF lattice]
cl_ident Int_in_lattice [OF TL BL lattice] Un_upper1)
apply (subgoal_tac "cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))")
prefer 2
--- a/src/HOL/UNITY/Simple/Common.thy Mon Sep 21 15:33:40 2009 +0200
+++ b/src/HOL/UNITY/Simple/Common.thy Mon Sep 21 15:35:24 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/UNITY/Common
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
@@ -10,7 +9,9 @@
From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
*)
-theory Common imports "../UNITY_Main" begin
+theory Common
+imports "../UNITY_Main"
+begin
consts
ftime :: "nat=>nat"
--- a/src/HOL/UNITY/Transformers.thy Mon Sep 21 15:33:40 2009 +0200
+++ b/src/HOL/UNITY/Transformers.thy Mon Sep 21 15:35:24 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/UNITY/Transformers
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 2003 University of Cambridge
@@ -133,7 +132,7 @@
apply (drule constrains_Un [OF Diff_wens_constrains [of F act A]])
apply (simp add: Un_Int_distrib2 Compl_partition2)
apply (erule constrains_weaken, blast)
-apply (simp add: Un_subset_iff wens_weakening)
+apply (simp add: wens_weakening)
done
text{*Assertion 4.20 in the thesis.*}
@@ -151,7 +150,7 @@
"[|T-B \<subseteq> awp F T; act \<in> Acts F|]
==> T \<inter> wens F act B = T \<inter> wens F act (T\<inter>B)"
apply (rule equalityI)
- apply (simp_all add: Int_lower1 Int_subset_iff)
+ apply (simp_all add: Int_lower1)
apply (rule wens_Int_eq_lemma, assumption+)
apply (rule subset_trans [OF _ wens_mono [of "T\<inter>B" B]], auto)
done
@@ -176,7 +175,7 @@
apply (drule_tac act1=act and A1=X
in constrains_Un [OF Diff_wens_constrains])
apply (erule constrains_weaken, blast)
- apply (simp add: Un_subset_iff wens_weakening)
+ apply (simp add: wens_weakening)
apply (rule constrains_weaken)
apply (rule_tac I=W and A="\<lambda>v. v-B" and A'="\<lambda>v. v" in constrains_UN, blast+)
done
@@ -229,7 +228,7 @@
apply (subgoal_tac "(T \<inter> wens F act B) - B \<subseteq>
wp act B \<inter> awp F (B \<union> wens F act B) \<inter> awp F T")
apply (rule subset_wens)
- apply (simp add: awp_Join_eq awp_Int_eq Int_subset_iff Un_commute)
+ apply (simp add: awp_Join_eq awp_Int_eq Un_commute)
apply (simp add: awp_def wp_def, blast)
apply (insert wens_subset [of F act B], blast)
done
@@ -253,7 +252,7 @@
apply (blast dest: wens_mono intro: wens_Join_subset [THEN subsetD], simp)
apply (rule equalityI)
prefer 2 apply blast
-apply (simp add: Int_lower1 Int_subset_iff)
+apply (simp add: Int_lower1)
apply (frule wens_set_imp_subset)
apply (subgoal_tac "T-X \<subseteq> awp F T")
prefer 2 apply (blast intro: awpF [THEN subsetD])
@@ -347,7 +346,7 @@
"single_valued act
==> wens_single act B \<union> wp act (wens_single act B) = wens_single act B"
apply (rule equalityI)
- apply (simp_all add: Un_upper1 Un_subset_iff)
+ apply (simp_all add: Un_upper1)
apply (simp add: wens_single_def wp_UN_eq, clarify)
apply (rule_tac a="Suc(i)" in UN_I, auto)
done
--- a/src/HOL/UNITY/UNITY_Main.thy Mon Sep 21 15:33:40 2009 +0200
+++ b/src/HOL/UNITY/UNITY_Main.thy Mon Sep 21 15:35:24 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/UNITY/WFair.thy Mon Sep 21 15:33:40 2009 +0200
+++ b/src/HOL/UNITY/WFair.thy Mon Sep 21 15:35:24 2009 +0200
@@ -113,7 +113,7 @@
lemma totalize_transient_iff:
"(totalize F \<in> transient A) = (\<exists>act\<in>Acts F. A \<subseteq> Domain act & act``A \<subseteq> -A)"
apply (simp add: totalize_def totalize_act_def transient_def
- Un_Image Un_subset_iff, safe)
+ Un_Image, safe)
apply (blast intro!: rev_bexI)+
done
--- a/src/HOL/ex/predicate_compile.ML Mon Sep 21 15:33:40 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Mon Sep 21 15:35:24 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 =