# HG changeset patch
# User wenzelm
# Date 1331675342 -3600
# Node ID 6d2a2f0e904ec2a71f7ab198d81a6b65b4c01965
# Parent  3e068ef04b42a380338931399d2218cb63f20cad
tuned proofs;

diff -r 3e068ef04b42 -r 6d2a2f0e904e src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Tue Mar 13 21:17:37 2012 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Tue Mar 13 22:49:02 2012 +0100
@@ -749,7 +749,7 @@
 
 lemma client_preserves_giv_oo_client_map: "[| i < Nclients; j < Nclients |]
       ==> Client : preserves (giv o sub i o fst o lift_map j o client_map)"
-  apply (case_tac "i=j")
+  apply (cases "i=j")
   apply (simp, simp add: o_def non_dummy_def)
   apply (drule Client_preserves_dummy [THEN preserves_sub_fst_lift_map])
   apply (drule_tac [!] subset_preserves_o [THEN [2] rev_subsetD])
diff -r 3e068ef04b42 -r 6d2a2f0e904e src/HOL/UNITY/Comp/AllocBase.thy
--- a/src/HOL/UNITY/Comp/AllocBase.thy	Tue Mar 13 21:17:37 2012 +0100
+++ b/src/HOL/UNITY/Comp/AllocBase.thy	Tue Mar 13 22:49:02 2012 +0100
@@ -27,11 +27,8 @@
 apply (auto simp add: lessThan_Suc)
 done
 
-lemma tokens_mono_prefix [rule_format]:
-     "ALL xs. xs <= ys --> tokens xs <= tokens ys"
-apply (induct_tac "ys")
-apply (auto simp add: prefix_Cons)
-done
+lemma tokens_mono_prefix: "xs <= ys ==> tokens xs <= tokens ys"
+  by (induct ys arbitrary: xs) (auto simp add: prefix_Cons)
 
 lemma mono_tokens: "mono tokens"
 apply (unfold mono_def)
@@ -42,9 +39,7 @@
 (** bag_of **)
 
 lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'"
-apply (induct_tac "l", simp)
- apply (simp add: add_ac)
-done
+  by (induct l) (simp_all add: add_ac)
 
 lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)"
 apply (rule monoI)
diff -r 3e068ef04b42 -r 6d2a2f0e904e src/HOL/UNITY/Comp/Counter.thy
--- a/src/HOL/UNITY/Comp/Counter.thy	Tue Mar 13 21:17:37 2012 +0100
+++ b/src/HOL/UNITY/Comp/Counter.thy	Tue Mar 13 22:49:02 2012 +0100
@@ -41,40 +41,30 @@
 declare a_def [THEN def_act_simp, simp]
 
 (* Theorems about sum and sumj *)
-lemma sum_upd_gt [rule_format]: "\<forall>n. I<n --> sum I (s(c n := x)) = sum I s"
-by (induct_tac "I", auto)
+lemma sum_upd_gt: "I<n ==> sum I (s(c n := x)) = sum I s"
+  by (induct I) auto
 
 
 lemma sum_upd_eq: "sum I (s(c I := x)) = sum I s"
-apply (induct_tac "I")
-apply (auto simp add: sum_upd_gt [unfolded fun_upd_def])
-done
+  by (induct I) (auto simp add: sum_upd_gt [unfolded fun_upd_def])
 
 lemma sum_upd_C: "sum I (s(C := x)) = sum I s"
-by (induct_tac "I", auto)
+  by (induct I) auto
 
 lemma sumj_upd_ci: "sumj I i (s(c i := x)) = sumj I i s"
-apply (induct_tac "I")
-apply (auto simp add: sum_upd_eq [unfolded fun_upd_def])
-done
+  by (induct I) (auto simp add: sum_upd_eq [unfolded fun_upd_def])
 
 lemma sumj_upd_C: "sumj I i (s(C := x)) = sumj I i s"
-apply (induct_tac "I")
-apply (auto simp add: sum_upd_C [unfolded fun_upd_def])
-done
+  by (induct I) (auto simp add: sum_upd_C [unfolded fun_upd_def])
 
-lemma sumj_sum_gt [rule_format]: "\<forall>i. I<i--> (sumj I i s = sum I s)"
-by (induct_tac "I", auto)
+lemma sumj_sum_gt: "I<i ==> sumj I i s = sum I s"
+  by (induct I) auto
 
 lemma sumj_sum_eq: "(sumj I I s = sum I s)"
-apply (induct_tac "I", auto)
-apply (simp (no_asm) add: sumj_sum_gt)
-done
+  by (induct I) (auto simp add: sumj_sum_gt)
 
-lemma sum_sumj [rule_format]: "\<forall>i. i<I-->(sum I s = s (c i) +  sumj I i s)"
-apply (induct_tac "I")
-apply (auto simp add: linorder_neq_iff sumj_sum_eq)
-done
+lemma sum_sumj: "i<I ==> sum I s = s (c i) +  sumj I i s"
+  by (induct I) (auto simp add: linorder_neq_iff sumj_sum_eq)
 
 (* Correctness proofs for Components *)
 (* p2 and p3 proofs *)
@@ -103,8 +93,8 @@
 
 (* Compositional Proof *)
 
-lemma sum_0' [rule_format]: "(\<forall>i. i < I --> s (c i) = 0) --> sum I s = 0"
-by (induct_tac "I", auto)
+lemma sum_0': "(\<And>i. i < I ==> s (c i) = 0) ==> sum I s = 0"
+  by (induct I) auto
 
 (* I cannot be empty *)
 lemma safety:
diff -r 3e068ef04b42 -r 6d2a2f0e904e src/HOL/UNITY/Comp/Counterc.thy
--- a/src/HOL/UNITY/Comp/Counterc.thy	Tue Mar 13 21:17:37 2012 +0100
+++ b/src/HOL/UNITY/Comp/Counterc.thy	Tue Mar 13 22:49:02 2012 +0100
@@ -46,27 +46,20 @@
 declare a_def [THEN def_act_simp, simp]
 
 (* Theorems about sum and sumj *)
-lemma sum_sumj_eq1 [rule_format]: "\<forall>i. I<i--> (sum I s = sumj I i s)"
-by (induct_tac "I", auto)
+lemma sum_sumj_eq1: "I<i ==> sum I s = sumj I i s"
+  by (induct I) auto
 
-lemma sum_sumj_eq2 [rule_format]: "i<I --> sum I s  = c s i + sumj I i s"
-apply (induct_tac "I")
-apply (auto simp add: linorder_neq_iff sum_sumj_eq1)
-done
+lemma sum_sumj_eq2: "i<I ==> sum I s  = c s i + sumj I i s"
+  by (induct I) (auto simp add: linorder_neq_iff sum_sumj_eq1)
 
-lemma sum_ext [rule_format]:
-     "(\<forall>i. i<I --> c s' i = c s i) --> (sum I s' = sum I s)"
-by (induct_tac "I", auto)
+lemma sum_ext: "(\<And>i. i<I \<Longrightarrow> c s' i = c s i) ==> sum I s' = sum I s"
+  by (induct I) auto
 
-lemma sumj_ext [rule_format]:
-     "(\<forall>j. j<I & j\<noteq>i --> c s' j =  c s j) --> (sumj I i s' = sumj I i s)"
-apply (induct_tac "I", safe)
-apply (auto intro!: sum_ext)
-done
+lemma sumj_ext: "(\<And>j. j<I ==> j\<noteq>i ==> c s' j =  c s j) ==> sumj I i s' = sumj I i s"
+  by (induct I) (auto intro!: sum_ext)
 
-
-lemma sum0 [rule_format]: "(\<forall>i. i<I --> c s i = 0) -->  sum I s = 0"
-by (induct_tac "I", auto)
+lemma sum0: "(\<And>i. i<I ==> c s i = 0) ==> sum I s = 0"
+  by (induct I) auto
 
 
 (* Safety properties for Components *)
diff -r 3e068ef04b42 -r 6d2a2f0e904e src/HOL/UNITY/Comp/Priority.thy
--- a/src/HOL/UNITY/Comp/Priority.thy	Tue Mar 13 21:17:37 2012 +0100
+++ b/src/HOL/UNITY/Comp/Priority.thy	Tue Mar 13 22:49:02 2012 +0100
@@ -143,16 +143,12 @@
 
 
 text{* p15: universal property: all Components well behave  *}
-lemma system_well_behaves [rule_format]:
-     "\<forall>i. system \<in> Highest i co Highest i Un Lowest i"
-apply clarify
-apply (simp add: system_def Component_def mk_total_program_def totalize_JN, 
-       safety, auto)
-done
+lemma system_well_behaves: "system \<in> Highest i co Highest i Un Lowest i"
+  by (simp add: system_def Component_def mk_total_program_def totalize_JN, safety, auto)
 
 
 lemma Acyclic_eq: "Acyclic = (\<Inter>i. {s. i\<notin>above i s})"
-by (auto simp add: Acyclic_def acyclic_def trancl_converse)
+  by (auto simp add: Acyclic_def acyclic_def trancl_converse)
 
 
 lemmas system_co =
diff -r 3e068ef04b42 -r 6d2a2f0e904e src/HOL/UNITY/Comp/PriorityAux.thy
--- a/src/HOL/UNITY/Comp/PriorityAux.thy	Tue Mar 13 21:17:37 2012 +0100
+++ b/src/HOL/UNITY/Comp/PriorityAux.thy	Tue Mar 13 22:49:02 2012 +0100
@@ -94,8 +94,8 @@
 apply (unfold reach_def)
 apply (erule ImageE)
 apply (erule trancl_induct) 
- apply (case_tac "i=k", simp_all) 
-  apply (blast intro: r_into_trancl, blast, clarify) 
+ apply (cases "i=k", simp_all) 
+  apply (blast, blast, clarify) 
 apply (drule_tac x = y in spec)
 apply (drule_tac x = z in spec)
 apply (blast dest: r_into_trancl intro: trancl_trans)
diff -r 3e068ef04b42 -r 6d2a2f0e904e src/HOL/UNITY/ELT.thy
--- a/src/HOL/UNITY/ELT.thy	Tue Mar 13 21:17:37 2012 +0100
+++ b/src/HOL/UNITY/ELT.thy	Tue Mar 13 22:49:02 2012 +0100
@@ -207,7 +207,7 @@
      "[| F : A leadsTo[CC] A';  A'<=B' |] ==> F : A leadsTo[CC] B'"
 by (blast intro: subset_imp_leadsETo leadsETo_Trans)
 
-lemma leadsETo_weaken_L [rule_format]:
+lemma leadsETo_weaken_L:
      "[| F : A leadsTo[CC] A'; B<=A |] ==> F : B leadsTo[CC] A'"
 by (blast intro: leadsETo_Trans subset_imp_leadsETo)
 
@@ -420,15 +420,15 @@
 
 lemmas empty_LeadsETo = empty_subsetI [THEN subset_imp_LeadsETo]
 
-lemma LeadsETo_weaken_R [rule_format]:
+lemma LeadsETo_weaken_R:
      "[| F : A LeadsTo[CC] A';  A' <= B' |] ==> F : A LeadsTo[CC] B'"
-apply (simp (no_asm_use) add: LeadsETo_def)
+apply (simp add: LeadsETo_def)
 apply (blast intro: leadsETo_weaken_R)
 done
 
-lemma LeadsETo_weaken_L [rule_format]:
+lemma LeadsETo_weaken_L:
      "[| F : A LeadsTo[CC] A';  B <= A |] ==> F : B LeadsTo[CC] A'"
-apply (simp (no_asm_use) add: LeadsETo_def)
+apply (simp add: LeadsETo_def)
 apply (blast intro: leadsETo_weaken_L)
 done
 
diff -r 3e068ef04b42 -r 6d2a2f0e904e src/HOL/UNITY/Lift_prog.thy
--- a/src/HOL/UNITY/Lift_prog.thy	Tue Mar 13 21:17:37 2012 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy	Tue Mar 13 22:49:02 2012 +0100
@@ -301,7 +301,7 @@
     "[| F i \<in> (A <*> UNIV) co (B <*> UNIV);   
         F j \<in> preserves snd |]   
      ==> lift j (F j) \<in> (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))"
-apply (case_tac "i=j")
+apply (cases "i=j")
 apply (simp add: lift_def lift_set_def rename_constrains)
 apply (erule preserves_snd_lift_stable[THEN stableD, THEN constrains_weaken_R],
        assumption)
diff -r 3e068ef04b42 -r 6d2a2f0e904e src/HOL/UNITY/ListOrder.thy
--- a/src/HOL/UNITY/ListOrder.thy	Tue Mar 13 21:17:37 2012 +0100
+++ b/src/HOL/UNITY/ListOrder.thy	Tue Mar 13 22:49:02 2012 +0100
@@ -179,22 +179,16 @@
 subsection{*recursion equations*}
 
 lemma genPrefix_Nil [simp]: "((xs, []) : genPrefix r) = (xs = [])"
-apply (induct_tac "xs")
-prefer 2 apply blast
-apply simp
-done
+  by (induct xs) auto
 
 lemma same_genPrefix_genPrefix [simp]: 
     "refl r ==> ((xs@ys, xs@zs) : genPrefix r) = ((ys,zs) : genPrefix r)"
-apply (unfold refl_on_def)
-apply (induct_tac "xs")
-apply (simp_all (no_asm_simp))
-done
+  by (induct xs) (simp_all add: refl_on_def)
 
 lemma genPrefix_Cons:
      "((xs, y#ys) : genPrefix r) =  
       (xs=[] | (EX z zs. xs=z#zs & (z,y) : r & (zs,ys) : genPrefix r))"
-by (case_tac "xs", auto)
+  by (cases xs) auto
 
 lemma genPrefix_take_append:
      "[| refl r;  (xs,ys) : genPrefix r |]  
diff -r 3e068ef04b42 -r 6d2a2f0e904e src/HOL/UNITY/Simple/Reach.thy
--- a/src/HOL/UNITY/Simple/Reach.thy	Tue Mar 13 21:17:37 2012 +0100
+++ b/src/HOL/UNITY/Simple/Reach.thy	Tue Mar 13 22:49:02 2012 +0100
@@ -126,9 +126,7 @@
 by (erule Suc_metric [THEN subst], blast)
 
 lemma metric_le: "metric (s(y:=s x | s y)) \<le> metric s"
-apply (case_tac "s x --> s y")
-apply (auto intro: less_imp_le simp add: fun_upd_idem)
-done
+  by (cases "s x --> s y") (auto intro: less_imp_le simp add: fun_upd_idem)
 
 lemma LeadsTo_Diff_fixedpoint:
      "Rprg \<in> ((metric-`{m}) - fixedpoint) LeadsTo (metric-`(lessThan m))"
diff -r 3e068ef04b42 -r 6d2a2f0e904e src/HOL/UNITY/Simple/Reachability.thy
--- a/src/HOL/UNITY/Simple/Reachability.thy	Tue Mar 13 21:17:37 2012 +0100
+++ b/src/HOL/UNITY/Simple/Reachability.thy	Tue Mar 13 22:49:02 2012 +0100
@@ -319,7 +319,7 @@
 done
 
 lemma LeadsTo_final: "F \<in> UNIV LeadsTo final"
-apply (case_tac "E={}")
+apply (cases "E={}")
  apply (rule_tac [2] LeadsTo_final_E_NOT_empty)
 apply (rule LeadsTo_final_E_empty, auto)
 done
@@ -361,7 +361,7 @@
 done
 
 lemma Stable_final: "F \<in> Stable final"
-apply (case_tac "E={}")
+apply (cases "E={}")
  prefer 2 apply (blast intro: Stable_final_E_NOT_empty)
 apply (blast intro: Stable_final_E_empty)
 done
diff -r 3e068ef04b42 -r 6d2a2f0e904e src/HOL/UNITY/Simple/Token.thy
--- a/src/HOL/UNITY/Simple/Token.thy	Tue Mar 13 21:17:37 2012 +0100
+++ b/src/HOL/UNITY/Simple/Token.thy	Tue Mar 13 22:49:02 2012 +0100
@@ -56,7 +56,7 @@
 
 lemma not_E_eq: "(s \<notin> E i) = (s \<in> H i | s \<in> T i)"
 apply (simp add: H_def E_def T_def)
-apply (case_tac "proc s i", auto)
+apply (cases "proc s i", auto)
 done
 
 lemma (in Token) token_stable: "F \<in> stable (-(E i) \<union> (HasTok i))"
@@ -83,11 +83,11 @@
 done
 
 text{*From "A Logic for Concurrent Programming", but not used in Chapter 4.
-  Note the use of @{text case_tac}.  Reasoning about leadsTo takes practice!*}
+  Note the use of @{text cases}.  Reasoning about leadsTo takes practice!*}
 lemma (in Token) TR7_nodeOrder:
      "[| i<N; j<N |] ==>    
       F \<in> (HasTok i) leadsTo ({s. (token s, i) \<in> nodeOrder j} \<union> HasTok j)"
-apply (case_tac "i=j")
+apply (cases "i=j")
 apply (blast intro: subset_imp_leadsTo)
 apply (rule TR7 [THEN leadsTo_weaken_R])
 apply (auto simp add: HasTok_def nodeOrder_eq)
diff -r 3e068ef04b42 -r 6d2a2f0e904e src/HOL/UNITY/Transformers.thy
--- a/src/HOL/UNITY/Transformers.thy	Tue Mar 13 21:17:37 2012 +0100
+++ b/src/HOL/UNITY/Transformers.thy	Tue Mar 13 22:49:02 2012 +0100
@@ -422,7 +422,7 @@
         W \<subseteq> insert (wens_single act B)
             (range (wens_single_finite act B))\<rbrakk>
        \<Longrightarrow> \<Union>W = wens_single act B"
-apply (case_tac "wens_single act B \<in> W")
+apply (cases "wens_single act B \<in> W")
  apply (blast dest: wens_single_finite_subset_wens_single [THEN subsetD]) 
 apply (simp add: wens_single_eq_Union) 
 apply (rule equalityI, blast)