11 |
11 |
12 subsection {* Relator for function space *} |
12 subsection {* Relator for function space *} |
13 |
13 |
14 locale lifting_syntax |
14 locale lifting_syntax |
15 begin |
15 begin |
16 notation fun_rel (infixr "===>" 55) |
16 notation rel_fun (infixr "===>" 55) |
17 notation map_fun (infixr "--->" 55) |
17 notation map_fun (infixr "--->" 55) |
18 end |
18 end |
19 |
19 |
20 context |
20 context |
21 begin |
21 begin |
22 interpretation lifting_syntax . |
22 interpretation lifting_syntax . |
23 |
23 |
24 lemma fun_relD2: |
24 lemma rel_funD2: |
25 assumes "fun_rel A B f g" and "A x x" |
25 assumes "rel_fun A B f g" and "A x x" |
26 shows "B (f x) (g x)" |
26 shows "B (f x) (g x)" |
27 using assms by (rule fun_relD) |
27 using assms by (rule rel_funD) |
28 |
28 |
29 lemma fun_relE: |
29 lemma rel_funE: |
30 assumes "fun_rel A B f g" and "A x y" |
30 assumes "rel_fun A B f g" and "A x y" |
31 obtains "B (f x) (g y)" |
31 obtains "B (f x) (g y)" |
32 using assms by (simp add: fun_rel_def) |
32 using assms by (simp add: rel_fun_def) |
33 |
33 |
34 lemmas fun_rel_eq = fun.rel_eq |
34 lemmas rel_fun_eq = fun.rel_eq |
35 |
35 |
36 lemma fun_rel_eq_rel: |
36 lemma rel_fun_eq_rel: |
37 shows "fun_rel (op =) R = (\<lambda>f g. \<forall>x. R (f x) (g x))" |
37 shows "rel_fun (op =) R = (\<lambda>f g. \<forall>x. R (f x) (g x))" |
38 by (simp add: fun_rel_def) |
38 by (simp add: rel_fun_def) |
39 |
39 |
40 |
40 |
41 subsection {* Transfer method *} |
41 subsection {* Transfer method *} |
42 |
42 |
43 text {* Explicit tag for relation membership allows for |
43 text {* Explicit tag for relation membership allows for |
161 lemma right_uniqueD: "\<lbrakk> right_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z" |
161 lemma right_uniqueD: "\<lbrakk> right_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z" |
162 unfolding right_unique_def by blast |
162 unfolding right_unique_def by blast |
163 |
163 |
164 lemma right_total_alt_def: |
164 lemma right_total_alt_def: |
165 "right_total R \<longleftrightarrow> ((R ===> op \<longrightarrow>) ===> op \<longrightarrow>) All All" |
165 "right_total R \<longleftrightarrow> ((R ===> op \<longrightarrow>) ===> op \<longrightarrow>) All All" |
166 unfolding right_total_def fun_rel_def |
166 unfolding right_total_def rel_fun_def |
167 apply (rule iffI, fast) |
167 apply (rule iffI, fast) |
168 apply (rule allI) |
168 apply (rule allI) |
169 apply (drule_tac x="\<lambda>x. True" in spec) |
169 apply (drule_tac x="\<lambda>x. True" in spec) |
170 apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec) |
170 apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec) |
171 apply fast |
171 apply fast |
172 done |
172 done |
173 |
173 |
174 lemma right_unique_alt_def: |
174 lemma right_unique_alt_def: |
175 "right_unique R \<longleftrightarrow> (R ===> R ===> op \<longrightarrow>) (op =) (op =)" |
175 "right_unique R \<longleftrightarrow> (R ===> R ===> op \<longrightarrow>) (op =) (op =)" |
176 unfolding right_unique_def fun_rel_def by auto |
176 unfolding right_unique_def rel_fun_def by auto |
177 |
177 |
178 lemma bi_total_alt_def: |
178 lemma bi_total_alt_def: |
179 "bi_total R \<longleftrightarrow> ((R ===> op =) ===> op =) All All" |
179 "bi_total R \<longleftrightarrow> ((R ===> op =) ===> op =) All All" |
180 unfolding bi_total_def fun_rel_def |
180 unfolding bi_total_def rel_fun_def |
181 apply (rule iffI, fast) |
181 apply (rule iffI, fast) |
182 apply safe |
182 apply safe |
183 apply (drule_tac x="\<lambda>x. \<exists>y. R x y" in spec) |
183 apply (drule_tac x="\<lambda>x. \<exists>y. R x y" in spec) |
184 apply (drule_tac x="\<lambda>y. True" in spec) |
184 apply (drule_tac x="\<lambda>y. True" in spec) |
185 apply fast |
185 apply fast |
246 apply (simp add: right_unique_def) |
246 apply (simp add: right_unique_def) |
247 done |
247 done |
248 |
248 |
249 lemma right_unique_fun [transfer_rule]: |
249 lemma right_unique_fun [transfer_rule]: |
250 "\<lbrakk>right_total A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A ===> B)" |
250 "\<lbrakk>right_total A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A ===> B)" |
251 unfolding right_total_def right_unique_def fun_rel_def |
251 unfolding right_total_def right_unique_def rel_fun_def |
252 by (clarify, rule ext, fast) |
252 by (clarify, rule ext, fast) |
253 |
253 |
254 lemma bi_total_fun [transfer_rule]: |
254 lemma bi_total_fun [transfer_rule]: |
255 "\<lbrakk>bi_unique A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A ===> B)" |
255 "\<lbrakk>bi_unique A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A ===> B)" |
256 unfolding bi_total_def fun_rel_def |
256 unfolding bi_total_def rel_fun_def |
257 apply safe |
257 apply safe |
258 apply (rename_tac f) |
258 apply (rename_tac f) |
259 apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI) |
259 apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI) |
260 apply clarify |
260 apply clarify |
261 apply (subgoal_tac "(THE x. A x y) = x", simp) |
261 apply (subgoal_tac "(THE x. A x y) = x", simp) |
275 apply (simp add: bi_unique_def) |
275 apply (simp add: bi_unique_def) |
276 done |
276 done |
277 |
277 |
278 lemma bi_unique_fun [transfer_rule]: |
278 lemma bi_unique_fun [transfer_rule]: |
279 "\<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A ===> B)" |
279 "\<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A ===> B)" |
280 unfolding bi_total_def bi_unique_def fun_rel_def fun_eq_iff |
280 unfolding bi_total_def bi_unique_def rel_fun_def fun_eq_iff |
281 by (safe, metis, fast) |
281 by (safe, metis, fast) |
282 |
282 |
283 |
283 |
284 subsection {* Transfer rules *} |
284 subsection {* Transfer rules *} |
285 |
285 |
286 lemma Domainp_forall_transfer [transfer_rule]: |
286 lemma Domainp_forall_transfer [transfer_rule]: |
287 assumes "right_total A" |
287 assumes "right_total A" |
288 shows "((A ===> op =) ===> op =) |
288 shows "((A ===> op =) ===> op =) |
289 (transfer_bforall (Domainp A)) transfer_forall" |
289 (transfer_bforall (Domainp A)) transfer_forall" |
290 using assms unfolding right_total_def |
290 using assms unfolding right_total_def |
291 unfolding transfer_forall_def transfer_bforall_def fun_rel_def Domainp_iff |
291 unfolding transfer_forall_def transfer_bforall_def rel_fun_def Domainp_iff |
292 by metis |
292 by metis |
293 |
293 |
294 text {* Transfer rules using implication instead of equality on booleans. *} |
294 text {* Transfer rules using implication instead of equality on booleans. *} |
295 |
295 |
296 lemma transfer_forall_transfer [transfer_rule]: |
296 lemma transfer_forall_transfer [transfer_rule]: |
297 "bi_total A \<Longrightarrow> ((A ===> op =) ===> op =) transfer_forall transfer_forall" |
297 "bi_total A \<Longrightarrow> ((A ===> op =) ===> op =) transfer_forall transfer_forall" |
298 "right_total A \<Longrightarrow> ((A ===> op =) ===> implies) transfer_forall transfer_forall" |
298 "right_total A \<Longrightarrow> ((A ===> op =) ===> implies) transfer_forall transfer_forall" |
299 "right_total A \<Longrightarrow> ((A ===> implies) ===> implies) transfer_forall transfer_forall" |
299 "right_total A \<Longrightarrow> ((A ===> implies) ===> implies) transfer_forall transfer_forall" |
300 "bi_total A \<Longrightarrow> ((A ===> op =) ===> rev_implies) transfer_forall transfer_forall" |
300 "bi_total A \<Longrightarrow> ((A ===> op =) ===> rev_implies) transfer_forall transfer_forall" |
301 "bi_total A \<Longrightarrow> ((A ===> rev_implies) ===> rev_implies) transfer_forall transfer_forall" |
301 "bi_total A \<Longrightarrow> ((A ===> rev_implies) ===> rev_implies) transfer_forall transfer_forall" |
302 unfolding transfer_forall_def rev_implies_def fun_rel_def right_total_def bi_total_def |
302 unfolding transfer_forall_def rev_implies_def rel_fun_def right_total_def bi_total_def |
303 by metis+ |
303 by metis+ |
304 |
304 |
305 lemma transfer_implies_transfer [transfer_rule]: |
305 lemma transfer_implies_transfer [transfer_rule]: |
306 "(op = ===> op = ===> op = ) transfer_implies transfer_implies" |
306 "(op = ===> op = ===> op = ) transfer_implies transfer_implies" |
307 "(rev_implies ===> implies ===> implies ) transfer_implies transfer_implies" |
307 "(rev_implies ===> implies ===> implies ) transfer_implies transfer_implies" |
310 "(op = ===> op = ===> implies ) transfer_implies transfer_implies" |
310 "(op = ===> op = ===> implies ) transfer_implies transfer_implies" |
311 "(implies ===> rev_implies ===> rev_implies) transfer_implies transfer_implies" |
311 "(implies ===> rev_implies ===> rev_implies) transfer_implies transfer_implies" |
312 "(implies ===> op = ===> rev_implies) transfer_implies transfer_implies" |
312 "(implies ===> op = ===> rev_implies) transfer_implies transfer_implies" |
313 "(op = ===> rev_implies ===> rev_implies) transfer_implies transfer_implies" |
313 "(op = ===> rev_implies ===> rev_implies) transfer_implies transfer_implies" |
314 "(op = ===> op = ===> rev_implies) transfer_implies transfer_implies" |
314 "(op = ===> op = ===> rev_implies) transfer_implies transfer_implies" |
315 unfolding transfer_implies_def rev_implies_def fun_rel_def by auto |
315 unfolding transfer_implies_def rev_implies_def rel_fun_def by auto |
316 |
316 |
317 lemma eq_imp_transfer [transfer_rule]: |
317 lemma eq_imp_transfer [transfer_rule]: |
318 "right_unique A \<Longrightarrow> (A ===> A ===> op \<longrightarrow>) (op =) (op =)" |
318 "right_unique A \<Longrightarrow> (A ===> A ===> op \<longrightarrow>) (op =) (op =)" |
319 unfolding right_unique_alt_def . |
319 unfolding right_unique_alt_def . |
320 |
320 |
321 lemma eq_transfer [transfer_rule]: |
321 lemma eq_transfer [transfer_rule]: |
322 assumes "bi_unique A" |
322 assumes "bi_unique A" |
323 shows "(A ===> A ===> op =) (op =) (op =)" |
323 shows "(A ===> A ===> op =) (op =) (op =)" |
324 using assms unfolding bi_unique_def fun_rel_def by auto |
324 using assms unfolding bi_unique_def rel_fun_def by auto |
325 |
325 |
326 lemma right_total_Ex_transfer[transfer_rule]: |
326 lemma right_total_Ex_transfer[transfer_rule]: |
327 assumes "right_total A" |
327 assumes "right_total A" |
328 shows "((A ===> op=) ===> op=) (Bex (Collect (Domainp A))) Ex" |
328 shows "((A ===> op=) ===> op=) (Bex (Collect (Domainp A))) Ex" |
329 using assms unfolding right_total_def Bex_def fun_rel_def Domainp_iff[abs_def] |
329 using assms unfolding right_total_def Bex_def rel_fun_def Domainp_iff[abs_def] |
330 by blast |
330 by blast |
331 |
331 |
332 lemma right_total_All_transfer[transfer_rule]: |
332 lemma right_total_All_transfer[transfer_rule]: |
333 assumes "right_total A" |
333 assumes "right_total A" |
334 shows "((A ===> op =) ===> op =) (Ball (Collect (Domainp A))) All" |
334 shows "((A ===> op =) ===> op =) (Ball (Collect (Domainp A))) All" |
335 using assms unfolding right_total_def Ball_def fun_rel_def Domainp_iff[abs_def] |
335 using assms unfolding right_total_def Ball_def rel_fun_def Domainp_iff[abs_def] |
336 by blast |
336 by blast |
337 |
337 |
338 lemma All_transfer [transfer_rule]: |
338 lemma All_transfer [transfer_rule]: |
339 assumes "bi_total A" |
339 assumes "bi_total A" |
340 shows "((A ===> op =) ===> op =) All All" |
340 shows "((A ===> op =) ===> op =) All All" |
341 using assms unfolding bi_total_def fun_rel_def by fast |
341 using assms unfolding bi_total_def rel_fun_def by fast |
342 |
342 |
343 lemma Ex_transfer [transfer_rule]: |
343 lemma Ex_transfer [transfer_rule]: |
344 assumes "bi_total A" |
344 assumes "bi_total A" |
345 shows "((A ===> op =) ===> op =) Ex Ex" |
345 shows "((A ===> op =) ===> op =) Ex Ex" |
346 using assms unfolding bi_total_def fun_rel_def by fast |
346 using assms unfolding bi_total_def rel_fun_def by fast |
347 |
347 |
348 lemma If_transfer [transfer_rule]: "(op = ===> A ===> A ===> A) If If" |
348 lemma If_transfer [transfer_rule]: "(op = ===> A ===> A ===> A) If If" |
349 unfolding fun_rel_def by simp |
349 unfolding rel_fun_def by simp |
350 |
350 |
351 lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let" |
351 lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let" |
352 unfolding fun_rel_def by simp |
352 unfolding rel_fun_def by simp |
353 |
353 |
354 lemma id_transfer [transfer_rule]: "(A ===> A) id id" |
354 lemma id_transfer [transfer_rule]: "(A ===> A) id id" |
355 unfolding fun_rel_def by simp |
355 unfolding rel_fun_def by simp |
356 |
356 |
357 lemma comp_transfer [transfer_rule]: |
357 lemma comp_transfer [transfer_rule]: |
358 "((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \<circ>) (op \<circ>)" |
358 "((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \<circ>) (op \<circ>)" |
359 unfolding fun_rel_def by simp |
359 unfolding rel_fun_def by simp |
360 |
360 |
361 lemma fun_upd_transfer [transfer_rule]: |
361 lemma fun_upd_transfer [transfer_rule]: |
362 assumes [transfer_rule]: "bi_unique A" |
362 assumes [transfer_rule]: "bi_unique A" |
363 shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd" |
363 shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd" |
364 unfolding fun_upd_def [abs_def] by transfer_prover |
364 unfolding fun_upd_def [abs_def] by transfer_prover |
365 |
365 |
366 lemma case_nat_transfer [transfer_rule]: |
366 lemma case_nat_transfer [transfer_rule]: |
367 "(A ===> (op = ===> A) ===> op = ===> A) case_nat case_nat" |
367 "(A ===> (op = ===> A) ===> op = ===> A) case_nat case_nat" |
368 unfolding fun_rel_def by (simp split: nat.split) |
368 unfolding rel_fun_def by (simp split: nat.split) |
369 |
369 |
370 lemma rec_nat_transfer [transfer_rule]: |
370 lemma rec_nat_transfer [transfer_rule]: |
371 "(A ===> (op = ===> A ===> A) ===> op = ===> A) rec_nat rec_nat" |
371 "(A ===> (op = ===> A ===> A) ===> op = ===> A) rec_nat rec_nat" |
372 unfolding fun_rel_def by (clarsimp, rename_tac n, induct_tac n, simp_all) |
372 unfolding rel_fun_def by (clarsimp, rename_tac n, induct_tac n, simp_all) |
373 |
373 |
374 lemma funpow_transfer [transfer_rule]: |
374 lemma funpow_transfer [transfer_rule]: |
375 "(op = ===> (A ===> A) ===> (A ===> A)) compow compow" |
375 "(op = ===> (A ===> A) ===> (A ===> A)) compow compow" |
376 unfolding funpow_def by transfer_prover |
376 unfolding funpow_def by transfer_prover |
377 |
377 |
407 "bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> op=) reflp reflp" |
407 "bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> op=) reflp reflp" |
408 "right_total A \<Longrightarrow> ((A ===> A ===> implies) ===> implies) reflp reflp" |
408 "right_total A \<Longrightarrow> ((A ===> A ===> implies) ===> implies) reflp reflp" |
409 "right_total A \<Longrightarrow> ((A ===> A ===> op=) ===> implies) reflp reflp" |
409 "right_total A \<Longrightarrow> ((A ===> A ===> op=) ===> implies) reflp reflp" |
410 "bi_total A \<Longrightarrow> ((A ===> A ===> rev_implies) ===> rev_implies) reflp reflp" |
410 "bi_total A \<Longrightarrow> ((A ===> A ===> rev_implies) ===> rev_implies) reflp reflp" |
411 "bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> rev_implies) reflp reflp" |
411 "bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> rev_implies) reflp reflp" |
412 using assms unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def fun_rel_def |
412 using assms unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def rel_fun_def |
413 by fast+ |
413 by fast+ |
414 |
414 |
415 lemma right_unique_transfer [transfer_rule]: |
415 lemma right_unique_transfer [transfer_rule]: |
416 assumes [transfer_rule]: "right_total A" |
416 assumes [transfer_rule]: "right_total A" |
417 assumes [transfer_rule]: "right_total B" |
417 assumes [transfer_rule]: "right_total B" |
418 assumes [transfer_rule]: "bi_unique B" |
418 assumes [transfer_rule]: "bi_unique B" |
419 shows "((A ===> B ===> op=) ===> implies) right_unique right_unique" |
419 shows "((A ===> B ===> op=) ===> implies) right_unique right_unique" |
420 using assms unfolding right_unique_def[abs_def] right_total_def bi_unique_def fun_rel_def |
420 using assms unfolding right_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def |
421 by metis |
421 by metis |
422 |
422 |
423 end |
423 end |
424 |
424 |
425 end |
425 end |