346 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
346 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
347 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
347 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
348 apply(rule cheat) |
348 apply(rule cheat) |
349 prefer 2 |
349 prefer 2 |
350 apply(rule cheat) |
350 apply(rule cheat) |
|
351 apply(tactic {* r_mk_comb_tac' @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
352 thm RES_FORALL_RSP |
|
353 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*}) |
|
355 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
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*}) |
351 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*}) |
352 sorry |
399 sorry |
353 |
400 |
354 quotient_def |
401 quotient_def |
355 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
402 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |