author | oheimb |
Fri, 23 Oct 1998 20:44:34 +0200 | |
changeset 5758 | 27a2b36efd95 |
parent 5561 | 426c1e330903 |
child 6153 | bff90585cce5 |
permissions | -rw-r--r-- |
5561
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
1 |
(* Title: ZF/Integ/Int.ML |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
4 |
Copyright 1993 University of Cambridge |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
5 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
6 |
The integers as equivalence classes over nat*nat. |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
7 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
8 |
Could also prove... |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
9 |
"znegative(z) ==> $# zmagnitude(z) = $~ z" |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
10 |
"~ znegative(z) ==> $# zmagnitude(z) = z" |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
11 |
$< is a linear ordering |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
12 |
$+ and $* are monotonic wrt $< |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
13 |
*) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
14 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
15 |
AddSEs [quotientE]; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
16 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
17 |
(*** Proving that intrel is an equivalence relation ***) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
18 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
19 |
(*By luck, requires no typing premises for y1, y2,y3*) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
20 |
val eqa::eqb::prems = goal Arith.thy |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
21 |
"[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2; \ |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
22 |
\ x1: nat; x2: nat; x3: nat |] ==> x1 #+ y3 = x3 #+ y1"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
23 |
by (res_inst_tac [("k","x2")] add_left_cancel 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
24 |
by (resolve_tac prems 2); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
25 |
by (rtac (add_left_commute RS trans) 1 THEN typechk_tac prems); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
26 |
by (stac eqb 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
27 |
by (rtac (add_left_commute RS trans) 1 THEN typechk_tac prems); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
28 |
by (stac eqa 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
29 |
by (rtac (add_left_commute) 1 THEN typechk_tac prems); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
30 |
qed "int_trans_lemma"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
31 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
32 |
(** Natural deduction for intrel **) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
33 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
34 |
Goalw [intrel_def] |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
35 |
"<<x1,y1>,<x2,y2>>: intrel <-> \ |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
36 |
\ x1: nat & y1: nat & x2: nat & y2: nat & x1#+y2 = x2#+y1"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
37 |
by (Fast_tac 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
38 |
qed "intrel_iff"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
39 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
40 |
Goalw [intrel_def] |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
41 |
"[| x1#+y2 = x2#+y1; x1: nat; y1: nat; x2: nat; y2: nat |] ==> \ |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
42 |
\ <<x1,y1>,<x2,y2>>: intrel"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
43 |
by (fast_tac (claset() addIs prems) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
44 |
qed "intrelI"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
45 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
46 |
(*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
47 |
Goalw [intrel_def] |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
48 |
"p: intrel --> (EX x1 y1 x2 y2. \ |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
49 |
\ p = <<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1 & \ |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
50 |
\ x1: nat & y1: nat & x2: nat & y2: nat)"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
51 |
by (Fast_tac 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
52 |
qed "intrelE_lemma"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
53 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
54 |
val [major,minor] = goal thy |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
55 |
"[| p: intrel; \ |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
56 |
\ !!x1 y1 x2 y2. [| p = <<x1,y1>,<x2,y2>>; x1#+y2 = x2#+y1; \ |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
57 |
\ x1: nat; y1: nat; x2: nat; y2: nat |] ==> Q |] \ |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
58 |
\ ==> Q"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
59 |
by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
60 |
by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1)); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
61 |
qed "intrelE"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
62 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
63 |
AddSIs [intrelI]; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
64 |
AddSEs [intrelE]; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
65 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
66 |
Goalw [equiv_def, refl_def, sym_def, trans_def] |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
67 |
"equiv(nat*nat, intrel)"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
68 |
by (fast_tac (claset() addSEs [sym, int_trans_lemma]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
69 |
qed "equiv_intrel"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
70 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
71 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
72 |
Addsimps [equiv_intrel RS eq_equiv_class_iff, intrel_iff, |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
73 |
add_0_right, add_succ_right]; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
74 |
Addcongs [conj_cong]; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
75 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
76 |
val eq_intrelD = equiv_intrel RSN (2,eq_equiv_class); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
77 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
78 |
(** int_of: the injection from nat to int **) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
79 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
80 |
Goalw [int_def,quotient_def,int_of_def] |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
81 |
"m : nat ==> $#m : int"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
82 |
by (fast_tac (claset() addSIs [nat_0I]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
83 |
qed "int_of_type"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
84 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
85 |
Addsimps [int_of_type]; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
86 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
87 |
Goalw [int_of_def] "[| $#m = $#n; m: nat |] ==> m=n"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
88 |
by (dtac (sym RS eq_intrelD) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
89 |
by (typechk_tac [nat_0I, SigmaI]); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
90 |
by (Asm_full_simp_tac 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
91 |
qed "int_of_inject"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
92 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
93 |
AddSDs [int_of_inject]; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
94 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
95 |
Goal "m: nat ==> ($# m = $# n) <-> (m = n)"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
96 |
by (Blast_tac 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
97 |
qed "int_of_eq"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
98 |
Addsimps [int_of_eq]; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
99 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
100 |
(**** zminus: unary negation on int ****) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
101 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
102 |
Goalw [congruent_def] "congruent(intrel, %<x,y>. intrel``{<y,x>})"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
103 |
by Safe_tac; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
104 |
by (asm_full_simp_tac (simpset() addsimps add_ac) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
105 |
qed "zminus_congruent"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
106 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
107 |
(*Resolve th against the corresponding facts for zminus*) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
108 |
val zminus_ize = RSLIST [equiv_intrel, zminus_congruent]; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
109 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
110 |
Goalw [int_def,zminus_def] "z : int ==> $~z : int"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
111 |
by (typechk_tac [split_type, SigmaI, zminus_ize UN_equiv_class_type, |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
112 |
quotientI]); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
113 |
qed "zminus_type"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
114 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
115 |
Goalw [int_def,zminus_def] "[| $~z = $~w; z: int; w: int |] ==> z=w"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
116 |
by (etac (zminus_ize UN_equiv_class_inject) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
117 |
by Safe_tac; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
118 |
(*The setloop is only needed because assumptions are in the wrong order!*) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
119 |
by (asm_full_simp_tac (simpset() addsimps add_ac |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
120 |
setloop dtac eq_intrelD) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
121 |
qed "zminus_inject"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
122 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
123 |
Goalw [zminus_def] |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
124 |
"[| x: nat; y: nat |] ==> $~ (intrel``{<x,y>}) = intrel `` {<y,x>}"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
125 |
by (asm_simp_tac (simpset() addsimps [zminus_ize UN_equiv_class, SigmaI]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
126 |
qed "zminus"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
127 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
128 |
Goalw [int_def] "z : int ==> $~ ($~ z) = z"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
129 |
by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
130 |
by (asm_simp_tac (simpset() addsimps [zminus]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
131 |
qed "zminus_zminus"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
132 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
133 |
Goalw [int_def, int_of_def] "$~ ($#0) = $#0"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
134 |
by (simp_tac (simpset() addsimps [zminus]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
135 |
qed "zminus_0"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
136 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
137 |
Addsimps [zminus_zminus, zminus_0]; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
138 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
139 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
140 |
(**** znegative: the test for negative integers ****) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
141 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
142 |
(*No natural number is negative!*) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
143 |
Goalw [znegative_def, int_of_def] "~ znegative($# n)"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
144 |
by Safe_tac; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
145 |
by (dres_inst_tac [("psi", "?lhs=?rhs")] asm_rl 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
146 |
by (dres_inst_tac [("psi", "?lhs<?rhs")] asm_rl 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
147 |
by (force_tac (claset(), |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
148 |
simpset() addsimps [add_le_self2 RS le_imp_not_lt]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
149 |
qed "not_znegative_int_of"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
150 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
151 |
Addsimps [not_znegative_int_of]; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
152 |
AddSEs [not_znegative_int_of RS notE]; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
153 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
154 |
Goalw [znegative_def, int_of_def] "n: nat ==> znegative($~ $# succ(n))"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
155 |
by (asm_simp_tac (simpset() addsimps [zminus]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
156 |
by (blast_tac (claset() addIs [nat_0_le]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
157 |
qed "znegative_zminus_int_of"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
158 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
159 |
Addsimps [znegative_zminus_int_of]; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
160 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
161 |
Goalw [znegative_def, int_of_def] "[| n: nat; ~ znegative($~ $# n) |] ==> n=0"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
162 |
by (asm_full_simp_tac (simpset() addsimps [zminus, image_singleton_iff]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
163 |
be natE 1; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
164 |
by (dres_inst_tac [("x","0")] spec 2); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
165 |
by Auto_tac; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
166 |
qed "not_znegative_imp_zero"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
167 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
168 |
(**** zmagnitude: magnitide of an integer, as a natural number ****) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
169 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
170 |
Goalw [zmagnitude_def] "n: nat ==> zmagnitude($# n) = n"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
171 |
by Auto_tac; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
172 |
qed "zmagnitude_int_of"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
173 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
174 |
Goalw [zmagnitude_def] "n: nat ==> zmagnitude($~ $# n) = n"; |
5758
27a2b36efd95
corrected auto_tac (applications of unsafe wrappers)
oheimb
parents:
5561
diff
changeset
|
175 |
by (force_tac(claset() addDs [not_znegative_imp_zero], simpset())1); |
5561
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
176 |
qed "zmagnitude_zminus_int_of"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
177 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
178 |
Addsimps [zmagnitude_int_of, zmagnitude_zminus_int_of]; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
179 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
180 |
Goalw [zmagnitude_def] "zmagnitude(z) : nat"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
181 |
br theI2 1; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
182 |
by Auto_tac; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
183 |
qed "zmagnitude_type"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
184 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
185 |
Goalw [int_def, znegative_def, int_of_def] |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
186 |
"[| z: int; ~ znegative(z) |] ==> EX n:nat. z = $# n"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
187 |
by (auto_tac(claset() , simpset() addsimps [image_singleton_iff])); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
188 |
by (rename_tac "i j" 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
189 |
by (dres_inst_tac [("x", "i")] spec 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
190 |
by (dres_inst_tac [("x", "j")] spec 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
191 |
br bexI 1; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
192 |
br (add_diff_inverse2 RS sym) 1; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
193 |
by Auto_tac; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
194 |
by (asm_full_simp_tac (simpset() addsimps [nat_into_Ord, not_lt_iff_le]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
195 |
qed "not_zneg_int_of"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
196 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
197 |
Goal "[| z: int; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
198 |
bd not_zneg_int_of 1; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
199 |
by Auto_tac; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
200 |
qed "not_zneg_mag"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
201 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
202 |
Addsimps [not_zneg_mag]; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
203 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
204 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
205 |
Goalw [int_def, znegative_def, int_of_def] |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
206 |
"[| z: int; znegative(z) |] ==> EX n:nat. z = $~ ($# succ(n))"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
207 |
by (auto_tac(claset() addSDs [less_imp_Suc_add], |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
208 |
simpset() addsimps [zminus, image_singleton_iff])); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
209 |
by (rename_tac "m n j k" 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
210 |
by (subgoal_tac "j #+ succ(m #+ k) = j #+ n" 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
211 |
by (rotate_tac ~2 2); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
212 |
by (asm_full_simp_tac (simpset() addsimps add_ac) 2); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
213 |
by (blast_tac (claset() addSDs [add_left_cancel]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
214 |
qed "zneg_int_of"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
215 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
216 |
Goal "[| z: int; znegative(z) |] ==> $# (zmagnitude(z)) = $~ z"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
217 |
bd zneg_int_of 1; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
218 |
by Auto_tac; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
219 |
qed "zneg_mag"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
220 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
221 |
Addsimps [zneg_mag]; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
222 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
223 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
224 |
(**** zadd: addition on int ****) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
225 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
226 |
(** Congruence property for addition **) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
227 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
228 |
Goalw [congruent2_def] |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
229 |
"congruent2(intrel, %z1 z2. \ |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
230 |
\ let <x1,y1>=z1; <x2,y2>=z2 \ |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
231 |
\ in intrel``{<x1#+x2, y1#+y2>})"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
232 |
(*Proof via congruent2_commuteI seems longer*) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
233 |
by Safe_tac; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
234 |
by (asm_simp_tac (simpset() addsimps [add_assoc, Let_def]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
235 |
(*The rest should be trivial, but rearranging terms is hard; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
236 |
add_ac does not help rewriting with the assumptions.*) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
237 |
by (res_inst_tac [("m1","x1a")] (add_left_commute RS ssubst) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
238 |
by (res_inst_tac [("m1","x2a")] (add_left_commute RS ssubst) 3); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
239 |
by (typechk_tac [add_type]); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
240 |
by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
241 |
qed "zadd_congruent2"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
242 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
243 |
(*Resolve th against the corresponding facts for zadd*) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
244 |
val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2]; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
245 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
246 |
Goalw [int_def,zadd_def] "[| z: int; w: int |] ==> z $+ w : int"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
247 |
by (rtac (zadd_ize UN_equiv_class_type2) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
248 |
by (simp_tac (simpset() addsimps [Let_def]) 3); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
249 |
by (REPEAT (ares_tac [split_type, add_type, quotientI, SigmaI] 1)); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
250 |
qed "zadd_type"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
251 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
252 |
Goalw [zadd_def] |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
253 |
"[| x1: nat; y1: nat; x2: nat; y2: nat |] ==> \ |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
254 |
\ (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) = \ |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
255 |
\ intrel `` {<x1#+x2, y1#+y2>}"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
256 |
by (asm_simp_tac (simpset() addsimps [zadd_ize UN_equiv_class2, SigmaI]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
257 |
by (simp_tac (simpset() addsimps [Let_def]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
258 |
qed "zadd"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
259 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
260 |
Goalw [int_def,int_of_def] "z : int ==> $#0 $+ z = z"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
261 |
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
262 |
by (asm_simp_tac (simpset() addsimps [zadd]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
263 |
qed "zadd_0"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
264 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
265 |
Goalw [int_def] "[| z: int; w: int |] ==> $~ (z $+ w) = $~ z $+ $~ w"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
266 |
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
267 |
by (asm_simp_tac (simpset() addsimps [zminus,zadd]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
268 |
qed "zminus_zadd_distrib"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
269 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
270 |
Goalw [int_def] "[| z: int; w: int |] ==> z $+ w = w $+ z"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
271 |
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
272 |
by (asm_simp_tac (simpset() addsimps add_ac @ [zadd]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
273 |
qed "zadd_commute"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
274 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
275 |
Goalw [int_def] |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
276 |
"[| z1: int; z2: int; z3: int |] \ |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
277 |
\ ==> (z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
278 |
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
279 |
(*rewriting is much faster without intrel_iff, etc.*) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
280 |
by (asm_simp_tac (simpset() addsimps [zadd, add_assoc]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
281 |
qed "zadd_assoc"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
282 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
283 |
(*For AC rewriting*) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
284 |
Goal "[| z1:int; z2:int; z3: int |] ==> z1$+(z2$+z3) = z2$+(z1$+z3)"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
285 |
by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym, zadd_commute]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
286 |
qed "zadd_left_commute"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
287 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
288 |
(*Integer addition is an AC operator*) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
289 |
val zadd_ac = [zadd_assoc, zadd_commute, zadd_left_commute]; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
290 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
291 |
Goalw [int_of_def] |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
292 |
"[| m: nat; n: nat |] ==> $# (m #+ n) = ($#m) $+ ($#n)"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
293 |
by (asm_simp_tac (simpset() addsimps [zadd]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
294 |
qed "int_of_add"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
295 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
296 |
Goalw [int_def,int_of_def] "z : int ==> z $+ ($~ z) = $#0"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
297 |
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
298 |
by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
299 |
qed "zadd_zminus_inverse"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
300 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
301 |
Goal "z : int ==> ($~ z) $+ z = $#0"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
302 |
by (asm_simp_tac |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
303 |
(simpset() addsimps [zadd_commute, zminus_type, zadd_zminus_inverse]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
304 |
qed "zadd_zminus_inverse2"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
305 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
306 |
Goal "z:int ==> z $+ $#0 = z"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
307 |
by (rtac (zadd_commute RS trans) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
308 |
by (REPEAT (ares_tac [int_of_type, nat_0I, zadd_0] 1)); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
309 |
qed "zadd_0_right"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
310 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
311 |
Addsimps [zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2]; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
312 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
313 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
314 |
(*Need properties of $- ??? Or use $- just as an abbreviation? |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
315 |
[| m: nat; n: nat; m>=n |] ==> $# (m #- n) = ($#m) $- ($#n) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
316 |
*) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
317 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
318 |
(**** zmult: multiplication on int ****) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
319 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
320 |
(** Congruence property for multiplication **) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
321 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
322 |
Goal "congruent2(intrel, %p1 p2. \ |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
323 |
\ split(%x1 y1. split(%x2 y2. \ |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
324 |
\ intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
325 |
by (rtac (equiv_intrel RS congruent2_commuteI) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
326 |
by Safe_tac; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
327 |
by (ALLGOALS Asm_simp_tac); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
328 |
(*Proof that zmult is congruent in one argument*) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
329 |
by (asm_simp_tac |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
330 |
(simpset() addsimps add_ac @ [add_mult_distrib_left RS sym]) 2); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
331 |
by (asm_simp_tac |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
332 |
(simpset() addsimps [add_assoc RS sym, add_mult_distrib_left RS sym]) 2); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
333 |
(*Proof that zmult is commutative on representatives*) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
334 |
by (asm_simp_tac (simpset() addsimps mult_ac@add_ac) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
335 |
qed "zmult_congruent2"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
336 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
337 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
338 |
(*Resolve th against the corresponding facts for zmult*) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
339 |
val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2]; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
340 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
341 |
Goalw [int_def,zmult_def] "[| z: int; w: int |] ==> z $* w : int"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
342 |
by (REPEAT (ares_tac [zmult_ize UN_equiv_class_type2, |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
343 |
split_type, add_type, mult_type, |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
344 |
quotientI, SigmaI] 1)); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
345 |
qed "zmult_type"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
346 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
347 |
Goalw [zmult_def] |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
348 |
"[| x1: nat; y1: nat; x2: nat; y2: nat |] ==> \ |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
349 |
\ (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) = \ |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
350 |
\ intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
351 |
by (asm_simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2, SigmaI]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
352 |
qed "zmult"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
353 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
354 |
Goalw [int_def,int_of_def] "z : int ==> $#0 $* z = $#0"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
355 |
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
356 |
by (asm_simp_tac (simpset() addsimps [zmult]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
357 |
qed "zmult_0"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
358 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
359 |
Goalw [int_def,int_of_def] "z : int ==> $#1 $* z = z"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
360 |
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
361 |
by (asm_simp_tac (simpset() addsimps [zmult, add_0_right]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
362 |
qed "zmult_1"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
363 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
364 |
Goalw [int_def] "[| z: int; w: int |] ==> ($~ z) $* w = $~ (z $* w)"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
365 |
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
366 |
by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
367 |
qed "zmult_zminus"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
368 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
369 |
Addsimps [zmult_0, zmult_1, zmult_zminus]; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
370 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
371 |
Goalw [int_def] "[| z: int; w: int |] ==> ($~ z) $* ($~ w) = (z $* w)"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
372 |
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
373 |
by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
374 |
qed "zmult_zminus_zminus"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
375 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
376 |
Goalw [int_def] "[| z: int; w: int |] ==> z $* w = w $* z"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
377 |
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
378 |
by (asm_simp_tac (simpset() addsimps [zmult] @ add_ac @ mult_ac) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
379 |
qed "zmult_commute"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
380 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
381 |
Goalw [int_def] |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
382 |
"[| z1: int; z2: int; z3: int |] \ |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
383 |
\ ==> (z1 $* z2) $* z3 = z1 $* (z2 $* z3)"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
384 |
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
385 |
by (asm_simp_tac |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
386 |
(simpset() addsimps [zmult, add_mult_distrib_left, |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
387 |
add_mult_distrib] @ add_ac @ mult_ac) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
388 |
qed "zmult_assoc"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
389 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
390 |
(*For AC rewriting*) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
391 |
Goal "[| z1:int; z2:int; z3: int |] ==> z1$*(z2$*z3) = z2$*(z1$*z3)"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
392 |
by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym, zmult_commute]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
393 |
qed "zmult_left_commute"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
394 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
395 |
(*Integer multiplication is an AC operator*) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
396 |
val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute]; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
397 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
398 |
Goalw [int_def] |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
399 |
"[| z1: int; z2: int; w: int |] ==> \ |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
400 |
\ (z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
401 |
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
402 |
by (asm_simp_tac (simpset() addsimps [zadd, zmult, add_mult_distrib]) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
403 |
by (asm_simp_tac (simpset() addsimps add_ac @ mult_ac) 1); |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
404 |
qed "zadd_zmult_distrib"; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
405 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
406 |
val int_typechecks = |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
407 |
[int_of_type, zminus_type, zmagnitude_type, zadd_type, zmult_type]; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
408 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
409 |
Addsimps int_typechecks; |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
410 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
411 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
412 |