allowed more general split rules to cope with div/mod 2
authornipkow
Fri May 17 11:25:07 2002 +0200 (2002-05-17 ago)
changeset 131574a4599f78f18
parent 13156 4597080b1947
child 13158 8e86582a90d1
allowed more general split rules to cope with div/mod 2
src/Provers/splitter.ML
     1.1 --- a/src/Provers/splitter.ML	Fri May 17 08:53:40 2002 +0200
     1.2 +++ b/src/Provers/splitter.ML	Fri May 17 11:25:07 2002 +0200
     1.3 @@ -4,6 +4,8 @@
     1.4      Copyright   1995  TU Munich
     1.5  
     1.6  Generic case-splitter, suitable for most logics.
     1.7 +Deals with equalities of the form ?P(f args) = ...
     1.8 +where "f args" must be a first-order term without duplicate variables.
     1.9  *)
    1.10  
    1.11  infix 4 addsplits delsplits;
    1.12 @@ -194,6 +196,31 @@
    1.13     t    : the term to be scanned
    1.14  ******************************************************************************)
    1.15  
    1.16 +(* Simplified first-order matching;
    1.17 +   assumes that all Vars in the pattern are distinct;
    1.18 +   see Pure/pattern.ML for the full version;
    1.19 +*)
    1.20 +local
    1.21 +exception MATCH
    1.22 +in
    1.23 +fun typ_match tsig args = (Type.typ_match tsig args)
    1.24 +                          handle Type.TYPE_MATCH => raise MATCH;
    1.25 +fun fomatch tsig args =
    1.26 +  let
    1.27 +    fun mtch tyinsts = fn
    1.28 +        (Ts,Var(_,T), t)  => typ_match tsig (tyinsts, (T, fastype_of1(Ts,t)))
    1.29 +      | (_,Free (a,T), Free (b,U)) =>
    1.30 +          if a=b then typ_match tsig (tyinsts,(T,U)) else raise MATCH
    1.31 +      | (_,Const (a,T), Const (b,U))  =>
    1.32 +          if a=b then typ_match tsig (tyinsts,(T,U)) else raise MATCH
    1.33 +      | (_,Bound i, Bound j)  =>  if  i=j  then tyinsts else raise MATCH
    1.34 +      | (Ts,Abs(_,T,t), Abs(_,U,u))  =>
    1.35 +          mtch (typ_match tsig (tyinsts,(T,U))) (U::Ts,t,u)
    1.36 +      | (Ts, f$t, g$u) => mtch (mtch tyinsts (Ts,f,g)) (Ts, t, u)
    1.37 +      | _ => raise MATCH
    1.38 +  in (mtch Vartab.empty args; true) handle MATCH => false end;
    1.39 +end
    1.40 +
    1.41  fun split_posns cmap sg Ts t =
    1.42    let
    1.43      val T' = fastype_of1 (Ts, t);
    1.44 @@ -207,13 +234,13 @@
    1.45              val a = case h of
    1.46                Const(c, cT) =>
    1.47                  let fun find [] = []
    1.48 -                      | find ((gcT, thm, T, n)::tups) =
    1.49 -                          if Sign.typ_instance sg (cT, gcT)
    1.50 -                          then
    1.51 -                            let val t2 = list_comb (h, take (n, ts))
    1.52 -                            in mk_split_pack(thm,T,T',n,ts,apsns,pos,type_of1(Ts,t2),t2)
    1.53 -                            end
    1.54 -                          else find tups
    1.55 +                      | find ((gcT, pat, thm, T, n)::tups) =
    1.56 +                          let val t2 = list_comb (h, take (n, ts))
    1.57 +                          in if Sign.typ_instance sg (cT, gcT)
    1.58 +                                andalso fomatch (Sign.tsig_of sg) (Ts,pat,t2)
    1.59 +                             then mk_split_pack(thm,T,T',n,ts,apsns,pos,type_of1(Ts,t2),t2)
    1.60 +                             else find tups
    1.61 +                          end
    1.62                  in find (assocs cmap c) end
    1.63              | _ => []
    1.64            in snd(foldl iter ((0, a), ts)) end
    1.65 @@ -304,7 +331,7 @@
    1.66        fun add_thm(cmap,thm) =
    1.67              (case concl_of thm of _$(t as _$lhs)$_ =>
    1.68                 (case strip_comb lhs of (Const(a,aT),args) =>
    1.69 -                  let val info = (aT,thm,fastype_of t,length args)
    1.70 +                  let val info = (aT,lhs,thm,fastype_of t,length args)
    1.71                    in case assoc(cmap,a) of
    1.72                         Some infos => overwrite(cmap,(a,info::infos))
    1.73                       | None => (a,[info])::cmap