472 nominal_inductive typing |
472 nominal_inductive typing |
473 *) |
473 *) |
474 |
474 |
475 (* Substitution *) |
475 (* Substitution *) |
476 |
476 |
477 fun |
477 definition new where |
|
478 "new s = (THE x. \<forall>a \<in> s. x \<noteq> a)" |
|
479 |
|
480 term "let n = new {s, x} in b" |
|
481 |
|
482 lemma size_no_change: "size (p \<bullet> (t :: lam_raw)) = size t" |
|
483 by (induct t) simp_all |
|
484 |
|
485 function |
478 subst_var_raw :: "lam_raw \<Rightarrow> name \<Rightarrow> name \<Rightarrow> lam_raw" |
486 subst_var_raw :: "lam_raw \<Rightarrow> name \<Rightarrow> name \<Rightarrow> lam_raw" |
479 where |
487 where |
480 "subst_var_raw (Var_raw x) y s = (if x=y then (Var_raw s) else (Var_raw x))" |
488 "subst_var_raw (Var_raw x) y s = (if x=y then (Var_raw s) else (Var_raw x))" |
481 | "subst_var_raw (App_raw l r) y s = App_raw (subst_var_raw l y s) (subst_var_raw r y s)" |
489 | "subst_var_raw (App_raw l r) y s = App_raw (subst_var_raw l y s) (subst_var_raw r y s)" |
482 | "subst_var_raw (Lam_raw x t) y s = |
490 | "subst_var_raw (Lam_raw x t) y s = |
483 (if x = y then Lam_raw x t else Lam_raw x (subst_var_raw t y s))" |
491 Lam_raw (new {s, y, x}) (subst_var_raw ((x \<leftrightarrow> new {s, y, x}) \<bullet> t) y s)" |
|
492 by (pat_completeness, auto) |
|
493 termination |
|
494 apply (relation "measure (\<lambda>(t, y, s). (size t))") |
|
495 apply (auto simp add: size_no_change) |
|
496 done |
|
497 |
|
498 lemma new_eqvt[eqvt]: "p \<bullet> (new s) = new (p \<bullet> s)" |
|
499 sorry |
|
500 |
|
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)" |
|
502 apply (induct t arbitrary: p y s) |
|
503 apply simp_all |
|
504 apply(perm_simp) |
|
505 apply simp |
|
506 sorry |
|
507 |
|
508 lemma subst_id: "alpha_lam_raw (subst_var_raw x d d) x" |
|
509 apply (induct x arbitrary: d) |
|
510 apply (simp_all add: alpha_lam_raw.intros) |
|
511 apply (rule alpha_lam_raw.intros) |
|
512 apply (rule_tac x="((new {d, name}) \<leftrightarrow> name)" in exI) |
|
513 |
|
514 apply (rule_tac s="subst_var_raw ((name \<leftrightarrow> n) \<bullet> x) d d" and |
|
515 t="(name \<leftrightarrow> n) \<bullet> (subst_var_raw x ((name \<leftrightarrow> n) \<bullet> d) ((name \<leftrightarrow> n) \<bullet> d))" in subst) |
|
516 sorry |
484 |
517 |
485 (* Should be true? *) |
518 (* Should be true? *) |
486 lemma "(alpha_lam_raw ===> op = ===> op = ===> alpha_lam_raw) subst_var_raw subst_var_raw" |
519 lemma "(alpha_lam_raw ===> op = ===> op = ===> alpha_lam_raw) subst_var_raw subst_var_raw" |
487 proof (intro fun_relI, (simp, clarify)) |
520 proof (intro fun_relI, (simp, clarify)) |
488 fix a b ba bb |
521 fix a b c d |
489 assume a: "alpha_lam_raw a b" |
522 assume a: "alpha_lam_raw a b" |
490 show "alpha_lam_raw (subst_var_raw a ba bb) (subst_var_raw b ba bb)" using a |
523 show "alpha_lam_raw (subst_var_raw a c d) (subst_var_raw b c d)" using a |
491 apply (induct a b rule: alpha_lam_raw.induct) |
524 apply (induct a b arbitrary: c d rule: alpha_lam_raw.induct) |
492 apply (simp add: equivp_reflp[OF lam_equivp]) |
525 apply (simp add: equivp_reflp[OF lam_equivp]) |
493 apply (simp add: alpha_lam_raw.intros) |
526 apply (simp add: alpha_lam_raw.intros) |
494 apply auto |
527 apply clarify |
495 apply (rule_tac[!] alpha_lam_raw.intros) |
528 (* apply (case_tac "c = d") |
496 apply (rule_tac[!] x="p" in exI) (* Need to do better *) |
529 apply clarify |
497 apply (simp_all add: alphas) |
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) |
498 apply clarify |
541 apply clarify |
499 apply simp |
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 |
500 sorry |
551 sorry |
501 qed |
552 qed |
502 |
553 |
503 fun |
554 fun |
504 subst_raw :: "lam_raw \<Rightarrow> name \<Rightarrow> lam_raw \<Rightarrow> lam_raw" |
555 subst_raw :: "lam_raw \<Rightarrow> name \<Rightarrow> lam_raw \<Rightarrow> lam_raw" |