tuned ML/simproc declarations;
authorwenzelm
Sat Jul 28 20:40:22 2007 +0200 (2007-07-28)
changeset 2401967bde7cfcf10
parent 24018 edd20fe274b5
child 24020 ed4d7abffee7
tuned ML/simproc declarations;
src/HOL/Bali/AxSem.thy
src/HOL/Bali/AxSound.thy
src/HOL/Bali/Basis.thy
src/HOL/Bali/DefiniteAssignment.thy
src/HOL/Bali/DefiniteAssignmentCorrect.thy
src/HOL/Bali/Eval.thy
src/HOL/Bali/Evaln.thy
src/HOL/Bali/Example.thy
src/HOL/Bali/Term.thy
src/HOL/Bali/TypeSafe.thy
src/HOL/Bali/WellForm.thy
src/HOL/Bali/WellType.thy
     1.1 --- a/src/HOL/Bali/AxSem.thy	Sat Jul 28 20:40:20 2007 +0200
     1.2 +++ b/src/HOL/Bali/AxSem.thy	Sat Jul 28 20:40:22 2007 +0200
     1.3 @@ -471,10 +471,8 @@
     1.4  declare split_paired_All [simp del] split_paired_Ex [simp del] 
     1.5  declare split_if     [split del] split_if_asm     [split del] 
     1.6          option.split [split del] option.split_asm [split del]
     1.7 -ML_setup {*
     1.8 -change_simpset (fn ss => ss delloop "split_all_tac");
     1.9 -change_claset (fn cs => cs delSWrapper "split_all_tac");
    1.10 -*}
    1.11 +declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
    1.12 +declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
    1.13  
    1.14  inductive
    1.15    ax_derivs :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool" ("_,_|\<turnstile>_" [61,58,58] 57)
    1.16 @@ -1015,9 +1013,7 @@
    1.17  apply  (auto simp add: type_ok_def)
    1.18  done
    1.19  
    1.20 -ML {*
    1.21 -bind_thms ("ax_Abrupts", sum3_instantiate (thm "ax_derivs.Abrupt"))
    1.22 -*}
    1.23 +ML_setup {* bind_thms ("ax_Abrupts", sum3_instantiate @{thm ax_derivs.Abrupt}) *}
    1.24  declare ax_Abrupts [intro!]
    1.25  
    1.26  lemmas ax_Normal_cases = ax_cases [of _ _ _ normal]
     2.1 --- a/src/HOL/Bali/AxSound.thy	Sat Jul 28 20:40:20 2007 +0200
     2.2 +++ b/src/HOL/Bali/AxSound.thy	Sat Jul 28 20:40:22 2007 +0200
     2.3 @@ -210,9 +210,7 @@
     2.4  done
     2.5    
     2.6  
     2.7 -
     2.8 -
     2.9 -ML "Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]"
    2.10 +declare [[simproc add: wt_expr wt_var wt_exprs wt_stmt]]
    2.11  
    2.12  lemma valid_stmtI: 
    2.13     assumes I: "\<And> n s0 L accC C s1 Y Z.
     3.1 --- a/src/HOL/Bali/Basis.thy	Sat Jul 28 20:40:20 2007 +0200
     3.2 +++ b/src/HOL/Bali/Basis.thy	Sat Jul 28 20:40:22 2007 +0200
     3.3 @@ -11,22 +11,13 @@
     3.4  Unify.search_bound := 40;
     3.5  Unify.trace_bound  := 40;
     3.6  *}
     3.7 -(*print_depth 100;*)
     3.8 -(*Syntax.ambiguity_level := 1;*)
     3.9  
    3.10  section "misc"
    3.11  
    3.12  declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *)
    3.13  
    3.14 -ML {*
    3.15 -fun cond_simproc name pat pred thm = Simplifier.simproc (Thm.theory_of_thm thm) name [pat]
    3.16 -  (fn _ => fn _ => fn t => if pred t then NONE else SOME (mk_meta_eq thm));
    3.17 -*}
    3.18 -
    3.19  declare split_if_asm  [split] option.split [split] option.split_asm [split]
    3.20 -ML {*
    3.21 -change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
    3.22 -*}
    3.23 +declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
    3.24  declare if_weak_cong [cong del] option.weak_case_cong [cong del]
    3.25  declare length_Suc_conv [iff]
    3.26  
     4.1 --- a/src/HOL/Bali/DefiniteAssignment.thy	Sat Jul 28 20:40:20 2007 +0200
     4.2 +++ b/src/HOL/Bali/DefiniteAssignment.thy	Sat Jul 28 20:40:22 2007 +0200
     4.3 @@ -820,9 +820,8 @@
     4.4  declare inj_term_sym_simps [simp]
     4.5  declare assigns_if.simps [simp del]
     4.6  declare split_paired_All [simp del] split_paired_Ex [simp del]
     4.7 -ML_setup {*
     4.8 -change_simpset (fn ss => ss delloop "split_all_tac");
     4.9 -*}
    4.10 +declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
    4.11 +
    4.12  inductive_cases da_elim_cases [cases set]:
    4.13    "Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A" 
    4.14    "Env\<turnstile> B \<guillemotright>In1r Skip\<guillemotright> A" 
    4.15 @@ -887,9 +886,8 @@
    4.16  declare inj_term_sym_simps [simp del]
    4.17  declare assigns_if.simps [simp]
    4.18  declare split_paired_All [simp] split_paired_Ex [simp]
    4.19 -ML_setup {*
    4.20 -change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
    4.21 -*}
    4.22 +declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
    4.23 +
    4.24  (* To be able to eliminate both the versions with the overloaded brackets: 
    4.25     (B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A) and with the explicit constructor (B \<guillemotright>In1r Skip\<guillemotright> A), 
    4.26     every rule appears in both versions
     5.1 --- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Sat Jul 28 20:40:20 2007 +0200
     5.2 +++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Sat Jul 28 20:40:22 2007 +0200
     5.3 @@ -4,9 +4,7 @@
     5.4  
     5.5  theory DefiniteAssignmentCorrect imports WellForm Eval begin
     5.6  
     5.7 -ML {*
     5.8 -Delsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
     5.9 -*}
    5.10 +declare [[simproc del: wt_expr wt_var wt_exprs wt_stmt]]
    5.11  
    5.12  lemma sxalloc_no_jump:
    5.13    assumes sxalloc: "G\<turnstile>s0 \<midarrow>sxalloc\<rightarrow> s1" and
    5.14 @@ -4496,7 +4494,6 @@
    5.15      using that by (rule da_good_approxE) iprover+
    5.16  qed
    5.17  
    5.18 -ML {*
    5.19 -Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
    5.20 -*}
    5.21 +declare [[simproc add: wt_expr wt_var wt_exprs wt_stmt]]
    5.22 +
    5.23  end
     6.1 --- a/src/HOL/Bali/Eval.thy	Sat Jul 28 20:40:20 2007 +0200
     6.2 +++ b/src/HOL/Bali/Eval.thy	Sat Jul 28 20:40:22 2007 +0200
     6.3 @@ -749,12 +749,12 @@
     6.4   29(AVar),24(Call)]
     6.5  *)
     6.6  
     6.7 -ML {*
     6.8 +ML_setup {*
     6.9  bind_thm ("eval_induct_", rearrange_prems 
    6.10  [0,1,2,8,4,30,31,27,15,16,
    6.11   17,18,19,20,21,3,5,25,26,23,6,
    6.12   7,11,9,13,14,12,22,10,28,
    6.13 - 29,24] (thm "eval.induct"))
    6.14 + 29,24] @{thm eval.induct})
    6.15  *}
    6.16  
    6.17  
    6.18 @@ -790,9 +790,8 @@
    6.19  
    6.20  declare not_None_eq [simp del] (* IntDef.Zero_def [simp del] *)
    6.21  declare split_paired_All [simp del] split_paired_Ex [simp del]
    6.22 -ML_setup {*
    6.23 -change_simpset (fn ss => ss delloop "split_all_tac");
    6.24 -*}
    6.25 +declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
    6.26 +
    6.27  inductive_cases eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v, s')"
    6.28  
    6.29  inductive_cases eval_elim_cases [cases set]:
    6.30 @@ -829,9 +828,7 @@
    6.31  	"G\<turnstile>Norm s \<midarrow>In1r (Init C)                       \<succ>\<rightarrow> (x, s')"
    6.32  declare not_None_eq [simp]  (* IntDef.Zero_def [simp] *)
    6.33  declare split_paired_All [simp] split_paired_Ex [simp]
    6.34 -ML_setup {*
    6.35 -change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
    6.36 -*}
    6.37 +declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
    6.38  declare split_if     [split] split_if_asm     [split] 
    6.39          option.split [split] option.split_asm [split]
    6.40  
    6.41 @@ -869,25 +866,35 @@
    6.42  lemma eval_stmt_eq: "G\<turnstile>s \<midarrow>In1r t\<succ>\<rightarrow> (w, s') = (w=\<diamondsuit> \<and> G\<turnstile>s \<midarrow>t \<rightarrow> s')"
    6.43    by (auto, frule eval_Inj_elim, auto, frule eval_Inj_elim, auto)
    6.44  
    6.45 +simproc_setup eval_expr ("G\<turnstile>s \<midarrow>In1l t\<succ>\<rightarrow> (w, s')") = {*
    6.46 +  fn _ => fn _ => fn ct =>
    6.47 +    (case Thm.term_of ct of
    6.48 +      (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
    6.49 +    | _ => SOME (mk_meta_eq @{thm eval_expr_eq})) *}
    6.50 +
    6.51 +simproc_setup eval_var ("G\<turnstile>s \<midarrow>In2 t\<succ>\<rightarrow> (w, s')") = {*
    6.52 +  fn _ => fn _ => fn ct =>
    6.53 +    (case Thm.term_of ct of
    6.54 +      (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
    6.55 +    | _ => SOME (mk_meta_eq @{thm eval_var_eq})) *}
    6.56 +
    6.57 +simproc_setup eval_exprs ("G\<turnstile>s \<midarrow>In3 t\<succ>\<rightarrow> (w, s')") = {*
    6.58 +  fn _ => fn _ => fn ct =>
    6.59 +    (case Thm.term_of ct of
    6.60 +      (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
    6.61 +    | _ => SOME (mk_meta_eq @{thm eval_exprs_eq})) *}
    6.62 +
    6.63 +simproc_setup eval_stmt ("G\<turnstile>s \<midarrow>In1r t\<succ>\<rightarrow> (w, s')") = {*
    6.64 +  fn _ => fn _ => fn ct =>
    6.65 +    (case Thm.term_of ct of
    6.66 +      (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
    6.67 +    | _ => SOME (mk_meta_eq @{thm eval_stmt_eq})) *}
    6.68 +
    6.69  ML_setup {*
    6.70 -fun eval_fun name lhs =
    6.71 -let
    6.72 -  fun is_Inj (Const (inj,_) $ _) = true
    6.73 -    | is_Inj _                   = false
    6.74 -  fun pred (_ $ _ $ _ $ _ $ x $ _) = is_Inj x
    6.75 -in
    6.76 -  cond_simproc name lhs pred (thm name)
    6.77 -end
    6.78 -
    6.79 -val eval_expr_proc  = eval_fun "eval_expr_eq"  "G\<turnstile>s \<midarrow>In1l t\<succ>\<rightarrow> (w, s')";
    6.80 -val eval_var_proc   = eval_fun "eval_var_eq"   "G\<turnstile>s \<midarrow>In2 t\<succ>\<rightarrow> (w, s')";
    6.81 -val eval_exprs_proc = eval_fun "eval_exprs_eq" "G\<turnstile>s \<midarrow>In3 t\<succ>\<rightarrow> (w, s')";
    6.82 -val eval_stmt_proc  = eval_fun "eval_stmt_eq"  "G\<turnstile>s \<midarrow>In1r t\<succ>\<rightarrow> (w, s')";
    6.83 -Addsimprocs [eval_expr_proc,eval_var_proc,eval_exprs_proc,eval_stmt_proc];
    6.84 -bind_thms ("AbruptIs", sum3_instantiate (thm "eval.Abrupt"))
    6.85 +bind_thms ("AbruptIs", sum3_instantiate @{thm eval.Abrupt})
    6.86  *}
    6.87  
    6.88 -declare halloc.Abrupt [intro!] eval.Abrupt [intro!]  AbruptIs [intro!] 
    6.89 +declare halloc.Abrupt [intro!] eval.Abrupt [intro!]  AbruptIs [intro!]
    6.90  
    6.91  text{* @{text Callee},@{text InsInitE}, @{text InsInitV}, @{text FinA} are only
    6.92  used in smallstep semantics, not in the bigstep semantics. So their is no
    6.93 @@ -955,17 +962,11 @@
    6.94  apply (frule eval_no_abrupt_lemma, auto)+
    6.95  done
    6.96  
    6.97 -ML {*
    6.98 -local
    6.99 -  fun is_None (Const ("Datatype.option.None",_)) = true
   6.100 -    | is_None _ = false
   6.101 -  fun pred (_ $ _ $ (Const ("Pair", _) $ x $ _) $ _  $ _ $ _) = is_None x
   6.102 -in
   6.103 -  val eval_no_abrupt_proc = 
   6.104 -  cond_simproc "eval_no_abrupt" "G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')" pred 
   6.105 -          (thm "eval_no_abrupt")
   6.106 -end;
   6.107 -Addsimprocs [eval_no_abrupt_proc]
   6.108 +simproc_setup eval_no_abrupt ("G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')") = {*
   6.109 +  fn _ => fn _ => fn ct =>
   6.110 +    (case Thm.term_of ct of
   6.111 +      (_ $ _ $ (Const ("Pair", _) $ (Const ("Datatype.option.None",_)) $ _) $ _  $ _ $ _) => NONE
   6.112 +    | _ => SOME (mk_meta_eq @{thm eval_no_abrupt}))
   6.113  *}
   6.114  
   6.115  
   6.116 @@ -981,17 +982,11 @@
   6.117  apply (frule eval_abrupt_lemma, auto)+
   6.118  done
   6.119  
   6.120 -ML {*
   6.121 -local
   6.122 -  fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true
   6.123 -    | is_Some _ = false
   6.124 -  fun pred (_ $ _ $ _ $ _ $ _ $ x) = is_Some x
   6.125 -in
   6.126 -  val eval_abrupt_proc = 
   6.127 -  cond_simproc "eval_abrupt" 
   6.128 -               "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')" pred (thm "eval_abrupt")
   6.129 -end;
   6.130 -Addsimprocs [eval_abrupt_proc]
   6.131 +simproc_setup eval_abrupt ("G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')") = {*
   6.132 +  fn _ => fn _ => fn ct =>
   6.133 +    (case Thm.term_of ct of
   6.134 +      (_ $ _ $ _ $ _ $ _ $ (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _)) => NONE
   6.135 +    | _ => SOME (mk_meta_eq @{thm eval_abrupt}))
   6.136  *}
   6.137  
   6.138  
     7.1 --- a/src/HOL/Bali/Evaln.thy	Sat Jul 28 20:40:20 2007 +0200
     7.2 +++ b/src/HOL/Bali/Evaln.thy	Sat Jul 28 20:40:22 2007 +0200
     7.3 @@ -198,9 +198,8 @@
     7.4          option.split [split del] option.split_asm [split del]
     7.5          not_None_eq [simp del] 
     7.6          split_paired_All [simp del] split_paired_Ex [simp del]
     7.7 -ML_setup {*
     7.8 -change_simpset (fn ss => ss delloop "split_all_tac");
     7.9 -*}
    7.10 +declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
    7.11 +
    7.12  inductive_cases evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s')"
    7.13  
    7.14  inductive_cases evaln_elim_cases:
    7.15 @@ -241,9 +240,8 @@
    7.16          option.split [split] option.split_asm [split]
    7.17          not_None_eq [simp] 
    7.18          split_paired_All [simp] split_paired_Ex [simp]
    7.19 -ML_setup {*
    7.20 -change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
    7.21 -*}
    7.22 +declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
    7.23 +
    7.24  lemma evaln_Inj_elim: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s') \<Longrightarrow> case t of In1 ec \<Rightarrow>  
    7.25    (case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v) | Inr c \<Rightarrow> w = \<diamondsuit>)  
    7.26    | In2 e \<Rightarrow> (\<exists>v. w = In2 v) | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
    7.27 @@ -272,24 +270,31 @@
    7.28  lemma evaln_stmt_eq: "G\<turnstile>s \<midarrow>In1r t\<succ>\<midarrow>n\<rightarrow> (w, s') = (w=\<diamondsuit> \<and> G\<turnstile>s \<midarrow>t \<midarrow>n\<rightarrow> s')"
    7.29    by (auto, frule evaln_Inj_elim, auto, frule evaln_Inj_elim, auto)
    7.30  
    7.31 -ML_setup {*
    7.32 -fun enf name lhs =
    7.33 -let
    7.34 -  fun is_Inj (Const (inj,_) $ _) = true
    7.35 -    | is_Inj _                   = false
    7.36 -  fun pred (_ $ _ $ _ $ _ $ _ $ x $ _) = is_Inj x
    7.37 -in
    7.38 -  cond_simproc name lhs pred (thm name)
    7.39 -end;
    7.40 +simproc_setup evaln_expr ("G\<turnstile>s \<midarrow>In1l t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {*
    7.41 +  fn _ => fn _ => fn ct =>
    7.42 +    (case Thm.term_of ct of
    7.43 +      (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
    7.44 +    | _ => SOME (mk_meta_eq @{thm evaln_expr_eq})) *}
    7.45 +
    7.46 +simproc_setup evaln_var ("G\<turnstile>s \<midarrow>In2 t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {*
    7.47 +  fn _ => fn _ => fn ct =>
    7.48 +    (case Thm.term_of ct of
    7.49 +      (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
    7.50 +    | _ => SOME (mk_meta_eq @{thm evaln_var_eq})) *}
    7.51  
    7.52 -val evaln_expr_proc  = enf "evaln_expr_eq"  "G\<turnstile>s \<midarrow>In1l t\<succ>\<midarrow>n\<rightarrow> (w, s')";
    7.53 -val evaln_var_proc   = enf "evaln_var_eq"   "G\<turnstile>s \<midarrow>In2 t\<succ>\<midarrow>n\<rightarrow> (w, s')";
    7.54 -val evaln_exprs_proc = enf "evaln_exprs_eq" "G\<turnstile>s \<midarrow>In3 t\<succ>\<midarrow>n\<rightarrow> (w, s')";
    7.55 -val evaln_stmt_proc  = enf "evaln_stmt_eq"  "G\<turnstile>s \<midarrow>In1r t\<succ>\<midarrow>n\<rightarrow> (w, s')";
    7.56 -Addsimprocs [evaln_expr_proc,evaln_var_proc,evaln_exprs_proc,evaln_stmt_proc];
    7.57 +simproc_setup evaln_exprs ("G\<turnstile>s \<midarrow>In3 t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {*
    7.58 +  fn _ => fn _ => fn ct =>
    7.59 +    (case Thm.term_of ct of
    7.60 +      (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
    7.61 +    | _ => SOME (mk_meta_eq @{thm evaln_exprs_eq})) *}
    7.62  
    7.63 -bind_thms ("evaln_AbruptIs", sum3_instantiate (thm "evaln.Abrupt"))
    7.64 -*}
    7.65 +simproc_setup evaln_stmt ("G\<turnstile>s \<midarrow>In1r t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {*
    7.66 +  fn _ => fn _ => fn ct =>
    7.67 +    (case Thm.term_of ct of
    7.68 +      (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
    7.69 +    | _ => SOME (mk_meta_eq @{thm evaln_stmt_eq})) *}
    7.70 +
    7.71 +ML_setup {* bind_thms ("evaln_AbruptIs", sum3_instantiate @{thm evaln.Abrupt}) *}
    7.72  declare evaln_AbruptIs [intro!]
    7.73  
    7.74  lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
    7.75 @@ -352,16 +357,12 @@
    7.76  apply (frule evaln_abrupt_lemma, auto)+
    7.77  done
    7.78  
    7.79 -ML {*
    7.80 -local
    7.81 -  fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true
    7.82 -    | is_Some _ = false
    7.83 -  fun pred (_ $ _ $ _ $ _ $ _ $ _ $ x) = is_Some x
    7.84 -in
    7.85 -  val evaln_abrupt_proc = 
    7.86 - cond_simproc "evaln_abrupt" "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')" pred (thm "evaln_abrupt")
    7.87 -end;
    7.88 -Addsimprocs [evaln_abrupt_proc]
    7.89 +simproc_setup evaln_abrupt ("G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')") = {*
    7.90 +  fn _ => fn _ => fn ct =>
    7.91 +    (case Thm.term_of ct of
    7.92 +      (_ $ _ $ _ $ _ $ _ $ _ $ (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _))
    7.93 +        => NONE
    7.94 +    | _ => SOME (mk_meta_eq @{thm evaln_abrupt}))
    7.95  *}
    7.96  
    7.97  lemma evaln_LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<midarrow>n\<rightarrow> s"
    7.98 @@ -509,9 +510,7 @@
    7.99    show ?thesis .
   7.100  qed
   7.101  
   7.102 -ML {*
   7.103 -Delsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
   7.104 -*}
   7.105 +declare [[simproc del: wt_expr wt_var wt_exprs wt_stmt]]
   7.106  
   7.107  section {* eval implies evaln *}
   7.108  lemma eval_evaln: 
     8.1 --- a/src/HOL/Bali/Example.thy	Sat Jul 28 20:40:20 2007 +0200
     8.2 +++ b/src/HOL/Bali/Example.thy	Sat Jul 28 20:40:22 2007 +0200
     8.3 @@ -894,7 +894,7 @@
     8.4  
     8.5  declare member_is_static_simp [simp]
     8.6  declare wt.Skip [rule del] wt.Init [rule del]
     8.7 -ML {* bind_thms ("wt_intros",map (rewrite_rule [id_def]) (thms "wt.intros")) *}
     8.8 +ML_setup {* bind_thms ("wt_intros", map (rewrite_rule @{thms id_def}) @{thms wt.intros}) *}
     8.9  lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros
    8.10  lemmas daIs = assigned.select_convs da_Skip da_NewC da_Lit da_Super da.intros
    8.11  
    8.12 @@ -1192,10 +1192,10 @@
    8.13  declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp]
    8.14          Base_foo_defs  [simp]
    8.15  
    8.16 -ML {* bind_thms ("eval_intros", map 
    8.17 -        (simplify (simpset() delsimps [thm "Skip_eq"]
    8.18 -                             addsimps [thm "lvar_def"]) o 
    8.19 -         rewrite_rule [thm "assign_def",Let_def]) (thms "eval.intros")) *}
    8.20 +ML_setup {* bind_thms ("eval_intros", map 
    8.21 +        (simplify (simpset() delsimps @{thms Skip_eq}
    8.22 +                             addsimps @{thms lvar_def}) o 
    8.23 +         rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
    8.24  lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
    8.25  
    8.26  consts
     9.1 --- a/src/HOL/Bali/Term.thy	Sat Jul 28 20:40:20 2007 +0200
     9.2 +++ b/src/HOL/Bali/Term.thy	Sat Jul 28 20:40:22 2007 +0200
     9.3 @@ -266,9 +266,7 @@
     9.4    is_stmt :: "term \<Rightarrow> bool"
     9.5   "is_stmt t \<equiv> \<exists>c. t=In1r c"
     9.6  
     9.7 -ML {*
     9.8 -bind_thms ("is_stmt_rews", sum3_instantiate (thm "is_stmt_def"));
     9.9 -*}
    9.10 +ML_setup {* bind_thms ("is_stmt_rews", sum3_instantiate @{thm is_stmt_def}) *}
    9.11  
    9.12  declare is_stmt_rews [simp]
    9.13  
    10.1 --- a/src/HOL/Bali/TypeSafe.thy	Sat Jul 28 20:40:20 2007 +0200
    10.2 +++ b/src/HOL/Bali/TypeSafe.thy	Sat Jul 28 20:40:22 2007 +0200
    10.3 @@ -733,10 +733,9 @@
    10.4  declare split_paired_All [simp del] split_paired_Ex [simp del] 
    10.5  declare split_if     [split del] split_if_asm     [split del] 
    10.6          option.split [split del] option.split_asm [split del]
    10.7 -ML_setup {*
    10.8 -change_simpset (fn ss => ss delloop "split_all_tac");
    10.9 -change_claset (fn cs => cs delSWrapper "split_all_tac");
   10.10 -*}
   10.11 +declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
   10.12 +declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
   10.13 +
   10.14  lemma FVar_lemma: 
   10.15  "\<lbrakk>((v, f), Norm s2') = fvar statDeclC (static field) fn a (x2, s2); 
   10.16    G\<turnstile>statC\<preceq>\<^sub>C statDeclC;  
   10.17 @@ -763,10 +762,8 @@
   10.18  declare split_paired_All [simp] split_paired_Ex [simp] 
   10.19  declare split_if     [split] split_if_asm     [split] 
   10.20          option.split [split] option.split_asm [split]
   10.21 -ML_setup {*
   10.22 -change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
   10.23 -change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
   10.24 -*}
   10.25 +declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
   10.26 +declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
   10.27  
   10.28  
   10.29  lemma AVar_lemma1: "\<lbrakk>globs s (Inl a) = Some obj;tag obj=Arr ty i; 
   10.30 @@ -881,10 +878,9 @@
   10.31  declare split_paired_All [simp del] split_paired_Ex [simp del] 
   10.32  declare split_if     [split del] split_if_asm     [split del] 
   10.33          option.split [split del] option.split_asm [split del]
   10.34 -ML_setup {*
   10.35 -change_simpset (fn ss => ss delloop "split_all_tac");
   10.36 -change_claset (fn cs => cs delSWrapper "split_all_tac");
   10.37 -*}
   10.38 +declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
   10.39 +declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
   10.40 +
   10.41  lemma conforms_init_lvars: 
   10.42  "\<lbrakk>wf_mhead G (pid declC) sig (mhead (mthd dm)); wf_prog G;  
   10.43    list_all2 (conf G s) pvs pTsa; G\<turnstile>pTsa[\<preceq>](parTs sig);  
   10.44 @@ -935,10 +931,8 @@
   10.45  declare split_paired_All [simp] split_paired_Ex [simp] 
   10.46  declare split_if     [split] split_if_asm     [split] 
   10.47          option.split [split] option.split_asm [split]
   10.48 -ML_setup {*
   10.49 -change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
   10.50 -change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
   10.51 -*}
   10.52 +declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
   10.53 +declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
   10.54  
   10.55  
   10.56  subsection "accessibility"
    11.1 --- a/src/HOL/Bali/WellForm.thy	Sat Jul 28 20:40:20 2007 +0200
    11.2 +++ b/src/HOL/Bali/WellForm.thy	Sat Jul 28 20:40:22 2007 +0200
    11.3 @@ -1751,8 +1751,9 @@
    11.4  qed
    11.5   	      
    11.6  (* local lemma *)
    11.7 -ML {* bind_thm("bexI'",permute_prems 0 1 bexI) *}
    11.8 -ML {* bind_thm("ballE'",permute_prems 1 1 ballE) *}
    11.9 +lemma bexI': "x \<in> A \<Longrightarrow> P x \<Longrightarrow> \<exists>x\<in>A. P x" by blast
   11.10 +lemma ballE': "\<forall>x\<in>A. P x \<Longrightarrow> (x \<notin> A \<Longrightarrow> Q) \<Longrightarrow> (P x \<Longrightarrow> Q) \<Longrightarrow> Q" by blast
   11.11 +
   11.12  lemma subint_widen_imethds: 
   11.13   "\<lbrakk>G\<turnstile>I\<preceq>I J; wf_prog G; is_iface G J; jm \<in> imethds G J sig\<rbrakk> \<Longrightarrow>   
   11.14    \<exists> im \<in> imethds G I sig. is_static im = is_static jm \<and> 
   11.15 @@ -2175,10 +2176,9 @@
   11.16  qed
   11.17  
   11.18  declare split_paired_All [simp del] split_paired_Ex [simp del]
   11.19 -ML_setup {*
   11.20 -change_simpset (fn ss => ss delloop "split_all_tac");
   11.21 -change_claset (fn cs => cs delSWrapper "split_all_tac");
   11.22 -*}
   11.23 +declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
   11.24 +declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
   11.25 +
   11.26  lemma dynamic_mheadsD:   
   11.27  "\<lbrakk>emh \<in> mheads G S statT sig;    
   11.28    G,statT \<turnstile> dynC valid_lookup_cls_for (is_static emh);
   11.29 @@ -2306,10 +2306,8 @@
   11.30    qed
   11.31  qed
   11.32  declare split_paired_All [simp] split_paired_Ex [simp]
   11.33 -ML_setup {*
   11.34 -change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
   11.35 -change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
   11.36 -*}
   11.37 +declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
   11.38 +declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
   11.39  
   11.40  (* Tactical version *)
   11.41  (*
   11.42 @@ -2452,10 +2450,9 @@
   11.43    
   11.44  
   11.45  declare split_paired_All [simp del] split_paired_Ex [simp del]
   11.46 -ML_setup {*
   11.47 -change_simpset (fn ss => ss delloop "split_all_tac");
   11.48 -change_claset (fn cs => cs delSWrapper "split_all_tac");
   11.49 -*}
   11.50 +declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
   11.51 +declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
   11.52 +
   11.53  lemma wt_is_type: "E,dt\<Turnstile>v\<Colon>T \<Longrightarrow>  wf_prog (prg E) \<longrightarrow> 
   11.54    dt=empty_dt \<longrightarrow> (case T of 
   11.55                       Inl T \<Rightarrow> is_type (prg E) T 
   11.56 @@ -2478,10 +2475,8 @@
   11.57      )
   11.58  done
   11.59  declare split_paired_All [simp] split_paired_Ex [simp]
   11.60 -ML_setup {*
   11.61 -change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
   11.62 -change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
   11.63 -*}
   11.64 +declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
   11.65 +declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
   11.66  
   11.67  lemma ty_expr_is_type: 
   11.68  "\<lbrakk>E\<turnstile>e\<Colon>-T; wf_prog (prg E)\<rbrakk> \<Longrightarrow> is_type (prg E) T"
    12.1 --- a/src/HOL/Bali/WellType.thy	Sat Jul 28 20:40:20 2007 +0200
    12.2 +++ b/src/HOL/Bali/WellType.thy	Sat Jul 28 20:40:22 2007 +0200
    12.3 @@ -452,9 +452,7 @@
    12.4  declare not_None_eq [simp del] 
    12.5  declare split_if [split del] split_if_asm [split del]
    12.6  declare split_paired_All [simp del] split_paired_Ex [simp del]
    12.7 -ML_setup {*
    12.8 -change_simpset (fn ss => ss delloop "split_all_tac")
    12.9 -*}
   12.10 +declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
   12.11  
   12.12  inductive_cases wt_elim_cases [cases set]:
   12.13  	"E,dt\<Turnstile>In2  (LVar vn)               \<Colon>T"
   12.14 @@ -490,9 +488,7 @@
   12.15  declare not_None_eq [simp] 
   12.16  declare split_if [split] split_if_asm [split]
   12.17  declare split_paired_All [simp] split_paired_Ex [simp]
   12.18 -ML_setup {*
   12.19 -change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
   12.20 -*}
   12.21 +declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
   12.22  
   12.23  lemma is_acc_class_is_accessible: 
   12.24    "is_acc_class G P C \<Longrightarrow> G\<turnstile>(Class C) accessible_in P"
   12.25 @@ -606,25 +602,29 @@
   12.26  lemma wt_stmt_eq: "E,dt\<Turnstile>In1r t\<Colon>U = (U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>)"
   12.27    by (auto, frule wt_Inj_elim, auto, frule wt_Inj_elim, auto)
   12.28  
   12.29 -ML {*
   12.30 -fun wt_fun name lhs =
   12.31 -let
   12.32 -  fun is_Inj (Const (inj,_) $ _) = true
   12.33 -    | is_Inj _                   = false
   12.34 -  fun pred (_ $ _ $ _ $ _ $ x) = is_Inj x
   12.35 -in
   12.36 -  cond_simproc name lhs pred (thm name)
   12.37 -end
   12.38 +simproc_setup wt_expr ("E,dt\<Turnstile>In1l t\<Colon>U") = {*
   12.39 +  fn _ => fn _ => fn ct =>
   12.40 +    (case Thm.term_of ct of
   12.41 +      (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
   12.42 +    | _ => SOME (mk_meta_eq @{thm wt_expr_eq})) *}
   12.43 +
   12.44 +simproc_setup wt_var ("E,dt\<Turnstile>In2 t\<Colon>U") = {*
   12.45 +  fn _ => fn _ => fn ct =>
   12.46 +    (case Thm.term_of ct of
   12.47 +      (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
   12.48 +    | _ => SOME (mk_meta_eq @{thm wt_var_eq})) *}
   12.49  
   12.50 -val wt_expr_proc  = wt_fun "wt_expr_eq"  "E,dt\<Turnstile>In1l t\<Colon>U";
   12.51 -val wt_var_proc   = wt_fun "wt_var_eq"   "E,dt\<Turnstile>In2 t\<Colon>U";
   12.52 -val wt_exprs_proc = wt_fun "wt_exprs_eq" "E,dt\<Turnstile>In3 t\<Colon>U";
   12.53 -val wt_stmt_proc  = wt_fun "wt_stmt_eq"  "E,dt\<Turnstile>In1r t\<Colon>U";
   12.54 -*}
   12.55 +simproc_setup wt_exprs ("E,dt\<Turnstile>In3 t\<Colon>U") = {*
   12.56 +  fn _ => fn _ => fn ct =>
   12.57 +    (case Thm.term_of ct of
   12.58 +      (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
   12.59 +    | _ => SOME (mk_meta_eq @{thm wt_exprs_eq})) *}
   12.60  
   12.61 -ML {*
   12.62 -Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
   12.63 -*}
   12.64 +simproc_setup wt_stmt ("E,dt\<Turnstile>In1r t\<Colon>U") = {*
   12.65 +  fn _ => fn _ => fn ct =>
   12.66 +    (case Thm.term_of ct of
   12.67 +      (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
   12.68 +    | _ => SOME (mk_meta_eq @{thm wt_stmt_eq})) *}
   12.69  
   12.70  lemma wt_elim_BinOp:
   12.71    "\<lbrakk>E,dt\<Turnstile>In1l (BinOp binop e1 e2)\<Colon>T;