# HG changeset patch # User wenzelm # Date 1329840557 -3600 # Node ID e5438c5797ae799e9030c1d9cf377cf9fdac1c20 # Parent ae9286f64574c620366c63bc3aef595d14905297 tuned proofs; diff -r ae9286f64574 -r e5438c5797ae src/HOL/UNITY/Comp/Alloc.thy --- a/src/HOL/UNITY/Comp/Alloc.thy Tue Feb 21 17:08:32 2012 +0100 +++ b/src/HOL/UNITY/Comp/Alloc.thy Tue Feb 21 17:09:17 2012 +0100 @@ -537,8 +537,6 @@ declare ask_inv_client_map_drop_map [simp] -declare finite_lessThan [iff] - text{*Client : *} lemmas client_spec_simps = client_spec_def client_increasing_def client_bounded_def diff -r ae9286f64574 -r e5438c5797ae src/HOL/UNITY/Comp/Progress.thy --- a/src/HOL/UNITY/Comp/Progress.thy Tue Feb 21 17:08:32 2012 +0100 +++ b/src/HOL/UNITY/Comp/Progress.thy Tue Feb 21 17:09:17 2012 +0100 @@ -13,10 +13,10 @@ text{*Thesis Section 4.4.2*} definition FF :: "int program" where - "FF == mk_total_program (UNIV, {range (\x. (x, x+1))}, UNIV)" + "FF = mk_total_program (UNIV, {range (\x. (x, x+1))}, UNIV)" definition GG :: "int program" where - "GG == mk_total_program (UNIV, {range (\x. (x, 2*x))}, UNIV)" + "GG = mk_total_program (UNIV, {range (\x. (x, 2*x))}, UNIV)" subsubsection {*Calculating @{term "wens_set FF (atLeast k)"}*} diff -r ae9286f64574 -r e5438c5797ae src/HOL/UNITY/ELT.thy --- a/src/HOL/UNITY/ELT.thy Tue Feb 21 17:08:32 2012 +0100 +++ b/src/HOL/UNITY/ELT.thy Tue Feb 21 17:09:17 2012 +0100 @@ -166,7 +166,7 @@ apply (erule leadsETo_induct) prefer 3 apply (blast intro: leadsETo_Union) prefer 2 apply (blast intro: leadsETo_Trans) -apply (blast intro: leadsETo_Basis) +apply blast done lemma leadsETo_Trans_Un: @@ -237,7 +237,7 @@ lemma leadsETo_givenBy: "[| F : A leadsTo[CC] A'; CC <= givenBy v |] ==> F : A leadsTo[givenBy v] A'" -by (blast intro: empty_mem_givenBy leadsETo_weaken) +by (blast intro: leadsETo_weaken) (*Set difference*) @@ -340,7 +340,7 @@ apply (blast intro: e_psp_stable2 [THEN leadsETo_weaken_L] leadsETo_Trans) apply (rule leadsETo_Basis) apply (auto simp add: Diff_eq_empty_iff [THEN iffD2] - Int_Diff ensures_def givenBy_eq_Collect Join_transient) + Int_Diff ensures_def givenBy_eq_Collect) prefer 3 apply (blast intro: transient_strengthen) apply (drule_tac [2] P1 = P in preserves_subset_stable [THEN subsetD]) apply (drule_tac P1 = P in preserves_subset_stable [THEN subsetD]) @@ -454,7 +454,7 @@ lemma lel_lemma: "F : A leadsTo B ==> F : (reachable F Int A) leadsTo[Pow(reachable F)] B" apply (erule leadsTo_induct) - apply (blast intro: reachable_ensures leadsETo_Basis) + apply (blast intro: reachable_ensures) apply (blast dest: e_psp_stable2 intro: leadsETo_Trans leadsETo_weaken_L) apply (subst Int_Union) apply (blast intro: leadsETo_UN) @@ -491,7 +491,7 @@ ==> extend h F : (extend_set h A) leadsTo[extend_set h ` CC] (extend_set h B)" apply (erule leadsETo_induct) - apply (force intro: leadsETo_Basis subset_imp_ensures + apply (force intro: subset_imp_ensures simp add: extend_ensures extend_set_Diff_distrib [symmetric]) apply (blast intro: leadsETo_Trans) apply (simp add: leadsETo_UN extend_set_Union) diff -r ae9286f64574 -r e5438c5797ae src/HOL/UNITY/Extend.thy --- a/src/HOL/UNITY/Extend.thy Tue Feb 21 17:08:32 2012 +0100 +++ b/src/HOL/UNITY/Extend.thy Tue Feb 21 17:09:17 2012 +0100 @@ -370,9 +370,7 @@ lemma (in Extend) Allowed_extend: "Allowed (extend h F) = project h UNIV -` Allowed F" -apply (simp (no_asm) add: AllowedActs_extend Allowed_def) -apply blast -done +by (auto simp add: Allowed_def) lemma (in Extend) extend_SKIP [simp]: "extend h SKIP = SKIP" apply (unfold SKIP_def) @@ -634,7 +632,7 @@ "extend h F \ AU leadsTo BU ==> \y. F \ (slice AU y) leadsTo (project_set h BU)" apply (erule leadsTo_induct) - apply (blast intro: extend_ensures_slice leadsTo_Basis) + apply (blast intro: extend_ensures_slice) apply (blast intro: leadsTo_slice_project_set leadsTo_Trans) apply (simp add: leadsTo_UN slice_Union) done @@ -682,7 +680,7 @@ "project h UNIV ((extend h F)\G) = F\(project h UNIV G)" apply (rule program_equalityI) apply (simp add: project_set_extend_set_Int) - apply (simp add: image_eq_UN UN_Un, auto) + apply (auto simp add: image_eq_UN) done lemma (in Extend) extend_Join_eq_extend_D: diff -r ae9286f64574 -r e5438c5797ae src/HOL/UNITY/Guar.thy --- a/src/HOL/UNITY/Guar.thy Tue Feb 21 17:08:32 2012 +0100 +++ b/src/HOL/UNITY/Guar.thy Tue Feb 21 17:09:17 2012 +0100 @@ -17,7 +17,7 @@ begin instance program :: (type) order -proof qed (auto simp add: program_less_le dest: component_antisym intro: component_refl component_trans) + by default (auto simp add: program_less_le dest: component_antisym intro: component_trans) text{*Existential and Universal properties. I formalize the two-program case, proving equivalence with Chandy and Sanders's n-ary definitions*} diff -r ae9286f64574 -r e5438c5797ae src/HOL/UNITY/Lift_prog.thy --- a/src/HOL/UNITY/Lift_prog.thy Tue Feb 21 17:08:32 2012 +0100 +++ b/src/HOL/UNITY/Lift_prog.thy Tue Feb 21 17:09:17 2012 +0100 @@ -120,7 +120,7 @@ else if i preserves snd ==> lift i F \ preserves snd" apply (drule_tac w1=snd in subset_preserves_o [THEN subsetD]) apply (simp add: lift_def rename_preserves) -apply (simp add: lift_map_def o_def split_def del: split_comp_eq) +apply (simp add: lift_map_def o_def split_def) done lemma delete_map_eqE': @@ -327,9 +327,9 @@ ==> lift i F \ preserves (v o sub j o fst) = (if i=j then F \ preserves (v o fst) else True)" apply (drule subset_preserves_o [THEN subsetD]) -apply (simp add: lift_preserves_eq o_def drop_map_lift_map_eq) +apply (simp add: lift_preserves_eq o_def) apply (auto cong del: if_weak_cong - simp add: lift_map_def eq_commute split_def o_def simp del:split_comp_eq) + simp add: lift_map_def eq_commute split_def o_def) done @@ -409,10 +409,10 @@ by (simp add: safety_prop_AllowedActs_iff_Allowed UNION_OK_lift_I) lemma Allowed_lift [simp]: "Allowed (lift i F) = lift i ` (Allowed F)" -by (simp add: lift_def Allowed_rename) +by (simp add: lift_def) lemma lift_image_preserves: "lift i ` preserves v = preserves (v o drop_map i)" -by (simp add: rename_image_preserves lift_def inv_lift_map_eq) +by (simp add: rename_image_preserves lift_def) end diff -r ae9286f64574 -r e5438c5797ae src/HOL/UNITY/ListOrder.thy --- a/src/HOL/UNITY/ListOrder.thy Tue Feb 21 17:08:32 2012 +0100 +++ b/src/HOL/UNITY/ListOrder.thy Tue Feb 21 17:09:17 2012 +0100 @@ -208,7 +208,7 @@ "[| refl r; (xs,ys) : genPrefix r; length xs = length ys |] ==> (xs@zs, ys @ zs) : genPrefix r" apply (drule genPrefix_take_append, assumption) -apply (simp add: take_all) +apply simp done @@ -301,14 +301,10 @@ (** recursion equations **) lemma Nil_prefix [iff]: "[] <= xs" -apply (unfold prefix_def) -apply (simp add: Nil_genPrefix) -done +by (simp add: prefix_def) lemma prefix_Nil [simp]: "(xs <= []) = (xs = [])" -apply (unfold prefix_def) -apply (simp add: genPrefix_Nil) -done +by (simp add: prefix_def) lemma Cons_prefix_Cons [simp]: "(x#xs <= y#ys) = (x=y & xs<=ys)" by (simp add: prefix_def) diff -r ae9286f64574 -r e5438c5797ae src/HOL/UNITY/PPROD.thy --- a/src/HOL/UNITY/PPROD.thy Tue Feb 21 17:08:32 2012 +0100 +++ b/src/HOL/UNITY/PPROD.thy Tue Feb 21 17:09:17 2012 +0100 @@ -29,7 +29,7 @@ by (simp add: PLam_def) lemma PLam_SKIP [simp]: "(plam i : I. SKIP) = SKIP" -by (simp add: PLam_def lift_SKIP JN_constant) +by (simp add: PLam_def JN_constant) lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) Join (PLam I F)" by (unfold PLam_def, auto) diff -r ae9286f64574 -r e5438c5797ae src/HOL/UNITY/Rename.thy --- a/src/HOL/UNITY/Rename.thy Tue Feb 21 17:08:32 2012 +0100 +++ b/src/HOL/UNITY/Rename.thy Tue Feb 21 17:09:17 2012 +0100 @@ -64,7 +64,7 @@ apply (simp add: bij_extend_act_eq_project_act) apply (rule surjI) apply (rule Extend.extend_act_inverse) -apply (blast intro: bij_imp_bij_inv good_map_bij) +apply (blast intro: bij_imp_bij_inv) done lemma bij_project_act: "bij h ==> bij (project_act (%(x,u::'c). h x))" diff -r ae9286f64574 -r e5438c5797ae src/HOL/UNITY/UNITY.thy --- a/src/HOL/UNITY/UNITY.thy Tue Feb 21 17:08:32 2012 +0100 +++ b/src/HOL/UNITY/UNITY.thy Tue Feb 21 17:09:17 2012 +0100 @@ -58,9 +58,6 @@ "increasing f == \z. stable {s. z \ f s}" -text{*Perhaps HOL shouldn't add this in the first place!*} -declare image_Collect [simp del] - subsubsection{*The abstract type of programs*} lemmas program_typedef = @@ -73,7 +70,7 @@ done lemma insert_Id_Acts [iff]: "insert Id (Acts F) = Acts F" -by (simp add: insert_absorb Id_in_Acts) +by (simp add: insert_absorb) lemma Acts_nonempty [simp]: "Acts F \ {}" by auto @@ -84,7 +81,7 @@ done lemma insert_Id_AllowedActs [iff]: "insert Id (AllowedActs F) = AllowedActs F" -by (simp add: insert_absorb Id_in_AllowedActs) +by (simp add: insert_absorb) subsubsection{*Inspectors for type "program"*} diff -r ae9286f64574 -r e5438c5797ae src/HOL/UNITY/Union.thy --- a/src/HOL/UNITY/Union.thy Tue Feb 21 17:08:32 2012 +0100 +++ b/src/HOL/UNITY/Union.thy Tue Feb 21 17:09:17 2012 +0100 @@ -202,7 +202,7 @@ lemma Join_unless [simp]: "(F\G \ A unless B) = (F \ A unless B & G \ A unless B)" -by (simp add: Join_constrains unless_def) +by (simp add: unless_def) (*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom. reachable (F\G) could be much bigger than reachable F, reachable G @@ -238,12 +238,12 @@ lemma Join_increasing [simp]: "(F\G \ increasing f) = (F \ increasing f & G \ increasing f)" -by (simp add: increasing_def Join_stable, blast) +by (auto simp add: increasing_def) lemma invariant_JoinI: "[| F \ invariant A; G \ invariant A |] ==> F\G \ invariant A" -by (simp add: invariant_def, blast) +by (auto simp add: invariant_def) lemma FP_JN: "FP (\i \ I. F i) = (\i \ I. FP (F i))" by (simp add: FP_def JN_stable INTER_eq) @@ -262,10 +262,10 @@ by (auto simp add: bex_Un transient_def Join_def) lemma Join_transient_I1: "F \ transient A ==> F\G \ transient A" -by (simp add: Join_transient) +by simp lemma Join_transient_I2: "G \ transient A ==> F\G \ transient A" -by (simp add: Join_transient) +by simp (*If I={} it degenerates to (SKIP \ A ensures B) = False, i.e. to ~(A \ B) *) lemma JN_ensures: @@ -278,7 +278,7 @@ "F\G \ A ensures B = (F \ (A-B) co (A \ B) & G \ (A-B) co (A \ B) & (F \ transient (A-B) | G \ transient (A-B)))" -by (auto simp add: ensures_def Join_transient) +by (auto simp add: ensures_def) lemma stable_Join_constrains: "[| F \ stable A; G \ A co A' |]