--- 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 : <unfolded specification> *}
lemmas client_spec_simps =
client_spec_def client_increasing_def client_bounded_def
--- 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 (\<lambda>x. (x, x+1))}, UNIV)"
+ "FF = mk_total_program (UNIV, {range (\<lambda>x. (x, x+1))}, UNIV)"
definition GG :: "int program" where
- "GG == mk_total_program (UNIV, {range (\<lambda>x. (x, 2*x))}, UNIV)"
+ "GG = mk_total_program (UNIV, {range (\<lambda>x. (x, 2*x))}, UNIV)"
subsubsection {*Calculating @{term "wens_set FF (atLeast k)"}*}
--- 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)
--- 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 \<in> AU leadsTo BU
==> \<forall>y. F \<in> (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)\<squnion>G) = F\<squnion>(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:
--- 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*}
--- 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<j then insert_map j t (f(i:=s))
else insert_map j t (f(i - Suc 0 := s)))"
apply (rule ext)
-apply (simp split add: nat_diff_split)
+apply (simp split add: nat_diff_split)
txt{*This simplification is VERY slow*}
done
@@ -254,7 +254,7 @@
lemma lift_preserves_snd_I: "F \<in> preserves snd ==> lift i F \<in> 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 \<in> preserves (v o sub j o fst) =
(if i=j then F \<in> 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
--- 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)
--- 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)
--- 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))"
--- 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 == \<Inter>z. stable {s. z \<le> 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 \<noteq> {}"
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"*}
--- 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\<squnion>G \<in> A unless B) = (F \<in> A unless B & G \<in> 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\<squnion>G) could be much bigger than reachable F, reachable G
@@ -238,12 +238,12 @@
lemma Join_increasing [simp]:
"(F\<squnion>G \<in> increasing f) =
(F \<in> increasing f & G \<in> increasing f)"
-by (simp add: increasing_def Join_stable, blast)
+by (auto simp add: increasing_def)
lemma invariant_JoinI:
"[| F \<in> invariant A; G \<in> invariant A |]
==> F\<squnion>G \<in> invariant A"
-by (simp add: invariant_def, blast)
+by (auto simp add: invariant_def)
lemma FP_JN: "FP (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> 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 \<in> transient A ==> F\<squnion>G \<in> transient A"
-by (simp add: Join_transient)
+by simp
lemma Join_transient_I2: "G \<in> transient A ==> F\<squnion>G \<in> transient A"
-by (simp add: Join_transient)
+by simp
(*If I={} it degenerates to (SKIP \<in> A ensures B) = False, i.e. to ~(A \<subseteq> B) *)
lemma JN_ensures:
@@ -278,7 +278,7 @@
"F\<squnion>G \<in> A ensures B =
(F \<in> (A-B) co (A \<union> B) & G \<in> (A-B) co (A \<union> B) &
(F \<in> transient (A-B) | G \<in> transient (A-B)))"
-by (auto simp add: ensures_def Join_transient)
+by (auto simp add: ensures_def)
lemma stable_Join_constrains:
"[| F \<in> stable A; G \<in> A co A' |]