src/HOL/List.thy
changeset 43594 ef1ddc59b825
parent 43580 023a1d1f97bd
child 44013 5cfc1c36ae97
     1.1 --- a/src/HOL/List.thy	Wed Jun 29 16:31:50 2011 +0200
     1.2 +++ b/src/HOL/List.thy	Wed Jun 29 17:35:46 2011 +0200
     1.3 @@ -726,54 +726,44 @@
     1.4  - or both lists end in the same list.
     1.5  *}
     1.6  
     1.7 -ML {*
     1.8 -local
     1.9 -
    1.10 -fun last (cons as Const(@{const_name Cons},_) $ _ $ xs) =
    1.11 -  (case xs of Const(@{const_name Nil},_) => cons | _ => last xs)
    1.12 -  | last (Const(@{const_name append},_) $ _ $ ys) = last ys
    1.13 -  | last t = t;
    1.14 -
    1.15 -fun list1 (Const(@{const_name Cons},_) $ _ $ Const(@{const_name Nil},_)) = true
    1.16 -  | list1 _ = false;
    1.17 -
    1.18 -fun butlast ((cons as Const(@{const_name Cons},_) $ x) $ xs) =
    1.19 -  (case xs of Const(@{const_name Nil},_) => xs | _ => cons $ butlast xs)
    1.20 -  | butlast ((app as Const(@{const_name append},_) $ xs) $ ys) = app $ butlast ys
    1.21 -  | butlast xs = Const(@{const_name Nil},fastype_of xs);
    1.22 -
    1.23 -val rearr_ss = HOL_basic_ss addsimps [@{thm append_assoc},
    1.24 -  @{thm append_Nil}, @{thm append_Cons}];
    1.25 -
    1.26 -fun list_eq ss (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
    1.27 +simproc_setup list_eq ("(xs::'a list) = ys")  = {*
    1.28    let
    1.29 -    val lastl = last lhs and lastr = last rhs;
    1.30 -    fun rearr conv =
    1.31 +    fun last (cons as Const (@{const_name Cons}, _) $ _ $ xs) =
    1.32 +          (case xs of Const (@{const_name Nil}, _) => cons | _ => last xs)
    1.33 +      | last (Const(@{const_name append},_) $ _ $ ys) = last ys
    1.34 +      | last t = t;
    1.35 +    
    1.36 +    fun list1 (Const(@{const_name Cons},_) $ _ $ Const(@{const_name Nil},_)) = true
    1.37 +      | list1 _ = false;
    1.38 +    
    1.39 +    fun butlast ((cons as Const(@{const_name Cons},_) $ x) $ xs) =
    1.40 +          (case xs of Const (@{const_name Nil}, _) => xs | _ => cons $ butlast xs)
    1.41 +      | butlast ((app as Const (@{const_name append}, _) $ xs) $ ys) = app $ butlast ys
    1.42 +      | butlast xs = Const(@{const_name Nil}, fastype_of xs);
    1.43 +    
    1.44 +    val rearr_ss =
    1.45 +      HOL_basic_ss addsimps [@{thm append_assoc}, @{thm append_Nil}, @{thm append_Cons}];
    1.46 +    
    1.47 +    fun list_eq ss (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
    1.48        let
    1.49 -        val lhs1 = butlast lhs and rhs1 = butlast rhs;
    1.50 -        val Type(_,listT::_) = eqT
    1.51 -        val appT = [listT,listT] ---> listT
    1.52 -        val app = Const(@{const_name append},appT)
    1.53 -        val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
    1.54 -        val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
    1.55 -        val thm = Goal.prove (Simplifier.the_context ss) [] [] eq
    1.56 -          (K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1));
    1.57 -      in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
    1.58 -
    1.59 -  in
    1.60 -    if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv}
    1.61 -    else if lastl aconv lastr then rearr @{thm append_same_eq}
    1.62 -    else NONE
    1.63 -  end;
    1.64 -
    1.65 -in
    1.66 -
    1.67 -val list_eq_simproc =
    1.68 -  Simplifier.simproc_global @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);
    1.69 -
    1.70 -end;
    1.71 -
    1.72 -Addsimprocs [list_eq_simproc];
    1.73 +        val lastl = last lhs and lastr = last rhs;
    1.74 +        fun rearr conv =
    1.75 +          let
    1.76 +            val lhs1 = butlast lhs and rhs1 = butlast rhs;
    1.77 +            val Type(_,listT::_) = eqT
    1.78 +            val appT = [listT,listT] ---> listT
    1.79 +            val app = Const(@{const_name append},appT)
    1.80 +            val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
    1.81 +            val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
    1.82 +            val thm = Goal.prove (Simplifier.the_context ss) [] [] eq
    1.83 +              (K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1));
    1.84 +          in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
    1.85 +      in
    1.86 +        if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv}
    1.87 +        else if lastl aconv lastr then rearr @{thm append_same_eq}
    1.88 +        else NONE
    1.89 +      end;
    1.90 +  in fn _ => fn ss => fn ct => list_eq ss (term_of ct) end;
    1.91  *}
    1.92  
    1.93