src/HOL/List.ML
changeset 5162 53e505c6019c
parent 5132 24f992a25adc
child 5183 89f162de39cf
     1.1 --- a/src/HOL/List.ML	Sat Jul 18 12:41:09 1998 +0200
     1.2 +++ b/src/HOL/List.ML	Mon Jul 20 16:04:53 1998 +0200
     1.3 @@ -779,3 +779,60 @@
     1.4  by (fast_tac (claset() addSDs [not0_implies_Suc] addSIs [lemma]) 1);
     1.5  qed "set_replicate";
     1.6  Addsimps [set_replicate];
     1.7 +
     1.8 +
     1.9 +(***
    1.10 +Simplification procedure for all list equalities.
    1.11 +Currently only tries to rearranges @ to see if
    1.12 +- both lists end in a singleton list,
    1.13 +- or both lists end in the same list.
    1.14 +***)
    1.15 +local
    1.16 +
    1.17 +val list_eq_pattern =
    1.18 +  read_cterm (sign_of List.thy) ("(xs::'a list) = ys",HOLogic.boolT);
    1.19 +
    1.20 +fun last (cons as Const("List.op #",_) $ _ $ xs) =
    1.21 +      (case xs of Const("List.[]",_) => cons | _ => last xs)
    1.22 +  | last (Const("List.op @",_) $ _ $ ys) = last ys
    1.23 +  | last t = t;
    1.24 +
    1.25 +fun list1 (Const("List.op #",_) $ _ $ Const("List.[]",_)) = true
    1.26 +  | list1 _ = false;
    1.27 +
    1.28 +fun butlast ((cons as Const("List.op #",_) $ x) $ xs) =
    1.29 +      (case xs of Const("List.[]",_) => xs | _ => cons $ butlast xs)
    1.30 +  | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
    1.31 +  | butlast xs = Const("List.[]",fastype_of xs);
    1.32 +
    1.33 +val rearr_tac =
    1.34 +  simp_tac (HOL_basic_ss addsimps [append_assoc,append_Nil,append_Cons]);
    1.35 +
    1.36 +fun list_eq sg _ (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
    1.37 +  let
    1.38 +    val lastl = last lhs and lastr = last rhs
    1.39 +    fun rearr conv =
    1.40 +      let val lhs1 = butlast lhs and rhs1 = butlast rhs
    1.41 +          val Type(_,listT::_) = eqT
    1.42 +          val appT = [listT,listT] ---> listT
    1.43 +          val app = Const("List.op @",appT)
    1.44 +          val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
    1.45 +          val ct = cterm_of sg (HOLogic.mk_Trueprop(HOLogic.mk_eq(F,F2)))
    1.46 +          val thm = prove_goalw_cterm [] ct (K [rearr_tac 1])
    1.47 +            handle ERROR =>
    1.48 +            error("The error(s) above occurred while trying to prove " ^
    1.49 +                  string_of_cterm ct)
    1.50 +      in Some((conv RS (thm RS trans)) RS eq_reflection) end
    1.51 +
    1.52 +  in if list1 lastl andalso list1 lastr
    1.53 +     then rearr append1_eq_conv
    1.54 +     else
    1.55 +     if lastl aconv lastr
    1.56 +     then rearr append_same_eq
    1.57 +     else None
    1.58 +  end;
    1.59 +in
    1.60 +val list_eq_simproc = mk_simproc "list_eq" [list_eq_pattern] list_eq;
    1.61 +end;
    1.62 +
    1.63 +Addsimprocs [list_eq_simproc];