Skip to content

Commit d3a4c90

Browse files
simondfostersimondfoster
committed
Added the complete lattice for scene spaces
1 parent c50fb0e commit d3a4c90

2 files changed

Lines changed: 242 additions & 1 deletion

File tree

‎Scene_Spaces.thy‎

Lines changed: 239 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
section \<open> Scene Spaces \<close>
22

33
theory Scene_Spaces
4-
imports Scenes
4+
imports "HOL-Algebra.Complete_Lattice" Scenes
55
begin
66

77
subsection \<open> Preliminaries \<close>
@@ -376,6 +376,9 @@ lemma scene_space_uminus: "\<lbrakk> a \<in> scene_space \<rbrakk> \<Longrightar
376376
by (auto simp add: scene_space_vars_decomp_iff uminus_vars_other_vars)
377377
(metis filter_is_subset)
378378

379+
lemma uminus_image_scene_space: "uminus ` scene_space = scene_space"
380+
by (metis (mono_tags, opaque_lifting) Set.set_eqI image_subset_iff scene_space_uminus subset_eq uminus_scene_twice)
381+
379382
lemma scene_space_inter: "\<lbrakk> a \<in> scene_space; b \<in> scene_space \<rbrakk> \<Longrightarrow> a \<sqinter>\<^sub>S b \<in> scene_space"
380383
by (simp add: inf_scene_def scene_space.union_scene_space scene_space_uminus)
381384

@@ -746,6 +749,241 @@ qed
746749

747750
end
748751

752+
subsection \<open> Complete lattice of scenes \<close>
753+
754+
definition Sup_scene :: "'a::scene_space scene set \<Rightarrow> 'a scene" where
755+
"Sup_scene A = \<Squnion>\<^sub>S (SOME xs. set xs = (A \<inter> scene_space))"
756+
757+
lemma Sup_scene_is_foldr_scene:
758+
assumes "set xs \<subseteq> scene_space"
759+
shows "Sup_scene (set xs) = \<Squnion>\<^sub>S xs"
760+
proof -
761+
have "set (SOME ys. set ys = set xs) = set xs"
762+
by (rule someI[where x="xs"], simp)
763+
thus ?thesis
764+
by (metis Sup_scene_def assms foldr_scene_union_eq_scene_space inf.absorb_iff1)
765+
qed
766+
767+
lemma Sup_scene_closed: "Sup_scene A \<in> scene_space"
768+
unfolding Sup_scene_def proof -
769+
fix A :: "'a scene set"
770+
obtain xs where A: "A \<inter> scene_space = set xs"
771+
by (metis finite_Int finite_list finite_scene_space)
772+
hence "\<Squnion>\<^sub>S xs \<in> scene_space"
773+
using scene_space_foldr by auto
774+
moreover have "\<Squnion>\<^sub>S (SOME xs. set xs = A \<inter> scene_space) = \<Squnion>\<^sub>S xs"
775+
by (metis (mono_tags, lifting) A Int_iff foldr_scene_union_eq_scene_space someI subsetI)
776+
ultimately show "\<Squnion>\<^sub>S (SOME xs. set xs = A \<inter> scene_space) \<in> scene_space"
777+
by simp
778+
qed
779+
780+
notation Sup_scene ("\<Union>\<^sub>S")
781+
782+
lemma Sup_scene_bot [simp]: "\<Union>\<^sub>S {} = bot"
783+
by (simp add: Sup_scene_def)
784+
785+
definition Inf_scene :: "'a::scene_space scene set \<Rightarrow> 'a scene" where
786+
"Inf_scene A = - (Sup_scene (uminus ` A))"
787+
788+
notation Inf_scene ("\<Inter>\<^sub>S")
789+
790+
lemma Inf_scene_top: "\<Inter>\<^sub>S {} = top_class.top"
791+
by (simp add: Inf_scene_def)
792+
793+
lemma uminus_scene_Inf: "- \<Inter>\<^sub>S A = \<Union>\<^sub>S (uminus ` A)"
794+
by (simp add: Inf_scene_def uminus_scene_twice)
795+
796+
lemma uminus_scene_Sup: "- \<Union>\<^sub>S A = \<Inter>\<^sub>S (uminus ` A)"
797+
by (metis (no_types, lifting) ext image_ident image_image uminus_scene_Inf uminus_scene_twice)
798+
799+
definition scene_gorder :: "'a::scene_space scene gorder" where
800+
"scene_gorder = \<lparr> carrier = scene_space, eq = (=), le = (\<le>) \<rparr>"
801+
802+
lemma carrier_scene_gorder [simp]: "carrier scene_gorder = scene_space"
803+
by (simp add: scene_gorder_def)
804+
805+
lemma eq_scene_gorder [simp]: "eq scene_gorder = (=)"
806+
by (simp add: scene_gorder_def)
807+
808+
lemma le_scene_gorder [simp]: "le scene_gorder = (\<subseteq>\<^sub>S)"
809+
by (simp add: scene_gorder_def)
810+
811+
lemma Sup_scene_props:
812+
assumes "A \<subseteq> scene_space"
813+
shows le_Sup_scene: "x \<in> A \<Longrightarrow> x \<subseteq>\<^sub>S \<Union>\<^sub>S A"
814+
and Sup_scene_le: "\<lbrakk> z \<in> scene_space; \<And>x. x \<in> A \<Longrightarrow> x \<subseteq>\<^sub>S z \<rbrakk> \<Longrightarrow> \<Union>\<^sub>S A \<subseteq>\<^sub>S z"
815+
proof -
816+
obtain xs where xs: "A = set xs"
817+
by (metis assms(1) finite_list finite_scene_space rev_finite_subset)
818+
have xs_ss: "set xs \<subseteq> scene_space"
819+
using assms(1) xs by auto
820+
show 1: "x \<in> A \<Longrightarrow> x \<le> \<Union>\<^sub>S A"
821+
by (simp add: Sup_scene_is_foldr_scene scene_space_in_foldr xs xs_ss)
822+
show 2: "\<lbrakk> z \<in> scene_space; \<And>x. x \<in> A \<Longrightarrow> x \<le> z \<rbrakk> \<Longrightarrow> \<Union>\<^sub>S A \<le> z"
823+
by (simp add: Upper_def Sup_scene_is_foldr_scene xs xs_ss)
824+
(meson scene_space_foldr_lb subset_iff xs_ss)
825+
qed
826+
827+
lemma Sup_scene_lub: "A \<subseteq> scene_space \<Longrightarrow> is_lub scene_gorder (\<Union>\<^sub>S A) A"
828+
by (rule_tac least_UpperI)
829+
(auto simp add: Upper_def intro!: Sup_scene_props Sup_scene_closed)
830+
831+
definition ss_union :: "'a::scene_space scene \<Rightarrow> 'a scene \<Rightarrow> 'a scene" (infixl \<open>\<union>\<^sub>S\<close> 65) where
832+
"ss_union x y = Sup_scene {x, y}"
833+
834+
lemma sup_scene_union:
835+
assumes "x \<in> scene_space" "y \<in> scene_space"
836+
shows "x \<union>\<^sub>S y = x \<squnion>\<^sub>S y"
837+
proof -
838+
have "x \<union>\<^sub>S y = \<Squnion>\<^sub>S [x, y]"
839+
by (metis ss_union_def Sup_scene_is_foldr_scene assms(1,2) bot.extremum insert_subset list.set(1) list.simps(15))
840+
thus ?thesis
841+
by simp
842+
qed
843+
844+
lemma Inf_scene_glb:
845+
assumes "A \<subseteq> scene_space"
846+
shows "is_glb scene_gorder (\<Inter>\<^sub>S A) A"
847+
proof (rule greatest_LowerI, simp_all add: Lower_def assms)
848+
fix x :: \<open>'a scene\<close>
849+
assume xA: \<open>x \<in> A\<close>
850+
have "\<Inter>\<^sub>S A \<le> x \<longleftrightarrow> (- \<Union>\<^sub>S (uminus ` A) \<le> x)"
851+
by (simp add: Inf_scene_def)
852+
also have "... \<longleftrightarrow> (- x \<le> \<Union>\<^sub>S (uminus ` A))"
853+
using scene_indep_sym scene_le_iff_indep_inv by blast
854+
also have "..."
855+
by (metis assms image_eqI image_subset_iff in_mono le_Sup_scene scene_space_uminus xA)
856+
finally show "\<Inter>\<^sub>S A \<le> x" .
857+
next
858+
fix y
859+
assume a:"(\<forall>x. x \<in> A \<and> x \<in> scene_space \<longrightarrow> y \<subseteq>\<^sub>S x) \<and> y \<in> scene_space"
860+
have "y \<le> \<Inter>\<^sub>S A \<longleftrightarrow> \<Union>\<^sub>S (uminus ` A) \<le> - y"
861+
by (metis Inf_scene_def scene_indep_sym scene_le_iff_indep_inv uminus_scene_twice)
862+
also from assms a have "..."
863+
using scene_space_uminus scene_compl_subset_iff
864+
by (force intro!: Sup_scene_le)
865+
finally show "y \<subseteq>\<^sub>S \<Inter>\<^sub>S A"
866+
by blast
867+
next
868+
show "\<Inter>\<^sub>S A \<in> scene_space"
869+
by (metis Inf_scene_def Sup_scene_closed scene_space_uminus)
870+
qed
871+
872+
lemma scene_space_complete_lattice: "complete_lattice scene_gorder"
873+
proof (unfold_locales, simp_all add: scene_gorder_def)
874+
fix x :: \<open>'a scene\<close>
875+
assume \<open>x \<in> scene_space\<close>
876+
show \<open>x \<subseteq>\<^sub>S x\<close>
877+
by (simp add: subscene_refl)
878+
next
879+
fix x :: \<open>'a scene\<close> and y :: \<open>'a scene\<close>
880+
assume
881+
\<open>x \<subseteq>\<^sub>S y\<close> and
882+
\<open>y \<subseteq>\<^sub>S x\<close> and
883+
\<open>x \<in> scene_space\<close> and
884+
\<open>y \<in> scene_space\<close>
885+
thus \<open>x = y\<close>
886+
using idem_scene_space subscene_antisym by auto
887+
next
888+
fix x :: \<open>'a scene\<close> and y :: \<open>'a scene\<close> and z :: \<open>'a scene\<close>
889+
assume
890+
\<open>x \<subseteq>\<^sub>S y\<close> and
891+
\<open>y \<subseteq>\<^sub>S z\<close> and
892+
\<open>x \<in> scene_space\<close> and
893+
\<open>y \<in> scene_space\<close> and
894+
\<open>z \<in> scene_space\<close>
895+
thus \<open>x \<subseteq>\<^sub>S z\<close>
896+
using idem_scene_space subscene_trans by auto
897+
next
898+
fix A :: \<open>'a scene set\<close>
899+
assume A: \<open>A \<subseteq> scene_space\<close>
900+
901+
hence "is_lub \<lparr>carrier = scene_space, eq = (=), le = (\<subseteq>\<^sub>S)\<rparr> (\<Union>\<^sub>S A) A"
902+
by (rule_tac least_UpperI)
903+
(auto simp add: Upper_def intro!: Sup_scene_props Sup_scene_closed)
904+
thus "\<exists>s. is_lub \<lparr>carrier = scene_space, eq = (=), le = (\<subseteq>\<^sub>S)\<rparr> s A"
905+
by blast
906+
next
907+
fix A :: \<open>'a scene set\<close>
908+
assume A: \<open>A \<subseteq> scene_space\<close>
909+
have "is_glb \<lparr>carrier = scene_space, eq = (=), le = (\<subseteq>\<^sub>S)\<rparr> (\<Inter>\<^sub>S A) A"
910+
by (metis A Inf_scene_glb scene_gorder_def)
911+
thus "\<exists>i. is_glb \<lparr>carrier = scene_space, eq = (=), le = (\<subseteq>\<^sub>S)\<rparr> i A"
912+
by blast
913+
qed
914+
915+
916+
lemma (in complete_lattice) is_lub_modulo_carrier:
917+
"is_lub L x A \<longleftrightarrow> is_lub L x (A \<inter> carrier L)"
918+
by (simp add: Upper_def)
919+
920+
lemma (in complete_lattice) is_glb_modulo_carrier:
921+
"is_glb L x A \<longleftrightarrow> is_glb L x (A \<inter> carrier L)"
922+
by (simp add: Lower_def)
923+
924+
lemma sup_scene_space:
925+
assumes "A \<subseteq> scene_space"
926+
shows "Lattice.sup scene_gorder A = \<Union>\<^sub>S A"
927+
proof -
928+
interpret ss_clat: complete_lattice scene_gorder
929+
by (simp add: scene_space_complete_lattice)
930+
show ?thesis
931+
by (metis Sup_scene_lub assms carrier_scene_gorder ss_clat.least_unique ss_clat.sup_lub)
932+
qed
933+
934+
lemma sup_scene_space_eq: "Lattice.sup scene_gorder A = \<Union>\<^sub>S A"
935+
proof -
936+
have "Lattice.sup scene_gorder A = Lattice.sup scene_gorder (A \<inter> scene_space)"
937+
by (metis Eps_cong carrier_scene_gorder complete_lattice.is_lub_modulo_carrier scene_space_complete_lattice sup_def)
938+
also have "... = \<Union>\<^sub>S (A \<inter> scene_space)"
939+
by (simp add: sup_scene_space)
940+
also have "... = \<Union>\<^sub>S A"
941+
by (simp add: Sup_scene_def)
942+
finally show ?thesis .
943+
qed
944+
945+
lemma sup_scene_space_def: "Lattice.sup scene_gorder = \<Union>\<^sub>S"
946+
using sup_scene_space_eq by auto
947+
948+
lemma inf_scene_space:
949+
assumes "A \<subseteq> scene_space"
950+
shows "Lattice.inf scene_gorder A = \<Inter>\<^sub>S A"
951+
proof -
952+
interpret ss_clat: complete_lattice scene_gorder
953+
by (simp add: scene_space_complete_lattice)
954+
show ?thesis
955+
by (metis Inf_scene_glb assms carrier_scene_gorder ss_clat.greatest_unique ss_clat.inf_glb)
956+
qed
957+
958+
lemma inf_scene_space_eq: "Lattice.inf scene_gorder A = \<Inter>\<^sub>S A"
959+
proof -
960+
have "Lattice.inf scene_gorder A = Lattice.inf scene_gorder (A \<inter> scene_space)"
961+
by (metis Eps_cong carrier_scene_gorder complete_lattice.is_glb_modulo_carrier scene_space_complete_lattice inf_def)
962+
also have "... = \<Inter>\<^sub>S (A \<inter> scene_space)"
963+
by (simp add: inf_scene_space)
964+
also have "... = \<Inter>\<^sub>S A"
965+
by (simp add: Inf_scene_def inj_uminus_scene image_Int Sup_scene_def uminus_image_scene_space)
966+
finally show ?thesis .
967+
qed
968+
969+
lemma scene_gorder_eqs [simp]:
970+
"\<top>\<^bsub>scene_gorder\<^esub> = \<top>\<^sub>S"
971+
"\<bottom>\<^bsub>scene_gorder\<^esub> = \<bottom>\<^sub>S"
972+
proof -
973+
interpret ss_clat: complete_lattice scene_gorder
974+
by (simp add: scene_space_complete_lattice)
975+
show "\<top>\<^bsub>scene_gorder\<^esub> = \<top>\<^sub>S"
976+
by (metis gorder.simps(1) partial_object.simps(1) scene_gorder_def scene_top_greatest ss_clat.le_antisym ss_clat.top_closed ss_clat.top_higher top_scene_space)
977+
show "\<bottom>\<^bsub>scene_gorder\<^esub> = \<bottom>\<^sub>S"
978+
by (metis gorder.simps(1) partial_object.simps(1) scene_bot_least scene_gorder_def scene_space.intros(1) ss_clat.bottom_lower ss_clat.le_antisym ss_clat.weak_partial_order_bottom_axioms
979+
weak_partial_order_bottom.bottom_closed)
980+
qed
981+
982+
interpretation ss_clat: complete_lattice scene_gorder
983+
rewrites "carrier scene_gorder = scene_space" and "elem scene_gorder = (\<in>)" and "le scene_gorder = (\<subseteq>\<^sub>S)" and "eq scene_gorder = (=)" and "\<top>\<^bsub>scene_gorder\<^esub> = \<top>\<^sub>S" and "\<bottom>\<^bsub>scene_gorder\<^esub> = \<bottom>\<^sub>S"
984+
and "Lattice.sup scene_gorder = (\<Union>\<^sub>S)" and "Lattice.inf scene_gorder = (\<Inter>\<^sub>S)" and "Lattice.join scene_gorder = (\<union>\<^sub>S)"
985+
by (auto simp add: scene_space_complete_lattice elem_def set_eq_def sup_scene_space_def fun_eq_iff join_def ss_union_def sup_scene_space_eq inf_scene_space_eq)
986+
749987
subsection \<open> Scene space and basis lenses \<close>
750988

751989
locale var_lens = vwb_lens +

‎Scenes.thy‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -191,6 +191,9 @@ lemma uminus_bot_scene [simp]: "- \<bottom>\<^sub>S = \<top>\<^sub>S"
191191
lemma uminus_scene_twice: "- (- (X :: 's scene)) = X"
192192
by (transfer, simp)
193193

194+
lemma inj_uminus_scene: "inj (uminus :: 'a scene \<Rightarrow> 'a scene)"
195+
by (metis injI uminus_scene_twice)
196+
194197
lemma scene_override_id [simp]: "S\<^sub>1 \<oplus>\<^sub>S S\<^sub>2 on \<top>\<^sub>S = S\<^sub>2"
195198
by (transfer, simp)
196199

0 commit comments

Comments
 (0)