author | fleury <Mathias.Fleury@mpi-inf.mpg.de> |
Tue, 14 Feb 2017 18:32:53 +0100 | |
changeset 65029 | 00731700e54f |
child 65367 | 83c30e290702 |
permissions | -rw-r--r-- |
65029
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1 |
(* Title: Provers/Arith/cancel_data.ML |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
2 |
Author: Mathias Fleury, MPII |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
3 |
Copyright 2017 |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
4 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
5 |
Based on: |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
6 |
Title: Tools/nat_numeral_simprocs.ML |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
7 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
8 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
9 |
Datastructure for the cancelation simprocs. |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
10 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
11 |
*) |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
12 |
signature CANCEL_DATA = |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
13 |
sig |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
14 |
val mk_sum : typ -> term list -> term |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
15 |
val dest_sum : term -> term list |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
16 |
val mk_coeff : int * term -> term |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
17 |
val dest_coeff : term -> int * term |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
18 |
val find_first_coeff : term -> term list -> int * term list |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
19 |
val trans_tac : Proof.context -> thm option -> tactic |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
20 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
21 |
val norm_ss1 : simpset |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
22 |
val norm_ss2: simpset |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
23 |
val norm_tac: Proof.context -> tactic |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
24 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
25 |
val numeral_simp_tac : Proof.context -> tactic |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
26 |
val simplify_meta_eq : Proof.context -> thm -> thm |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
27 |
val prove_conv : tactic list -> Proof.context -> thm list -> term * term -> thm option |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
28 |
end; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
29 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
30 |
structure Cancel_Data : CANCEL_DATA = |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
31 |
struct |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
32 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
33 |
(*** Utilities ***) |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
34 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
35 |
(*No reordering of the arguments.*) |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
36 |
fun fast_mk_iterate_add (n, mset) = |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
37 |
let val T = fastype_of mset |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
38 |
in |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
39 |
Const (@{const_name "iterate_add"}, @{typ nat} --> T --> T) $ n $ mset |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
40 |
end; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
41 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
42 |
(*iterate_add is not symmetric, unlike multiplication over natural numbers.*) |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
43 |
fun mk_iterate_add (t, u) = |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
44 |
(if fastype_of t = @{typ nat} then (t, u) else (u, t)) |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
45 |
|> fast_mk_iterate_add; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
46 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
47 |
(*Maps n to #n for n = 1, 2*) |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
48 |
val numeral_syms = |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
49 |
map (fn th => th RS sym) @{thms numeral_One numeral_2_eq_2 numeral_1_eq_Suc_0}; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
50 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
51 |
val numeral_sym_ss = |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
52 |
simpset_of (put_simpset HOL_basic_ss @{context} addsimps numeral_syms); |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
53 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
54 |
fun mk_number 1 = HOLogic.numeral_const HOLogic.natT $ HOLogic.one_const |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
55 |
| mk_number n = HOLogic.mk_number HOLogic.natT n; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
56 |
fun dest_number t = Int.max (0, snd (HOLogic.dest_number t)); |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
57 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
58 |
fun find_first_numeral past (t::terms) = |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
59 |
((dest_number t, t, rev past @ terms) |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
60 |
handle TERM _ => find_first_numeral (t::past) terms) |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
61 |
| find_first_numeral _ [] = raise TERM("find_first_numeral", []); |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
62 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
63 |
fun typed_zero T = Const (@{const_name "Groups.zero"}, T); |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
64 |
fun typed_one T = HOLogic.numeral_const T $ HOLogic.one_const |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
65 |
val mk_plus = HOLogic.mk_binop @{const_name Groups.plus}; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
66 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
67 |
(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero.*) |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
68 |
fun mk_sum T [] = typed_zero T |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
69 |
| mk_sum _ [t,u] = mk_plus (t, u) |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
70 |
| mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
71 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
72 |
val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} dummyT; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
73 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
74 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
75 |
(*** Other simproc items ***) |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
76 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
77 |
val bin_simps = |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
78 |
(@{thm numeral_One} RS sym) :: |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
79 |
@{thms add_numeral_left diff_nat_numeral diff_0_eq_0 mult_numeral_left(1) |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
80 |
if_True if_False not_False_eq_True nat_0 nat_numeral nat_neg_numeral iterate_add_simps(1) |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
81 |
iterate_add_empty arith_simps rel_simps of_nat_numeral}; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
82 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
83 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
84 |
(*** CancelNumerals simprocs ***) |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
85 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
86 |
val one = mk_number 1; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
87 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
88 |
fun mk_prod T [] = typed_one T |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
89 |
| mk_prod _ [t] = t |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
90 |
| mk_prod T (t :: ts) = if t = one then mk_prod T ts else mk_iterate_add (t, mk_prod T ts); |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
91 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
92 |
val dest_iterate_add = HOLogic.dest_bin @{const_name iterate_add} dummyT; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
93 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
94 |
fun dest_iterate_adds t = |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
95 |
let val (t,u) = dest_iterate_add t in |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
96 |
t :: dest_iterate_adds u end |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
97 |
handle TERM _ => [t]; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
98 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
99 |
fun mk_coeff (k,t) = mk_iterate_add (mk_number k, t); |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
100 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
101 |
(*Express t as a product of (possibly) a numeral with other factors, sorted*) |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
102 |
fun dest_coeff t = |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
103 |
let |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
104 |
val T = fastype_of t |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
105 |
val ts = sort Term_Ord.term_ord (dest_iterate_adds t); |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
106 |
val (n, _, ts') = |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
107 |
find_first_numeral [] ts |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
108 |
handle TERM _ => (1, one, ts); |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
109 |
in (n, mk_prod T ts') end; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
110 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
111 |
(*Find first coefficient-term THAT MATCHES u*) |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
112 |
fun find_first_coeff _ _ [] = raise TERM("find_first_coeff", []) |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
113 |
| find_first_coeff past u (t::terms) = |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
114 |
let val (n,u') = dest_coeff t in |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
115 |
if u aconv u' then (n, rev past @ terms) else find_first_coeff (t::past) u terms end |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
116 |
handle TERM _ => find_first_coeff (t::past) u terms; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
117 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
118 |
(* |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
119 |
Split up a sum into the list of its constituent terms. |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
120 |
*) |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
121 |
fun dest_summation (t, ts) = |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
122 |
let val (t1,t2) = dest_plus t in |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
123 |
dest_summation (t1, dest_summation (t2, ts)) end |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
124 |
handle TERM _ => t :: ts; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
125 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
126 |
fun dest_sum t = dest_summation (t, []); |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
127 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
128 |
val rename_numerals = simplify (put_simpset numeral_sym_ss @{context}) o Thm.transfer @{theory}; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
129 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
130 |
(*Simplify \<open>iterate_add (Suc 0) n\<close>, \<open>iterate_add n (Suc 0)\<close>, \<open>n+0\<close>, and \<open>0+n\<close> to \<open>n\<close>*) |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
131 |
val add_0s = map rename_numerals @{thms monoid_add_class.add_0_left monoid_add_class.add_0_right}; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
132 |
val mult_1s = map rename_numerals @{thms iterate_add_1 iterate_add_simps(2)[of 0]}; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
133 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
134 |
(*And these help the simproc return False when appropriate. We use the same list as the |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
135 |
simproc for natural numbers, but adapted.*) |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
136 |
fun contra_rules ctxt = |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
137 |
@{thms le_zero_eq} @ Named_Theorems.get ctxt @{named_theorems cancelation_simproc_eq_elim}; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
138 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
139 |
fun simplify_meta_eq ctxt = |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
140 |
Arith_Data.simplify_meta_eq |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
141 |
(@{thms numeral_1_eq_Suc_0 Nat.add_0_right |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
142 |
mult_0 mult_0_right mult_1 mult_1_right iterate_add_Numeral1 of_nat_numeral |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
143 |
monoid_add_class.add_0_left iterate_add_simps(1) monoid_add_class.add_0_right |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
144 |
iterate_add_Numeral1} @ |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
145 |
contra_rules ctxt) ctxt; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
146 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
147 |
val mk_sum = mk_sum; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
148 |
val dest_sum = dest_sum; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
149 |
val mk_coeff = mk_coeff; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
150 |
val dest_coeff = dest_coeff; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
151 |
val find_first_coeff = find_first_coeff []; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
152 |
val trans_tac = Numeral_Simprocs.trans_tac; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
153 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
154 |
val norm_ss1 = |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
155 |
simpset_of (put_simpset Numeral_Simprocs.num_ss @{context} addsimps |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
156 |
numeral_syms @ add_0s @ mult_1s @ @{thms ac_simps iterate_add_simps}); |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
157 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
158 |
val norm_ss2 = |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
159 |
simpset_of (put_simpset Numeral_Simprocs.num_ss @{context} addsimps |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
160 |
bin_simps @ |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
161 |
@{thms ac_simps}); |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
162 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
163 |
fun norm_tac ctxt = |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
164 |
ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt)) |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
165 |
THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt)); |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
166 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
167 |
val mset_simps_ss = |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
168 |
simpset_of (put_simpset HOL_basic_ss @{context} addsimps bin_simps); |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
169 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
170 |
fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset mset_simps_ss ctxt)); |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
171 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
172 |
val simplify_meta_eq = simplify_meta_eq; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
173 |
val prove_conv = Arith_Data.prove_conv; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
174 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
175 |
end |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
176 |