346 |
346 |
347 lemma cheat: "P" sorry |
347 lemma cheat: "P" sorry |
348 |
348 |
349 lemma imp_refl: "P \<longrightarrow> P" by simp |
349 lemma imp_refl: "P \<longrightarrow> P" by simp |
350 |
350 |
|
351 lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P" |
|
352 apply(auto) |
|
353 done |
|
354 |
351 thm Set.conj_mono |
355 thm Set.conj_mono |
352 thm Set.imp_mono |
356 thm Set.imp_mono |
353 ML {* Inductive.get_monos @{context} *} |
357 ML {* Inductive.get_monos @{context} *} |
354 |
358 |
355 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
359 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
363 apply(rule my_equiv_res_forallR) |
367 apply(rule my_equiv_res_forallR) |
364 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
368 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
365 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
369 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
366 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
370 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
367 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
371 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
368 apply(rule Set.imp_mono) |
372 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
373 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
374 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
375 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
369 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
376 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
370 apply(rule my_equiv_res_forallL) |
377 apply(rule my_equiv_res_forallL) |
371 apply(rule cheat) |
378 apply(rule cheat) |
|
379 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
372 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
380 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
373 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
381 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
374 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
382 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
375 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
383 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
376 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
384 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |