tuned
authorhaftmann
Wed Apr 11 08:28:14 2007 +0200 (2007-04-11)
changeset 22633a47e4fd7ebc1
parent 22632 59c117a0bcf3
child 22634 399e4b4835da
tuned
src/HOL/Bali/Basis.thy
src/HOL/List.thy
src/HOL/MicroJava/J/WellForm.thy
     1.1 --- a/src/HOL/Bali/Basis.thy	Wed Apr 11 08:28:13 2007 +0200
     1.2 +++ b/src/HOL/Bali/Basis.thy	Wed Apr 11 08:28:14 2007 +0200
     1.3 @@ -246,7 +246,7 @@
     1.4     "the_In1r" == "the_Inr \<circ> the_In1"
     1.5  
     1.6  ML {*
     1.7 -fun sum3_instantiate thm = map (fn s => simplify(simpset()delsimps[not_None_eq])
     1.8 +fun sum3_instantiate thm = map (fn s => simplify(simpset()delsimps[@{thm not_None_eq}])
     1.9   (read_instantiate [("t","In"^s^" ?x")] thm)) ["1l","2","3","1r"]
    1.10  *}
    1.11  (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
     2.1 --- a/src/HOL/List.thy	Wed Apr 11 08:28:13 2007 +0200
     2.2 +++ b/src/HOL/List.thy	Wed Apr 11 08:28:14 2007 +0200
     2.3 @@ -299,8 +299,6 @@
     2.4  ML_setup {*
     2.5  local
     2.6  
     2.7 -val neq_if_length_neq = thm "neq_if_length_neq";
     2.8 -
     2.9  fun len (Const("List.list.Nil",_)) acc = acc
    2.10    | len (Const("List.list.Cons",_) $ _ $ xs) (ts,n) = len xs (ts,n+1)
    2.11    | len (Const("List.op @",_) $ xs $ ys) acc = len xs (len ys acc)
    2.12 @@ -308,8 +306,6 @@
    2.13    | len (Const("List.map",_) $ _ $ xs) acc = len xs acc
    2.14    | len t (ts,n) = (t::ts,n);
    2.15  
    2.16 -val list_ss = simpset_of(the_context());
    2.17 -
    2.18  fun list_eq ss (Const(_,eqT) $ lhs $ rhs) =
    2.19    let
    2.20      val (ls,m) = len lhs ([],0) and (rs,n) = len rhs ([],0);
    2.21 @@ -320,8 +316,8 @@
    2.22          val eq_len = HOLogic.mk_eq (size $ lhs, size $ rhs);
    2.23          val neq_len = HOLogic.mk_Trueprop (HOLogic.Not $ eq_len);
    2.24          val thm = Goal.prove (Simplifier.the_context ss) [] [] neq_len
    2.25 -          (K (simp_tac (Simplifier.inherit_context ss list_ss) 1));
    2.26 -      in SOME (thm RS neq_if_length_neq) end
    2.27 +          (K (simp_tac (Simplifier.inherit_context ss @{simpset}) 1));
    2.28 +      in SOME (thm RS @{thm neq_if_length_neq}) end
    2.29    in
    2.30      if m < n andalso gen_submultiset (op aconv) (ls,rs) orelse
    2.31         n < m andalso gen_submultiset (op aconv) (rs,ls)
    2.32 @@ -331,7 +327,7 @@
    2.33  in
    2.34  
    2.35  val list_neq_simproc =
    2.36 -  Simplifier.simproc (the_context ()) "list_neq" ["(xs::'a list) = ys"] (K list_eq);
    2.37 +  Simplifier.simproc @{theory} "list_neq" ["(xs::'a list) = ys"] (K list_eq);
    2.38  
    2.39  end;
    2.40  
    2.41 @@ -441,12 +437,6 @@
    2.42  ML_setup {*
    2.43  local
    2.44  
    2.45 -val append_assoc = thm "append_assoc";
    2.46 -val append_Nil = thm "append_Nil";
    2.47 -val append_Cons = thm "append_Cons";
    2.48 -val append1_eq_conv = thm "append1_eq_conv";
    2.49 -val append_same_eq = thm "append_same_eq";
    2.50 -
    2.51  fun last (cons as Const("List.list.Cons",_) $ _ $ xs) =
    2.52    (case xs of Const("List.list.Nil",_) => cons | _ => last xs)
    2.53    | last (Const("List.op @",_) $ _ $ ys) = last ys
    2.54 @@ -460,7 +450,8 @@
    2.55    | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
    2.56    | butlast xs = Const("List.list.Nil",fastype_of xs);
    2.57  
    2.58 -val rearr_ss = HOL_basic_ss addsimps [append_assoc, append_Nil, append_Cons];
    2.59 +val rearr_ss = HOL_basic_ss addsimps [@{thm append_assoc},
    2.60 +  @{thm append_Nil}, @{thm append_Cons}];
    2.61  
    2.62  fun list_eq ss (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
    2.63    let
    2.64 @@ -478,15 +469,15 @@
    2.65        in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
    2.66  
    2.67    in
    2.68 -    if list1 lastl andalso list1 lastr then rearr append1_eq_conv
    2.69 -    else if lastl aconv lastr then rearr append_same_eq
    2.70 +    if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv}
    2.71 +    else if lastl aconv lastr then rearr @{thm append_same_eq}
    2.72      else NONE
    2.73    end;
    2.74  
    2.75  in
    2.76  
    2.77  val list_eq_simproc =
    2.78 -  Simplifier.simproc (the_context ()) "list_eq" ["(xs::'a list) = ys"] (K list_eq);
    2.79 +  Simplifier.simproc @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);
    2.80  
    2.81  end;
    2.82  
     3.1 --- a/src/HOL/MicroJava/J/WellForm.thy	Wed Apr 11 08:28:13 2007 +0200
     3.2 +++ b/src/HOL/MicroJava/J/WellForm.thy	Wed Apr 11 08:28:14 2007 +0200
     3.3 @@ -505,7 +505,7 @@
     3.4  apply(  rotate_tac -1, frule ssubst, erule_tac [2] asm_rl)
     3.5  prefer 2
     3.6  apply(  rotate_tac -1, frule ssubst, erule_tac [2] asm_rl)
     3.7 -apply(  tactic "asm_full_simp_tac (HOL_ss addsimps [not_None_eq RS sym]) 1")
     3.8 +apply(  tactic "asm_full_simp_tac (HOL_ss addsimps [@{thm not_None_eq} RS sym]) 1")
     3.9  apply(  simp_all (no_asm_simp) del: split_paired_Ex)
    3.10  apply( frule (1) class_wf)
    3.11  apply( simp (no_asm_simp) only: split_tupled_all)