349 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
349 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
350 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
350 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
351 apply(rule cheat) |
351 apply(rule cheat) |
352 prefer 2 |
352 prefer 2 |
353 apply(rule cheat) |
353 apply(rule cheat) |
|
354 apply(tactic {* r_mk_comb_tac' @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
355 thm RES_FORALL_RSP |
|
356 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
357 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
358 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
359 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
360 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
361 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
362 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
363 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
364 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
365 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
366 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
367 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
368 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
369 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
370 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
371 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
372 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
373 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
374 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
375 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
376 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
377 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
378 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
379 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
380 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
381 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
382 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
383 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
384 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
385 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
386 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
387 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
388 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
389 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
390 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
391 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
392 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
393 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
394 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
395 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
396 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
397 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
398 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
399 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
400 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
354 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
401 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
355 |
402 |
356 quotient_def |
403 quotient_def |
357 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
404 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
358 where |
405 where |