44 fun proc ctxt ct = |
44 fun proc ctxt ct = |
45 let |
45 let |
46 val prems = Simplifier.prems_of ctxt; |
46 val prems = Simplifier.prems_of ctxt; |
47 val t = Thm.term_of ct; |
47 val t = Thm.term_of ct; |
48 val ([t'], ctxt') = Variable.import_terms true [t] ctxt |
48 val ([t'], ctxt') = Variable.import_terms true [t] ctxt |
49 val export = singleton (Variable.export ctxt' ctxt) |
|
50 (* FIXME ctxt vs. ctxt' *) |
|
51 |
49 |
52 val (t1,t2) = Data.dest_bal t' |
50 val (t1,t2) = Data.dest_bal t' |
53 val (m1, t1') = Data.dest_coeff t1 |
51 val (m1, t1') = Data.dest_coeff t1 |
54 and (m2, t2') = Data.dest_coeff t2 |
52 and (m2, t2') = Data.dest_coeff t2 |
55 val d = (*if both are negative, also divide through by ~1*) |
53 val d = (*if both are negative, also divide through by ~1*) |
63 val rhs = if d<0 andalso Data.neg_exchanges |
61 val rhs = if d<0 andalso Data.neg_exchanges |
64 then Data.mk_bal (Data.mk_coeff(n2,t2'), Data.mk_coeff(n1,t1')) |
62 then Data.mk_bal (Data.mk_coeff(n2,t2'), Data.mk_coeff(n1,t1')) |
65 else Data.mk_bal (Data.mk_coeff(n1,t1'), Data.mk_coeff(n2,t2')) |
63 else Data.mk_bal (Data.mk_coeff(n1,t1'), Data.mk_coeff(n2,t2')) |
66 val reshape = (*Move d to the front and put the rest into standard form |
64 val reshape = (*Move d to the front and put the rest into standard form |
67 i * #m * j == #d * (#n * (j * k)) *) |
65 i * #m * j == #d * (#n * (j * k)) *) |
68 Data.prove_conv [Data.norm_tac ctxt] ctxt prems |
66 Data.prove_conv [Data.norm_tac ctxt'] ctxt' prems |
69 (t', Data.mk_bal (newshape(n1,t1'), newshape(n2,t2'))) |
67 (t', Data.mk_bal (newshape(n1,t1'), newshape(n2,t2'))) |
70 in |
68 in |
71 Option.map (export o Data.simplify_meta_eq ctxt) |
69 Option.map (singleton (Variable.export ctxt' ctxt) o Data.simplify_meta_eq ctxt') |
72 (Data.prove_conv |
70 (Data.prove_conv |
73 [Data.trans_tac ctxt reshape, resolve_tac ctxt [Data.cancel] 1, |
71 [Data.trans_tac ctxt' reshape, resolve_tac ctxt' [Data.cancel] 1, |
74 Data.numeral_simp_tac ctxt] ctxt prems (t', rhs)) |
72 Data.numeral_simp_tac ctxt'] ctxt' prems (t', rhs)) |
75 end |
73 end |
76 (* FIXME avoid handling of generic exceptions *) |
74 (* FIXME avoid handling of generic exceptions *) |
77 handle TERM _ => NONE |
75 handle TERM _ => NONE |
78 | TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) |
76 | TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) |
79 Undeclared type constructor "Numeral.bin"*) |
77 Undeclared type constructor "Numeral.bin"*) |