src/Provers/splitter.ML
changeset 1030 1d8fa2fc4b9c
parent 943 8477483f663f
child 1064 5d6fb2c938e0
     1.1 --- a/src/Provers/splitter.ML	Wed Apr 12 13:53:34 1995 +0200
     1.2 +++ b/src/Provers/splitter.ML	Thu Apr 13 10:20:55 1995 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      Provers/splitter
     1.5      ID:         $Id$
     1.6      Author:     Tobias Nipkow
     1.7 -    Copyright   1993  TU Munich
     1.8 +    Copyright   1995  TU Munich
     1.9  
    1.10  Generic case-splitter, suitable for most logics.
    1.11  
    1.12 @@ -30,42 +30,61 @@
    1.13  val trlift = lift RS transitive_thm;
    1.14  val _ $ (Var(P,PT)$_) $ _ = concl_of trlift;
    1.15  
    1.16 -fun contains cmap =
    1.17 -  let fun isin i (Abs(_,_,b)) = isin 0 b
    1.18 -        | isin i (s$t) = isin (i+1) s orelse isin 0 t
    1.19 -        | isin i (Const(c,_)) = (case assoc(cmap,c) of
    1.20 -                                   Some(n,_) => n <= i
    1.21 -                                 | None => false)
    1.22 -        | isin _ _ = false
    1.23 -  in isin 0 end;
    1.24  
    1.25 -fun mk_context cmap Ts maxi t =
    1.26 -  let fun var (t,i) = Var(("X",i),type_of1(Ts,t))
    1.27 +fun mk_cntxt Ts t pos T maxi =
    1.28 +  let fun var (t,i) = Var(("X",i),type_of1(Ts,t));
    1.29 +      fun down [] t i = Bound 0
    1.30 +        | down (p::ps) t i =
    1.31 +            let val (h,ts) = strip_comb t
    1.32 +                val v1 = map var (take(p,ts) ~~ (i upto (i+p-1)))
    1.33 +                val u::us = drop(p,ts)
    1.34 +                val v2 = map var (us ~~ ((i+p) upto (i+length(ts)-2)))
    1.35 +      in list_comb(h,v1@[down ps u (i+length ts)]@v2) end;
    1.36 +  in Abs("", T, down (rev pos) t maxi) end;
    1.37 +
    1.38 +fun add_lbnos(is,t) = add_loose_bnos(t,0,is);
    1.39 +
    1.40 +fun typ_test _ [] = true
    1.41 +  | typ_test T ((_,U,_)::_) = (T=U);
    1.42  
    1.43 -      fun mka((None,i,ts),t) = if contains cmap t
    1.44 -            then let val (u,T,j) = mk(t,i) in (Some(T),j,ts@[u]) end
    1.45 -            else (None,i+1,ts@[var(t,i)])
    1.46 -        | mka((some,i,ts),t) = (some,i+1,ts@[var(t,i)])
    1.47 -      and mk(t as Abs _, i) = (Bound 0,type_of1(Ts,t),i)
    1.48 -        | mk(t,i) =
    1.49 -            let val (f,ts) = strip_comb t
    1.50 -                val (Some(T),j,us) = foldl mka ((None,i,[]),ts)
    1.51 -            in (list_comb(f,us),T,j) end
    1.52 +fun mk_split_pack(thm,T,n,ts,apsns) =
    1.53 +  if n <= length ts andalso typ_test T apsns
    1.54 +  then let val lev = length apsns
    1.55 +           val lbnos = foldl add_lbnos ([],take(n,ts))
    1.56 +           val flbnos = filter (fn i => i < lev) lbnos
    1.57 +       in [(thm, if null flbnos then [] else rev apsns)] end
    1.58 +  else [];
    1.59  
    1.60 -      val (u,T,_) = mk(t,maxi+1)
    1.61 -  in Abs("",T,u) end;
    1.62 +fun split_posns cmap Ts t =
    1.63 +  let fun posns Ts pos apsns (Abs(_,T,t)) =
    1.64 +            let val U = fastype_of1(T::Ts,t)
    1.65 +            in posns (T::Ts) (0::pos) ((T,U,pos)::apsns) t end
    1.66 +        | posns Ts pos apsns t =
    1.67 +            let val (h,ts) = strip_comb t
    1.68 +                fun iter((i,a),t) = (i+1, (posns Ts (i::pos) apsns t) @ a);
    1.69 +                val a = case h of
    1.70 +                  Const(c,_) =>
    1.71 +                    (case assoc(cmap,c) of
    1.72 +                       Some(thm,T,n) => mk_split_pack(thm,T,n,ts,apsns)
    1.73 +                     | None => [])
    1.74 +                | _ => []
    1.75 +             in snd(foldl iter ((0,a),ts)) end
    1.76 +  in posns Ts [] [] t end;
    1.77  
    1.78  fun nth_subgoal i thm = nth_elem(i-1,prems_of thm);
    1.79  
    1.80 -fun goal_concl i thm = Logic.strip_assums_concl(nth_subgoal i thm);
    1.81 +fun shorter((_,ps),(_,qs)) = length ps <= length qs;
    1.82  
    1.83 -fun inst_lift cmap state lift i =
    1.84 +fun select cmap state i =
    1.85 +  let val goali = nth_subgoal i state
    1.86 +      val Ts = rev(map #2 (Logic.strip_params goali))
    1.87 +      val _ $ t $ _ = Logic.strip_assums_concl goali;
    1.88 +  in (Ts,t,sort shorter (split_posns cmap Ts t)) end;
    1.89 +
    1.90 +fun inst_lift Ts t (T,U,pos) state lift i =
    1.91    let val sg = #sign(rep_thm state)
    1.92        val tsig = #tsig(Sign.rep_sg sg)
    1.93 -      val goali = nth_subgoal i state
    1.94 -      val Ts = map #2 (Logic.strip_params goali)
    1.95 -      val _ $ t $ _ = Logic.strip_assums_concl goali;
    1.96 -      val cntxt = mk_context cmap (rev Ts) (#maxidx(rep_thm lift)) t
    1.97 +      val cntxt = mk_cntxt Ts t pos (T-->U) (#maxidx(rep_thm lift))
    1.98        val cu = cterm_of sg cntxt
    1.99        val uT = #T(rep_cterm cu)
   1.100        val cP' = cterm_of sg (Var(P,uT))
   1.101 @@ -73,45 +92,27 @@
   1.102        val ixncTs = map (fn (x,y) => (x,ctyp_of sg y)) ixnTs;
   1.103    in instantiate (ixncTs, [(cP',cu)]) lift end;
   1.104  
   1.105 -fun splittable al i thm =
   1.106 -  let val tm = goal_concl i thm
   1.107 -      fun nobound j k (Abs(_,_,t)) = nobound j (k+1) t
   1.108 -        | nobound j k (s$t) = nobound j k s andalso nobound j k t
   1.109 -        | nobound j k (Bound n) = n < k orelse k+j <= n
   1.110 -        | nobound _ _ _ = true;
   1.111 -      fun find j (None,t) = (case t of
   1.112 -            Abs(_,_,t) => find (j+1) (None,t)
   1.113 -          | _ => let val (h,args) = strip_comb t
   1.114 -                     fun no() = foldl (find j) (None,args)
   1.115 -                 in case h of
   1.116 -                      Const(c,_) =>
   1.117 -                        (case assoc(al,c) of
   1.118 -                           Some(n,thm) =>
   1.119 -                             if length args < n then no()
   1.120 -                             else if forall (nobound j 0) (take(n,args))
   1.121 -                                  then Some(thm)
   1.122 -                                  else no()
   1.123 -                         | None => no())
   1.124 -                    | _ => no()
   1.125 -                 end)
   1.126 -        | find _ (some,_) = some
   1.127 -  in find 0 (None,tm) end;
   1.128  
   1.129  fun split_tac [] i = no_tac
   1.130    | split_tac splits i =
   1.131 -  let fun const(thm) = let val _$(_$lhs)$_ = concl_of thm
   1.132 +  let fun const(thm) = let val _$(t as _$lhs)$_ = concl_of thm
   1.133                             val (Const(a,_),args) = strip_comb lhs
   1.134 -                       in (a,(length args,thm)) end
   1.135 +                       in (a,(thm,fastype_of t,length args)) end
   1.136        val cmap = map const splits;
   1.137 -      fun lift thm = rtac (inst_lift cmap thm trlift i) i
   1.138 -      fun lift_split thm =
   1.139 -            case splittable cmap i thm of
   1.140 -              Some(split) => rtac split i
   1.141 -            | None => EVERY[STATE lift, rtac reflexive_thm (i+1),
   1.142 -                            STATE lift_split]
   1.143 +      fun lift Ts t p state = rtac (inst_lift Ts t p state trlift i) i
   1.144 +      fun lift_split state =
   1.145 +            let val (Ts,t,splits) = select cmap state i
   1.146 +            in case splits of
   1.147 +                 [] => no_tac
   1.148 +               | (thm,apsns)::_ =>
   1.149 +                   (case apsns of
   1.150 +                      [] => rtac thm i
   1.151 +                    | p::_ => EVERY[STATE(lift Ts t p),
   1.152 +                                    rtac reflexive_thm (i+1),
   1.153 +                                    STATE lift_split])
   1.154 +            end
   1.155    in STATE(fn thm =>
   1.156 -       if (i <= nprems_of thm)  andalso  contains cmap (goal_concl i thm)
   1.157 -       then EVERY[rtac iffD i, STATE lift_split]
   1.158 +       if i <= nprems_of thm then rtac iffD i THEN STATE lift_split
   1.159         else no_tac)
   1.160    end;
   1.161