loads the new simproc extract_common_term
authorpaulson
Mon Dec 18 12:21:54 2000 +0100 (2000-12-18)
changeset 106895c44de6aadf4
parent 10688 4cf4bbc25267
child 10690 cd80241125b0
loads the new simproc extract_common_term
src/HOL/ROOT.ML
src/HOL/Real/RealArith.ML
src/HOL/Real/RealBin.ML
     1.1 --- a/src/HOL/ROOT.ML	Sat Dec 16 21:43:28 2000 +0100
     1.2 +++ b/src/HOL/ROOT.ML	Mon Dec 18 12:21:54 2000 +0100
     1.3 @@ -34,6 +34,7 @@
     1.4  use "~~/src/Provers/Arith/cancel_numerals.ML";
     1.5  use "~~/src/Provers/Arith/combine_numerals.ML";
     1.6  use "~~/src/Provers/Arith/cancel_numeral_factor.ML";
     1.7 +use "~~/src/Provers/Arith/extract_common_term.ML";
     1.8  
     1.9  with_path "Integ" use_thy "Main";
    1.10  
     2.1 --- a/src/HOL/Real/RealArith.ML	Sat Dec 16 21:43:28 2000 +0100
     2.2 +++ b/src/HOL/Real/RealArith.ML	Mon Dec 18 12:21:54 2000 +0100
     2.3 @@ -208,6 +208,11 @@
     2.4  by (asm_full_simp_tac (HOL_ss addsimps real_mult_ac) 1); 
     2.5  qed "real_mult_div_cancel1";
     2.6  
     2.7 +(*For ExtractCommonTerm*)
     2.8 +Goal "(k*m) / (k*n) = (if k = (#0::real) then #0 else m/n)";
     2.9 +by (simp_tac (simpset() addsimps [real_mult_div_cancel1]) 1); 
    2.10 +qed "real_mult_div_cancel_disj";
    2.11 +
    2.12  
    2.13  local
    2.14    open Real_Numeral_Simprocs
    2.15 @@ -324,6 +329,77 @@
    2.16  test "-x <= #-23 * (y::real)";
    2.17  *)
    2.18  
    2.19 +
    2.20 +(** Declarations for ExtractCommonTerm **)
    2.21 +
    2.22 +local
    2.23 +  open Real_Numeral_Simprocs
    2.24 +in
    2.25 +
    2.26 +structure CancelFactorCommon =
    2.27 +  struct
    2.28 +  val mk_sum    	= long_mk_prod
    2.29 +  val dest_sum		= dest_prod
    2.30 +  val mk_coeff		= mk_coeff
    2.31 +  val dest_coeff	= dest_coeff
    2.32 +  val find_first	= find_first []
    2.33 +  val trans_tac         = trans_tac
    2.34 +  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@real_mult_ac))
    2.35 +  end;
    2.36 +
    2.37 +structure EqCancelFactor = ExtractCommonTermFun
    2.38 + (open CancelFactorCommon
    2.39 +  val prove_conv = prove_conv "real_eq_cancel_factor"
    2.40 +  val mk_bal   = HOLogic.mk_eq
    2.41 +  val dest_bal = HOLogic.dest_bin "op =" HOLogic.realT
    2.42 +  val simplify_meta_eq  = cancel_simplify_meta_eq real_mult_eq_cancel1
    2.43 +);
    2.44 +
    2.45 +
    2.46 +structure DivideCancelFactor = ExtractCommonTermFun
    2.47 + (open CancelFactorCommon
    2.48 +  val prove_conv = prove_conv "real_divide_cancel_factor"
    2.49 +  val mk_bal   = HOLogic.mk_binop "HOL.divide"
    2.50 +  val dest_bal = HOLogic.dest_bin "HOL.divide" HOLogic.realT
    2.51 +  val simplify_meta_eq  = cancel_simplify_meta_eq real_mult_div_cancel_disj
    2.52 +);
    2.53 +
    2.54 +val real_cancel_factor = 
    2.55 +  map prep_simproc
    2.56 +   [("real_eq_cancel_factor",
    2.57 +     prep_pats ["(l::real) * m = n", "(l::real) = m * n"], 
    2.58 +     EqCancelFactor.proc),
    2.59 +    ("real_divide_cancel_factor", 
    2.60 +     prep_pats ["((l::real) * m) / n", "(l::real) / (m * n)"], 
    2.61 +     DivideCancelFactor.proc)];
    2.62 +
    2.63 +end;
    2.64 +
    2.65 +Addsimprocs real_cancel_factor;
    2.66 +
    2.67 +
    2.68 +(*examples:
    2.69 +print_depth 22;
    2.70 +set timing;
    2.71 +set trace_simp;
    2.72 +fun test s = (Goal s; by (Asm_simp_tac 1)); 
    2.73 +
    2.74 +test "x*k = k*(y::real)";
    2.75 +test "k = k*(y::real)"; 
    2.76 +test "a*(b*c) = (b::real)";
    2.77 +test "a*(b*c) = d*(b::real)*(x*a)";
    2.78 +
    2.79 +
    2.80 +test "(x*k) / (k*(y::real)) = (uu::real)";
    2.81 +test "(k) / (k*(y::real)) = (uu::real)"; 
    2.82 +test "(a*(b*c)) / ((b::real)) = (uu::real)";
    2.83 +test "(a*(b*c)) / (d*(b::real)*(x*a)) = (uu::real)";
    2.84 +
    2.85 +(*FIXME: what do we do about this?*)
    2.86 +test "a*(b*c)/(y*z) = d*(b::real)*(x*a)/z";
    2.87 +*)
    2.88 +
    2.89 +
    2.90  (*** Simplification of inequalities involving literal divisors ***)
    2.91  
    2.92  Goal "#0<z ==> ((x::real) <= y/z) = (x*z <= y)";
     3.1 --- a/src/HOL/Real/RealBin.ML	Sat Dec 16 21:43:28 2000 +0100
     3.2 +++ b/src/HOL/Real/RealBin.ML	Mon Dec 18 12:21:54 2000 +0100
     3.3 @@ -485,6 +485,26 @@
     3.4  		  prep_pats ["(i::real) + j", "(i::real) - j"],
     3.5  		  CombineNumerals.proc);
     3.6  
     3.7 +
     3.8 +(** Declarations for ExtractCommonTerm **)
     3.9 +
    3.10 +(*this version ALWAYS includes a trailing one*)
    3.11 +fun long_mk_prod []        = one
    3.12 +  | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);
    3.13 +
    3.14 +(*Find first term that matches u*)
    3.15 +fun find_first past u []         = raise TERM("find_first", []) 
    3.16 +  | find_first past u (t::terms) =
    3.17 +	if u aconv t then (rev past @ terms)
    3.18 +        else find_first (t::past) u terms
    3.19 +	handle TERM _ => find_first (t::past) u terms;
    3.20 +
    3.21 +(*Final simplification: cancel + and *  *)
    3.22 +fun cancel_simplify_meta_eq cancel_th th = 
    3.23 +    Int_Numeral_Simprocs.simplify_meta_eq 
    3.24 +        [real_mult_1, real_mult_1_right] 
    3.25 +        (([th, cancel_th]) MRS trans);
    3.26 +
    3.27  end;
    3.28  
    3.29