src/Provers/splitter.ML
changeset 1030 1d8fa2fc4b9c
parent 943 8477483f663f
child 1064 5d6fb2c938e0
equal deleted inserted replaced
1029:27808dabf4af 1030:1d8fa2fc4b9c
     1 (*  Title:      Provers/splitter
     1 (*  Title:      Provers/splitter
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     3     Author:     Tobias Nipkow
     4     Copyright   1993  TU Munich
     4     Copyright   1995  TU Munich
     5 
     5 
     6 Generic case-splitter, suitable for most logics.
     6 Generic case-splitter, suitable for most logics.
     7 
     7 
     8 Use:
     8 Use:
     9 
     9 
    28   end;
    28   end;
    29 
    29 
    30 val trlift = lift RS transitive_thm;
    30 val trlift = lift RS transitive_thm;
    31 val _ $ (Var(P,PT)$_) $ _ = concl_of trlift;
    31 val _ $ (Var(P,PT)$_) $ _ = concl_of trlift;
    32 
    32 
    33 fun contains cmap =
       
    34   let fun isin i (Abs(_,_,b)) = isin 0 b
       
    35         | isin i (s$t) = isin (i+1) s orelse isin 0 t
       
    36         | isin i (Const(c,_)) = (case assoc(cmap,c) of
       
    37                                    Some(n,_) => n <= i
       
    38                                  | None => false)
       
    39         | isin _ _ = false
       
    40   in isin 0 end;
       
    41 
    33 
    42 fun mk_context cmap Ts maxi t =
    34 fun mk_cntxt Ts t pos T maxi =
    43   let fun var (t,i) = Var(("X",i),type_of1(Ts,t))
    35   let fun var (t,i) = Var(("X",i),type_of1(Ts,t));
       
    36       fun down [] t i = Bound 0
       
    37         | down (p::ps) t i =
       
    38             let val (h,ts) = strip_comb t
       
    39                 val v1 = map var (take(p,ts) ~~ (i upto (i+p-1)))
       
    40                 val u::us = drop(p,ts)
       
    41                 val v2 = map var (us ~~ ((i+p) upto (i+length(ts)-2)))
       
    42       in list_comb(h,v1@[down ps u (i+length ts)]@v2) end;
       
    43   in Abs("", T, down (rev pos) t maxi) end;
    44 
    44 
    45       fun mka((None,i,ts),t) = if contains cmap t
    45 fun add_lbnos(is,t) = add_loose_bnos(t,0,is);
    46             then let val (u,T,j) = mk(t,i) in (Some(T),j,ts@[u]) end
       
    47             else (None,i+1,ts@[var(t,i)])
       
    48         | mka((some,i,ts),t) = (some,i+1,ts@[var(t,i)])
       
    49       and mk(t as Abs _, i) = (Bound 0,type_of1(Ts,t),i)
       
    50         | mk(t,i) =
       
    51             let val (f,ts) = strip_comb t
       
    52                 val (Some(T),j,us) = foldl mka ((None,i,[]),ts)
       
    53             in (list_comb(f,us),T,j) end
       
    54 
    46 
    55       val (u,T,_) = mk(t,maxi+1)
    47 fun typ_test _ [] = true
    56   in Abs("",T,u) end;
    48   | typ_test T ((_,U,_)::_) = (T=U);
       
    49 
       
    50 fun mk_split_pack(thm,T,n,ts,apsns) =
       
    51   if n <= length ts andalso typ_test T apsns
       
    52   then let val lev = length apsns
       
    53            val lbnos = foldl add_lbnos ([],take(n,ts))
       
    54            val flbnos = filter (fn i => i < lev) lbnos
       
    55        in [(thm, if null flbnos then [] else rev apsns)] end
       
    56   else [];
       
    57 
       
    58 fun split_posns cmap Ts t =
       
    59   let fun posns Ts pos apsns (Abs(_,T,t)) =
       
    60             let val U = fastype_of1(T::Ts,t)
       
    61             in posns (T::Ts) (0::pos) ((T,U,pos)::apsns) t end
       
    62         | posns Ts pos apsns t =
       
    63             let val (h,ts) = strip_comb t
       
    64                 fun iter((i,a),t) = (i+1, (posns Ts (i::pos) apsns t) @ a);
       
    65                 val a = case h of
       
    66                   Const(c,_) =>
       
    67                     (case assoc(cmap,c) of
       
    68                        Some(thm,T,n) => mk_split_pack(thm,T,n,ts,apsns)
       
    69                      | None => [])
       
    70                 | _ => []
       
    71              in snd(foldl iter ((0,a),ts)) end
       
    72   in posns Ts [] [] t end;
    57 
    73 
    58 fun nth_subgoal i thm = nth_elem(i-1,prems_of thm);
    74 fun nth_subgoal i thm = nth_elem(i-1,prems_of thm);
    59 
    75 
    60 fun goal_concl i thm = Logic.strip_assums_concl(nth_subgoal i thm);
    76 fun shorter((_,ps),(_,qs)) = length ps <= length qs;
    61 
    77 
    62 fun inst_lift cmap state lift i =
    78 fun select cmap state i =
       
    79   let val goali = nth_subgoal i state
       
    80       val Ts = rev(map #2 (Logic.strip_params goali))
       
    81       val _ $ t $ _ = Logic.strip_assums_concl goali;
       
    82   in (Ts,t,sort shorter (split_posns cmap Ts t)) end;
       
    83 
       
    84 fun inst_lift Ts t (T,U,pos) state lift i =
    63   let val sg = #sign(rep_thm state)
    85   let val sg = #sign(rep_thm state)
    64       val tsig = #tsig(Sign.rep_sg sg)
    86       val tsig = #tsig(Sign.rep_sg sg)
    65       val goali = nth_subgoal i state
    87       val cntxt = mk_cntxt Ts t pos (T-->U) (#maxidx(rep_thm lift))
    66       val Ts = map #2 (Logic.strip_params goali)
       
    67       val _ $ t $ _ = Logic.strip_assums_concl goali;
       
    68       val cntxt = mk_context cmap (rev Ts) (#maxidx(rep_thm lift)) t
       
    69       val cu = cterm_of sg cntxt
    88       val cu = cterm_of sg cntxt
    70       val uT = #T(rep_cterm cu)
    89       val uT = #T(rep_cterm cu)
    71       val cP' = cterm_of sg (Var(P,uT))
    90       val cP' = cterm_of sg (Var(P,uT))
    72       val ixnTs = Type.typ_match tsig ([],(PT,uT));
    91       val ixnTs = Type.typ_match tsig ([],(PT,uT));
    73       val ixncTs = map (fn (x,y) => (x,ctyp_of sg y)) ixnTs;
    92       val ixncTs = map (fn (x,y) => (x,ctyp_of sg y)) ixnTs;
    74   in instantiate (ixncTs, [(cP',cu)]) lift end;
    93   in instantiate (ixncTs, [(cP',cu)]) lift end;
    75 
    94 
    76 fun splittable al i thm =
       
    77   let val tm = goal_concl i thm
       
    78       fun nobound j k (Abs(_,_,t)) = nobound j (k+1) t
       
    79         | nobound j k (s$t) = nobound j k s andalso nobound j k t
       
    80         | nobound j k (Bound n) = n < k orelse k+j <= n
       
    81         | nobound _ _ _ = true;
       
    82       fun find j (None,t) = (case t of
       
    83             Abs(_,_,t) => find (j+1) (None,t)
       
    84           | _ => let val (h,args) = strip_comb t
       
    85                      fun no() = foldl (find j) (None,args)
       
    86                  in case h of
       
    87                       Const(c,_) =>
       
    88                         (case assoc(al,c) of
       
    89                            Some(n,thm) =>
       
    90                              if length args < n then no()
       
    91                              else if forall (nobound j 0) (take(n,args))
       
    92                                   then Some(thm)
       
    93                                   else no()
       
    94                          | None => no())
       
    95                     | _ => no()
       
    96                  end)
       
    97         | find _ (some,_) = some
       
    98   in find 0 (None,tm) end;
       
    99 
    95 
   100 fun split_tac [] i = no_tac
    96 fun split_tac [] i = no_tac
   101   | split_tac splits i =
    97   | split_tac splits i =
   102   let fun const(thm) = let val _$(_$lhs)$_ = concl_of thm
    98   let fun const(thm) = let val _$(t as _$lhs)$_ = concl_of thm
   103                            val (Const(a,_),args) = strip_comb lhs
    99                            val (Const(a,_),args) = strip_comb lhs
   104                        in (a,(length args,thm)) end
   100                        in (a,(thm,fastype_of t,length args)) end
   105       val cmap = map const splits;
   101       val cmap = map const splits;
   106       fun lift thm = rtac (inst_lift cmap thm trlift i) i
   102       fun lift Ts t p state = rtac (inst_lift Ts t p state trlift i) i
   107       fun lift_split thm =
   103       fun lift_split state =
   108             case splittable cmap i thm of
   104             let val (Ts,t,splits) = select cmap state i
   109               Some(split) => rtac split i
   105             in case splits of
   110             | None => EVERY[STATE lift, rtac reflexive_thm (i+1),
   106                  [] => no_tac
   111                             STATE lift_split]
   107                | (thm,apsns)::_ =>
       
   108                    (case apsns of
       
   109                       [] => rtac thm i
       
   110                     | p::_ => EVERY[STATE(lift Ts t p),
       
   111                                     rtac reflexive_thm (i+1),
       
   112                                     STATE lift_split])
       
   113             end
   112   in STATE(fn thm =>
   114   in STATE(fn thm =>
   113        if (i <= nprems_of thm)  andalso  contains cmap (goal_concl i thm)
   115        if i <= nprems_of thm then rtac iffD i THEN STATE lift_split
   114        then EVERY[rtac iffD i, STATE lift_split]
       
   115        else no_tac)
   116        else no_tac)
   116   end;
   117   end;
   117 
   118 
   118 in split_tac end;
   119 in split_tac end;