1.1 --- a/src/HOL/UNITY/Comp/Alloc.thy Tue Feb 21 17:08:32 2012 +0100
1.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy Tue Feb 21 17:09:17 2012 +0100
1.3 @@ -537,8 +537,6 @@
1.4 declare ask_inv_client_map_drop_map [simp]
1.5
1.6
1.7 -declare finite_lessThan [iff]
1.8 -
1.9 text{*Client : <unfolded specification> *}
1.10 lemmas client_spec_simps =
1.11 client_spec_def client_increasing_def client_bounded_def
2.1 --- a/src/HOL/UNITY/Comp/Progress.thy Tue Feb 21 17:08:32 2012 +0100
2.2 +++ b/src/HOL/UNITY/Comp/Progress.thy Tue Feb 21 17:09:17 2012 +0100
2.3 @@ -13,10 +13,10 @@
2.4 text{*Thesis Section 4.4.2*}
2.5
2.6 definition FF :: "int program" where
2.7 - "FF == mk_total_program (UNIV, {range (\<lambda>x. (x, x+1))}, UNIV)"
2.8 + "FF = mk_total_program (UNIV, {range (\<lambda>x. (x, x+1))}, UNIV)"
2.9
2.10 definition GG :: "int program" where
2.11 - "GG == mk_total_program (UNIV, {range (\<lambda>x. (x, 2*x))}, UNIV)"
2.12 + "GG = mk_total_program (UNIV, {range (\<lambda>x. (x, 2*x))}, UNIV)"
2.13
2.14 subsubsection {*Calculating @{term "wens_set FF (atLeast k)"}*}
2.15
3.1 --- a/src/HOL/UNITY/ELT.thy Tue Feb 21 17:08:32 2012 +0100
3.2 +++ b/src/HOL/UNITY/ELT.thy Tue Feb 21 17:09:17 2012 +0100
3.3 @@ -166,7 +166,7 @@
3.4 apply (erule leadsETo_induct)
3.5 prefer 3 apply (blast intro: leadsETo_Union)
3.6 prefer 2 apply (blast intro: leadsETo_Trans)
3.7 -apply (blast intro: leadsETo_Basis)
3.8 +apply blast
3.9 done
3.10
3.11 lemma leadsETo_Trans_Un:
3.12 @@ -237,7 +237,7 @@
3.13 lemma leadsETo_givenBy:
3.14 "[| F : A leadsTo[CC] A'; CC <= givenBy v |]
3.15 ==> F : A leadsTo[givenBy v] A'"
3.16 -by (blast intro: empty_mem_givenBy leadsETo_weaken)
3.17 +by (blast intro: leadsETo_weaken)
3.18
3.19
3.20 (*Set difference*)
3.21 @@ -340,7 +340,7 @@
3.22 apply (blast intro: e_psp_stable2 [THEN leadsETo_weaken_L] leadsETo_Trans)
3.23 apply (rule leadsETo_Basis)
3.24 apply (auto simp add: Diff_eq_empty_iff [THEN iffD2]
3.25 - Int_Diff ensures_def givenBy_eq_Collect Join_transient)
3.26 + Int_Diff ensures_def givenBy_eq_Collect)
3.27 prefer 3 apply (blast intro: transient_strengthen)
3.28 apply (drule_tac [2] P1 = P in preserves_subset_stable [THEN subsetD])
3.29 apply (drule_tac P1 = P in preserves_subset_stable [THEN subsetD])
3.30 @@ -454,7 +454,7 @@
3.31 lemma lel_lemma:
3.32 "F : A leadsTo B ==> F : (reachable F Int A) leadsTo[Pow(reachable F)] B"
3.33 apply (erule leadsTo_induct)
3.34 - apply (blast intro: reachable_ensures leadsETo_Basis)
3.35 + apply (blast intro: reachable_ensures)
3.36 apply (blast dest: e_psp_stable2 intro: leadsETo_Trans leadsETo_weaken_L)
3.37 apply (subst Int_Union)
3.38 apply (blast intro: leadsETo_UN)
3.39 @@ -491,7 +491,7 @@
3.40 ==> extend h F : (extend_set h A) leadsTo[extend_set h ` CC]
3.41 (extend_set h B)"
3.42 apply (erule leadsETo_induct)
3.43 - apply (force intro: leadsETo_Basis subset_imp_ensures
3.44 + apply (force intro: subset_imp_ensures
3.45 simp add: extend_ensures extend_set_Diff_distrib [symmetric])
3.46 apply (blast intro: leadsETo_Trans)
3.47 apply (simp add: leadsETo_UN extend_set_Union)
4.1 --- a/src/HOL/UNITY/Extend.thy Tue Feb 21 17:08:32 2012 +0100
4.2 +++ b/src/HOL/UNITY/Extend.thy Tue Feb 21 17:09:17 2012 +0100
4.3 @@ -370,9 +370,7 @@
4.4
4.5 lemma (in Extend) Allowed_extend:
4.6 "Allowed (extend h F) = project h UNIV -` Allowed F"
4.7 -apply (simp (no_asm) add: AllowedActs_extend Allowed_def)
4.8 -apply blast
4.9 -done
4.10 +by (auto simp add: Allowed_def)
4.11
4.12 lemma (in Extend) extend_SKIP [simp]: "extend h SKIP = SKIP"
4.13 apply (unfold SKIP_def)
4.14 @@ -634,7 +632,7 @@
4.15 "extend h F \<in> AU leadsTo BU
4.16 ==> \<forall>y. F \<in> (slice AU y) leadsTo (project_set h BU)"
4.17 apply (erule leadsTo_induct)
4.18 - apply (blast intro: extend_ensures_slice leadsTo_Basis)
4.19 + apply (blast intro: extend_ensures_slice)
4.20 apply (blast intro: leadsTo_slice_project_set leadsTo_Trans)
4.21 apply (simp add: leadsTo_UN slice_Union)
4.22 done
4.23 @@ -682,7 +680,7 @@
4.24 "project h UNIV ((extend h F)\<squnion>G) = F\<squnion>(project h UNIV G)"
4.25 apply (rule program_equalityI)
4.26 apply (simp add: project_set_extend_set_Int)
4.27 - apply (simp add: image_eq_UN UN_Un, auto)
4.28 + apply (auto simp add: image_eq_UN)
4.29 done
4.30
4.31 lemma (in Extend) extend_Join_eq_extend_D:
5.1 --- a/src/HOL/UNITY/Guar.thy Tue Feb 21 17:08:32 2012 +0100
5.2 +++ b/src/HOL/UNITY/Guar.thy Tue Feb 21 17:09:17 2012 +0100
5.3 @@ -17,7 +17,7 @@
5.4 begin
5.5
5.6 instance program :: (type) order
5.7 -proof qed (auto simp add: program_less_le dest: component_antisym intro: component_refl component_trans)
5.8 + by default (auto simp add: program_less_le dest: component_antisym intro: component_trans)
5.9
5.10 text{*Existential and Universal properties. I formalize the two-program
5.11 case, proving equivalence with Chandy and Sanders's n-ary definitions*}
6.1 --- a/src/HOL/UNITY/Lift_prog.thy Tue Feb 21 17:08:32 2012 +0100
6.2 +++ b/src/HOL/UNITY/Lift_prog.thy Tue Feb 21 17:09:17 2012 +0100
6.3 @@ -120,7 +120,7 @@
6.4 else if i<j then insert_map j t (f(i:=s))
6.5 else insert_map j t (f(i - Suc 0 := s)))"
6.6 apply (rule ext)
6.7 -apply (simp split add: nat_diff_split)
6.8 +apply (simp split add: nat_diff_split)
6.9 txt{*This simplification is VERY slow*}
6.10 done
6.11
6.12 @@ -254,7 +254,7 @@
6.13 lemma lift_preserves_snd_I: "F \<in> preserves snd ==> lift i F \<in> preserves snd"
6.14 apply (drule_tac w1=snd in subset_preserves_o [THEN subsetD])
6.15 apply (simp add: lift_def rename_preserves)
6.16 -apply (simp add: lift_map_def o_def split_def del: split_comp_eq)
6.17 +apply (simp add: lift_map_def o_def split_def)
6.18 done
6.19
6.20 lemma delete_map_eqE':
6.21 @@ -327,9 +327,9 @@
6.22 ==> lift i F \<in> preserves (v o sub j o fst) =
6.23 (if i=j then F \<in> preserves (v o fst) else True)"
6.24 apply (drule subset_preserves_o [THEN subsetD])
6.25 -apply (simp add: lift_preserves_eq o_def drop_map_lift_map_eq)
6.26 +apply (simp add: lift_preserves_eq o_def)
6.27 apply (auto cong del: if_weak_cong
6.28 - simp add: lift_map_def eq_commute split_def o_def simp del:split_comp_eq)
6.29 + simp add: lift_map_def eq_commute split_def o_def)
6.30 done
6.31
6.32
6.33 @@ -409,10 +409,10 @@
6.34 by (simp add: safety_prop_AllowedActs_iff_Allowed UNION_OK_lift_I)
6.35
6.36 lemma Allowed_lift [simp]: "Allowed (lift i F) = lift i ` (Allowed F)"
6.37 -by (simp add: lift_def Allowed_rename)
6.38 +by (simp add: lift_def)
6.39
6.40 lemma lift_image_preserves:
6.41 "lift i ` preserves v = preserves (v o drop_map i)"
6.42 -by (simp add: rename_image_preserves lift_def inv_lift_map_eq)
6.43 +by (simp add: rename_image_preserves lift_def)
6.44
6.45 end
7.1 --- a/src/HOL/UNITY/ListOrder.thy Tue Feb 21 17:08:32 2012 +0100
7.2 +++ b/src/HOL/UNITY/ListOrder.thy Tue Feb 21 17:09:17 2012 +0100
7.3 @@ -208,7 +208,7 @@
7.4 "[| refl r; (xs,ys) : genPrefix r; length xs = length ys |]
7.5 ==> (xs@zs, ys @ zs) : genPrefix r"
7.6 apply (drule genPrefix_take_append, assumption)
7.7 -apply (simp add: take_all)
7.8 +apply simp
7.9 done
7.10
7.11
7.12 @@ -301,14 +301,10 @@
7.13 (** recursion equations **)
7.14
7.15 lemma Nil_prefix [iff]: "[] <= xs"
7.16 -apply (unfold prefix_def)
7.17 -apply (simp add: Nil_genPrefix)
7.18 -done
7.19 +by (simp add: prefix_def)
7.20
7.21 lemma prefix_Nil [simp]: "(xs <= []) = (xs = [])"
7.22 -apply (unfold prefix_def)
7.23 -apply (simp add: genPrefix_Nil)
7.24 -done
7.25 +by (simp add: prefix_def)
7.26
7.27 lemma Cons_prefix_Cons [simp]: "(x#xs <= y#ys) = (x=y & xs<=ys)"
7.28 by (simp add: prefix_def)
8.1 --- a/src/HOL/UNITY/PPROD.thy Tue Feb 21 17:08:32 2012 +0100
8.2 +++ b/src/HOL/UNITY/PPROD.thy Tue Feb 21 17:09:17 2012 +0100
8.3 @@ -29,7 +29,7 @@
8.4 by (simp add: PLam_def)
8.5
8.6 lemma PLam_SKIP [simp]: "(plam i : I. SKIP) = SKIP"
8.7 -by (simp add: PLam_def lift_SKIP JN_constant)
8.8 +by (simp add: PLam_def JN_constant)
8.9
8.10 lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) Join (PLam I F)"
8.11 by (unfold PLam_def, auto)
9.1 --- a/src/HOL/UNITY/Rename.thy Tue Feb 21 17:08:32 2012 +0100
9.2 +++ b/src/HOL/UNITY/Rename.thy Tue Feb 21 17:09:17 2012 +0100
9.3 @@ -64,7 +64,7 @@
9.4 apply (simp add: bij_extend_act_eq_project_act)
9.5 apply (rule surjI)
9.6 apply (rule Extend.extend_act_inverse)
9.7 -apply (blast intro: bij_imp_bij_inv good_map_bij)
9.8 +apply (blast intro: bij_imp_bij_inv)
9.9 done
9.10
9.11 lemma bij_project_act: "bij h ==> bij (project_act (%(x,u::'c). h x))"
10.1 --- a/src/HOL/UNITY/UNITY.thy Tue Feb 21 17:08:32 2012 +0100
10.2 +++ b/src/HOL/UNITY/UNITY.thy Tue Feb 21 17:09:17 2012 +0100
10.3 @@ -58,9 +58,6 @@
10.4 "increasing f == \<Inter>z. stable {s. z \<le> f s}"
10.5
10.6
10.7 -text{*Perhaps HOL shouldn't add this in the first place!*}
10.8 -declare image_Collect [simp del]
10.9 -
10.10 subsubsection{*The abstract type of programs*}
10.11
10.12 lemmas program_typedef =
10.13 @@ -73,7 +70,7 @@
10.14 done
10.15
10.16 lemma insert_Id_Acts [iff]: "insert Id (Acts F) = Acts F"
10.17 -by (simp add: insert_absorb Id_in_Acts)
10.18 +by (simp add: insert_absorb)
10.19
10.20 lemma Acts_nonempty [simp]: "Acts F \<noteq> {}"
10.21 by auto
10.22 @@ -84,7 +81,7 @@
10.23 done
10.24
10.25 lemma insert_Id_AllowedActs [iff]: "insert Id (AllowedActs F) = AllowedActs F"
10.26 -by (simp add: insert_absorb Id_in_AllowedActs)
10.27 +by (simp add: insert_absorb)
10.28
10.29 subsubsection{*Inspectors for type "program"*}
10.30
11.1 --- a/src/HOL/UNITY/Union.thy Tue Feb 21 17:08:32 2012 +0100
11.2 +++ b/src/HOL/UNITY/Union.thy Tue Feb 21 17:09:17 2012 +0100
11.3 @@ -202,7 +202,7 @@
11.4
11.5 lemma Join_unless [simp]:
11.6 "(F\<squnion>G \<in> A unless B) = (F \<in> A unless B & G \<in> A unless B)"
11.7 -by (simp add: Join_constrains unless_def)
11.8 +by (simp add: unless_def)
11.9
11.10 (*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
11.11 reachable (F\<squnion>G) could be much bigger than reachable F, reachable G
11.12 @@ -238,12 +238,12 @@
11.13 lemma Join_increasing [simp]:
11.14 "(F\<squnion>G \<in> increasing f) =
11.15 (F \<in> increasing f & G \<in> increasing f)"
11.16 -by (simp add: increasing_def Join_stable, blast)
11.17 +by (auto simp add: increasing_def)
11.18
11.19 lemma invariant_JoinI:
11.20 "[| F \<in> invariant A; G \<in> invariant A |]
11.21 ==> F\<squnion>G \<in> invariant A"
11.22 -by (simp add: invariant_def, blast)
11.23 +by (auto simp add: invariant_def)
11.24
11.25 lemma FP_JN: "FP (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. FP (F i))"
11.26 by (simp add: FP_def JN_stable INTER_eq)
11.27 @@ -262,10 +262,10 @@
11.28 by (auto simp add: bex_Un transient_def Join_def)
11.29
11.30 lemma Join_transient_I1: "F \<in> transient A ==> F\<squnion>G \<in> transient A"
11.31 -by (simp add: Join_transient)
11.32 +by simp
11.33
11.34 lemma Join_transient_I2: "G \<in> transient A ==> F\<squnion>G \<in> transient A"
11.35 -by (simp add: Join_transient)
11.36 +by simp
11.37
11.38 (*If I={} it degenerates to (SKIP \<in> A ensures B) = False, i.e. to ~(A \<subseteq> B) *)
11.39 lemma JN_ensures:
11.40 @@ -278,7 +278,7 @@
11.41 "F\<squnion>G \<in> A ensures B =
11.42 (F \<in> (A-B) co (A \<union> B) & G \<in> (A-B) co (A \<union> B) &
11.43 (F \<in> transient (A-B) | G \<in> transient (A-B)))"
11.44 -by (auto simp add: ensures_def Join_transient)
11.45 +by (auto simp add: ensures_def)
11.46
11.47 lemma stable_Join_constrains:
11.48 "[| F \<in> stable A; G \<in> A co A' |]