98 | "subst s t (App l r) = App (subst s t l) (subst s t r)" |
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)" |
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)" |
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" |
101 | "substa s t ANil = ANil" |
102 | "substa s t (ACons v t' as) = ACons v (subst v t t') as" |
102 | "substa s t (ACons v t' as) = ACons v (subst v t t') as" |
103 oops |
103 (*unfolding eqvt_def subst_substa_graph_def |
|
104 apply (rule, perm_simp)*) |
|
105 defer |
|
106 apply (rule TrueI) |
|
107 apply (case_tac x) |
|
108 apply (case_tac a) |
|
109 apply (rule_tac y="c" and c="(aa,b)" in trm_assn.strong_exhaust(1)) |
|
110 apply (auto simp add: fresh_star_def)[3] |
|
111 apply (drule_tac x="assn" in meta_spec) |
|
112 apply (simp add: Abs1_eq_iff alpha_bn_refl) |
|
113 apply (case_tac b) |
|
114 apply (case_tac c rule: trm_assn.exhaust(2)) |
|
115 apply (auto)[2] |
|
116 apply blast |
|
117 apply blast |
|
118 apply auto |
|
119 apply (simp_all add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff]) |
|
120 apply (simp_all add: meta_eq_to_obj_eq[OF substa_def, symmetric, unfolded fun_eq_iff]) |
|
121 prefer 3 |
|
122 apply (erule alpha_bn_inducts) |
|
123 apply (simp add: alpha_bn_refl) |
|
124 (* Needs an invariant *) |
|
125 oops |
104 |
126 |
105 (*apply (subgoal_tac "\<forall>l. \<exists>!r. subst_substa_graph l r") |
|
106 defer |
|
107 apply rule |
|
108 apply (simp only: Ex1_def) |
|
109 apply (case_tac l) |
|
110 apply (case_tac a) |
|
111 apply (rule_tac y="c" and c="(aa,b)" in trm_assn.strong_exhaust(1)) |
|
112 apply simp_all[3] |
|
113 apply rule |
|
114 apply rule |
|
115 apply (rule subst_substa_graph.intros)*) |
|
116 |
|
117 (* |
|
118 defer |
|
119 apply (case_tac x) |
|
120 apply (case_tac a) |
|
121 thm trm_assn.strong_exhaust(1) |
|
122 apply (rule_tac y="c" and c="(aa,b)" in trm_assn.strong_exhaust(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) |
|
126 apply auto[1] |
|
127 apply (simp add: trm_assn.distinct trm_assn.eq_iff fresh_star_def) |
|
128 apply (simp add: trm_assn.distinct trm_assn.eq_iff) |
|
129 apply (drule_tac x="assn" in meta_spec) |
|
130 apply (rotate_tac 3) |
|
131 apply (drule_tac x="aa" in meta_spec) |
|
132 apply (rotate_tac -1) |
|
133 apply (drule_tac x="b" in meta_spec) |
|
134 apply (rotate_tac -1) |
|
135 apply (drule_tac x="trm" in meta_spec) |
|
136 apply (auto simp add: alpha_bn_refl)[1] |
|
137 apply (case_tac b) |
|
138 apply (rule_tac ya="c" in trm_assn.strong_exhaust(2)) |
|
139 apply (simp add: trm_assn.distinct trm_assn.eq_iff) |
|
140 apply auto[1] |
|
141 apply blast |
|
142 apply (simp add: trm_assn.distinct trm_assn.eq_iff) |
|
143 apply auto[1] |
|
144 apply blast |
|
145 apply (simp_all only: sum.simps Pair_eq trm_assn.distinct trm_assn.eq_iff) |
|
146 apply simp_all |
|
147 apply (simp_all add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff]) |
|
148 apply (simp_all add: meta_eq_to_obj_eq[OF substa_def, symmetric, unfolded fun_eq_iff]) |
|
149 apply clarify |
|
150 prefer 2 |
|
151 apply clarify |
|
152 apply (rule conjI) |
|
153 prefer 2 |
|
154 apply (rename_tac a pp vv zzz a2 s t zz) |
|
155 apply (erule alpha_bn_inducts) |
|
156 apply (rule alpha_bn_refl) |
|
157 apply clarify |
|
158 apply (rename_tac t' a1 a2 n1 n2) |
|
159 thm subst_substa_graph.intros[no_vars] |
|
160 . |
|
161 alpha_bn (substa s t (ACons n1 t' a1)) |
|
162 (substa s t (ACons n2 t' a2)) |
|
163 |
|
164 alpha_bn (Acons s (subst a t t') a1) |
|
165 (Acons s (subst a t t') a2) |
|
166 |
|
167 ACons v (subst v t t') as" |
|
168 *) |
|
169 end |
127 end |
170 |
128 |
171 |
129 |
172 |
130 |