1.1 --- a/src/HOL/Tools/abel_cancel.ML Tue Jul 20 08:54:21 2010 +0200
1.2 +++ b/src/HOL/Tools/abel_cancel.ML Tue Jul 20 10:24:18 2010 +0200
1.3 @@ -16,74 +16,41 @@
1.4 structure Abel_Cancel: ABEL_CANCEL =
1.5 struct
1.6
1.7 -(* term order for abelian groups *)
1.8 +(** compute cancellation **)
1.9
1.10 -fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')
1.11 - [@{const_name Groups.zero}, @{const_name Groups.plus},
1.12 - @{const_name Groups.uminus}, @{const_name Groups.minus}]
1.13 - | agrp_ord _ = ~1;
1.14 +fun add_atoms pos (Const (@{const_name Groups.plus}, _) $ x $ y) =
1.15 + add_atoms pos x #> add_atoms pos y
1.16 + | add_atoms pos (Const (@{const_name Groups.minus}, _) $ x $ y) =
1.17 + add_atoms pos x #> add_atoms (not pos) y
1.18 + | add_atoms pos (Const (@{const_name Groups.uminus}, _) $ x) =
1.19 + add_atoms (not pos) x
1.20 + | add_atoms pos x = cons (pos, x);
1.21
1.22 -fun termless_agrp (a, b) = (Term_Ord.term_lpo agrp_ord (a, b) = LESS);
1.23 +fun atoms fml = add_atoms true fml [];
1.24
1.25 -local
1.26 - val ac1 = mk_meta_eq @{thm add_assoc};
1.27 - val ac2 = mk_meta_eq @{thm add_commute};
1.28 - val ac3 = mk_meta_eq @{thm add_left_commute};
1.29 - fun solve_add_ac thy _ (_ $ (Const (@{const_name Groups.plus},_) $ _ $ _) $ _) =
1.30 - SOME ac1
1.31 - | solve_add_ac thy _ (_ $ x $ (Const (@{const_name Groups.plus},_) $ y $ z)) =
1.32 - if termless_agrp (y, x) then SOME ac3 else NONE
1.33 - | solve_add_ac thy _ (_ $ x $ y) =
1.34 - if termless_agrp (y, x) then SOME ac2 else NONE
1.35 - | solve_add_ac thy _ _ = NONE
1.36 -in
1.37 - val add_ac_proc = Simplifier.simproc @{theory}
1.38 - "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
1.39 -end;
1.40 -
1.41 -val cancel_ss = HOL_basic_ss settermless termless_agrp
1.42 - addsimprocs [add_ac_proc] addsimps
1.43 - [@{thm add_0_left}, @{thm add_0_right}, @{thm diff_minus},
1.44 - @{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero},
1.45 - @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},
1.46 - @{thm minus_add_cancel}];
1.47 -
1.48 -val eqI_rules = [@{thm diff_eq_diff_less}, @{thm diff_eq_diff_less_eq}, @{thm diff_eq_diff_eq}];
1.49 -
1.50 -fun zero t = Const (@{const_name Groups.zero}, t);
1.51 -fun minus t = Const (@{const_name Groups.uminus}, t --> t);
1.52 -
1.53 -fun add_terms pos (Const (@{const_name Groups.plus}, _) $ x $ y, ts) =
1.54 - add_terms pos (x, add_terms pos (y, ts))
1.55 - | add_terms pos (Const (@{const_name Groups.minus}, _) $ x $ y, ts) =
1.56 - add_terms pos (x, add_terms (not pos) (y, ts))
1.57 - | add_terms pos (Const (@{const_name Groups.uminus}, _) $ x, ts) =
1.58 - add_terms (not pos) (x, ts)
1.59 - | add_terms pos (x, ts) = (pos,x) :: ts;
1.60 -
1.61 -fun terms fml = add_terms true (fml, []);
1.62 -
1.63 -fun zero1 pt (u as (c as Const(@{const_name Groups.plus},_)) $ x $ y) =
1.64 +fun zero1 pt (c as Const (@{const_name Groups.plus}, _) $ x $ y) =
1.65 (case zero1 pt x of NONE => (case zero1 pt y of NONE => NONE
1.66 | SOME z => SOME(c $ x $ z))
1.67 - | SOME z => SOME(c $ z $ y))
1.68 - | zero1 (pos,t) (u as (c as Const(@{const_name Groups.minus},_)) $ x $ y) =
1.69 - (case zero1 (pos,t) x of
1.70 - NONE => (case zero1 (not pos,t) y of NONE => NONE
1.71 - | SOME z => SOME(c $ x $ z))
1.72 - | SOME z => SOME(c $ z $ y))
1.73 - | zero1 (pos,t) (u as (c as Const(@{const_name Groups.uminus},_)) $ x) =
1.74 - (case zero1 (not pos,t) x of NONE => NONE
1.75 - | SOME z => SOME(c $ z))
1.76 - | zero1 (pos,t) u =
1.77 - if pos andalso (t aconv u) then SOME(zero(fastype_of t)) else NONE
1.78 + | SOME z => SOME (c $ z $ y))
1.79 + | zero1 pt (c as Const (@{const_name Groups.minus}, _) $ x $ y) =
1.80 + (case zero1 pt x of
1.81 + NONE => (case zero1 (apfst not pt) y of NONE => NONE
1.82 + | SOME z => SOME (c $ x $ z))
1.83 + | SOME z => SOME (c $ z $ y))
1.84 + | zero1 pt (c as Const (@{const_name Groups.uminus}, _) $ x) =
1.85 + (case zero1 (apfst not pt) x of NONE => NONE
1.86 + | SOME z => SOME (c $ z))
1.87 + | zero1 (pos, t) u =
1.88 + if pos andalso (t aconv u)
1.89 + then SOME (Const (@{const_name Groups.zero}, fastype_of t))
1.90 + else NONE
1.91
1.92 exception Cancel;
1.93
1.94 fun find_common _ [] _ = raise Cancel
1.95 - | find_common opp ((p,l)::ls) rs =
1.96 + | find_common opp ((p, l) :: ls) rs =
1.97 let val pr = if opp then not p else p
1.98 - in if exists (fn (q,r) => pr = q andalso l aconv r) rs then (p,l)
1.99 + in if exists (fn (q, r) => pr = q andalso l aconv r) rs then (p, l)
1.100 else find_common opp ls rs
1.101 end
1.102
1.103 @@ -93,36 +60,73 @@
1.104 fun cancel t =
1.105 let
1.106 val c $ lhs $ rhs = t
1.107 - val opp = case c of Const(@{const_name Groups.plus},_) => true | _ => false;
1.108 - val (pos,l) = find_common opp (terms lhs) (terms rhs)
1.109 - val posr = if opp then not pos else pos
1.110 - val t' = c $ (the(zero1 (pos,l) lhs)) $ (the(zero1 (posr,l) rhs))
1.111 - in t' end;
1.112 + val opp = case c of Const(@{const_name Groups.plus}, _) => true | _ => false;
1.113 + val (pos, l) = find_common opp (atoms lhs) (atoms rhs);
1.114 + val posr = if opp then not pos else pos;
1.115 + in c $ the (zero1 (pos, l) lhs) $ the (zero1 (posr, l) rhs) end;
1.116
1.117
1.118 -(*A simproc to cancel complementary terms in arbitrary sums.*)
1.119 +(** prove cancellation **)
1.120 +
1.121 +fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')
1.122 + [@{const_name Groups.zero}, @{const_name Groups.plus},
1.123 + @{const_name Groups.uminus}, @{const_name Groups.minus}]
1.124 + | agrp_ord _ = ~1;
1.125 +
1.126 +fun less_agrp (a, b) = (Term_Ord.term_lpo agrp_ord (a, b) = LESS);
1.127 +
1.128 +fun solve (_ $ (Const (@{const_name Groups.plus}, _) $ _ $ _) $ _) =
1.129 + SOME @{thm add_assoc [THEN eq_reflection]}
1.130 + | solve (_ $ x $ (Const (@{const_name Groups.plus}, _) $ y $ _)) =
1.131 + if less_agrp (y, x) then
1.132 + SOME @{thm add_left_commute [THEN eq_reflection]}
1.133 + else NONE
1.134 + | solve (_ $ x $ y) =
1.135 + if less_agrp (y, x) then
1.136 + SOME @{thm add_commute [THEN eq_reflection]} else
1.137 + NONE
1.138 + | solve _ = NONE;
1.139 +
1.140 +val simproc = Simplifier.simproc @{theory}
1.141 + "add_ac_proc" ["x + y::'a::ab_semigroup_add"] ((K o K) solve);
1.142 +
1.143 +val cancel_ss = HOL_basic_ss settermless less_agrp
1.144 + addsimprocs [simproc] addsimps
1.145 + [@{thm add_0_left}, @{thm add_0_right}, @{thm diff_minus},
1.146 + @{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero},
1.147 + @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},
1.148 + @{thm minus_add_cancel}];
1.149 +
1.150 +fun cancel_simp_tac ss = simp_tac (Simplifier.inherit_context ss cancel_ss);
1.151 +
1.152 +
1.153 +(** simprocs **)
1.154 +
1.155 +(* cancel complementary terms in arbitrary sums *)
1.156 +
1.157 fun sum_proc ss ct =
1.158 let
1.159 val t = Thm.term_of ct;
1.160 val t' = cancel t;
1.161 val thm =
1.162 Goal.prove (Simplifier.the_context ss) [] [] (Logic.mk_equals (t, t'))
1.163 - (fn _ => simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
1.164 + (fn _ => cancel_simp_tac ss 1)
1.165 in SOME thm end handle Cancel => NONE;
1.166
1.167
1.168 -(*A simproc to cancel like terms on the opposite sides of relations:
1.169 - (x + y - z < -z + x) = (y < 0)
1.170 - Works for (=) and (<=) as well as (<), if the necessary rules are supplied.
1.171 - Reduces the problem to subtraction.*)
1.172 +(* cancel like terms on the opposite sides of relations:
1.173 + (x + y - z < -z + x) = (y < 0)
1.174 + Works for (=) and (<=) as well as (<), if the necessary rules are supplied.
1.175 + Reduces the problem to subtraction. *)
1.176 +
1.177 fun rel_proc ss ct =
1.178 let
1.179 val t = Thm.term_of ct;
1.180 val t' = cancel t;
1.181 val thm = Goal.prove (Simplifier.the_context ss) [] [] (Logic.mk_equals (t, t'))
1.182 (fn _ => rtac @{thm eq_reflection} 1 THEN
1.183 - resolve_tac eqI_rules 1 THEN
1.184 - simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
1.185 + resolve_tac [@{thm diff_eq_diff_less}, @{thm diff_eq_diff_less_eq}, @{thm diff_eq_diff_eq}] 1 THEN
1.186 + cancel_simp_tac ss 1)
1.187 in SOME thm end handle Cancel => NONE;
1.188
1.189 end;