Tuned function mk_cntxt_splitthm.
authorberghofe
Mon Nov 17 09:52:20 1997 +0100 (1997-11-17)
changeset 423229f3875596ad
parent 4231 a73f5a63f197
child 4233 85d004a96b98
Tuned function mk_cntxt_splitthm.
Fixed bug which caused split_tac to fail when
(Const ("splitconst", ...) $ ...) was of function type.
src/Provers/splitter.ML
     1.1 --- a/src/Provers/splitter.ML	Sun Nov 16 16:18:31 1997 +0100
     1.2 +++ b/src/Provers/splitter.ML	Mon Nov 17 09:52:20 1997 +0100
     1.3 @@ -68,31 +68,21 @@
     1.4     Set up term for instantiation of P in the split-theorem
     1.5     P(...) == rhs
     1.6  
     1.7 -   Ts    : types of parameters (i.e. variables bound by meta-quantifiers)
     1.8     t     : lefthand side of meta-equality in subgoal
     1.9             the split theorem is applied to (see select)
    1.10     T     : type of body of P(...)
    1.11 -   tt    : the term  Const(..,..) $ ...
    1.12 -   maxi  : maximum index of Vars
    1.13 -
    1.14 -   lev   : abstraction level
    1.15 +   tt    : the term  Const(key,..) $ ...
    1.16  *************************************************************************)
    1.17  
    1.18 -fun mk_cntxt_splitthm Ts t tt T maxi =
    1.19 -  let fun down lev (Abs(v,T2,t)) = Abs(v,T2,down (lev+1) t)
    1.20 -        | down lev (Bound i) = if i >= lev
    1.21 -                               then Var(("X",maxi+i-lev),nth_elem(i-lev,Ts))
    1.22 -                               else Bound i 
    1.23 -        | down lev t = 
    1.24 -            let val (h,ts) = strip_comb t
    1.25 -                val h2 = (case h of Bound _ => down lev h | _ => h)
    1.26 -            in if incr_bv(lev,0,tt)=t 
    1.27 -               then
    1.28 -                 Bound (lev)
    1.29 -               else
    1.30 -                 list_comb(h2,map (down lev) ts)
    1.31 -            end;
    1.32 -  in Abs("",T,down 0 t) end;
    1.33 +fun mk_cntxt_splitthm t tt T =
    1.34 +  let fun repl lev t =
    1.35 +    if incr_boundvars lev tt = t then Bound lev
    1.36 +    else case t of
    1.37 +        (Abs (v, T2, t)) => Abs (v, T2, repl (lev+1) t)
    1.38 +      | (Bound i) => Bound (if i>=lev then i+1 else i)
    1.39 +      | (t1 $ t2) => (repl lev t1) $ (repl lev t2)
    1.40 +      | t => t
    1.41 +  in Abs("", T, repl 0 t) end;
    1.42  
    1.43  
    1.44  (* add all loose bound variables in t to list is *)
    1.45 @@ -137,7 +127,7 @@
    1.46    else let val lev = length apsns
    1.47             val lbnos = foldl add_lbnos ([],take(n,ts))
    1.48             val flbnos = filter (fn i => i < lev) lbnos
    1.49 -           val tt = incr_bv(~lev,0,t)
    1.50 +           val tt = incr_boundvars (~lev) t
    1.51         in if null flbnos then [(thm,[],pos,TB,tt)]
    1.52            else if type_test(T,flbnos,apsns) then [(thm, rev apsns,pos,TB,tt)] 
    1.53                 else []
    1.54 @@ -168,7 +158,10 @@
    1.55                  val a = case h of
    1.56                    Const(c,_) =>
    1.57                      (case assoc(cmap,c) of
    1.58 -                       Some(thm,T,n) => mk_split_pack(thm,T,n,ts,apsns,pos,type_of1(Ts,t),t)
    1.59 +                       Some(thm, T, n) =>
    1.60 +                         let val t2 = list_comb (h, take (n, ts)) in
    1.61 +                           mk_split_pack(thm,T,n,ts,apsns,pos,type_of1(Ts, t2),t2)
    1.62 +                         end
    1.63                       | None => [])
    1.64                  | _ => []
    1.65               in snd(foldl iter ((0,a),ts)) end
    1.66 @@ -229,23 +222,24 @@
    1.67     Ts    : types of parameters
    1.68     t     : lefthand side of meta-equality in subgoal
    1.69             the split theorem is applied to (see cmap)
    1.70 -   pos   : "path" to the body of P(...)
    1.71 +   tt    : the term  Const(key,..) $ ...
    1.72     thm   : the split theorem
    1.73     TB    : type of body of P(...)
    1.74     state : current proof state
    1.75 +   i     : number of subgoal
    1.76  **************************************************************)
    1.77  
    1.78 -fun inst_split Ts t tt thm TB state =
    1.79 -  let val _$((Var(P2,PT2))$_)$_ = concl_of thm
    1.80 +fun inst_split Ts t tt thm TB state i =
    1.81 +  let val _ $ ((Var (P2, PT2)) $ _) $ _ = concl_of thm;
    1.82        val sg = #sign(rep_thm state)
    1.83        val tsig = #tsig(Sign.rep_sg sg)
    1.84 -      val cntxt = mk_cntxt_splitthm Ts t tt TB (#maxidx(rep_thm thm))
    1.85 -      val cu = cterm_of sg cntxt
    1.86 -      val uT = #T(rep_cterm cu)
    1.87 -      val cP' = cterm_of sg (Var(P2,uT))
    1.88 -      val ixnTs = Type.typ_match tsig ([],(PT2,uT));
    1.89 -      val ixncTs = map (fn (x,y) => (x,ctyp_of sg y)) ixnTs;
    1.90 -  in instantiate (ixncTs, [(cP',cu)]) thm end;
    1.91 +      val cntxt = mk_cntxt_splitthm t tt TB;
    1.92 +      val T = fastype_of cntxt;
    1.93 +      val ixnTs = Type.typ_match tsig ([],(PT2, T))
    1.94 +      val abss = foldl (fn (t, T) => Abs ("", T, t))
    1.95 +  in
    1.96 +    term_lift_inst_rule (state, i, ixnTs, [((P2, T), abss (cntxt, Ts))], thm)
    1.97 +  end;
    1.98  
    1.99  
   1.100  (*****************************************************************************
   1.101 @@ -272,7 +266,7 @@
   1.102                 | (thm,apsns,pos,TB,tt)::_ =>
   1.103                     (case apsns of
   1.104                        [] => (fn state => state |>
   1.105 -			           rtac (inst_split Ts t tt thm TB state) i)
   1.106 +			           compose_tac (false, inst_split Ts t tt thm TB state i, 0) i)
   1.107                      | p::_ => EVERY[lift_tac Ts t p,
   1.108                                      rtac reflexive_thm (i+1),
   1.109                                      lift_split_tac])