src/Provers/splitter.ML
changeset 1721 445654b6cb95
parent 1686 c67d543bc395
child 2143 093bbe6d333b
     1.1 --- a/src/Provers/splitter.ML	Mon May 06 10:44:43 1996 +0200
     1.2 +++ b/src/Provers/splitter.ML	Mon May 06 15:19:50 1996 +0200
     1.3 @@ -16,7 +16,9 @@
     1.4  
     1.5  *)
     1.6  
     1.7 -fun mk_case_split_tac iffD =
     1.8 +local
     1.9 +
    1.10 +fun mk_case_split_tac_2 iffD order =
    1.11  let
    1.12  
    1.13  
    1.14 @@ -69,25 +71,28 @@
    1.15     Ts    : types of parameters (i.e. variables bound by meta-quantifiers)
    1.16     t     : lefthand side of meta-equality in subgoal
    1.17             the split theorem is applied to (see select)
    1.18 -   pos   : "path" leading to body of P(...), coded as a list
    1.19     T     : type of body of P(...)
    1.20 +   tt    : the term  Const(..,..) $ ...
    1.21     maxi  : maximum index of Vars
    1.22  
    1.23 -   bvars : type of variables bound by other than meta-quantifiers
    1.24 +   lev   : abstraction level
    1.25  *************************************************************************)
    1.26  
    1.27 -fun mk_cntxt_splitthm Ts t pos T maxi =
    1.28 -  let fun down [] t i bvars = Bound (length bvars)
    1.29 -        | down (p::ps) (Abs(v,T2,t)) i bvars = Abs(v,T2,down ps t i (T2::bvars))
    1.30 -        | down (p::ps) t i bvars =
    1.31 -            let val vars = map Bound (0 upto ((length bvars)-1))
    1.32 -                val (h,ts) = strip_comb t
    1.33 -                fun var (t,i) = list_comb(Var(("X",i),bvars ---> (type_of1(bvars @ Ts,t))),vars);
    1.34 -                val v1 = map var (take(p,ts) ~~ (i upto (i+p-1)))
    1.35 -                val u::us = drop(p,ts)
    1.36 -                val v2 = map var (us ~~ ((i+p) upto (i+length(ts)-2)))
    1.37 -            in list_comb(h,v1@[down ps u (i+length ts) bvars]@v2) end;
    1.38 -  in Abs("",T,down (rev pos) t maxi []) end;
    1.39 +fun mk_cntxt_splitthm Ts t tt T maxi =
    1.40 +  let fun down lev (Abs(v,T2,t)) = Abs(v,T2,down (lev+1) t)
    1.41 +        | down lev (Bound i) = if i >= lev
    1.42 +                               then Var(("X",maxi+i-lev),nth_elem(i-lev,Ts))
    1.43 +                               else Bound i 
    1.44 +        | down lev t = 
    1.45 +            let val (h,ts) = strip_comb t
    1.46 +                val h2 = (case h of Bound _ => down lev h | _ => h)
    1.47 +            in if incr_bv(lev,0,tt)=t 
    1.48 +               then
    1.49 +                 Bound (lev)
    1.50 +               else
    1.51 +                 list_comb(h2,map (down lev) ts)
    1.52 +            end;
    1.53 +  in Abs("",T,down 0 t) end;
    1.54  
    1.55  
    1.56  (* add all loose bound variables in t to list is *)
    1.57 @@ -117,6 +122,7 @@
    1.58             pos : "path" leading to the body of the abstraction
    1.59     pos   : "path" leading to the position where Const(key, ...) $ ...  occurs.
    1.60     TB    : type of  Const(key,...) $ t_1 $ ... $ t_n
    1.61 +   t     : the term Const(key,...) $ t_1 $ ... $ t_n
    1.62  
    1.63     A split pack is a tuple of the form
    1.64     (thm, apsns, pos, TB)
    1.65 @@ -126,13 +132,14 @@
    1.66            lifting is required before applying the split-theorem.
    1.67  ******************************************************************************) 
    1.68  
    1.69 -fun mk_split_pack(thm,T,n,ts,apsns,pos,TB) =
    1.70 +fun mk_split_pack(thm,T,n,ts,apsns,pos,TB,t) =
    1.71    if n > length ts then []
    1.72    else let val lev = length apsns
    1.73             val lbnos = foldl add_lbnos ([],take(n,ts))
    1.74             val flbnos = filter (fn i => i < lev) lbnos
    1.75 -       in if null flbnos then [(thm,[],pos,TB)]
    1.76 -          else if type_test(T,flbnos,apsns) then [(thm, rev apsns,pos,TB)] else []
    1.77 +           val tt = incr_bv(~lev,0,t)
    1.78 +       in if null flbnos then [(thm,[],pos,TB,tt)]
    1.79 +          else if type_test(T,flbnos,apsns) then [(thm, rev apsns,pos,TB,tt)] else []
    1.80         end;
    1.81  
    1.82  
    1.83 @@ -160,7 +167,7 @@
    1.84                  val a = case h of
    1.85                    Const(c,_) =>
    1.86                      (case assoc(cmap,c) of
    1.87 -                       Some(thm,T,n) => mk_split_pack(thm,T,n,ts,apsns,pos,type_of1(Ts,t))
    1.88 +                       Some(thm,T,n) => mk_split_pack(thm,T,n,ts,apsns,pos,type_of1(Ts,t),t)
    1.89                       | None => [])
    1.90                  | _ => []
    1.91               in snd(foldl iter ((0,a),ts)) end
    1.92 @@ -169,9 +176,9 @@
    1.93  
    1.94  fun nth_subgoal i thm = nth_elem(i-1,prems_of thm);
    1.95  
    1.96 -fun shorter((_,ps,pos,_),(_,qs,qos,_)) =
    1.97 +fun shorter((_,ps,pos,_,_),(_,qs,qos,_,_)) =
    1.98    let val ms = length ps and ns = length qs
    1.99 -  in ms < ns orelse (ms = ns andalso length pos >= length qos) end;
   1.100 +  in ms < ns orelse (ms = ns andalso order(length pos,length qos)) end;
   1.101  
   1.102  
   1.103  (************************************************************
   1.104 @@ -227,11 +234,11 @@
   1.105     state : current proof state
   1.106  **************************************************************)
   1.107  
   1.108 -fun inst_split Ts t pos thm TB state =
   1.109 +fun inst_split Ts t tt thm TB state =
   1.110    let val _$((Var(P2,PT2))$_)$_ = concl_of thm
   1.111        val sg = #sign(rep_thm state)
   1.112        val tsig = #tsig(Sign.rep_sg sg)
   1.113 -      val cntxt = mk_cntxt_splitthm Ts t pos TB (#maxidx(rep_thm thm))
   1.114 +      val cntxt = mk_cntxt_splitthm Ts t tt TB (#maxidx(rep_thm thm))
   1.115        val cu = cterm_of sg cntxt
   1.116        val uT = #T(rep_cterm cu)
   1.117        val cP' = cterm_of sg (Var(P2,uT))
   1.118 @@ -258,9 +265,9 @@
   1.119              let val (Ts,t,splits) = select cmap state i
   1.120              in case splits of
   1.121                   [] => no_tac
   1.122 -               | (thm,apsns,pos,TB)::_ =>
   1.123 +               | (thm,apsns,pos,TB,tt)::_ =>
   1.124                     (case apsns of
   1.125 -                      [] => STATE(fn state => rtac (inst_split Ts t pos thm TB state) i)
   1.126 +                      [] => STATE(fn state => rtac (inst_split Ts t tt thm TB state) i)
   1.127                      | p::_ => EVERY[STATE(lift Ts t p),
   1.128                                      rtac reflexive_thm (i+1),
   1.129                                      STATE lift_split])
   1.130 @@ -271,3 +278,11 @@
   1.131    end;
   1.132  
   1.133  in split_tac end;
   1.134 +
   1.135 +in
   1.136 +
   1.137 +fun mk_case_split_tac iffD = mk_case_split_tac_2 iffD (op <=) ;
   1.138 +
   1.139 +fun mk_case_split_inside_tac iffD = mk_case_split_tac_2 iffD (op >=) ;
   1.140 +
   1.141 +end;