18 (*A further rule to deal with the case that |
18 (*A further rule to deal with the case that |
19 everything gets cancelled on the right.*) |
19 everything gets cancelled on the right.*) |
20 val zadd_cancel_end = prove_goal IntDef.thy |
20 val zadd_cancel_end = prove_goal IntDef.thy |
21 "((x::int) + (y + z) = y) = (x = -z)" |
21 "((x::int) + (y + z) = y) = (x = -z)" |
22 (fn _ => [stac zadd_left_commute 1, |
22 (fn _ => [stac zadd_left_commute 1, |
23 res_inst_tac [("t", "y")] (zadd_nat0_right RS subst) 1, |
23 res_inst_tac [("t", "y")] (zadd_int0_right RS subst) 1, |
24 stac zadd_left_cancel 1, |
24 stac zadd_left_cancel 1, |
25 simp_tac (simpset() addsimps [eq_zdiff_eq RS sym]) 1]); |
25 simp_tac (simpset() addsimps [eq_zdiff_eq RS sym]) 1]); |
26 |
26 |
27 |
27 |
28 structure Int_Cancel_Data = |
28 structure Int_Cancel_Data = |
37 val add_cancel_end = zadd_cancel_end |
37 val add_cancel_end = zadd_cancel_end |
38 val add_left_cancel = zadd_left_cancel |
38 val add_left_cancel = zadd_left_cancel |
39 val add_assoc = zadd_assoc |
39 val add_assoc = zadd_assoc |
40 val add_commute = zadd_commute |
40 val add_commute = zadd_commute |
41 val add_left_commute = zadd_left_commute |
41 val add_left_commute = zadd_left_commute |
42 val add_0 = zadd_nat0 |
42 val add_0 = zadd_int0 |
43 val add_0_right = zadd_nat0_right |
43 val add_0_right = zadd_int0_right |
44 |
44 |
45 val eq_diff_eq = eq_zdiff_eq |
45 val eq_diff_eq = eq_zdiff_eq |
46 val eqI_rules = [zless_eqI, zeq_eqI, zle_eqI] |
46 val eqI_rules = [zless_eqI, zeq_eqI, zle_eqI] |
47 fun dest_eqI th = |
47 fun dest_eqI th = |
48 #1 (HOLogic.dest_bin "op =" HOLogic.boolT |
48 #1 (HOLogic.dest_bin "op =" HOLogic.boolT |
49 (HOLogic.dest_Trueprop (concl_of th))) |
49 (HOLogic.dest_Trueprop (concl_of th))) |
50 |
50 |
51 val diff_def = zdiff_def |
51 val diff_def = zdiff_def |
52 val minus_add_distrib = zminus_zadd_distrib |
52 val minus_add_distrib = zminus_zadd_distrib |
53 val minus_minus = zminus_zminus |
53 val minus_minus = zminus_zminus |
54 val minus_0 = zminus_nat0 |
54 val minus_0 = zminus_int0 |
55 val add_inverses = [zadd_zminus_inverse, zadd_zminus_inverse2]; |
55 val add_inverses = [zadd_zminus_inverse, zadd_zminus_inverse2]; |
56 val cancel_simps = [zadd_zminus_cancel, zminus_zadd_cancel] |
56 val cancel_simps = [zadd_zminus_cancel, zminus_zadd_cancel] |
57 end; |
57 end; |
58 |
58 |
59 structure Int_Cancel = Abel_Cancel (Int_Cancel_Data); |
59 structure Int_Cancel = Abel_Cancel (Int_Cancel_Data); |