344 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *} |
344 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *} |
345 ML {* val app_prs_thms = map (applic_prs_old @{context} rty qty absrep) aps *} |
345 ML {* val app_prs_thms = map (applic_prs_old @{context} rty qty absrep) aps *} |
346 |
346 |
347 lemma cheat: "P" sorry |
347 lemma cheat: "P" sorry |
348 |
348 |
349 lemma imp_refl: "P \<longrightarrow> P" by simp |
|
350 |
|
351 lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P" |
|
352 apply(auto) |
|
353 done |
|
354 |
|
355 thm Set.conj_mono |
|
356 thm Set.imp_mono |
|
357 ML {* Inductive.get_monos @{context} *} |
|
358 thm LEFT_RES_FORALL_REGULAR |
|
359 |
|
360 lemma test: |
|
361 fixes P Q::"'a \<Rightarrow> bool" |
|
362 and x::"'a" |
|
363 assumes a: "REFL R2" |
|
364 and b: "\<And>f. Q (f x) \<Longrightarrow> P (f x)" |
|
365 shows "(\<forall>f\<in>(Respects (R1 ===> R2)). Q (f x)) \<longrightarrow> (\<forall>f. P (f x))" |
|
366 apply(rule impI) |
|
367 apply(rule allI) |
|
368 apply(drule_tac x="\<lambda>y. f x" in bspec) |
|
369 apply(simp add: Respects_def IN_RESPECTS) |
|
370 apply(rule impI) |
|
371 using a |
|
372 apply(simp add: REFL_def) |
|
373 using b |
|
374 apply - |
|
375 apply(simp) |
|
376 done |
|
377 |
|
378 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" |
379 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
350 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
380 defer |
|
381 apply(rule cheat) |
351 apply(rule cheat) |
|
352 prefer 2 |
382 apply(rule cheat) |
353 apply(rule cheat) |
383 apply(atomize (full)) |
354 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
384 apply(rule RIGHT_RES_FORALL_REGULAR) |
|
385 apply(rule RIGHT_RES_FORALL_REGULAR) |
|
386 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+ |
|
387 apply(rule LEFT_RES_FORALL_REGULAR) |
|
388 apply(rule conjI) |
|
389 using list_eq_refl |
|
390 thm Ball_def IN_RESPECTS FUN_REL.simps |
|
391 |
|
392 apply - |
|
393 apply(simp (no_asm) add: Respects_def) |
|
394 apply(blast) |
|
395 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
396 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
397 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
398 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
399 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
400 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
401 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
402 apply(rule LEFT_RES_FORALL_REGULAR) |
|
403 apply(rule conjI) |
|
404 defer |
|
405 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
406 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
407 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
408 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
409 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
410 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
411 apply(unfold Respects_def) |
|
412 sorry |
|
413 |
|
414 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
|
415 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
|
416 defer |
|
417 apply(rule cheat) |
|
418 apply(rule cheat) |
|
419 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
|
420 done |
|
421 |
355 |
422 quotient_def |
356 quotient_def |
423 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
357 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
424 where |
358 where |
425 "fset_rec \<equiv> list_rec" |
359 "fset_rec \<equiv> list_rec" |