# 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 : <unfolded specification> *}
 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 (\<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)"}*}
 
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 \<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:
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<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
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 == \<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"*}
 
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\<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' |]