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 -> theory -> |
32 val prove_conv: tactic list -> Proof.context -> |
33 thm list -> string list -> term * term -> thm option |
33 thm list -> string list -> term * term -> thm option |
34 val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*) |
34 val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*) |
35 val norm_tac: simpset -> tactic (*proves the initial lemma*) |
35 val norm_tac: simpset -> tactic (*proves the initial lemma*) |
36 val numeral_simp_tac: simpset -> tactic (*proves the final theorem*) |
36 val numeral_simp_tac: simpset -> tactic (*proves the final theorem*) |
37 val simplify_meta_eq: simpset -> 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: theory -> simpset -> term -> thm option |
43 val proc: 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 thy ss t = |
49 fun proc ss t = |
50 let |
50 let |
|
51 val ctxt = Simplifier.the_context ss; |
51 val hyps = prems_of_ss ss; |
52 val hyps = prems_of_ss ss; |
52 (*first freeze any Vars in the term to prevent flex-flex problems*) |
53 (*first freeze any Vars in the term to prevent flex-flex problems*) |
53 val (t', xs) = Term.adhoc_freeze_vars t; |
54 val (t', xs) = Term.adhoc_freeze_vars t; |
54 val (t1,t2) = Data.dest_bal t' |
55 val (t1,t2) = Data.dest_bal t' |
55 val (m1, t1') = Data.dest_coeff t1 |
56 val (m1, t1') = Data.dest_coeff t1 |
65 val rhs = if d<0 andalso Data.neg_exchanges |
66 val rhs = if d<0 andalso Data.neg_exchanges |
66 then Data.mk_bal (Data.mk_coeff(n2,t2'), Data.mk_coeff(n1,t1')) |
67 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')) |
68 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 |
69 val reshape = (*Move d to the front and put the rest into standard form |
69 i * #m * j == #d * (#n * (j * k)) *) |
70 i * #m * j == #d * (#n * (j * k)) *) |
70 Data.prove_conv [Data.norm_tac ss] thy hyps xs |
71 Data.prove_conv [Data.norm_tac ss] ctxt hyps xs |
71 (t', Data.mk_bal (newshape(n1,t1'), newshape(n2,t2'))) |
72 (t', Data.mk_bal (newshape(n1,t1'), newshape(n2,t2'))) |
72 in |
73 in |
73 Option.map (Data.simplify_meta_eq ss) |
74 Option.map (Data.simplify_meta_eq ss) |
74 (Data.prove_conv |
75 (Data.prove_conv |
75 [Data.trans_tac ss reshape, rtac Data.cancel 1, |
76 [Data.trans_tac ss reshape, rtac Data.cancel 1, |
76 Data.numeral_simp_tac ss] thy hyps xs (t', rhs)) |
77 Data.numeral_simp_tac ss] ctxt hyps xs (t', rhs)) |
77 end |
78 end |
78 handle TERM _ => NONE |
79 handle TERM _ => NONE |
79 | TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) |
80 | TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) |
80 Undeclared type constructor "Numeral.bin"*) |
81 Undeclared type constructor "Numeral.bin"*) |
81 |
82 |