equal
deleted
inserted
replaced
88 |
88 |
89 (* A simproc to cancel complementary terms in arbitrary sums. *) |
89 (* A simproc to cancel complementary terms in arbitrary sums. *) |
90 |
90 |
91 fun sum_proc sg ss t = |
91 fun sum_proc sg ss t = |
92 let val t' = cancel sg t |
92 let val t' = cancel sg t |
93 val thm = Tactic.prove sg [] [] (Logic.mk_equals (t, t')) |
93 val thm = Goal.prove sg [] [] (Logic.mk_equals (t, t')) |
94 (fn _ => simp_tac (Simplifier.inherit_context ss cancel_ss) 1) |
94 (fn _ => simp_tac (Simplifier.inherit_context ss cancel_ss) 1) |
95 in SOME thm end |
95 in SOME thm end |
96 handle Cancel => NONE; |
96 handle Cancel => NONE; |
97 |
97 |
98 val sum_conv = |
98 val sum_conv = |
108 Reduces the problem to subtraction. |
108 Reduces the problem to subtraction. |
109 *) |
109 *) |
110 |
110 |
111 fun rel_proc sg ss t = |
111 fun rel_proc sg ss t = |
112 let val t' = cancel sg t |
112 let val t' = cancel sg t |
113 val thm = Tactic.prove sg [] [] (Logic.mk_equals (t, t')) |
113 val thm = Goal.prove sg [] [] (Logic.mk_equals (t, t')) |
114 (fn _ => rtac eq_reflection 1 THEN |
114 (fn _ => rtac eq_reflection 1 THEN |
115 resolve_tac eqI_rules 1 THEN |
115 resolve_tac eqI_rules 1 THEN |
116 simp_tac (Simplifier.inherit_context ss cancel_ss) 1) |
116 simp_tac (Simplifier.inherit_context ss cancel_ss) 1) |
117 in SOME thm end |
117 in SOME thm end |
118 handle Cancel => NONE; |
118 handle Cancel => NONE; |