src/Provers/splitter.ML
author nipkow
Sun Apr 16 11:56:11 1995 +0200 (1995-04-16)
changeset 1064 5d6fb2c938e0
parent 1030 1d8fa2fc4b9c
child 1686 c67d543bc395
permissions -rw-r--r--
Fixed bug.
     1 (*  Title:      Provers/splitter
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1995  TU Munich
     5 
     6 Generic case-splitter, suitable for most logics.
     7 
     8 Use:
     9 
    10 val split_tac = mk_case_split_tac iffD;
    11 
    12 by(case_split_tac splits i);
    13 
    14 where splits = [P(elim(...)) == rhs, ...]
    15       iffD  = [| P <-> Q; Q |] ==> P (* is called iffD2 in HOL *)
    16 
    17 *)
    18 
    19 fun mk_case_split_tac iffD =
    20 let
    21 
    22 val lift =
    23   let val ct = read_cterm (#sign(rep_thm iffD))
    24            ("[| !!x::'b::logic. Q(x) == R(x) |] ==> \
    25             \P(%x.Q(x)) == P(%x.R(x))::'a::logic",propT)
    26   in prove_goalw_cterm [] ct
    27      (fn [prem] => [rewtac prem, rtac reflexive_thm 1])
    28   end;
    29 
    30 val trlift = lift RS transitive_thm;
    31 val _ $ (Var(P,PT)$_) $ _ = concl_of trlift;
    32 
    33 
    34 fun mk_cntxt Ts t pos T maxi =
    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 
    45 fun add_lbnos(is,t) = add_loose_bnos(t,0,is);
    46 
    47 (* check if the innermost quantifier that needs to be removed
    48    has a body of type T; otherwise the expansion thm will fail later on
    49 *)
    50 fun type_test(T,lbnos,apsns) =
    51   let val (_,U,_) = nth_elem(min lbnos,apsns)
    52   in T=U end;
    53 
    54 fun mk_split_pack(thm,T,n,ts,apsns) =
    55   if n > length ts then []
    56   else let val lev = length apsns
    57            val lbnos = foldl add_lbnos ([],take(n,ts))
    58            val flbnos = filter (fn i => i < lev) lbnos
    59        in if null flbnos then [(thm,[])]
    60           else if type_test(T,flbnos,apsns) then [(thm, rev apsns)] else []
    61        end;
    62 
    63 fun split_posns cmap Ts t =
    64   let fun posns Ts pos apsns (Abs(_,T,t)) =
    65             let val U = fastype_of1(T::Ts,t)
    66             in posns (T::Ts) (0::pos) ((T,U,pos)::apsns) t end
    67         | posns Ts pos apsns t =
    68             let val (h,ts) = strip_comb t
    69                 fun iter((i,a),t) = (i+1, (posns Ts (i::pos) apsns t) @ a);
    70                 val a = case h of
    71                   Const(c,_) =>
    72                     (case assoc(cmap,c) of
    73                        Some(thm,T,n) => mk_split_pack(thm,T,n,ts,apsns)
    74                      | None => [])
    75                 | _ => []
    76              in snd(foldl iter ((0,a),ts)) end
    77   in posns Ts [] [] t end;
    78 
    79 fun nth_subgoal i thm = nth_elem(i-1,prems_of thm);
    80 
    81 fun shorter((_,ps),(_,qs)) = length ps <= length qs;
    82 
    83 fun select cmap state i =
    84   let val goali = nth_subgoal i state
    85       val Ts = rev(map #2 (Logic.strip_params goali))
    86       val _ $ t $ _ = Logic.strip_assums_concl goali;
    87   in (Ts,t,sort shorter (split_posns cmap Ts t)) end;
    88 
    89 fun inst_lift Ts t (T,U,pos) state lift i =
    90   let val sg = #sign(rep_thm state)
    91       val tsig = #tsig(Sign.rep_sg sg)
    92       val cntxt = mk_cntxt Ts t pos (T-->U) (#maxidx(rep_thm lift))
    93       val cu = cterm_of sg cntxt
    94       val uT = #T(rep_cterm cu)
    95       val cP' = cterm_of sg (Var(P,uT))
    96       val ixnTs = Type.typ_match tsig ([],(PT,uT));
    97       val ixncTs = map (fn (x,y) => (x,ctyp_of sg y)) ixnTs;
    98   in instantiate (ixncTs, [(cP',cu)]) lift end;
    99 
   100 
   101 fun split_tac [] i = no_tac
   102   | split_tac splits i =
   103   let fun const(thm) = let val _$(t as _$lhs)$_ = concl_of thm
   104                            val (Const(a,_),args) = strip_comb lhs
   105                        in (a,(thm,fastype_of t,length args)) end
   106       val cmap = map const splits;
   107       fun lift Ts t p state = rtac (inst_lift Ts t p state trlift i) i
   108       fun lift_split state =
   109             let val (Ts,t,splits) = select cmap state i
   110             in case splits of
   111                  [] => no_tac
   112                | (thm,apsns)::_ =>
   113                    (case apsns of
   114                       [] => rtac thm i
   115                     | p::_ => EVERY[STATE(lift Ts t p),
   116                                     rtac reflexive_thm (i+1),
   117                                     STATE lift_split])
   118             end
   119   in STATE(fn thm =>
   120        if i <= nprems_of thm then rtac iffD i THEN STATE lift_split
   121        else no_tac)
   122   end;
   123 
   124 in split_tac end;