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_simprocs.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 |
Base on: |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
6 |
Title: Provers/Arith/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 |
Cancelation simprocs declaration. |
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_SIMPROCS = |
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 eq_cancel: Proof.context -> cterm -> thm option |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
15 |
val less_cancel: Proof.context -> cterm -> thm option |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
16 |
val less_eq_cancel: Proof.context -> cterm -> thm option |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
17 |
val diff_cancel: Proof.context -> cterm -> thm option |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
18 |
end; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
19 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
20 |
structure Cancel_Simprocs : CANCEL_SIMPROCS = |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
21 |
struct |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
22 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
23 |
structure Eq_Cancel_Comm_Monoid_add = Cancel_Fun |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
24 |
(open Cancel_Data |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
25 |
val mk_bal = HOLogic.mk_eq |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
26 |
val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} dummyT |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
27 |
val bal_add1 = @{thm iterate_add_eq_add_iff1} RS trans |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
28 |
val bal_add2 = @{thm iterate_add_eq_add_iff2} RS trans |
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 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
31 |
structure Eq_Cancel_Comm_Monoid_less = Cancel_Fun |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
32 |
(open Cancel_Data |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
33 |
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
34 |
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} dummyT |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
35 |
val bal_add1 = @{thm iterate_add_less_iff1} RS trans |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
36 |
val bal_add2 = @{thm iterate_add_less_iff2} RS trans |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
37 |
); |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
38 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
39 |
structure Eq_Cancel_Comm_Monoid_less_eq = Cancel_Fun |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
40 |
(open Cancel_Data |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
41 |
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
42 |
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} dummyT |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
43 |
val bal_add1 = @{thm iterate_add_less_eq_iff1} RS trans |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
44 |
val bal_add2 = @{thm iterate_add_less_eq_iff2} RS trans |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
45 |
); |
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 |
structure Diff_Cancel_Comm_Monoid_less_eq = Cancel_Fun |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
48 |
(open Cancel_Data |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
49 |
val mk_bal = HOLogic.mk_binop @{const_name Groups.minus} |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
50 |
val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} dummyT |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
51 |
val bal_add1 = @{thm iterate_add_add_eq1} RS trans |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
52 |
val bal_add2 = @{thm iterate_add_diff_add_eq2} RS trans |
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 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
55 |
val eq_cancel = Eq_Cancel_Comm_Monoid_add.proc; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
56 |
val less_cancel = Eq_Cancel_Comm_Monoid_less.proc; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
57 |
val less_eq_cancel = Eq_Cancel_Comm_Monoid_less_eq.proc; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
58 |
val diff_cancel = Diff_Cancel_Comm_Monoid_less_eq.proc; |
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
59 |
|
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
60 |
end |