new files in Integ
authorpaulson
Fri Sep 18 14:39:51 1998 +0200 (1998-09-18)
changeset 5501a63e0c326e6c
parent 5500 7e0ed3e31590
child 5502 da4d0444ea85
new files in Integ
src/HOL/Integ/simproc.ML
src/HOL/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Integ/simproc.ML	Fri Sep 18 14:39:51 1998 +0200
     1.3 @@ -0,0 +1,95 @@
     1.4 +(*  Title:      HOL/Integ/simproc
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1998  University of Cambridge
     1.8 +
     1.9 +Simplification procedures for the integers
    1.10 +
    1.11 +This one cancels complementary terms in sums.  Examples:
    1.12 +   x + (y + -x)   =   x + (-x + y)  =  y
    1.13 +   -x + (y + (x + z))   =   -x + (x + (y + z))  =  y + z
    1.14 +
    1.15 +Should be used with zdiff_def (to eliminate subtraction) and zadd_ac.
    1.16 +*)
    1.17 +
    1.18 +
    1.19 +structure Int_Cancel =
    1.20 +struct
    1.21 +
    1.22 +val intT = Type ("IntDef.int", []);
    1.23 +
    1.24 +val zplus = Const ("op +", [intT,intT] ---> intT);
    1.25 +val zminus = Const ("uminus", intT --> intT);
    1.26 +
    1.27 +val ssubst_left = read_instantiate [("P", "%x. ?lhs x = ?rhs")] ssubst;
    1.28 +
    1.29 +fun inst_left_commute ct = instantiate' [] [None, Some ct] zadd_left_commute;
    1.30 +
    1.31 +(*Can LOOP, so include only if the first occurrence at the very end*)
    1.32 +fun inst_commute ct = instantiate' [] [None, Some ct] zadd_commute;
    1.33 +
    1.34 +fun terms (t as f$x$y) =
    1.35 +        if f=zplus then x :: terms y else [t]
    1.36 +  | terms t = [t];
    1.37 +
    1.38 +val mk_sum = foldr1 (fn (x,y) => zplus $ x $ y);
    1.39 +
    1.40 +(*We map -t to t and (in other cases) t to -t.  No need to check the type of
    1.41 +  uminus, since the simproc is only called on integer sums.*)
    1.42 +fun negate (Const("uminus",_) $ t) = t
    1.43 +  | negate t                       = zminus $ t;
    1.44 +
    1.45 +(*These rules eliminate the first two terms, if they cancel*)
    1.46 +val cancel_laws = [zadd_zminus_cancel, zminus_zadd_cancel];
    1.47 +
    1.48 +exception Cancel;
    1.49 +
    1.50 +(*Cancels just the first occurrence of head', leaving the rest unchanged*)
    1.51 +fun cancelled head' tail =
    1.52 +    let fun find ([], _) = raise Cancel
    1.53 +	  | find (t::ts, heads) = if head' aconv t then rev heads @ ts
    1.54 +				  else find (ts, t::heads)
    1.55 +    in  mk_sum (find (tail, []))  end;
    1.56 +
    1.57 +
    1.58 +val trace = ref false;
    1.59 +
    1.60 +fun proc sg _ lhs =
    1.61 +  let val _ = if !trace then prs ("lhs = " ^ string_of_cterm (cterm_of sg lhs))
    1.62 +              else ()
    1.63 +      val (head::tail) = terms lhs
    1.64 +      val head' = negate head
    1.65 +      val rhs = cancelled head' tail
    1.66 +      and chead' = Thm.cterm_of sg head'
    1.67 +      val comms = [inst_left_commute chead' RS ssubst_left,
    1.68 +		   inst_commute chead' RS ssubst_left]
    1.69 +      val _ = if !trace then 
    1.70 +	        writeln ("rhs = " ^ string_of_cterm (Thm.cterm_of sg rhs))
    1.71 +              else ()
    1.72 +      val ct = Thm.cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
    1.73 +      (*Simplification is much faster than substitution, but loops for terms
    1.74 +        like (x + (-x + (-x + y))).  Substitution finds the outermost -x, so
    1.75 +        is seems not to loop, and the counter prevents looping for sure.*)
    1.76 +      fun cancel_tac 0 = no_tac   
    1.77 +	| cancel_tac n = 
    1.78 +	      (resolve_tac cancel_laws 1 ORELSE
    1.79 +	       resolve_tac comms 1 THEN cancel_tac (n-1));
    1.80 +      val thm = prove_goalw_cterm [] ct 
    1.81 +	          (fn _ => [cancel_tac (length tail + 1)])
    1.82 +	handle ERROR =>
    1.83 +	error("The error(s) above occurred while trying to prove " ^
    1.84 +	      string_of_cterm ct)
    1.85 +  in Some (meta_eq thm) end
    1.86 +  handle Cancel => None;
    1.87 +
    1.88 +
    1.89 +val conv = 
    1.90 +    Simplifier.mk_simproc "cancel_sums"
    1.91 +      [Thm.read_cterm (sign_of IntDef.thy) ("x + (y + (z::int))", intT)]
    1.92 +      proc;
    1.93 +
    1.94 +end;
    1.95 +
    1.96 +
    1.97 +Addsimprocs [Int_Cancel.conv];
    1.98 +
     2.1 --- a/src/HOL/ROOT.ML	Fri Sep 18 14:39:08 1998 +0200
     2.2 +++ b/src/HOL/ROOT.ML	Fri Sep 18 14:39:51 1998 +0200
     2.3 @@ -64,6 +64,8 @@
     2.4  cd "$ISABELLE_HOME/src/HOL";
     2.5  
     2.6  cd "Integ";
     2.7 +use_thy "IntDef";
     2.8 +use     "simproc";
     2.9  use_thy "Bin";
    2.10  cd "..";
    2.11  
    2.12 @@ -72,4 +74,6 @@
    2.13  
    2.14  print_depth 8;
    2.15  
    2.16 +Goal "True";  (*leave subgoal package empty*)
    2.17 +
    2.18  val HOL_build_completed = ();   (*indicate successful build*)