Adapted Proofterm.bicompose_proof to Larry's changes in
Logic.assum_pairs from 2005-01-24 (revision 1.44).
--- a/src/Pure/proofterm.ML Fri Jun 08 18:09:37 2007 +0200
+++ b/src/Pure/proofterm.ML Fri Jun 08 18:13:58 2007 +0200
@@ -81,7 +81,7 @@
val lift_proof : term -> int -> term -> proof -> proof
val assumption_proof : term list -> term -> int -> proof -> proof
val bicompose_proof : bool -> term list -> term list -> term list -> term option ->
- int -> proof -> proof -> proof
+ int -> int -> proof -> proof -> proof
val equality_axms : (string * term) list
val reflexive_axm : proof
val symmetric_axm : proof
@@ -717,13 +717,18 @@
(***** proof by assumption *****)
-fun mk_asm_prf (Const ("==>", _) $ A $ B) i = AbsP ("H", NONE (*A*), mk_asm_prf B (i+1))
- | mk_asm_prf (Const ("all", _) $ Abs (a, T, t)) i = Abst (a, NONE (*T*), mk_asm_prf t i)
- | mk_asm_prf _ i = PBound i;
+fun mk_asm_prf t i m =
+ let
+ fun imp_prf _ i 0 = PBound i
+ | imp_prf (Const ("==>", _) $ A $ B) i m = AbsP ("H", NONE (*A*), imp_prf B (i+1) (m-1))
+ | imp_prf _ i _ = PBound i;
+ fun all_prf (Const ("all", _) $ Abs (a, T, t)) = Abst (a, NONE (*T*), all_prf t)
+ | all_prf t = imp_prf t (~i) m
+ in all_prf t end;
fun assumption_proof Bs Bi n prf =
mk_AbsP (length Bs, proof_combP (prf,
- map PBound (length Bs - 1 downto 0) @ [mk_asm_prf Bi (~n)]));
+ map PBound (length Bs - 1 downto 0) @ [mk_asm_prf Bi n ~1]));
(***** Composition of object rule with proof state *****)
@@ -735,14 +740,14 @@
| flatten_params_proof i j n (_, k) = proof_combP (proof_combt (PBound (k+i),
map Bound (j-1 downto 0)), map PBound (remove (op =) (i-n) (i-1 downto 0)));
-fun bicompose_proof flatten Bs oldAs newAs A n rprf sprf =
+fun bicompose_proof flatten Bs oldAs newAs A n m rprf sprf =
let
val la = length newAs;
val lb = length Bs;
in
mk_AbsP (lb+la, proof_combP (sprf,
map PBound (lb + la - 1 downto la)) %%
- proof_combP (rprf, (if n>0 then [mk_asm_prf (the A) (~n)] else []) @
+ proof_combP (rprf, (if n>0 then [mk_asm_prf (the A) n m] else []) @
map (if flatten then flatten_params_proof 0 0 n else PBound o snd)
(oldAs ~~ (la - 1 downto 0))))
end;
--- a/src/Pure/thm.ML Fri Jun 08 18:09:37 2007 +0200
+++ b/src/Pure/thm.ML Fri Jun 08 18:13:58 2007 +0200
@@ -1505,7 +1505,7 @@
(fn f => fn der => f (Pt.norm_proof' env der))
else
curry op oo (Pt.norm_proof' env))
- (Pt.bicompose_proof flatten Bs oldAs As A n)) rder' sder,
+ (Pt.bicompose_proof flatten Bs oldAs As A n (nlift+1))) rder' sder,
tags = [],
maxidx = maxidx,
shyps = may_insert_env_sorts thy env (Sorts.union rshyps sshyps),