--- 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])
--- 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)
--- 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:
--- 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 *)
--- 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 =
--- 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)
--- 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
--- 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)
--- 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 |]
--- 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))"
--- 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
--- 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)
--- 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)