|
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 int_induct_raw: |
|
169 assumes a: "P (0::nat, 0)" |
|
170 and b: "\<And>i. P i \<Longrightarrow> P (my_plus i (1,0))" |
|
171 and c: "\<And>i. P i \<Longrightarrow> P (my_plus i (my_neg (1,0)))" |
|
172 shows "P x" |
|
173 apply(case_tac x) apply(simp) |
|
174 apply(rule_tac x="b" in spec) |
|
175 apply(rule_tac Nat.induct) |
|
176 apply(rule allI) |
|
177 apply(rule_tac Nat.induct) |
|
178 using a b c apply(auto) |
|
179 done |
|
180 |
|
181 lemma int_induct: |
|
182 assumes a: "P ZERO" |
|
183 and b: "\<And>i. P i \<Longrightarrow> P (PLUS i ONE)" |
|
184 and c: "\<And>i. P i \<Longrightarrow> P (PLUS i (NEG ONE))" |
|
185 shows "P x" |
|
186 using a b c |
|
187 by (lifting int_induct_raw) |
|
188 |
|
189 lemma ex1tst: "Bex1_rel (op \<approx>) (\<lambda>x :: nat \<times> nat. x \<approx> x)" |
|
190 sorry |
|
191 |
|
192 lemma ex1tst': "\<exists>!(x::my_int). x = x" |
|
193 apply(lifting ex1tst) |
|
194 done |
|
195 |
|
196 |
|
197 lemma ho_tst: "foldl my_plus x [] = x" |
|
198 apply simp |
|
199 done |
|
200 |
|
201 |
|
202 term foldl |
|
203 lemma "foldl PLUS x [] = x" |
|
204 apply(lifting ho_tst) |
|
205 done |
|
206 |
|
207 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)" |
|
208 sorry |
|
209 |
|
210 lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)" |
|
211 apply(lifting ho_tst2) |
|
212 done |
|
213 |
|
214 lemma ho_tst3: "foldl f (s::nat \<times> nat) ([]::(nat \<times> nat) list) = s" |
|
215 by simp |
|
216 |
|
217 lemma "foldl f (x::my_int) ([]::my_int list) = x" |
|
218 apply(lifting ho_tst3) |
|
219 done |
|
220 |
|
221 lemma lam_tst: "(\<lambda>x. (x, x)) y = (y, (y :: nat \<times> nat))" |
|
222 by simp |
|
223 |
|
224 (* Don't know how to keep the goal non-contracted... *) |
|
225 lemma "(\<lambda>x. (x, x)) (y::my_int) = (y, y)" |
|
226 apply(lifting lam_tst) |
|
227 done |
|
228 |
|
229 lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)" |
|
230 by simp |
|
231 |
|
232 lemma |
|
233 shows "equivp (op \<approx>)" |
|
234 and "equivp ((op \<approx>) ===> (op \<approx>))" |
|
235 (* Nitpick finds a counterexample! *) |
|
236 oops |
|
237 |
|
238 lemma lam_tst3a: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)" |
|
239 by auto |
|
240 |
|
241 lemma id_rsp: |
|
242 shows "(R ===> R) id id" |
|
243 by simp |
|
244 |
|
245 lemma lam_tst3a_reg: "(op \<approx> ===> op \<approx>) (Babs (Respects op \<approx>) (\<lambda>y. y)) (Babs (Respects op \<approx>) (\<lambda>x. x))" |
|
246 apply (rule babs_rsp[OF Quotient_my_int]) |
|
247 apply (simp add: id_rsp) |
|
248 done |
|
249 |
|
250 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)" |
|
251 apply(lifting lam_tst3a) |
|
252 apply(rule impI) |
|
253 apply(rule lam_tst3a_reg) |
|
254 done |
|
255 |
|
256 lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)" |
|
257 by auto |
|
258 |
|
259 lemma "(\<lambda>(y :: my_int => my_int). y) = (\<lambda>(x :: my_int => my_int). x)" |
|
260 apply(lifting lam_tst3b) |
|
261 apply(rule impI) |
|
262 apply(rule babs_rsp[OF fun_quotient[OF Quotient_my_int Quotient_my_int]]) |
|
263 apply(simp add: id_rsp) |
|
264 done |
|
265 |
|
266 lemma lam_tst4: "map (\<lambda>x. my_plus x (0,0)) l = l" |
|
267 apply (induct l) |
|
268 apply simp |
|
269 apply (case_tac a) |
|
270 apply simp |
|
271 done |
|
272 |
|
273 lemma "map (\<lambda>x. PLUS x ZERO) l = l" |
|
274 apply(lifting lam_tst4) |
|
275 done |
|
276 |
|
277 end |