src/Provers/splitter.ML
author berghofe
Thu Apr 25 13:03:57 1996 +0200 (1996-04-25)
changeset 1686 c67d543bc395
parent 1064 5d6fb2c938e0
child 1721 445654b6cb95
permissions -rw-r--r--
Added functions mk_cntxt_splitthm and inst_split which instantiate
the split-rule before it is applied.
Inserted some comments.
     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 
    23 (************************************************************
    24    Create lift-theorem "trlift" :
    25 
    26    [| !! x. Q(x)==R(x) ; P(R) == C |] ==> P(Q)==C
    27 
    28 *************************************************************)
    29  
    30 val lift =
    31   let val ct = read_cterm (#sign(rep_thm iffD))
    32            ("[| !!x::'b::logic. Q(x) == R(x) |] ==> \
    33             \P(%x.Q(x)) == P(%x.R(x))::'a::logic",propT)
    34   in prove_goalw_cterm [] ct
    35      (fn [prem] => [rewtac prem, rtac reflexive_thm 1])
    36   end;
    37 
    38 val trlift = lift RS transitive_thm;
    39 val _ $ (Var(P,PT)$_) $ _ = concl_of trlift;
    40 
    41 
    42 (************************************************************************ 
    43    Set up term for instantiation of P in the lift-theorem
    44    
    45    Ts    : types of parameters (i.e. variables bound by meta-quantifiers)
    46    t     : lefthand side of meta-equality in subgoal
    47            the lift theorem is applied to (see select)
    48    pos   : "path" leading to abstraction, coded as a list
    49    T     : type of body of P(...)
    50    maxi  : maximum index of Vars
    51 *************************************************************************)
    52 
    53 fun mk_cntxt Ts t pos T maxi =
    54   let fun var (t,i) = Var(("X",i),type_of1(Ts,t));
    55       fun down [] t i = Bound 0
    56         | down (p::ps) t i =
    57             let val (h,ts) = strip_comb t
    58                 val v1 = map var (take(p,ts) ~~ (i upto (i+p-1)))
    59                 val u::us = drop(p,ts)
    60                 val v2 = map var (us ~~ ((i+p) upto (i+length(ts)-2)))
    61       in list_comb(h,v1@[down ps u (i+length ts)]@v2) end;
    62   in Abs("", T, down (rev pos) t maxi) end;
    63 
    64 
    65 (************************************************************************ 
    66    Set up term for instantiation of P in the split-theorem
    67    P(...) == rhs
    68 
    69    Ts    : types of parameters (i.e. variables bound by meta-quantifiers)
    70    t     : lefthand side of meta-equality in subgoal
    71            the split theorem is applied to (see select)
    72    pos   : "path" leading to body of P(...), coded as a list
    73    T     : type of body of P(...)
    74    maxi  : maximum index of Vars
    75 
    76    bvars : type of variables bound by other than meta-quantifiers
    77 *************************************************************************)
    78 
    79 fun mk_cntxt_splitthm Ts t pos T maxi =
    80   let fun down [] t i bvars = Bound (length bvars)
    81         | down (p::ps) (Abs(v,T2,t)) i bvars = Abs(v,T2,down ps t i (T2::bvars))
    82         | down (p::ps) t i bvars =
    83             let val vars = map Bound (0 upto ((length bvars)-1))
    84                 val (h,ts) = strip_comb t
    85                 fun var (t,i) = list_comb(Var(("X",i),bvars ---> (type_of1(bvars @ Ts,t))),vars);
    86                 val v1 = map var (take(p,ts) ~~ (i upto (i+p-1)))
    87                 val u::us = drop(p,ts)
    88                 val v2 = map var (us ~~ ((i+p) upto (i+length(ts)-2)))
    89             in list_comb(h,v1@[down ps u (i+length ts) bvars]@v2) end;
    90   in Abs("",T,down (rev pos) t maxi []) end;
    91 
    92 
    93 (* add all loose bound variables in t to list is *)
    94 fun add_lbnos(is,t) = add_loose_bnos(t,0,is);
    95 
    96 (* check if the innermost quantifier that needs to be removed
    97    has a body of type T; otherwise the expansion thm will fail later on
    98 *)
    99 fun type_test(T,lbnos,apsns) =
   100   let val (_,U,_) = nth_elem(min lbnos,apsns)
   101   in T=U end;
   102 
   103 (*************************************************************************
   104    Create a "split_pack".
   105 
   106    thm   : the relevant split-theorem, i.e. P(...) == rhs , where P(...)
   107            is of the form
   108            P( Const(key,...) $ t_1 $ ... $ t_n )      (e.g. key = "if")
   109    T     : type of P(...)
   110    n     : number of arguments expected by Const(key,...)
   111    ts    : list of arguments actually found
   112    apsns : list of tuples of the form (T,U,pos), one tuple for each
   113            abstraction that is encountered on the way to the position where 
   114            Const(key, ...) $ ...  occurs, where
   115            T   : type of the variable bound by the abstraction
   116            U   : type of the abstraction's body
   117            pos : "path" leading to the body of the abstraction
   118    pos   : "path" leading to the position where Const(key, ...) $ ...  occurs.
   119    TB    : type of  Const(key,...) $ t_1 $ ... $ t_n
   120 
   121    A split pack is a tuple of the form
   122    (thm, apsns, pos, TB)
   123    Note : apsns is reversed, so that the outermost quantifier's position
   124           comes first ! If the terms in ts don't contain variables bound
   125           by other than meta-quantifiers, apsns is empty, because no further
   126           lifting is required before applying the split-theorem.
   127 ******************************************************************************) 
   128 
   129 fun mk_split_pack(thm,T,n,ts,apsns,pos,TB) =
   130   if n > length ts then []
   131   else let val lev = length apsns
   132            val lbnos = foldl add_lbnos ([],take(n,ts))
   133            val flbnos = filter (fn i => i < lev) lbnos
   134        in if null flbnos then [(thm,[],pos,TB)]
   135           else if type_test(T,flbnos,apsns) then [(thm, rev apsns,pos,TB)] else []
   136        end;
   137 
   138 
   139 (****************************************************************************
   140    Recursively scans term for occurences of Const(key,...) $ ...
   141    Returns a list of "split-packs" (one for each occurence of Const(key,...) )
   142 
   143    cmap : association list of split-theorems that should be tried.
   144           The elements have the format (key,(thm,T,n)) , where
   145           key : the theorem's key constant ( Const(key,...) $ ... )
   146           thm : the theorem itself
   147           T   : type of P( Const(key,...) $ ... )
   148           n   : number of arguments expected by Const(key,...)
   149    Ts   : types of parameters
   150    t    : the term to be scanned
   151 ******************************************************************************)
   152 
   153 fun split_posns cmap Ts t =
   154   let fun posns Ts pos apsns (Abs(_,T,t)) =
   155             let val U = fastype_of1(T::Ts,t)
   156             in posns (T::Ts) (0::pos) ((T,U,pos)::apsns) t end
   157         | posns Ts pos apsns t =
   158             let val (h,ts) = strip_comb t
   159                 fun iter((i,a),t) = (i+1, (posns Ts (i::pos) apsns t) @ a);
   160                 val a = case h of
   161                   Const(c,_) =>
   162                     (case assoc(cmap,c) of
   163                        Some(thm,T,n) => mk_split_pack(thm,T,n,ts,apsns,pos,type_of1(Ts,t))
   164                      | None => [])
   165                 | _ => []
   166              in snd(foldl iter ((0,a),ts)) end
   167   in posns Ts [] [] t end;
   168 
   169 
   170 fun nth_subgoal i thm = nth_elem(i-1,prems_of thm);
   171 
   172 fun shorter((_,ps,pos,_),(_,qs,qos,_)) =
   173   let val ms = length ps and ns = length qs
   174   in ms < ns orelse (ms = ns andalso length pos >= length qos) end;
   175 
   176 
   177 (************************************************************
   178    call split_posns with appropriate parameters
   179 *************************************************************)
   180 
   181 fun select cmap state i =
   182   let val goali = nth_subgoal i state
   183       val Ts = rev(map #2 (Logic.strip_params goali))
   184       val _ $ t $ _ = Logic.strip_assums_concl goali;
   185   in (Ts,t,sort shorter (split_posns cmap Ts t)) end;
   186 
   187 
   188 (*************************************************************
   189    instantiate lift theorem
   190 
   191    if t is of the form
   192    ... ( Const(...,...) $ Abs( .... ) ) ...
   193    then
   194    P = %a.  ... ( Const(...,...) $ a ) ...
   195    where a has type T --> U
   196 
   197    Ts      : types of parameters
   198    t       : lefthand side of meta-equality in subgoal
   199              the split theorem is applied to (see cmap)
   200    T,U,pos : see mk_split_pack
   201    state   : current proof state
   202    lift    : the lift theorem
   203    i       : no. of subgoal
   204 **************************************************************)
   205 
   206 fun inst_lift Ts t (T,U,pos) state lift i =
   207   let val sg = #sign(rep_thm state)
   208       val tsig = #tsig(Sign.rep_sg sg)
   209       val cntxt = mk_cntxt Ts t pos (T-->U) (#maxidx(rep_thm lift))
   210       val cu = cterm_of sg cntxt
   211       val uT = #T(rep_cterm cu)
   212       val cP' = cterm_of sg (Var(P,uT))
   213       val ixnTs = Type.typ_match tsig ([],(PT,uT));
   214       val ixncTs = map (fn (x,y) => (x,ctyp_of sg y)) ixnTs;
   215   in instantiate (ixncTs, [(cP',cu)]) lift end;
   216 
   217 
   218 (*************************************************************
   219    instantiate split theorem
   220 
   221    Ts    : types of parameters
   222    t     : lefthand side of meta-equality in subgoal
   223            the split theorem is applied to (see cmap)
   224    pos   : "path" to the body of P(...)
   225    thm   : the split theorem
   226    TB    : type of body of P(...)
   227    state : current proof state
   228 **************************************************************)
   229 
   230 fun inst_split Ts t pos thm TB state =
   231   let val _$((Var(P2,PT2))$_)$_ = concl_of thm
   232       val sg = #sign(rep_thm state)
   233       val tsig = #tsig(Sign.rep_sg sg)
   234       val cntxt = mk_cntxt_splitthm Ts t pos TB (#maxidx(rep_thm thm))
   235       val cu = cterm_of sg cntxt
   236       val uT = #T(rep_cterm cu)
   237       val cP' = cterm_of sg (Var(P2,uT))
   238       val ixnTs = Type.typ_match tsig ([],(PT2,uT));
   239       val ixncTs = map (fn (x,y) => (x,ctyp_of sg y)) ixnTs;
   240   in instantiate (ixncTs, [(cP',cu)]) thm end;
   241 
   242 
   243 (*****************************************************************************
   244    The split-tactic
   245    
   246    splits : list of split-theorems to be tried
   247    i      : number of subgoal the tactic should be applied to
   248 *****************************************************************************)
   249 
   250 fun split_tac [] i = no_tac
   251   | split_tac splits i =
   252   let fun const(thm) = let val _$(t as _$lhs)$_ = concl_of thm
   253                            val (Const(a,_),args) = strip_comb lhs
   254                        in (a,(thm,fastype_of t,length args)) end
   255       val cmap = map const splits;
   256       fun lift Ts t p state = rtac (inst_lift Ts t p state trlift i) i
   257       fun lift_split state =
   258             let val (Ts,t,splits) = select cmap state i
   259             in case splits of
   260                  [] => no_tac
   261                | (thm,apsns,pos,TB)::_ =>
   262                    (case apsns of
   263                       [] => STATE(fn state => rtac (inst_split Ts t pos thm TB state) i)
   264                     | p::_ => EVERY[STATE(lift Ts t p),
   265                                     rtac reflexive_thm (i+1),
   266                                     STATE lift_split])
   267             end
   268   in STATE(fn thm =>
   269        if i <= nprems_of thm then rtac iffD i THEN STATE lift_split
   270        else no_tac)
   271   end;
   272 
   273 in split_tac end;