11 end; |
11 end; |
12 |
12 |
13 structure Multiset_Order_Simprocs : MULTISET_ORDER_SIMPROCS = |
13 structure Multiset_Order_Simprocs : MULTISET_ORDER_SIMPROCS = |
14 struct |
14 struct |
15 |
15 |
16 structure LessCancelMultiset = CancelNumeralsFun |
16 structure LessCancelMultiset = Cancel_Fun |
17 (open Multiset_Cancel_Common |
17 (open Cancel_Data |
18 val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} |
18 val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} |
19 val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} dummyT |
19 val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} dummyT |
20 val bal_add1 = @{thm mset_less_add_iff1} RS trans |
20 val bal_add1 = @{thm mset_less_add_iff1[unfolded repeat_mset_iterate_add]} RS trans |
21 val bal_add2 = @{thm mset_less_add_iff2} RS trans |
21 val bal_add2 = @{thm mset_less_add_iff2[unfolded repeat_mset_iterate_add]} RS trans |
22 ); |
22 ); |
23 |
23 |
24 structure LeCancelMultiset = CancelNumeralsFun |
24 structure LeCancelMultiset = Cancel_Fun |
25 (open Multiset_Cancel_Common |
25 (open Cancel_Data |
26 val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} |
26 val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} |
27 val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} dummyT |
27 val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} dummyT |
28 val bal_add1 = @{thm mset_le_add_iff1} RS trans |
28 val bal_add1 = @{thm mset_le_add_iff1[unfolded repeat_mset_iterate_add]} RS trans |
29 val bal_add2 = @{thm mset_le_add_iff2} RS trans |
29 val bal_add2 = @{thm mset_le_add_iff2[unfolded repeat_mset_iterate_add]} RS trans |
30 ); |
30 ); |
31 |
31 |
32 val less_cancel_msets = LessCancelMultiset.proc; |
32 val less_cancel_msets = LessCancelMultiset.proc; |
33 val le_cancel_msets = LeCancelMultiset.proc; |
33 val le_cancel_msets = LeCancelMultiset.proc; |
34 |
34 |