475 (* Substitution *) |
475 (* Substitution *) |
476 |
476 |
477 definition new where |
477 definition new where |
478 "new s = (THE x. \<forall>a \<in> s. atom x \<noteq> a)" |
478 "new s = (THE x. \<forall>a \<in> s. atom x \<noteq> a)" |
479 |
479 |
|
480 primrec match_Var_raw where |
|
481 "match_Var_raw (Var_raw x) = Some x" |
|
482 | "match_Var_raw (App_raw x y) = None" |
|
483 | "match_Var_raw (Lam_raw n t) = None" |
|
484 |
|
485 quotient_definition |
|
486 "match_Var :: lam \<Rightarrow> name option" |
|
487 is match_Var_raw |
|
488 |
|
489 lemma [quot_respect]: "(alpha_lam_raw ===> op =) match_Var_raw match_Var_raw" |
|
490 apply rule |
|
491 apply (induct_tac a b rule: alpha_lam_raw.induct) |
|
492 apply simp_all |
|
493 done |
|
494 |
|
495 lemmas match_Var_simps = match_Var_raw.simps[quot_lifted] |
|
496 |
|
497 primrec match_App_raw where |
|
498 "match_App_raw (Var_raw x) = None" |
|
499 | "match_App_raw (App_raw x y) = Some (x, y)" |
|
500 | "match_App_raw (Lam_raw n t) = None" |
|
501 |
|
502 quotient_definition |
|
503 "match_App :: lam \<Rightarrow> (lam \<times> lam) option" |
|
504 is match_App_raw |
|
505 |
|
506 lemma [quot_respect]: |
|
507 "(alpha_lam_raw ===> option_rel (prod_rel alpha_lam_raw alpha_lam_raw)) match_App_raw match_App_raw" |
|
508 apply (intro fun_relI) |
|
509 apply (induct_tac a b rule: alpha_lam_raw.induct) |
|
510 apply simp_all |
|
511 done |
|
512 |
|
513 lemmas match_App_simps = match_App_raw.simps[quot_lifted] |
|
514 |
|
515 primrec match_Lam_raw where |
|
516 "match_Lam_raw (S :: atom set) (Var_raw x) = None" |
|
517 | "match_Lam_raw S (App_raw x y) = None" |
|
518 | "match_Lam_raw S (Lam_raw n t) = (let z = new (S \<union> (fv_lam_raw t - {atom n})) in Some (z, (n \<leftrightarrow> z) \<bullet> t))" |
|
519 |
|
520 quotient_definition |
|
521 "match_Lam :: (atom set) \<Rightarrow> lam \<Rightarrow> (name \<times> lam) option" |
|
522 is match_Lam_raw |
|
523 |
|
524 lemma [quot_respect]: |
|
525 "(op = ===> alpha_lam_raw ===> option_rel (prod_rel op = alpha_lam_raw)) match_Lam_raw match_Lam_raw" |
|
526 proof (intro fun_relI, clarify) |
|
527 fix S t s |
|
528 assume a: "alpha_lam_raw t s" |
|
529 show "option_rel (prod_rel op = alpha_lam_raw) (match_Lam_raw S t) (match_Lam_raw S s)" |
|
530 using a proof (induct t s rule: alpha_lam_raw.induct) |
|
531 case goal1 show ?case by simp |
|
532 next |
|
533 case goal2 show ?case by simp |
|
534 next |
|
535 case (goal3 x t y s) |
|
536 then obtain p where "({atom x}, t) \<approx>gen (\<lambda>x1 x2. alpha_lam_raw x1 x2 \<and> |
|
537 option_rel (prod_rel op = alpha_lam_raw) (match_Lam_raw S x1) |
|
538 (match_Lam_raw S x2)) fv_lam_raw p ({atom y}, s)" .. |
|
539 then have |
|
540 c: "fv_lam_raw t - {atom x} = fv_lam_raw s - {atom y}" and |
|
541 d: "(fv_lam_raw t - {atom x}) \<sharp>* p" and |
|
542 e: "alpha_lam_raw (p \<bullet> t) s" and |
|
543 f: "option_rel (prod_rel op = alpha_lam_raw) (match_Lam_raw S (p \<bullet> t)) (match_Lam_raw S s)" and |
|
544 g: "p \<bullet> {atom x} = {atom y}" unfolding alphas(1) by - (elim conjE, assumption)+ |
|
545 let ?z = "new (S \<union> (fv_lam_raw t - {atom x}))" |
|
546 have h: "?z = new (S \<union> (fv_lam_raw s - {atom y}))" using c by simp |
|
547 show ?case |
|
548 unfolding match_Lam_raw.simps Let_def option_rel.simps prod_rel.simps split_conv |
|
549 proof |
|
550 show "?z = new (S \<union> (fv_lam_raw s - {atom y}))" by (fact h) |
|
551 next |
|
552 have "atom y \<sharp> p" sorry |
|
553 have "fv_lam_raw t \<sharp>* ((x \<leftrightarrow> y) \<bullet> p)" sorry |
|
554 then have "alpha_lam_raw (((x \<leftrightarrow> y) \<bullet> p) \<bullet> t) t" sorry |
|
555 have "alpha_lam_raw (p \<bullet> t) ((x \<leftrightarrow> y) \<bullet> t)" sorry |
|
556 have "alpha_lam_raw t ((x \<leftrightarrow> y) \<bullet> s)" sorry |
|
557 then have "alpha_lam_raw ((x \<leftrightarrow> ?z) \<bullet> t) ((y \<leftrightarrow> ?z) \<bullet> s)" using eqvts(15) sorry |
|
558 then show "alpha_lam_raw ((x \<leftrightarrow> new (S \<union> (fv_lam_raw t - {atom x}))) \<bullet> t) |
|
559 ((y \<leftrightarrow> new (S \<union> (fv_lam_raw s - {atom y}))) \<bullet> s)" unfolding h . |
|
560 qed |
|
561 qed |
|
562 qed |
|
563 |
|
564 lemmas match_Lam_simps = match_Lam_raw.simps[quot_lifted] |
|
565 |
|
566 lemma app_some: "match_App x = Some (a, b) \<Longrightarrow> x = App a b" |
|
567 by (induct x rule: lam.induct) (simp_all add: match_App_simps) |
|
568 |
|
569 lemma lam_some: "match_Lam S x = Some (z, s) \<Longrightarrow> x = Lam z s \<and> atom z \<sharp> S" |
|
570 apply (induct x rule: lam.induct) |
|
571 apply (simp_all add: match_Lam_simps) |
|
572 apply (simp add: Let_def) |
|
573 apply (erule conjE) |
|
574 apply (thin_tac "match_Lam S lam = Some (z, s) \<Longrightarrow> lam = Lam z s \<and> atom z \<sharp> S") |
|
575 apply (rule conjI) |
|
576 apply (simp add: lam.eq_iff) |
|
577 apply (rule_tac x="(name \<leftrightarrow> z)" in exI) |
|
578 apply (simp add: alphas) |
|
579 apply (simp add: eqvts) |
|
580 apply (simp only: lam.fv(3)[symmetric]) |
|
581 apply (subgoal_tac "Lam name lam = Lam z s") |
|
582 apply (simp del: lam.fv) |
|
583 prefer 3 |
|
584 apply (thin_tac "(name \<leftrightarrow> new (S \<union> (fv_lam lam - {atom name}))) \<bullet> lam = s") |
|
585 apply (simp only: new_def) |
|
586 apply (subgoal_tac "\<forall>a \<in> S. atom z \<noteq> a") |
|
587 apply (simp only: fresh_def) |
|
588 |
|
589 thm new_def |
|
590 apply simp |
|
591 |
|
592 |
|
593 function subst where |
|
594 "subst v s t = ( |
|
595 case match_Var t of Some n \<Rightarrow> if n = v then s else Var n | None \<Rightarrow> |
|
596 case match_App t of Some (l, r) \<Rightarrow> App (subst v s l) (subst v s r) | None \<Rightarrow> |
|
597 case match_Lam (supp (v,s)) t of Some (n, t) \<Rightarrow> Lam n (subst v s t) | None \<Rightarrow> undefined)" |
|
598 by pat_completeness auto |
|
599 |
|
600 termination apply (relation "measure (\<lambda>(_, _, t). size t)") |
|
601 apply auto[1] |
|
602 defer |
|
603 apply (case_tac a) apply simp |
|
604 apply (frule app_some) apply simp |
|
605 apply (case_tac a) apply simp |
|
606 apply (frule app_some) apply simp |
|
607 apply (case_tac a) apply simp |
|
608 apply (frule lam_some) |
|
609 apply simp |
|
610 done |
|
611 |
|
612 lemmas lam_exhaust = lam_raw.exhaust[quot_lifted] |
|
613 |
|
614 lemma subst_eqvt: |
|
615 "p \<bullet> (subst v s t) = subst (p \<bullet> v) (p \<bullet> s) (p \<bullet> t)" |
|
616 proof (induct v s t rule: subst.induct) |
|
617 case (1 v s t) |
|
618 show ?case proof (cases t rule: lam_exhaust) |
|
619 fix n |
|
620 assume "t = Var n" |
|
621 then show ?thesis by (simp add: match_Var_simps) |
|
622 next |
|
623 fix l r |
|
624 assume "t = App l r" |
|
625 then show ?thesis |
|
626 apply (simp only:) |
|
627 apply (subst subst.simps) |
|
628 apply (subst match_Var_simps) |
|
629 apply (simp only: option.cases) |
|
630 apply (subst match_App_simps) |
|
631 apply (simp only: option.cases) |
|
632 apply (simp only: prod.cases) |
|
633 apply (simp only: lam.perm) |
|
634 apply (subst (3) subst.simps) |
|
635 apply (subst match_Var_simps) |
|
636 apply (simp only: option.cases) |
|
637 apply (subst match_App_simps) |
|
638 apply (simp only: option.cases) |
|
639 apply (simp only: prod.cases) |
|
640 apply (subst 1(2)[of "(l, r)" "l" "r"]) |
|
641 apply (simp add: match_Var_simps) |
|
642 apply (simp add: match_App_simps) |
|
643 apply (rule refl) |
|
644 apply (subst 1(3)[of "(l, r)" "l" "r"]) |
|
645 apply (simp add: match_Var_simps) |
|
646 apply (simp add: match_App_simps) |
|
647 apply (rule refl) |
|
648 apply (rule refl) |
|
649 done |
|
650 next |
|
651 fix n t' |
|
652 assume "t = Lam n t'" |
|
653 then show ?thesis |
|
654 apply (simp only: ) |
|
655 apply (simp only: lam.perm) |
|
656 apply (subst subst.simps) |
|
657 apply (subst match_Var_simps) |
|
658 apply (simp only: option.cases) |
|
659 apply (subst match_App_simps) |
|
660 apply (simp only: option.cases) |
|
661 apply (subst match_Lam_simps) |
|
662 apply (simp only: Let_def) |
|
663 apply (simp only: option.cases) |
|
664 apply (simp only: prod.cases) |
|
665 apply (subst (2) subst.simps) |
|
666 apply (subst match_Var_simps) |
|
667 apply (simp only: option.cases) |
|
668 apply (subst match_App_simps) |
|
669 apply (simp only: option.cases) |
|
670 apply (subst match_Lam_simps) |
|
671 apply (simp only: Let_def) |
|
672 apply (simp only: option.cases) |
|
673 apply (simp only: prod.cases) |
|
674 apply (simp only: lam.perm) |
|
675 apply (simp only: lam.eq_iff) |
|
676 sorry |
|
677 qed |
|
678 qed |
|
679 |
480 lemma size_no_change: "size (p \<bullet> (t :: lam_raw)) = size t" |
680 lemma size_no_change: "size (p \<bullet> (t :: lam_raw)) = size t" |
481 by (induct t) simp_all |
681 by (induct t) simp_all |
482 |
682 |
483 function |
683 function |
484 subst_raw :: "lam_raw \<Rightarrow> name \<Rightarrow> lam_raw \<Rightarrow> lam_raw" |
684 subst_raw :: "lam_raw \<Rightarrow> name \<Rightarrow> lam_raw \<Rightarrow> lam_raw" |