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.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
```