src/Pure/proofterm.ML
changeset 12279 dc3020e938e2
parent 12233 3348aa8061d1
child 12293 ce14a4faeded
     1.1 --- a/src/Pure/proofterm.ML	Fri Nov 23 19:20:58 2001 +0100
     1.2 +++ b/src/Pure/proofterm.ML	Sat Nov 24 13:58:19 2001 +0100
     1.3 @@ -51,6 +51,8 @@
     1.4    val incr_pboundvars : int -> int -> proof -> proof
     1.5    val prf_loose_bvar1 : proof -> int -> bool
     1.6    val prf_loose_Pbvar1 : proof -> int -> bool
     1.7 +  val prf_add_loose_bnos : int -> int -> proof ->
     1.8 +    int list * int list -> int list * int list
     1.9    val norm_proof : Envir.env -> proof -> proof
    1.10    val norm_proof' : Envir.env -> proof -> proof
    1.11    val prf_subst_bounds : term list -> proof -> proof
    1.12 @@ -342,6 +344,23 @@
    1.13    | prf_loose_Pbvar1 (Abst (_, _, prf)) k = prf_loose_Pbvar1 prf k
    1.14    | prf_loose_Pbvar1 _ _ = false;
    1.15  
    1.16 +fun prf_add_loose_bnos plev tlev (PBound i) (is, js) =
    1.17 +      if i < plev then (is, js) else ((i-plev) ins is, js)
    1.18 +  | prf_add_loose_bnos plev tlev (prf1 %% prf2) p =
    1.19 +      prf_add_loose_bnos plev tlev prf2
    1.20 +        (prf_add_loose_bnos plev tlev prf1 p)
    1.21 +  | prf_add_loose_bnos plev tlev (prf % opt) (is, js) =
    1.22 +      prf_add_loose_bnos plev tlev prf (case opt of
    1.23 +          None => (is, ~1 ins js)
    1.24 +        | Some t => (is, add_loose_bnos (t, tlev, js)))
    1.25 +  | prf_add_loose_bnos plev tlev (AbsP (_, opt, prf)) (is, js) =
    1.26 +      prf_add_loose_bnos (plev+1) tlev prf (case opt of
    1.27 +          None => (is, ~1 ins js)
    1.28 +        | Some t => (is, add_loose_bnos (t, tlev, js)))
    1.29 +  | prf_add_loose_bnos plev tlev (Abst (_, _, prf)) p =
    1.30 +      prf_add_loose_bnos plev (tlev+1) prf p
    1.31 +  | prf_add_loose_bnos _ _ _ _ = ([], []);
    1.32 +
    1.33  
    1.34  (**** substitutions ****)
    1.35  
    1.36 @@ -856,46 +875,73 @@
    1.37  
    1.38  (** see pattern.ML **)
    1.39  
    1.40 -fun fomatch Ts tmatch =
    1.41 +fun flt i = filter (fn n => n < i);
    1.42 +
    1.43 +fun fomatch Ts tymatch j =
    1.44    let
    1.45      fun mtch (instsp as (tyinsts, insts)) = fn
    1.46          (Var (ixn, T), t)  =>
    1.47 -	  (tmatch (tyinsts, fn () => (T, fastype_of1 (Ts, t))), (ixn, t)::insts)
    1.48 +          if j>0 andalso not (null (flt j (loose_bnos t)))
    1.49 +          then raise PMatch
    1.50 +          else (tymatch (tyinsts, fn () => (T, fastype_of1 (Ts, t))),
    1.51 +            (ixn, t) :: insts)
    1.52        | (Free (a, T), Free (b, U)) =>
    1.53 -	  if a=b then (tmatch (tyinsts, K (T, U)), insts) else raise PMatch
    1.54 +	  if a=b then (tymatch (tyinsts, K (T, U)), insts) else raise PMatch
    1.55        | (Const (a, T), Const (b, U))  =>
    1.56 -	  if a=b then (tmatch (tyinsts, K (T, U)), insts) else raise PMatch
    1.57 +	  if a=b then (tymatch (tyinsts, K (T, U)), insts) else raise PMatch
    1.58        | (f $ t, g $ u) => mtch (mtch instsp (f, g)) (t, u)
    1.59 +      | (Bound i, Bound j) => if i=j then instsp else raise PMatch
    1.60        | _ => raise PMatch
    1.61    in mtch end;
    1.62  
    1.63 -fun match_proof Ts tmatch =
    1.64 +fun match_proof Ts tymatch =
    1.65    let
    1.66 -    fun mtch (inst as (pinst, tinst as (tyinsts, insts))) = fn
    1.67 -        (Hyp (Var (ixn, _)), prf) => ((ixn, prf)::pinst, tinst)
    1.68 -      | (prf1 % opt1, prf2 % opt2) =>
    1.69 -          let val inst' as (pinst, tinst) = mtch inst (prf1, prf2)
    1.70 -          in (case (opt1, opt2) of
    1.71 -                (None, _) => inst'
    1.72 -              | (Some _, None) => raise PMatch
    1.73 -              | (Some t, Some u) => (pinst, fomatch Ts tmatch tinst (t, Envir.beta_norm u)))
    1.74 -          end
    1.75 -      | (prf1 %% prf2, prf1' %% prf2') =>
    1.76 -          mtch (mtch inst (prf1, prf1')) (prf2, prf2')
    1.77 -      | (PThm ((name1, _), _, prop1, None), PThm ((name2, _), _, prop2, _)) =>
    1.78 -          if name1=name2 andalso prop1=prop2 then inst else raise PMatch
    1.79 -      | (PThm ((name1, _), _, prop1, Some Ts), PThm ((name2, _), _, prop2, Some Us)) =>
    1.80 +    fun optmatch _ inst (None, _) = inst
    1.81 +      | optmatch _ _ (Some _, None) = raise PMatch
    1.82 +      | optmatch mtch inst (Some x, Some y) = mtch inst (x, y)
    1.83 +
    1.84 +    fun matcht Ts j (pinst, tinst) (t, u) =
    1.85 +      (pinst, fomatch Ts tymatch j tinst (t, Envir.beta_norm u));
    1.86 +    fun matchT (pinst, (tyinsts, insts)) p =
    1.87 +      (pinst, (tymatch (tyinsts, K p), insts));
    1.88 +    fun matchTs inst (Ts, Us) = foldl (uncurry matchT) (inst, Ts ~~ Us);
    1.89 +
    1.90 +    fun mtch Ts i j (pinst, tinst) (Hyp (Var (ixn, _)), prf) =
    1.91 +          if i = 0 andalso j = 0 then ((ixn, prf) :: pinst, tinst)
    1.92 +          else (case apfst (flt i) (apsnd (flt j)
    1.93 +                  (prf_add_loose_bnos 0 0 prf ([], []))) of
    1.94 +              ([], []) => ((ixn, incr_pboundvars (~i) (~j) prf) :: pinst, tinst)
    1.95 +            | ([], _) => if j = 0 then
    1.96 +                   ((ixn, incr_pboundvars (~i) (~j) prf) :: pinst, tinst)
    1.97 +                 else raise PMatch
    1.98 +            | _ => raise PMatch)
    1.99 +      | mtch Ts i j (pinst, tinst) (Hyp (Var (ixn, _)), prf) =
   1.100 +          ((ixn, prf) :: pinst, tinst)
   1.101 +      | mtch Ts i j inst (prf1 % opt1, prf2 % opt2) =
   1.102 +          optmatch (matcht Ts j) (mtch Ts i j inst (prf1, prf2)) (opt1, opt2)
   1.103 +      | mtch Ts i j inst (prf1 %% prf2, prf1' %% prf2') =
   1.104 +          mtch Ts i j (mtch Ts i j inst (prf1, prf1')) (prf2, prf2')
   1.105 +      | mtch Ts i j inst (Abst (_, opT, prf1), Abst (_, opU, prf2)) =
   1.106 +          mtch (if_none opU dummyT :: Ts) i (j+1)
   1.107 +            (optmatch matchT inst (opT, opU)) (prf1, prf2)
   1.108 +      | mtch Ts i j inst (prf1, Abst (_, opU, prf2)) =
   1.109 +          mtch (if_none opU dummyT :: Ts) i (j+1) inst
   1.110 +            (incr_pboundvars 0 1 prf1 %> Bound 0, prf2)
   1.111 +      | mtch Ts i j inst (AbsP (_, opt, prf1), AbsP (_, opu, prf2)) =
   1.112 +          mtch Ts (i+1) j (optmatch (matcht Ts j) inst (opt, opu)) (prf1, prf2)
   1.113 +      | mtch Ts i j inst (prf1, AbsP (_, _, prf2)) =
   1.114 +          mtch Ts (i+1) j inst (incr_pboundvars 1 0 prf1 %% PBound 0, prf2)
   1.115 +      | mtch Ts i j inst (PThm ((name1, _), _, prop1, opTs),
   1.116 +            PThm ((name2, _), _, prop2, opUs)) =
   1.117            if name1=name2 andalso prop1=prop2 then
   1.118 -            (pinst, (foldl (tmatch o apsnd K) (tyinsts, Ts ~~ Us), insts))
   1.119 +            optmatch matchTs inst (opTs, opUs)
   1.120            else raise PMatch
   1.121 -      | (PAxm (s1, _, None), PAxm (s2, _, _)) =>
   1.122 -          if s1=s2 then inst else raise PMatch
   1.123 -      | (PAxm (s1, _, Some Ts), PAxm (s2, _, Some Us)) =>
   1.124 -          if s1=s2 then
   1.125 -            (pinst, (foldl (tmatch o apsnd K) (tyinsts, Ts ~~ Us), insts))
   1.126 +      | mtch Ts i j inst (PAxm (s1, _, opTs), PAxm (s2, _, opUs)) =
   1.127 +          if s1=s2 then optmatch matchTs inst (opTs, opUs)
   1.128            else raise PMatch
   1.129 -      | _ => raise PMatch
   1.130 -  in mtch end;
   1.131 +      | mtch _ _ _ inst (PBound i, PBound j) = if i = j then inst else raise PMatch
   1.132 +      | mtch _ _ _ _ _ = raise PMatch
   1.133 +  in mtch Ts 0 0 end;
   1.134  
   1.135  fun prf_subst (pinst, (tyinsts, insts)) =
   1.136    let
   1.137 @@ -928,14 +974,14 @@
   1.138  
   1.139  (**** rewriting on proof terms ****)
   1.140  
   1.141 -fun rewrite_prf tmatch (rules, procs) prf =
   1.142 +fun rewrite_prf tymatch (rules, procs) prf =
   1.143    let
   1.144      fun rew _ (Abst (_, _, body) % Some t) = Some (prf_subst_bounds [t] body)
   1.145        | rew _ (AbsP (_, _, body) %% prf) = Some (prf_subst_pbounds [prf] body)
   1.146        | rew Ts prf = (case get_first (fn (_, r) => r Ts prf) procs of
   1.147            Some prf' => Some prf'
   1.148          | None => get_first (fn (prf1, prf2) => Some (prf_subst
   1.149 -            (match_proof Ts tmatch ([], (Vartab.empty, [])) (prf1, prf)) prf2)
   1.150 +            (match_proof Ts tymatch ([], (Vartab.empty, [])) (prf1, prf)) prf2)
   1.151                 handle PMatch => None) rules);
   1.152  
   1.153      fun rew0 Ts (prf as AbsP (_, _, prf' %% PBound 0)) =