now freezes Vars in order to prevent errors in cases like these:
authorpaulson
Thu Jun 29 16:50:52 2000 +0200 (2000-06-29)
changeset 9191300bd596d696
parent 9190 b86ff604729f
child 9192 df32cd0881b9
now freezes Vars in order to prevent errors in cases like these:

Goal "Suc (x + i + j) + ?q ?ii ?jj + k + x = xxx";
Goal "Suc (x + i + j) = x + f(?q i j) + k";
Goal "Suc (x + i + j) = x + ?q i j + k";
Goal "Suc (?q ?ii ?jj + i + j) + ?rq ?ii ?jj + k + ?q ?ii ?jj = xxx";
src/Provers/Arith/cancel_numerals.ML
src/Provers/Arith/combine_numerals.ML
     1.1 --- a/src/Provers/Arith/cancel_numerals.ML	Thu Jun 29 12:19:27 2000 +0200
     1.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Thu Jun 29 16:50:52 2000 +0200
     1.3 @@ -69,7 +69,12 @@
     1.4  
     1.5  (*the simplification procedure*)
     1.6  fun proc sg _ t =
     1.7 -  let val (t1,t2) = Data.dest_bal t 
     1.8 +  let (*first freeze any Vars in the term to prevent flex-flex problems*)
     1.9 +      val rand_s = gensym"_"
    1.10 +      fun mk_inst (var as Var((a,i),T))  = 
    1.11 +	    (var,  Free((a ^ rand_s ^ string_of_int i), T))
    1.12 +      val t' = subst_atomic (map mk_inst (term_vars t)) t
    1.13 +      val (t1,t2) = Data.dest_bal t' 
    1.14        val terms1 = Data.dest_sum t1
    1.15        and terms2 = Data.dest_sum t2
    1.16        val u = find_common (terms1,terms2)
    1.17 @@ -81,22 +86,23 @@
    1.18  	    if n1=0 orelse n2=0 then   (*trivial, so do nothing*)
    1.19  		raise TERM("cancel_numerals", []) 
    1.20  	    else Data.prove_conv [Data.norm_tac] sg 
    1.21 -			(t, 
    1.22 +			(t', 
    1.23  			 Data.mk_bal (newshape(n1,terms1'), 
    1.24  				      newshape(n2,terms2')))
    1.25    in
    1.26 -
    1.27        apsome Data.simplify_meta_eq
    1.28         (if n2<=n1 then 
    1.29  	    Data.prove_conv 
    1.30  	       [Data.trans_tac reshape, rtac Data.bal_add1 1,
    1.31  		Data.numeral_simp_tac] sg
    1.32 -	       (t, Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum terms2'))
    1.33 +	       (t', Data.mk_bal (newshape(n1-n2,terms1'), 
    1.34 +				 Data.mk_sum terms2'))
    1.35  	else
    1.36  	    Data.prove_conv 
    1.37  	       [Data.trans_tac reshape, rtac Data.bal_add2 1,
    1.38  		Data.numeral_simp_tac] sg
    1.39 -	       (t, Data.mk_bal (Data.mk_sum terms1', newshape(n2-n1,terms2'))))
    1.40 +	       (t', Data.mk_bal (Data.mk_sum terms1', 
    1.41 +				 newshape(n2-n1,terms2'))))
    1.42    end
    1.43    handle TERM _ => None
    1.44         | TYPE _ => None;   (*Typically (if thy doesn't include Numeral)
     2.1 --- a/src/Provers/Arith/combine_numerals.ML	Thu Jun 29 12:19:27 2000 +0200
     2.2 +++ b/src/Provers/Arith/combine_numerals.ML	Thu Jun 29 16:50:52 2000 +0200
     2.3 @@ -64,13 +64,18 @@
     2.4  
     2.5  (*the simplification procedure*)
     2.6  fun proc sg _ t =
     2.7 -  let val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t)
     2.8 +  let (*first freeze any Vars in the term to prevent flex-flex problems*)
     2.9 +      val rand_s = gensym"_"
    2.10 +      fun mk_inst (var as Var((a,i),T))  = 
    2.11 +	    (var,  Free((a ^ rand_s ^ string_of_int i), T))
    2.12 +      val t' = subst_atomic (map mk_inst (term_vars t)) t
    2.13 +      val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')
    2.14        val reshape =  (*Move i*u to the front and put j*u into standard form
    2.15  		       i + #m + j + k == #m + i + (j + k) *)
    2.16  	    if m=0 orelse n=0 then   (*trivial, so do nothing*)
    2.17  		raise TERM("combine_numerals", []) 
    2.18  	    else Data.prove_conv [Data.norm_tac] sg 
    2.19 -			(t, 
    2.20 +			(t', 
    2.21  			 Data.mk_sum ([Data.mk_coeff(m,u),
    2.22  				       Data.mk_coeff(n,u)] @ terms))
    2.23    in
    2.24 @@ -78,7 +83,7 @@
    2.25  	 (Data.prove_conv 
    2.26  	    [Data.trans_tac reshape, rtac Data.left_distrib 1,
    2.27  	     Data.numeral_simp_tac] sg
    2.28 -	    (t, Data.mk_sum (Data.mk_coeff(m+n,u) :: terms)))
    2.29 +	    (t', Data.mk_sum (Data.mk_coeff(m+n,u) :: terms)))
    2.30    end
    2.31    handle TERM _ => None
    2.32         | TYPE _ => None;   (*Typically (if thy doesn't include Numeral)