5588
|
1 |
(* Title: HOL/Real/simproc.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1998 University of Cambridge
|
|
5 |
|
|
6 |
Apply Abel_Cancel to the reals
|
|
7 |
*)
|
|
8 |
|
|
9 |
(*** Two lemmas needed for the simprocs ***)
|
|
10 |
|
|
11 |
(*Deletion of other terms in the formula, seeking the -x at the front of z*)
|
7585
|
12 |
Goal "((x::real) + (y + z) = y + u) = ((x + z) = u)";
|
|
13 |
by (stac real_add_left_commute 1);
|
|
14 |
by (rtac real_add_left_cancel 1);
|
|
15 |
qed "real_add_cancel_21";
|
5588
|
16 |
|
|
17 |
(*A further rule to deal with the case that
|
|
18 |
everything gets cancelled on the right.*)
|
7585
|
19 |
Goal "((x::real) + (y + z) = y) = (x = -z)";
|
|
20 |
by (stac real_add_left_commute 1);
|
|
21 |
by (res_inst_tac [("t", "y")] (real_add_zero_right RS subst) 1
|
|
22 |
THEN stac real_add_left_cancel 1);
|
|
23 |
by (simp_tac (simpset() addsimps [real_eq_diff_eq RS sym]) 1);
|
|
24 |
qed "real_add_cancel_end";
|
5588
|
25 |
|
|
26 |
|
|
27 |
structure Real_Cancel_Data =
|
|
28 |
struct
|
|
29 |
val ss = HOL_ss
|
5610
|
30 |
val eq_reflection = eq_reflection
|
5588
|
31 |
|
|
32 |
val thy = RealDef.thy
|
|
33 |
val T = Type ("RealDef.real", [])
|
|
34 |
val zero = Const ("RealDef.0r", T)
|
7585
|
35 |
val restrict_to_left = restrict_to_left
|
5588
|
36 |
val add_cancel_21 = real_add_cancel_21
|
|
37 |
val add_cancel_end = real_add_cancel_end
|
|
38 |
val add_left_cancel = real_add_left_cancel
|
|
39 |
val add_assoc = real_add_assoc
|
|
40 |
val add_commute = real_add_commute
|
|
41 |
val add_left_commute = real_add_left_commute
|
|
42 |
val add_0 = real_add_zero_left
|
|
43 |
val add_0_right = real_add_zero_right
|
|
44 |
|
|
45 |
val eq_diff_eq = real_eq_diff_eq
|
|
46 |
val eqI_rules = [real_less_eqI, real_eq_eqI, real_le_eqI]
|
|
47 |
fun dest_eqI th =
|
|
48 |
#1 (HOLogic.dest_bin "op =" HOLogic.boolT
|
|
49 |
(HOLogic.dest_Trueprop (concl_of th)))
|
|
50 |
|
|
51 |
val diff_def = real_diff_def
|
|
52 |
val minus_add_distrib = real_minus_add_distrib
|
|
53 |
val minus_minus = real_minus_minus
|
|
54 |
val minus_0 = real_minus_zero
|
|
55 |
val add_inverses = [real_add_minus, real_add_minus_left];
|
|
56 |
val cancel_simps = [real_add_minus_cancel, real_minus_add_cancel]
|
|
57 |
end;
|
|
58 |
|
|
59 |
structure Real_Cancel = Abel_Cancel (Real_Cancel_Data);
|
|
60 |
|
|
61 |
Addsimprocs [Real_Cancel.sum_conv, Real_Cancel.rel_conv];
|
|
62 |
|