343 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) |
343 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) |
344 done |
344 done |
345 |
345 |
346 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *} |
346 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *} |
347 ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} |
347 ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} |
|
348 |
|
349 lemma cheat: "P" sorry |
|
350 |
|
351 lemma imp_refl: "P \<longrightarrow> P" by simp |
|
352 |
|
353 thm Set.conj_mono |
|
354 thm Set.imp_mono |
|
355 ML {* Inductive.get_monos @{context} *} |
|
356 |
348 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
357 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
349 apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *}) |
358 apply(tactic {* procedure_tac @{thm list.induct} @{context} 1 *}) |
350 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *}) |
359 defer |
351 apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *}) |
360 apply(rule cheat) |
352 done |
361 apply(rule cheat) |
|
362 apply(atomize (full)) |
|
363 apply(rule my_equiv_res_forallR) |
|
364 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
365 apply(rule my_equiv_res_forallR) |
|
366 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
367 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
368 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
369 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
370 apply(rule Set.imp_mono) |
|
371 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
372 apply(rule my_equiv_res_forallL) |
|
373 apply(rule cheat) |
|
374 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
375 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
376 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
377 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
378 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
379 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
380 done |
|
381 |
|
382 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
|
383 apply(tactic {* procedure_tac @{thm list.induct} @{context} 1 *}) |
|
384 defer |
|
385 apply(rule cheat) |
|
386 apply(rule cheat) |
|
387 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
|
388 oops |
353 |
389 |
354 quotient_def |
390 quotient_def |
355 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
391 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
356 where |
392 where |
357 "fset_rec \<equiv> list_rec" |
393 "fset_rec \<equiv> list_rec" |