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);  aset 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);  xset 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 "bset (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;  bset 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 fstL @ map_lcomp Vars sndL"

instance proof
  have pw: "pairwise (⨝S) (set (map_lcomp Vars fstL @ map_lcomp Vars sndL))"
    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 1L"
  by (force intro: composite_lens.intro composite_lens_axioms.intro)

lemma fst_composite_lens: "composite_lens fstL"
  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 sndL"
  by (rule composite_lens.intro, simp add: snd_vwb_lens, rule composite_lens_axioms.intro, simp add: Vars_prod_def)

end