343 |
343 |
344 lemma cheat: "P" sorry |
344 lemma cheat: "P" sorry |
345 |
345 |
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(tactic {* regularize_tac @{context} [rel_eqv] rel_refl 1 *}) |
349 prefer 2 |
349 prefer 2 |
350 apply(rule cheat) |
350 apply (tactic {* clean_tac @{context} quot defs reps_same absrep [(@{typ "('a list \<Rightarrow> bool)"},@{typ "('a fset \<Rightarrow> bool)"})] 1 *}) |
351 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*}) |
352 thm RES_FORALL_RSP |
352 done |
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*}) |
|
398 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
|
399 sorry |
|
400 |
353 |
401 quotient_def |
354 quotient_def |
402 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
355 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
403 where |
356 where |
404 "fset_rec \<equiv> list_rec" |
357 "fset_rec \<equiv> list_rec" |