414 declare (in CLF) f_cl [simp] |
414 declare (in CLF) f_cl [simp] |
415 |
415 |
416 (*never proved, 2007-01-22: Tarski__CLF_unnamed_lemma |
416 (*never proved, 2007-01-22: Tarski__CLF_unnamed_lemma |
417 NOT PROVABLE because of the conjunction used in the definition: we don't |
417 NOT PROVABLE because of the conjunction used in the definition: we don't |
418 allow reasoning with rules like conjE, which is essential here.*) |
418 allow reasoning with rules like conjE, which is essential here.*) |
419 ML_command{*AtpWrapper.problem_name:="Tarski__CLF_unnamed_lemma"*} |
419 declare [[ atp_problem_prefix = "Tarski__CLF_unnamed_lemma" ]] |
420 lemma (in CLF) [simp]: |
420 lemma (in CLF) [simp]: |
421 "f: pset cl -> pset cl & monotone f (pset cl) (order cl)" |
421 "f: pset cl -> pset cl & monotone f (pset cl) (order cl)" |
422 apply (insert f_cl) |
422 apply (insert f_cl) |
423 apply (unfold CLF_set_def) |
423 apply (unfold CLF_set_def) |
424 apply (erule SigmaE2) |
424 apply (erule SigmaE2) |
431 |
431 |
432 lemma (in CLF) monotone_f: "monotone f A r" |
432 lemma (in CLF) monotone_f: "monotone f A r" |
433 by (simp add: A_def r_def) |
433 by (simp add: A_def r_def) |
434 |
434 |
435 (*never proved, 2007-01-22*) |
435 (*never proved, 2007-01-22*) |
436 ML_command{*AtpWrapper.problem_name:="Tarski__CLF_CLF_dual"*} |
436 declare [[ atp_problem_prefix = "Tarski__CLF_CLF_dual" ]] |
437 declare (in CLF) CLF_set_def [simp] CL_dualCL [simp] monotone_dual [simp] dualA_iff [simp] |
437 declare (in CLF) CLF_set_def [simp] CL_dualCL [simp] monotone_dual [simp] dualA_iff [simp] |
438 |
438 |
439 lemma (in CLF) CLF_dual: "(dual cl, f) \<in> CLF_set" |
439 lemma (in CLF) CLF_dual: "(dual cl, f) \<in> CLF_set" |
440 apply (simp del: dualA_iff) |
440 apply (simp del: dualA_iff) |
441 apply (simp) |
441 apply (simp) |
459 |
459 |
460 |
460 |
461 subsection {* lemmas for Tarski, lub *} |
461 subsection {* lemmas for Tarski, lub *} |
462 |
462 |
463 (*never proved, 2007-01-22*) |
463 (*never proved, 2007-01-22*) |
464 ML{*AtpWrapper.problem_name:="Tarski__CLF_lubH_le_flubH"*} |
464 declare [[ atp_problem_prefix = "Tarski__CLF_lubH_le_flubH" ]] |
465 declare CL.lub_least[intro] CLF.f_in_funcset[intro] funcset_mem[intro] CL.lub_in_lattice[intro] PO.transE[intro] PO.monotoneE[intro] CLF.monotone_f[intro] CL.lub_upper[intro] |
465 declare CL.lub_least[intro] CLF.f_in_funcset[intro] funcset_mem[intro] CL.lub_in_lattice[intro] PO.transE[intro] PO.monotoneE[intro] CLF.monotone_f[intro] CL.lub_upper[intro] |
466 lemma (in CLF) lubH_le_flubH: |
466 lemma (in CLF) lubH_le_flubH: |
467 "H = {x. (x, f x) \<in> r & x \<in> A} ==> (lub H cl, f (lub H cl)) \<in> r" |
467 "H = {x. (x, f x) \<in> r & x \<in> A} ==> (lub H cl, f (lub H cl)) \<in> r" |
468 apply (rule lub_least, fast) |
468 apply (rule lub_least, fast) |
469 apply (rule f_in_funcset [THEN funcset_mem]) |
469 apply (rule f_in_funcset [THEN funcset_mem]) |
470 apply (rule lub_in_lattice, fast) |
470 apply (rule lub_in_lattice, fast) |
471 -- {* @{text "\<forall>x:H. (x, f (lub H r)) \<in> r"} *} |
471 -- {* @{text "\<forall>x:H. (x, f (lub H r)) \<in> r"} *} |
472 apply (rule ballI) |
472 apply (rule ballI) |
473 (*never proved, 2007-01-22*) |
473 (*never proved, 2007-01-22*) |
474 ML_command{*AtpWrapper.problem_name:="Tarski__CLF_lubH_le_flubH_simpler"*} |
474 using [[ atp_problem_prefix = "Tarski__CLF_lubH_le_flubH_simpler" ]] |
475 apply (rule transE) |
475 apply (rule transE) |
476 -- {* instantiates @{text "(x, ?z) \<in> order cl to (x, f x)"}, *} |
476 -- {* instantiates @{text "(x, ?z) \<in> order cl to (x, f x)"}, *} |
477 -- {* because of the def of @{text H} *} |
477 -- {* because of the def of @{text H} *} |
478 apply fast |
478 apply fast |
479 -- {* so it remains to show @{text "(f x, f (lub H cl)) \<in> r"} *} |
479 -- {* so it remains to show @{text "(f x, f (lub H cl)) \<in> r"} *} |
487 funcset_mem[rule del] CL.lub_in_lattice[rule del] |
487 funcset_mem[rule del] CL.lub_in_lattice[rule del] |
488 PO.transE[rule del] PO.monotoneE[rule del] |
488 PO.transE[rule del] PO.monotoneE[rule del] |
489 CLF.monotone_f[rule del] CL.lub_upper[rule del] |
489 CLF.monotone_f[rule del] CL.lub_upper[rule del] |
490 |
490 |
491 (*never proved, 2007-01-22*) |
491 (*never proved, 2007-01-22*) |
492 ML{*AtpWrapper.problem_name:="Tarski__CLF_flubH_le_lubH"*} |
492 declare [[ atp_problem_prefix = "Tarski__CLF_flubH_le_lubH" ]] |
493 declare CLF.f_in_funcset[intro] funcset_mem[intro] CL.lub_in_lattice[intro] |
493 declare CLF.f_in_funcset[intro] funcset_mem[intro] CL.lub_in_lattice[intro] |
494 PO.monotoneE[intro] CLF.monotone_f[intro] CL.lub_upper[intro] |
494 PO.monotoneE[intro] CLF.monotone_f[intro] CL.lub_upper[intro] |
495 CLF.lubH_le_flubH[simp] |
495 CLF.lubH_le_flubH[simp] |
496 lemma (in CLF) flubH_le_lubH: |
496 lemma (in CLF) flubH_le_lubH: |
497 "[| H = {x. (x, f x) \<in> r & x \<in> A} |] ==> (f (lub H cl), lub H cl) \<in> r" |
497 "[| H = {x. (x, f x) \<in> r & x \<in> A} |] ==> (f (lub H cl), lub H cl) \<in> r" |
498 apply (rule lub_upper, fast) |
498 apply (rule lub_upper, fast) |
499 apply (rule_tac t = "H" in ssubst, assumption) |
499 apply (rule_tac t = "H" in ssubst, assumption) |
500 apply (rule CollectI) |
500 apply (rule CollectI) |
501 apply (rule conjI) |
501 apply (rule conjI) |
502 ML_command{*AtpWrapper.problem_name:="Tarski__CLF_flubH_le_lubH_simpler"*} |
502 using [[ atp_problem_prefix = "Tarski__CLF_flubH_le_lubH_simpler" ]] |
503 (*??no longer terminates, with combinators |
503 (*??no longer terminates, with combinators |
504 apply (metis CO_refl_on lubH_le_flubH monotone_def monotone_f reflD1 reflD2) |
504 apply (metis CO_refl_on lubH_le_flubH monotone_def monotone_f reflD1 reflD2) |
505 *) |
505 *) |
506 apply (metis CO_refl_on lubH_le_flubH monotoneE [OF monotone_f] refl_onD1 refl_onD2) |
506 apply (metis CO_refl_on lubH_le_flubH monotoneE [OF monotone_f] refl_onD1 refl_onD2) |
507 apply (metis CO_refl_on lubH_le_flubH refl_onD2) |
507 apply (metis CO_refl_on lubH_le_flubH refl_onD2) |
511 CLF.monotone_f[rule del] CL.lub_upper[rule del] |
511 CLF.monotone_f[rule del] CL.lub_upper[rule del] |
512 CLF.lubH_le_flubH[simp del] |
512 CLF.lubH_le_flubH[simp del] |
513 |
513 |
514 |
514 |
515 (*never proved, 2007-01-22*) |
515 (*never proved, 2007-01-22*) |
516 ML{*AtpWrapper.problem_name:="Tarski__CLF_lubH_is_fixp"*} |
516 declare [[ atp_problem_prefix = "Tarski__CLF_lubH_is_fixp" ]] |
517 (*Single-step version fails. The conjecture clauses refer to local abstraction |
517 (*Single-step version fails. The conjecture clauses refer to local abstraction |
518 functions (Frees), which prevents expand_defs_tac from removing those |
518 functions (Frees), which prevents expand_defs_tac from removing those |
519 "definitions" at the end of the proof. *) |
519 "definitions" at the end of the proof. *) |
520 lemma (in CLF) lubH_is_fixp: |
520 lemma (in CLF) lubH_is_fixp: |
521 "H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A" |
521 "H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A" |
586 |
586 |
587 lemma (in CLF) (*lubH_is_fixp:*) |
587 lemma (in CLF) (*lubH_is_fixp:*) |
588 "H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A" |
588 "H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A" |
589 apply (simp add: fix_def) |
589 apply (simp add: fix_def) |
590 apply (rule conjI) |
590 apply (rule conjI) |
591 ML_command{*AtpWrapper.problem_name:="Tarski__CLF_lubH_is_fixp_simpler"*} |
591 using [[ atp_problem_prefix = "Tarski__CLF_lubH_is_fixp_simpler" ]] |
592 apply (metis CO_refl_on lubH_le_flubH refl_onD1) |
592 apply (metis CO_refl_on lubH_le_flubH refl_onD1) |
593 apply (metis antisymE flubH_le_lubH lubH_le_flubH) |
593 apply (metis antisymE flubH_le_lubH lubH_le_flubH) |
594 done |
594 done |
595 |
595 |
596 lemma (in CLF) fix_in_H: |
596 lemma (in CLF) fix_in_H: |
605 apply (rule lub_upper, fast) |
605 apply (rule lub_upper, fast) |
606 apply (rule fix_in_H) |
606 apply (rule fix_in_H) |
607 apply (simp_all add: P_def) |
607 apply (simp_all add: P_def) |
608 done |
608 done |
609 |
609 |
610 ML{*AtpWrapper.problem_name:="Tarski__CLF_lubH_least_fixf"*} |
610 declare [[ atp_problem_prefix = "Tarski__CLF_lubH_least_fixf" ]] |
611 lemma (in CLF) lubH_least_fixf: |
611 lemma (in CLF) lubH_least_fixf: |
612 "H = {x. (x, f x) \<in> r & x \<in> A} |
612 "H = {x. (x, f x) \<in> r & x \<in> A} |
613 ==> \<forall>L. (\<forall>y \<in> fix f A. (y,L) \<in> r) --> (lub H cl, L) \<in> r" |
613 ==> \<forall>L. (\<forall>y \<in> fix f A. (y,L) \<in> r) --> (lub H cl, L) \<in> r" |
614 apply (metis P_def lubH_is_fixp) |
614 apply (metis P_def lubH_is_fixp) |
615 done |
615 done |
616 |
616 |
617 subsection {* Tarski fixpoint theorem 1, first part *} |
617 subsection {* Tarski fixpoint theorem 1, first part *} |
618 ML{*AtpWrapper.problem_name:="Tarski__CLF_T_thm_1_lub"*} |
618 declare [[ atp_problem_prefix = "Tarski__CLF_T_thm_1_lub" ]] |
619 declare CL.lubI[intro] fix_subset[intro] CL.lub_in_lattice[intro] |
619 declare CL.lubI[intro] fix_subset[intro] CL.lub_in_lattice[intro] |
620 CLF.fixf_le_lubH[simp] CLF.lubH_least_fixf[simp] |
620 CLF.fixf_le_lubH[simp] CLF.lubH_least_fixf[simp] |
621 lemma (in CLF) T_thm_1_lub: "lub P cl = lub {x. (x, f x) \<in> r & x \<in> A} cl" |
621 lemma (in CLF) T_thm_1_lub: "lub P cl = lub {x. (x, f x) \<in> r & x \<in> A} cl" |
622 (*sledgehammer;*) |
622 (*sledgehammer;*) |
623 apply (rule sym) |
623 apply (rule sym) |
624 apply (simp add: P_def) |
624 apply (simp add: P_def) |
625 apply (rule lubI) |
625 apply (rule lubI) |
626 ML_command{*AtpWrapper.problem_name:="Tarski__CLF_T_thm_1_lub_simpler"*} |
626 using [[ atp_problem_prefix = "Tarski__CLF_T_thm_1_lub_simpler" ]] |
627 apply (metis P_def fix_subset) |
627 apply (metis P_def fix_subset) |
628 apply (metis Collect_conj_eq Collect_mem_eq Int_commute Int_lower1 lub_in_lattice vimage_def) |
628 apply (metis Collect_conj_eq Collect_mem_eq Int_commute Int_lower1 lub_in_lattice vimage_def) |
629 (*??no longer terminates, with combinators |
629 (*??no longer terminates, with combinators |
630 apply (metis P_def fix_def fixf_le_lubH) |
630 apply (metis P_def fix_def fixf_le_lubH) |
631 apply (metis P_def fix_def lubH_least_fixf) |
631 apply (metis P_def fix_def lubH_least_fixf) |
636 declare CL.lubI[rule del] fix_subset[rule del] CL.lub_in_lattice[rule del] |
636 declare CL.lubI[rule del] fix_subset[rule del] CL.lub_in_lattice[rule del] |
637 CLF.fixf_le_lubH[simp del] CLF.lubH_least_fixf[simp del] |
637 CLF.fixf_le_lubH[simp del] CLF.lubH_least_fixf[simp del] |
638 |
638 |
639 |
639 |
640 (*never proved, 2007-01-22*) |
640 (*never proved, 2007-01-22*) |
641 ML{*AtpWrapper.problem_name:="Tarski__CLF_glbH_is_fixp"*} |
641 declare [[ atp_problem_prefix = "Tarski__CLF_glbH_is_fixp" ]] |
642 declare glb_dual_lub[simp] PO.dualA_iff[intro] CLF.lubH_is_fixp[intro] |
642 declare glb_dual_lub[simp] PO.dualA_iff[intro] CLF.lubH_is_fixp[intro] |
643 PO.dualPO[intro] CL.CL_dualCL[intro] PO.dualr_iff[simp] |
643 PO.dualPO[intro] CL.CL_dualCL[intro] PO.dualr_iff[simp] |
644 lemma (in CLF) glbH_is_fixp: "H = {x. (f x, x) \<in> r & x \<in> A} ==> glb H cl \<in> P" |
644 lemma (in CLF) glbH_is_fixp: "H = {x. (f x, x) \<in> r & x \<in> A} ==> glb H cl \<in> P" |
645 -- {* Tarski for glb *} |
645 -- {* Tarski for glb *} |
646 (*sledgehammer;*) |
646 (*sledgehammer;*) |
660 declare glb_dual_lub[simp del] PO.dualA_iff[rule del] CLF.lubH_is_fixp[rule del] |
660 declare glb_dual_lub[simp del] PO.dualA_iff[rule del] CLF.lubH_is_fixp[rule del] |
661 PO.dualPO[rule del] CL.CL_dualCL[rule del] PO.dualr_iff[simp del] |
661 PO.dualPO[rule del] CL.CL_dualCL[rule del] PO.dualr_iff[simp del] |
662 |
662 |
663 |
663 |
664 (*never proved, 2007-01-22*) |
664 (*never proved, 2007-01-22*) |
665 ML{*AtpWrapper.problem_name:="Tarski__T_thm_1_glb"*} (*ALL THEOREMS*) |
665 declare [[ atp_problem_prefix = "Tarski__T_thm_1_glb" ]] (*ALL THEOREMS*) |
666 lemma (in CLF) T_thm_1_glb: "glb P cl = glb {x. (f x, x) \<in> r & x \<in> A} cl" |
666 lemma (in CLF) T_thm_1_glb: "glb P cl = glb {x. (f x, x) \<in> r & x \<in> A} cl" |
667 (*sledgehammer;*) |
667 (*sledgehammer;*) |
668 apply (simp add: glb_dual_lub P_def A_def r_def) |
668 apply (simp add: glb_dual_lub P_def A_def r_def) |
669 apply (rule dualA_iff [THEN subst]) |
669 apply (rule dualA_iff [THEN subst]) |
670 (*never proved, 2007-01-22*) |
670 (*never proved, 2007-01-22*) |
671 ML_command{*AtpWrapper.problem_name:="Tarski__T_thm_1_glb_simpler"*} (*ALL THEOREMS*) |
671 using [[ atp_problem_prefix = "Tarski__T_thm_1_glb_simpler" ]] (*ALL THEOREMS*) |
672 (*sledgehammer;*) |
672 (*sledgehammer;*) |
673 apply (simp add: CLF.T_thm_1_lub [of _ f, OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro, |
673 apply (simp add: CLF.T_thm_1_lub [of _ f, OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro, |
674 OF dualPO CL_dualCL] dualPO CL_dualCL CLF_dual dualr_iff) |
674 OF dualPO CL_dualCL] dualPO CL_dualCL CLF_dual dualr_iff) |
675 done |
675 done |
676 |
676 |
677 subsection {* interval *} |
677 subsection {* interval *} |
678 |
678 |
679 |
679 |
680 ML{*AtpWrapper.problem_name:="Tarski__rel_imp_elem"*} |
680 declare [[ atp_problem_prefix = "Tarski__rel_imp_elem" ]] |
681 declare (in CLF) CO_refl_on[simp] refl_on_def [simp] |
681 declare (in CLF) CO_refl_on[simp] refl_on_def [simp] |
682 lemma (in CLF) rel_imp_elem: "(x, y) \<in> r ==> x \<in> A" |
682 lemma (in CLF) rel_imp_elem: "(x, y) \<in> r ==> x \<in> A" |
683 by (metis CO_refl_on refl_onD1) |
683 by (metis CO_refl_on refl_onD1) |
684 declare (in CLF) CO_refl_on[simp del] refl_on_def [simp del] |
684 declare (in CLF) CO_refl_on[simp del] refl_on_def [simp del] |
685 |
685 |
686 ML{*AtpWrapper.problem_name:="Tarski__interval_subset"*} |
686 declare [[ atp_problem_prefix = "Tarski__interval_subset" ]] |
687 declare (in CLF) rel_imp_elem[intro] |
687 declare (in CLF) rel_imp_elem[intro] |
688 declare interval_def [simp] |
688 declare interval_def [simp] |
689 lemma (in CLF) interval_subset: "[| a \<in> A; b \<in> A |] ==> interval r a b \<subseteq> A" |
689 lemma (in CLF) interval_subset: "[| a \<in> A; b \<in> A |] ==> interval r a b \<subseteq> A" |
690 by (metis CO_refl_on interval_imp_mem refl_onD refl_onD2 rel_imp_elem subset_eq) |
690 by (metis CO_refl_on interval_imp_mem refl_onD refl_onD2 rel_imp_elem subset_eq) |
691 declare (in CLF) rel_imp_elem[rule del] |
691 declare (in CLF) rel_imp_elem[rule del] |
716 |
716 |
717 lemma (in CLF) S_intv_cl: |
717 lemma (in CLF) S_intv_cl: |
718 "[| a \<in> A; b \<in> A; S \<subseteq> interval r a b |]==> S \<subseteq> A" |
718 "[| a \<in> A; b \<in> A; S \<subseteq> interval r a b |]==> S \<subseteq> A" |
719 by (simp add: subset_trans [OF _ interval_subset]) |
719 by (simp add: subset_trans [OF _ interval_subset]) |
720 |
720 |
721 ML{*AtpWrapper.problem_name:="Tarski__L_in_interval"*} (*ALL THEOREMS*) |
721 declare [[ atp_problem_prefix = "Tarski__L_in_interval" ]] (*ALL THEOREMS*) |
722 lemma (in CLF) L_in_interval: |
722 lemma (in CLF) L_in_interval: |
723 "[| a \<in> A; b \<in> A; S \<subseteq> interval r a b; |
723 "[| a \<in> A; b \<in> A; S \<subseteq> interval r a b; |
724 S \<noteq> {}; isLub S cl L; interval r a b \<noteq> {} |] ==> L \<in> interval r a b" |
724 S \<noteq> {}; isLub S cl L; interval r a b \<noteq> {} |] ==> L \<in> interval r a b" |
725 (*WON'T TERMINATE |
725 (*WON'T TERMINATE |
726 apply (metis CO_trans intervalI interval_lemma1 interval_lemma2 isLub_least isLub_upper subset_empty subset_iff trans_def) |
726 apply (metis CO_trans intervalI interval_lemma1 interval_lemma2 isLub_least isLub_upper subset_empty subset_iff trans_def) |
735 -- {* @{text "(L, b) \<in> r"} *} |
735 -- {* @{text "(L, b) \<in> r"} *} |
736 apply (simp add: isLub_least interval_lemma2) |
736 apply (simp add: isLub_least interval_lemma2) |
737 done |
737 done |
738 |
738 |
739 (*never proved, 2007-01-22*) |
739 (*never proved, 2007-01-22*) |
740 ML{*AtpWrapper.problem_name:="Tarski__G_in_interval"*} (*ALL THEOREMS*) |
740 declare [[ atp_problem_prefix = "Tarski__G_in_interval" ]] (*ALL THEOREMS*) |
741 lemma (in CLF) G_in_interval: |
741 lemma (in CLF) G_in_interval: |
742 "[| a \<in> A; b \<in> A; interval r a b \<noteq> {}; S \<subseteq> interval r a b; isGlb S cl G; |
742 "[| a \<in> A; b \<in> A; interval r a b \<noteq> {}; S \<subseteq> interval r a b; isGlb S cl G; |
743 S \<noteq> {} |] ==> G \<in> interval r a b" |
743 S \<noteq> {} |] ==> G \<in> interval r a b" |
744 apply (simp add: interval_dual) |
744 apply (simp add: interval_dual) |
745 apply (simp add: CLF.L_in_interval [of _ f, OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] |
745 apply (simp add: CLF.L_in_interval [of _ f, OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] |
746 dualA_iff A_def dualPO CL_dualCL CLF_dual isGlb_dual_isLub) |
746 dualA_iff A_def dualPO CL_dualCL CLF_dual isGlb_dual_isLub) |
747 done |
747 done |
748 |
748 |
749 ML{*AtpWrapper.problem_name:="Tarski__intervalPO"*} (*ALL THEOREMS*) |
749 declare [[ atp_problem_prefix = "Tarski__intervalPO" ]] (*ALL THEOREMS*) |
750 lemma (in CLF) intervalPO: |
750 lemma (in CLF) intervalPO: |
751 "[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |] |
751 "[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |] |
752 ==> (| pset = interval r a b, order = induced (interval r a b) r |) |
752 ==> (| pset = interval r a b, order = induced (interval r a b) r |) |
753 \<in> PartialOrder" |
753 \<in> PartialOrder" |
754 proof (neg_clausify) |
754 proof (neg_clausify) |
817 done |
817 done |
818 |
818 |
819 lemmas (in CLF) intv_CL_glb = intv_CL_lub [THEN Rdual] |
819 lemmas (in CLF) intv_CL_glb = intv_CL_lub [THEN Rdual] |
820 |
820 |
821 (*never proved, 2007-01-22*) |
821 (*never proved, 2007-01-22*) |
822 ML{*AtpWrapper.problem_name:="Tarski__interval_is_sublattice"*} (*ALL THEOREMS*) |
822 declare [[ atp_problem_prefix = "Tarski__interval_is_sublattice" ]] (*ALL THEOREMS*) |
823 lemma (in CLF) interval_is_sublattice: |
823 lemma (in CLF) interval_is_sublattice: |
824 "[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |] |
824 "[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |] |
825 ==> interval r a b <<= cl" |
825 ==> interval r a b <<= cl" |
826 (*sledgehammer *) |
826 (*sledgehammer *) |
827 apply (rule sublatticeI) |
827 apply (rule sublatticeI) |
828 apply (simp add: interval_subset) |
828 apply (simp add: interval_subset) |
829 (*never proved, 2007-01-22*) |
829 (*never proved, 2007-01-22*) |
830 ML_command{*AtpWrapper.problem_name:="Tarski__interval_is_sublattice_simpler"*} |
830 using [[ atp_problem_prefix = "Tarski__interval_is_sublattice_simpler" ]] |
831 (*sledgehammer *) |
831 (*sledgehammer *) |
832 apply (rule CompleteLatticeI) |
832 apply (rule CompleteLatticeI) |
833 apply (simp add: intervalPO) |
833 apply (simp add: intervalPO) |
834 apply (simp add: intv_CL_lub) |
834 apply (simp add: intv_CL_lub) |
835 apply (simp add: intv_CL_glb) |
835 apply (simp add: intv_CL_glb) |
844 by (simp add: Top_def Bot_def least_def greatest_def dualA_iff dualr_iff) |
844 by (simp add: Top_def Bot_def least_def greatest_def dualA_iff dualr_iff) |
845 |
845 |
846 lemma (in CLF) Bot_dual_Top: "Bot cl = Top (dual cl)" |
846 lemma (in CLF) Bot_dual_Top: "Bot cl = Top (dual cl)" |
847 by (simp add: Top_def Bot_def least_def greatest_def dualA_iff dualr_iff) |
847 by (simp add: Top_def Bot_def least_def greatest_def dualA_iff dualr_iff) |
848 |
848 |
849 ML_command{*AtpWrapper.problem_name:="Tarski__Bot_in_lattice"*} (*ALL THEOREMS*) |
849 declare [[ atp_problem_prefix = "Tarski__Bot_in_lattice" ]] (*ALL THEOREMS*) |
850 lemma (in CLF) Bot_in_lattice: "Bot cl \<in> A" |
850 lemma (in CLF) Bot_in_lattice: "Bot cl \<in> A" |
851 (*sledgehammer; *) |
851 (*sledgehammer; *) |
852 apply (simp add: Bot_def least_def) |
852 apply (simp add: Bot_def least_def) |
853 apply (rule_tac a="glb A cl" in someI2) |
853 apply (rule_tac a="glb A cl" in someI2) |
854 apply (simp_all add: glb_in_lattice glb_lower |
854 apply (simp_all add: glb_in_lattice glb_lower |
855 r_def [symmetric] A_def [symmetric]) |
855 r_def [symmetric] A_def [symmetric]) |
856 done |
856 done |
857 |
857 |
858 (*first proved 2007-01-25 after relaxing relevance*) |
858 (*first proved 2007-01-25 after relaxing relevance*) |
859 ML_command{*AtpWrapper.problem_name:="Tarski__Top_in_lattice"*} (*ALL THEOREMS*) |
859 declare [[ atp_problem_prefix = "Tarski__Top_in_lattice" ]] (*ALL THEOREMS*) |
860 lemma (in CLF) Top_in_lattice: "Top cl \<in> A" |
860 lemma (in CLF) Top_in_lattice: "Top cl \<in> A" |
861 (*sledgehammer;*) |
861 (*sledgehammer;*) |
862 apply (simp add: Top_dual_Bot A_def) |
862 apply (simp add: Top_dual_Bot A_def) |
863 (*first proved 2007-01-25 after relaxing relevance*) |
863 (*first proved 2007-01-25 after relaxing relevance*) |
864 ML_command{*AtpWrapper.problem_name:="Tarski__Top_in_lattice_simpler"*} (*ALL THEOREMS*) |
864 using [[ atp_problem_prefix = "Tarski__Top_in_lattice_simpler" ]] (*ALL THEOREMS*) |
865 (*sledgehammer*) |
865 (*sledgehammer*) |
866 apply (rule dualA_iff [THEN subst]) |
866 apply (rule dualA_iff [THEN subst]) |
867 apply (blast intro!: CLF.Bot_in_lattice [OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] dualPO CL_dualCL CLF_dual) |
867 apply (blast intro!: CLF.Bot_in_lattice [OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] dualPO CL_dualCL CLF_dual) |
868 done |
868 done |
869 |
869 |
874 apply (simp_all add: lub_in_lattice lub_upper |
874 apply (simp_all add: lub_in_lattice lub_upper |
875 r_def [symmetric] A_def [symmetric]) |
875 r_def [symmetric] A_def [symmetric]) |
876 done |
876 done |
877 |
877 |
878 (*never proved, 2007-01-22*) |
878 (*never proved, 2007-01-22*) |
879 ML_command{*AtpWrapper.problem_name:="Tarski__Bot_prop"*} (*ALL THEOREMS*) |
879 declare [[ atp_problem_prefix = "Tarski__Bot_prop" ]] (*ALL THEOREMS*) |
880 lemma (in CLF) Bot_prop: "x \<in> A ==> (Bot cl, x) \<in> r" |
880 lemma (in CLF) Bot_prop: "x \<in> A ==> (Bot cl, x) \<in> r" |
881 (*sledgehammer*) |
881 (*sledgehammer*) |
882 apply (simp add: Bot_dual_Top r_def) |
882 apply (simp add: Bot_dual_Top r_def) |
883 apply (rule dualr_iff [THEN subst]) |
883 apply (rule dualr_iff [THEN subst]) |
884 apply (simp add: CLF.Top_prop [of _ f, OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] |
884 apply (simp add: CLF.Top_prop [of _ f, OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] |
885 dualA_iff A_def dualPO CL_dualCL CLF_dual) |
885 dualA_iff A_def dualPO CL_dualCL CLF_dual) |
886 done |
886 done |
887 |
887 |
888 ML_command{*AtpWrapper.problem_name:="Tarski__Bot_in_lattice"*} (*ALL THEOREMS*) |
888 declare [[ atp_problem_prefix = "Tarski__Bot_in_lattice" ]] (*ALL THEOREMS*) |
889 lemma (in CLF) Top_intv_not_empty: "x \<in> A ==> interval r x (Top cl) \<noteq> {}" |
889 lemma (in CLF) Top_intv_not_empty: "x \<in> A ==> interval r x (Top cl) \<noteq> {}" |
890 apply (metis Top_in_lattice Top_prop empty_iff intervalI reflE) |
890 apply (metis Top_in_lattice Top_prop empty_iff intervalI reflE) |
891 done |
891 done |
892 |
892 |
893 ML_command{*AtpWrapper.problem_name:="Tarski__Bot_intv_not_empty"*} (*ALL THEOREMS*) |
893 declare [[ atp_problem_prefix = "Tarski__Bot_intv_not_empty" ]] (*ALL THEOREMS*) |
894 lemma (in CLF) Bot_intv_not_empty: "x \<in> A ==> interval r (Bot cl) x \<noteq> {}" |
894 lemma (in CLF) Bot_intv_not_empty: "x \<in> A ==> interval r (Bot cl) x \<noteq> {}" |
895 apply (metis Bot_prop ex_in_conv intervalI reflE rel_imp_elem) |
895 apply (metis Bot_prop ex_in_conv intervalI reflE rel_imp_elem) |
896 done |
896 done |
897 |
897 |
898 |
898 |
900 |
900 |
901 lemma (in CLF) fixf_po: "(| pset = P, order = induced P r|) \<in> PartialOrder" |
901 lemma (in CLF) fixf_po: "(| pset = P, order = induced P r|) \<in> PartialOrder" |
902 by (simp add: P_def fix_subset po_subset_po) |
902 by (simp add: P_def fix_subset po_subset_po) |
903 |
903 |
904 (*first proved 2007-01-25 after relaxing relevance*) |
904 (*first proved 2007-01-25 after relaxing relevance*) |
905 ML_command{*AtpWrapper.problem_name:="Tarski__Y_subset_A"*} |
905 declare [[ atp_problem_prefix = "Tarski__Y_subset_A" ]] |
906 declare (in Tarski) P_def[simp] Y_ss [simp] |
906 declare (in Tarski) P_def[simp] Y_ss [simp] |
907 declare fix_subset [intro] subset_trans [intro] |
907 declare fix_subset [intro] subset_trans [intro] |
908 lemma (in Tarski) Y_subset_A: "Y \<subseteq> A" |
908 lemma (in Tarski) Y_subset_A: "Y \<subseteq> A" |
909 (*sledgehammer*) |
909 (*sledgehammer*) |
910 apply (rule subset_trans [OF _ fix_subset]) |
910 apply (rule subset_trans [OF _ fix_subset]) |
916 |
916 |
917 lemma (in Tarski) lubY_in_A: "lub Y cl \<in> A" |
917 lemma (in Tarski) lubY_in_A: "lub Y cl \<in> A" |
918 by (rule Y_subset_A [THEN lub_in_lattice]) |
918 by (rule Y_subset_A [THEN lub_in_lattice]) |
919 |
919 |
920 (*never proved, 2007-01-22*) |
920 (*never proved, 2007-01-22*) |
921 ML_command{*AtpWrapper.problem_name:="Tarski__lubY_le_flubY"*} (*ALL THEOREMS*) |
921 declare [[ atp_problem_prefix = "Tarski__lubY_le_flubY" ]] (*ALL THEOREMS*) |
922 lemma (in Tarski) lubY_le_flubY: "(lub Y cl, f (lub Y cl)) \<in> r" |
922 lemma (in Tarski) lubY_le_flubY: "(lub Y cl, f (lub Y cl)) \<in> r" |
923 (*sledgehammer*) |
923 (*sledgehammer*) |
924 apply (rule lub_least) |
924 apply (rule lub_least) |
925 apply (rule Y_subset_A) |
925 apply (rule Y_subset_A) |
926 apply (rule f_in_funcset [THEN funcset_mem]) |
926 apply (rule f_in_funcset [THEN funcset_mem]) |
927 apply (rule lubY_in_A) |
927 apply (rule lubY_in_A) |
928 -- {* @{text "Y \<subseteq> P ==> f x = x"} *} |
928 -- {* @{text "Y \<subseteq> P ==> f x = x"} *} |
929 apply (rule ballI) |
929 apply (rule ballI) |
930 ML_command{*AtpWrapper.problem_name:="Tarski__lubY_le_flubY_simpler"*} (*ALL THEOREMS*) |
930 using [[ atp_problem_prefix = "Tarski__lubY_le_flubY_simpler" ]] (*ALL THEOREMS*) |
931 (*sledgehammer *) |
931 (*sledgehammer *) |
932 apply (rule_tac t = "x" in fix_imp_eq [THEN subst]) |
932 apply (rule_tac t = "x" in fix_imp_eq [THEN subst]) |
933 apply (erule Y_ss [simplified P_def, THEN subsetD]) |
933 apply (erule Y_ss [simplified P_def, THEN subsetD]) |
934 -- {* @{text "reduce (f x, f (lub Y cl)) \<in> r to (x, lub Y cl) \<in> r"} by monotonicity *} |
934 -- {* @{text "reduce (f x, f (lub Y cl)) \<in> r to (x, lub Y cl) \<in> r"} by monotonicity *} |
935 ML_command{*AtpWrapper.problem_name:="Tarski__lubY_le_flubY_simplest"*} (*ALL THEOREMS*) |
935 using [[ atp_problem_prefix = "Tarski__lubY_le_flubY_simplest" ]] (*ALL THEOREMS*) |
936 (*sledgehammer*) |
936 (*sledgehammer*) |
937 apply (rule_tac f = "f" in monotoneE) |
937 apply (rule_tac f = "f" in monotoneE) |
938 apply (rule monotone_f) |
938 apply (rule monotone_f) |
939 apply (simp add: Y_subset_A [THEN subsetD]) |
939 apply (simp add: Y_subset_A [THEN subsetD]) |
940 apply (rule lubY_in_A) |
940 apply (rule lubY_in_A) |
941 apply (simp add: lub_upper Y_subset_A) |
941 apply (simp add: lub_upper Y_subset_A) |
942 done |
942 done |
943 |
943 |
944 (*first proved 2007-01-25 after relaxing relevance*) |
944 (*first proved 2007-01-25 after relaxing relevance*) |
945 ML_command{*AtpWrapper.problem_name:="Tarski__intY1_subset"*} (*ALL THEOREMS*) |
945 declare [[ atp_problem_prefix = "Tarski__intY1_subset" ]] (*ALL THEOREMS*) |
946 lemma (in Tarski) intY1_subset: "intY1 \<subseteq> A" |
946 lemma (in Tarski) intY1_subset: "intY1 \<subseteq> A" |
947 (*sledgehammer*) |
947 (*sledgehammer*) |
948 apply (unfold intY1_def) |
948 apply (unfold intY1_def) |
949 apply (rule interval_subset) |
949 apply (rule interval_subset) |
950 apply (rule lubY_in_A) |
950 apply (rule lubY_in_A) |
952 done |
952 done |
953 |
953 |
954 lemmas (in Tarski) intY1_elem = intY1_subset [THEN subsetD] |
954 lemmas (in Tarski) intY1_elem = intY1_subset [THEN subsetD] |
955 |
955 |
956 (*never proved, 2007-01-22*) |
956 (*never proved, 2007-01-22*) |
957 ML_command{*AtpWrapper.problem_name:="Tarski__intY1_f_closed"*} (*ALL THEOREMS*) |
957 declare [[ atp_problem_prefix = "Tarski__intY1_f_closed" ]] (*ALL THEOREMS*) |
958 lemma (in Tarski) intY1_f_closed: "x \<in> intY1 \<Longrightarrow> f x \<in> intY1" |
958 lemma (in Tarski) intY1_f_closed: "x \<in> intY1 \<Longrightarrow> f x \<in> intY1" |
959 (*sledgehammer*) |
959 (*sledgehammer*) |
960 apply (simp add: intY1_def interval_def) |
960 apply (simp add: intY1_def interval_def) |
961 apply (rule conjI) |
961 apply (rule conjI) |
962 apply (rule transE) |
962 apply (rule transE) |
963 apply (rule lubY_le_flubY) |
963 apply (rule lubY_le_flubY) |
964 -- {* @{text "(f (lub Y cl), f x) \<in> r"} *} |
964 -- {* @{text "(f (lub Y cl), f x) \<in> r"} *} |
965 ML_command{*AtpWrapper.problem_name:="Tarski__intY1_f_closed_simpler"*} (*ALL THEOREMS*) |
965 using [[ atp_problem_prefix = "Tarski__intY1_f_closed_simpler" ]] (*ALL THEOREMS*) |
966 (*sledgehammer [has been proved before now...]*) |
966 (*sledgehammer [has been proved before now...]*) |
967 apply (rule_tac f=f in monotoneE) |
967 apply (rule_tac f=f in monotoneE) |
968 apply (rule monotone_f) |
968 apply (rule monotone_f) |
969 apply (rule lubY_in_A) |
969 apply (rule lubY_in_A) |
970 apply (simp add: intY1_def interval_def intY1_elem) |
970 apply (simp add: intY1_def interval_def intY1_elem) |
973 apply (rule Top_prop) |
973 apply (rule Top_prop) |
974 apply (rule f_in_funcset [THEN funcset_mem]) |
974 apply (rule f_in_funcset [THEN funcset_mem]) |
975 apply (simp add: intY1_def interval_def intY1_elem) |
975 apply (simp add: intY1_def interval_def intY1_elem) |
976 done |
976 done |
977 |
977 |
978 ML_command{*AtpWrapper.problem_name:="Tarski__intY1_func"*} (*ALL THEOREMS*) |
978 declare [[ atp_problem_prefix = "Tarski__intY1_func" ]] (*ALL THEOREMS*) |
979 lemma (in Tarski) intY1_func: "(%x: intY1. f x) \<in> intY1 -> intY1" |
979 lemma (in Tarski) intY1_func: "(%x: intY1. f x) \<in> intY1 -> intY1" |
980 apply (rule restrict_in_funcset) |
980 apply (rule restrict_in_funcset) |
981 apply (metis intY1_f_closed restrict_in_funcset) |
981 apply (metis intY1_f_closed restrict_in_funcset) |
982 done |
982 done |
983 |
983 |
984 ML_command{*AtpWrapper.problem_name:="Tarski__intY1_mono"*} (*ALL THEOREMS*) |
984 declare [[ atp_problem_prefix = "Tarski__intY1_mono" ]] (*ALL THEOREMS*) |
985 lemma (in Tarski) intY1_mono: |
985 lemma (in Tarski) intY1_mono: |
986 "monotone (%x: intY1. f x) intY1 (induced intY1 r)" |
986 "monotone (%x: intY1. f x) intY1 (induced intY1 r)" |
987 (*sledgehammer *) |
987 (*sledgehammer *) |
988 apply (auto simp add: monotone_def induced_def intY1_f_closed) |
988 apply (auto simp add: monotone_def induced_def intY1_f_closed) |
989 apply (blast intro: intY1_elem monotone_f [THEN monotoneE]) |
989 apply (blast intro: intY1_elem monotone_f [THEN monotoneE]) |
990 done |
990 done |
991 |
991 |
992 (*proof requires relaxing relevance: 2007-01-25*) |
992 (*proof requires relaxing relevance: 2007-01-25*) |
993 ML_command{*AtpWrapper.problem_name:="Tarski__intY1_is_cl"*} (*ALL THEOREMS*) |
993 declare [[ atp_problem_prefix = "Tarski__intY1_is_cl" ]] (*ALL THEOREMS*) |
994 lemma (in Tarski) intY1_is_cl: |
994 lemma (in Tarski) intY1_is_cl: |
995 "(| pset = intY1, order = induced intY1 r |) \<in> CompleteLattice" |
995 "(| pset = intY1, order = induced intY1 r |) \<in> CompleteLattice" |
996 (*sledgehammer*) |
996 (*sledgehammer*) |
997 apply (unfold intY1_def) |
997 apply (unfold intY1_def) |
998 apply (rule interv_is_compl_latt) |
998 apply (rule interv_is_compl_latt) |
1001 apply (rule Top_intv_not_empty) |
1001 apply (rule Top_intv_not_empty) |
1002 apply (rule lubY_in_A) |
1002 apply (rule lubY_in_A) |
1003 done |
1003 done |
1004 |
1004 |
1005 (*never proved, 2007-01-22*) |
1005 (*never proved, 2007-01-22*) |
1006 ML_command{*AtpWrapper.problem_name:="Tarski__v_in_P"*} (*ALL THEOREMS*) |
1006 declare [[ atp_problem_prefix = "Tarski__v_in_P" ]] (*ALL THEOREMS*) |
1007 lemma (in Tarski) v_in_P: "v \<in> P" |
1007 lemma (in Tarski) v_in_P: "v \<in> P" |
1008 (*sledgehammer*) |
1008 (*sledgehammer*) |
1009 apply (unfold P_def) |
1009 apply (unfold P_def) |
1010 apply (rule_tac A = "intY1" in fixf_subset) |
1010 apply (rule_tac A = "intY1" in fixf_subset) |
1011 apply (rule intY1_subset) |
1011 apply (rule intY1_subset) |
1012 apply (simp add: CLF.glbH_is_fixp [OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro, OF _ intY1_is_cl, simplified] |
1012 apply (simp add: CLF.glbH_is_fixp [OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro, OF _ intY1_is_cl, simplified] |
1013 v_def CL_imp_PO intY1_is_cl CLF_set_def intY1_func intY1_mono) |
1013 v_def CL_imp_PO intY1_is_cl CLF_set_def intY1_func intY1_mono) |
1014 done |
1014 done |
1015 |
1015 |
1016 ML_command{*AtpWrapper.problem_name:="Tarski__z_in_interval"*} (*ALL THEOREMS*) |
1016 declare [[ atp_problem_prefix = "Tarski__z_in_interval" ]] (*ALL THEOREMS*) |
1017 lemma (in Tarski) z_in_interval: |
1017 lemma (in Tarski) z_in_interval: |
1018 "[| z \<in> P; \<forall>y\<in>Y. (y, z) \<in> induced P r |] ==> z \<in> intY1" |
1018 "[| z \<in> P; \<forall>y\<in>Y. (y, z) \<in> induced P r |] ==> z \<in> intY1" |
1019 (*sledgehammer *) |
1019 (*sledgehammer *) |
1020 apply (unfold intY1_def P_def) |
1020 apply (unfold intY1_def P_def) |
1021 apply (rule intervalI) |
1021 apply (rule intervalI) |
1025 apply (rule Y_subset_A) |
1025 apply (rule Y_subset_A) |
1026 apply (fast elim!: fix_subset [THEN subsetD]) |
1026 apply (fast elim!: fix_subset [THEN subsetD]) |
1027 apply (simp add: induced_def) |
1027 apply (simp add: induced_def) |
1028 done |
1028 done |
1029 |
1029 |
1030 ML_command{*AtpWrapper.problem_name:="Tarski__fz_in_int_rel"*} (*ALL THEOREMS*) |
1030 declare [[ atp_problem_prefix = "Tarski__fz_in_int_rel" ]] (*ALL THEOREMS*) |
1031 lemma (in Tarski) f'z_in_int_rel: "[| z \<in> P; \<forall>y\<in>Y. (y, z) \<in> induced P r |] |
1031 lemma (in Tarski) f'z_in_int_rel: "[| z \<in> P; \<forall>y\<in>Y. (y, z) \<in> induced P r |] |
1032 ==> ((%x: intY1. f x) z, z) \<in> induced intY1 r" |
1032 ==> ((%x: intY1. f x) z, z) \<in> induced intY1 r" |
1033 apply (metis P_def acc_def fix_imp_eq fix_subset indI reflE restrict_apply subset_eq z_in_interval) |
1033 apply (metis P_def acc_def fix_imp_eq fix_subset indI reflE restrict_apply subset_eq z_in_interval) |
1034 done |
1034 done |
1035 |
1035 |
1036 (*never proved, 2007-01-22*) |
1036 (*never proved, 2007-01-22*) |
1037 ML_command{*AtpWrapper.problem_name:="Tarski__tarski_full_lemma"*} (*ALL THEOREMS*) |
1037 declare [[ atp_problem_prefix = "Tarski__tarski_full_lemma" ]] (*ALL THEOREMS*) |
1038 lemma (in Tarski) tarski_full_lemma: |
1038 lemma (in Tarski) tarski_full_lemma: |
1039 "\<exists>L. isLub Y (| pset = P, order = induced P r |) L" |
1039 "\<exists>L. isLub Y (| pset = P, order = induced P r |) L" |
1040 apply (rule_tac x = "v" in exI) |
1040 apply (rule_tac x = "v" in exI) |
1041 apply (simp add: isLub_def) |
1041 apply (simp add: isLub_def) |
1042 -- {* @{text "v \<in> P"} *} |
1042 -- {* @{text "v \<in> P"} *} |
1062 apply (rule indI) |
1062 apply (rule indI) |
1063 prefer 3 apply assumption |
1063 prefer 3 apply assumption |
1064 prefer 2 apply (simp add: v_in_P) |
1064 prefer 2 apply (simp add: v_in_P) |
1065 apply (unfold v_def) |
1065 apply (unfold v_def) |
1066 (*never proved, 2007-01-22*) |
1066 (*never proved, 2007-01-22*) |
1067 ML_command{*AtpWrapper.problem_name:="Tarski__tarski_full_lemma_simpler"*} |
1067 using [[ atp_problem_prefix = "Tarski__tarski_full_lemma_simpler" ]] |
1068 (*sledgehammer*) |
1068 (*sledgehammer*) |
1069 apply (rule indE) |
1069 apply (rule indE) |
1070 apply (rule_tac [2] intY1_subset) |
1070 apply (rule_tac [2] intY1_subset) |
1071 (*never proved, 2007-01-22*) |
1071 (*never proved, 2007-01-22*) |
1072 ML_command{*AtpWrapper.problem_name:="Tarski__tarski_full_lemma_simplest"*} |
1072 using [[ atp_problem_prefix = "Tarski__tarski_full_lemma_simplest" ]] |
1073 (*sledgehammer*) |
1073 (*sledgehammer*) |
1074 apply (rule CL.glb_lower [OF CL.intro, OF PO.intro CL_axioms.intro, OF _ intY1_is_cl, simplified]) |
1074 apply (rule CL.glb_lower [OF CL.intro, OF PO.intro CL_axioms.intro, OF _ intY1_is_cl, simplified]) |
1075 apply (simp add: CL_imp_PO intY1_is_cl) |
1075 apply (simp add: CL_imp_PO intY1_is_cl) |
1076 apply force |
1076 apply force |
1077 apply (simp add: induced_def intY1_f_closed z_in_interval) |
1077 apply (simp add: induced_def intY1_f_closed z_in_interval) |
1085 ==> (| pset = A, order = r |) \<in> CompleteLattice" |
1085 ==> (| pset = A, order = r |) \<in> CompleteLattice" |
1086 by (simp add: CompleteLatticeI Rdual) |
1086 by (simp add: CompleteLatticeI Rdual) |
1087 |
1087 |
1088 |
1088 |
1089 (*never proved, 2007-01-22*) |
1089 (*never proved, 2007-01-22*) |
1090 ML_command{*AtpWrapper.problem_name:="Tarski__Tarski_full"*} |
1090 declare [[ atp_problem_prefix = "Tarski__Tarski_full" ]] |
1091 declare (in CLF) fixf_po[intro] P_def [simp] A_def [simp] r_def [simp] |
1091 declare (in CLF) fixf_po[intro] P_def [simp] A_def [simp] r_def [simp] |
1092 Tarski.tarski_full_lemma [intro] cl_po [intro] cl_co [intro] |
1092 Tarski.tarski_full_lemma [intro] cl_po [intro] cl_co [intro] |
1093 CompleteLatticeI_simp [intro] |
1093 CompleteLatticeI_simp [intro] |
1094 theorem (in CLF) Tarski_full: |
1094 theorem (in CLF) Tarski_full: |
1095 "(| pset = P, order = induced P r|) \<in> CompleteLattice" |
1095 "(| pset = P, order = induced P r|) \<in> CompleteLattice" |
1096 (*sledgehammer*) |
1096 (*sledgehammer*) |
1097 apply (rule CompleteLatticeI_simp) |
1097 apply (rule CompleteLatticeI_simp) |
1098 apply (rule fixf_po, clarify) |
1098 apply (rule fixf_po, clarify) |
1099 (*never proved, 2007-01-22*) |
1099 (*never proved, 2007-01-22*) |
1100 ML_command{*AtpWrapper.problem_name:="Tarski__Tarski_full_simpler"*} |
1100 using [[ atp_problem_prefix = "Tarski__Tarski_full_simpler" ]] |
1101 (*sledgehammer*) |
1101 (*sledgehammer*) |
1102 apply (simp add: P_def A_def r_def) |
1102 apply (simp add: P_def A_def r_def) |
1103 apply (blast intro!: Tarski.tarski_full_lemma [OF Tarski.intro, OF CLF.intro Tarski_axioms.intro, |
1103 apply (blast intro!: Tarski.tarski_full_lemma [OF Tarski.intro, OF CLF.intro Tarski_axioms.intro, |
1104 OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] cl_po cl_co f_cl) |
1104 OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] cl_po cl_co f_cl) |
1105 done |
1105 done |