src/Provers/Arith/cancel_numerals.ML
changeset 17223 430edc6b7826
parent 16973 b2a894562b8f
child 17412 e26cb20ef0cc
     1.1 --- a/src/Provers/Arith/cancel_numerals.ML	Thu Sep 01 18:48:54 2005 +0200
     1.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Thu Sep 01 22:15:10 2005 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  
     1.5  It works by (a) massaging both sides to bring the selected term to the front:
     1.6  
     1.7 -     #m*u + (i + j) ~~ #m'*u + (i' + j') 
     1.8 +     #m*u + (i + j) ~~ #m'*u + (i' + j')
     1.9  
    1.10  (b) then using bal_add1 or bal_add2 to reach
    1.11  
    1.12 @@ -36,7 +36,7 @@
    1.13    val bal_add1: thm
    1.14    val bal_add2: thm
    1.15    (*proof tools*)
    1.16 -  val prove_conv: tactic list -> theory -> 
    1.17 +  val prove_conv: tactic list -> theory ->
    1.18                    thm list -> string list -> term * term -> thm option
    1.19    val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
    1.20    val norm_tac: simpset -> tactic                (*proves the initial lemma*)
    1.21 @@ -48,24 +48,22 @@
    1.22  functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA):
    1.23    sig
    1.24    val proc: theory -> simpset -> term -> thm option
    1.25 -  end 
    1.26 +  end
    1.27  =
    1.28  struct
    1.29  
    1.30  (*For t = #n*u then put u in the table*)
    1.31 -fun update_by_coeff (tab, t) =
    1.32 -  Termtab.update ((#2 (Data.dest_coeff t), ()), tab);
    1.33 +fun update_by_coeff t =
    1.34 +  Termtab.curried_update (#2 (Data.dest_coeff t), ());
    1.35  
    1.36  (*a left-to-right scan of terms1, seeking a term of the form #n*u, where
    1.37    #m*u is in terms2 for some m*)
    1.38  fun find_common (terms1,terms2) =
    1.39 -  let val tab2 = Library.foldl update_by_coeff (Termtab.empty, terms2)
    1.40 -      fun seek [] = raise TERM("find_common", []) 
    1.41 -	| seek (t::terms) =
    1.42 -	      let val (_,u) = Data.dest_coeff t 
    1.43 -	      in  if isSome (Termtab.lookup (tab2, u)) then u
    1.44 -		  else seek terms
    1.45 -	      end
    1.46 +  let val tab2 = fold update_by_coeff terms2 Termtab.empty
    1.47 +      fun seek [] = raise TERM("find_common", [])
    1.48 +        | seek (t::terms) =
    1.49 +              let val (_,u) = Data.dest_coeff t
    1.50 +              in if Termtab.defined tab2 u then u else seek terms end
    1.51    in  seek terms1 end;
    1.52  
    1.53  (*the simplification procedure*)
    1.54 @@ -74,7 +72,7 @@
    1.55        val hyps = prems_of_ss ss;
    1.56        (*first freeze any Vars in the term to prevent flex-flex problems*)
    1.57        val (t', xs) = Term.adhoc_freeze_vars t;
    1.58 -      val (t1,t2) = Data.dest_bal t' 
    1.59 +      val (t1,t2) = Data.dest_bal t'
    1.60        val terms1 = Data.dest_sum t1
    1.61        and terms2 = Data.dest_sum t2
    1.62        val u = find_common (terms1,terms2)
    1.63 @@ -83,30 +81,30 @@
    1.64        and T = Term.fastype_of u
    1.65        fun newshape (i,terms) = Data.mk_sum T (Data.mk_coeff(i,u)::terms)
    1.66        val reshape =  (*Move i*u to the front and put j*u into standard form
    1.67 -		       i + #m + j + k == #m + i + (j + k) *)
    1.68 -	    if n1=0 orelse n2=0 then   (*trivial, so do nothing*)
    1.69 -		raise TERM("cancel_numerals", []) 
    1.70 -	    else Data.prove_conv [Data.norm_tac ss] thy hyps xs
    1.71 -			(t', 
    1.72 -			 Data.mk_bal (newshape(n1,terms1'), 
    1.73 -				      newshape(n2,terms2')))
    1.74 +                       i + #m + j + k == #m + i + (j + k) *)
    1.75 +            if n1=0 orelse n2=0 then   (*trivial, so do nothing*)
    1.76 +                raise TERM("cancel_numerals", [])
    1.77 +            else Data.prove_conv [Data.norm_tac ss] thy hyps xs
    1.78 +                        (t',
    1.79 +                         Data.mk_bal (newshape(n1,terms1'),
    1.80 +                                      newshape(n2,terms2')))
    1.81    in
    1.82        Option.map (Data.simplify_meta_eq ss)
    1.83 -       (if n2<=n1 then 
    1.84 -	    Data.prove_conv 
    1.85 -	       [Data.trans_tac ss reshape, rtac Data.bal_add1 1,
    1.86 -		Data.numeral_simp_tac ss] thy hyps xs
    1.87 -	       (t', Data.mk_bal (newshape(n1-n2,terms1'), 
    1.88 -				 Data.mk_sum T terms2'))
    1.89 -	else
    1.90 -	    Data.prove_conv 
    1.91 -	       [Data.trans_tac ss reshape, rtac Data.bal_add2 1,
    1.92 -		Data.numeral_simp_tac ss] thy hyps xs
    1.93 -	       (t', Data.mk_bal (Data.mk_sum T terms1', 
    1.94 -				 newshape(n2-n1,terms2'))))
    1.95 +       (if n2<=n1 then
    1.96 +            Data.prove_conv
    1.97 +               [Data.trans_tac ss reshape, rtac Data.bal_add1 1,
    1.98 +                Data.numeral_simp_tac ss] thy hyps xs
    1.99 +               (t', Data.mk_bal (newshape(n1-n2,terms1'),
   1.100 +                                 Data.mk_sum T terms2'))
   1.101 +        else
   1.102 +            Data.prove_conv
   1.103 +               [Data.trans_tac ss reshape, rtac Data.bal_add2 1,
   1.104 +                Data.numeral_simp_tac ss] thy hyps xs
   1.105 +               (t', Data.mk_bal (Data.mk_sum T terms1',
   1.106 +                                 newshape(n2-n1,terms2'))))
   1.107    end
   1.108    handle TERM _ => NONE
   1.109         | TYPE _ => NONE;   (*Typically (if thy doesn't include Numeral)
   1.110 -			     Undeclared type constructor "Numeral.bin"*)
   1.111 +                             Undeclared type constructor "Numeral.bin"*)
   1.112  
   1.113  end;