316 apply(simp_all) |
316 apply(simp_all) |
317 apply(rule alpha.a2) |
317 apply(rule alpha.a2) |
318 apply(simp_all) |
318 apply(simp_all) |
319 done |
319 done |
320 |
320 |
|
321 lemma rlam_distinct: |
|
322 shows "\<not>(rVar nam \<approx> rApp rlam1' rlam2')" |
|
323 and "\<not>(rApp rlam1' rlam2' \<approx> rVar nam)" |
|
324 and "\<not>(rVar nam \<approx> rLam nam' rlam')" |
|
325 and "\<not>(rLam nam' rlam' \<approx> rVar nam)" |
|
326 and "\<not>(rApp rlam1 rlam2 \<approx> rLam nam' rlam')" |
|
327 and "\<not>(rLam nam' rlam' \<approx> rApp rlam1 rlam2)" |
|
328 apply auto |
|
329 apply(erule alpha.cases) |
|
330 apply simp_all |
|
331 apply(erule alpha.cases) |
|
332 apply simp_all |
|
333 apply(erule alpha.cases) |
|
334 apply simp_all |
|
335 apply(erule alpha.cases) |
|
336 apply simp_all |
|
337 apply(erule alpha.cases) |
|
338 apply simp_all |
|
339 apply(erule alpha.cases) |
|
340 apply simp_all |
|
341 done |
|
342 |
|
343 lemma lam_distinct[simp]: |
|
344 shows "Var nam \<noteq> App lam1' lam2'" |
|
345 and "App lam1' lam2' \<noteq> Var nam" |
|
346 and "Var nam \<noteq> Lam nam' lam'" |
|
347 and "Lam nam' lam' \<noteq> Var nam" |
|
348 and "App lam1 lam2 \<noteq> Lam nam' lam'" |
|
349 and "Lam nam' lam' \<noteq> App lam1 lam2" |
|
350 apply(lifting rlam_distinct(1) rlam_distinct(2) rlam_distinct(3) rlam_distinct(4) rlam_distinct(5) rlam_distinct(6)) |
|
351 done |
|
352 |
321 lemma var_supp1: |
353 lemma var_supp1: |
322 shows "(supp (Var a)) = ((supp a)::name set)" |
354 shows "(supp (Var a)) = ((supp a)::name set)" |
323 apply(simp add: supp_def) |
355 by (simp add: supp_def) |
324 done |
|
325 |
356 |
326 lemma var_supp: |
357 lemma var_supp: |
327 shows "(supp (Var a)) = {a::name}" |
358 shows "(supp (Var a)) = {a::name}" |
328 using var_supp1 |
359 using var_supp1 by (simp add: supp_atm) |
329 apply(simp add: supp_atm) |
|
330 done |
|
331 |
360 |
332 lemma app_supp: |
361 lemma app_supp: |
333 shows "supp (App t1 t2) = (supp t1) \<union> ((supp t2)::name set)" |
362 shows "supp (App t1 t2) = (supp t1) \<union> ((supp t2)::name set)" |
334 apply(simp only: perm_lam supp_def lam_inject) |
363 apply(simp only: perm_lam supp_def lam_inject) |
335 apply(simp add: Collect_imp_eq Collect_neg_eq) |
364 apply(simp add: Collect_imp_eq Collect_neg_eq) |
488 apply(induct t) |
517 apply(induct t) |
489 apply(auto) |
518 apply(auto) |
490 done |
519 done |
491 |
520 |
492 termination term1_hom |
521 termination term1_hom |
493 apply - |
|
494 apply(relation "measure (\<lambda>(f1, f2, f3, t). size t)") |
522 apply(relation "measure (\<lambda>(f1, f2, f3, t). size t)") |
495 apply(auto simp add: pi_size) |
523 apply(auto simp add: pi_size) |
496 done |
524 done |
497 |
525 |
498 (* |
526 lemma lam_exhaust: |
|
527 "\<lbrakk>\<And>name. y = Var name \<Longrightarrow> P; \<And>rlam1 rlam2. y = App rlam1 rlam2 \<Longrightarrow> P; \<And>name rlam. y = Lam name rlam \<Longrightarrow> P\<rbrakk> |
|
528 \<Longrightarrow> P" |
|
529 apply(lifting rlam.exhaust) |
|
530 done |
|
531 |
|
532 (* THIS IS NOT TRUE, but it lets prove the existence of the hom function *) |
|
533 lemma lam_inject': |
|
534 "(Lam a x = Lam b y) = ((\<lambda>c. [(a, c)] \<bullet> x) = (\<lambda>c. [(b, c)] \<bullet> y))" |
|
535 sorry |
|
536 |
499 function |
537 function |
500 hom :: "(name \<Rightarrow> 'a) \<Rightarrow> |
538 hom :: "(name \<Rightarrow> 'a) \<Rightarrow> |
501 (lam \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> |
539 (lam \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> |
502 ((name \<Rightarrow> lam) \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> 'a) \<Rightarrow> lam \<Rightarrow> 'a" |
540 ((name \<Rightarrow> lam) \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> 'a) \<Rightarrow> lam \<Rightarrow> 'a" |
503 where |
541 where |
504 "hom f_var f_app f_lam (Var x) = f_var x" |
542 "hom f_var f_app f_lam (Var x) = f_var x" |
505 | "hom f_var f_app f_lam (App l r) = f_app l r (hom f_var f_app f_lam l) (hom f_var f_app f_lam r)" |
543 | "hom f_var f_app f_lam (App l r) = f_app l r (hom f_var f_app f_lam l) (hom f_var f_app f_lam r)" |
506 | "hom f_var f_app f_lam (Lam a x) = f_lam (\<lambda>b. ([(a,b)] \<bullet> x)) (\<lambda>b. hom f_var f_app f_lam ([(a,b)] \<bullet> x))" |
544 | "hom f_var f_app f_lam (Lam a x) = f_lam (\<lambda>b. ([(a,b)] \<bullet> x)) (\<lambda>b. hom f_var f_app f_lam ([(a,b)] \<bullet> x))" |
507 apply(pat_completeness) |
545 defer |
508 apply(auto) |
546 apply(simp_all add: lam_inject') (* inject, distinct *) |
509 done |
547 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
|
548 apply(rule refl) |
|
549 apply(rule ext) |
|
550 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
|
551 apply simp_all |
|
552 apply(erule conjE)+ |
|
553 apply(rule_tac x="b" in cong) |
|
554 apply simp_all |
|
555 apply auto |
|
556 apply(rule_tac y="b" in lam_exhaust) |
|
557 apply simp_all |
|
558 apply auto |
|
559 apply meson |
|
560 apply(simp_all add: lam_inject') |
|
561 apply metis |
|
562 done |
|
563 |
|
564 termination hom |
|
565 apply - |
|
566 (* |
|
567 ML_prf {* Size.size_thms @{theory} "LamEx.lam" *} |
510 *) |
568 *) |
|
569 sorry |
|
570 |
|
571 thm hom.simps |
511 |
572 |
512 lemma term1_hom_rsp: |
573 lemma term1_hom_rsp: |
513 "\<lbrakk>(alpha ===> alpha ===> op =) f_app f_app; ((op = ===> alpha) ===> op =) f_lam f_lam\<rbrakk> |
574 "\<lbrakk>(alpha ===> alpha ===> op =) f_app f_app; ((op = ===> alpha) ===> op =) f_lam f_lam\<rbrakk> |
514 \<Longrightarrow> (alpha ===> op =) (term1_hom f_var f_app f_lam) (term1_hom f_var f_app f_lam)" |
575 \<Longrightarrow> (alpha ===> op =) (term1_hom f_var f_app f_lam) (term1_hom f_var f_app f_lam)" |
515 sorry |
576 sorry |