9 (*the main outcome*) |
9 (*the main outcome*) |
10 val nat_cancel: simproc list |
10 val nat_cancel: simproc list |
11 (*tools for use in similar applications*) |
11 (*tools for use in similar applications*) |
12 val gen_trans_tac: thm -> thm option -> tactic |
12 val gen_trans_tac: thm -> thm option -> tactic |
13 val prove_conv: string -> tactic list -> Proof.context -> thm list -> term * term -> thm option |
13 val prove_conv: string -> tactic list -> Proof.context -> thm list -> term * term -> thm option |
14 val simplify_meta_eq: thm list -> simpset -> thm -> thm |
14 val simplify_meta_eq: thm list -> Proof.context -> thm -> thm |
15 (*debugging*) |
15 (*debugging*) |
16 structure EqCancelNumeralsData : CANCEL_NUMERALS_DATA |
16 structure EqCancelNumeralsData : CANCEL_NUMERALS_DATA |
17 structure LessCancelNumeralsData : CANCEL_NUMERALS_DATA |
17 structure LessCancelNumeralsData : CANCEL_NUMERALS_DATA |
18 structure DiffCancelNumeralsData : CANCEL_NUMERALS_DATA |
18 structure DiffCancelNumeralsData : CANCEL_NUMERALS_DATA |
19 end; |
19 end; |
123 val tc_rules = [@{thm natify_in_nat}, @{thm add_type}, @{thm diff_type}, @{thm mult_type}]; |
123 val tc_rules = [@{thm natify_in_nat}, @{thm add_type}, @{thm diff_type}, @{thm mult_type}]; |
124 val natifys = [@{thm natify_0}, @{thm natify_ident}, @{thm add_natify1}, @{thm add_natify2}, |
124 val natifys = [@{thm natify_0}, @{thm natify_ident}, @{thm add_natify1}, @{thm add_natify2}, |
125 @{thm diff_natify1}, @{thm diff_natify2}]; |
125 @{thm diff_natify1}, @{thm diff_natify2}]; |
126 |
126 |
127 (*Final simplification: cancel + and **) |
127 (*Final simplification: cancel + and **) |
128 fun simplify_meta_eq rules = |
128 fun simplify_meta_eq rules ctxt = |
129 let val ss0 = |
129 let val ctxt' = |
130 FOL_ss |
130 put_simpset FOL_ss ctxt |
131 delsimps @{thms iff_simps} (*these could erase the whole rule!*) |
131 delsimps @{thms iff_simps} (*these could erase the whole rule!*) |
132 addsimps rules |
132 addsimps rules |
133 |> fold Simplifier.add_eqcong [@{thm eq_cong2}, @{thm iff_cong2}] |
133 |> fold Simplifier.add_eqcong [@{thm eq_cong2}, @{thm iff_cong2}] |
134 in fn ss => mk_meta_eq o simplify (Simplifier.inherit_context ss ss0) end; |
134 in mk_meta_eq o simplify ctxt' end; |
135 |
135 |
136 val final_rules = add_0s @ mult_1s @ [@{thm mult_0}, @{thm mult_0_right}]; |
136 val final_rules = add_0s @ mult_1s @ [@{thm mult_0}, @{thm mult_0_right}]; |
137 |
137 |
138 structure CancelNumeralsCommon = |
138 structure CancelNumeralsCommon = |
139 struct |
139 struct |
141 val dest_sum = dest_sum |
141 val dest_sum = dest_sum |
142 val mk_coeff = mk_coeff |
142 val mk_coeff = mk_coeff |
143 val dest_coeff = dest_coeff |
143 val dest_coeff = dest_coeff |
144 val find_first_coeff = find_first_coeff [] |
144 val find_first_coeff = find_first_coeff [] |
145 |
145 |
146 val norm_ss1 = ZF_ss addsimps add_0s @ add_succs @ mult_1s @ @{thms add_ac} |
146 val norm_ss1 = |
147 val norm_ss2 = ZF_ss addsimps add_0s @ mult_1s @ @{thms add_ac} @ |
147 simpset_of (put_simpset ZF_ss @{context} addsimps add_0s @ add_succs @ mult_1s @ @{thms add_ac}) |
148 @{thms mult_ac} @ tc_rules @ natifys |
148 val norm_ss2 = |
149 fun norm_tac ss = |
149 simpset_of (put_simpset ZF_ss @{context} addsimps add_0s @ mult_1s @ @{thms add_ac} @ |
150 ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1)) |
150 @{thms mult_ac} @ tc_rules @ natifys) |
151 THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2)) |
151 fun norm_tac ctxt = |
152 val numeral_simp_ss = ZF_ss addsimps add_0s @ tc_rules @ natifys |
152 ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt)) |
153 fun numeral_simp_tac ss = |
153 THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt)) |
154 ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) |
154 val numeral_simp_ss = |
|
155 simpset_of (put_simpset ZF_ss @{context} addsimps add_0s @ tc_rules @ natifys) |
|
156 fun numeral_simp_tac ctxt = |
|
157 ALLGOALS (asm_simp_tac (put_simpset numeral_simp_ss ctxt)) |
155 val simplify_meta_eq = simplify_meta_eq final_rules |
158 val simplify_meta_eq = simplify_meta_eq final_rules |
156 end; |
159 end; |
157 |
160 |
158 (** The functor argumnets are declared as separate structures |
161 (** The functor argumnets are declared as separate structures |
159 so that they can be exported to ease debugging. **) |
162 so that they can be exported to ease debugging. **) |
202 map (prep_simproc @{theory}) |
205 map (prep_simproc @{theory}) |
203 [("nateq_cancel_numerals", |
206 [("nateq_cancel_numerals", |
204 ["l #+ m = n", "l = m #+ n", |
207 ["l #+ m = n", "l = m #+ n", |
205 "l #* m = n", "l = m #* n", |
208 "l #* m = n", "l = m #* n", |
206 "succ(m) = n", "m = succ(n)"], |
209 "succ(m) = n", "m = succ(n)"], |
207 (K EqCancelNumerals.proc)), |
210 EqCancelNumerals.proc), |
208 ("natless_cancel_numerals", |
211 ("natless_cancel_numerals", |
209 ["l #+ m < n", "l < m #+ n", |
212 ["l #+ m < n", "l < m #+ n", |
210 "l #* m < n", "l < m #* n", |
213 "l #* m < n", "l < m #* n", |
211 "succ(m) < n", "m < succ(n)"], |
214 "succ(m) < n", "m < succ(n)"], |
212 (K LessCancelNumerals.proc)), |
215 LessCancelNumerals.proc), |
213 ("natdiff_cancel_numerals", |
216 ("natdiff_cancel_numerals", |
214 ["(l #+ m) #- n", "l #- (m #+ n)", |
217 ["(l #+ m) #- n", "l #- (m #+ n)", |
215 "(l #* m) #- n", "l #- (m #* n)", |
218 "(l #* m) #- n", "l #- (m #* n)", |
216 "succ(m) #- n", "m #- succ(n)"], |
219 "succ(m) #- n", "m #- succ(n)"], |
217 (K DiffCancelNumerals.proc))]; |
220 DiffCancelNumerals.proc)]; |
218 |
221 |
219 end; |
222 end; |
220 |
223 |
221 Addsimprocs ArithData.nat_cancel; |
224 Addsimprocs ArithData.nat_cancel; |
222 |
225 |