src/HOL/List.thy
changeset 22633 a47e4fd7ebc1
parent 22551 e52f5400e331
child 22793 dc13dfd588b2
     1.1 --- a/src/HOL/List.thy	Wed Apr 11 08:28:13 2007 +0200
     1.2 +++ b/src/HOL/List.thy	Wed Apr 11 08:28:14 2007 +0200
     1.3 @@ -299,8 +299,6 @@
     1.4  ML_setup {*
     1.5  local
     1.6  
     1.7 -val neq_if_length_neq = thm "neq_if_length_neq";
     1.8 -
     1.9  fun len (Const("List.list.Nil",_)) acc = acc
    1.10    | len (Const("List.list.Cons",_) $ _ $ xs) (ts,n) = len xs (ts,n+1)
    1.11    | len (Const("List.op @",_) $ xs $ ys) acc = len xs (len ys acc)
    1.12 @@ -308,8 +306,6 @@
    1.13    | len (Const("List.map",_) $ _ $ xs) acc = len xs acc
    1.14    | len t (ts,n) = (t::ts,n);
    1.15  
    1.16 -val list_ss = simpset_of(the_context());
    1.17 -
    1.18  fun list_eq ss (Const(_,eqT) $ lhs $ rhs) =
    1.19    let
    1.20      val (ls,m) = len lhs ([],0) and (rs,n) = len rhs ([],0);
    1.21 @@ -320,8 +316,8 @@
    1.22          val eq_len = HOLogic.mk_eq (size $ lhs, size $ rhs);
    1.23          val neq_len = HOLogic.mk_Trueprop (HOLogic.Not $ eq_len);
    1.24          val thm = Goal.prove (Simplifier.the_context ss) [] [] neq_len
    1.25 -          (K (simp_tac (Simplifier.inherit_context ss list_ss) 1));
    1.26 -      in SOME (thm RS neq_if_length_neq) end
    1.27 +          (K (simp_tac (Simplifier.inherit_context ss @{simpset}) 1));
    1.28 +      in SOME (thm RS @{thm neq_if_length_neq}) end
    1.29    in
    1.30      if m < n andalso gen_submultiset (op aconv) (ls,rs) orelse
    1.31         n < m andalso gen_submultiset (op aconv) (rs,ls)
    1.32 @@ -331,7 +327,7 @@
    1.33  in
    1.34  
    1.35  val list_neq_simproc =
    1.36 -  Simplifier.simproc (the_context ()) "list_neq" ["(xs::'a list) = ys"] (K list_eq);
    1.37 +  Simplifier.simproc @{theory} "list_neq" ["(xs::'a list) = ys"] (K list_eq);
    1.38  
    1.39  end;
    1.40  
    1.41 @@ -441,12 +437,6 @@
    1.42  ML_setup {*
    1.43  local
    1.44  
    1.45 -val append_assoc = thm "append_assoc";
    1.46 -val append_Nil = thm "append_Nil";
    1.47 -val append_Cons = thm "append_Cons";
    1.48 -val append1_eq_conv = thm "append1_eq_conv";
    1.49 -val append_same_eq = thm "append_same_eq";
    1.50 -
    1.51  fun last (cons as Const("List.list.Cons",_) $ _ $ xs) =
    1.52    (case xs of Const("List.list.Nil",_) => cons | _ => last xs)
    1.53    | last (Const("List.op @",_) $ _ $ ys) = last ys
    1.54 @@ -460,7 +450,8 @@
    1.55    | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
    1.56    | butlast xs = Const("List.list.Nil",fastype_of xs);
    1.57  
    1.58 -val rearr_ss = HOL_basic_ss addsimps [append_assoc, append_Nil, append_Cons];
    1.59 +val rearr_ss = HOL_basic_ss addsimps [@{thm append_assoc},
    1.60 +  @{thm append_Nil}, @{thm append_Cons}];
    1.61  
    1.62  fun list_eq ss (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
    1.63    let
    1.64 @@ -478,15 +469,15 @@
    1.65        in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
    1.66  
    1.67    in
    1.68 -    if list1 lastl andalso list1 lastr then rearr append1_eq_conv
    1.69 -    else if lastl aconv lastr then rearr append_same_eq
    1.70 +    if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv}
    1.71 +    else if lastl aconv lastr then rearr @{thm append_same_eq}
    1.72      else NONE
    1.73    end;
    1.74  
    1.75  in
    1.76  
    1.77  val list_eq_simproc =
    1.78 -  Simplifier.simproc (the_context ()) "list_eq" ["(xs::'a list) = ys"] (K list_eq);
    1.79 +  Simplifier.simproc @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);
    1.80  
    1.81  end;
    1.82