35 (*rules*) |
35 (*rules*) |
36 val bal_add1: thm |
36 val bal_add1: thm |
37 val bal_add2: thm |
37 val bal_add2: thm |
38 (*proof tools*) |
38 (*proof tools*) |
39 val prove_conv: tactic list -> Sign.sg -> term * term -> thm option |
39 val prove_conv: tactic list -> Sign.sg -> term * term -> thm option |
40 val subst_tac: thm option -> tactic |
40 val trans_tac: thm option -> tactic (*applies the initial lemma*) |
41 val norm_tac: tactic |
41 val norm_tac: tactic (*proves the initial lemma*) |
42 val numeral_simp_tac: tactic |
42 val numeral_simp_tac: tactic (*proves the final theorem*) |
|
43 val simplify_meta_eq: thm -> thm (*simplifies the final theorem*) |
43 end; |
44 end; |
44 |
45 |
45 |
46 |
46 functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA): |
47 functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA): |
47 sig |
48 sig |
83 (t, |
84 (t, |
84 Data.mk_bal (newshape(n1,terms1'), |
85 Data.mk_bal (newshape(n1,terms1'), |
85 newshape(n2,terms2'))) |
86 newshape(n2,terms2'))) |
86 in |
87 in |
87 |
88 |
88 if n2<=n1 then |
89 apsome Data.simplify_meta_eq |
89 Data.prove_conv |
90 (if n2<=n1 then |
90 [Data.subst_tac reshape, rtac Data.bal_add1 1, |
91 Data.prove_conv |
91 Data.numeral_simp_tac] sg |
92 [Data.trans_tac reshape, rtac Data.bal_add1 1, |
92 (t, Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum terms2')) |
93 Data.numeral_simp_tac] sg |
93 else |
94 (t, Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum terms2')) |
94 Data.prove_conv |
95 else |
95 [Data.subst_tac reshape, rtac Data.bal_add2 1, |
96 Data.prove_conv |
96 Data.numeral_simp_tac] sg |
97 [Data.trans_tac reshape, rtac Data.bal_add2 1, |
97 (t, Data.mk_bal (Data.mk_sum terms1', newshape(n2-n1,terms2'))) |
98 Data.numeral_simp_tac] sg |
|
99 (t, Data.mk_bal (Data.mk_sum terms1', newshape(n2-n1,terms2')))) |
98 end |
100 end |
99 handle TERM _ => None |
101 handle TERM _ => None |
100 | TYPE _ => None; (*Typically (if thy doesn't include Numeral) |
102 | TYPE _ => None; (*Typically (if thy doesn't include Numeral) |
101 Undeclared type constructor "Numeral.bin"*) |
103 Undeclared type constructor "Numeral.bin"*) |
102 |
104 |