291 apply (simp (no_asm_simp) add: interval_def) |
289 apply (simp (no_asm_simp) add: interval_def) |
292 apply (simp add: PO_imp_trans interval_not_empty) |
290 apply (simp add: PO_imp_trans interval_not_empty) |
293 apply (simp add: reflE) |
291 apply (simp add: reflE) |
294 done |
292 done |
295 |
293 |
296 |
|
297 subsection {* sublattice *} |
294 subsection {* sublattice *} |
298 |
295 |
299 lemma (in PO) sublattice_imp_CL: |
296 lemma (in PO) sublattice_imp_CL: |
300 "S <<= cl ==> (| pset = S, order = induced S r |) \<in> CompleteLattice" |
297 "S <<= cl ==> (| pset = S, order = induced S r |) \<in> CompleteLattice" |
301 by (simp add: sublattice_def CompleteLattice_def A_def r_def) |
298 by (simp add: sublattice_def CompleteLattice_def A_def r_def) |
302 |
299 |
303 lemma (in CL) sublatticeI: |
300 lemma (in CL) sublatticeI: |
304 "[| S \<subseteq> A; (| pset = S, order = induced S r |) \<in> CompleteLattice |] |
301 "[| S \<subseteq> A; (| pset = S, order = induced S r |) \<in> CompleteLattice |] |
305 ==> S <<= cl" |
302 ==> S <<= cl" |
306 by (simp add: sublattice_def A_def r_def) |
303 by (simp add: sublattice_def A_def r_def) |
307 |
|
308 |
304 |
309 subsection {* lub *} |
305 subsection {* lub *} |
310 |
306 |
311 lemma (in CL) lub_unique: "[| S \<subseteq> A; isLub S cl x; isLub S cl L|] ==> x = L" |
307 lemma (in CL) lub_unique: "[| S \<subseteq> A; isLub S cl x; isLub S cl L|] ==> x = L" |
312 apply (rule antisymE) |
308 apply (rule antisymE) |
428 |
421 |
429 lemma (in CLF) monotone_f: "monotone f A r" |
422 lemma (in CLF) monotone_f: "monotone f A r" |
430 by (simp add: A_def r_def) |
423 by (simp add: A_def r_def) |
431 |
424 |
432 (*never proved, 2007-01-22*) |
425 (*never proved, 2007-01-22*) |
433 declare [[ sledgehammer_problem_prefix = "Tarski__CLF_CLF_dual" ]] |
426 |
434 declare (in CLF) CLF_set_def [simp] CL_dualCL [simp] monotone_dual [simp] dualA_iff [simp] |
427 declare (in CLF) CLF_set_def [simp] CL_dualCL [simp] monotone_dual [simp] dualA_iff [simp] |
435 |
428 |
436 lemma (in CLF) CLF_dual: "(dual cl, f) \<in> CLF_set" |
429 lemma (in CLF) CLF_dual: "(dual cl, f) \<in> CLF_set" |
437 apply (simp del: dualA_iff) |
430 apply (simp del: dualA_iff) |
438 apply (simp) |
431 apply (simp) |
439 done |
432 done |
440 |
433 |
441 declare (in CLF) CLF_set_def[simp del] CL_dualCL[simp del] monotone_dual[simp del] |
434 declare (in CLF) CLF_set_def[simp del] CL_dualCL[simp del] monotone_dual[simp del] |
442 dualA_iff[simp del] |
435 dualA_iff[simp del] |
443 |
436 |
444 |
|
445 subsection {* fixed points *} |
437 subsection {* fixed points *} |
446 |
438 |
447 lemma fix_subset: "fix f A \<subseteq> A" |
439 lemma fix_subset: "fix f A \<subseteq> A" |
448 by (simp add: fix_def, fast) |
440 by (simp add: fix_def, fast) |
449 |
441 |
452 |
444 |
453 lemma fixf_subset: |
445 lemma fixf_subset: |
454 "[| A \<subseteq> B; x \<in> fix (%y: A. f y) A |] ==> x \<in> fix f B" |
446 "[| A \<subseteq> B; x \<in> fix (%y: A. f y) A |] ==> x \<in> fix f B" |
455 by (simp add: fix_def, auto) |
447 by (simp add: fix_def, auto) |
456 |
448 |
457 |
|
458 subsection {* lemmas for Tarski, lub *} |
449 subsection {* lemmas for Tarski, lub *} |
459 |
450 |
460 (*never proved, 2007-01-22*) |
451 (*never proved, 2007-01-22*) |
461 declare [[ sledgehammer_problem_prefix = "Tarski__CLF_lubH_le_flubH" ]] |
452 |
462 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] |
453 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] |
|
454 |
463 lemma (in CLF) lubH_le_flubH: |
455 lemma (in CLF) lubH_le_flubH: |
464 "H = {x. (x, f x) \<in> r & x \<in> A} ==> (lub H cl, f (lub H cl)) \<in> r" |
456 "H = {x. (x, f x) \<in> r & x \<in> A} ==> (lub H cl, f (lub H cl)) \<in> r" |
465 apply (rule lub_least, fast) |
457 apply (rule lub_least, fast) |
466 apply (rule f_in_funcset [THEN funcset_mem]) |
458 apply (rule f_in_funcset [THEN funcset_mem]) |
467 apply (rule lub_in_lattice, fast) |
459 apply (rule lub_in_lattice, fast) |
468 -- {* @{text "\<forall>x:H. (x, f (lub H r)) \<in> r"} *} |
460 -- {* @{text "\<forall>x:H. (x, f (lub H r)) \<in> r"} *} |
469 apply (rule ballI) |
461 apply (rule ballI) |
470 (*never proved, 2007-01-22*) |
462 (*never proved, 2007-01-22*) |
471 using [[ sledgehammer_problem_prefix = "Tarski__CLF_lubH_le_flubH_simpler" ]] |
|
472 apply (rule transE) |
463 apply (rule transE) |
473 -- {* instantiates @{text "(x, ?z) \<in> order cl to (x, f x)"}, *} |
464 -- {* instantiates @{text "(x, ?z) \<in> order cl to (x, f x)"}, *} |
474 -- {* because of the def of @{text H} *} |
465 -- {* because of the def of @{text H} *} |
475 apply fast |
466 apply fast |
476 -- {* so it remains to show @{text "(f x, f (lub H cl)) \<in> r"} *} |
467 -- {* so it remains to show @{text "(f x, f (lub H cl)) \<in> r"} *} |
478 apply (rule monotone_f, fast) |
469 apply (rule monotone_f, fast) |
479 apply (rule lub_in_lattice, fast) |
470 apply (rule lub_in_lattice, fast) |
480 apply (rule lub_upper, fast) |
471 apply (rule lub_upper, fast) |
481 apply assumption |
472 apply assumption |
482 done |
473 done |
483 declare CL.lub_least[rule del] CLF.f_in_funcset[rule del] |
474 |
484 funcset_mem[rule del] CL.lub_in_lattice[rule del] |
475 declare CL.lub_least[rule del] CLF.f_in_funcset[rule del] |
485 PO.transE[rule del] PO.monotoneE[rule del] |
476 funcset_mem[rule del] CL.lub_in_lattice[rule del] |
486 CLF.monotone_f[rule del] CL.lub_upper[rule del] |
477 PO.transE[rule del] PO.monotoneE[rule del] |
487 |
478 CLF.monotone_f[rule del] CL.lub_upper[rule del] |
488 (*never proved, 2007-01-22*) |
479 |
489 declare [[ sledgehammer_problem_prefix = "Tarski__CLF_flubH_le_lubH" ]] |
480 (*never proved, 2007-01-22*) |
490 declare CLF.f_in_funcset[intro] funcset_mem[intro] CL.lub_in_lattice[intro] |
481 |
491 PO.monotoneE[intro] CLF.monotone_f[intro] CL.lub_upper[intro] |
482 declare CLF.f_in_funcset[intro] funcset_mem[intro] CL.lub_in_lattice[intro] |
492 CLF.lubH_le_flubH[simp] |
483 PO.monotoneE[intro] CLF.monotone_f[intro] CL.lub_upper[intro] |
|
484 CLF.lubH_le_flubH[simp] |
|
485 |
493 lemma (in CLF) flubH_le_lubH: |
486 lemma (in CLF) flubH_le_lubH: |
494 "[| H = {x. (x, f x) \<in> r & x \<in> A} |] ==> (f (lub H cl), lub H cl) \<in> r" |
487 "[| H = {x. (x, f x) \<in> r & x \<in> A} |] ==> (f (lub H cl), lub H cl) \<in> r" |
495 apply (rule lub_upper, fast) |
488 apply (rule lub_upper, fast) |
496 apply (rule_tac t = "H" in ssubst, assumption) |
489 apply (rule_tac t = "H" in ssubst, assumption) |
497 apply (rule CollectI) |
490 apply (rule CollectI) |
498 apply (rule conjI) |
491 apply (rule conjI) |
499 using [[ sledgehammer_problem_prefix = "Tarski__CLF_flubH_le_lubH_simpler" ]] |
|
500 (*??no longer terminates, with combinators |
492 (*??no longer terminates, with combinators |
501 apply (metis CO_refl_on lubH_le_flubH monotone_def monotone_f reflD1 reflD2) |
493 apply (metis CO_refl_on lubH_le_flubH monotone_def monotone_f reflD1 reflD2) |
502 *) |
494 *) |
503 apply (metis CO_refl_on lubH_le_flubH monotoneE [OF monotone_f] refl_onD1 refl_onD2) |
495 apply (metis CO_refl_on lubH_le_flubH monotoneE [OF monotone_f] refl_onD1 refl_onD2) |
504 apply (metis CO_refl_on lubH_le_flubH refl_onD2) |
496 apply (metis CO_refl_on lubH_le_flubH refl_onD2) |
505 done |
497 done |
506 declare CLF.f_in_funcset[rule del] funcset_mem[rule del] |
498 |
507 CL.lub_in_lattice[rule del] PO.monotoneE[rule del] |
499 declare CLF.f_in_funcset[rule del] funcset_mem[rule del] |
508 CLF.monotone_f[rule del] CL.lub_upper[rule del] |
500 CL.lub_in_lattice[rule del] PO.monotoneE[rule del] |
509 CLF.lubH_le_flubH[simp del] |
501 CLF.monotone_f[rule del] CL.lub_upper[rule del] |
510 |
502 CLF.lubH_le_flubH[simp del] |
511 |
503 |
512 (*never proved, 2007-01-22*) |
504 (*never proved, 2007-01-22*) |
513 declare [[ sledgehammer_problem_prefix = "Tarski__CLF_lubH_is_fixp" ]] |
505 |
514 (* Single-step version fails. The conjecture clauses refer to local abstraction |
506 (* Single-step version fails. The conjecture clauses refer to local abstraction |
515 functions (Frees). *) |
507 functions (Frees). *) |
516 lemma (in CLF) lubH_is_fixp: |
508 lemma (in CLF) lubH_is_fixp: |
517 "H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A" |
509 "H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A" |
518 apply (simp add: fix_def) |
510 apply (simp add: fix_def) |
547 |
539 |
548 lemma (in CLF) (*lubH_is_fixp:*) |
540 lemma (in CLF) (*lubH_is_fixp:*) |
549 "H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A" |
541 "H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A" |
550 apply (simp add: fix_def) |
542 apply (simp add: fix_def) |
551 apply (rule conjI) |
543 apply (rule conjI) |
552 using [[ sledgehammer_problem_prefix = "Tarski__CLF_lubH_is_fixp_simpler" ]] |
|
553 apply (metis CO_refl_on lubH_le_flubH refl_onD1) |
544 apply (metis CO_refl_on lubH_le_flubH refl_onD1) |
554 apply (metis antisymE flubH_le_lubH lubH_le_flubH) |
545 apply (metis antisymE flubH_le_lubH lubH_le_flubH) |
555 done |
546 done |
556 |
547 |
557 lemma (in CLF) fix_in_H: |
548 lemma (in CLF) fix_in_H: |
558 "[| H = {x. (x, f x) \<in> r & x \<in> A}; x \<in> P |] ==> x \<in> H" |
549 "[| H = {x. (x, f x) \<in> r & x \<in> A}; x \<in> P |] ==> x \<in> H" |
559 by (simp add: P_def fix_imp_eq [of _ f A] reflE CO_refl_on |
550 by (simp add: P_def fix_imp_eq [of _ f A] reflE CO_refl_on |
560 fix_subset [of f A, THEN subsetD]) |
551 fix_subset [of f A, THEN subsetD]) |
561 |
|
562 |
552 |
563 lemma (in CLF) fixf_le_lubH: |
553 lemma (in CLF) fixf_le_lubH: |
564 "H = {x. (x, f x) \<in> r & x \<in> A} ==> \<forall>x \<in> fix f A. (x, lub H cl) \<in> r" |
554 "H = {x. (x, f x) \<in> r & x \<in> A} ==> \<forall>x \<in> fix f A. (x, lub H cl) \<in> r" |
565 apply (rule ballI) |
555 apply (rule ballI) |
566 apply (rule lub_upper, fast) |
556 apply (rule lub_upper, fast) |
567 apply (rule fix_in_H) |
557 apply (rule fix_in_H) |
568 apply (simp_all add: P_def) |
558 apply (simp_all add: P_def) |
569 done |
559 done |
570 |
560 |
571 declare [[ sledgehammer_problem_prefix = "Tarski__CLF_lubH_least_fixf" ]] |
|
572 lemma (in CLF) lubH_least_fixf: |
561 lemma (in CLF) lubH_least_fixf: |
573 "H = {x. (x, f x) \<in> r & x \<in> A} |
562 "H = {x. (x, f x) \<in> r & x \<in> A} |
574 ==> \<forall>L. (\<forall>y \<in> fix f A. (y,L) \<in> r) --> (lub H cl, L) \<in> r" |
563 ==> \<forall>L. (\<forall>y \<in> fix f A. (y,L) \<in> r) --> (lub H cl, L) \<in> r" |
575 apply (metis P_def lubH_is_fixp) |
564 apply (metis P_def lubH_is_fixp) |
576 done |
565 done |
577 |
566 |
578 subsection {* Tarski fixpoint theorem 1, first part *} |
567 subsection {* Tarski fixpoint theorem 1, first part *} |
579 declare [[ sledgehammer_problem_prefix = "Tarski__CLF_T_thm_1_lub" ]] |
568 |
580 declare CL.lubI[intro] fix_subset[intro] CL.lub_in_lattice[intro] |
569 declare CL.lubI[intro] fix_subset[intro] CL.lub_in_lattice[intro] |
581 CLF.fixf_le_lubH[simp] CLF.lubH_least_fixf[simp] |
570 CLF.fixf_le_lubH[simp] CLF.lubH_least_fixf[simp] |
|
571 |
582 lemma (in CLF) T_thm_1_lub: "lub P cl = lub {x. (x, f x) \<in> r & x \<in> A} cl" |
572 lemma (in CLF) T_thm_1_lub: "lub P cl = lub {x. (x, f x) \<in> r & x \<in> A} cl" |
583 (*sledgehammer;*) |
573 (*sledgehammer;*) |
584 apply (rule sym) |
574 apply (rule sym) |
585 apply (simp add: P_def) |
575 apply (simp add: P_def) |
586 apply (rule lubI) |
576 apply (rule lubI) |
587 using [[ sledgehammer_problem_prefix = "Tarski__CLF_T_thm_1_lub_simpler" ]] |
|
588 apply (metis P_def fix_subset) |
577 apply (metis P_def fix_subset) |
589 apply (metis Collect_conj_eq Collect_mem_eq Int_commute Int_lower1 lub_in_lattice vimage_def) |
578 apply (metis Collect_conj_eq Collect_mem_eq Int_commute Int_lower1 lub_in_lattice vimage_def) |
590 (*??no longer terminates, with combinators |
579 (*??no longer terminates, with combinators |
591 apply (metis P_def fix_def fixf_le_lubH) |
580 apply (metis P_def fix_def fixf_le_lubH) |
592 apply (metis P_def fix_def lubH_least_fixf) |
581 apply (metis P_def fix_def lubH_least_fixf) |
593 *) |
582 *) |
594 apply (simp add: fixf_le_lubH) |
583 apply (simp add: fixf_le_lubH) |
595 apply (simp add: lubH_least_fixf) |
584 apply (simp add: lubH_least_fixf) |
596 done |
585 done |
597 declare CL.lubI[rule del] fix_subset[rule del] CL.lub_in_lattice[rule del] |
586 |
598 CLF.fixf_le_lubH[simp del] CLF.lubH_least_fixf[simp del] |
587 declare CL.lubI[rule del] fix_subset[rule del] CL.lub_in_lattice[rule del] |
599 |
588 CLF.fixf_le_lubH[simp del] CLF.lubH_least_fixf[simp del] |
600 |
589 |
601 (*never proved, 2007-01-22*) |
590 (*never proved, 2007-01-22*) |
602 declare [[ sledgehammer_problem_prefix = "Tarski__CLF_glbH_is_fixp" ]] |
591 |
603 declare glb_dual_lub[simp] PO.dualA_iff[intro] CLF.lubH_is_fixp[intro] |
592 declare glb_dual_lub[simp] PO.dualA_iff[intro] CLF.lubH_is_fixp[intro] |
604 PO.dualPO[intro] CL.CL_dualCL[intro] PO.dualr_iff[simp] |
593 PO.dualPO[intro] CL.CL_dualCL[intro] PO.dualr_iff[simp] |
|
594 |
605 lemma (in CLF) glbH_is_fixp: "H = {x. (f x, x) \<in> r & x \<in> A} ==> glb H cl \<in> P" |
595 lemma (in CLF) glbH_is_fixp: "H = {x. (f x, x) \<in> r & x \<in> A} ==> glb H cl \<in> P" |
606 -- {* Tarski for glb *} |
596 -- {* Tarski for glb *} |
607 (*sledgehammer;*) |
597 (*sledgehammer;*) |
608 apply (simp add: glb_dual_lub P_def A_def r_def) |
598 apply (simp add: glb_dual_lub P_def A_def r_def) |
609 apply (rule dualA_iff [THEN subst]) |
599 apply (rule dualA_iff [THEN subst]) |
616 apply (rule CL_dualCL) |
606 apply (rule CL_dualCL) |
617 apply (rule CLF_axioms.intro) |
607 apply (rule CLF_axioms.intro) |
618 apply (rule CLF_dual) |
608 apply (rule CLF_dual) |
619 apply (simp add: dualr_iff dualA_iff) |
609 apply (simp add: dualr_iff dualA_iff) |
620 done |
610 done |
621 declare glb_dual_lub[simp del] PO.dualA_iff[rule del] CLF.lubH_is_fixp[rule del] |
611 |
622 PO.dualPO[rule del] CL.CL_dualCL[rule del] PO.dualr_iff[simp del] |
612 declare glb_dual_lub[simp del] PO.dualA_iff[rule del] CLF.lubH_is_fixp[rule del] |
623 |
613 PO.dualPO[rule del] CL.CL_dualCL[rule del] PO.dualr_iff[simp del] |
624 |
614 |
625 (*never proved, 2007-01-22*) |
615 (*never proved, 2007-01-22*) |
626 declare [[ sledgehammer_problem_prefix = "Tarski__T_thm_1_glb" ]] (*ALL THEOREMS*) |
616 |
627 lemma (in CLF) T_thm_1_glb: "glb P cl = glb {x. (f x, x) \<in> r & x \<in> A} cl" |
617 lemma (in CLF) T_thm_1_glb: "glb P cl = glb {x. (f x, x) \<in> r & x \<in> A} cl" |
628 (*sledgehammer;*) |
618 (*sledgehammer;*) |
629 apply (simp add: glb_dual_lub P_def A_def r_def) |
619 apply (simp add: glb_dual_lub P_def A_def r_def) |
630 apply (rule dualA_iff [THEN subst]) |
620 apply (rule dualA_iff [THEN subst]) |
631 (*never proved, 2007-01-22*) |
621 (*never proved, 2007-01-22*) |
632 using [[ sledgehammer_problem_prefix = "Tarski__T_thm_1_glb_simpler" ]] (*ALL THEOREMS*) |
|
633 (*sledgehammer;*) |
622 (*sledgehammer;*) |
634 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, |
623 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, |
635 OF dualPO CL_dualCL] dualPO CL_dualCL CLF_dual dualr_iff) |
624 OF dualPO CL_dualCL] dualPO CL_dualCL CLF_dual dualr_iff) |
636 done |
625 done |
637 |
626 |
638 subsection {* interval *} |
627 subsection {* interval *} |
639 |
628 |
640 |
629 declare (in CLF) CO_refl_on[simp] refl_on_def [simp] |
641 declare [[ sledgehammer_problem_prefix = "Tarski__rel_imp_elem" ]] |
630 |
642 declare (in CLF) CO_refl_on[simp] refl_on_def [simp] |
|
643 lemma (in CLF) rel_imp_elem: "(x, y) \<in> r ==> x \<in> A" |
631 lemma (in CLF) rel_imp_elem: "(x, y) \<in> r ==> x \<in> A" |
644 by (metis CO_refl_on refl_onD1) |
632 by (metis CO_refl_on refl_onD1) |
645 declare (in CLF) CO_refl_on[simp del] refl_on_def [simp del] |
633 |
646 |
634 declare (in CLF) CO_refl_on[simp del] refl_on_def [simp del] |
647 declare [[ sledgehammer_problem_prefix = "Tarski__interval_subset" ]] |
635 |
648 declare (in CLF) rel_imp_elem[intro] |
636 declare (in CLF) rel_imp_elem[intro] |
649 declare interval_def [simp] |
637 declare interval_def [simp] |
|
638 |
650 lemma (in CLF) interval_subset: "[| a \<in> A; b \<in> A |] ==> interval r a b \<subseteq> A" |
639 lemma (in CLF) interval_subset: "[| a \<in> A; b \<in> A |] ==> interval r a b \<subseteq> A" |
651 by (metis CO_refl_on interval_imp_mem refl_onD refl_onD2 rel_imp_elem subset_eq) |
640 by (metis CO_refl_on interval_imp_mem refl_onD refl_onD2 rel_imp_elem subset_eq) |
652 declare (in CLF) rel_imp_elem[rule del] |
641 |
653 declare interval_def [simp del] |
642 declare (in CLF) rel_imp_elem[rule del] |
654 |
643 declare interval_def [simp del] |
655 |
644 |
656 lemma (in CLF) intervalI: |
645 lemma (in CLF) intervalI: |
657 "[| (a, x) \<in> r; (x, b) \<in> r |] ==> x \<in> interval r a b" |
646 "[| (a, x) \<in> r; (x, b) \<in> r |] ==> x \<in> interval r a b" |
658 by (simp add: interval_def) |
647 by (simp add: interval_def) |
659 |
648 |
696 -- {* @{text "(L, b) \<in> r"} *} |
685 -- {* @{text "(L, b) \<in> r"} *} |
697 apply (simp add: isLub_least interval_lemma2) |
686 apply (simp add: isLub_least interval_lemma2) |
698 done |
687 done |
699 |
688 |
700 (*never proved, 2007-01-22*) |
689 (*never proved, 2007-01-22*) |
701 declare [[ sledgehammer_problem_prefix = "Tarski__G_in_interval" ]] (*ALL THEOREMS*) |
690 |
702 lemma (in CLF) G_in_interval: |
691 lemma (in CLF) G_in_interval: |
703 "[| a \<in> A; b \<in> A; interval r a b \<noteq> {}; S \<subseteq> interval r a b; isGlb S cl G; |
692 "[| a \<in> A; b \<in> A; interval r a b \<noteq> {}; S \<subseteq> interval r a b; isGlb S cl G; |
704 S \<noteq> {} |] ==> G \<in> interval r a b" |
693 S \<noteq> {} |] ==> G \<in> interval r a b" |
705 apply (simp add: interval_dual) |
694 apply (simp add: interval_dual) |
706 apply (simp add: CLF.L_in_interval [of _ f, OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] |
695 apply (simp add: CLF.L_in_interval [of _ f, OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] |
707 dualA_iff A_def dualPO CL_dualCL CLF_dual isGlb_dual_isLub) |
696 dualA_iff A_def dualPO CL_dualCL CLF_dual isGlb_dual_isLub) |
708 done |
697 done |
709 |
698 |
710 declare [[ sledgehammer_problem_prefix = "Tarski__intervalPO" ]] (*ALL THEOREMS*) |
699 |
711 lemma (in CLF) intervalPO: |
700 lemma (in CLF) intervalPO: |
712 "[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |] |
701 "[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |] |
713 ==> (| pset = interval r a b, order = induced (interval r a b) r |) |
702 ==> (| pset = interval r a b, order = induced (interval r a b) r |) |
714 \<in> PartialOrder" |
703 \<in> PartialOrder" |
715 proof - |
704 proof - |
773 done |
762 done |
774 |
763 |
775 lemmas (in CLF) intv_CL_glb = intv_CL_lub [THEN Rdual] |
764 lemmas (in CLF) intv_CL_glb = intv_CL_lub [THEN Rdual] |
776 |
765 |
777 (*never proved, 2007-01-22*) |
766 (*never proved, 2007-01-22*) |
778 declare [[ sledgehammer_problem_prefix = "Tarski__interval_is_sublattice" ]] (*ALL THEOREMS*) |
767 |
779 lemma (in CLF) interval_is_sublattice: |
768 lemma (in CLF) interval_is_sublattice: |
780 "[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |] |
769 "[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |] |
781 ==> interval r a b <<= cl" |
770 ==> interval r a b <<= cl" |
782 (*sledgehammer *) |
771 (*sledgehammer *) |
783 apply (rule sublatticeI) |
772 apply (rule sublatticeI) |
784 apply (simp add: interval_subset) |
773 apply (simp add: interval_subset) |
785 (*never proved, 2007-01-22*) |
774 (*never proved, 2007-01-22*) |
786 using [[ sledgehammer_problem_prefix = "Tarski__interval_is_sublattice_simpler" ]] |
|
787 (*sledgehammer *) |
775 (*sledgehammer *) |
788 apply (rule CompleteLatticeI) |
776 apply (rule CompleteLatticeI) |
789 apply (simp add: intervalPO) |
777 apply (simp add: intervalPO) |
790 apply (simp add: intv_CL_lub) |
778 apply (simp add: intv_CL_lub) |
791 apply (simp add: intv_CL_glb) |
779 apply (simp add: intv_CL_glb) |
792 done |
780 done |
793 |
781 |
794 lemmas (in CLF) interv_is_compl_latt = |
782 lemmas (in CLF) interv_is_compl_latt = |
795 interval_is_sublattice [THEN sublattice_imp_CL] |
783 interval_is_sublattice [THEN sublattice_imp_CL] |
796 |
784 |
797 |
|
798 subsection {* Top and Bottom *} |
785 subsection {* Top and Bottom *} |
799 lemma (in CLF) Top_dual_Bot: "Top cl = Bot (dual cl)" |
786 lemma (in CLF) Top_dual_Bot: "Top cl = Bot (dual cl)" |
800 by (simp add: Top_def Bot_def least_def greatest_def dualA_iff dualr_iff) |
787 by (simp add: Top_def Bot_def least_def greatest_def dualA_iff dualr_iff) |
801 |
788 |
802 lemma (in CLF) Bot_dual_Top: "Bot cl = Top (dual cl)" |
789 lemma (in CLF) Bot_dual_Top: "Bot cl = Top (dual cl)" |
803 by (simp add: Top_def Bot_def least_def greatest_def dualA_iff dualr_iff) |
790 by (simp add: Top_def Bot_def least_def greatest_def dualA_iff dualr_iff) |
804 |
791 |
805 declare [[ sledgehammer_problem_prefix = "Tarski__Bot_in_lattice" ]] (*ALL THEOREMS*) |
792 |
806 lemma (in CLF) Bot_in_lattice: "Bot cl \<in> A" |
793 lemma (in CLF) Bot_in_lattice: "Bot cl \<in> A" |
807 (*sledgehammer; *) |
794 (*sledgehammer; *) |
808 apply (simp add: Bot_def least_def) |
795 apply (simp add: Bot_def least_def) |
809 apply (rule_tac a="glb A cl" in someI2) |
796 apply (rule_tac a="glb A cl" in someI2) |
810 apply (simp_all add: glb_in_lattice glb_lower |
797 apply (simp_all add: glb_in_lattice glb_lower |
811 r_def [symmetric] A_def [symmetric]) |
798 r_def [symmetric] A_def [symmetric]) |
812 done |
799 done |
813 |
800 |
814 (*first proved 2007-01-25 after relaxing relevance*) |
801 (*first proved 2007-01-25 after relaxing relevance*) |
815 declare [[ sledgehammer_problem_prefix = "Tarski__Top_in_lattice" ]] (*ALL THEOREMS*) |
802 |
816 lemma (in CLF) Top_in_lattice: "Top cl \<in> A" |
803 lemma (in CLF) Top_in_lattice: "Top cl \<in> A" |
817 (*sledgehammer;*) |
804 (*sledgehammer;*) |
818 apply (simp add: Top_dual_Bot A_def) |
805 apply (simp add: Top_dual_Bot A_def) |
819 (*first proved 2007-01-25 after relaxing relevance*) |
806 (*first proved 2007-01-25 after relaxing relevance*) |
820 using [[ sledgehammer_problem_prefix = "Tarski__Top_in_lattice_simpler" ]] (*ALL THEOREMS*) |
|
821 (*sledgehammer*) |
807 (*sledgehammer*) |
822 apply (rule dualA_iff [THEN subst]) |
808 apply (rule dualA_iff [THEN subst]) |
823 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) |
809 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) |
824 done |
810 done |
825 |
811 |
830 apply (simp_all add: lub_in_lattice lub_upper |
816 apply (simp_all add: lub_in_lattice lub_upper |
831 r_def [symmetric] A_def [symmetric]) |
817 r_def [symmetric] A_def [symmetric]) |
832 done |
818 done |
833 |
819 |
834 (*never proved, 2007-01-22*) |
820 (*never proved, 2007-01-22*) |
835 declare [[ sledgehammer_problem_prefix = "Tarski__Bot_prop" ]] (*ALL THEOREMS*) |
821 |
836 lemma (in CLF) Bot_prop: "x \<in> A ==> (Bot cl, x) \<in> r" |
822 lemma (in CLF) Bot_prop: "x \<in> A ==> (Bot cl, x) \<in> r" |
837 (*sledgehammer*) |
823 (*sledgehammer*) |
838 apply (simp add: Bot_dual_Top r_def) |
824 apply (simp add: Bot_dual_Top r_def) |
839 apply (rule dualr_iff [THEN subst]) |
825 apply (rule dualr_iff [THEN subst]) |
840 apply (simp add: CLF.Top_prop [of _ f, OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] |
826 apply (simp add: CLF.Top_prop [of _ f, OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] |
841 dualA_iff A_def dualPO CL_dualCL CLF_dual) |
827 dualA_iff A_def dualPO CL_dualCL CLF_dual) |
842 done |
828 done |
843 |
829 |
844 declare [[ sledgehammer_problem_prefix = "Tarski__Bot_in_lattice" ]] (*ALL THEOREMS*) |
830 |
845 lemma (in CLF) Top_intv_not_empty: "x \<in> A ==> interval r x (Top cl) \<noteq> {}" |
831 lemma (in CLF) Top_intv_not_empty: "x \<in> A ==> interval r x (Top cl) \<noteq> {}" |
846 apply (metis Top_in_lattice Top_prop empty_iff intervalI reflE) |
832 apply (metis Top_in_lattice Top_prop empty_iff intervalI reflE) |
847 done |
833 done |
848 |
834 |
849 declare [[ sledgehammer_problem_prefix = "Tarski__Bot_intv_not_empty" ]] (*ALL THEOREMS*) |
835 |
850 lemma (in CLF) Bot_intv_not_empty: "x \<in> A ==> interval r (Bot cl) x \<noteq> {}" |
836 lemma (in CLF) Bot_intv_not_empty: "x \<in> A ==> interval r (Bot cl) x \<noteq> {}" |
851 apply (metis Bot_prop ex_in_conv intervalI reflE rel_imp_elem) |
837 apply (metis Bot_prop ex_in_conv intervalI reflE rel_imp_elem) |
852 done |
838 done |
853 |
839 |
854 |
|
855 subsection {* fixed points form a partial order *} |
840 subsection {* fixed points form a partial order *} |
856 |
841 |
857 lemma (in CLF) fixf_po: "(| pset = P, order = induced P r|) \<in> PartialOrder" |
842 lemma (in CLF) fixf_po: "(| pset = P, order = induced P r|) \<in> PartialOrder" |
858 by (simp add: P_def fix_subset po_subset_po) |
843 by (simp add: P_def fix_subset po_subset_po) |
859 |
844 |
860 (*first proved 2007-01-25 after relaxing relevance*) |
845 (*first proved 2007-01-25 after relaxing relevance*) |
861 declare [[ sledgehammer_problem_prefix = "Tarski__Y_subset_A" ]] |
846 |
862 declare (in Tarski) P_def[simp] Y_ss [simp] |
847 declare (in Tarski) P_def[simp] Y_ss [simp] |
863 declare fix_subset [intro] subset_trans [intro] |
848 declare fix_subset [intro] subset_trans [intro] |
|
849 |
864 lemma (in Tarski) Y_subset_A: "Y \<subseteq> A" |
850 lemma (in Tarski) Y_subset_A: "Y \<subseteq> A" |
865 (*sledgehammer*) |
851 (*sledgehammer*) |
866 apply (rule subset_trans [OF _ fix_subset]) |
852 apply (rule subset_trans [OF _ fix_subset]) |
867 apply (rule Y_ss [simplified P_def]) |
853 apply (rule Y_ss [simplified P_def]) |
868 done |
854 done |
869 declare (in Tarski) P_def[simp del] Y_ss [simp del] |
855 |
870 declare fix_subset [rule del] subset_trans [rule del] |
856 declare (in Tarski) P_def[simp del] Y_ss [simp del] |
871 |
857 declare fix_subset [rule del] subset_trans [rule del] |
872 |
858 |
873 lemma (in Tarski) lubY_in_A: "lub Y cl \<in> A" |
859 lemma (in Tarski) lubY_in_A: "lub Y cl \<in> A" |
874 by (rule Y_subset_A [THEN lub_in_lattice]) |
860 by (rule Y_subset_A [THEN lub_in_lattice]) |
875 |
861 |
876 (*never proved, 2007-01-22*) |
862 (*never proved, 2007-01-22*) |
877 declare [[ sledgehammer_problem_prefix = "Tarski__lubY_le_flubY" ]] (*ALL THEOREMS*) |
863 |
878 lemma (in Tarski) lubY_le_flubY: "(lub Y cl, f (lub Y cl)) \<in> r" |
864 lemma (in Tarski) lubY_le_flubY: "(lub Y cl, f (lub Y cl)) \<in> r" |
879 (*sledgehammer*) |
865 (*sledgehammer*) |
880 apply (rule lub_least) |
866 apply (rule lub_least) |
881 apply (rule Y_subset_A) |
867 apply (rule Y_subset_A) |
882 apply (rule f_in_funcset [THEN funcset_mem]) |
868 apply (rule f_in_funcset [THEN funcset_mem]) |
883 apply (rule lubY_in_A) |
869 apply (rule lubY_in_A) |
884 -- {* @{text "Y \<subseteq> P ==> f x = x"} *} |
870 -- {* @{text "Y \<subseteq> P ==> f x = x"} *} |
885 apply (rule ballI) |
871 apply (rule ballI) |
886 using [[ sledgehammer_problem_prefix = "Tarski__lubY_le_flubY_simpler" ]] (*ALL THEOREMS*) |
|
887 (*sledgehammer *) |
872 (*sledgehammer *) |
888 apply (rule_tac t = "x" in fix_imp_eq [THEN subst]) |
873 apply (rule_tac t = "x" in fix_imp_eq [THEN subst]) |
889 apply (erule Y_ss [simplified P_def, THEN subsetD]) |
874 apply (erule Y_ss [simplified P_def, THEN subsetD]) |
890 -- {* @{text "reduce (f x, f (lub Y cl)) \<in> r to (x, lub Y cl) \<in> r"} by monotonicity *} |
875 -- {* @{text "reduce (f x, f (lub Y cl)) \<in> r to (x, lub Y cl) \<in> r"} by monotonicity *} |
891 using [[ sledgehammer_problem_prefix = "Tarski__lubY_le_flubY_simplest" ]] (*ALL THEOREMS*) |
|
892 (*sledgehammer*) |
876 (*sledgehammer*) |
893 apply (rule_tac f = "f" in monotoneE) |
877 apply (rule_tac f = "f" in monotoneE) |
894 apply (rule monotone_f) |
878 apply (rule monotone_f) |
895 apply (simp add: Y_subset_A [THEN subsetD]) |
879 apply (simp add: Y_subset_A [THEN subsetD]) |
896 apply (rule lubY_in_A) |
880 apply (rule lubY_in_A) |
897 apply (simp add: lub_upper Y_subset_A) |
881 apply (simp add: lub_upper Y_subset_A) |
898 done |
882 done |
899 |
883 |
900 (*first proved 2007-01-25 after relaxing relevance*) |
884 (*first proved 2007-01-25 after relaxing relevance*) |
901 declare [[ sledgehammer_problem_prefix = "Tarski__intY1_subset" ]] (*ALL THEOREMS*) |
885 |
902 lemma (in Tarski) intY1_subset: "intY1 \<subseteq> A" |
886 lemma (in Tarski) intY1_subset: "intY1 \<subseteq> A" |
903 (*sledgehammer*) |
887 (*sledgehammer*) |
904 apply (unfold intY1_def) |
888 apply (unfold intY1_def) |
905 apply (rule interval_subset) |
889 apply (rule interval_subset) |
906 apply (rule lubY_in_A) |
890 apply (rule lubY_in_A) |
908 done |
892 done |
909 |
893 |
910 lemmas (in Tarski) intY1_elem = intY1_subset [THEN subsetD] |
894 lemmas (in Tarski) intY1_elem = intY1_subset [THEN subsetD] |
911 |
895 |
912 (*never proved, 2007-01-22*) |
896 (*never proved, 2007-01-22*) |
913 declare [[ sledgehammer_problem_prefix = "Tarski__intY1_f_closed" ]] (*ALL THEOREMS*) |
897 |
914 lemma (in Tarski) intY1_f_closed: "x \<in> intY1 \<Longrightarrow> f x \<in> intY1" |
898 lemma (in Tarski) intY1_f_closed: "x \<in> intY1 \<Longrightarrow> f x \<in> intY1" |
915 (*sledgehammer*) |
899 (*sledgehammer*) |
916 apply (simp add: intY1_def interval_def) |
900 apply (simp add: intY1_def interval_def) |
917 apply (rule conjI) |
901 apply (rule conjI) |
918 apply (rule transE) |
902 apply (rule transE) |
919 apply (rule lubY_le_flubY) |
903 apply (rule lubY_le_flubY) |
920 -- {* @{text "(f (lub Y cl), f x) \<in> r"} *} |
904 -- {* @{text "(f (lub Y cl), f x) \<in> r"} *} |
921 using [[ sledgehammer_problem_prefix = "Tarski__intY1_f_closed_simpler" ]] (*ALL THEOREMS*) |
|
922 (*sledgehammer [has been proved before now...]*) |
905 (*sledgehammer [has been proved before now...]*) |
923 apply (rule_tac f=f in monotoneE) |
906 apply (rule_tac f=f in monotoneE) |
924 apply (rule monotone_f) |
907 apply (rule monotone_f) |
925 apply (rule lubY_in_A) |
908 apply (rule lubY_in_A) |
926 apply (simp add: intY1_def interval_def intY1_elem) |
909 apply (simp add: intY1_def interval_def intY1_elem) |
929 apply (rule Top_prop) |
912 apply (rule Top_prop) |
930 apply (rule f_in_funcset [THEN funcset_mem]) |
913 apply (rule f_in_funcset [THEN funcset_mem]) |
931 apply (simp add: intY1_def interval_def intY1_elem) |
914 apply (simp add: intY1_def interval_def intY1_elem) |
932 done |
915 done |
933 |
916 |
934 declare [[ sledgehammer_problem_prefix = "Tarski__intY1_func" ]] (*ALL THEOREMS*) |
917 |
935 lemma (in Tarski) intY1_func: "(%x: intY1. f x) \<in> intY1 -> intY1" |
918 lemma (in Tarski) intY1_func: "(%x: intY1. f x) \<in> intY1 -> intY1" |
936 apply (rule restrict_in_funcset) |
919 apply (rule restrict_in_funcset) |
937 apply (metis intY1_f_closed restrict_in_funcset) |
920 apply (metis intY1_f_closed restrict_in_funcset) |
938 done |
921 done |
939 |
922 |
940 declare [[ sledgehammer_problem_prefix = "Tarski__intY1_mono" ]] (*ALL THEOREMS*) |
923 |
941 lemma (in Tarski) intY1_mono: |
924 lemma (in Tarski) intY1_mono: |
942 "monotone (%x: intY1. f x) intY1 (induced intY1 r)" |
925 "monotone (%x: intY1. f x) intY1 (induced intY1 r)" |
943 (*sledgehammer *) |
926 (*sledgehammer *) |
944 apply (auto simp add: monotone_def induced_def intY1_f_closed) |
927 apply (auto simp add: monotone_def induced_def intY1_f_closed) |
945 apply (blast intro: intY1_elem monotone_f [THEN monotoneE]) |
928 apply (blast intro: intY1_elem monotone_f [THEN monotoneE]) |
946 done |
929 done |
947 |
930 |
948 (*proof requires relaxing relevance: 2007-01-25*) |
931 (*proof requires relaxing relevance: 2007-01-25*) |
949 declare [[ sledgehammer_problem_prefix = "Tarski__intY1_is_cl" ]] (*ALL THEOREMS*) |
932 |
950 lemma (in Tarski) intY1_is_cl: |
933 lemma (in Tarski) intY1_is_cl: |
951 "(| pset = intY1, order = induced intY1 r |) \<in> CompleteLattice" |
934 "(| pset = intY1, order = induced intY1 r |) \<in> CompleteLattice" |
952 (*sledgehammer*) |
935 (*sledgehammer*) |
953 apply (unfold intY1_def) |
936 apply (unfold intY1_def) |
954 apply (rule interv_is_compl_latt) |
937 apply (rule interv_is_compl_latt) |
957 apply (rule Top_intv_not_empty) |
940 apply (rule Top_intv_not_empty) |
958 apply (rule lubY_in_A) |
941 apply (rule lubY_in_A) |
959 done |
942 done |
960 |
943 |
961 (*never proved, 2007-01-22*) |
944 (*never proved, 2007-01-22*) |
962 declare [[ sledgehammer_problem_prefix = "Tarski__v_in_P" ]] (*ALL THEOREMS*) |
945 |
963 lemma (in Tarski) v_in_P: "v \<in> P" |
946 lemma (in Tarski) v_in_P: "v \<in> P" |
964 (*sledgehammer*) |
947 (*sledgehammer*) |
965 apply (unfold P_def) |
948 apply (unfold P_def) |
966 apply (rule_tac A = "intY1" in fixf_subset) |
949 apply (rule_tac A = "intY1" in fixf_subset) |
967 apply (rule intY1_subset) |
950 apply (rule intY1_subset) |
968 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] |
951 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] |
969 v_def CL_imp_PO intY1_is_cl CLF_set_def intY1_func intY1_mono) |
952 v_def CL_imp_PO intY1_is_cl CLF_set_def intY1_func intY1_mono) |
970 done |
953 done |
971 |
954 |
972 declare [[ sledgehammer_problem_prefix = "Tarski__z_in_interval" ]] (*ALL THEOREMS*) |
955 |
973 lemma (in Tarski) z_in_interval: |
956 lemma (in Tarski) z_in_interval: |
974 "[| z \<in> P; \<forall>y\<in>Y. (y, z) \<in> induced P r |] ==> z \<in> intY1" |
957 "[| z \<in> P; \<forall>y\<in>Y. (y, z) \<in> induced P r |] ==> z \<in> intY1" |
975 (*sledgehammer *) |
958 (*sledgehammer *) |
976 apply (unfold intY1_def P_def) |
959 apply (unfold intY1_def P_def) |
977 apply (rule intervalI) |
960 apply (rule intervalI) |
981 apply (rule Y_subset_A) |
964 apply (rule Y_subset_A) |
982 apply (fast elim!: fix_subset [THEN subsetD]) |
965 apply (fast elim!: fix_subset [THEN subsetD]) |
983 apply (simp add: induced_def) |
966 apply (simp add: induced_def) |
984 done |
967 done |
985 |
968 |
986 declare [[ sledgehammer_problem_prefix = "Tarski__fz_in_int_rel" ]] (*ALL THEOREMS*) |
969 |
987 lemma (in Tarski) f'z_in_int_rel: "[| z \<in> P; \<forall>y\<in>Y. (y, z) \<in> induced P r |] |
970 lemma (in Tarski) f'z_in_int_rel: "[| z \<in> P; \<forall>y\<in>Y. (y, z) \<in> induced P r |] |
988 ==> ((%x: intY1. f x) z, z) \<in> induced intY1 r" |
971 ==> ((%x: intY1. f x) z, z) \<in> induced intY1 r" |
989 apply (metis P_def acc_def fix_imp_eq fix_subset indI reflE restrict_apply subset_eq z_in_interval) |
972 apply (metis P_def acc_def fix_imp_eq fix_subset indI reflE restrict_apply subset_eq z_in_interval) |
990 done |
973 done |
991 |
974 |
992 (*never proved, 2007-01-22*) |
975 (*never proved, 2007-01-22*) |
993 declare [[ sledgehammer_problem_prefix = "Tarski__tarski_full_lemma" ]] (*ALL THEOREMS*) |
976 |
994 lemma (in Tarski) tarski_full_lemma: |
977 lemma (in Tarski) tarski_full_lemma: |
995 "\<exists>L. isLub Y (| pset = P, order = induced P r |) L" |
978 "\<exists>L. isLub Y (| pset = P, order = induced P r |) L" |
996 apply (rule_tac x = "v" in exI) |
979 apply (rule_tac x = "v" in exI) |
997 apply (simp add: isLub_def) |
980 apply (simp add: isLub_def) |
998 -- {* @{text "v \<in> P"} *} |
981 -- {* @{text "v \<in> P"} *} |
1018 apply (rule indI) |
1001 apply (rule indI) |
1019 prefer 3 apply assumption |
1002 prefer 3 apply assumption |
1020 prefer 2 apply (simp add: v_in_P) |
1003 prefer 2 apply (simp add: v_in_P) |
1021 apply (unfold v_def) |
1004 apply (unfold v_def) |
1022 (*never proved, 2007-01-22*) |
1005 (*never proved, 2007-01-22*) |
1023 using [[ sledgehammer_problem_prefix = "Tarski__tarski_full_lemma_simpler" ]] |
|
1024 (*sledgehammer*) |
1006 (*sledgehammer*) |
1025 apply (rule indE) |
1007 apply (rule indE) |
1026 apply (rule_tac [2] intY1_subset) |
1008 apply (rule_tac [2] intY1_subset) |
1027 (*never proved, 2007-01-22*) |
1009 (*never proved, 2007-01-22*) |
1028 using [[ sledgehammer_problem_prefix = "Tarski__tarski_full_lemma_simplest" ]] |
|
1029 (*sledgehammer*) |
1010 (*sledgehammer*) |
1030 apply (rule CL.glb_lower [OF CL.intro, OF PO.intro CL_axioms.intro, OF _ intY1_is_cl, simplified]) |
1011 apply (rule CL.glb_lower [OF CL.intro, OF PO.intro CL_axioms.intro, OF _ intY1_is_cl, simplified]) |
1031 apply (simp add: CL_imp_PO intY1_is_cl) |
1012 apply (simp add: CL_imp_PO intY1_is_cl) |
1032 apply force |
1013 apply force |
1033 apply (simp add: induced_def intY1_f_closed z_in_interval) |
1014 apply (simp add: induced_def intY1_f_closed z_in_interval) |
1039 "[| (| pset = A, order = r |) \<in> PartialOrder; |
1020 "[| (| pset = A, order = r |) \<in> PartialOrder; |
1040 \<forall>S. S \<subseteq> A --> (\<exists>L. isLub S (| pset = A, order = r |) L) |] |
1021 \<forall>S. S \<subseteq> A --> (\<exists>L. isLub S (| pset = A, order = r |) L) |] |
1041 ==> (| pset = A, order = r |) \<in> CompleteLattice" |
1022 ==> (| pset = A, order = r |) \<in> CompleteLattice" |
1042 by (simp add: CompleteLatticeI Rdual) |
1023 by (simp add: CompleteLatticeI Rdual) |
1043 |
1024 |
1044 |
1025 (*never proved, 2007-01-22*) |
1045 (*never proved, 2007-01-22*) |
1026 |
1046 declare [[ sledgehammer_problem_prefix = "Tarski__Tarski_full" ]] |
1027 declare (in CLF) fixf_po[intro] P_def [simp] A_def [simp] r_def [simp] |
1047 declare (in CLF) fixf_po[intro] P_def [simp] A_def [simp] r_def [simp] |
1028 Tarski.tarski_full_lemma [intro] cl_po [intro] cl_co [intro] |
1048 Tarski.tarski_full_lemma [intro] cl_po [intro] cl_co [intro] |
1029 CompleteLatticeI_simp [intro] |
1049 CompleteLatticeI_simp [intro] |
1030 |
1050 theorem (in CLF) Tarski_full: |
1031 theorem (in CLF) Tarski_full: |
1051 "(| pset = P, order = induced P r|) \<in> CompleteLattice" |
1032 "(| pset = P, order = induced P r|) \<in> CompleteLattice" |
1052 (*sledgehammer*) |
1033 (*sledgehammer*) |
1053 apply (rule CompleteLatticeI_simp) |
1034 apply (rule CompleteLatticeI_simp) |
1054 apply (rule fixf_po, clarify) |
1035 apply (rule fixf_po, clarify) |
1055 (*never proved, 2007-01-22*) |
1036 (*never proved, 2007-01-22*) |
1056 using [[ sledgehammer_problem_prefix = "Tarski__Tarski_full_simpler" ]] |
|
1057 (*sledgehammer*) |
1037 (*sledgehammer*) |
1058 apply (simp add: P_def A_def r_def) |
1038 apply (simp add: P_def A_def r_def) |
1059 apply (blast intro!: Tarski.tarski_full_lemma [OF Tarski.intro, OF CLF.intro Tarski_axioms.intro, |
1039 apply (blast intro!: Tarski.tarski_full_lemma [OF Tarski.intro, OF CLF.intro Tarski_axioms.intro, |
1060 OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] cl_po cl_co f_cl) |
1040 OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] cl_po cl_co f_cl) |
1061 done |
1041 done |