tuned proofs;
authorwenzelm
Tue Feb 21 17:09:17 2012 +0100 (2012-02-21)
changeset 46577e5438c5797ae
parent 46576 ae9286f64574
child 46578 1bc7e91a5c77
tuned proofs;
src/HOL/UNITY/Comp/Alloc.thy
src/HOL/UNITY/Comp/Progress.thy
src/HOL/UNITY/ELT.thy
src/HOL/UNITY/Extend.thy
src/HOL/UNITY/Guar.thy
src/HOL/UNITY/Lift_prog.thy
src/HOL/UNITY/ListOrder.thy
src/HOL/UNITY/PPROD.thy
src/HOL/UNITY/Rename.thy
src/HOL/UNITY/UNITY.thy
src/HOL/UNITY/Union.thy
     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' |]