prove_conv gets an extra argument, so the ZF instantiation can use hyps
authorpaulson
Mon Aug 07 10:28:32 2000 +0200 (2000-08-07)
changeset 9546be095014e72f
parent 9545 c1d9500e2927
child 9547 8dad21f06b24
prove_conv gets an extra argument, so the ZF instantiation can use hyps
src/Provers/Arith/cancel_numerals.ML
     1.1 --- a/src/Provers/Arith/cancel_numerals.ML	Mon Aug 07 10:27:35 2000 +0200
     1.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Mon Aug 07 10:28:32 2000 +0200
     1.3 @@ -36,7 +36,8 @@
     1.4    val bal_add1: thm
     1.5    val bal_add2: thm
     1.6    (*proof tools*)
     1.7 -  val prove_conv: tactic list -> Sign.sg -> term * term -> thm option
     1.8 +  val prove_conv: tactic list -> Sign.sg -> 
     1.9 +                  thm list -> term * term -> thm option
    1.10    val trans_tac: thm option -> tactic (*applies the initial lemma*)
    1.11    val norm_tac: tactic                (*proves the initial lemma*)
    1.12    val numeral_simp_tac: tactic        (*proves the final theorem*)
    1.13 @@ -68,7 +69,7 @@
    1.14    in  seek terms1 end;
    1.15  
    1.16  (*the simplification procedure*)
    1.17 -fun proc sg _ t =
    1.18 +fun proc sg hyps t =
    1.19    let (*first freeze any Vars in the term to prevent flex-flex problems*)
    1.20        val rand_s = gensym"_"
    1.21        fun mk_inst (var as Var((a,i),T))  = 
    1.22 @@ -85,7 +86,7 @@
    1.23  		       i + #m + j + k == #m + i + (j + k) *)
    1.24  	    if n1=0 orelse n2=0 then   (*trivial, so do nothing*)
    1.25  		raise TERM("cancel_numerals", []) 
    1.26 -	    else Data.prove_conv [Data.norm_tac] sg 
    1.27 +	    else Data.prove_conv [Data.norm_tac] sg hyps
    1.28  			(t', 
    1.29  			 Data.mk_bal (newshape(n1,terms1'), 
    1.30  				      newshape(n2,terms2')))
    1.31 @@ -94,13 +95,13 @@
    1.32         (if n2<=n1 then 
    1.33  	    Data.prove_conv 
    1.34  	       [Data.trans_tac reshape, rtac Data.bal_add1 1,
    1.35 -		Data.numeral_simp_tac] sg
    1.36 +		Data.numeral_simp_tac] sg hyps
    1.37  	       (t', Data.mk_bal (newshape(n1-n2,terms1'), 
    1.38  				 Data.mk_sum terms2'))
    1.39  	else
    1.40  	    Data.prove_conv 
    1.41  	       [Data.trans_tac reshape, rtac Data.bal_add2 1,
    1.42 -		Data.numeral_simp_tac] sg
    1.43 +		Data.numeral_simp_tac] sg hyps
    1.44  	       (t', Data.mk_bal (Data.mk_sum terms1', 
    1.45  				 newshape(n2-n1,terms2'))))
    1.46    end