--- a/src/HOL/Bali/AxSem.thy Sat Jul 28 20:40:20 2007 +0200
+++ b/src/HOL/Bali/AxSem.thy Sat Jul 28 20:40:22 2007 +0200
@@ -471,10 +471,8 @@
declare split_paired_All [simp del] split_paired_Ex [simp del]
declare split_if [split del] split_if_asm [split del]
option.split [split del] option.split_asm [split del]
-ML_setup {*
-change_simpset (fn ss => ss delloop "split_all_tac");
-change_claset (fn cs => cs delSWrapper "split_all_tac");
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
+declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
inductive
ax_derivs :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool" ("_,_|\<turnstile>_" [61,58,58] 57)
@@ -1015,9 +1013,7 @@
apply (auto simp add: type_ok_def)
done
-ML {*
-bind_thms ("ax_Abrupts", sum3_instantiate (thm "ax_derivs.Abrupt"))
-*}
+ML_setup {* bind_thms ("ax_Abrupts", sum3_instantiate @{thm ax_derivs.Abrupt}) *}
declare ax_Abrupts [intro!]
lemmas ax_Normal_cases = ax_cases [of _ _ _ normal]
--- a/src/HOL/Bali/AxSound.thy Sat Jul 28 20:40:20 2007 +0200
+++ b/src/HOL/Bali/AxSound.thy Sat Jul 28 20:40:22 2007 +0200
@@ -210,9 +210,7 @@
done
-
-
-ML "Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]"
+declare [[simproc add: wt_expr wt_var wt_exprs wt_stmt]]
lemma valid_stmtI:
assumes I: "\<And> n s0 L accC C s1 Y Z.
--- a/src/HOL/Bali/Basis.thy Sat Jul 28 20:40:20 2007 +0200
+++ b/src/HOL/Bali/Basis.thy Sat Jul 28 20:40:22 2007 +0200
@@ -11,22 +11,13 @@
Unify.search_bound := 40;
Unify.trace_bound := 40;
*}
-(*print_depth 100;*)
-(*Syntax.ambiguity_level := 1;*)
section "misc"
declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *)
-ML {*
-fun cond_simproc name pat pred thm = Simplifier.simproc (Thm.theory_of_thm thm) name [pat]
- (fn _ => fn _ => fn t => if pred t then NONE else SOME (mk_meta_eq thm));
-*}
-
declare split_if_asm [split] option.split [split] option.split_asm [split]
-ML {*
-change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
declare if_weak_cong [cong del] option.weak_case_cong [cong del]
declare length_Suc_conv [iff]
--- a/src/HOL/Bali/DefiniteAssignment.thy Sat Jul 28 20:40:20 2007 +0200
+++ b/src/HOL/Bali/DefiniteAssignment.thy Sat Jul 28 20:40:22 2007 +0200
@@ -820,9 +820,8 @@
declare inj_term_sym_simps [simp]
declare assigns_if.simps [simp del]
declare split_paired_All [simp del] split_paired_Ex [simp del]
-ML_setup {*
-change_simpset (fn ss => ss delloop "split_all_tac");
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
+
inductive_cases da_elim_cases [cases set]:
"Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A"
"Env\<turnstile> B \<guillemotright>In1r Skip\<guillemotright> A"
@@ -887,9 +886,8 @@
declare inj_term_sym_simps [simp del]
declare assigns_if.simps [simp]
declare split_paired_All [simp] split_paired_Ex [simp]
-ML_setup {*
-change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
+
(* To be able to eliminate both the versions with the overloaded brackets:
(B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A) and with the explicit constructor (B \<guillemotright>In1r Skip\<guillemotright> A),
every rule appears in both versions
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy Sat Jul 28 20:40:20 2007 +0200
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy Sat Jul 28 20:40:22 2007 +0200
@@ -4,9 +4,7 @@
theory DefiniteAssignmentCorrect imports WellForm Eval begin
-ML {*
-Delsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
-*}
+declare [[simproc del: wt_expr wt_var wt_exprs wt_stmt]]
lemma sxalloc_no_jump:
assumes sxalloc: "G\<turnstile>s0 \<midarrow>sxalloc\<rightarrow> s1" and
@@ -4496,7 +4494,6 @@
using that by (rule da_good_approxE) iprover+
qed
-ML {*
-Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
-*}
+declare [[simproc add: wt_expr wt_var wt_exprs wt_stmt]]
+
end
--- a/src/HOL/Bali/Eval.thy Sat Jul 28 20:40:20 2007 +0200
+++ b/src/HOL/Bali/Eval.thy Sat Jul 28 20:40:22 2007 +0200
@@ -749,12 +749,12 @@
29(AVar),24(Call)]
*)
-ML {*
+ML_setup {*
bind_thm ("eval_induct_", rearrange_prems
[0,1,2,8,4,30,31,27,15,16,
17,18,19,20,21,3,5,25,26,23,6,
7,11,9,13,14,12,22,10,28,
- 29,24] (thm "eval.induct"))
+ 29,24] @{thm eval.induct})
*}
@@ -790,9 +790,8 @@
declare not_None_eq [simp del] (* IntDef.Zero_def [simp del] *)
declare split_paired_All [simp del] split_paired_Ex [simp del]
-ML_setup {*
-change_simpset (fn ss => ss delloop "split_all_tac");
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
+
inductive_cases eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v, s')"
inductive_cases eval_elim_cases [cases set]:
@@ -829,9 +828,7 @@
"G\<turnstile>Norm s \<midarrow>In1r (Init C) \<succ>\<rightarrow> (x, s')"
declare not_None_eq [simp] (* IntDef.Zero_def [simp] *)
declare split_paired_All [simp] split_paired_Ex [simp]
-ML_setup {*
-change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
declare split_if [split] split_if_asm [split]
option.split [split] option.split_asm [split]
@@ -869,25 +866,35 @@
lemma eval_stmt_eq: "G\<turnstile>s \<midarrow>In1r t\<succ>\<rightarrow> (w, s') = (w=\<diamondsuit> \<and> G\<turnstile>s \<midarrow>t \<rightarrow> s')"
by (auto, frule eval_Inj_elim, auto, frule eval_Inj_elim, auto)
+simproc_setup eval_expr ("G\<turnstile>s \<midarrow>In1l t\<succ>\<rightarrow> (w, s')") = {*
+ fn _ => fn _ => fn ct =>
+ (case Thm.term_of ct of
+ (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
+ | _ => SOME (mk_meta_eq @{thm eval_expr_eq})) *}
+
+simproc_setup eval_var ("G\<turnstile>s \<midarrow>In2 t\<succ>\<rightarrow> (w, s')") = {*
+ fn _ => fn _ => fn ct =>
+ (case Thm.term_of ct of
+ (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
+ | _ => SOME (mk_meta_eq @{thm eval_var_eq})) *}
+
+simproc_setup eval_exprs ("G\<turnstile>s \<midarrow>In3 t\<succ>\<rightarrow> (w, s')") = {*
+ fn _ => fn _ => fn ct =>
+ (case Thm.term_of ct of
+ (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
+ | _ => SOME (mk_meta_eq @{thm eval_exprs_eq})) *}
+
+simproc_setup eval_stmt ("G\<turnstile>s \<midarrow>In1r t\<succ>\<rightarrow> (w, s')") = {*
+ fn _ => fn _ => fn ct =>
+ (case Thm.term_of ct of
+ (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
+ | _ => SOME (mk_meta_eq @{thm eval_stmt_eq})) *}
+
ML_setup {*
-fun eval_fun name lhs =
-let
- fun is_Inj (Const (inj,_) $ _) = true
- | is_Inj _ = false
- fun pred (_ $ _ $ _ $ _ $ x $ _) = is_Inj x
-in
- cond_simproc name lhs pred (thm name)
-end
-
-val eval_expr_proc = eval_fun "eval_expr_eq" "G\<turnstile>s \<midarrow>In1l t\<succ>\<rightarrow> (w, s')";
-val eval_var_proc = eval_fun "eval_var_eq" "G\<turnstile>s \<midarrow>In2 t\<succ>\<rightarrow> (w, s')";
-val eval_exprs_proc = eval_fun "eval_exprs_eq" "G\<turnstile>s \<midarrow>In3 t\<succ>\<rightarrow> (w, s')";
-val eval_stmt_proc = eval_fun "eval_stmt_eq" "G\<turnstile>s \<midarrow>In1r t\<succ>\<rightarrow> (w, s')";
-Addsimprocs [eval_expr_proc,eval_var_proc,eval_exprs_proc,eval_stmt_proc];
-bind_thms ("AbruptIs", sum3_instantiate (thm "eval.Abrupt"))
+bind_thms ("AbruptIs", sum3_instantiate @{thm eval.Abrupt})
*}
-declare halloc.Abrupt [intro!] eval.Abrupt [intro!] AbruptIs [intro!]
+declare halloc.Abrupt [intro!] eval.Abrupt [intro!] AbruptIs [intro!]
text{* @{text Callee},@{text InsInitE}, @{text InsInitV}, @{text FinA} are only
used in smallstep semantics, not in the bigstep semantics. So their is no
@@ -955,17 +962,11 @@
apply (frule eval_no_abrupt_lemma, auto)+
done
-ML {*
-local
- fun is_None (Const ("Datatype.option.None",_)) = true
- | is_None _ = false
- fun pred (_ $ _ $ (Const ("Pair", _) $ x $ _) $ _ $ _ $ _) = is_None x
-in
- val eval_no_abrupt_proc =
- cond_simproc "eval_no_abrupt" "G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')" pred
- (thm "eval_no_abrupt")
-end;
-Addsimprocs [eval_no_abrupt_proc]
+simproc_setup eval_no_abrupt ("G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')") = {*
+ fn _ => fn _ => fn ct =>
+ (case Thm.term_of ct of
+ (_ $ _ $ (Const ("Pair", _) $ (Const ("Datatype.option.None",_)) $ _) $ _ $ _ $ _) => NONE
+ | _ => SOME (mk_meta_eq @{thm eval_no_abrupt}))
*}
@@ -981,17 +982,11 @@
apply (frule eval_abrupt_lemma, auto)+
done
-ML {*
-local
- fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true
- | is_Some _ = false
- fun pred (_ $ _ $ _ $ _ $ _ $ x) = is_Some x
-in
- val eval_abrupt_proc =
- cond_simproc "eval_abrupt"
- "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')" pred (thm "eval_abrupt")
-end;
-Addsimprocs [eval_abrupt_proc]
+simproc_setup eval_abrupt ("G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')") = {*
+ fn _ => fn _ => fn ct =>
+ (case Thm.term_of ct of
+ (_ $ _ $ _ $ _ $ _ $ (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _)) => NONE
+ | _ => SOME (mk_meta_eq @{thm eval_abrupt}))
*}
--- a/src/HOL/Bali/Evaln.thy Sat Jul 28 20:40:20 2007 +0200
+++ b/src/HOL/Bali/Evaln.thy Sat Jul 28 20:40:22 2007 +0200
@@ -198,9 +198,8 @@
option.split [split del] option.split_asm [split del]
not_None_eq [simp del]
split_paired_All [simp del] split_paired_Ex [simp del]
-ML_setup {*
-change_simpset (fn ss => ss delloop "split_all_tac");
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
+
inductive_cases evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s')"
inductive_cases evaln_elim_cases:
@@ -241,9 +240,8 @@
option.split [split] option.split_asm [split]
not_None_eq [simp]
split_paired_All [simp] split_paired_Ex [simp]
-ML_setup {*
-change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
+
lemma evaln_Inj_elim: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s') \<Longrightarrow> case t of In1 ec \<Rightarrow>
(case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v) | Inr c \<Rightarrow> w = \<diamondsuit>)
| In2 e \<Rightarrow> (\<exists>v. w = In2 v) | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
@@ -272,24 +270,31 @@
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')"
by (auto, frule evaln_Inj_elim, auto, frule evaln_Inj_elim, auto)
-ML_setup {*
-fun enf name lhs =
-let
- fun is_Inj (Const (inj,_) $ _) = true
- | is_Inj _ = false
- fun pred (_ $ _ $ _ $ _ $ _ $ x $ _) = is_Inj x
-in
- cond_simproc name lhs pred (thm name)
-end;
+simproc_setup evaln_expr ("G\<turnstile>s \<midarrow>In1l t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {*
+ fn _ => fn _ => fn ct =>
+ (case Thm.term_of ct of
+ (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
+ | _ => SOME (mk_meta_eq @{thm evaln_expr_eq})) *}
+
+simproc_setup evaln_var ("G\<turnstile>s \<midarrow>In2 t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {*
+ fn _ => fn _ => fn ct =>
+ (case Thm.term_of ct of
+ (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
+ | _ => SOME (mk_meta_eq @{thm evaln_var_eq})) *}
-val evaln_expr_proc = enf "evaln_expr_eq" "G\<turnstile>s \<midarrow>In1l t\<succ>\<midarrow>n\<rightarrow> (w, s')";
-val evaln_var_proc = enf "evaln_var_eq" "G\<turnstile>s \<midarrow>In2 t\<succ>\<midarrow>n\<rightarrow> (w, s')";
-val evaln_exprs_proc = enf "evaln_exprs_eq" "G\<turnstile>s \<midarrow>In3 t\<succ>\<midarrow>n\<rightarrow> (w, s')";
-val evaln_stmt_proc = enf "evaln_stmt_eq" "G\<turnstile>s \<midarrow>In1r t\<succ>\<midarrow>n\<rightarrow> (w, s')";
-Addsimprocs [evaln_expr_proc,evaln_var_proc,evaln_exprs_proc,evaln_stmt_proc];
+simproc_setup evaln_exprs ("G\<turnstile>s \<midarrow>In3 t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {*
+ fn _ => fn _ => fn ct =>
+ (case Thm.term_of ct of
+ (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
+ | _ => SOME (mk_meta_eq @{thm evaln_exprs_eq})) *}
-bind_thms ("evaln_AbruptIs", sum3_instantiate (thm "evaln.Abrupt"))
-*}
+simproc_setup evaln_stmt ("G\<turnstile>s \<midarrow>In1r t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {*
+ fn _ => fn _ => fn ct =>
+ (case Thm.term_of ct of
+ (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
+ | _ => SOME (mk_meta_eq @{thm evaln_stmt_eq})) *}
+
+ML_setup {* bind_thms ("evaln_AbruptIs", sum3_instantiate @{thm evaln.Abrupt}) *}
declare evaln_AbruptIs [intro!]
lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
@@ -352,16 +357,12 @@
apply (frule evaln_abrupt_lemma, auto)+
done
-ML {*
-local
- fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true
- | is_Some _ = false
- fun pred (_ $ _ $ _ $ _ $ _ $ _ $ x) = is_Some x
-in
- val evaln_abrupt_proc =
- cond_simproc "evaln_abrupt" "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')" pred (thm "evaln_abrupt")
-end;
-Addsimprocs [evaln_abrupt_proc]
+simproc_setup evaln_abrupt ("G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')") = {*
+ fn _ => fn _ => fn ct =>
+ (case Thm.term_of ct of
+ (_ $ _ $ _ $ _ $ _ $ _ $ (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _))
+ => NONE
+ | _ => SOME (mk_meta_eq @{thm evaln_abrupt}))
*}
lemma evaln_LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<midarrow>n\<rightarrow> s"
@@ -509,9 +510,7 @@
show ?thesis .
qed
-ML {*
-Delsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
-*}
+declare [[simproc del: wt_expr wt_var wt_exprs wt_stmt]]
section {* eval implies evaln *}
lemma eval_evaln:
--- a/src/HOL/Bali/Example.thy Sat Jul 28 20:40:20 2007 +0200
+++ b/src/HOL/Bali/Example.thy Sat Jul 28 20:40:22 2007 +0200
@@ -894,7 +894,7 @@
declare member_is_static_simp [simp]
declare wt.Skip [rule del] wt.Init [rule del]
-ML {* bind_thms ("wt_intros",map (rewrite_rule [id_def]) (thms "wt.intros")) *}
+ML_setup {* bind_thms ("wt_intros", map (rewrite_rule @{thms id_def}) @{thms wt.intros}) *}
lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros
lemmas daIs = assigned.select_convs da_Skip da_NewC da_Lit da_Super da.intros
@@ -1192,10 +1192,10 @@
declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp]
Base_foo_defs [simp]
-ML {* bind_thms ("eval_intros", map
- (simplify (simpset() delsimps [thm "Skip_eq"]
- addsimps [thm "lvar_def"]) o
- rewrite_rule [thm "assign_def",Let_def]) (thms "eval.intros")) *}
+ML_setup {* bind_thms ("eval_intros", map
+ (simplify (simpset() delsimps @{thms Skip_eq}
+ addsimps @{thms lvar_def}) o
+ rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
consts
--- a/src/HOL/Bali/Term.thy Sat Jul 28 20:40:20 2007 +0200
+++ b/src/HOL/Bali/Term.thy Sat Jul 28 20:40:22 2007 +0200
@@ -266,9 +266,7 @@
is_stmt :: "term \<Rightarrow> bool"
"is_stmt t \<equiv> \<exists>c. t=In1r c"
-ML {*
-bind_thms ("is_stmt_rews", sum3_instantiate (thm "is_stmt_def"));
-*}
+ML_setup {* bind_thms ("is_stmt_rews", sum3_instantiate @{thm is_stmt_def}) *}
declare is_stmt_rews [simp]
--- a/src/HOL/Bali/TypeSafe.thy Sat Jul 28 20:40:20 2007 +0200
+++ b/src/HOL/Bali/TypeSafe.thy Sat Jul 28 20:40:22 2007 +0200
@@ -733,10 +733,9 @@
declare split_paired_All [simp del] split_paired_Ex [simp del]
declare split_if [split del] split_if_asm [split del]
option.split [split del] option.split_asm [split del]
-ML_setup {*
-change_simpset (fn ss => ss delloop "split_all_tac");
-change_claset (fn cs => cs delSWrapper "split_all_tac");
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
+declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
+
lemma FVar_lemma:
"\<lbrakk>((v, f), Norm s2') = fvar statDeclC (static field) fn a (x2, s2);
G\<turnstile>statC\<preceq>\<^sub>C statDeclC;
@@ -763,10 +762,8 @@
declare split_paired_All [simp] split_paired_Ex [simp]
declare split_if [split] split_if_asm [split]
option.split [split] option.split_asm [split]
-ML_setup {*
-change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
-change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
-*}
+declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
+declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
lemma AVar_lemma1: "\<lbrakk>globs s (Inl a) = Some obj;tag obj=Arr ty i;
@@ -881,10 +878,9 @@
declare split_paired_All [simp del] split_paired_Ex [simp del]
declare split_if [split del] split_if_asm [split del]
option.split [split del] option.split_asm [split del]
-ML_setup {*
-change_simpset (fn ss => ss delloop "split_all_tac");
-change_claset (fn cs => cs delSWrapper "split_all_tac");
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
+declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
+
lemma conforms_init_lvars:
"\<lbrakk>wf_mhead G (pid declC) sig (mhead (mthd dm)); wf_prog G;
list_all2 (conf G s) pvs pTsa; G\<turnstile>pTsa[\<preceq>](parTs sig);
@@ -935,10 +931,8 @@
declare split_paired_All [simp] split_paired_Ex [simp]
declare split_if [split] split_if_asm [split]
option.split [split] option.split_asm [split]
-ML_setup {*
-change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
-change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
-*}
+declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
+declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
subsection "accessibility"
--- a/src/HOL/Bali/WellForm.thy Sat Jul 28 20:40:20 2007 +0200
+++ b/src/HOL/Bali/WellForm.thy Sat Jul 28 20:40:22 2007 +0200
@@ -1751,8 +1751,9 @@
qed
(* local lemma *)
-ML {* bind_thm("bexI'",permute_prems 0 1 bexI) *}
-ML {* bind_thm("ballE'",permute_prems 1 1 ballE) *}
+lemma bexI': "x \<in> A \<Longrightarrow> P x \<Longrightarrow> \<exists>x\<in>A. P x" by blast
+lemma ballE': "\<forall>x\<in>A. P x \<Longrightarrow> (x \<notin> A \<Longrightarrow> Q) \<Longrightarrow> (P x \<Longrightarrow> Q) \<Longrightarrow> Q" by blast
+
lemma subint_widen_imethds:
"\<lbrakk>G\<turnstile>I\<preceq>I J; wf_prog G; is_iface G J; jm \<in> imethds G J sig\<rbrakk> \<Longrightarrow>
\<exists> im \<in> imethds G I sig. is_static im = is_static jm \<and>
@@ -2175,10 +2176,9 @@
qed
declare split_paired_All [simp del] split_paired_Ex [simp del]
-ML_setup {*
-change_simpset (fn ss => ss delloop "split_all_tac");
-change_claset (fn cs => cs delSWrapper "split_all_tac");
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
+declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
+
lemma dynamic_mheadsD:
"\<lbrakk>emh \<in> mheads G S statT sig;
G,statT \<turnstile> dynC valid_lookup_cls_for (is_static emh);
@@ -2306,10 +2306,8 @@
qed
qed
declare split_paired_All [simp] split_paired_Ex [simp]
-ML_setup {*
-change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
-change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
-*}
+declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
+declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
(* Tactical version *)
(*
@@ -2452,10 +2450,9 @@
declare split_paired_All [simp del] split_paired_Ex [simp del]
-ML_setup {*
-change_simpset (fn ss => ss delloop "split_all_tac");
-change_claset (fn cs => cs delSWrapper "split_all_tac");
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
+declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
+
lemma wt_is_type: "E,dt\<Turnstile>v\<Colon>T \<Longrightarrow> wf_prog (prg E) \<longrightarrow>
dt=empty_dt \<longrightarrow> (case T of
Inl T \<Rightarrow> is_type (prg E) T
@@ -2478,10 +2475,8 @@
)
done
declare split_paired_All [simp] split_paired_Ex [simp]
-ML_setup {*
-change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
-change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
-*}
+declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
+declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
lemma ty_expr_is_type:
"\<lbrakk>E\<turnstile>e\<Colon>-T; wf_prog (prg E)\<rbrakk> \<Longrightarrow> is_type (prg E) T"
--- a/src/HOL/Bali/WellType.thy Sat Jul 28 20:40:20 2007 +0200
+++ b/src/HOL/Bali/WellType.thy Sat Jul 28 20:40:22 2007 +0200
@@ -452,9 +452,7 @@
declare not_None_eq [simp del]
declare split_if [split del] split_if_asm [split del]
declare split_paired_All [simp del] split_paired_Ex [simp del]
-ML_setup {*
-change_simpset (fn ss => ss delloop "split_all_tac")
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
inductive_cases wt_elim_cases [cases set]:
"E,dt\<Turnstile>In2 (LVar vn) \<Colon>T"
@@ -490,9 +488,7 @@
declare not_None_eq [simp]
declare split_if [split] split_if_asm [split]
declare split_paired_All [simp] split_paired_Ex [simp]
-ML_setup {*
-change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
lemma is_acc_class_is_accessible:
"is_acc_class G P C \<Longrightarrow> G\<turnstile>(Class C) accessible_in P"
@@ -606,25 +602,29 @@
lemma wt_stmt_eq: "E,dt\<Turnstile>In1r t\<Colon>U = (U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>)"
by (auto, frule wt_Inj_elim, auto, frule wt_Inj_elim, auto)
-ML {*
-fun wt_fun name lhs =
-let
- fun is_Inj (Const (inj,_) $ _) = true
- | is_Inj _ = false
- fun pred (_ $ _ $ _ $ _ $ x) = is_Inj x
-in
- cond_simproc name lhs pred (thm name)
-end
+simproc_setup wt_expr ("E,dt\<Turnstile>In1l t\<Colon>U") = {*
+ fn _ => fn _ => fn ct =>
+ (case Thm.term_of ct of
+ (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
+ | _ => SOME (mk_meta_eq @{thm wt_expr_eq})) *}
+
+simproc_setup wt_var ("E,dt\<Turnstile>In2 t\<Colon>U") = {*
+ fn _ => fn _ => fn ct =>
+ (case Thm.term_of ct of
+ (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
+ | _ => SOME (mk_meta_eq @{thm wt_var_eq})) *}
-val wt_expr_proc = wt_fun "wt_expr_eq" "E,dt\<Turnstile>In1l t\<Colon>U";
-val wt_var_proc = wt_fun "wt_var_eq" "E,dt\<Turnstile>In2 t\<Colon>U";
-val wt_exprs_proc = wt_fun "wt_exprs_eq" "E,dt\<Turnstile>In3 t\<Colon>U";
-val wt_stmt_proc = wt_fun "wt_stmt_eq" "E,dt\<Turnstile>In1r t\<Colon>U";
-*}
+simproc_setup wt_exprs ("E,dt\<Turnstile>In3 t\<Colon>U") = {*
+ fn _ => fn _ => fn ct =>
+ (case Thm.term_of ct of
+ (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
+ | _ => SOME (mk_meta_eq @{thm wt_exprs_eq})) *}
-ML {*
-Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
-*}
+simproc_setup wt_stmt ("E,dt\<Turnstile>In1r t\<Colon>U") = {*
+ fn _ => fn _ => fn ct =>
+ (case Thm.term_of ct of
+ (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
+ | _ => SOME (mk_meta_eq @{thm wt_stmt_eq})) *}
lemma wt_elim_BinOp:
"\<lbrakk>E,dt\<Turnstile>In1l (BinOp binop e1 e2)\<Colon>T;