157 defer |
157 defer |
158 apply (simp add: eqvt_at_def height_trm_def) |
158 apply (simp add: eqvt_at_def height_trm_def) |
159 apply (simp add: eqvt_at_def height_trm_def) |
159 apply (simp add: eqvt_at_def height_trm_def) |
160 apply (simp add: eqvt_at_def height_bp_def) |
160 apply (simp add: eqvt_at_def height_bp_def) |
161 apply (simp add: eqvt_at_def height_bp_def) |
161 apply (simp add: eqvt_at_def height_bp_def) |
162 --"I'd like to apply FCB here, but the following fails" |
|
163 apply (subgoal_tac "height_bp bp = height_bp bpa") |
162 apply (subgoal_tac "height_bp bp = height_bp bpa") |
164 apply (subgoal_tac "height_trm b = height_trm ba") |
163 apply (subgoal_tac "height_trm b = height_trm ba") |
165 apply simp |
164 apply simp |
166 apply (subgoal_tac "(\<lambda>as x c. height_trm (snd (bp, b))) as x c = (\<lambda>as x c. height_trm (snd (bpa, ba))) as x c") |
165 apply (subgoal_tac "(\<lambda>as x c. height_trm (snd (bp, b))) as x c = (\<lambda>as x c. height_trm (snd (bpa, ba))) as x c") |
167 apply simp |
166 apply simp |
168 apply (erule_tac c="()" and ba="bn" and f="\<lambda>as x c. height_trm (snd x)" in Abs_lst_fcb2) |
167 apply (erule_tac c="()" in Abs_lst_fcb2) |
169 ... |
168 apply (simp add: fresh_star_def pure_fresh) |
|
169 apply (simp add: fresh_star_def pure_fresh) |
|
170 apply (simp add: fresh_star_def pure_fresh) |
|
171 apply (simp add: eqvt_at_def) |
|
172 apply (simp add: eqvt_at_def) |
|
173 defer defer |
|
174 apply (subgoal_tac "(\<lambda>as x c. height_bp (fst (bp, b))) as x c = (\<lambda>as x c. height_bp (fst (bpa, ba))) as x c") |
|
175 apply simp |
|
176 apply (erule_tac c="()" in Abs_lst_fcb2) |
|
177 apply (simp add: fresh_star_def pure_fresh) |
|
178 apply (simp add: fresh_star_def pure_fresh) |
|
179 apply (simp add: fresh_star_def pure_fresh) |
|
180 apply (simp add: fresh_star_def pure_fresh) |
|
181 apply (simp add: eqvt_at_def) |
|
182 apply (simp add: eqvt_at_def) |
|
183 --"" |
170 done |
184 done |
171 |
185 |
172 termination by lexicographic_order |
186 termination by lexicographic_order |
173 |
187 |
174 end |
188 end |