src/Provers/Arith/cancel_numerals.ML
changeset 16973 b2a894562b8f
parent 15965 f422f8283491
child 17223 430edc6b7826
     1.1 --- a/src/Provers/Arith/cancel_numerals.ML	Mon Aug 01 19:20:25 2005 +0200
     1.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Mon Aug 01 19:20:26 2005 +0200
     1.3 @@ -36,18 +36,18 @@
     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 -> 
     1.8 +  val prove_conv: tactic list -> theory -> 
     1.9                    thm list -> string 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 -  val simplify_meta_eq: thm -> thm    (*simplifies the final theorem*)
    1.14 +  val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
    1.15 +  val norm_tac: simpset -> tactic                (*proves the initial lemma*)
    1.16 +  val numeral_simp_tac: simpset -> tactic        (*proves the final theorem*)
    1.17 +  val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the final theorem*)
    1.18  end;
    1.19  
    1.20  
    1.21  functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA):
    1.22    sig
    1.23 -  val proc: Sign.sg -> simpset -> term -> thm option
    1.24 +  val proc: theory -> simpset -> term -> thm option
    1.25    end 
    1.26  =
    1.27  struct
    1.28 @@ -69,7 +69,7 @@
    1.29    in  seek terms1 end;
    1.30  
    1.31  (*the simplification procedure*)
    1.32 -fun proc sg ss t =
    1.33 +fun proc thy ss t =
    1.34    let
    1.35        val hyps = prems_of_ss ss;
    1.36        (*first freeze any Vars in the term to prevent flex-flex problems*)
    1.37 @@ -86,22 +86,22 @@
    1.38  		       i + #m + j + k == #m + i + (j + k) *)
    1.39  	    if n1=0 orelse n2=0 then   (*trivial, so do nothing*)
    1.40  		raise TERM("cancel_numerals", []) 
    1.41 -	    else Data.prove_conv [Data.norm_tac] sg hyps xs
    1.42 +	    else Data.prove_conv [Data.norm_tac ss] thy hyps xs
    1.43  			(t', 
    1.44  			 Data.mk_bal (newshape(n1,terms1'), 
    1.45  				      newshape(n2,terms2')))
    1.46    in
    1.47 -      Option.map Data.simplify_meta_eq
    1.48 +      Option.map (Data.simplify_meta_eq ss)
    1.49         (if n2<=n1 then 
    1.50  	    Data.prove_conv 
    1.51 -	       [Data.trans_tac reshape, rtac Data.bal_add1 1,
    1.52 -		Data.numeral_simp_tac] sg hyps xs
    1.53 +	       [Data.trans_tac ss reshape, rtac Data.bal_add1 1,
    1.54 +		Data.numeral_simp_tac ss] thy hyps xs
    1.55  	       (t', Data.mk_bal (newshape(n1-n2,terms1'), 
    1.56  				 Data.mk_sum T terms2'))
    1.57  	else
    1.58  	    Data.prove_conv 
    1.59 -	       [Data.trans_tac reshape, rtac Data.bal_add2 1,
    1.60 -		Data.numeral_simp_tac] sg hyps xs
    1.61 +	       [Data.trans_tac ss reshape, rtac Data.bal_add2 1,
    1.62 +		Data.numeral_simp_tac ss] thy hyps xs
    1.63  	       (t', Data.mk_bal (Data.mk_sum T terms1', 
    1.64  				 newshape(n2-n1,terms2'))))
    1.65    end