106 and a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)" |
106 and a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)" |
107 and a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)" |
107 and a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)" |
108 shows "P c lm" |
108 shows "P c lm" |
109 proof - |
109 proof - |
110 have "\<And>p. P c (p \<bullet> lm)" |
110 have "\<And>p. P c (p \<bullet> lm)" |
111 apply(induct lm arbitrary: c rule: lm_induct) |
111 apply(induct lm arbitrary: c rule: lm.induct) |
112 apply(simp only: lm_perm) |
112 apply(simp only: lm.perm) |
113 apply(rule a1) |
113 apply(rule a1) |
114 apply(simp only: lm_perm) |
114 apply(simp only: lm.perm) |
115 apply(rule a2) |
115 apply(rule a2) |
116 apply(blast)[1] |
116 apply(blast)[1] |
117 apply(assumption) |
117 apply(assumption) |
118 thm at_set_avoiding |
118 thm at_set_avoiding |
119 apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lm name lm) \<sharp>* q") |
119 apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lm name lm) \<sharp>* q") |
120 apply(erule exE) |
120 apply(erule exE) |
121 apply(rule_tac t="p \<bullet> Lm name lm" and |
121 apply(rule_tac t="p \<bullet> Lm name lm" and |
122 s="q \<bullet> p \<bullet> Lm name lm" in subst) |
122 s="q \<bullet> p \<bullet> Lm name lm" in subst) |
123 defer |
123 defer |
124 apply(simp add: lm_perm) |
124 apply(simp add: lm.perm) |
125 apply(rule a3) |
125 apply(rule a3) |
126 apply(simp add: eqvts fresh_star_def) |
126 apply(simp add: eqvts fresh_star_def) |
127 apply(drule_tac x="q + p" in meta_spec) |
127 apply(drule_tac x="q + p" in meta_spec) |
128 apply(simp) |
128 apply(simp) |
129 sorry |
129 sorry |
649 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.perm |
649 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.perm |
650 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct |
650 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct |
651 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts |
651 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts |
652 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct |
652 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct |
653 |
653 |
|
654 lemma |
|
655 "fv_mexp j = supp j \<and> fv_body k = supp k \<and> |
|
656 (fv_defn c = supp c \<and> fv_cbinders c = {a. infinite {b. \<not>alpha_cbinders ((a \<rightleftharpoons> b) \<bullet> c) c}}) \<and> |
|
657 fv_sexp d = supp d \<and> fv_sbody e = supp e \<and> |
|
658 (fv_spec l = supp l \<and> fv_Cbinders l = {a. infinite {b. \<not>alpha_Cbinders ((a \<rightleftharpoons> b) \<bullet> l) l}}) \<and> |
|
659 fv_tyty g = supp g \<and> fv_path h = supp h \<and> fv_trmtrm i = supp i" |
|
660 apply(induct rule: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct) |
|
661 apply(simp_all only: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv) |
|
662 apply(simp_all only: supp_Abs[symmetric]) |
|
663 apply(simp_all (no_asm) only: supp_def) |
|
664 apply(simp_all only: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.perm) |
|
665 apply(simp_all only: permute_ABS) |
|
666 apply(simp_all only: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.eq_iff Abs_eq_iff) |
|
667 apply(simp_all only: alpha_gen) |
|
668 apply(simp_all only: eqvts[symmetric] supp_Pair) |
|
669 apply(simp_all only: eqvts Pair_eq) |
|
670 apply(simp_all only: supp_at_base[symmetric,simplified supp_def]) |
|
671 apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric]) |
|
672 apply(simp_all only: de_Morgan_conj[symmetric]) |
|
673 apply simp_all |
|
674 done |
|
675 |
654 (* example 3 from Peter Sewell's bestiary *) |
676 (* example 3 from Peter Sewell's bestiary *) |
655 |
677 |
656 nominal_datatype exp = |
678 nominal_datatype exp = |
657 VarP "name" |
679 VarP "name" |
658 | AppP "exp" "exp" |
680 | AppP "exp" "exp" |