27 (*rules*) |
27 (*rules*) |
28 val cancel: thm |
28 val cancel: thm |
29 val neg_exchanges: bool (*true if a negative coeff swaps the two operands, |
29 val neg_exchanges: bool (*true if a negative coeff swaps the two operands, |
30 as with < and <= but not = and div*) |
30 as with < and <= but not = and div*) |
31 (*proof tools*) |
31 (*proof tools*) |
32 val prove_conv: tactic list -> Sign.sg -> |
32 val prove_conv: tactic list -> theory -> |
33 thm list -> string list -> term * term -> thm option |
33 thm list -> string list -> term * term -> thm option |
34 val trans_tac: thm option -> tactic (*applies the initial lemma*) |
34 val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*) |
35 val norm_tac: tactic (*proves the initial lemma*) |
35 val norm_tac: simpset -> tactic (*proves the initial lemma*) |
36 val numeral_simp_tac: tactic (*proves the final theorem*) |
36 val numeral_simp_tac: simpset -> tactic (*proves the final theorem*) |
37 val simplify_meta_eq: thm -> thm (*simplifies the final theorem*) |
37 val simplify_meta_eq: simpset -> thm -> thm (*simplifies the final theorem*) |
38 end; |
38 end; |
39 |
39 |
40 |
40 |
41 functor CancelNumeralFactorFun(Data: CANCEL_NUMERAL_FACTOR_DATA): |
41 functor CancelNumeralFactorFun(Data: CANCEL_NUMERAL_FACTOR_DATA): |
42 sig |
42 sig |
43 val proc: Sign.sg -> simpset -> term -> thm option |
43 val proc: theory -> simpset -> term -> thm option |
44 end |
44 end |
45 = |
45 = |
46 struct |
46 struct |
47 |
47 |
48 (*the simplification procedure*) |
48 (*the simplification procedure*) |
49 fun proc sg ss t = |
49 fun proc thy ss t = |
50 let |
50 let |
51 val hyps = prems_of_ss ss; |
51 val hyps = prems_of_ss ss; |
52 (*first freeze any Vars in the term to prevent flex-flex problems*) |
52 (*first freeze any Vars in the term to prevent flex-flex problems*) |
53 val (t', xs) = Term.adhoc_freeze_vars t; |
53 val (t', xs) = Term.adhoc_freeze_vars t; |
54 val (t1,t2) = Data.dest_bal t' |
54 val (t1,t2) = Data.dest_bal t' |
65 val rhs = if d<0 andalso Data.neg_exchanges |
65 val rhs = if d<0 andalso Data.neg_exchanges |
66 then Data.mk_bal (Data.mk_coeff(n2,t2'), Data.mk_coeff(n1,t1')) |
66 then Data.mk_bal (Data.mk_coeff(n2,t2'), Data.mk_coeff(n1,t1')) |
67 else Data.mk_bal (Data.mk_coeff(n1,t1'), Data.mk_coeff(n2,t2')) |
67 else Data.mk_bal (Data.mk_coeff(n1,t1'), Data.mk_coeff(n2,t2')) |
68 val reshape = (*Move d to the front and put the rest into standard form |
68 val reshape = (*Move d to the front and put the rest into standard form |
69 i * #m * j == #d * (#n * (j * k)) *) |
69 i * #m * j == #d * (#n * (j * k)) *) |
70 Data.prove_conv [Data.norm_tac] sg hyps xs |
70 Data.prove_conv [Data.norm_tac ss] thy hyps xs |
71 (t', Data.mk_bal (newshape(n1,t1'), newshape(n2,t2'))) |
71 (t', Data.mk_bal (newshape(n1,t1'), newshape(n2,t2'))) |
72 in |
72 in |
73 Option.map Data.simplify_meta_eq |
73 Option.map (Data.simplify_meta_eq ss) |
74 (Data.prove_conv |
74 (Data.prove_conv |
75 [Data.trans_tac reshape, rtac Data.cancel 1, |
75 [Data.trans_tac ss reshape, rtac Data.cancel 1, |
76 Data.numeral_simp_tac] sg hyps xs (t', rhs)) |
76 Data.numeral_simp_tac ss] thy hyps xs (t', rhs)) |
77 end |
77 end |
78 handle TERM _ => NONE |
78 handle TERM _ => NONE |
79 | TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) |
79 | TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) |
80 Undeclared type constructor "Numeral.bin"*) |
80 Undeclared type constructor "Numeral.bin"*) |
81 |
81 |