src/Provers/Arith/assoc_fold.ML
changeset 13462 56610e2ba220
parent 12262 11ff5f47df6e
child 13480 bb72bd43c6c3
     1.1 --- a/src/Provers/Arith/assoc_fold.ML	Tue Aug 06 11:20:47 2002 +0200
     1.2 +++ b/src/Provers/Arith/assoc_fold.ML	Tue Aug 06 11:22:05 2002 +0200
     1.3 @@ -11,12 +11,12 @@
     1.4  
     1.5  signature ASSOC_FOLD_DATA =
     1.6  sig
     1.7 -  val ss		: simpset	(*basic simpset of object-logtic*)
     1.8 -  val eq_reflection	: thm		(*object-equality to meta-equality*)
     1.9 -  val sg_ref 		: Sign.sg_ref	(*the operator's signature*)
    1.10 -  val T			: typ		(*the operator's numeric type*)
    1.11 -  val plus		: term		(*the operator being folded*)
    1.12 -  val add_ac		: thm list      (*AC-rewrites for plus*)
    1.13 +  val ss                : simpset       (*basic simpset of object-logtic*)
    1.14 +  val eq_reflection     : thm           (*object-equality to meta-equality*)
    1.15 +  val sg_ref            : Sign.sg_ref   (*the operator's signature*)
    1.16 +  val T                 : typ           (*the operator's numeric type*)
    1.17 +  val plus              : term          (*the operator being folded*)
    1.18 +  val add_ac            : thm list      (*AC-rewrites for plus*)
    1.19  end;
    1.20  
    1.21  
    1.22 @@ -26,11 +26,11 @@
    1.23   val assoc_ss = Data.ss addsimps Data.add_ac;
    1.24  
    1.25   (*prove while suppressing timing information*)
    1.26 - fun prove name ct tacf = 
    1.27 + fun prove name ct tacf =
    1.28       setmp Library.timing false (prove_goalw_cterm [] ct) tacf
    1.29       handle ERROR =>
    1.30 -	 error(name ^ " simproc:\nfailed to prove " ^ string_of_cterm ct);
    1.31 -                
    1.32 +         error(name ^ " simproc:\nfailed to prove " ^ string_of_cterm ct);
    1.33 +
    1.34   exception Assoc_fail;
    1.35  
    1.36   fun mk_sum []  = raise Assoc_fail
    1.37 @@ -39,13 +39,13 @@
    1.38   (*Separate the literals from the other terms being combined*)
    1.39   fun sift_terms (t, (lits,others)) =
    1.40       case t of
    1.41 -	  Const("Numeral.number_of", _) $ _ =>
    1.42 -	      (t::lits, others)         (*new literal*)
    1.43 -	| (f as Const _) $ x $ y =>
    1.44 -	      if f = Data.plus 
    1.45 +          Const("Numeral.number_of", _) $ _ =>
    1.46 +              (t::lits, others)         (*new literal*)
    1.47 +        | (f as Const _) $ x $ y =>
    1.48 +              if f = Data.plus
    1.49                then sift_terms (x, sift_terms (y, (lits,others)))
    1.50 -	      else (lits, t::others)    (*arbitrary summand*)
    1.51 -	| _ => (lits, t::others);
    1.52 +              else (lits, t::others)    (*arbitrary summand*)
    1.53 +        | _ => (lits, t::others);
    1.54  
    1.55   val trace = ref false;
    1.56  
    1.57 @@ -53,25 +53,23 @@
    1.58   fun proc sg _ lhs =
    1.59     let fun show t = string_of_cterm (Thm.cterm_of sg t)
    1.60         val _ = if !trace then tracing ("assoc_fold simproc: LHS = " ^ show lhs)
    1.61 -	       else ()
    1.62 +               else ()
    1.63         val (lits,others) = sift_terms (lhs, ([],[]))
    1.64         val _ = if length lits < 2
    1.65                 then raise Assoc_fail (*we can't reduce the number of terms*)
    1.66 -               else ()  
    1.67 +               else ()
    1.68         val rhs = Data.plus $ mk_sum lits $ mk_sum others
    1.69         val _ = if !trace then tracing ("RHS = " ^ show rhs) else ()
    1.70 -       val th = prove "assoc_fold" 
    1.71 -	           (Thm.cterm_of sg (Logic.mk_equals (lhs, rhs)))
    1.72 -		   (fn _ => [rtac Data.eq_reflection 1,
    1.73 -			     simp_tac assoc_ss 1])
    1.74 +       val th = prove "assoc_fold"
    1.75 +                   (Thm.cterm_of sg (Logic.mk_equals (lhs, rhs)))
    1.76 +                   (fn _ => [rtac Data.eq_reflection 1,
    1.77 +                             simp_tac assoc_ss 1])
    1.78     in Some th end
    1.79     handle Assoc_fail => None;
    1.80 - 
    1.81 - val conv = 
    1.82 -     Simplifier.mk_simproc "assoc_fold"
    1.83 -       [Thm.cterm_of (Sign.deref Data.sg_ref)
    1.84 -	             (Data.plus $ Free("x",Data.T) $ Free("y",Data.T))]
    1.85 -       proc;
    1.86 +
    1.87 + val conv =
    1.88 +     Simplifier.simproc_i (Sign.deref Data.sg_ref) "assoc_fold"
    1.89 +       [Data.plus $ Free ("x", Data.T) $ Free ("y",Data.T)] proc;
    1.90  
    1.91  end;
    1.92