src/Provers/Arith/cancel_numerals.ML
 changeset 9546 be095014e72f parent 9191 300bd596d696 child 13484 d8f5d3391766
```     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.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
```