319 |
319 |
320 lemma acc_le_listI [intro!]: |
320 lemma acc_le_listI [intro!]: |
321 "\<lbrakk> order r; acc r \<rbrakk> \<Longrightarrow> acc(Listn.le r)" |
321 "\<lbrakk> order r; acc r \<rbrakk> \<Longrightarrow> acc(Listn.le r)" |
322 apply (unfold acc_def) |
322 apply (unfold acc_def) |
323 apply (subgoal_tac |
323 apply (subgoal_tac |
324 "wf(UN n. {(ys,xs). size xs = n & size ys = n & xs <_(Listn.le r) ys})") |
324 "wfP (SUP n. (\<lambda>ys xs. size xs = n & size ys = n & xs <_(Listn.le r) ys))") |
325 apply (erule wf_subset) |
325 apply (erule wfP_subset) |
326 apply (blast intro: lesssub_list_impl_same_size) |
326 apply (blast intro: lesssub_list_impl_same_size) |
327 apply (rule wf_UN) |
327 apply (rule wfP_SUP) |
328 prefer 2 |
328 prefer 2 |
329 apply clarify |
329 apply clarify |
330 apply (rename_tac m n) |
330 apply (rename_tac m n) |
331 apply (case_tac "m=n") |
331 apply (case_tac "m=n") |
332 apply simp |
332 apply simp |
333 apply (fast intro!: equals0I dest: not_sym) |
333 apply (fast intro!: equals0I [to_pred] dest: not_sym) |
334 apply clarify |
334 apply clarify |
335 apply (rename_tac n) |
335 apply (rename_tac n) |
336 apply (induct_tac n) |
336 apply (induct_tac n) |
337 apply (simp add: lesssub_def cong: conj_cong) |
337 apply (simp add: lesssub_def cong: conj_cong) |
338 apply (rename_tac k) |
338 apply (rename_tac k) |
339 apply (simp add: wf_eq_minimal) |
339 apply (simp add: wfP_eq_minimal) |
340 apply (simp (no_asm) add: length_Suc_conv cong: conj_cong) |
340 apply (simp (no_asm) add: length_Suc_conv cong: conj_cong) |
341 apply clarify |
341 apply clarify |
342 apply (rename_tac M m) |
342 apply (rename_tac M m) |
343 apply (case_tac "\<exists>x xs. size xs = k & x#xs : M") |
343 apply (case_tac "\<exists>x xs. size xs = k & x#xs : M") |
344 prefer 2 |
344 prefer 2 |