34 val find_first_coeff: term -> term list -> IntInf.int * term list |
34 val find_first_coeff: term -> term list -> IntInf.int * term list |
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 -> |
39 val prove_conv: tactic list -> theory -> |
40 thm list -> string list -> term * term -> thm option |
40 thm list -> string list -> term * term -> thm option |
41 val trans_tac: thm option -> tactic (*applies the initial lemma*) |
41 val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*) |
42 val norm_tac: tactic (*proves the initial lemma*) |
42 val norm_tac: simpset -> tactic (*proves the initial lemma*) |
43 val numeral_simp_tac: tactic (*proves the final theorem*) |
43 val numeral_simp_tac: simpset -> tactic (*proves the final theorem*) |
44 val simplify_meta_eq: thm -> thm (*simplifies the final theorem*) |
44 val simplify_meta_eq: simpset -> thm -> thm (*simplifies the final theorem*) |
45 end; |
45 end; |
46 |
46 |
47 |
47 |
48 functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA): |
48 functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA): |
49 sig |
49 sig |
50 val proc: Sign.sg -> simpset -> term -> thm option |
50 val proc: theory -> simpset -> term -> thm option |
51 end |
51 end |
52 = |
52 = |
53 struct |
53 struct |
54 |
54 |
55 (*For t = #n*u then put u in the table*) |
55 (*For t = #n*u then put u in the table*) |
67 else seek terms |
67 else seek terms |
68 end |
68 end |
69 in seek terms1 end; |
69 in seek terms1 end; |
70 |
70 |
71 (*the simplification procedure*) |
71 (*the simplification procedure*) |
72 fun proc sg ss t = |
72 fun proc thy ss t = |
73 let |
73 let |
74 val hyps = prems_of_ss ss; |
74 val hyps = prems_of_ss ss; |
75 (*first freeze any Vars in the term to prevent flex-flex problems*) |
75 (*first freeze any Vars in the term to prevent flex-flex problems*) |
76 val (t', xs) = Term.adhoc_freeze_vars t; |
76 val (t', xs) = Term.adhoc_freeze_vars t; |
77 val (t1,t2) = Data.dest_bal t' |
77 val (t1,t2) = Data.dest_bal t' |
84 fun newshape (i,terms) = Data.mk_sum T (Data.mk_coeff(i,u)::terms) |
84 fun newshape (i,terms) = Data.mk_sum T (Data.mk_coeff(i,u)::terms) |
85 val reshape = (*Move i*u to the front and put j*u into standard form |
85 val reshape = (*Move i*u to the front and put j*u into standard form |
86 i + #m + j + k == #m + i + (j + k) *) |
86 i + #m + j + k == #m + i + (j + k) *) |
87 if n1=0 orelse n2=0 then (*trivial, so do nothing*) |
87 if n1=0 orelse n2=0 then (*trivial, so do nothing*) |
88 raise TERM("cancel_numerals", []) |
88 raise TERM("cancel_numerals", []) |
89 else Data.prove_conv [Data.norm_tac] sg hyps xs |
89 else Data.prove_conv [Data.norm_tac ss] thy hyps xs |
90 (t', |
90 (t', |
91 Data.mk_bal (newshape(n1,terms1'), |
91 Data.mk_bal (newshape(n1,terms1'), |
92 newshape(n2,terms2'))) |
92 newshape(n2,terms2'))) |
93 in |
93 in |
94 Option.map Data.simplify_meta_eq |
94 Option.map (Data.simplify_meta_eq ss) |
95 (if n2<=n1 then |
95 (if n2<=n1 then |
96 Data.prove_conv |
96 Data.prove_conv |
97 [Data.trans_tac reshape, rtac Data.bal_add1 1, |
97 [Data.trans_tac ss reshape, rtac Data.bal_add1 1, |
98 Data.numeral_simp_tac] sg hyps xs |
98 Data.numeral_simp_tac ss] thy hyps xs |
99 (t', Data.mk_bal (newshape(n1-n2,terms1'), |
99 (t', Data.mk_bal (newshape(n1-n2,terms1'), |
100 Data.mk_sum T terms2')) |
100 Data.mk_sum T terms2')) |
101 else |
101 else |
102 Data.prove_conv |
102 Data.prove_conv |
103 [Data.trans_tac reshape, rtac Data.bal_add2 1, |
103 [Data.trans_tac ss reshape, rtac Data.bal_add2 1, |
104 Data.numeral_simp_tac] sg hyps xs |
104 Data.numeral_simp_tac ss] thy hyps xs |
105 (t', Data.mk_bal (Data.mk_sum T terms1', |
105 (t', Data.mk_bal (Data.mk_sum T terms1', |
106 newshape(n2-n1,terms2')))) |
106 newshape(n2-n1,terms2')))) |
107 end |
107 end |
108 handle TERM _ => NONE |
108 handle TERM _ => NONE |
109 | TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) |
109 | TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) |