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 -> Sign.sg -> |
33 thm 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: thm option -> tactic (*applies the initial lemma*) |
35 val norm_tac: tactic (*proves the initial lemma*) |
35 val norm_tac: tactic (*proves the initial lemma*) |
36 val numeral_simp_tac: tactic (*proves the final theorem*) |
36 val numeral_simp_tac: tactic (*proves the final theorem*) |
37 val simplify_meta_eq: thm -> thm (*simplifies the final theorem*) |
37 val simplify_meta_eq: thm -> thm (*simplifies the final theorem*) |
38 end; |
38 end; |
51 | gcd (m, n) = gcd (n mod m, m); |
51 | gcd (m, n) = gcd (n mod m, m); |
52 |
52 |
53 (*the simplification procedure*) |
53 (*the simplification procedure*) |
54 fun proc sg hyps t = |
54 fun proc sg hyps t = |
55 let (*first freeze any Vars in the term to prevent flex-flex problems*) |
55 let (*first freeze any Vars in the term to prevent flex-flex problems*) |
56 val rand_s = gensym"_" |
56 val (t', xs) = Term.adhoc_freeze_vars t; |
57 fun mk_inst (var as Var((a,i),T)) = |
|
58 (var, Free((a ^ rand_s ^ string_of_int i), T)) |
|
59 val t' = subst_atomic (map mk_inst (term_vars t)) t |
|
60 val (t1,t2) = Data.dest_bal t' |
57 val (t1,t2) = Data.dest_bal t' |
61 val (m1, t1') = Data.dest_coeff t1 |
58 val (m1, t1') = Data.dest_coeff t1 |
62 and (m2, t2') = Data.dest_coeff t2 |
59 and (m2, t2') = Data.dest_coeff t2 |
63 val d = (*if both are negative, also divide through by ~1*) |
60 val d = (*if both are negative, also divide through by ~1*) |
64 if (m1<0 andalso m2<=0) orelse |
61 if (m1<0 andalso m2<=0) orelse |
71 val rhs = if d<0 andalso Data.neg_exchanges |
68 val rhs = if d<0 andalso Data.neg_exchanges |
72 then Data.mk_bal (Data.mk_coeff(n2,t2'), Data.mk_coeff(n1,t1')) |
69 then Data.mk_bal (Data.mk_coeff(n2,t2'), Data.mk_coeff(n1,t1')) |
73 else Data.mk_bal (Data.mk_coeff(n1,t1'), Data.mk_coeff(n2,t2')) |
70 else Data.mk_bal (Data.mk_coeff(n1,t1'), Data.mk_coeff(n2,t2')) |
74 val reshape = (*Move d to the front and put the rest into standard form |
71 val reshape = (*Move d to the front and put the rest into standard form |
75 i * #m * j == #d * (#n * (j * k)) *) |
72 i * #m * j == #d * (#n * (j * k)) *) |
76 Data.prove_conv [Data.norm_tac] sg hyps |
73 Data.prove_conv [Data.norm_tac] sg hyps xs |
77 (t', Data.mk_bal (newshape(n1,t1'), newshape(n2,t2'))) |
74 (t', Data.mk_bal (newshape(n1,t1'), newshape(n2,t2'))) |
78 in |
75 in |
79 apsome Data.simplify_meta_eq |
76 apsome Data.simplify_meta_eq |
80 (Data.prove_conv |
77 (Data.prove_conv |
81 [Data.trans_tac reshape, rtac Data.cancel 1, |
78 [Data.trans_tac reshape, rtac Data.cancel 1, |
82 Data.numeral_simp_tac] sg hyps (t', rhs)) |
79 Data.numeral_simp_tac] sg hyps xs (t', rhs)) |
83 end |
80 end |
84 handle TERM _ => None |
81 handle TERM _ => None |
85 | TYPE _ => None; (*Typically (if thy doesn't include Numeral) |
82 | TYPE _ => None; (*Typically (if thy doesn't include Numeral) |
86 Undeclared type constructor "Numeral.bin"*) |
83 Undeclared type constructor "Numeral.bin"*) |
87 |
84 |