# HG changeset patch # User haftmann # Date 1253541720 -7200 # Node ID 46a20c74bd91e8857a71e9cfb5b8275f6f83737d # Parent 55a0be42327c5c281ba9acc2aa0a7bb9dbddae66# Parent 66ae4e8b1309ce19e9cc8c97902c69d301bd0b3f merged diff -r 55a0be42327c -r 46a20c74bd91 NEWS --- a/NEWS Mon Sep 21 16:01:38 2009 +0200 +++ b/NEWS Mon Sep 21 16:02:00 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 diff -r 55a0be42327c -r 46a20c74bd91 src/HOL/Algebra/FiniteProduct.thy --- a/src/HOL/Algebra/FiniteProduct.thy Mon Sep 21 16:01:38 2009 +0200 +++ b/src/HOL/Algebra/FiniteProduct.thy Mon Sep 21 16:02:00 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 \ D; B \ D |] ==> foldD D f e (A Un B) = foldD D f e A \ 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 \ 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: diff -r 55a0be42327c -r 46a20c74bd91 src/HOL/Auth/Guard/Extensions.thy --- a/src/HOL/Auth/Guard/Extensions.thy Mon Sep 21 16:01:38 2009 +0200 +++ b/src/HOL/Auth/Guard/Extensions.thy Mon Sep 21 16:02:00 2009 +0200 @@ -11,7 +11,9 @@ header {*Extensions to Standard Theories*} -theory Extensions imports "../Event" begin +theory Extensions +imports "../Event" +begin subsection{*Extensions to Theory @{text Set}*} @@ -173,7 +175,7 @@ subsubsection{*lemmas on analz*} lemma analz_UnI1 [intro]: "X:analz G ==> X:analz (G Un H)" -by (subgoal_tac "G <= G Un H", auto dest: analz_mono) + by (subgoal_tac "G <= G Un H") (blast dest: analz_mono)+ lemma analz_sub: "[| X:analz G; G <= H |] ==> X:analz H" by (auto dest: analz_mono) diff -r 55a0be42327c -r 46a20c74bd91 src/HOL/Bali/DefiniteAssignmentCorrect.thy --- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy Mon Sep 21 16:01:38 2009 +0200 +++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy Mon Sep 21 16:02:00 2009 +0200 @@ -1747,7 +1747,7 @@ have "assigns (In1l e2) \ 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 diff -r 55a0be42327c -r 46a20c74bd91 src/HOL/Bali/TypeSafe.thy --- a/src/HOL/Bali/TypeSafe.thy Mon Sep 21 16:01:38 2009 +0200 +++ b/src/HOL/Bali/TypeSafe.thy Mon Sep 21 16:02:00 2009 +0200 @@ -2953,7 +2953,7 @@ by simp from da_e1 s0_s1 True obtain E1' where "\prg=G,cls=accC,lcl=L\\ (dom (locals (store s1)))\In1l e1\ 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\\(G, L)" @@ -2972,7 +2972,7 @@ by simp from da_e2 s0_s1 False obtain E2' where "\prg=G,cls=accC,lcl=L\\ (dom (locals (store s1)))\In1l e2\ 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\\(G, L)" diff -r 55a0be42327c -r 46a20c74bd91 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Mon Sep 21 16:01:38 2009 +0200 +++ b/src/HOL/Finite_Set.thy Mon Sep 21 16:02:00 2009 +0200 @@ -1566,8 +1566,6 @@ prefer 2 apply assumption apply auto - apply (rule setsum_cong) - apply auto done lemma setsum_right_distrib: diff -r 55a0be42327c -r 46a20c74bd91 src/HOL/Hoare_Parallel/Gar_Coll.thy --- a/src/HOL/Hoare_Parallel/Gar_Coll.thy Mon Sep 21 16:01:38 2009 +0200 +++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy Mon Sep 21 16:02:00 2009 +0200 @@ -253,7 +253,7 @@ \ ( \obc < Blacks \M \ \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) diff -r 55a0be42327c -r 46a20c74bd91 src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy --- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Mon Sep 21 16:01:38 2009 +0200 +++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Mon Sep 21 16:02:00 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 *} diff -r 55a0be42327c -r 46a20c74bd91 src/HOL/Hoare_Parallel/RG_Hoare.thy --- a/src/HOL/Hoare_Parallel/RG_Hoare.thy Mon Sep 21 16:01:38 2009 +0200 +++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy Mon Sep 21 16:02:00 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 \ ('a \ 'a) set \ bool" diff -r 55a0be42327c -r 46a20c74bd91 src/HOL/Inductive.thy --- a/src/HOL/Inductive.thy Mon Sep 21 16:01:38 2009 +0200 +++ b/src/HOL/Inductive.thy Mon Sep 21 16:02:00 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\complete_lattice \ 'a" @@ -184,7 +184,7 @@ text{*strong version, thanks to Coen and Frost*} lemma coinduct_set: "[| mono(f); a: X; X \ 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 \ f (sup X (gfp f)) |] ==> X \ gfp(f)" apply (rule order_trans) diff -r 55a0be42327c -r 46a20c74bd91 src/HOL/Library/Euclidean_Space.thy --- a/src/HOL/Library/Euclidean_Space.thy Mon Sep 21 16:01:38 2009 +0200 +++ b/src/HOL/Library/Euclidean_Space.thy Mon Sep 21 16:02:00 2009 +0200 @@ -3649,10 +3649,7 @@ from setsum_restrict_set[OF fS, of "\v. u v *s v" S', symmetric] SS' have "setsum (\v. ?u v *s v) S = setsum (\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 (\v. ?u v *s v) S = y" by (metis u) hence "y \ ?rhs" by auto} moreover diff -r 55a0be42327c -r 46a20c74bd91 src/HOL/Library/Executable_Set.thy --- a/src/HOL/Library/Executable_Set.thy Mon Sep 21 16:01:38 2009 +0200 +++ b/src/HOL/Library/Executable_Set.thy Mon Sep 21 16:02:00 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 \ 'a set \ 'a set" where + "inter = op \" + +declare inter_def [symmetric, code_unfold] + +definition union :: "'a set \ 'a set \ 'a set" where + "union = op \" + +declare union_def [symmetric, code_unfold] + definition subset :: "'a set \ 'a set \ bool" where "subset = op \" @@ -69,7 +84,7 @@ Set ("\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 \" ("{*Fset.union*}") - "op \" ("{*Fset.inter*}") + "union" ("{*Fset.union*}") + "inter" ("{*Fset.inter*}") "op - \ 'a set \ 'a set \ 'a set" ("{*flip Fset.subtract*}") "Union" ("{*Fset.Union*}") "Inter" ("{*Fset.Inter*}") diff -r 55a0be42327c -r 46a20c74bd91 src/HOL/Library/Topology_Euclidean_Space.thy --- a/src/HOL/Library/Topology_Euclidean_Space.thy Mon Sep 21 16:01:38 2009 +0200 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy Mon Sep 21 16:02:00 2009 +0200 @@ -99,11 +99,9 @@ lemma Diff_Diff_Int: "A - (A - B) = A \ B" by blast lemma openin_closedin_eq: "openin U S \ S \ topspace U \ 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 \ S = S") - by auto + done lemma openin_closedin: "S \ topspace U \ (openin U S \ closedin U (topspace U - S))" by (simp add: openin_closedin_eq) diff -r 55a0be42327c -r 46a20c74bd91 src/HOL/MetisExamples/Message.thy --- a/src/HOL/MetisExamples/Message.thy Mon Sep 21 16:01:38 2009 +0200 +++ b/src/HOL/MetisExamples/Message.thy Mon Sep 21 16:02:00 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) \ analz H \ synth H" have 1: "\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) \ analz (synth H)" - by (metis 0 sup_set_eq) + by (metis 0) have 3: "\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: "\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: "\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: "\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 diff -r 55a0be42327c -r 46a20c74bd91 src/HOL/MetisExamples/set.thy --- a/src/HOL/MetisExamples/set.thy Mon Sep 21 16:01:38 2009 +0200 +++ b/src/HOL/MetisExamples/set.thy Mon Sep 21 16:02:00 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: "(\ Y \ X \ \ Z \ X \ \ X \ x) \ X \ Y \ Z" assume 5: "\V. ((\ Y \ V \ \ Z \ V) \ X \ V) \ X = Y \ Z" have 6: "sup Y Z = X \ Y \ X" - by (metis 0 sup_set_eq) + by (metis 0) have 7: "sup Y Z = X \ Z \ X" - by (metis 1 sup_set_eq) + by (metis 1) have 8: "\X3. sup Y Z = X \ X \ X3 \ \ Y \ X3 \ \ Z \ X3" - by (metis 5 sup_set_eq) + by (metis 5) have 9: "Y \ x \ sup Y Z \ X \ \ Y \ X \ \ Z \ X" - by (metis 2 sup_set_eq) + by (metis 2) have 10: "Z \ x \ sup Y Z \ X \ \ Y \ X \ \ Z \ X" - by (metis 3 sup_set_eq) + by (metis 3) have 11: "sup Y Z \ X \ \ X \ x \ \ Y \ X \ \ Z \ X" - by (metis 4 sup_set_eq) + by (metis 4) have 12: "Z \ X" - by (metis Un_upper2 sup_set_eq 7) + by (metis Un_upper2 7) have 13: "\X3. sup Y Z = X \ X \ sup X3 Z \ \ Y \ sup X3 Z" - by (metis 8 Un_upper2 sup_set_eq) + by (metis 8 Un_upper2) have 14: "Y \ X" - by (metis Un_upper1 sup_set_eq 6) + by (metis Un_upper1 6) have 15: "Z \ x \ sup Y Z \ X \ \ Y \ X" by (metis 10 12) have 16: "Y \ x \ sup Y Z \ X \ \ Y \ X" @@ -66,17 +65,17 @@ have 20: "Y \ x \ sup Y Z \ X" by (metis 16 14) have 21: "sup Y Z = X \ X \ sup Y Z" - by (metis 13 Un_upper1 sup_set_eq) + by (metis 13 Un_upper1) have 22: "sup Y Z = X \ \ sup Y Z \ X" by (metis equalityI 21) have 23: "sup Y Z = X \ \ Z \ X \ \ Y \ X" - by (metis 22 Un_least sup_set_eq) + by (metis 22 Un_least) have 24: "sup Y Z = X \ \ Y \ X" by (metis 23 12) have 25: "sup Y Z = X" by (metis 24 14) have 26: "\X3. X \ X3 \ \ Z \ X3 \ \ Y \ X3" - by (metis Un_least sup_set_eq 25) + by (metis Un_least 25) have 27: "Y \ x" by (metis 20 25) have 28: "Z \ x" @@ -105,31 +104,31 @@ assume 4: "(\ Y \ X \ \ Z \ X \ \ X \ x) \ X \ Y \ Z" assume 5: "\V. ((\ Y \ V \ \ Z \ V) \ X \ V) \ X = Y \ Z" have 6: "sup Y Z = X \ Y \ X" - by (metis 0 sup_set_eq) + by (metis 0) have 7: "Y \ x \ sup Y Z \ X \ \ Y \ X \ \ Z \ X" - by (metis 2 sup_set_eq) + by (metis 2) have 8: "sup Y Z \ X \ \ X \ x \ \ Y \ X \ \ Z \ X" - by (metis 4 sup_set_eq) + by (metis 4) have 9: "\X3. sup Y Z = X \ X \ sup X3 Z \ \ Y \ sup X3 Z" - by (metis 5 sup_set_eq Un_upper2 sup_set_eq) + by (metis 5 Un_upper2) have 10: "Z \ x \ sup Y Z \ X \ \ Y \ 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 \ X \ \ X \ x \ \ Y \ X" - by (metis 8 Un_upper2 sup_set_eq sup_set_eq) + by (metis 8 Un_upper2) have 12: "Z \ x \ sup Y Z \ X" - by (metis 10 Un_upper1 sup_set_eq) + by (metis 10 Un_upper1) have 13: "sup Y Z = X \ X \ sup Y Z" - by (metis 9 Un_upper1 sup_set_eq) + by (metis 9 Un_upper1) have 14: "sup Y Z = X \ \ Z \ X \ \ Y \ 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 \ 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: "\ X \ x" - by (metis 11 Un_upper1 sup_set_eq 15) + by (metis 11 Un_upper1 15) have 18: "X \ 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: "(\ Y \ X \ \ Z \ X \ \ X \ x) \ X \ Y \ Z" assume 5: "\V. ((\ Y \ V \ \ Z \ V) \ X \ V) \ X = Y \ Z" have 6: "Z \ x \ sup Y Z \ X \ \ Y \ X \ \ Z \ X" - by (metis 3 sup_set_eq) + by (metis 3) have 7: "\X3. sup Y Z = X \ X \ sup X3 Z \ \ Y \ sup X3 Z" - by (metis 5 sup_set_eq Un_upper2 sup_set_eq) + by (metis 5 Un_upper2) have 8: "Y \ x \ sup Y Z \ X \ \ Y \ X" - by (metis 2 sup_set_eq Un_upper2 sup_set_eq sup_set_eq) + by (metis 2 Un_upper2) have 9: "Z \ x \ sup Y Z \ 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 \ \ sup Y Z \ 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 \ x" by (metis 9 11) have 13: "X \ 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: "(\ Y \ X \ \ Z \ X \ \ X \ x) \ X \ Y \ Z" assume 5: "\V. ((\ Y \ V \ \ Z \ V) \ X \ V) \ X = Y \ Z" have 6: "sup Y Z \ X \ \ X \ x \ \ Y \ X \ \ Z \ X" - by (metis 4 sup_set_eq) + by (metis 4) have 7: "Z \ x \ sup Y Z \ X \ \ Y \ X" - by (metis 3 sup_set_eq Un_upper2 sup_set_eq sup_set_eq) + by (metis 3 Un_upper2) have 8: "Z \ x \ sup Y Z \ X" - by (metis 7 Un_upper1 sup_set_eq sup_set_eq) + by (metis 7 Un_upper1) have 9: "sup Y Z = X \ \ Z \ X \ \ Y \ 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 \ 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 \ 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:*) "\x \ S. \S \ x \ \z. S \ {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: "\x \ S. \S \ x \ \z. S \ {z}" diff -r 55a0be42327c -r 46a20c74bd91 src/HOL/MicroJava/BV/Typing_Framework_JVM.thy --- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Mon Sep 21 16:01:38 2009 +0200 +++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Mon Sep 21 16:02:00 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 diff -r 55a0be42327c -r 46a20c74bd91 src/HOL/Set.thy --- a/src/HOL/Set.thy Mon Sep 21 16:01:38 2009 +0200 +++ b/src/HOL/Set.thy Mon Sep 21 16:02:00 2009 +0200 @@ -652,8 +652,8 @@ subsubsection {* Binary union -- Un *} -definition union :: "'a set \ 'a set \ 'a set" (infixl "Un" 65) where - sup_set_eq [symmetric]: "A Un B = sup A B" +abbreviation union :: "'a set \ 'a set \ 'a set" (infixl "Un" 65) where + "op Un \ sup" notation (xsymbols) union (infixl "\" 65) @@ -663,7 +663,7 @@ lemma Un_def: "A \ B = {x. x \ A \ x \ 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 \ f A \ f B \ f (A \ B)" - apply (fold sup_set_eq) - apply (erule mono_sup) - done + by (fact mono_sup) subsubsection {* Binary intersection -- Int *} -definition inter :: "'a set \ 'a set \ 'a set" (infixl "Int" 70) where - inf_set_eq [symmetric]: "A Int B = inf A B" +abbreviation inter :: "'a set \ 'a set \ 'a set" (infixl "Int" 70) where + "op Int \ inf" notation (xsymbols) inter (infixl "\" 70) @@ -707,7 +705,7 @@ lemma Int_def: "A \ B = {x. x \ A \ x \ 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 \ f (A \ B) \ f A \ f B" - apply (fold inf_set_eq) - apply (erule mono_inf) - done + by (fact mono_inf) subsubsection {* Set difference *} diff -r 55a0be42327c -r 46a20c74bd91 src/HOL/Tools/Function/fundef_lib.ML --- a/src/HOL/Tools/Function/fundef_lib.ML Mon Sep 21 16:01:38 2009 +0200 +++ b/src/HOL/Tools/Function/fundef_lib.ML Mon Sep 21 16:02:00 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 diff -r 55a0be42327c -r 46a20c74bd91 src/HOL/Tools/Function/termination.ML --- a/src/HOL/Tools/Function/termination.ML Mon Sep 21 16:01:38 2009 +0200 +++ b/src/HOL/Tools/Function/termination.ML Mon Sep 21 16:02:00 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 *) diff -r 55a0be42327c -r 46a20c74bd91 src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Mon Sep 21 16:01:38 2009 +0200 +++ b/src/HOL/Tools/inductive_set.ML Mon Sep 21 16:02:00 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 diff -r 55a0be42327c -r 46a20c74bd91 src/HOL/UNITY/Follows.thy --- a/src/HOL/UNITY/Follows.thy Mon Sep 21 16:01:38 2009 +0200 +++ b/src/HOL/UNITY/Follows.thy Mon Sep 21 16:02:00 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 \ f' Fols f; F \ g' Fols g |] ==> F \ (%s. (f' s) \ (g' s)) Fols (%s. (f s) \ (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*) diff -r 55a0be42327c -r 46a20c74bd91 src/HOL/UNITY/ProgressSets.thy --- a/src/HOL/UNITY/ProgressSets.thy Mon Sep 21 16:01:38 2009 +0200 +++ b/src/HOL/UNITY/ProgressSets.thy Mon Sep 21 16:02:00 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\?r) \ ?r" by (blast intro!: subset_wens) then have cl_subset: "cl C (T\?r) \ T\?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 \ wp act M) \ T \ (B \ wp act (cl L (T \ M)))") prefer 2 diff -r 55a0be42327c -r 46a20c74bd91 src/HOL/UNITY/Simple/Common.thy --- a/src/HOL/UNITY/Simple/Common.thy Mon Sep 21 16:01:38 2009 +0200 +++ b/src/HOL/UNITY/Simple/Common.thy Mon Sep 21 16:02:00 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" diff -r 55a0be42327c -r 46a20c74bd91 src/HOL/UNITY/Transformers.thy --- a/src/HOL/UNITY/Transformers.thy Mon Sep 21 16:01:38 2009 +0200 +++ b/src/HOL/UNITY/Transformers.thy Mon Sep 21 16:02:00 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 \ awp F T; act \ Acts F|] ==> T \ wens F act B = T \ wens F act (T\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\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="\v. v-B" and A'="\v. v" in constrains_UN, blast+) done @@ -229,7 +228,7 @@ apply (subgoal_tac "(T \ wens F act B) - B \ wp act B \ awp F (B \ wens F act B) \ 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 \ awp F T") prefer 2 apply (blast intro: awpF [THEN subsetD]) @@ -347,7 +346,7 @@ "single_valued act ==> wens_single act B \ 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 diff -r 55a0be42327c -r 46a20c74bd91 src/HOL/UNITY/UNITY_Main.thy --- a/src/HOL/UNITY/UNITY_Main.thy Mon Sep 21 16:01:38 2009 +0200 +++ b/src/HOL/UNITY/UNITY_Main.thy Mon Sep 21 16:02:00 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 => diff -r 55a0be42327c -r 46a20c74bd91 src/HOL/UNITY/WFair.thy --- a/src/HOL/UNITY/WFair.thy Mon Sep 21 16:01:38 2009 +0200 +++ b/src/HOL/UNITY/WFair.thy Mon Sep 21 16:02:00 2009 +0200 @@ -113,7 +113,7 @@ lemma totalize_transient_iff: "(totalize F \ transient A) = (\act\Acts F. A \ Domain act & act``A \ -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 diff -r 55a0be42327c -r 46a20c74bd91 src/HOL/ex/predicate_compile.ML --- a/src/HOL/ex/predicate_compile.ML Mon Sep 21 16:01:38 2009 +0200 +++ b/src/HOL/ex/predicate_compile.ML Mon Sep 21 16:02:00 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 =