Theory Scene_Spaces
section ‹ Scene Spaces ›
theory Scene_Spaces
imports Scenes
begin
subsection ‹ Preliminaries ›
abbreviation foldr_scene :: "'a scene list ⇒ 'a scene" (‹⨆⇩S›) where
"foldr_scene as ≡ foldr (⊔⇩S) as ⊥⇩S"
lemma pairwise_indep_then_compat [simp]: "pairwise (⨝⇩S) A ⟹ pairwise (##⇩S) A"
by (simp add: pairwise_alt)
lemma pairwise_compat_foldr:
"⟦ pairwise (##⇩S) (set as); ∀ b ∈ set as. a ##⇩S b ⟧ ⟹ a ##⇩S ⨆⇩S as"
apply (induct as)
apply (simp)
apply (auto simp add: pairwise_insert scene_union_pres_compat)
done
lemma foldr_scene_indep:
"⟦ pairwise (##⇩S) (set as); ∀ b ∈ set as. a ⨝⇩S b ⟧ ⟹ a ⨝⇩S ⨆⇩S as"
apply (induct as)
apply (simp)
apply (auto intro: scene_indep_pres_compat simp add: pairwise_insert )
done
lemma foldr_compat_dist:
"pairwise (##⇩S) (set as) ⟹ foldr (⊔⇩S) (map (λa. a ;⇩S x) as) ⊥⇩S = ⨆⇩S as ;⇩S x"
apply (induct as)
apply (simp)
apply (auto simp add: pairwise_insert)
apply (metis pairwise_compat_foldr scene_compat_refl scene_union_comp_distl)
done
lemma foldr_compat_quotient_dist:
"⟦ pairwise (##⇩S) (set as); ∀ a∈set as. a ≤ ⟦x⟧⇩∼ ⟧ ⟹ foldr (⊔⇩S) (map (λa. a /⇩S x) as) ⊥⇩S = ⨆⇩S as /⇩S x"
apply (induct as)
apply (auto simp add: pairwise_insert)
apply (subst scene_union_quotient)
apply simp_all
using pairwise_compat_foldr scene_compat_refl apply blast
apply (meson foldr_scene_indep scene_indep_sym scene_le_iff_indep_inv)
done
lemma foldr_scene_union_add_tail:
"⟦ pairwise (##⇩S) (set xs); ∀ x∈set xs. x ##⇩S b ⟧ ⟹ ⨆⇩S xs ⊔⇩S b = foldr (⊔⇩S) xs b"
apply (induct xs)
apply (simp)
apply (simp)
apply (subst scene_union_assoc[THEN sym])
apply (auto simp add: pairwise_insert)
using pairwise_compat_foldr scene_compat_refl apply blast
apply (meson pairwise_compat_foldr scene_compat_sym)
done
lemma pairwise_Diff: "pairwise R A ⟹ pairwise R (A - B)"
using pairwise_mono by fastforce
lemma scene_compats_members: "⟦ pairwise (##⇩S) A; x ∈ A; y ∈ A ⟧ ⟹ x ##⇩S y"
by (metis pairwise_def scene_compat_refl)
corollary foldr_scene_union_removeAll:
assumes "pairwise (##⇩S) (set xs)" "x ∈ set xs"
shows "⨆⇩S (removeAll x xs) ⊔⇩S x = ⨆⇩S xs"
using assms proof (induct xs)
case Nil
then show ?case by simp
next
case (Cons a xs)
have x_compat: "⋀ z. z ∈ set xs ⟹ x ##⇩S z"
using Cons.prems(1) Cons.prems(2) scene_compats_members by auto
from Cons have x_compats: "x ##⇩S ⨆⇩S (removeAll x xs)"
by (metis (no_types, lifting) insert_Diff list.simps(15) pairwise_compat_foldr pairwise_insert removeAll_id set_removeAll x_compat)
from Cons have a_compats: "a ##⇩S ⨆⇩S (removeAll x xs)"
by (metis (no_types, lifting) insert_Diff insert_iff list.simps(15) pairwise_compat_foldr pairwise_insert scene_compat_refl set_removeAll x_compats)
from Cons show ?case
proof (cases "x ∈ set xs")
case True
with Cons show ?thesis
by (auto simp add: pairwise_insert scene_union_commute)
(metis a_compats scene_compats_members scene_union_assoc scene_union_idem,
metis (full_types) a_compats scene_union_assoc scene_union_commute x_compats)
next
case False
with Cons show ?thesis
by (simp add: scene_union_commute)
qed
qed
lemma foldr_scene_union_eq_sets:
assumes "pairwise (##⇩S) (set xs)" "set xs = set ys"
shows "⨆⇩S xs = ⨆⇩S ys"
using assms proof (induct xs arbitrary: ys)
case Nil
then show ?case
by simp
next
case (Cons a xs)
hence ys: "set ys = insert a (set (removeAll a ys))"
by (auto)
then show ?case
by (metis (no_types, lifting) Cons.hyps Cons.prems(1) Cons.prems(2) Diff_insert_absorb foldr_scene_union_removeAll insertCI insert_absorb list.simps(15) pairwise_insert set_removeAll)
qed
lemma foldr_scene_removeAll:
assumes "pairwise (##⇩S) (set xs)"
shows "x ⊔⇩S ⨆⇩S (removeAll x xs) = x ⊔⇩S ⨆⇩S xs"
by (metis (mono_tags, opaque_lifting) assms foldr_Cons foldr_scene_union_eq_sets insertCI insert_Diff list.simps(15) o_apply removeAll.simps(2) removeAll_id set_removeAll)
lemma pairwise_Collect: "pairwise R A ⟹ pairwise R {x ∈ A. P x}"
by (simp add: pairwise_def)
lemma removeAll_overshadow_filter:
"removeAll x (filter (λxa. xa ∉ A - {x}) xs) = removeAll x (filter (λ xa. xa ∉ A) xs)"
apply (simp add: removeAll_filter_not_eq)
apply (rule filter_cong)
apply (simp)
apply auto
done
corollary foldr_scene_union_filter:
assumes "pairwise (##⇩S) (set xs)" "set ys ⊆ set xs"
shows "⨆⇩S xs = ⨆⇩S (filter (λx. x ∉ set ys) xs) ⊔⇩S ⨆⇩S ys"
using assms proof (induct xs arbitrary: ys)
case Nil
then show ?case by (simp)
next
case (Cons x xs)
show ?case
proof (cases "x ∈ set ys")
case True
with Cons have 1: "set ys - {x} ⊆ set xs"
by (auto)
have 2: "x ##⇩S ⨆⇩S (removeAll x ys)"
by (metis Cons.prems(1) Cons.prems(2) True foldr_scene_removeAll foldr_scene_union_removeAll pairwise_subset scene_compat_bot(2) scene_compat_sym scene_union_incompat scene_union_unit(1))
have 3: "⋀ P. x ##⇩S ⨆⇩S (filter P xs)"
by (meson Cons.prems(1) Cons.prems(2) True filter_is_subset in_mono pairwise_compat_foldr pairwise_subset scene_compats_members set_subset_Cons)
have 4: "⋀ P. ⨆⇩S (filter P xs) ##⇩S ⨆⇩S (removeAll x ys)"
by (rule pairwise_compat_foldr)
(metis Cons.prems(1) Cons.prems(2) pairwise_Diff pairwise_subset set_removeAll,
metis (no_types, lifting) "1" Cons.prems(1) filter_is_subset pairwise_compat_foldr pairwise_subset scene_compat_sym scene_compats_members set_removeAll set_subset_Cons subsetD)
have "⨆⇩S (x # xs) = x ⊔⇩S ⨆⇩S xs"
by simp
also have "... = x ⊔⇩S (⨆⇩S (filter (λxa. xa ∉ set ys - {x}) xs) ⊔⇩S ⨆⇩S (removeAll x ys))"
using 1 Cons(1)[where ys="removeAll x ys"] Cons(2) by (simp add: pairwise_insert)
also have "... = (x ⊔⇩S ⨆⇩S (filter (λxa. xa ∉ set ys - {x}) xs)) ⊔⇩S ⨆⇩S (removeAll x ys)"
by (simp add: scene_union_assoc 1 2 3 4)
also have "... = (x ⊔⇩S ⨆⇩S (removeAll x (filter (λxa. xa ∉ set ys - {x}) xs))) ⊔⇩S ⨆⇩S (removeAll x ys)"
by (metis (no_types, lifting) Cons.prems(1) filter_is_subset foldr_scene_removeAll pairwise_subset set_subset_Cons)
also have "... = (x ⊔⇩S ⨆⇩S (removeAll x (filter (λxa. xa ∉ set ys) xs))) ⊔⇩S ⨆⇩S (removeAll x ys)"
by (simp only: removeAll_overshadow_filter)
also have "... = (x ⊔⇩S ⨆⇩S (removeAll x (filter (λxa. xa ∉ set ys) (x # xs)))) ⊔⇩S ⨆⇩S (removeAll x ys)"
by simp
also have "... = (x ⊔⇩S ⨆⇩S (filter (λxa. xa ∉ set ys) (x # xs))) ⊔⇩S ⨆⇩S (removeAll x ys)"
by (simp add: True)
also have "... = (⨆⇩S (filter (λxa. xa ∉ set ys) (x # xs)) ⊔⇩S x) ⊔⇩S ⨆⇩S (removeAll x ys)"
by (simp add: scene_union_commute)
also have "... = ⨆⇩S (filter (λxa. xa ∉ set ys) (x # xs)) ⊔⇩S (x ⊔⇩S ⨆⇩S (removeAll x ys))"
by (simp add: scene_union_assoc True 2 3 4 scene_compat_sym)
also have "... = ⨆⇩S (filter (λxa. xa ∉ set ys) (x # xs)) ⊔⇩S ⨆⇩S ys"
by (metis (no_types, lifting) Cons.prems(1) Cons.prems(2) True foldr_scene_union_removeAll pairwise_subset scene_union_commute)
finally show ?thesis .
next
case False
with Cons(2-3) have 1: "set ys ⊆ set xs"
by auto
have 2: "x ##⇩S ⨆⇩S (filter (λx. x ∉ set ys) xs)"
by (metis (no_types, lifting) Cons.prems(1) filter_is_subset filter_set list.simps(15) member_filter pairwise_compat_foldr pairwise_insert pairwise_subset scene_compat_refl)
have 3: "x ##⇩S ⨆⇩S ys"
by (meson Cons.prems(1) Cons.prems(2) list.set_intros(1) pairwise_compat_foldr pairwise_subset scene_compats_members subset_code(1))
from Cons(1)[of ys] Cons(2-3) have 4: "⨆⇩S (filter (λx. x ∉ set ys) xs) ##⇩S ⨆⇩S ys"
by (auto simp add: pairwise_insert)
(metis (no_types, lifting) "1" foldr_append foldr_scene_union_eq_sets scene_compat_bot(1) scene_union_incompat set_append subset_Un_eq)
with 1 False Cons(1)[of ys] Cons(2-3) show ?thesis
by (auto simp add: pairwise_insert scene_union_assoc 2 3 4)
qed
qed
lemma foldr_scene_append:
"⟦ pairwise (##⇩S) (set (xs @ ys)) ⟧ ⟹ ⨆⇩S (xs @ ys) = ⨆⇩S xs ⊔⇩S ⨆⇩S ys"
by (simp add: foldr_scene_union_add_tail pairwise_compat_foldr pairwise_subset scene_compats_members)
lemma foldr_scene_concat:
"⟦ pairwise (##⇩S) (set (concat xs)) ⟧ ⟹ ⨆⇩S (concat xs) = ⨆⇩S (map ⨆⇩S xs)"
by (induct xs, simp_all, metis foldr_append foldr_scene_append pairwise_subset set_append set_concat sup_ge2)
subsection ‹ Predicates ›
text ‹ All scenes in the set are independent ›
definition scene_indeps :: "'s scene set ⇒ bool" where
"scene_indeps = pairwise (⨝⇩S)"
text ‹ All scenes in the set cover the entire state space ›
definition scene_span :: "'s scene list ⇒ bool" where
"scene_span S = (foldr (⊔⇩S) S ⊥⇩S = ⊤⇩S)"
text ‹ cf. @{term finite_dimensional_vector_space}, which scene spaces are based on. ›
subsection ‹ Scene space class ›
class scene_space =
fixes Vars :: "'a scene list"
assumes idem_scene_Vars [simp]: "⋀ x. x ∈ set Vars ⟹ idem_scene x"
and indep_Vars: "scene_indeps (set Vars)"
and span_Vars: "scene_span Vars"
begin
lemma scene_space_compats [simp]: "pairwise (##⇩S) (set Vars)"
by (metis local.indep_Vars pairwise_alt scene_indep_compat scene_indeps_def)
lemma Vars_ext_lens_indep: "⟦ a ;⇩S x ≠ b ;⇩S x; a ∈ set Vars; b ∈ set Vars ⟧ ⟹ a ;⇩S x ⨝⇩S b ;⇩S x"
by (metis indep_Vars pairwiseD scene_comp_indep scene_indeps_def)
inductive_set scene_space :: "'a scene set" where
bot_scene_space [intro]: "⊥⇩S ∈ scene_space" |
Vars_scene_space [intro]: "x ∈ set Vars ⟹ x ∈ scene_space" |
union_scene_space [intro]: "⟦ x ∈ scene_space; y ∈ scene_space ⟧ ⟹ x ⊔⇩S y ∈ scene_space"
lemma idem_scene_space: "a ∈ scene_space ⟹ idem_scene a"
by (induct rule: scene_space.induct) auto
lemma set_Vars_scene_space [simp]: "set Vars ⊆ scene_space"
by blast
lemma pairwise_compat_Vars_subset: "set xs ⊆ set Vars ⟹ pairwise (##⇩S) (set xs)"
using pairwise_subset scene_space_compats by blast
lemma scene_space_foldr: "set xs ⊆ scene_space ⟹ ⨆⇩S xs ∈ scene_space"
by (induction xs, auto)
lemma top_scene_eq: "⊤⇩S = ⨆⇩S Vars"
using local.span_Vars scene_span_def by force
lemma top_scene_space: "⊤⇩S ∈ scene_space"
proof -
have "⊤⇩S = foldr (⊔⇩S) Vars ⊥⇩S"
using span_Vars by (simp add: scene_span_def)
also have "... ∈ scene_space"
by (simp add: scene_space_foldr)
finally show ?thesis .
qed
lemma Vars_compat_scene_space: "⟦ b ∈ scene_space; x ∈ set Vars ⟧ ⟹ x ##⇩S b"
proof (induct b rule: scene_space.induct)
case bot_scene_space
then show ?case
by (metis scene_compat_refl scene_union_incompat scene_union_unit(1))
next
case (Vars_scene_space a)
then show ?case
by (metis local.indep_Vars pairwiseD scene_compat_refl scene_indep_compat scene_indeps_def)
next
case (union_scene_space a b)
then show ?case
using scene_union_pres_compat by blast
qed
lemma scene_space_compat: "⟦ a ∈ scene_space; b ∈ scene_space ⟧ ⟹ a ##⇩S b"
proof (induct rule: scene_space.induct)
case bot_scene_space
then show ?case
by simp
next
case (Vars_scene_space x)
then show ?case
by (simp add: Vars_compat_scene_space)
next
case (union_scene_space x y)
then show ?case
using scene_compat_sym scene_union_pres_compat by blast
qed
corollary scene_space_union_assoc:
assumes "x ∈ scene_space" "y ∈ scene_space" "z ∈ scene_space"
shows "x ⊔⇩S (y ⊔⇩S z) = (x ⊔⇩S y) ⊔⇩S z"
by (simp add: assms scene_space_compat scene_union_assoc)
lemma scene_space_vars_decomp: "a ∈ scene_space ⟹ ∃xs. set xs ⊆ set Vars ∧ foldr (⊔⇩S) xs ⊥⇩S = a"
proof (induct rule: scene_space.induct)
case bot_scene_space
then show ?case
by (simp add: exI[where x="[]"])
next
case (Vars_scene_space x)
show ?case
apply (rule exI[where x="[x]"])
using Vars_scene_space by simp
next
case (union_scene_space x y)
then obtain xs ys where xsys: "set xs ⊆ set Vars ∧ foldr (⊔⇩S) xs ⊥⇩S = x"
"set ys ⊆ set Vars ∧ foldr (⊔⇩S) ys ⊥⇩S = y"
by blast+
show ?case
proof (rule exI[where x="xs @ ys"])
show "set (xs @ ys) ⊆ set Vars ∧ ⨆⇩S (xs @ ys) = x ⊔⇩S y"
by (auto simp: xsys)
(metis (full_types) Vars_compat_scene_space foldr_scene_union_add_tail pairwise_subset
scene_space_compats subsetD union_scene_space.hyps(3) xsys(1))
qed
qed
lemma scene_space_vars_decomp_iff: "a ∈ scene_space ⟷ (∃xs. set xs ⊆ set Vars ∧ a = foldr (⊔⇩S) xs ⊥⇩S)"
apply (auto simp add: scene_space_vars_decomp scene_space.Vars_scene_space scene_space_foldr)
apply (simp add: scene_space.Vars_scene_space scene_space_foldr subset_eq)
using scene_space_vars_decomp apply auto[1]
by (meson dual_order.trans scene_space_foldr set_Vars_scene_space)
lemma "fold (⊔⇩S) (map (λx. x ;⇩S a) Vars) b = ⟦a⟧⇩∼ ⊔⇩S b"
oops
lemma Vars_indep_foldr:
assumes "x ∈ set Vars" "set xs ⊆ set Vars"
shows "x ⨝⇩S ⨆⇩S (removeAll x xs)"
proof (rule foldr_scene_indep)
show "pairwise (##⇩S) (set (removeAll x xs))"
by (simp, metis Diff_subset assms(2) pairwise_mono scene_space_compats)
from assms show "∀b∈set (removeAll x xs). x ⨝⇩S b"
by (simp)
(metis DiffE insertI1 local.indep_Vars pairwiseD scene_indeps_def subset_iff)
qed
lemma Vars_indeps_foldr:
assumes "set xs ⊆ set Vars"
shows "foldr (⊔⇩S) xs ⊥⇩S ⨝⇩S foldr (⊔⇩S) (filter (λx. x ∉ set xs) Vars) ⊥⇩S"
apply (rule foldr_scene_indep)
apply (meson filter_is_subset pairwise_subset scene_space_compats)
apply (simp)
apply auto
apply (rule scene_indep_sym)
apply (metis (no_types, lifting) assms foldr_scene_indep local.indep_Vars pairwiseD pairwise_mono scene_indeps_def scene_space_compats subset_iff)
done
lemma uminus_var_other_vars:
assumes "x ∈ set Vars"
shows "- x = foldr (⊔⇩S) (removeAll x Vars) ⊥⇩S"
proof (rule scene_union_indep_uniq[where Z="x"])
show "idem_scene (foldr (⊔⇩S) (removeAll x Vars) ⊥⇩S)"
by (metis Diff_subset idem_scene_space order_trans scene_space_foldr set_Vars_scene_space set_removeAll)
show "idem_scene x" "idem_scene (-x)"
by (simp_all add: assms local.idem_scene_Vars)
show "foldr (⊔⇩S) (removeAll x Vars) ⊥⇩S ⨝⇩S x"
using Vars_indep_foldr assms scene_indep_sym by blast
show "- x ⨝⇩S x"
using scene_indep_self_compl scene_indep_sym by blast
show "- x ⊔⇩S x = foldr (⊔⇩S) (removeAll x Vars) ⊥⇩S ⊔⇩S x"
by (metis ‹idem_scene (- x)› assms foldr_scene_union_removeAll local.span_Vars scene_space_compats scene_span_def scene_union_compl uminus_scene_twice)
qed
lemma uminus_vars_other_vars:
assumes "set xs ⊆ set Vars"
shows "- ⨆⇩S xs = ⨆⇩S (filter (λx. x ∉ set xs) Vars)"
proof (rule scene_union_indep_uniq[where Z="foldr (⊔⇩S) xs ⊥⇩S"])
show "idem_scene (- foldr (⊔⇩S) xs ⊥⇩S)" "idem_scene (foldr (⊔⇩S) xs ⊥⇩S)"
using assms idem_scene_space idem_scene_uminus scene_space_vars_decomp_iff by blast+
show "idem_scene (foldr (⊔⇩S) (filter (λx. x ∉ set xs) Vars) ⊥⇩S)"
by (meson filter_is_subset idem_scene_space scene_space_vars_decomp_iff)
show "- foldr (⊔⇩S) xs ⊥⇩S ⨝⇩S foldr (⊔⇩S) xs ⊥⇩S"
by (metis scene_indep_self_compl uminus_scene_twice)
show "foldr (⊔⇩S) (filter (λx. x ∉ set xs) Vars) ⊥⇩S ⨝⇩S foldr (⊔⇩S) xs ⊥⇩S"
using Vars_indeps_foldr assms scene_indep_sym by blast
show "- ⨆⇩S xs ⊔⇩S ⨆⇩S xs = ⨆⇩S (filter (λx. x ∉ set xs) Vars) ⊔⇩S ⨆⇩S xs"
using foldr_scene_union_filter[of Vars xs, THEN sym]
by (simp add: assms)
(metis ‹idem_scene (- ⨆⇩S xs)› local.span_Vars scene_span_def scene_union_compl uminus_scene_twice)
qed
lemma scene_space_uminus: "⟦ a ∈ scene_space ⟧ ⟹ - a ∈ scene_space"
by (auto simp add: scene_space_vars_decomp_iff uminus_vars_other_vars)
(metis filter_is_subset)
lemma scene_space_inter: "⟦ a ∈ scene_space; b ∈ scene_space ⟧ ⟹ a ⊓⇩S b ∈ scene_space"
by (simp add: inf_scene_def scene_space.union_scene_space scene_space_uminus)
lemma scene_union_foldr_remove_element:
assumes "set xs ⊆ set Vars"
shows "a ⊔⇩S ⨆⇩S xs = a ⊔⇩S ⨆⇩S (removeAll a xs)"
using assms proof (induct xs)
case Nil
then show ?case by simp
next
case (Cons a xs)
then show ?case apply auto
apply (metis order_trans scene_space.Vars_scene_space scene_space_foldr scene_space_union_assoc scene_union_idem set_Vars_scene_space)
apply (smt (verit, best) Diff_subset dual_order.trans removeAll_id scene_space_foldr scene_space_union_assoc scene_union_commute set_Vars_scene_space set_removeAll subset_iff)
done
qed
lemma scene_union_foldr_Cons_removeAll:
assumes "set xs ⊆ set Vars" "a ∈ set xs"
shows "foldr (⊔⇩S) xs ⊥⇩S = foldr (⊔⇩S) (a # removeAll a xs) ⊥⇩S"
by (metis assms(1) assms(2) foldr_scene_union_eq_sets insert_Diff list.simps(15) pairwise_subset scene_space_compats set_removeAll)
lemma scene_union_foldr_Cons_removeAll':
assumes "set xs ⊆ set Vars" "a ∈ set Vars"
shows "foldr (⊔⇩S) (a # xs) ⊥⇩S = foldr (⊔⇩S) (a # removeAll a xs) ⊥⇩S"
by (simp add: assms(1) scene_union_foldr_remove_element)
lemma scene_in_foldr: "⟦ a ∈ set xs; set xs ⊆ set Vars ⟧ ⟹ a ⊆⇩S ⨆⇩S xs"
apply (induct xs)
apply (simp)
apply (subst scene_union_foldr_Cons_removeAll')
apply simp
apply simp
apply (auto)
apply (rule scene_union_ub)
apply (metis Diff_subset dual_order.trans idem_scene_space scene_space_vars_decomp_iff set_removeAll)
using Vars_indep_foldr apply blast
apply (metis Vars_indep_foldr foldr_scene_union_removeAll idem_scene_space local.idem_scene_Vars order.trans pairwise_mono removeAll_id scene_indep_sym scene_space_compats scene_space_foldr scene_union_commute scene_union_ub set_Vars_scene_space subscene_trans)
done
lemma scene_union_foldr_subset:
assumes "set xs ⊆ set ys" "set ys ⊆ set Vars"
shows "⨆⇩S xs ⊆⇩S ⨆⇩S ys"
using assms proof (induct xs arbitrary: ys)
case Nil
then show ?case
by (simp add: scene_bot_least)
next
case (Cons a xs)
{ assume "a ∈ set xs"
with Cons have "foldr (⊔⇩S) xs ⊥⇩S = foldr (⊔⇩S) (a # removeAll a xs) ⊥⇩S"
apply (subst scene_union_foldr_Cons_removeAll)
apply (auto)
done
} note a_in = this
{ assume "a ∉ set xs"
then have "a ⊔⇩S foldr (⊔⇩S) xs ⊥⇩S = foldr (⊔⇩S) (a # xs) ⊥⇩S"
by simp
} note a_out = this
show ?case apply (simp)
apply (cases "a ∈ set xs")
using a_in Cons apply auto
apply (metis dual_order.trans scene_union_foldr_remove_element)
using a_out Cons apply auto
apply (rule scene_union_mono)
using scene_in_foldr apply blast
apply blast
apply (meson Vars_compat_scene_space dual_order.trans scene_space_foldr set_Vars_scene_space subsetD)
using local.idem_scene_Vars apply blast
apply (meson idem_scene_space scene_space_foldr set_Vars_scene_space subset_trans)
done
qed
lemma union_scene_space_foldrs:
assumes "set xs ⊆ set Vars" "set ys ⊆ set Vars"
shows "(foldr (⊔⇩S) xs ⊥⇩S) ⊔⇩S (foldr (⊔⇩S) ys ⊥⇩S) = foldr (⊔⇩S) (xs @ ys) ⊥⇩S"
using assms
apply (induct ys)
apply (simp_all)
apply (metis Vars_compat_scene_space foldr_scene_union_add_tail local.indep_Vars pairwise_mono scene_indep_compat scene_indeps_def scene_space.Vars_scene_space scene_space.union_scene_space scene_space_foldr subset_eq)
done
lemma scene_space_ub:
assumes "a ∈ scene_space" "b ∈ scene_space"
shows "a ⊆⇩S a ⊔⇩S b"
using assms
apply (auto simp add: scene_space_vars_decomp_iff union_scene_space_foldrs)
by (smt (verit, ccfv_SIG) foldr_append scene_union_foldr_subset set_append sup.bounded_iff sup_commute sup_ge2)
lemma scene_compl_subset_iff:
assumes "a ∈ scene_space" "b ∈ scene_space"
shows "- a ⊆⇩S -b ⟷ b ⊆⇩S a"
by (metis scene_indep_sym scene_le_iff_indep_inv uminus_scene_twice)
lemma inter_scene_space_foldrs:
assumes "set xs ⊆ set Vars" "set ys ⊆ set Vars"
shows "⨆⇩S xs ⊓⇩S ⨆⇩S ys = ⨆⇩S (filter (λ x. x ∈ set xs ∩ set ys) Vars)"
proof -
have "⨆⇩S xs ⊓⇩S ⨆⇩S ys = - (- ⨆⇩S xs ⊔⇩S - ⨆⇩S ys)"
by (simp add: inf_scene_def)
also have "... = - (⨆⇩S (filter (λx. x ∉ set xs) Vars) ⊔⇩S ⨆⇩S (filter (λx. x ∉ set ys) Vars))"
by (simp add: uminus_vars_other_vars assms)
also have "... = - ⨆⇩S (filter (λx. x ∉ set xs) Vars @ filter (λx. x ∉ set ys) Vars)"
by (simp add: union_scene_space_foldrs assms)
also have "... = ⨆⇩S (filter (λx. x ∉ set (filter (λx. x ∉ set xs) Vars @ filter (λx. x ∉ set ys) Vars)) Vars)"
by (subst uminus_vars_other_vars, simp_all)
also have "... = ⨆⇩S (filter (λ x. x ∈ set xs ∩ set ys) Vars)"
proof -
have "⋀x. x ∈ set Vars ⟹ ((x ∈ set Vars ⟶ x ∈ set xs) ∧ (x ∈ set Vars ⟶ x ∈ set ys)) = (x ∈ set xs ∧ x ∈ set ys)"
by auto
thus ?thesis
by (simp cong: arg_cong[where f="⨆⇩S"] filter_cong add: assms)
qed
finally show ?thesis .
qed
lemma scene_inter_distrib_lemma:
assumes "set xs ⊆ set Vars" "set ys ⊆ set Vars" "set zs ⊆ set Vars"
shows "⨆⇩S xs ⊔⇩S (⨆⇩S ys ⊓⇩S ⨆⇩S zs) = (⨆⇩S xs ⊔⇩S ⨆⇩S ys) ⊓⇩S (⨆⇩S xs ⊔⇩S ⨆⇩S zs)"
using assms
apply (simp only: union_scene_space_foldrs inter_scene_space_foldrs)
apply (subst union_scene_space_foldrs)
apply (simp add: assms)
apply (simp add: assms)
apply (subst inter_scene_space_foldrs)
apply (simp)
apply (simp)
apply (rule foldr_scene_union_eq_sets)
apply (simp)
apply (smt (verit, ccfv_threshold) Un_subset_iff mem_Collect_eq pairwise_subset scene_space_compats subset_iff)
apply (auto)
done
lemma scene_union_inter_distrib:
assumes "a ∈ scene_space" "b ∈ scene_space" "c ∈ scene_space"
shows "a ⊔⇩S b ⊓⇩S c = (a ⊔⇩S b) ⊓⇩S (a ⊔⇩S c)"
using assms
by (auto simp add: scene_space_vars_decomp_iff scene_inter_distrib_lemma)
lemma finite_distinct_lists_subset:
assumes "finite A"
shows "finite {xs. distinct xs ∧ set xs ⊆ A}"
by (metis (no_types, lifting) Collect_cong finite_subset_distinct[OF assms])
lemma foldr_scene_union_remdups: "set xs ⊆ set Vars ⟹ ⨆⇩S (remdups xs) = ⨆⇩S xs"
by (auto intro: foldr_scene_union_eq_sets simp add: pairwise_compat_Vars_subset)
lemma scene_space_as_lists:
"scene_space = {⨆⇩S xs | xs. distinct xs ∧ set xs ⊆ set Vars}"
proof (rule Set.set_eqI, rule iffI)
fix a
assume "a ∈ scene_space"
then obtain xs where xs: "set xs ⊆ set Vars" "⨆⇩S xs = a"
using scene_space_vars_decomp_iff by auto
thus "a ∈ {⨆⇩S xs |xs. distinct xs ∧ set xs ⊆ set Vars}"
by auto (metis distinct_remdups foldr_scene_union_remdups set_remdups)
next
fix a
assume "a ∈ {⨆⇩S xs |xs. distinct xs ∧ set xs ⊆ set Vars}"
thus "a ∈ scene_space"
using scene_space_vars_decomp_iff by auto
qed
lemma finite_scene_space: "finite scene_space"
proof -
have "scene_space = {⨆⇩S xs | xs. distinct xs ∧ set xs ⊆ set Vars}"
by (simp add: scene_space_as_lists)
also have "... = ⨆⇩S ` {xs. distinct xs ∧ set xs ⊆ set Vars}"
by auto
also have "finite ..."
by (rule finite_imageI, simp add: finite_distinct_lists_subset)
finally show ?thesis .
qed
lemma scene_space_inter_assoc:
assumes "x ∈ scene_space" "y ∈ scene_space" "z ∈ scene_space"
shows "(x ⊓⇩S y) ⊓⇩S z = x ⊓⇩S (y ⊓⇩S z)"
proof -
have "(x ⊓⇩S y) ⊓⇩S z = - (- x ⊔⇩S - y ⊔⇩S - z)"
by (simp add: scene_demorgan1 uminus_scene_twice)
also have "... = - (- x ⊔⇩S (- y ⊔⇩S - z))"
by (simp add: assms scene_space_uminus scene_space_union_assoc)
also have "... = x ⊓⇩S (y ⊓⇩S z)"
by (simp add: scene_demorgan1 uminus_scene_twice)
finally show ?thesis .
qed
lemma scene_inter_union_distrib:
assumes "x ∈ scene_space" "y ∈ scene_space" "z ∈ scene_space"
shows "x ⊓⇩S (y ⊔⇩S z) = (x ⊓⇩S y) ⊔⇩S (x ⊓⇩S z)"
proof-
have "x ⊓⇩S (y ⊔⇩S z) = (x ⊓⇩S (x ⊔⇩S z)) ⊓⇩S (y ⊔⇩S z)"
by (metis assms(1) assms(3) idem_scene_space local.scene_union_inter_distrib scene_indep_bot scene_inter_commute scene_inter_indep scene_space.simps scene_union_unit(1))
also have "... = (y ⊔⇩S z) ⊓⇩S (x ⊓⇩S (x ⊔⇩S z))"
by (simp add: scene_union_inter_distrib assms scene_inter_commute scene_union_assoc union_scene_space scene_space_inter scene_union_commute)
also have "… = x ⊓⇩S ((y ⊔⇩S z) ⊓⇩S (x ⊔⇩S z))"
by (metis assms scene_inter_commute scene_space.union_scene_space scene_space_inter_assoc)
also have "… = x ⊓⇩S (z ⊔⇩S (x ⊓⇩S y))"
by (simp add: assms scene_union_inter_distrib scene_inter_commute scene_union_commute)
also have "… = ((x ⊓⇩S y) ⊔⇩S x) ⊓⇩S ((x ⊓⇩S y) ⊔⇩S z)"
by (metis (no_types, opaque_lifting) assms(1) assms(2) idem_scene_space local.scene_union_inter_distrib scene_indep_bot scene_inter_commute scene_inter_indep scene_space.bot_scene_space scene_union_commute scene_union_idem scene_union_unit(1))
also have "… = (x ⊓⇩S y) ⊔⇩S (x ⊓⇩S z)"
by (simp add: assms scene_union_inter_distrib scene_space_inter)
finally show ?thesis .
qed
lemma scene_union_inter_minus:
assumes "a ∈ scene_space" "b ∈ scene_space"
shows "a ⊔⇩S (b ⊓⇩S - a) = a ⊔⇩S b"
by (metis assms(1) assms(2) bot_idem_scene idem_scene_space idem_scene_uminus local.scene_union_inter_distrib scene_demorgan1 scene_space_uminus scene_union_compl scene_union_unit(1) uminus_scene_twice)
lemma scene_union_foldr_minus_element:
assumes "a ∈ scene_space" "set xs ⊆ scene_space"
shows "a ⊔⇩S ⨆⇩S xs = a ⊔⇩S ⨆⇩S (map (λ x. x ⊓⇩S - a) xs)"
using assms proof (induct xs)
case Nil
then show ?case by (simp)
next
case (Cons y ys)
have "a ⊔⇩S (y ⊔⇩S ⨆⇩S ys) = y ⊔⇩S (a ⊔⇩S ⨆⇩S ys)"
by (metis Cons.prems(2) assms(1) insert_subset list.simps(15) scene_space_foldr scene_space_union_assoc scene_union_commute)
also have "... = y ⊔⇩S (a ⊔⇩S ⨆⇩S (map (λx. x ⊓⇩S - a) ys))"
using Cons.hyps Cons.prems(2) assms(1) by auto
also have "... = y ⊔⇩S a ⊔⇩S ⨆⇩S (map (λx. x ⊓⇩S - a) ys)"
apply (subst scene_union_assoc)
using Cons.prems(2) assms(1) scene_space_compat apply auto[1]
apply (rule pairwise_compat_foldr)
apply (simp)
apply (rule pairwise_imageI)
apply (meson Cons.prems(2) assms(1) scene_space_compat scene_space_inter scene_space_uminus set_subset_Cons subsetD)
apply simp
apply (meson Cons.prems(2) assms(1) in_mono list.set_intros(1) scene_space_compat scene_space_inter scene_space_uminus set_subset_Cons)
apply (rule pairwise_compat_foldr)
apply (simp)
apply (rule pairwise_imageI)
apply (meson Cons.prems(2) assms(1) in_mono scene_space_compat scene_space_inter scene_space_uminus set_subset_Cons)
apply (simp)
apply (meson Cons.prems(2) assms(1) in_mono scene_space_compat scene_space_inter scene_space_uminus set_subset_Cons)
apply simp
done
also have "... = a ⊔⇩S (y ⊓⇩S - a ⊔⇩S ⨆⇩S (map (λx. x ⊓⇩S - a) ys))"
apply (subst scene_union_assoc)
using Cons.prems(2) assms(1) scene_space_compat scene_space_inter scene_space_uminus apply force
apply (metis (no_types, lifting) Cons.hyps Cons.prems(2) assms(1) insert_subset list.simps(15) scene_compat_sym scene_space_compat scene_space_foldr scene_union_assoc scene_union_idem scene_union_incompat scene_union_unit(1))
apply (rule scene_space_compat)
using Cons.prems(2) assms(1) scene_space_inter scene_space_uminus apply auto[1]
apply (rule scene_space_foldr)
apply auto
apply (meson Cons.prems(2) assms(1) in_mono scene_space_inter scene_space_uminus set_subset_Cons)
apply (metis Cons.prems(2) assms(1) insert_subset list.simps(15) scene_union_inter_minus scene_union_commute)
done
finally show ?case using Cons
by auto
qed
lemma scene_space_in_foldr: "⟦ a ∈ set xs; set xs ⊆ scene_space ⟧ ⟹ a ⊆⇩S ⨆⇩S xs"
proof (induct xs)
case Nil
then show ?case
by simp
next
case (Cons y ys)
have ysp: "y ⊔⇩S ⨆⇩S ys = y ⊔⇩S ⨆⇩S (map (λ x. x ⊓⇩S - y) ys)"
using Cons.prems(2) scene_union_foldr_minus_element by force
show ?case
proof (cases "a ⊆⇩S y")
case False
with Cons show ?thesis
by (simp)
(metis (no_types, lifting) idem_scene_space scene_space_foldr scene_space_ub scene_union_commute subscene_trans)
next
case True
with Cons show ?thesis
by (simp)
(meson idem_scene_space scene_space_foldr scene_space_ub subscene_trans)
qed
qed
lemma scene_space_foldr_lb:
"⟦ a ∈ scene_space; set xs ⊆ scene_space; ∀ b∈set xs. b ≤ a ⟧ ⟹ ⨆⇩S xs ⊆⇩S a"
proof (induct xs arbitrary: a)
case Nil
then show ?case
by (simp add: scene_bot_least)
next
case (Cons x xs)
then show ?case
by (simp add: scene_space_compat scene_space_foldr scene_union_lb)
qed
lemma var_le_union_choice:
"⟦ x ∈ set Vars; a ∈ scene_space; b ∈ scene_space; x ≤ a ⊔⇩S b ⟧ ⟹ (x ≤ a ∨ x ≤ b)"
by (auto simp add: scene_space_vars_decomp_iff)
(metis Vars_indep_foldr bot_idem_scene idem_scene_space removeAll_id scene_bot_least scene_indep_pres_compat scene_le_iff_indep_inv scene_space.union_scene_space scene_space_foldr scene_space_in_foldr scene_union_compl set_Vars_scene_space subscene_trans subset_trans uminus_scene_twice uminus_top_scene)
lemma var_le_union_iff:
"⟦ x ∈ set Vars; a ∈ scene_space; b ∈ scene_space ⟧ ⟹ x ≤ a ⊔⇩S b ⟷ (x ≤ a ∨ x ≤ b)"
apply (rule iffI, simp add: var_le_union_choice)
apply (auto)
apply (meson idem_scene_space scene_space_ub subscene_trans)
apply (metis idem_scene_space scene_space_ub scene_union_commute subscene_trans)
done
text ‹ @{term Vars} may contain the empty scene, as we want to allow vacuous lenses in alphabets ›
lemma le_vars_then_equal: "⟦ x ∈ set Vars; y ∈ set Vars; x ≤ y; x ≠ ⊥⇩S ⟧ ⟹ x = y"
by (metis bot_idem_scene foldr_scene_removeAll local.idem_scene_Vars local.indep_Vars local.span_Vars pairwiseD scene_bot_least scene_indep_pres_compat scene_indeps_def scene_le_iff_indep_inv scene_space_compats scene_span_def scene_union_annhil subscene_antisym uminus_scene_twice uminus_top_scene uminus_var_other_vars)
end
lemma foldr_scene_union_eq_scene_space:
"⟦ set xs ⊆ scene_space; set xs = set ys ⟧ ⟹ ⨆⇩S xs = ⨆⇩S ys"
by (metis foldr_scene_union_eq_sets pairwise_def pairwise_subset scene_space_compat)
subsection ‹ Mapping a lens over a scene list ›
definition map_lcomp :: "'b scene list ⇒ ('b ⟹ 'a) ⇒ 'a scene list" where
"map_lcomp ss a = map (λ x. x ;⇩S a) ss"
lemma map_lcomp_dist:
"⟦ pairwise (##⇩S) (set xs); vwb_lens a ⟧ ⟹ ⨆⇩S (map_lcomp xs a) = ⨆⇩S xs ;⇩S a"
by (simp add: foldr_compat_dist map_lcomp_def)
lemma map_lcomp_Vars_is_lens [simp]: "vwb_lens a ⟹ ⨆⇩S (map_lcomp Vars a) = ⟦a⟧⇩∼"
by (metis map_lcomp_dist scene_comp_top_scene scene_space_compats top_scene_eq)
lemma set_map_lcomp [simp]: "set (map_lcomp xs a) = (λx. x ;⇩S a) ` set xs"
by (simp add: map_lcomp_def)
subsection ‹ Instances ›
instantiation unit :: scene_space
begin
definition Vars_unit :: "unit scene list" where [simp]: "Vars_unit = []"
instance
by (intro_classes, simp_all add: scene_indeps_def scene_span_def unit_scene_top_eq_bot)
end
instantiation prod :: (scene_space, scene_space) scene_space
begin
definition Vars_prod :: "('a × 'b) scene list" where "Vars_prod = map_lcomp Vars fst⇩L @ map_lcomp Vars snd⇩L"
instance proof
have pw: "pairwise (⨝⇩S) (set (map_lcomp Vars fst⇩L @ map_lcomp Vars snd⇩L))"
by (auto simp add: pairwise_def Vars_ext_lens_indep scene_comp_pres_indep scene_indep_sym)
show "⋀x:: ('a × 'b) scene. x ∈ set Vars ⟹ idem_scene x"
by (auto simp add: Vars_prod_def)
from pw show "scene_indeps (set (Vars :: ('a × 'b) scene list))"
by (simp add: Vars_prod_def scene_indeps_def)
show "scene_span (Vars :: ('a × 'b) scene list)"
by (simp only: scene_span_def Vars_prod_def foldr_scene_append pw pairwise_indep_then_compat map_lcomp_Vars_is_lens fst_vwb_lens snd_vwb_lens)
(metis fst_vwb_lens lens_plus_scene lens_scene_top_iff_bij_lens plus_mwb_lens scene_union_commute snd_fst_lens_indep snd_vwb_lens swap_bij_lens vwb_lens_mwb)
qed
end
subsection ‹ Scene space and basis lenses ›
locale var_lens = vwb_lens +
assumes lens_in_scene_space: "⟦x⟧⇩∼ ∈ scene_space"
declare var_lens.lens_in_scene_space [simp]
declare var_lens.axioms(1) [simp]
locale basis_lens = vwb_lens +
assumes lens_in_basis: "⟦x⟧⇩∼ ∈ set Vars"
sublocale basis_lens ⊆ var_lens
using lens_in_basis var_lens_axioms_def var_lens_def vwb_lens_axioms by blast
declare basis_lens.lens_in_basis [simp]
text ‹ Effectual variable and basis lenses need to have at least two view elements ›
abbreviation (input) evar_lens :: "('a::two ⟹ 's::scene_space) ⇒ bool"
where "evar_lens ≡ var_lens"
abbreviation (input) ebasis_lens :: "('a::two ⟹ 's::scene_space) ⇒ bool"
where "ebasis_lens ≡ basis_lens"
lemma basis_then_var [simp]: "basis_lens x ⟹ var_lens x"
using basis_lens.lens_in_basis basis_lens_def var_lens_axioms_def var_lens_def by blast
lemma basis_lens_intro: "⟦ vwb_lens x; ⟦x⟧⇩∼ ∈ set Vars ⟧ ⟹ basis_lens x"
using basis_lens.intro basis_lens_axioms.intro by blast
subsection ‹ Composite lenses ›
locale composite_lens = vwb_lens +
assumes comp_in_Vars: "(λ a. a ;⇩S x) ` set Vars ⊆ set Vars"
begin
lemma Vars_closed_comp: "a ∈ set Vars ⟹ a ;⇩S x ∈ set Vars"
using comp_in_Vars by blast
lemma scene_space_closed_comp:
assumes "a ∈ scene_space"
shows "a ;⇩S x ∈ scene_space"
proof -
obtain xs where xs: "a = ⨆⇩S xs" "set xs ⊆ set Vars"
using assms scene_space_vars_decomp by blast
have "(⨆⇩S xs) ;⇩S x = ⨆⇩S (map (λ a. a ;⇩S x) xs)"
by (metis foldr_compat_dist pairwise_subset scene_space_compats xs(2))
also have "... ∈ scene_space"
by (auto simp add: scene_space_vars_decomp_iff)
(metis comp_in_Vars image_Un le_iff_sup le_supE list.set_map xs(2))
finally show ?thesis
by (simp add: xs)
qed
sublocale var_lens
proof
show "⟦x⟧⇩∼ ∈ scene_space"
by (metis scene_comp_top_scene scene_space_closed_comp top_scene_space vwb_lens_axioms)
qed
end
lemma composite_implies_var_lens [simp]:
"composite_lens x ⟹ var_lens x"
by (metis composite_lens.axioms(1) composite_lens.scene_space_closed_comp scene_comp_top_scene top_scene_space var_lens_axioms.intro var_lens_def)
text ‹ The extension of any lens in the scene space remains in the scene space ›
lemma composite_lens_comp [simp]:
"⟦ composite_lens a; var_lens x ⟧ ⟹ var_lens (x ;⇩L a)"
by (metis comp_vwb_lens composite_lens.scene_space_closed_comp composite_lens_def lens_scene_comp var_lens_axioms_def var_lens_def)
lemma comp_composite_lens [simp]:
"⟦ composite_lens a; composite_lens x ⟧ ⟹ composite_lens (x ;⇩L a)"
by (auto intro!: composite_lens.intro simp add: composite_lens_axioms_def)
(metis composite_lens.Vars_closed_comp composite_lens.axioms(1) scene_comp_assoc)
text ‹ A basis lens within a composite lens remains a basis lens (i.e. it remains atomic) ›
lemma composite_lens_basis_comp [simp]:
"⟦ composite_lens a; basis_lens x ⟧ ⟹ basis_lens (x ;⇩L a)"
by (metis basis_lens.lens_in_basis basis_lens_def basis_lens_intro comp_vwb_lens composite_lens.Vars_closed_comp composite_lens_def lens_scene_comp)
lemma id_composite_lens: "composite_lens 1⇩L"
by (force intro: composite_lens.intro composite_lens_axioms.intro)
lemma fst_composite_lens: "composite_lens fst⇩L"
by (rule composite_lens.intro, simp add: fst_vwb_lens, rule composite_lens_axioms.intro, simp add: Vars_prod_def)
lemma snd_composite_lens: "composite_lens snd⇩L"
by (rule composite_lens.intro, simp add: snd_vwb_lens, rule composite_lens_axioms.intro, simp add: Vars_prod_def)
end