tuned proofs;
authorwenzelm
Tue Mar 13 22:49:02 2012 +0100 (2012-03-13)
changeset 469116d2a2f0e904e
parent 46910 3e068ef04b42
child 46912 e0cd5c4df8e6
tuned proofs;
src/HOL/UNITY/Comp/Alloc.thy
src/HOL/UNITY/Comp/AllocBase.thy
src/HOL/UNITY/Comp/Counter.thy
src/HOL/UNITY/Comp/Counterc.thy
src/HOL/UNITY/Comp/Priority.thy
src/HOL/UNITY/Comp/PriorityAux.thy
src/HOL/UNITY/ELT.thy
src/HOL/UNITY/Lift_prog.thy
src/HOL/UNITY/ListOrder.thy
src/HOL/UNITY/Simple/Reach.thy
src/HOL/UNITY/Simple/Reachability.thy
src/HOL/UNITY/Simple/Token.thy
src/HOL/UNITY/Transformers.thy
     1.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Tue Mar 13 21:17:37 2012 +0100
     1.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Tue Mar 13 22:49:02 2012 +0100
     1.3 @@ -749,7 +749,7 @@
     1.4  
     1.5  lemma client_preserves_giv_oo_client_map: "[| i < Nclients; j < Nclients |]
     1.6        ==> Client : preserves (giv o sub i o fst o lift_map j o client_map)"
     1.7 -  apply (case_tac "i=j")
     1.8 +  apply (cases "i=j")
     1.9    apply (simp, simp add: o_def non_dummy_def)
    1.10    apply (drule Client_preserves_dummy [THEN preserves_sub_fst_lift_map])
    1.11    apply (drule_tac [!] subset_preserves_o [THEN [2] rev_subsetD])
     2.1 --- a/src/HOL/UNITY/Comp/AllocBase.thy	Tue Mar 13 21:17:37 2012 +0100
     2.2 +++ b/src/HOL/UNITY/Comp/AllocBase.thy	Tue Mar 13 22:49:02 2012 +0100
     2.3 @@ -27,11 +27,8 @@
     2.4  apply (auto simp add: lessThan_Suc)
     2.5  done
     2.6  
     2.7 -lemma tokens_mono_prefix [rule_format]:
     2.8 -     "ALL xs. xs <= ys --> tokens xs <= tokens ys"
     2.9 -apply (induct_tac "ys")
    2.10 -apply (auto simp add: prefix_Cons)
    2.11 -done
    2.12 +lemma tokens_mono_prefix: "xs <= ys ==> tokens xs <= tokens ys"
    2.13 +  by (induct ys arbitrary: xs) (auto simp add: prefix_Cons)
    2.14  
    2.15  lemma mono_tokens: "mono tokens"
    2.16  apply (unfold mono_def)
    2.17 @@ -42,9 +39,7 @@
    2.18  (** bag_of **)
    2.19  
    2.20  lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'"
    2.21 -apply (induct_tac "l", simp)
    2.22 - apply (simp add: add_ac)
    2.23 -done
    2.24 +  by (induct l) (simp_all add: add_ac)
    2.25  
    2.26  lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)"
    2.27  apply (rule monoI)
     3.1 --- a/src/HOL/UNITY/Comp/Counter.thy	Tue Mar 13 21:17:37 2012 +0100
     3.2 +++ b/src/HOL/UNITY/Comp/Counter.thy	Tue Mar 13 22:49:02 2012 +0100
     3.3 @@ -41,40 +41,30 @@
     3.4  declare a_def [THEN def_act_simp, simp]
     3.5  
     3.6  (* Theorems about sum and sumj *)
     3.7 -lemma sum_upd_gt [rule_format]: "\<forall>n. I<n --> sum I (s(c n := x)) = sum I s"
     3.8 -by (induct_tac "I", auto)
     3.9 +lemma sum_upd_gt: "I<n ==> sum I (s(c n := x)) = sum I s"
    3.10 +  by (induct I) auto
    3.11  
    3.12  
    3.13  lemma sum_upd_eq: "sum I (s(c I := x)) = sum I s"
    3.14 -apply (induct_tac "I")
    3.15 -apply (auto simp add: sum_upd_gt [unfolded fun_upd_def])
    3.16 -done
    3.17 +  by (induct I) (auto simp add: sum_upd_gt [unfolded fun_upd_def])
    3.18  
    3.19  lemma sum_upd_C: "sum I (s(C := x)) = sum I s"
    3.20 -by (induct_tac "I", auto)
    3.21 +  by (induct I) auto
    3.22  
    3.23  lemma sumj_upd_ci: "sumj I i (s(c i := x)) = sumj I i s"
    3.24 -apply (induct_tac "I")
    3.25 -apply (auto simp add: sum_upd_eq [unfolded fun_upd_def])
    3.26 -done
    3.27 +  by (induct I) (auto simp add: sum_upd_eq [unfolded fun_upd_def])
    3.28  
    3.29  lemma sumj_upd_C: "sumj I i (s(C := x)) = sumj I i s"
    3.30 -apply (induct_tac "I")
    3.31 -apply (auto simp add: sum_upd_C [unfolded fun_upd_def])
    3.32 -done
    3.33 +  by (induct I) (auto simp add: sum_upd_C [unfolded fun_upd_def])
    3.34  
    3.35 -lemma sumj_sum_gt [rule_format]: "\<forall>i. I<i--> (sumj I i s = sum I s)"
    3.36 -by (induct_tac "I", auto)
    3.37 +lemma sumj_sum_gt: "I<i ==> sumj I i s = sum I s"
    3.38 +  by (induct I) auto
    3.39  
    3.40  lemma sumj_sum_eq: "(sumj I I s = sum I s)"
    3.41 -apply (induct_tac "I", auto)
    3.42 -apply (simp (no_asm) add: sumj_sum_gt)
    3.43 -done
    3.44 +  by (induct I) (auto simp add: sumj_sum_gt)
    3.45  
    3.46 -lemma sum_sumj [rule_format]: "\<forall>i. i<I-->(sum I s = s (c i) +  sumj I i s)"
    3.47 -apply (induct_tac "I")
    3.48 -apply (auto simp add: linorder_neq_iff sumj_sum_eq)
    3.49 -done
    3.50 +lemma sum_sumj: "i<I ==> sum I s = s (c i) +  sumj I i s"
    3.51 +  by (induct I) (auto simp add: linorder_neq_iff sumj_sum_eq)
    3.52  
    3.53  (* Correctness proofs for Components *)
    3.54  (* p2 and p3 proofs *)
    3.55 @@ -103,8 +93,8 @@
    3.56  
    3.57  (* Compositional Proof *)
    3.58  
    3.59 -lemma sum_0' [rule_format]: "(\<forall>i. i < I --> s (c i) = 0) --> sum I s = 0"
    3.60 -by (induct_tac "I", auto)
    3.61 +lemma sum_0': "(\<And>i. i < I ==> s (c i) = 0) ==> sum I s = 0"
    3.62 +  by (induct I) auto
    3.63  
    3.64  (* I cannot be empty *)
    3.65  lemma safety:
     4.1 --- a/src/HOL/UNITY/Comp/Counterc.thy	Tue Mar 13 21:17:37 2012 +0100
     4.2 +++ b/src/HOL/UNITY/Comp/Counterc.thy	Tue Mar 13 22:49:02 2012 +0100
     4.3 @@ -46,27 +46,20 @@
     4.4  declare a_def [THEN def_act_simp, simp]
     4.5  
     4.6  (* Theorems about sum and sumj *)
     4.7 -lemma sum_sumj_eq1 [rule_format]: "\<forall>i. I<i--> (sum I s = sumj I i s)"
     4.8 -by (induct_tac "I", auto)
     4.9 +lemma sum_sumj_eq1: "I<i ==> sum I s = sumj I i s"
    4.10 +  by (induct I) auto
    4.11  
    4.12 -lemma sum_sumj_eq2 [rule_format]: "i<I --> sum I s  = c s i + sumj I i s"
    4.13 -apply (induct_tac "I")
    4.14 -apply (auto simp add: linorder_neq_iff sum_sumj_eq1)
    4.15 -done
    4.16 +lemma sum_sumj_eq2: "i<I ==> sum I s  = c s i + sumj I i s"
    4.17 +  by (induct I) (auto simp add: linorder_neq_iff sum_sumj_eq1)
    4.18  
    4.19 -lemma sum_ext [rule_format]:
    4.20 -     "(\<forall>i. i<I --> c s' i = c s i) --> (sum I s' = sum I s)"
    4.21 -by (induct_tac "I", auto)
    4.22 +lemma sum_ext: "(\<And>i. i<I \<Longrightarrow> c s' i = c s i) ==> sum I s' = sum I s"
    4.23 +  by (induct I) auto
    4.24  
    4.25 -lemma sumj_ext [rule_format]:
    4.26 -     "(\<forall>j. j<I & j\<noteq>i --> c s' j =  c s j) --> (sumj I i s' = sumj I i s)"
    4.27 -apply (induct_tac "I", safe)
    4.28 -apply (auto intro!: sum_ext)
    4.29 -done
    4.30 +lemma sumj_ext: "(\<And>j. j<I ==> j\<noteq>i ==> c s' j =  c s j) ==> sumj I i s' = sumj I i s"
    4.31 +  by (induct I) (auto intro!: sum_ext)
    4.32  
    4.33 -
    4.34 -lemma sum0 [rule_format]: "(\<forall>i. i<I --> c s i = 0) -->  sum I s = 0"
    4.35 -by (induct_tac "I", auto)
    4.36 +lemma sum0: "(\<And>i. i<I ==> c s i = 0) ==> sum I s = 0"
    4.37 +  by (induct I) auto
    4.38  
    4.39  
    4.40  (* Safety properties for Components *)
     5.1 --- a/src/HOL/UNITY/Comp/Priority.thy	Tue Mar 13 21:17:37 2012 +0100
     5.2 +++ b/src/HOL/UNITY/Comp/Priority.thy	Tue Mar 13 22:49:02 2012 +0100
     5.3 @@ -143,16 +143,12 @@
     5.4  
     5.5  
     5.6  text{* p15: universal property: all Components well behave  *}
     5.7 -lemma system_well_behaves [rule_format]:
     5.8 -     "\<forall>i. system \<in> Highest i co Highest i Un Lowest i"
     5.9 -apply clarify
    5.10 -apply (simp add: system_def Component_def mk_total_program_def totalize_JN, 
    5.11 -       safety, auto)
    5.12 -done
    5.13 +lemma system_well_behaves: "system \<in> Highest i co Highest i Un Lowest i"
    5.14 +  by (simp add: system_def Component_def mk_total_program_def totalize_JN, safety, auto)
    5.15  
    5.16  
    5.17  lemma Acyclic_eq: "Acyclic = (\<Inter>i. {s. i\<notin>above i s})"
    5.18 -by (auto simp add: Acyclic_def acyclic_def trancl_converse)
    5.19 +  by (auto simp add: Acyclic_def acyclic_def trancl_converse)
    5.20  
    5.21  
    5.22  lemmas system_co =
     6.1 --- a/src/HOL/UNITY/Comp/PriorityAux.thy	Tue Mar 13 21:17:37 2012 +0100
     6.2 +++ b/src/HOL/UNITY/Comp/PriorityAux.thy	Tue Mar 13 22:49:02 2012 +0100
     6.3 @@ -94,8 +94,8 @@
     6.4  apply (unfold reach_def)
     6.5  apply (erule ImageE)
     6.6  apply (erule trancl_induct) 
     6.7 - apply (case_tac "i=k", simp_all) 
     6.8 -  apply (blast intro: r_into_trancl, blast, clarify) 
     6.9 + apply (cases "i=k", simp_all) 
    6.10 +  apply (blast, blast, clarify) 
    6.11  apply (drule_tac x = y in spec)
    6.12  apply (drule_tac x = z in spec)
    6.13  apply (blast dest: r_into_trancl intro: trancl_trans)
     7.1 --- a/src/HOL/UNITY/ELT.thy	Tue Mar 13 21:17:37 2012 +0100
     7.2 +++ b/src/HOL/UNITY/ELT.thy	Tue Mar 13 22:49:02 2012 +0100
     7.3 @@ -207,7 +207,7 @@
     7.4       "[| F : A leadsTo[CC] A';  A'<=B' |] ==> F : A leadsTo[CC] B'"
     7.5  by (blast intro: subset_imp_leadsETo leadsETo_Trans)
     7.6  
     7.7 -lemma leadsETo_weaken_L [rule_format]:
     7.8 +lemma leadsETo_weaken_L:
     7.9       "[| F : A leadsTo[CC] A'; B<=A |] ==> F : B leadsTo[CC] A'"
    7.10  by (blast intro: leadsETo_Trans subset_imp_leadsETo)
    7.11  
    7.12 @@ -420,15 +420,15 @@
    7.13  
    7.14  lemmas empty_LeadsETo = empty_subsetI [THEN subset_imp_LeadsETo]
    7.15  
    7.16 -lemma LeadsETo_weaken_R [rule_format]:
    7.17 +lemma LeadsETo_weaken_R:
    7.18       "[| F : A LeadsTo[CC] A';  A' <= B' |] ==> F : A LeadsTo[CC] B'"
    7.19 -apply (simp (no_asm_use) add: LeadsETo_def)
    7.20 +apply (simp add: LeadsETo_def)
    7.21  apply (blast intro: leadsETo_weaken_R)
    7.22  done
    7.23  
    7.24 -lemma LeadsETo_weaken_L [rule_format]:
    7.25 +lemma LeadsETo_weaken_L:
    7.26       "[| F : A LeadsTo[CC] A';  B <= A |] ==> F : B LeadsTo[CC] A'"
    7.27 -apply (simp (no_asm_use) add: LeadsETo_def)
    7.28 +apply (simp add: LeadsETo_def)
    7.29  apply (blast intro: leadsETo_weaken_L)
    7.30  done
    7.31  
     8.1 --- a/src/HOL/UNITY/Lift_prog.thy	Tue Mar 13 21:17:37 2012 +0100
     8.2 +++ b/src/HOL/UNITY/Lift_prog.thy	Tue Mar 13 22:49:02 2012 +0100
     8.3 @@ -301,7 +301,7 @@
     8.4      "[| F i \<in> (A <*> UNIV) co (B <*> UNIV);   
     8.5          F j \<in> preserves snd |]   
     8.6       ==> lift j (F j) \<in> (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))"
     8.7 -apply (case_tac "i=j")
     8.8 +apply (cases "i=j")
     8.9  apply (simp add: lift_def lift_set_def rename_constrains)
    8.10  apply (erule preserves_snd_lift_stable[THEN stableD, THEN constrains_weaken_R],
    8.11         assumption)
     9.1 --- a/src/HOL/UNITY/ListOrder.thy	Tue Mar 13 21:17:37 2012 +0100
     9.2 +++ b/src/HOL/UNITY/ListOrder.thy	Tue Mar 13 22:49:02 2012 +0100
     9.3 @@ -179,22 +179,16 @@
     9.4  subsection{*recursion equations*}
     9.5  
     9.6  lemma genPrefix_Nil [simp]: "((xs, []) : genPrefix r) = (xs = [])"
     9.7 -apply (induct_tac "xs")
     9.8 -prefer 2 apply blast
     9.9 -apply simp
    9.10 -done
    9.11 +  by (induct xs) auto
    9.12  
    9.13  lemma same_genPrefix_genPrefix [simp]: 
    9.14      "refl r ==> ((xs@ys, xs@zs) : genPrefix r) = ((ys,zs) : genPrefix r)"
    9.15 -apply (unfold refl_on_def)
    9.16 -apply (induct_tac "xs")
    9.17 -apply (simp_all (no_asm_simp))
    9.18 -done
    9.19 +  by (induct xs) (simp_all add: refl_on_def)
    9.20  
    9.21  lemma genPrefix_Cons:
    9.22       "((xs, y#ys) : genPrefix r) =  
    9.23        (xs=[] | (EX z zs. xs=z#zs & (z,y) : r & (zs,ys) : genPrefix r))"
    9.24 -by (case_tac "xs", auto)
    9.25 +  by (cases xs) auto
    9.26  
    9.27  lemma genPrefix_take_append:
    9.28       "[| refl r;  (xs,ys) : genPrefix r |]  
    10.1 --- a/src/HOL/UNITY/Simple/Reach.thy	Tue Mar 13 21:17:37 2012 +0100
    10.2 +++ b/src/HOL/UNITY/Simple/Reach.thy	Tue Mar 13 22:49:02 2012 +0100
    10.3 @@ -126,9 +126,7 @@
    10.4  by (erule Suc_metric [THEN subst], blast)
    10.5  
    10.6  lemma metric_le: "metric (s(y:=s x | s y)) \<le> metric s"
    10.7 -apply (case_tac "s x --> s y")
    10.8 -apply (auto intro: less_imp_le simp add: fun_upd_idem)
    10.9 -done
   10.10 +  by (cases "s x --> s y") (auto intro: less_imp_le simp add: fun_upd_idem)
   10.11  
   10.12  lemma LeadsTo_Diff_fixedpoint:
   10.13       "Rprg \<in> ((metric-`{m}) - fixedpoint) LeadsTo (metric-`(lessThan m))"
    11.1 --- a/src/HOL/UNITY/Simple/Reachability.thy	Tue Mar 13 21:17:37 2012 +0100
    11.2 +++ b/src/HOL/UNITY/Simple/Reachability.thy	Tue Mar 13 22:49:02 2012 +0100
    11.3 @@ -319,7 +319,7 @@
    11.4  done
    11.5  
    11.6  lemma LeadsTo_final: "F \<in> UNIV LeadsTo final"
    11.7 -apply (case_tac "E={}")
    11.8 +apply (cases "E={}")
    11.9   apply (rule_tac [2] LeadsTo_final_E_NOT_empty)
   11.10  apply (rule LeadsTo_final_E_empty, auto)
   11.11  done
   11.12 @@ -361,7 +361,7 @@
   11.13  done
   11.14  
   11.15  lemma Stable_final: "F \<in> Stable final"
   11.16 -apply (case_tac "E={}")
   11.17 +apply (cases "E={}")
   11.18   prefer 2 apply (blast intro: Stable_final_E_NOT_empty)
   11.19  apply (blast intro: Stable_final_E_empty)
   11.20  done
    12.1 --- a/src/HOL/UNITY/Simple/Token.thy	Tue Mar 13 21:17:37 2012 +0100
    12.2 +++ b/src/HOL/UNITY/Simple/Token.thy	Tue Mar 13 22:49:02 2012 +0100
    12.3 @@ -56,7 +56,7 @@
    12.4  
    12.5  lemma not_E_eq: "(s \<notin> E i) = (s \<in> H i | s \<in> T i)"
    12.6  apply (simp add: H_def E_def T_def)
    12.7 -apply (case_tac "proc s i", auto)
    12.8 +apply (cases "proc s i", auto)
    12.9  done
   12.10  
   12.11  lemma (in Token) token_stable: "F \<in> stable (-(E i) \<union> (HasTok i))"
   12.12 @@ -83,11 +83,11 @@
   12.13  done
   12.14  
   12.15  text{*From "A Logic for Concurrent Programming", but not used in Chapter 4.
   12.16 -  Note the use of @{text case_tac}.  Reasoning about leadsTo takes practice!*}
   12.17 +  Note the use of @{text cases}.  Reasoning about leadsTo takes practice!*}
   12.18  lemma (in Token) TR7_nodeOrder:
   12.19       "[| i<N; j<N |] ==>    
   12.20        F \<in> (HasTok i) leadsTo ({s. (token s, i) \<in> nodeOrder j} \<union> HasTok j)"
   12.21 -apply (case_tac "i=j")
   12.22 +apply (cases "i=j")
   12.23  apply (blast intro: subset_imp_leadsTo)
   12.24  apply (rule TR7 [THEN leadsTo_weaken_R])
   12.25  apply (auto simp add: HasTok_def nodeOrder_eq)
    13.1 --- a/src/HOL/UNITY/Transformers.thy	Tue Mar 13 21:17:37 2012 +0100
    13.2 +++ b/src/HOL/UNITY/Transformers.thy	Tue Mar 13 22:49:02 2012 +0100
    13.3 @@ -422,7 +422,7 @@
    13.4          W \<subseteq> insert (wens_single act B)
    13.5              (range (wens_single_finite act B))\<rbrakk>
    13.6         \<Longrightarrow> \<Union>W = wens_single act B"
    13.7 -apply (case_tac "wens_single act B \<in> W")
    13.8 +apply (cases "wens_single act B \<in> W")
    13.9   apply (blast dest: wens_single_finite_subset_wens_single [THEN subsetD]) 
   13.10  apply (simp add: wens_single_eq_Union) 
   13.11  apply (rule equalityI, blast)