353 done |
353 done |
354 |
354 |
355 thm Set.conj_mono |
355 thm Set.conj_mono |
356 thm Set.imp_mono |
356 thm Set.imp_mono |
357 ML {* Inductive.get_monos @{context} *} |
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 |
358 |
377 |
359 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
378 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
360 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
379 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
361 defer |
380 defer |
362 apply(rule cheat) |
381 apply(rule cheat) |
363 apply(rule cheat) |
382 apply(rule cheat) |
364 apply(atomize (full)) |
383 apply(atomize (full)) |
365 apply(rule my_equiv_res_forallR) |
384 apply(rule RIGHT_RES_FORALL_REGULAR) |
366 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
385 apply(rule RIGHT_RES_FORALL_REGULAR) |
367 apply(rule my_equiv_res_forallR) |
386 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+ |
368 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
387 apply(rule LEFT_RES_FORALL_REGULAR) |
369 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
388 apply(rule conjI) |
370 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
389 using list_eq_refl |
371 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
390 thm Ball_def IN_RESPECTS FUN_REL.simps |
372 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
391 |
373 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
392 apply - |
374 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
393 apply(simp (no_asm) add: Respects_def) |
375 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
394 apply(blast) |
376 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
395 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
377 apply(rule my_equiv_res_forallL) |
396 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
378 apply(rule cheat) |
397 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
379 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
398 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
380 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
399 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
381 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
400 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
382 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
401 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
383 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
402 apply(rule LEFT_RES_FORALL_REGULAR) |
384 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
403 apply(rule conjI) |
385 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
404 defer |
386 done |
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 |
387 |
413 |
388 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
414 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
389 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
415 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
390 defer |
416 defer |
391 apply(rule cheat) |
417 apply(rule cheat) |