1 (* Author: Mathias Fleury, MPII |
|
2 |
|
3 |
|
4 Datatructure for the cancelation simprocs for multisets, based on Larry Paulson's simprocs for |
|
5 natural numbers and numerals. |
|
6 *) |
|
7 signature MULTISET_CANCEL_COMMON = |
|
8 sig |
|
9 val mk_sum : typ -> term list -> term |
|
10 val dest_sum : term -> term list |
|
11 val mk_coeff : int * term -> term |
|
12 val dest_coeff : term -> int * term |
|
13 val find_first_coeff : term -> term list -> int * term list |
|
14 val trans_tac : Proof.context -> thm option -> tactic |
|
15 |
|
16 val norm_ss1 : simpset |
|
17 val norm_ss2: simpset |
|
18 val norm_tac: Proof.context -> tactic |
|
19 |
|
20 val numeral_simp_tac : Proof.context -> tactic |
|
21 val simplify_meta_eq : Proof.context -> thm -> thm |
|
22 val prove_conv : tactic list -> Proof.context -> thm list -> term * term -> thm option |
|
23 end; |
|
24 |
|
25 structure Multiset_Cancel_Common : MULTISET_CANCEL_COMMON = |
|
26 struct |
|
27 |
|
28 (*** Utilities ***) |
|
29 |
|
30 (*No reordering of the arguments.*) |
|
31 fun fast_mk_repeat_mset (n, mset) = |
|
32 let val T = fastype_of mset in |
|
33 Const (@{const_name "repeat_mset"}, @{typ nat} --> T --> T) $ n $ mset |
|
34 end; |
|
35 |
|
36 (*repeat_mset is not symmetric, unlike multiplication over natural numbers.*) |
|
37 fun mk_repeat_mset (t, u) = |
|
38 (if fastype_of t = @{typ nat} then (t, u) else (u, t)) |
|
39 |> fast_mk_repeat_mset; |
|
40 |
|
41 (*Maps n to #n for n = 1, 2*) |
|
42 val numeral_syms = |
|
43 map (fn th => th RS sym) @{thms numeral_One numeral_2_eq_2 numeral_1_eq_Suc_0}; |
|
44 |
|
45 val numeral_sym_ss = |
|
46 simpset_of (put_simpset HOL_basic_ss @{context} addsimps numeral_syms); |
|
47 |
|
48 fun mk_number 1 = HOLogic.numeral_const HOLogic.natT $ HOLogic.one_const |
|
49 | mk_number n = HOLogic.mk_number HOLogic.natT n; |
|
50 fun dest_number t = Int.max (0, snd (HOLogic.dest_number t)); |
|
51 |
|
52 fun find_first_numeral past (t::terms) = |
|
53 ((dest_number t, t, rev past @ terms) |
|
54 handle TERM _ => find_first_numeral (t::past) terms) |
|
55 | find_first_numeral _ [] = raise TERM("find_first_numeral", []); |
|
56 |
|
57 fun typed_zero T = Const (@{const_name "Groups.zero"}, T); |
|
58 val mk_plus = HOLogic.mk_binop @{const_name Groups.plus}; |
|
59 |
|
60 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero.*) |
|
61 fun mk_sum T [] = typed_zero T |
|
62 | mk_sum _ [t,u] = mk_plus (t, u) |
|
63 | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); |
|
64 |
|
65 val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} dummyT; |
|
66 |
|
67 |
|
68 (*** Other simproc items ***) |
|
69 |
|
70 val bin_simps = |
|
71 (@{thm numeral_One} RS sym) :: |
|
72 @{thms add_numeral_left diff_nat_numeral diff_0_eq_0 mult_numeral_left(1) |
|
73 if_True if_False not_False_eq_True |
|
74 nat_0 nat_numeral nat_neg_numeral add_mset_commute repeat_mset.simps(1) |
|
75 replicate_mset_0 repeat_mset_empty |
|
76 arith_simps rel_simps}; |
|
77 |
|
78 |
|
79 (*** CancelNumerals simprocs ***) |
|
80 |
|
81 val one = mk_number 1; |
|
82 |
|
83 fun mk_prod [] = one |
|
84 | mk_prod [t] = t |
|
85 | mk_prod (t :: ts) = if t = one then mk_prod ts else mk_repeat_mset (t, mk_prod ts); |
|
86 |
|
87 val dest_repeat_mset = HOLogic.dest_bin @{const_name repeat_mset} dummyT; |
|
88 |
|
89 fun dest_repeat_msets t = |
|
90 let val (t,u) = dest_repeat_mset t in |
|
91 t :: dest_repeat_msets u end |
|
92 handle TERM _ => [t]; |
|
93 |
|
94 fun mk_coeff (k,t) = mk_repeat_mset (mk_number k, t); |
|
95 |
|
96 (*Express t as a product of (possibly) a numeral with other factors, sorted*) |
|
97 fun dest_coeff t = |
|
98 let |
|
99 val ts = sort Term_Ord.term_ord (dest_repeat_msets t); |
|
100 val (n, _, ts') = |
|
101 find_first_numeral [] ts |
|
102 handle TERM _ => (1, one, ts); |
|
103 in (n, mk_prod ts') end; |
|
104 |
|
105 (*Find first coefficient-term THAT MATCHES u*) |
|
106 fun find_first_coeff _ _ [] = raise TERM("find_first_coeff", []) |
|
107 | find_first_coeff past u (t::terms) = |
|
108 let val (n,u') = dest_coeff t in |
|
109 if u aconv u' then (n, rev past @ terms) else find_first_coeff (t::past) u terms end |
|
110 handle TERM _ => find_first_coeff (t::past) u terms; |
|
111 |
|
112 (* |
|
113 Split up a sum into the list of its constituent terms, on the way replace: |
|
114 * the \<open>add_mset a C\<close> by \<open>add_mset a {#}\<close> and \<open>C\<close>, iff C was not already the empty set; |
|
115 * the \<open>replicate_mset n a\<close> by \<open>repeat_mset n {#a#}\<close>. |
|
116 *) |
|
117 fun dest_add_mset (Const (@{const_name add_mset}, T) $ a $ |
|
118 Const (@{const_name "Groups.zero_class.zero"}, U), ts) = |
|
119 Const (@{const_name add_mset}, T) $ a $ typed_zero U :: ts |
|
120 | dest_add_mset (Const (@{const_name add_mset}, T) $ a $ mset, ts) = |
|
121 dest_add_mset (mset, Const (@{const_name add_mset}, T) $ a $ |
|
122 typed_zero (fastype_of mset) :: ts) |
|
123 | dest_add_mset (Const (@{const_name replicate_mset}, |
|
124 Type (_, [_, Type (_, [T, U])])) $ n $ a, ts) = |
|
125 let val single_a = Const (@{const_name add_mset}, T --> U --> U) $ a $ typed_zero U in |
|
126 fast_mk_repeat_mset (n, single_a) :: ts end |
|
127 | dest_add_mset (t, ts) = |
|
128 let val (t1,t2) = dest_plus t in |
|
129 dest_add_mset (t1, dest_add_mset (t2, ts)) end |
|
130 handle TERM _ => t :: ts; |
|
131 |
|
132 fun dest_add_mset_sum t = dest_add_mset (t, []); |
|
133 |
|
134 val rename_numerals = simplify (put_simpset numeral_sym_ss @{context}) o Thm.transfer @{theory}; |
|
135 |
|
136 (*Simplify \<open>repeat_mset (Suc 0) n\<close>, \<open>n+0\<close>, and \<open>0+n\<close> to \<open>n\<close>*) |
|
137 val add_0s = map rename_numerals @{thms Groups.add_0 Groups.add_0_right}; |
|
138 val mult_1s = map rename_numerals @{thms repeat_mset.simps(2)[of 0]}; |
|
139 |
|
140 |
|
141 (*And these help the simproc return False when appropriate. We use the same list as the |
|
142 simproc for natural numbers, but adapted to multisets.*) |
|
143 val contra_rules = |
|
144 @{thms union_mset_add_mset_left union_mset_add_mset_right |
|
145 empty_not_add_mset add_mset_not_empty subset_mset.le_zero_eq le_zero_eq}; |
|
146 |
|
147 val simplify_meta_eq = |
|
148 Arith_Data.simplify_meta_eq |
|
149 (@{thms numeral_1_eq_Suc_0 Nat.add_0_right |
|
150 mult_0 mult_0_right mult_1 mult_1_right |
|
151 Groups.add_0 repeat_mset.simps(1) monoid_add_class.add_0_right} @ |
|
152 contra_rules); |
|
153 |
|
154 val mk_sum = mk_sum; |
|
155 val dest_sum = dest_add_mset_sum; |
|
156 val mk_coeff = mk_coeff; |
|
157 val dest_coeff = dest_coeff; |
|
158 val find_first_coeff = find_first_coeff []; |
|
159 val trans_tac = Numeral_Simprocs.trans_tac; |
|
160 |
|
161 val norm_ss1 = |
|
162 simpset_of (put_simpset Numeral_Simprocs.num_ss @{context} addsimps |
|
163 numeral_syms @ add_0s @ mult_1s @ @{thms ac_simps}); |
|
164 |
|
165 val norm_ss2 = |
|
166 simpset_of (put_simpset Numeral_Simprocs.num_ss @{context} addsimps |
|
167 bin_simps @ |
|
168 @{thms union_mset_add_mset_left union_mset_add_mset_right |
|
169 repeat_mset_replicate_mset ac_simps}); |
|
170 |
|
171 fun norm_tac ctxt = |
|
172 ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt)) |
|
173 THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt)); |
|
174 |
|
175 val mset_simps_ss = |
|
176 simpset_of (put_simpset HOL_basic_ss @{context} addsimps bin_simps); |
|
177 |
|
178 fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset mset_simps_ss ctxt)); |
|
179 |
|
180 val simplify_meta_eq = simplify_meta_eq; |
|
181 val prove_conv = Arith_Data.prove_conv; |
|
182 |
|
183 end |
|