4295

1 
(* Title: HOL/arith_data.ML


2 
ID: $Id$


3 
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen


4 


5 
Setup various arithmetic proof procedures.


6 
*)


7 


8 
signature ARITH_DATA =


9 
sig

4309

10 
val nat_cancel_sums: simproc list


11 
val nat_cancel_factor: simproc list

4295

12 
val nat_cancel: simproc list


13 
end;


14 

4309

15 
structure ArithData: ARITH_DATA =

4295

16 
struct


17 


18 


19 
(** abstract syntax of structure nat: 0, Suc, + **)


20 

4310

21 
(* mk_sum, mk_norm_sum *)

4295

22 

4310

23 
val one = HOLogic.mk_nat 1;

4295

24 
val mk_plus = HOLogic.mk_binop "op +";


25 


26 
fun mk_sum [] = HOLogic.zero


27 
 mk_sum [t] = t


28 
 mk_sum (t :: ts) = mk_plus (t, mk_sum ts);


29 

4310

30 
(*normal form of sums: Suc (... (Suc (a + (b + ...))))*)


31 
fun mk_norm_sum ts =


32 
let val (ones, sums) = partition (equal one) ts in


33 
funpow (length ones) HOLogic.mk_Suc (mk_sum sums)


34 
end;


35 

4295

36 


37 
(* dest_sum *)


38 


39 
val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;


40 


41 
fun dest_sum tm =


42 
if HOLogic.is_zero tm then []


43 
else


44 
(case try HOLogic.dest_Suc tm of


45 
Some t => one :: dest_sum t


46 
 None =>


47 
(case try dest_plus tm of


48 
Some (t, u) => dest_sum t @ dest_sum u


49 
 None => [tm]));


50 


51 


52 
(** generic proof tools **)


53 


54 
(* prove conversions *)


55 


56 
val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;


57 


58 
fun prove_conv expand_tac norm_tac sg (t, u) =


59 
mk_meta_eq (prove_goalw_cterm [] (cterm_of sg (mk_eqv (t, u)))


60 
(K [expand_tac, norm_tac]))


61 
handle ERROR => error ("The error(s) above occurred while trying to prove " ^


62 
(string_of_cterm (cterm_of sg (mk_eqv (t, u)))));


63 


64 
val subst_equals = prove_goal HOL.thy "[ t = s; u = t ] ==> u = s"


65 
(fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]);


66 


67 


68 
(* rewriting *)


69 


70 
fun simp_all rules = ALLGOALS (simp_tac (HOL_ss addsimps rules));


71 


72 
val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right];


73 
val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right];


74 


75 


76 


77 
(** cancel common summands **)


78 


79 
structure Sum =


80 
struct

4310

81 
val mk_sum = mk_norm_sum;

4295

82 
val dest_sum = dest_sum;


83 
val prove_conv = prove_conv;


84 
val norm_tac = simp_all add_rules THEN simp_all add_ac;


85 
end;


86 


87 
fun gen_uncancel_tac rule ct =


88 
rtac (instantiate' [] [None, Some ct] (rule RS subst_equals)) 1;


89 


90 


91 
(* nat eq *)


92 


93 
structure EqCancelSums = CancelSumsFun


94 
(struct


95 
open Sum;


96 
val mk_bal = HOLogic.mk_eq;


97 
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;


98 
val uncancel_tac = gen_uncancel_tac add_left_cancel;


99 
end);


100 


101 


102 
(* nat less *)


103 


104 
structure LessCancelSums = CancelSumsFun


105 
(struct


106 
open Sum;


107 
val mk_bal = HOLogic.mk_binrel "op <";


108 
val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;


109 
val uncancel_tac = gen_uncancel_tac add_left_cancel_less;


110 
end);


111 


112 


113 
(* nat le *)


114 


115 
structure LeCancelSums = CancelSumsFun


116 
(struct


117 
open Sum;


118 
val mk_bal = HOLogic.mk_binrel "op <=";


119 
val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;


120 
val uncancel_tac = gen_uncancel_tac add_left_cancel_le;


121 
end);


122 


123 


124 
(* nat diff *)


125 

4332

126 
structure DiffCancelSums = CancelSumsFun


127 
(struct


128 
open Sum;


129 
val mk_bal = HOLogic.mk_binop "op ";


130 
val dest_bal = HOLogic.dest_bin "op " HOLogic.natT;


131 
val uncancel_tac = gen_uncancel_tac diff_cancel;


132 
end);

4295

133 


134 


135 


136 
(** cancel common factor **)


137 


138 
structure Factor =


139 
struct

4310

140 
val mk_sum = mk_norm_sum;

4295

141 
val dest_sum = dest_sum;


142 
val prove_conv = prove_conv;


143 
val norm_tac = simp_all (add_rules @ mult_rules) THEN simp_all add_ac;


144 
end;


145 


146 
fun mk_cnat n = cterm_of (sign_of Nat.thy) (HOLogic.mk_nat n);


147 


148 
fun gen_multiply_tac rule k =


149 
if k > 0 then


150 
rtac (instantiate' [] [None, Some (mk_cnat (k  1))] (rule RS subst_equals)) 1


151 
else no_tac;


152 


153 


154 
(* nat eq *)


155 


156 
structure EqCancelFactor = CancelFactorFun


157 
(struct


158 
open Factor;


159 
val mk_bal = HOLogic.mk_eq;


160 
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;


161 
val multiply_tac = gen_multiply_tac Suc_mult_cancel1;


162 
end);


163 


164 


165 
(* nat less *)


166 


167 
structure LessCancelFactor = CancelFactorFun


168 
(struct


169 
open Factor;


170 
val mk_bal = HOLogic.mk_binrel "op <";


171 
val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;


172 
val multiply_tac = gen_multiply_tac Suc_mult_less_cancel1;


173 
end);


174 


175 


176 
(* nat le *)


177 


178 
structure LeCancelFactor = CancelFactorFun


179 
(struct


180 
open Factor;


181 
val mk_bal = HOLogic.mk_binrel "op <=";


182 
val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;


183 
val multiply_tac = gen_multiply_tac Suc_mult_le_cancel1;


184 
end);


185 


186 


187 


188 
(** prepare nat_cancel simprocs **)


189 


190 
fun prep_pat s = Thm.read_cterm (sign_of Arith.thy) (s, HOLogic.termTVar);


191 
val prep_pats = map prep_pat;


192 


193 
fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;


194 


195 
val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"];


196 
val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"];


197 
val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"];

4332

198 
val diff_pats = prep_pats ["((l::nat) + m)  n", "(l::nat)  (m + n)", "Suc m  n", "m  Suc n"];

4295

199 

4309

200 
val nat_cancel_sums = map prep_simproc


201 
[("nateq_cancel_sums", eq_pats, EqCancelSums.proc),

4295

202 
("natless_cancel_sums", less_pats, LessCancelSums.proc),

4332

203 
("natle_cancel_sums", le_pats, LeCancelSums.proc),


204 
("natdiff_cancel_sums", diff_pats, DiffCancelSums.proc)];

4295

205 

4309

206 
val nat_cancel_factor = map prep_simproc


207 
[("nateq_cancel_factor", eq_pats, EqCancelFactor.proc),


208 
("natless_cancel_factor", less_pats, LessCancelFactor.proc),


209 
("natle_cancel_factor", le_pats, LeCancelFactor.proc)];


210 


211 
val nat_cancel = nat_cancel_factor @ nat_cancel_sums;


212 

4295

213 


214 
end;

4336

215 


216 


217 
open ArithData;
