1.1 --- a/src/HOL/Bali/AxCompl.thy	Fri May 25 13:19:10 2012 +0200
     1.2 +++ b/src/HOL/Bali/AxCompl.thy	Fri May 25 13:23:43 2012 +0200
     1.3 @@ -38,49 +38,32 @@
     1.4  
     1.5  lemma nyinitcls_set_locals_cong [simp]: 
     1.6    "nyinitcls G (x,set_locals l s) = nyinitcls G (x,s)"
     1.7 -apply (unfold nyinitcls_def)
     1.8 -apply (simp (no_asm))
     1.9 -done
    1.10 +  by (simp add: nyinitcls_def)
    1.11  
    1.12  lemma nyinitcls_abrupt_cong [simp]: "nyinitcls G (f x, y) = nyinitcls G (x, y)"
    1.13 -apply (unfold nyinitcls_def)
    1.14 -apply (simp (no_asm))
    1.15 -done
    1.16 +  by (simp add: nyinitcls_def)
    1.17  
    1.18 -lemma nyinitcls_abupd_cong [simp]:"!!s. nyinitcls G (abupd f s) = nyinitcls G s"
    1.19 -apply (unfold nyinitcls_def)
    1.20 -apply (simp (no_asm_simp) only: split_tupled_all)
    1.21 -apply (simp (no_asm))
    1.22 -done
    1.23 +lemma nyinitcls_abupd_cong [simp]: "nyinitcls G (abupd f s) = nyinitcls G s"
    1.24 +  by (simp add: nyinitcls_def)
    1.25  
    1.26  lemma card_nyinitcls_abrupt_congE [elim!]: 
    1.27 -        "card (nyinitcls G (x, s)) \<le> n \<Longrightarrow> card (nyinitcls G (y, s)) \<le> n"
    1.28 -apply (unfold nyinitcls_def)
    1.29 -apply auto
    1.30 -done
    1.31 +  "card (nyinitcls G (x, s)) \<le> n \<Longrightarrow> card (nyinitcls G (y, s)) \<le> n"
    1.32 +  unfolding nyinitcls_def by auto
    1.33  
    1.34  lemma nyinitcls_new_xcpt_var [simp]: 
    1.35 -"nyinitcls G (new_xcpt_var vn s) = nyinitcls G s"
    1.36 -apply (unfold nyinitcls_def)
    1.37 -apply (induct_tac "s")
    1.38 -apply (simp (no_asm))
    1.39 -done
    1.40 +  "nyinitcls G (new_xcpt_var vn s) = nyinitcls G s"
    1.41 +  by (induct s) (simp_all add: nyinitcls_def)
    1.42  
    1.43  lemma nyinitcls_init_lvars [simp]: 
    1.44    "nyinitcls G ((init_lvars G C sig mode a' pvs) s) = nyinitcls G s"
    1.45 -apply (induct_tac "s")
    1.46 -apply (simp (no_asm) add: init_lvars_def2 split add: split_if)
    1.47 -done
    1.48 +  by (induct s) (simp add: init_lvars_def2 split add: split_if)
    1.49  
    1.50  lemma nyinitcls_emptyD: "\<lbrakk>nyinitcls G s = {}; is_class G C\<rbrakk> \<Longrightarrow> initd C s"
    1.51 -apply (unfold nyinitcls_def)
    1.52 -apply fast
    1.53 -done
    1.54 +  unfolding nyinitcls_def by fast
    1.55  
    1.56  lemma card_Suc_lemma: 
    1.57    "\<lbrakk>card (insert a A) \<le> Suc n; a\<notin>A; finite A\<rbrakk> \<Longrightarrow> card A \<le> n"
    1.58 -apply clarsimp
    1.59 -done
    1.60 +  by auto
    1.61  
    1.62  lemma nyinitcls_le_SucD: 
    1.63  "\<lbrakk>card (nyinitcls G (x,s)) \<le> Suc n; \<not>inited C (globs s); class G C=Some y\<rbrakk> \<Longrightarrow> 
    1.64 @@ -95,12 +78,10 @@
    1.65  done
    1.66  
    1.67  lemma inited_gext': "\<lbrakk>s\<le>|s';inited C (globs s)\<rbrakk> \<Longrightarrow> inited C (globs s')"
    1.68 -by (rule inited_gext)
    1.69 +  by (rule inited_gext)
    1.70  
    1.71  lemma nyinitcls_gext: "snd s\<le>|snd s' \<Longrightarrow> nyinitcls G s' \<subseteq> nyinitcls G s"
    1.72 -apply (unfold nyinitcls_def)
    1.73 -apply (force dest!: inited_gext')
    1.74 -done
    1.75 +  unfolding nyinitcls_def by (force dest!: inited_gext')
    1.76  
    1.77  lemma card_nyinitcls_gext: 
    1.78    "\<lbrakk>snd s\<le>|snd s'; card (nyinitcls G s) \<le> n\<rbrakk>\<Longrightarrow> card (nyinitcls G s') \<le> n"
    1.79 @@ -161,19 +142,16 @@
    1.80  
    1.81  lemma MGF_res_eq_lemma [simp]: 
    1.82    "(\<forall>Y' Y s. Y = Y' \<and> P s \<longrightarrow> Q s) = (\<forall>s. P s \<longrightarrow> Q s)"
    1.83 -apply auto
    1.84 -done
    1.85 +  by auto
    1.86  
    1.87  lemma MGFn_def2: 
    1.88  "G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>} = G,A\<turnstile>{\<doteq> \<and>. G\<turnstile>init\<le>n} 
    1.89                      t\<succ> {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}"
    1.90 -apply (unfold MGFn_def MGF_def)
    1.91 -apply fast
    1.92 -done
    1.93 +  unfolding MGFn_def MGF_def by fast
    1.94  
    1.95  lemma MGF_MGFn_iff: 
    1.96  "G,(A::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>} = (\<forall>n. G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>})"
    1.97 -apply (simp (no_asm_use) add: MGFn_def2 MGF_def)
    1.98 +apply (simp add: MGFn_def2 MGF_def)
    1.99  apply safe
   1.100  apply  (erule_tac [2] All_init_leD)
   1.101  apply (erule conseq1)

     2.1 --- a/src/HOL/Bali/WellType.thy	Fri May 25 13:19:10 2012 +0200
     2.2 +++ b/src/HOL/Bali/WellType.thy	Fri May 25 13:23:43 2012 +0200
     2.3 @@ -668,7 +668,7 @@
     2.4  apply (tactic {*ALLGOALS (eresolve_tac @{thms wt_elim_cases})*})
     2.5  apply (simp_all (no_asm_use) split del: split_if_asm)
     2.6  apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *)
     2.7 -apply ((blast del: equalityCE dest: sym [THEN trans])+)
     2.8 +apply (blast del: equalityCE dest: sym [THEN trans])+
     2.9  done
    2.10  
    2.11  (* unused *)
    2.12 @@ -680,19 +680,11 @@
    2.13  apply (auto intro!: widen_antisym)
    2.14  done
    2.15  
    2.16 -lemma typeof_empty_is_type [rule_format (no_asm)]: 
    2.17 -  "typeof (\<lambda>a. None) v = Some T \<longrightarrow> is_type G T"
    2.18 -apply (rule val.induct)
    2.19 -apply           auto
    2.20 -done
    2.21 +lemma typeof_empty_is_type: "typeof (\<lambda>a. None) v = Some T \<Longrightarrow> is_type G T"
    2.22 +  by (induct v) auto
    2.23  
    2.24  (* unused *)
    2.25 -lemma typeof_is_type [rule_format (no_asm)]: 
    2.26 - "(\<forall>a. v \<noteq> Addr a) \<longrightarrow> (\<exists>T. typeof dt v = Some T \<and> is_type G T)"
    2.27 -apply (rule val.induct)
    2.28 -prefer 5 
    2.29 -apply     fast
    2.30 -apply  (simp_all (no_asm))
    2.31 -done
    2.32 +lemma typeof_is_type: "(\<forall>a. v \<noteq> Addr a) \<Longrightarrow> \<exists>T. typeof dt v = Some T \<and> is_type G T"
    2.33 +  by (induct v) auto
    2.34  
    2.35  end