71 shows "\<exists>p.([atom a], Var c) \<approx>lst (op =) supp p ([atom b], Var c)" |
71 shows "\<exists>p.([atom a], Var c) \<approx>lst (op =) supp p ([atom b], Var c)" |
72 apply (rule_tac x="(a \<leftrightarrow> b)" in exI) |
72 apply (rule_tac x="(a \<leftrightarrow> b)" in exI) |
73 apply (simp add: alphas trm_assn.supp supp_at_base x y fresh_star_def atom_eqvt) |
73 apply (simp add: alphas trm_assn.supp supp_at_base x y fresh_star_def atom_eqvt) |
74 by (metis Rep_name_inverse atom_name_def flip_fresh_fresh fresh_atom fresh_perm x y) |
74 by (metis Rep_name_inverse atom_name_def flip_fresh_fresh fresh_atom fresh_perm x y) |
75 |
75 |
76 lemma |
76 lemma alpha_bn_refl: "alpha_bn x x" |
77 assumes "atom a \<noteq> atom c \<and> atom b \<noteq> atom c" |
77 apply (induct x rule: trm_assn.inducts(2)) |
78 shows "\<exists>p. ([atom a], Var c) \<approx>lst (op =) supp p ([atom b], Var c) \<and> supp p \<subseteq> (supp (Var c) \<inter> {atom a}) \<union> (supp (Var c) \<inter> {atom b})" |
78 apply (rule TrueI) |
79 apply (simp add: alphas trm_assn.supp supp_at_base assms trm_assn.eq_iff atom_eqvt fresh_star_def) |
79 apply (auto simp add: trm_assn.eq_iff) |
80 oops |
80 done |
|
81 |
|
82 lemma alpha_bn_inducts_raw: |
|
83 "\<lbrakk>alpha_bn_raw a b; P3 ANil_raw ANil_raw; |
|
84 \<And>trm_raw trm_rawa assn_raw assn_rawa name namea. |
|
85 \<lbrakk>alpha_trm_raw trm_raw trm_rawa; alpha_bn_raw assn_raw assn_rawa; |
|
86 P3 assn_raw assn_rawa\<rbrakk> |
|
87 \<Longrightarrow> P3 (ACons_raw name trm_raw assn_raw) |
|
88 (ACons_raw namea trm_rawa assn_rawa)\<rbrakk> \<Longrightarrow> P3 a b" |
|
89 by (erule alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.inducts(3)[of _ _ "\<lambda>x y. True" _ "\<lambda>x y. True", simplified]) auto |
|
90 |
|
91 lemmas alpha_bn_inducts = alpha_bn_inducts_raw[quot_lifted] |
|
92 |
|
93 nominal_primrec |
|
94 subst :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" |
|
95 and substa :: "name \<Rightarrow> trm \<Rightarrow> assn \<Rightarrow> assn" |
|
96 where |
|
97 "subst s t (Var x) = (if (s = x) then t else (Var x))" |
|
98 | "subst s t (App l r) = App (subst s t l) (subst s t r)" |
|
99 | "atom v \<sharp> (s, t) \<Longrightarrow> subst s t (Lam v b) = Lam v (subst s t b)" |
|
100 | "set (bn as) \<sharp>* (s, t) \<Longrightarrow> subst s t (Let as b) = Let (substa s t as) (subst s t b)" |
|
101 | "substa s t ANil = ANil" |
|
102 | "substa s t (ACons v t' as) = ACons v (subst v t t') as" |
|
103 |
|
104 (*apply (subgoal_tac "\<forall>l. \<exists>!r. subst_substa_graph l r") |
|
105 defer |
|
106 apply rule |
|
107 apply (simp only: Ex1_def) |
|
108 apply (case_tac l) |
|
109 apply (case_tac a) |
|
110 apply (rule_tac y="c" and c="(aa,b)" in trm_assn.strong_exhaust(1)) |
|
111 apply simp_all[3] |
|
112 apply rule |
|
113 apply rule |
|
114 apply (rule subst_substa_graph.intros)*) |
|
115 |
|
116 defer |
|
117 apply (case_tac x) |
|
118 apply (case_tac a) |
|
119 thm trm_assn.strong_exhaust(1) |
|
120 apply (rule_tac y="c" and c="(aa,b)" in trm_assn.strong_exhaust(1)) |
|
121 apply (simp add: trm_assn.distinct trm_assn.eq_iff) |
|
122 apply auto[1] |
|
123 apply (simp add: trm_assn.distinct trm_assn.eq_iff) |
|
124 apply auto[1] |
|
125 apply (simp add: trm_assn.distinct trm_assn.eq_iff fresh_star_def) |
|
126 apply (simp add: trm_assn.distinct trm_assn.eq_iff) |
|
127 apply (drule_tac x="assn" in meta_spec) |
|
128 apply (rotate_tac 3) |
|
129 apply (drule_tac x="aa" in meta_spec) |
|
130 apply (rotate_tac -1) |
|
131 apply (drule_tac x="b" in meta_spec) |
|
132 apply (rotate_tac -1) |
|
133 apply (drule_tac x="trm" in meta_spec) |
|
134 apply (auto simp add: alpha_bn_refl)[1] |
|
135 apply (case_tac b) |
|
136 apply (rule_tac ya="c" in trm_assn.strong_exhaust(2)) |
|
137 apply (simp add: trm_assn.distinct trm_assn.eq_iff) |
|
138 apply auto[1] |
|
139 apply blast |
|
140 apply (simp add: trm_assn.distinct trm_assn.eq_iff) |
|
141 apply auto[1] |
|
142 apply blast |
|
143 apply (simp_all only: sum.simps Pair_eq trm_assn.distinct trm_assn.eq_iff) |
|
144 apply simp_all |
|
145 apply (simp_all add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff]) |
|
146 apply (simp_all add: meta_eq_to_obj_eq[OF substa_def, symmetric, unfolded fun_eq_iff]) |
|
147 apply clarify |
|
148 prefer 2 |
|
149 apply clarify |
|
150 apply (rule conjI) |
|
151 prefer 2 |
|
152 apply (rename_tac a pp vv zzz a2 s t zz) |
|
153 apply (erule alpha_bn_inducts) |
|
154 apply (rule alpha_bn_refl) |
|
155 apply clarify |
|
156 apply (rename_tac t' a1 a2 n1 n2) |
|
157 thm subst_substa_graph.intros[no_vars] |
|
158 . |
|
159 alpha_bn (substa s t (ACons n1 t' a1)) |
|
160 (substa s t (ACons n2 t' a2)) |
|
161 |
|
162 alpha_bn (Acons s (subst a t t') a1) |
|
163 (Acons s (subst a t t') a2) |
|
164 |
|
165 ACons v (subst v t t') as" |
81 |
166 |
82 end |
167 end |
83 |
168 |
84 |
169 |
85 |
170 |