tuned proofs;

--- a/src/HOL/Bali/AxCompl.thy	Fri May 25 13:19:10 2012 +0200
+++ b/src/HOL/Bali/AxCompl.thy	Fri May 25 13:23:43 2012 +0200
@@ -38,49 +38,32 @@
 
 lemma nyinitcls_set_locals_cong [simp]: 
   "nyinitcls G (x,set_locals l s) = nyinitcls G (x,s)"
-apply (unfold nyinitcls_def)
-apply (simp (no_asm))
-done
+  by (simp add: nyinitcls_def)
 
 lemma nyinitcls_abrupt_cong [simp]: "nyinitcls G (f x, y) = nyinitcls G (x, y)"
-apply (unfold nyinitcls_def)
-apply (simp (no_asm))
-done
+  by (simp add: nyinitcls_def)
 
-lemma nyinitcls_abupd_cong [simp]:"!!s. nyinitcls G (abupd f s) = nyinitcls G s"
-apply (unfold nyinitcls_def)
-apply (simp (no_asm_simp) only: split_tupled_all)
-apply (simp (no_asm))
-done
+lemma nyinitcls_abupd_cong [simp]: "nyinitcls G (abupd f s) = nyinitcls G s"
+  by (simp add: nyinitcls_def)
 
 lemma card_nyinitcls_abrupt_congE [elim!]: 
-        "card (nyinitcls G (x, s)) \<le> n \<Longrightarrow> card (nyinitcls G (y, s)) \<le> n"
-apply (unfold nyinitcls_def)
-apply auto
-done
+  "card (nyinitcls G (x, s)) \<le> n \<Longrightarrow> card (nyinitcls G (y, s)) \<le> n"
+  unfolding nyinitcls_def by auto
 
 lemma nyinitcls_new_xcpt_var [simp]: 
-"nyinitcls G (new_xcpt_var vn s) = nyinitcls G s"
-apply (unfold nyinitcls_def)
-apply (induct_tac "s")
-apply (simp (no_asm))
-done
+  "nyinitcls G (new_xcpt_var vn s) = nyinitcls G s"
+  by (induct s) (simp_all add: nyinitcls_def)
 
 lemma nyinitcls_init_lvars [simp]: 
   "nyinitcls G ((init_lvars G C sig mode a' pvs) s) = nyinitcls G s"
-apply (induct_tac "s")
-apply (simp (no_asm) add: init_lvars_def2 split add: split_if)
-done
+  by (induct s) (simp add: init_lvars_def2 split add: split_if)
 
 lemma nyinitcls_emptyD: "\<lbrakk>nyinitcls G s = {}; is_class G C\<rbrakk> \<Longrightarrow> initd C s"
-apply (unfold nyinitcls_def)
-apply fast
-done
+  unfolding nyinitcls_def by fast
 
 lemma card_Suc_lemma: 
   "\<lbrakk>card (insert a A) \<le> Suc n; a\<notin>A; finite A\<rbrakk> \<Longrightarrow> card A \<le> n"
-apply clarsimp
-done
+  by auto
 
 lemma nyinitcls_le_SucD: 
 "\<lbrakk>card (nyinitcls G (x,s)) \<le> Suc n; \<not>inited C (globs s); class G C=Some y\<rbrakk> \<Longrightarrow> 
@@ -95,12 +78,10 @@
 done
 
 lemma inited_gext': "\<lbrakk>s\<le>|s';inited C (globs s)\<rbrakk> \<Longrightarrow> inited C (globs s')"
-by (rule inited_gext)
+  by (rule inited_gext)
 
 lemma nyinitcls_gext: "snd s\<le>|snd s' \<Longrightarrow> nyinitcls G s' \<subseteq> nyinitcls G s"
-apply (unfold nyinitcls_def)
-apply (force dest!: inited_gext')
-done
+  unfolding nyinitcls_def by (force dest!: inited_gext')
 
 lemma card_nyinitcls_gext: 
   "\<lbrakk>snd s\<le>|snd s'; card (nyinitcls G s) \<le> n\<rbrakk>\<Longrightarrow> card (nyinitcls G s') \<le> n"
@@ -161,19 +142,16 @@
 
 lemma MGF_res_eq_lemma [simp]: 
   "(\<forall>Y' Y s. Y = Y' \<and> P s \<longrightarrow> Q s) = (\<forall>s. P s \<longrightarrow> Q s)"
-apply auto
-done
+  by auto
 
 lemma MGFn_def2: 
 "G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>} = G,A\<turnstile>{\<doteq> \<and>. G\<turnstile>init\<le>n} 
                     t\<succ> {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}"
-apply (unfold MGFn_def MGF_def)
-apply fast
-done
+  unfolding MGFn_def MGF_def by fast
 
 lemma MGF_MGFn_iff: 
 "G,(A::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>} = (\<forall>n. G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>})"
-apply (simp (no_asm_use) add: MGFn_def2 MGF_def)
+apply (simp add: MGFn_def2 MGF_def)
 apply safe
 apply  (erule_tac [2] All_init_leD)
 apply (erule conseq1)

--- a/src/HOL/Bali/WellType.thy	Fri May 25 13:19:10 2012 +0200
+++ b/src/HOL/Bali/WellType.thy	Fri May 25 13:23:43 2012 +0200
@@ -668,7 +668,7 @@
 apply (tactic {*ALLGOALS (eresolve_tac @{thms wt_elim_cases})*})
 apply (simp_all (no_asm_use) split del: split_if_asm)
 apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *)
-apply ((blast del: equalityCE dest: sym [THEN trans])+)
+apply (blast del: equalityCE dest: sym [THEN trans])+
 done
 
 (* unused *)
@@ -680,19 +680,11 @@
 apply (auto intro!: widen_antisym)
 done
 
-lemma typeof_empty_is_type [rule_format (no_asm)]: 
-  "typeof (\<lambda>a. None) v = Some T \<longrightarrow> is_type G T"
-apply (rule val.induct)
-apply           auto
-done
+lemma typeof_empty_is_type: "typeof (\<lambda>a. None) v = Some T \<Longrightarrow> is_type G T"
+  by (induct v) auto
 
 (* unused *)
-lemma typeof_is_type [rule_format (no_asm)]: 
- "(\<forall>a. v \<noteq> Addr a) \<longrightarrow> (\<exists>T. typeof dt v = Some T \<and> is_type G T)"
-apply (rule val.induct)
-prefer 5 
-apply     fast
-apply  (simp_all (no_asm))
-done
+lemma typeof_is_type: "(\<forall>a. v \<noteq> Addr a) \<Longrightarrow> \<exists>T. typeof dt v = Some T \<and> is_type G T"
+  by (induct v) auto
 
 end