59 |
59 |
60 Top :: "'a potype => 'a" |
60 Top :: "'a potype => 'a" |
61 "Top po == greatest (%x. True) po" |
61 "Top po == greatest (%x. True) po" |
62 |
62 |
63 PartialOrder :: "('a potype) set" |
63 PartialOrder :: "('a potype) set" |
64 "PartialOrder == {P. refl (pset P) (order P) & antisym (order P) & |
64 "PartialOrder == {P. refl_on (pset P) (order P) & antisym (order P) & |
65 trans (order P)}" |
65 trans (order P)}" |
66 |
66 |
67 CompleteLattice :: "('a potype) set" |
67 CompleteLattice :: "('a potype) set" |
68 "CompleteLattice == {cl. cl: PartialOrder & |
68 "CompleteLattice == {cl. cl: PartialOrder & |
69 (\<forall>S. S \<subseteq> pset cl --> (\<exists>L. isLub S cl L)) & |
69 (\<forall>S. S \<subseteq> pset cl --> (\<exists>L. isLub S cl L)) & |
124 (| pset=intY1, order=induced intY1 r|)" |
124 (| pset=intY1, order=induced intY1 r|)" |
125 |
125 |
126 |
126 |
127 subsection {* Partial Order *} |
127 subsection {* Partial Order *} |
128 |
128 |
129 lemma (in PO) PO_imp_refl: "refl A r" |
129 lemma (in PO) PO_imp_refl_on: "refl_on A r" |
130 apply (insert cl_po) |
130 apply (insert cl_po) |
131 apply (simp add: PartialOrder_def A_def r_def) |
131 apply (simp add: PartialOrder_def A_def r_def) |
132 done |
132 done |
133 |
133 |
134 lemma (in PO) PO_imp_sym: "antisym r" |
134 lemma (in PO) PO_imp_sym: "antisym r" |
141 apply (simp add: PartialOrder_def r_def) |
141 apply (simp add: PartialOrder_def r_def) |
142 done |
142 done |
143 |
143 |
144 lemma (in PO) reflE: "x \<in> A ==> (x, x) \<in> r" |
144 lemma (in PO) reflE: "x \<in> A ==> (x, x) \<in> r" |
145 apply (insert cl_po) |
145 apply (insert cl_po) |
146 apply (simp add: PartialOrder_def refl_def A_def r_def) |
146 apply (simp add: PartialOrder_def refl_on_def A_def r_def) |
147 done |
147 done |
148 |
148 |
149 lemma (in PO) antisymE: "[| (a, b) \<in> r; (b, a) \<in> r |] ==> a = b" |
149 lemma (in PO) antisymE: "[| (a, b) \<in> r; (b, a) \<in> r |] ==> a = b" |
150 apply (insert cl_po) |
150 apply (insert cl_po) |
151 apply (simp add: PartialOrder_def antisym_def r_def) |
151 apply (simp add: PartialOrder_def antisym_def r_def) |
164 lemma (in PO) po_subset_po: |
164 lemma (in PO) po_subset_po: |
165 "S \<subseteq> A ==> (| pset = S, order = induced S r |) \<in> PartialOrder" |
165 "S \<subseteq> A ==> (| pset = S, order = induced S r |) \<in> PartialOrder" |
166 apply (simp (no_asm) add: PartialOrder_def) |
166 apply (simp (no_asm) add: PartialOrder_def) |
167 apply auto |
167 apply auto |
168 -- {* refl *} |
168 -- {* refl *} |
169 apply (simp add: refl_def induced_def) |
169 apply (simp add: refl_on_def induced_def) |
170 apply (blast intro: reflE) |
170 apply (blast intro: reflE) |
171 -- {* antisym *} |
171 -- {* antisym *} |
172 apply (simp add: antisym_def induced_def) |
172 apply (simp add: antisym_def induced_def) |
173 apply (blast intro: antisymE) |
173 apply (blast intro: antisymE) |
174 -- {* trans *} |
174 -- {* trans *} |
201 lemma isLub_dual_isGlb: "isLub S cl = isGlb S (dual cl)" |
201 lemma isLub_dual_isGlb: "isLub S cl = isGlb S (dual cl)" |
202 by (simp add: isLub_def isGlb_def dual_def converse_def) |
202 by (simp add: isLub_def isGlb_def dual_def converse_def) |
203 |
203 |
204 lemma (in PO) dualPO: "dual cl \<in> PartialOrder" |
204 lemma (in PO) dualPO: "dual cl \<in> PartialOrder" |
205 apply (insert cl_po) |
205 apply (insert cl_po) |
206 apply (simp add: PartialOrder_def dual_def refl_converse |
206 apply (simp add: PartialOrder_def dual_def refl_on_converse |
207 trans_converse antisym_converse) |
207 trans_converse antisym_converse) |
208 done |
208 done |
209 |
209 |
210 lemma Rdual: |
210 lemma Rdual: |
211 "\<forall>S. (S \<subseteq> A -->( \<exists>L. isLub S (| pset = A, order = r|) L)) |
211 "\<forall>S. (S \<subseteq> A -->( \<exists>L. isLub S (| pset = A, order = r|) L)) |
228 lemma CL_subset_PO: "CompleteLattice \<subseteq> PartialOrder" |
228 lemma CL_subset_PO: "CompleteLattice \<subseteq> PartialOrder" |
229 by (simp add: PartialOrder_def CompleteLattice_def, fast) |
229 by (simp add: PartialOrder_def CompleteLattice_def, fast) |
230 |
230 |
231 lemmas CL_imp_PO = CL_subset_PO [THEN subsetD] |
231 lemmas CL_imp_PO = CL_subset_PO [THEN subsetD] |
232 |
232 |
233 declare PO.PO_imp_refl [OF PO.intro [OF CL_imp_PO], simp] |
233 declare PO.PO_imp_refl_on [OF PO.intro [OF CL_imp_PO], simp] |
234 declare PO.PO_imp_sym [OF PO.intro [OF CL_imp_PO], simp] |
234 declare PO.PO_imp_sym [OF PO.intro [OF CL_imp_PO], simp] |
235 declare PO.PO_imp_trans [OF PO.intro [OF CL_imp_PO], simp] |
235 declare PO.PO_imp_trans [OF PO.intro [OF CL_imp_PO], simp] |
236 |
236 |
237 lemma (in CL) CO_refl: "refl A r" |
237 lemma (in CL) CO_refl_on: "refl_on A r" |
238 by (rule PO_imp_refl) |
238 by (rule PO_imp_refl_on) |
239 |
239 |
240 lemma (in CL) CO_antisym: "antisym r" |
240 lemma (in CL) CO_antisym: "antisym r" |
241 by (rule PO_imp_sym) |
241 by (rule PO_imp_sym) |
242 |
242 |
243 lemma (in CL) CO_trans: "trans r" |
243 lemma (in CL) CO_trans: "trans r" |
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 ML_command{*AtpWrapper.problem_name:="Tarski__CLF_flubH_le_lubH_simpler"*} |
503 (*??no longer terminates, with combinators |
503 (*??no longer terminates, with combinators |
504 apply (metis CO_refl 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 lubH_le_flubH monotoneE [OF monotone_f] reflD1 reflD2) |
506 apply (metis CO_refl_on lubH_le_flubH monotoneE [OF monotone_f] refl_onD1 refl_onD2) |
507 apply (metis CO_refl lubH_le_flubH reflD2) |
507 apply (metis CO_refl_on lubH_le_flubH refl_onD2) |
508 done |
508 done |
509 declare CLF.f_in_funcset[rule del] funcset_mem[rule del] |
509 declare CLF.f_in_funcset[rule del] funcset_mem[rule del] |
510 CL.lub_in_lattice[rule del] PO.monotoneE[rule del] |
510 CL.lub_in_lattice[rule del] PO.monotoneE[rule del] |
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] |
540 by (metis antisymE 4) |
540 by (metis antisymE 4) |
541 have 6: "lub H cl = f (lub H cl)" |
541 have 6: "lub H cl = f (lub H cl)" |
542 by (metis 5 3) |
542 by (metis 5 3) |
543 have 7: "(lub H cl, lub H cl) \<in> r" |
543 have 7: "(lub H cl, lub H cl) \<in> r" |
544 by (metis 6 4) |
544 by (metis 6 4) |
545 have 8: "\<And>X1. lub H cl \<in> X1 \<or> \<not> refl X1 r" |
545 have 8: "\<And>X1. lub H cl \<in> X1 \<or> \<not> refl_on X1 r" |
546 by (metis 7 reflD2) |
546 by (metis 7 refl_onD2) |
547 have 9: "\<not> refl A r" |
547 have 9: "\<not> refl_on A r" |
548 by (metis 8 2) |
548 by (metis 8 2) |
549 show "False" |
549 show "False" |
550 by (metis CO_refl 9); |
550 by (metis CO_refl_on 9); |
551 next --{*apparently the way to insert a second structured proof*} |
551 next --{*apparently the way to insert a second structured proof*} |
552 show "H = {x. (x, f x) \<in> r \<and> x \<in> A} \<Longrightarrow> |
552 show "H = {x. (x, f x) \<in> r \<and> x \<in> A} \<Longrightarrow> |
553 f (lub {x. (x, f x) \<in> r \<and> x \<in> A} cl) = lub {x. (x, f x) \<in> r \<and> x \<in> A} cl" |
553 f (lub {x. (x, f x) \<in> r \<and> x \<in> A} cl) = lub {x. (x, f x) \<in> r \<and> x \<in> A} cl" |
554 proof (neg_clausify) |
554 proof (neg_clausify) |
555 assume 0: "H = |
555 assume 0: "H = |
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 ML_command{*AtpWrapper.problem_name:="Tarski__CLF_lubH_is_fixp_simpler"*} |
592 apply (metis CO_refl lubH_le_flubH reflD1) |
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: |
597 "[| H = {x. (x, f x) \<in> r & x \<in> A}; x \<in> P |] ==> x \<in> H" |
597 "[| H = {x. (x, f x) \<in> r & x \<in> A}; x \<in> P |] ==> x \<in> H" |
598 by (simp add: P_def fix_imp_eq [of _ f A] reflE CO_refl |
598 by (simp add: P_def fix_imp_eq [of _ f A] reflE CO_refl_on |
599 fix_subset [of f A, THEN subsetD]) |
599 fix_subset [of f A, THEN subsetD]) |
600 |
600 |
601 |
601 |
602 lemma (in CLF) fixf_le_lubH: |
602 lemma (in CLF) fixf_le_lubH: |
603 "H = {x. (x, f x) \<in> r & x \<in> A} ==> \<forall>x \<in> fix f A. (x, lub H cl) \<in> r" |
603 "H = {x. (x, f x) \<in> r & x \<in> A} ==> \<forall>x \<in> fix f A. (x, lub H cl) \<in> r" |
676 |
676 |
677 subsection {* interval *} |
677 subsection {* interval *} |
678 |
678 |
679 |
679 |
680 ML{*AtpWrapper.problem_name:="Tarski__rel_imp_elem"*} |
680 ML{*AtpWrapper.problem_name:="Tarski__rel_imp_elem"*} |
681 declare (in CLF) CO_refl[simp] refl_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 reflD1) |
683 by (metis CO_refl_on refl_onD1) |
684 declare (in CLF) CO_refl[simp del] refl_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 ML{*AtpWrapper.problem_name:="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 interval_imp_mem reflD reflD2 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] |
692 declare interval_def [simp del] |
692 declare interval_def [simp del] |
693 |
693 |
694 |
694 |
695 lemma (in CLF) intervalI: |
695 lemma (in CLF) intervalI: |