src/HOL/Integ/int_factor_simprocs.ML
changeset 13462 56610e2ba220
parent 12018 ec054019c910
child 13485 acf39e924091
     1.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Tue Aug 06 11:20:47 2002 +0200
     1.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Tue Aug 06 11:22:05 2002 +0200
     1.3 @@ -12,26 +12,26 @@
     1.4  
     1.5  Goal "!!k::int. (k*m <= k*n) = ((0 < k --> m<=n) & (k < 0 --> n<=m))";
     1.6  by (stac zmult_zle_cancel1 1);
     1.7 -by Auto_tac;  
     1.8 +by Auto_tac;
     1.9  qed "int_mult_le_cancel1";
    1.10  
    1.11  Goal "!!k::int. (k*m < k*n) = ((0 < k & m<n) | (k < 0 & n<m))";
    1.12  by (stac zmult_zless_cancel1 1);
    1.13 -by Auto_tac;  
    1.14 +by Auto_tac;
    1.15  qed "int_mult_less_cancel1";
    1.16  
    1.17  Goal "!!k::int. (k*m = k*n) = (k = 0 | m=n)";
    1.18 -by Auto_tac;  
    1.19 +by Auto_tac;
    1.20  qed "int_mult_eq_cancel1";
    1.21  
    1.22  Goal "!!k::int. k~=0 ==> (k*m) div (k*n) = (m div n)";
    1.23 -by (stac zdiv_zmult_zmult1 1); 
    1.24 -by Auto_tac;  
    1.25 +by (stac zdiv_zmult_zmult1 1);
    1.26 +by Auto_tac;
    1.27  qed "int_mult_div_cancel1";
    1.28  
    1.29  (*For ExtractCommonTermFun, cancelling common factors*)
    1.30  Goal "(k*m) div (k*n) = (if k = (0::int) then 0 else m div n)";
    1.31 -by (simp_tac (simpset() addsimps [int_mult_div_cancel1]) 1); 
    1.32 +by (simp_tac (simpset() addsimps [int_mult_div_cancel1]) 1);
    1.33  qed "int_mult_div_cancel_disj";
    1.34  
    1.35  local
    1.36 @@ -40,15 +40,15 @@
    1.37  
    1.38  structure CancelNumeralFactorCommon =
    1.39    struct
    1.40 -  val mk_coeff		= mk_coeff
    1.41 -  val dest_coeff	= dest_coeff 1
    1.42 +  val mk_coeff          = mk_coeff
    1.43 +  val dest_coeff        = dest_coeff 1
    1.44    val trans_tac         = trans_tac
    1.45 -  val norm_tac = 
    1.46 +  val norm_tac =
    1.47       ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@mult_1s))
    1.48       THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps))
    1.49       THEN ALLGOALS
    1.50              (simp_tac (HOL_ss addsimps zmult_ac))
    1.51 -  val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
    1.52 +  val numeral_simp_tac  = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
    1.53    val simplify_meta_eq  = simplify_meta_eq mult_1s
    1.54    end
    1.55  
    1.56 @@ -88,19 +88,15 @@
    1.57    val neg_exchanges = true
    1.58  )
    1.59  
    1.60 -val int_cancel_numeral_factors = 
    1.61 +val int_cancel_numeral_factors =
    1.62    map Bin_Simprocs.prep_simproc
    1.63 -   [("inteq_cancel_numeral_factors",
    1.64 -     Bin_Simprocs.prep_pats ["(l::int) * m = n", "(l::int) = m * n"], 
    1.65 +   [("inteq_cancel_numeral_factors", ["(l::int) * m = n", "(l::int) = m * n"],
    1.66       EqCancelNumeralFactor.proc),
    1.67 -    ("intless_cancel_numeral_factors", 
    1.68 -     Bin_Simprocs.prep_pats ["(l::int) * m < n", "(l::int) < m * n"], 
    1.69 +    ("intless_cancel_numeral_factors", ["(l::int) * m < n", "(l::int) < m * n"],
    1.70       LessCancelNumeralFactor.proc),
    1.71 -    ("intle_cancel_numeral_factors", 
    1.72 -     Bin_Simprocs.prep_pats ["(l::int) * m <= n", "(l::int) <= m * n"], 
    1.73 +    ("intle_cancel_numeral_factors", ["(l::int) * m <= n", "(l::int) <= m * n"],
    1.74       LeCancelNumeralFactor.proc),
    1.75 -    ("intdiv_cancel_numeral_factors", 
    1.76 -     Bin_Simprocs.prep_pats ["((l::int) * m) div n", "(l::int) div (m * n)"], 
    1.77 +    ("intdiv_cancel_numeral_factors", ["((l::int) * m) div n", "(l::int) div (m * n)"],
    1.78       DivCancelNumeralFactor.proc)];
    1.79  
    1.80  end;
    1.81 @@ -112,7 +108,7 @@
    1.82  print_depth 22;
    1.83  set timing;
    1.84  set trace_simp;
    1.85 -fun test s = (Goal s; by (Simp_tac 1)); 
    1.86 +fun test s = (Goal s; by (Simp_tac 1));
    1.87  
    1.88  test "9*x = 12 * (y::int)";
    1.89  test "(9*x) div (12 * (y::int)) = z";
    1.90 @@ -156,25 +152,25 @@
    1.91    | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);
    1.92  
    1.93  (*Find first term that matches u*)
    1.94 -fun find_first past u []         = raise TERM("find_first", []) 
    1.95 +fun find_first past u []         = raise TERM("find_first", [])
    1.96    | find_first past u (t::terms) =
    1.97 -	if u aconv t then (rev past @ terms)
    1.98 +        if u aconv t then (rev past @ terms)
    1.99          else find_first (t::past) u terms
   1.100 -	handle TERM _ => find_first (t::past) u terms;
   1.101 +        handle TERM _ => find_first (t::past) u terms;
   1.102  
   1.103  (*Final simplification: cancel + and *  *)
   1.104 -fun cancel_simplify_meta_eq cancel_th th = 
   1.105 -    Int_Numeral_Simprocs.simplify_meta_eq 
   1.106 -        [zmult_1, zmult_1_right] 
   1.107 +fun cancel_simplify_meta_eq cancel_th th =
   1.108 +    Int_Numeral_Simprocs.simplify_meta_eq
   1.109 +        [zmult_1, zmult_1_right]
   1.110          (([th, cancel_th]) MRS trans);
   1.111  
   1.112  structure CancelFactorCommon =
   1.113    struct
   1.114 -  val mk_sum    	= long_mk_prod
   1.115 -  val dest_sum		= dest_prod
   1.116 -  val mk_coeff		= mk_coeff
   1.117 -  val dest_coeff	= dest_coeff
   1.118 -  val find_first	= find_first []
   1.119 +  val mk_sum            = long_mk_prod
   1.120 +  val dest_sum          = dest_prod
   1.121 +  val mk_coeff          = mk_coeff
   1.122 +  val dest_coeff        = dest_coeff
   1.123 +  val find_first        = find_first []
   1.124    val trans_tac         = trans_tac
   1.125    val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@zmult_ac))
   1.126    end;
   1.127 @@ -195,13 +191,10 @@
   1.128    val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_div_cancel_disj
   1.129  );
   1.130  
   1.131 -val int_cancel_factor = 
   1.132 +val int_cancel_factor =
   1.133    map Bin_Simprocs.prep_simproc
   1.134 -   [("int_eq_cancel_factor",
   1.135 -     Bin_Simprocs.prep_pats ["(l::int) * m = n", "(l::int) = m * n"], 
   1.136 -     EqCancelFactor.proc),
   1.137 -    ("int_divide_cancel_factor", 
   1.138 -     Bin_Simprocs.prep_pats ["((l::int) * m) div n", "(l::int) div (m * n)"], 
   1.139 +   [("int_eq_cancel_factor", ["(l::int) * m = n", "(l::int) = m * n"], EqCancelFactor.proc),
   1.140 +    ("int_divide_cancel_factor", ["((l::int) * m) div n", "(l::int) div (m * n)"],
   1.141       DivideCancelFactor.proc)];
   1.142  
   1.143  end;
   1.144 @@ -213,15 +206,15 @@
   1.145  print_depth 22;
   1.146  set timing;
   1.147  set trace_simp;
   1.148 -fun test s = (Goal s; by (Asm_simp_tac 1)); 
   1.149 +fun test s = (Goal s; by (Asm_simp_tac 1));
   1.150  
   1.151  test "x*k = k*(y::int)";
   1.152 -test "k = k*(y::int)"; 
   1.153 +test "k = k*(y::int)";
   1.154  test "a*(b*c) = (b::int)";
   1.155  test "a*(b*c) = d*(b::int)*(x*a)";
   1.156  
   1.157  test "(x*k) div (k*(y::int)) = (uu::int)";
   1.158 -test "(k) div (k*(y::int)) = (uu::int)"; 
   1.159 +test "(k) div (k*(y::int)) = (uu::int)";
   1.160  test "(a*(b*c)) div ((b::int)) = (uu::int)";
   1.161  test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)";
   1.162  *)