1 theory IntEx |
|
2 imports "../Quotient_Product" "../Quotient_List" |
|
3 begin |
|
4 |
|
5 fun |
|
6 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |
|
7 where |
|
8 "intrel (x, y) (u, v) = (x + v = u + y)" |
|
9 |
|
10 quotient_type |
|
11 my_int = "nat \<times> nat" / intrel |
|
12 apply(unfold equivp_def) |
|
13 apply(auto simp add: mem_def expand_fun_eq) |
|
14 done |
|
15 |
|
16 quotient_definition |
|
17 "ZERO :: my_int" |
|
18 is |
|
19 "(0::nat, 0::nat)" |
|
20 |
|
21 quotient_definition |
|
22 "ONE :: my_int" |
|
23 is |
|
24 "(1::nat, 0::nat)" |
|
25 |
|
26 fun |
|
27 my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
|
28 where |
|
29 "my_plus (x, y) (u, v) = (x + u, y + v)" |
|
30 |
|
31 quotient_definition |
|
32 "PLUS :: my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
|
33 is |
|
34 "my_plus" |
|
35 |
|
36 fun |
|
37 my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
|
38 where |
|
39 "my_neg (x, y) = (y, x)" |
|
40 |
|
41 quotient_definition |
|
42 "NEG :: my_int \<Rightarrow> my_int" |
|
43 is |
|
44 "my_neg" |
|
45 |
|
46 definition |
|
47 MINUS :: "my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
|
48 where |
|
49 "MINUS z w = PLUS z (NEG w)" |
|
50 |
|
51 fun |
|
52 my_mult :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
|
53 where |
|
54 "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)" |
|
55 |
|
56 quotient_definition |
|
57 "MULT :: my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
|
58 is |
|
59 "my_mult" |
|
60 |
|
61 |
|
62 (* NOT SURE WETHER THIS DEFINITION IS CORRECT *) |
|
63 fun |
|
64 my_le :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
|
65 where |
|
66 "my_le (x, y) (u, v) = (x+v \<le> u+y)" |
|
67 |
|
68 quotient_definition |
|
69 "LE :: my_int \<Rightarrow> my_int \<Rightarrow> bool" |
|
70 is |
|
71 "my_le" |
|
72 |
|
73 term LE |
|
74 thm LE_def |
|
75 |
|
76 |
|
77 definition |
|
78 LESS :: "my_int \<Rightarrow> my_int \<Rightarrow> bool" |
|
79 where |
|
80 "LESS z w = (LE z w \<and> z \<noteq> w)" |
|
81 |
|
82 term LESS |
|
83 thm LESS_def |
|
84 |
|
85 definition |
|
86 ABS :: "my_int \<Rightarrow> my_int" |
|
87 where |
|
88 "ABS i = (if (LESS i ZERO) then (NEG i) else i)" |
|
89 |
|
90 definition |
|
91 SIGN :: "my_int \<Rightarrow> my_int" |
|
92 where |
|
93 "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))" |
|
94 |
|
95 print_quotconsts |
|
96 |
|
97 lemma plus_sym_pre: |
|
98 shows "my_plus a b \<approx> my_plus b a" |
|
99 apply(cases a) |
|
100 apply(cases b) |
|
101 apply(auto) |
|
102 done |
|
103 |
|
104 lemma plus_rsp[quot_respect]: |
|
105 shows "(intrel ===> intrel ===> intrel) my_plus my_plus" |
|
106 by (simp) |
|
107 |
|
108 lemma neg_rsp[quot_respect]: |
|
109 shows "(op \<approx> ===> op \<approx>) my_neg my_neg" |
|
110 by simp |
|
111 |
|
112 lemma test1: "my_plus a b = my_plus a b" |
|
113 apply(rule refl) |
|
114 done |
|
115 |
|
116 lemma "PLUS a b = PLUS a b" |
|
117 apply(lifting_setup test1) |
|
118 apply(regularize) |
|
119 apply(injection) |
|
120 apply(cleaning) |
|
121 done |
|
122 |
|
123 thm lambda_prs |
|
124 |
|
125 lemma test2: "my_plus a = my_plus a" |
|
126 apply(rule refl) |
|
127 done |
|
128 |
|
129 lemma "PLUS a = PLUS a" |
|
130 apply(lifting_setup test2) |
|
131 apply(rule impI) |
|
132 apply(rule ballI) |
|
133 apply(rule apply_rsp[OF Quotient_my_int plus_rsp]) |
|
134 apply(simp only: in_respects) |
|
135 apply(injection) |
|
136 apply(cleaning) |
|
137 done |
|
138 |
|
139 lemma test3: "my_plus = my_plus" |
|
140 apply(rule refl) |
|
141 done |
|
142 |
|
143 lemma "PLUS = PLUS" |
|
144 apply(lifting_setup test3) |
|
145 apply(rule impI) |
|
146 apply(rule plus_rsp) |
|
147 apply(injection) |
|
148 apply(cleaning) |
|
149 done |
|
150 |
|
151 |
|
152 lemma "PLUS a b = PLUS b a" |
|
153 apply(lifting plus_sym_pre) |
|
154 done |
|
155 |
|
156 lemma plus_assoc_pre: |
|
157 shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)" |
|
158 apply (cases i) |
|
159 apply (cases j) |
|
160 apply (cases k) |
|
161 apply (simp) |
|
162 done |
|
163 |
|
164 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" |
|
165 apply(lifting plus_assoc_pre) |
|
166 done |
|
167 |
|
168 lemma ex1tst: "Bex1_rel (op \<approx>) (\<lambda>x :: nat \<times> nat. x \<approx> x)" |
|
169 sorry |
|
170 |
|
171 lemma ex1tst': "\<exists>!(x::my_int). x = x" |
|
172 apply(lifting ex1tst) |
|
173 done |
|
174 |
|
175 |
|
176 lemma ho_tst: "foldl my_plus x [] = x" |
|
177 apply simp |
|
178 done |
|
179 |
|
180 |
|
181 term foldl |
|
182 lemma "foldl PLUS x [] = x" |
|
183 apply(lifting ho_tst) |
|
184 done |
|
185 |
|
186 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)" |
|
187 sorry |
|
188 |
|
189 lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)" |
|
190 apply(lifting ho_tst2) |
|
191 done |
|
192 |
|
193 lemma ho_tst3: "foldl f (s::nat \<times> nat) ([]::(nat \<times> nat) list) = s" |
|
194 by simp |
|
195 |
|
196 lemma "foldl f (x::my_int) ([]::my_int list) = x" |
|
197 apply(lifting ho_tst3) |
|
198 done |
|
199 |
|
200 lemma lam_tst: "(\<lambda>x. (x, x)) y = (y, (y :: nat \<times> nat))" |
|
201 by simp |
|
202 |
|
203 (* Don't know how to keep the goal non-contracted... *) |
|
204 lemma "(\<lambda>x. (x, x)) (y::my_int) = (y, y)" |
|
205 apply(lifting lam_tst) |
|
206 done |
|
207 |
|
208 lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)" |
|
209 by simp |
|
210 |
|
211 lemma |
|
212 shows "equivp (op \<approx>)" |
|
213 and "equivp ((op \<approx>) ===> (op \<approx>))" |
|
214 (* Nitpick finds a counterexample! *) |
|
215 oops |
|
216 |
|
217 lemma lam_tst3a: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)" |
|
218 by auto |
|
219 |
|
220 lemma id_rsp: |
|
221 shows "(R ===> R) id id" |
|
222 by simp |
|
223 |
|
224 lemma lam_tst3a_reg: "(op \<approx> ===> op \<approx>) (Babs (Respects op \<approx>) (\<lambda>y. y)) (Babs (Respects op \<approx>) (\<lambda>x. x))" |
|
225 apply (rule babs_rsp[OF Quotient_my_int]) |
|
226 apply (simp add: id_rsp) |
|
227 done |
|
228 |
|
229 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)" |
|
230 apply(lifting lam_tst3a) |
|
231 apply(rule impI) |
|
232 apply(rule lam_tst3a_reg) |
|
233 done |
|
234 |
|
235 lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)" |
|
236 by auto |
|
237 |
|
238 lemma "(\<lambda>(y :: my_int => my_int). y) = (\<lambda>(x :: my_int => my_int). x)" |
|
239 apply(lifting lam_tst3b) |
|
240 apply(rule impI) |
|
241 apply(rule babs_rsp[OF fun_quotient[OF Quotient_my_int Quotient_my_int]]) |
|
242 apply(simp add: id_rsp) |
|
243 done |
|
244 |
|
245 lemma lam_tst4: "map (\<lambda>x. my_plus x (0,0)) l = l" |
|
246 apply (induct l) |
|
247 apply simp |
|
248 apply (case_tac a) |
|
249 apply simp |
|
250 done |
|
251 |
|
252 lemma "map (\<lambda>x. PLUS x ZERO) l = l" |
|
253 apply(lifting lam_tst4) |
|
254 done |
|
255 |
|
256 end |
|