473 *) |
473 *) |
474 |
474 |
475 (* Substitution *) |
475 (* Substitution *) |
476 |
476 |
477 definition new where |
477 definition new where |
478 "new s = (THE x. \<forall>a \<in> s. x \<noteq> a)" |
478 "new s = (THE x. \<forall>a \<in> s. atom x \<noteq> a)" |
479 |
|
480 term "let n = new {s, x} in b" |
|
481 |
479 |
482 lemma size_no_change: "size (p \<bullet> (t :: lam_raw)) = size t" |
480 lemma size_no_change: "size (p \<bullet> (t :: lam_raw)) = size t" |
483 by (induct t) simp_all |
481 by (induct t) simp_all |
484 |
482 |
485 function |
483 function |
486 subst_var_raw :: "lam_raw \<Rightarrow> name \<Rightarrow> name \<Rightarrow> lam_raw" |
484 subst_raw :: "lam_raw \<Rightarrow> name \<Rightarrow> lam_raw \<Rightarrow> lam_raw" |
487 where |
485 where |
488 "subst_var_raw (Var_raw x) y s = (if x=y then (Var_raw s) else (Var_raw x))" |
486 "subst_raw (Var_raw x) y s = (if x=y then s else (Var_raw x))" |
489 | "subst_var_raw (App_raw l r) y s = App_raw (subst_var_raw l y s) (subst_var_raw r y s)" |
487 | "subst_raw (App_raw l r) y s = App_raw (subst_raw l y s) (subst_raw r y s)" |
490 | "subst_var_raw (Lam_raw x t) y s = |
488 | "subst_raw (Lam_raw x t) y s = |
491 Lam_raw (new {s, y, x}) (subst_var_raw ((x \<leftrightarrow> new {s, y, x}) \<bullet> t) y s)" |
489 Lam_raw (new ({atom y} \<union> fv_lam_raw s \<union> fv_lam_raw t - {atom x})) |
|
490 (subst_raw ((x \<leftrightarrow> (new ({atom y} \<union> fv_lam_raw s \<union> fv_lam_raw t - {atom x}))) \<bullet> t) y s)" |
492 by (pat_completeness, auto) |
491 by (pat_completeness, auto) |
493 termination |
492 termination |
494 apply (relation "measure (\<lambda>(t, y, s). (size t))") |
493 apply (relation "measure (\<lambda>(t, y, s). (size t))") |
495 apply (auto simp add: size_no_change) |
494 apply (auto simp add: size_no_change) |
496 done |
495 done |
497 |
496 |
|
497 lemma fv_subst[simp]: "fv_lam_raw (subst_raw t y s) = |
|
498 (if (atom y \<in> fv_lam_raw t) then fv_lam_raw s \<union> (fv_lam_raw t - {atom y}) else fv_lam_raw t)" |
|
499 apply (induct t arbitrary: s) |
|
500 apply (auto simp add: supp_at_base)[1] |
|
501 apply (auto simp add: supp_at_base)[1] |
|
502 apply (simp only: fv_lam_raw.simps) |
|
503 apply simp |
|
504 apply (rule conjI) |
|
505 apply clarify |
|
506 sorry |
|
507 |
|
508 thm supp_at_base |
498 lemma new_eqvt[eqvt]: "p \<bullet> (new s) = new (p \<bullet> s)" |
509 lemma new_eqvt[eqvt]: "p \<bullet> (new s) = new (p \<bullet> s)" |
499 sorry |
510 sorry |
500 |
511 |
501 lemma subst_var_raw_eqvt[eqvt]: "p \<bullet> (subst_var_raw t y s) = subst_var_raw (p \<bullet> t) (p \<bullet> y) (p \<bullet> s)" |
512 lemma subst_var_raw_eqvt[eqvt]: "p \<bullet> (subst_raw t y s) = subst_raw (p \<bullet> t) (p \<bullet> y) (p \<bullet> s)" |
502 apply (induct t arbitrary: p y s) |
513 apply (induct t arbitrary: p y s) |
503 apply simp_all |
514 apply simp_all |
504 apply(perm_simp) |
515 apply(perm_simp) |
505 apply simp |
516 apply simp |
506 sorry |
517 sorry |
507 |
518 |
508 lemma subst_id: "alpha_lam_raw (subst_var_raw x d d) x" |
519 lemma subst_id: "alpha_lam_raw (subst_raw x d (Var_raw d)) x" |
509 apply (induct x arbitrary: d) |
520 apply (induct x arbitrary: d) |
510 apply (simp_all add: alpha_lam_raw.intros) |
521 apply (simp_all add: alpha_lam_raw.intros) |
511 apply (rule alpha_lam_raw.intros) |
522 apply (rule alpha_lam_raw.intros) |
512 apply (rule_tac x="((new {d, name}) \<leftrightarrow> name)" in exI) |
523 apply (rule_tac x="(name \<leftrightarrow> new (insert (atom d) (supp d)))" in exI) |
513 |
524 apply (simp add: alphas) |
514 apply (rule_tac s="subst_var_raw ((name \<leftrightarrow> n) \<bullet> x) d d" and |
525 oops |
515 t="(name \<leftrightarrow> n) \<bullet> (subst_var_raw x ((name \<leftrightarrow> n) \<bullet> d) ((name \<leftrightarrow> n) \<bullet> d))" in subst) |
|
516 sorry |
|
517 |
|
518 (* Should be true? *) |
|
519 lemma "(alpha_lam_raw ===> op = ===> op = ===> alpha_lam_raw) subst_var_raw subst_var_raw" |
|
520 proof (intro fun_relI, (simp, clarify)) |
|
521 fix a b c d |
|
522 assume a: "alpha_lam_raw a b" |
|
523 show "alpha_lam_raw (subst_var_raw a c d) (subst_var_raw b c d)" using a |
|
524 apply (induct a b arbitrary: c d rule: alpha_lam_raw.induct) |
|
525 apply (simp add: equivp_reflp[OF lam_equivp]) |
|
526 apply (simp add: alpha_lam_raw.intros) |
|
527 apply clarify |
|
528 (* apply (case_tac "c = d") |
|
529 apply clarify |
|
530 apply (simp only: subst_id) |
|
531 apply (rule alpha_lam_raw.intros) |
|
532 apply (rule_tac x="p" in exI) |
|
533 apply (simp add: alphas) |
|
534 apply clarify |
|
535 apply simp*) |
|
536 apply (rename_tac x l y r c d p) |
|
537 apply simp |
|
538 unfolding Let_def |
|
539 apply (rule alpha_lam_raw.intros) |
|
540 apply (simp add: alphas) |
|
541 apply clarify |
|
542 apply simp |
|
543 apply (rule conjI) |
|
544 defer (* The fv one looks ok *) |
|
545 apply (rule_tac x="p + (x \<leftrightarrow> new {d, c, x}) + (y \<leftrightarrow> new {d, c, y})" in exI) |
|
546 apply (rule conjI) |
|
547 defer (* should do sth like subst fresh_star_permute_iff[symmetric] *) |
|
548 apply (simp only: eqvts) |
|
549 apply simp |
|
550 apply clarify |
|
551 sorry |
|
552 qed |
|
553 |
|
554 fun |
|
555 subst_raw :: "lam_raw \<Rightarrow> name \<Rightarrow> lam_raw \<Rightarrow> lam_raw" |
|
556 where |
|
557 "subst_raw (Var_raw x) y s = (if x=y then s else (Var_raw x))" |
|
558 | "subst_raw (App_raw l r) y s = App_raw (subst_raw l y s) (subst_raw r y s)" |
|
559 | "subst_raw (Lam_raw x t) y s = |
|
560 (if x = y then t else |
|
561 (if atom x \<notin> (fv_lam_raw s) then (Lam_raw x (subst_raw t y s)) else undefined))" |
|
562 (* termination/lifting fail with sth like: |
|
563 | "subst_raw (Lam_raw x t) y s = |
|
564 (FRESH v. Lam_raw v (subst_raw (subst_var_raw t x v) y s))" |
|
565 *) |
|
566 |
526 |
567 quotient_definition |
527 quotient_definition |
568 subst ("_ [ _ ::= _ ]" [100,100,100] 100) |
528 subst ("_ [ _ ::= _ ]" [100,100,100] 100) |
569 where |
529 where |
570 "subst :: lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" is "subst_raw" |
530 "subst :: lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" is "subst_raw" |
571 |
531 |
572 lemmas fv_rsp = quot_respect(10)[simplified,rulify] |
532 lemmas fv_rsp = quot_respect(10)[simplified] |
573 |
533 |
574 lemma subst_rsp_pre1: |
534 lemma subst_rsp_pre1: |
575 assumes a: "alpha_lam_raw a b" |
535 assumes a: "alpha_lam_raw a b" |
576 shows "alpha_lam_raw (subst_raw a y c) (subst_raw b y c)" |
536 shows "alpha_lam_raw (subst_raw a y c) (subst_raw b y c)" |
577 using a |
537 using a |
579 apply (simp add: equivp_reflp[OF lam_equivp]) |
539 apply (simp add: equivp_reflp[OF lam_equivp]) |
580 apply (simp add: alpha_lam_raw.intros) |
540 apply (simp add: alpha_lam_raw.intros) |
581 apply (simp only: alphas) |
541 apply (simp only: alphas) |
582 apply clarify |
542 apply clarify |
583 apply (simp only: subst_raw.simps) |
543 apply (simp only: subst_raw.simps) |
|
544 apply (rule alpha_lam_raw.intros) |
|
545 apply (simp only: alphas) |
584 sorry |
546 sorry |
585 |
547 |
586 lemma subst_rsp_pre2: |
548 lemma subst_rsp_pre2: |
587 assumes a: "alpha_lam_raw a b" |
549 assumes a: "alpha_lam_raw a b" |
588 shows "alpha_lam_raw (subst_raw c y a) (subst_raw c y b)" |
550 shows "alpha_lam_raw (subst_raw c y a) (subst_raw c y b)" |
|
551 using a |
|
552 apply (induct c arbitrary: a b y) |
|
553 apply (simp add: equivp_reflp[OF lam_equivp]) |
|
554 apply (simp add: alpha_lam_raw.intros) |
|
555 apply simp |
|
556 apply (rule alpha_lam_raw.intros) |
589 sorry |
557 sorry |
590 |
558 |
591 (* The below is definitely not true... *) |
|
592 lemma [quot_respect]: |
559 lemma [quot_respect]: |
593 "(alpha_lam_raw ===> op = ===> alpha_lam_raw ===> alpha_lam_raw) subst_raw subst_raw" |
560 "(alpha_lam_raw ===> op = ===> alpha_lam_raw ===> alpha_lam_raw) subst_raw subst_raw" |
594 proof (intro fun_relI, simp) |
561 proof (intro fun_relI, simp) |
595 fix a b c d :: lam_raw |
562 fix a b c d :: lam_raw |
596 fix y :: name |
563 fix y :: name |