27 val cancel: thm |
27 val cancel: thm |
28 val neg_exchanges: bool (*true if a negative coeff swaps the two operands, |
28 val neg_exchanges: bool (*true if a negative coeff swaps the two operands, |
29 as with < and <= but not = and div*) |
29 as with < and <= but not = and div*) |
30 (*proof tools*) |
30 (*proof tools*) |
31 val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option |
31 val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option |
32 val trans_tac: thm option -> tactic (*applies the initial lemma*) |
32 val trans_tac: thm option -> tactic (*applies the initial lemma*) |
33 val norm_tac: simpset -> tactic (*proves the initial lemma*) |
33 val norm_tac: Proof.context -> tactic (*proves the initial lemma*) |
34 val numeral_simp_tac: simpset -> tactic (*proves the final theorem*) |
34 val numeral_simp_tac: Proof.context -> tactic (*proves the final theorem*) |
35 val simplify_meta_eq: simpset -> thm -> thm (*simplifies the final theorem*) |
35 val simplify_meta_eq: Proof.context -> thm -> thm (*simplifies the final theorem*) |
36 end; |
36 end; |
37 |
37 |
38 |
38 |
39 functor CancelNumeralFactorFun(Data: CANCEL_NUMERAL_FACTOR_DATA): |
39 functor CancelNumeralFactorFun(Data: CANCEL_NUMERAL_FACTOR_DATA): |
40 sig |
40 sig |
41 val proc: simpset -> term -> thm option |
41 val proc: Proof.context -> term -> thm option |
42 end |
42 end |
43 = |
43 = |
44 struct |
44 struct |
45 |
45 |
46 (*the simplification procedure*) |
46 (*the simplification procedure*) |
47 fun proc ss t = |
47 fun proc ctxt t = |
48 let |
48 let |
49 val ctxt = Simplifier.the_context ss; |
49 val prems = Simplifier.prems_of ctxt; |
50 val prems = Simplifier.prems_of ss; |
|
51 val ([t'], ctxt') = Variable.import_terms true [t] ctxt |
50 val ([t'], ctxt') = Variable.import_terms true [t] ctxt |
52 val export = singleton (Variable.export ctxt' ctxt) |
51 val export = singleton (Variable.export ctxt' ctxt) |
|
52 (* FIXME ctxt vs. ctxt' *) |
53 |
53 |
54 val (t1,t2) = Data.dest_bal t' |
54 val (t1,t2) = Data.dest_bal t' |
55 val (m1, t1') = Data.dest_coeff t1 |
55 val (m1, t1') = Data.dest_coeff t1 |
56 and (m2, t2') = Data.dest_coeff t2 |
56 and (m2, t2') = Data.dest_coeff t2 |
57 val d = (*if both are negative, also divide through by ~1*) |
57 val d = (*if both are negative, also divide through by ~1*) |
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 ss] ctxt prems |
70 Data.prove_conv [Data.norm_tac ctxt] ctxt prems |
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 (export o Data.simplify_meta_eq ss) |
73 Option.map (export o Data.simplify_meta_eq ctxt) |
74 (Data.prove_conv |
74 (Data.prove_conv |
75 [Data.trans_tac reshape, rtac Data.cancel 1, |
75 [Data.trans_tac reshape, rtac Data.cancel 1, |
76 Data.numeral_simp_tac ss] ctxt prems (t', rhs)) |
76 Data.numeral_simp_tac ctxt] ctxt prems (t', rhs)) |
77 end |
77 end |
78 (* FIXME avoid handling of generic exceptions *) |
78 (* FIXME avoid handling of generic exceptions *) |
79 handle TERM _ => NONE |
79 handle TERM _ => NONE |
80 | TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) |
80 | TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) |
81 Undeclared type constructor "Numeral.bin"*) |
81 Undeclared type constructor "Numeral.bin"*) |