src/HOL/Bali/WellType.thy
changeset 24019 67bde7cfcf10
parent 23747 b07cff284683
child 24783 5a3e336a2e37
     1.1 --- a/src/HOL/Bali/WellType.thy	Sat Jul 28 20:40:20 2007 +0200
     1.2 +++ b/src/HOL/Bali/WellType.thy	Sat Jul 28 20:40:22 2007 +0200
     1.3 @@ -452,9 +452,7 @@
     1.4  declare not_None_eq [simp del] 
     1.5  declare split_if [split del] split_if_asm [split del]
     1.6  declare split_paired_All [simp del] split_paired_Ex [simp del]
     1.7 -ML_setup {*
     1.8 -change_simpset (fn ss => ss delloop "split_all_tac")
     1.9 -*}
    1.10 +declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
    1.11  
    1.12  inductive_cases wt_elim_cases [cases set]:
    1.13  	"E,dt\<Turnstile>In2  (LVar vn)               \<Colon>T"
    1.14 @@ -490,9 +488,7 @@
    1.15  declare not_None_eq [simp] 
    1.16  declare split_if [split] split_if_asm [split]
    1.17  declare split_paired_All [simp] split_paired_Ex [simp]
    1.18 -ML_setup {*
    1.19 -change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
    1.20 -*}
    1.21 +declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
    1.22  
    1.23  lemma is_acc_class_is_accessible: 
    1.24    "is_acc_class G P C \<Longrightarrow> G\<turnstile>(Class C) accessible_in P"
    1.25 @@ -606,25 +602,29 @@
    1.26  lemma wt_stmt_eq: "E,dt\<Turnstile>In1r t\<Colon>U = (U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>)"
    1.27    by (auto, frule wt_Inj_elim, auto, frule wt_Inj_elim, auto)
    1.28  
    1.29 -ML {*
    1.30 -fun wt_fun name lhs =
    1.31 -let
    1.32 -  fun is_Inj (Const (inj,_) $ _) = true
    1.33 -    | is_Inj _                   = false
    1.34 -  fun pred (_ $ _ $ _ $ _ $ x) = is_Inj x
    1.35 -in
    1.36 -  cond_simproc name lhs pred (thm name)
    1.37 -end
    1.38 +simproc_setup wt_expr ("E,dt\<Turnstile>In1l t\<Colon>U") = {*
    1.39 +  fn _ => fn _ => fn ct =>
    1.40 +    (case Thm.term_of ct of
    1.41 +      (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
    1.42 +    | _ => SOME (mk_meta_eq @{thm wt_expr_eq})) *}
    1.43 +
    1.44 +simproc_setup wt_var ("E,dt\<Turnstile>In2 t\<Colon>U") = {*
    1.45 +  fn _ => fn _ => fn ct =>
    1.46 +    (case Thm.term_of ct of
    1.47 +      (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
    1.48 +    | _ => SOME (mk_meta_eq @{thm wt_var_eq})) *}
    1.49  
    1.50 -val wt_expr_proc  = wt_fun "wt_expr_eq"  "E,dt\<Turnstile>In1l t\<Colon>U";
    1.51 -val wt_var_proc   = wt_fun "wt_var_eq"   "E,dt\<Turnstile>In2 t\<Colon>U";
    1.52 -val wt_exprs_proc = wt_fun "wt_exprs_eq" "E,dt\<Turnstile>In3 t\<Colon>U";
    1.53 -val wt_stmt_proc  = wt_fun "wt_stmt_eq"  "E,dt\<Turnstile>In1r t\<Colon>U";
    1.54 -*}
    1.55 +simproc_setup wt_exprs ("E,dt\<Turnstile>In3 t\<Colon>U") = {*
    1.56 +  fn _ => fn _ => fn ct =>
    1.57 +    (case Thm.term_of ct of
    1.58 +      (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
    1.59 +    | _ => SOME (mk_meta_eq @{thm wt_exprs_eq})) *}
    1.60  
    1.61 -ML {*
    1.62 -Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
    1.63 -*}
    1.64 +simproc_setup wt_stmt ("E,dt\<Turnstile>In1r t\<Colon>U") = {*
    1.65 +  fn _ => fn _ => fn ct =>
    1.66 +    (case Thm.term_of ct of
    1.67 +      (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
    1.68 +    | _ => SOME (mk_meta_eq @{thm wt_stmt_eq})) *}
    1.69  
    1.70  lemma wt_elim_BinOp:
    1.71    "\<lbrakk>E,dt\<Turnstile>In1l (BinOp binop e1 e2)\<Colon>T;