section ‹Chain-Complete Partial Orders› theory CCPO_Extensions imports "HOL-Library.Complete_Partial_Order2" ENat_Extensions Set_Extensions begin lemma chain_split[dest]: assumes "Complete_Partial_Order.chain ord C" "x ∈ C" shows "C = {y ∈ C. ord x y} ∪ {y ∈ C. ord y x}" proof - have 1: "⋀ y. y ∈ C ⟹ ord x y ∨ ord y x" using chainD assms by this show ?thesis using 1 by blast qed lemma infinite_chain_below[dest]: assumes "Complete_Partial_Order.chain ord C" "infinite C" "x ∈ C" assumes "finite {y ∈ C. ord x y}" shows "infinite {y ∈ C. ord y x}" proof - have 1: "C = {y ∈ C. ord x y} ∪ {y ∈ C. ord y x}" using assms(1, 3) by rule show ?thesis using finite_Un assms(2, 4) 1 by (metis (poly_guards_query)) qed lemma infinite_chain_above[dest]: assumes "Complete_Partial_Order.chain ord C" "infinite C" "x ∈ C" assumes "finite {y ∈ C. ord y x}" shows "infinite {y ∈ C. ord x y}" proof - have 1: "C = {y ∈ C. ord x y} ∪ {y ∈ C. ord y x}" using assms(1, 3) by rule show ?thesis using finite_Un assms(2, 4) 1 by (metis (poly_guards_query)) qed lemma (in ccpo) ccpo_Sup_upper_inv: assumes "Complete_Partial_Order.chain less_eq C" "x > ⨆ C" shows "x ∉ C" using assms ccpo_Sup_upper by fastforce lemma (in ccpo) ccpo_Sup_least_inv: assumes "Complete_Partial_Order.chain less_eq C" "⨆ C > x" obtains y where "y ∈ C" "¬ y ≤ x" using assms ccpo_Sup_least that by fastforce lemma ccpo_Sup_least_inv': fixes C :: "'a :: {ccpo, linorder} set" assumes "Complete_Partial_Order.chain less_eq C" "⨆ C > x" obtains y where "y ∈ C" "y > x" proof - obtain y where 1: "y ∈ C" "¬ y ≤ x" using ccpo_Sup_least_inv assms by this show ?thesis using that 1 by simp qed lemma mcont2mcont_lessThan[THEN lfp.mcont2mcont, simp, cont_intro]: shows mcont_lessThan: "mcont Sup less_eq Sup less_eq (lessThan :: 'a :: {ccpo, linorder} ⇒ 'a set)" proof show "monotone less_eq less_eq (lessThan :: 'a ⇒ 'a set)" by (rule, auto) show "cont Sup less_eq Sup less_eq (lessThan :: 'a ⇒ 'a set)" proof fix C :: "'a set" assume 1: "Complete_Partial_Order.chain less_eq C" show "{..< ⨆ C} = ⋃ (lessThan ` C)" proof (intro equalityI subsetI) fix A assume 2: "A ∈ {..< ⨆ C}" obtain B where 3: "B ∈ C" "B > A" using ccpo_Sup_least_inv' 1 2 by blast show "A ∈ ⋃ (lessThan ` C)" using 3 by auto next fix A assume 2: "A ∈ ⋃ (lessThan ` C)" show "A ∈ {..< ⨆ C}" using ccpo_Sup_upper 2 by force qed qed qed class esize = fixes esize :: "'a ⇒ enat" class esize_order = esize + order + assumes esize_finite[dest]: "esize x ≠ ∞ ⟹ finite {y. y ≤ x}" assumes esize_mono[intro]: "x ≤ y ⟹ esize x ≤ esize y" assumes esize_strict_mono[intro]: "esize x ≠ ∞ ⟹ x < y ⟹ esize x < esize y" begin lemma infinite_chain_eSuc_esize[dest]: assumes "Complete_Partial_Order.chain less_eq C" "infinite C" "x ∈ C" obtains y where "y ∈ C" "esize y ≥ eSuc (esize x)" proof (cases "esize x") case (enat k) have 1: "finite {y ∈ C. y ≤ x}" using esize_finite enat by simp have 2: "infinite {y ∈ C. y ≥ x}" using assms 1 by rule have 3: "{y ∈ C. y > x} = {y ∈ C. y ≥ x} - {x}" by auto have 4: "infinite {y ∈ C. y > x}" using 2 unfolding 3 by simp obtain y where 5: "y ∈ C" "y > x" using 4 by auto have 6: "esize y > esize x" using esize_strict_mono enat 5(2) by blast show ?thesis using that 5(1) 6 ileI1 by simp next case (infinity) show ?thesis using that infinity assms(3) by simp qed lemma infinite_chain_arbitrary_esize[dest]: assumes "Complete_Partial_Order.chain less_eq C" "infinite C" obtains x where "x ∈ C" "esize x ≥ enat n" proof (induct n arbitrary: thesis) case 0 show ?case using assms(2) 0 by force next case (Suc n) obtain x where 1: "x ∈ C" "esize x ≥ enat n" using Suc(1) by blast obtain y where 2: "y ∈ C" "esize y ≥ eSuc (esize x)" using assms 1(1) by rule show ?case using gfp.leq_trans Suc(2) 1(2) 2 by fastforce qed end class esize_ccpo = esize_order + ccpo begin lemma esize_cont[dest]: assumes "Complete_Partial_Order.chain less_eq C" "C ≠ {}" shows "esize (⨆ C) = ⨆ (esize ` C)" proof (cases "finite C") case False have 1: "esize (⨆ C) = ∞" proof fix n obtain A where 1: "A ∈ C" "esize A ≥ enat n" using assms(1) False by rule have 2: "A ≤ ⨆ C" using ccpo_Sup_upper assms(1) 1(1) by this have "enat n ≤ esize A" using 1(2) by this also have "… ≤ esize (⨆ C)" using 2 by rule finally show "enat n ≤ esize (⨆ C)" by this qed have 2: "(⨆ A ∈ C. esize A) = ∞" proof fix n obtain A where 1: "A ∈ C" "esize A ≥ enat n" using assms(1) False by rule show "enat n ≤ (⨆ A ∈ C. esize A)" using SUP_upper2 1 by this qed show ?thesis using 1 2 by simp next case True have 1: "esize (⨆ C) = (⨆ x ∈ C. esize x)" proof (intro order_class.order.antisym SUP_upper SUP_least esize_mono) show "⨆ C ∈ C" using in_chain_finite assms(1) True assms(2) by this show "⋀ x. x ∈ C ⟹ x ≤ ⨆ C" using ccpo_Sup_upper assms(1) by this qed show ?thesis using 1 by simp qed lemma esize_mcont: "mcont Sup less_eq Sup less_eq esize" by (blast intro: mcontI monotoneI contI) lemmas mcont2mcont_esize = esize_mcont[THEN lfp.mcont2mcont, simp, cont_intro] end end