Theory Preliminaries

section ‹Preliminaries›

(*<*)
theory Preliminaries
imports "List-Index.List_Index"
begin
(*>*)

subsection ‹Iterated Function Update›

abbreviation fun_upds ("_[_ :=* _]" [90, 0, 0] 91) where
  "f[xs :=* ys]  fold (λ(x, y) f. f(x := y)) (zip xs ys) f"

fun restrict where
  "restrict A (x # xs) (y # ys) = (if x  A then y # restrict (A - {x}) xs ys else restrict A xs ys)"
| "restrict A _ _ = []"

fun extend :: "nat set  nat list  'a list  'a list set" where
  "extend A (x # xs) ys = (if x  A
     then (zs  extend (A - {x}) xs (tl ys). {hd ys # zs})
     else (z  UNIV. zs  extend A xs ys. {z # zs}))"
| "extend A _ _ = {[]}"

fun lookup where
  "lookup (x # xs) (y # ys) z = (if x = z then y else lookup xs ys z)"
| "lookup _ _ _ = undefined"

lemma extend_nonempty: "extend A xs ys  {}"
  by (induct xs arbitrary: A ys) auto

lemma length_extend: "zs  extend A xs ys  length zs = length xs"
  by (induct xs arbitrary: A ys zs) (auto split: if_splits)

lemma ex_lookup_extend: "x  A  x  set xs  zs  extend A xs ys. lookup xs zs x = d"
proof (induct xs arbitrary: A ys)
  case (Cons a xs)
  from Cons(1)[of "A - {a}" "tl ys"] Cons(1)[of A ys] Cons(2-) show ?case
    by (auto simp: ex_in_conv extend_nonempty)
qed simp

lemma restrict_extend: "A  set xs  length ys = card A  zs  extend A xs ys  restrict A xs zs = ys"
proof (induct xs arbitrary: A ys zs)
  case (Cons a xs)
  then have "finite A"
    by (elim finite_subset) auto
  with Cons(1)[of "A - {a}" "tl ys" "tl zs"] Cons(1)[of A ys "tl zs"] Cons(2-) show ?case
    by (cases ys) (auto simp: subset_insert_iff split: if_splits)
qed simp

lemma fun_upds_notin[simp]: "length xs = length ys  x  set xs  (σ[xs :=* ys]) x = σ x"
  by (induct xs ys arbitrary: σ rule: list_induct2) auto

lemma fun_upds_twist: "length xs = length ys  a  set xs  σ(a := x)[xs :=* ys] = (σ[xs :=* ys])(a := x)"
  by (induct xs ys arbitrary: σ rule: list_induct2) (auto simp: fun_upd_twist)

lemma fun_upds_twist_apply: "length xs = length ys  a  set xs  a  b  (σ(a := x)[xs :=* ys]) b = (σ[xs :=* ys]) b"
  by (induct xs ys arbitrary: σ rule: list_induct2) (auto simp: fun_upd_twist)

lemma fun_upds_extend:
  "x  A  A  set xs  distinct xs  sorted xs  length ys = card A  zs  extend A xs ys 
    (σ[xs :=* zs]) x = (σ[sorted_list_of_set A :=* ys]) x"
proof (induct xs arbitrary: A ys zs σ)
  case (Cons a xs)
  then have fin[simp]: "finite A"
    by (elim finite_subset) auto
  from Cons(2-) have "a  A  Min A = a" if "a  A"
    by (intro Min_eqI) auto
  with Cons(2) fin have *: "a  A  sorted_list_of_set A = a # sorted_list_of_set (A - {a})"
    by (subst sorted_list_of_set_nonempty) auto
  show ?case
    using Cons(1)[of "A - {a}" "tl ys"] Cons(1)[of A ys] Cons(2-)
    by (cases ys; cases "x = a")
      (auto simp add: subset_insert_iff * fun_upds_twist_apply length_extend simp del: fun_upd_apply split: if_splits)
qed simp

lemma fun_upds_map_self: "σ[xs :=* map σ xs] = σ"
  by (induct xs arbitrary: σ) auto

lemma fun_upds_single: "distinct xs  σ[xs :=* map (σ(y := d)) xs] = (if y  set xs then σ(y := d) else σ)"
  by (induct xs arbitrary: σ) (auto simp: fun_upds_twist)

subsection ‹Lists and Sets›

lemma find_index_less_size: "x  set xs. P x  find_index P xs < size xs"
  by (induct xs) auto

lemma index_less_size: "x  set xs  index xs x < size xs"
  by (simp add: index_def find_index_less_size)

lemma fun_upds_in: "length xs = length ys  distinct xs  x  set xs  (σ[xs :=* ys]) x = ys ! index xs x"
  by (induct xs ys arbitrary: σ rule: list_induct2) auto

lemma remove_nth_index: "remove_nth (index ys y) ys = remove1 y ys"
  by (induct ys) auto

lemma index_remove_nth: "distinct xs  x  set xs  index (remove_nth i xs) x = (if index xs x < i then index xs x else if i = index xs x then length xs - 1 else index xs x - 1)"
  by (induct i xs rule: remove_nth.induct) (auto simp: not_less intro!: Suc_pred split: if_splits)

lemma insert_nth_nth_index:
  "y  z  y  set ys  z  set ys  length ys = Suc (length xs)  distinct ys 
  insert_nth (index ys y) x xs ! index ys z =
  xs ! index (remove1 y ys) z"
  by (subst nth_insert_nth;
      auto simp: remove_nth_index[symmetric] index_remove_nth dest: index_less_size intro!: arg_cong[of _ _ "nth xs"] index_eqI)

lemma index_lt_index_remove: "index xs x < index xs y  index xs x = index (remove1 y xs) x"
  by (induct xs) auto

lemma index_gt_index_remove: "index xs x > index xs y  index xs x = Suc (index (remove1 y xs) x)"
proof (induct xs)
  case (Cons z xs)
  then show ?case
    by (cases "z = x") auto
qed simp

lemma lookup_map[simp]: "x  set xs  lookup xs (map f xs) x = f x"
  by (induct xs) auto

lemma in_set_remove_cases: "P z  (x  set (remove1 z xs). P x)  x  set xs  P x"
  by (cases "x = z") auto

lemma insert_remove_id: "x  X  X = insert x (X - {x})"
  by auto

lemma infinite_surj: "infinite A  A  f ` B  infinite B"
  by (elim contrapos_nn finite_surj)

class infinite =
  fixes to_nat :: "'a  nat"
  assumes surj_to_nat: "surj to_nat"
begin

lemma infinite_UNIV: "infinite (UNIV :: 'a set)"
  using surj_to_nat by (intro infinite_surj[of UNIV to_nat]) auto

end

instantiation nat :: infinite begin
definition to_nat_nat :: "nat  nat" where "to_nat_nat = id"
instance by standard (auto simp: to_nat_nat_def)
end

instantiation list :: (type) infinite begin
definition to_nat_list :: "'a list  nat" where "to_nat_list = length"
instance by standard (auto simp: image_iff to_nat_list_def intro!: exI[of _ "replicate _ _"])
end

subsection ‹Equivalence Closure and Classes›

definition symcl where
  "symcl r = {(x, y). (x, y)  r  (y, x)  r}"

definition transymcl where
  "transymcl r = trancl (symcl r)"

lemma symclp_symcl_eq[pred_set_conv]: "symclp (λx y. (x, y)  r) = (λx y. (x, y)  symcl r)"
  by (auto simp: symclp_def symcl_def fun_eq_iff)

definition "classes Qeq = quotient (Field Qeq) (transymcl Qeq)"

lemma Field_symcl[simp]: "Field (symcl r) = Field r"
  unfolding symcl_def Field_def by auto

lemma Domain_symcl[simp]: "Domain (symcl r) = Field r"
  unfolding symcl_def Field_def by auto

lemma Field_trancl[simp]: "Field (trancl r) = Field r"
  unfolding Field_def by auto

lemma Field_transymcl[simp]: "Field (transymcl r) = Field r"
  unfolding transymcl_def by auto

lemma eqclass_empty_iff[simp]: "r `` {x} = {}  x  Domain r"
  by auto

lemma sym_symcl[simp]: "sym (symcl r)"
  unfolding symcl_def sym_def by auto

lemma in_symclI:
  "(a,b)  r  (a,b)  symcl r"
  "(a,b)  r  (b,a)  symcl r"
  by (auto simp: symcl_def)

lemma sym_transymcl: "sym (transymcl r)"
  by (simp add: sym_trancl transymcl_def)

lemma symcl_insert:
  "symcl (insert (x, y) Qeq) = insert (y, x) (insert (x, y) (symcl Qeq))"
  by (auto simp: symcl_def)

lemma equiv_transymcl: "Equiv_Relations.equiv (Field Qeq) (transymcl Qeq)"
  by (auto simp: Equiv_Relations.equiv_def sym_trancl refl_on_def transymcl_def
    dest: FieldI1 FieldI2 Field_def[THEN equalityD1, THEN set_mp]
    intro: r_r_into_trancl[of x _ _ x for x]  elim!: in_symclI)

lemma equiv_quotient_no_empty_class: "Equiv_Relations.equiv A r  {}  A // r"
  by (auto simp: quotient_def refl_on_def sym_def Equiv_Relations.equiv_def)

lemma classes_cover: "(classes Qeq) = Field Qeq"
  by (simp add: Union_quotient classes_def equiv_transymcl)

lemma classes_disjoint: "X  classes Qeq  Y  classes Qeq  X = Y  X  Y = {}"
  using quotient_disj[OF equiv_transymcl]
  by (auto simp: classes_def)

lemma classes_nonempty: "{}  classes Qeq"
  using equiv_quotient_no_empty_class[OF equiv_transymcl]
  by (auto simp: classes_def)

definition "class x Qeq = (if X  classes Qeq. x  X then Some (THE X. X  classes Qeq  x  X) else None)"

lemma class_Some_eq: "class x Qeq = Some X  X  classes Qeq  x  X"
  unfolding class_def
  by (auto 0 3 dest: classes_disjoint del: conjI intro!: the_equality[of _ X]
   conjI[of "(Xclasses Qeq. x  X)"] intro: theI[where P="λX. X  classes Qeq  x  X"])

lemma class_None_eq: "class x Qeq = None  x  Field Qeq"
  by (simp add: class_def classes_cover[symmetric] split: if_splits)

lemma insert_Image_triv: "x  r  insert (x, y) Qeq `` r = Qeq `` r"
  by auto

lemma Un1_Image_triv: "Domain B  r = {}  (A  B) `` r = A `` r"
  by auto

lemma Un2_Image_triv: "Domain A  r = {}  (A  B) `` r = B `` r"
  by auto

lemma classes_empty: "classes {} = {}"
  unfolding classes_def by auto

lemma ex_class: "x  Field Qeq  X. class x Qeq = Some X  x  X"
  by (metis Union_iff class_Some_eq classes_cover)

lemma equivD:
  "Equiv_Relations.equiv A r  refl_on A r"
  "Equiv_Relations.equiv A r  sym r"
  "Equiv_Relations.equiv A r  trans r"
  by (blast elim: Equiv_Relations.equivE)+

lemma transymcl_into:
  "(x, y)  r  (x, y)  transymcl r"
  "(x, y)  r  (y, x)  transymcl r"
  unfolding transymcl_def by (blast intro: in_symclI r_into_trancl')+

lemma transymcl_self:
  "(x, y)  r  (x, x)  transymcl r"
  "(x, y)  r  (y, y)  transymcl r"
  unfolding transymcl_def by (blast intro: in_symclI(1) in_symclI(2) r_r_into_trancl)+

lemma transymcl_trans: "(x, y)  transymcl r  (y, z)  transymcl r  (x, z)  transymcl r"
  using equiv_transymcl[THEN equivD(3), THEN transD] .

lemma transymcl_sym: "(x, y)  transymcl r  (y, x)  transymcl r"
  using equiv_transymcl[THEN equivD(2), THEN symD] .

lemma edge_same_class: "X  classes Qeq  (a, b)  Qeq  a  X  b  X"
  unfolding classes_def by (elim quotientE) (auto elim!: transymcl_trans transymcl_into)

lemma Field_transymcl_self: "a  Field Qeq  (a, a)  transymcl Qeq"
  by (auto simp: Field_def transymcl_def[symmetric] transymcl_self)

lemma transymcl_insert: "transymcl (insert (a, b) Qeq) = transymcl Qeq  {(a,a),(b,b)} 
   ((transymcl Qeq  {(a, a), (b, b)}) O {(a, b), (b, a)} O (transymcl Qeq  {(a, a), (b, b)}) - transymcl Qeq)"
  by (auto simp: relcomp_def relcompp_apply transymcl_def symcl_insert trancl_insert2 dest: trancl_trans)

lemma transymcl_insert_both_new: "a  Field Qeq  b  Field Qeq 
  transymcl (insert (a, b) Qeq) = transymcl Qeq  {(a,a),(b,b),(a,b),(b,a)}"
  unfolding transymcl_insert
  by (auto dest: FieldI1 FieldI2)

lemma transymcl_insert_same_class: "(x, y)  transymcl Qeq  transymcl (insert (x, y) Qeq) = transymcl Qeq"
  by (auto 0 3 simp: transymcl_insert intro: transymcl_sym transymcl_trans)

lemma classes_insert: "classes (insert (x, y) Qeq) =
  (case (class x Qeq, class y Qeq) of
    (Some X, Some Y)  if X = Y then classes Qeq else classes Qeq - {X, Y}  {X  Y}
  | (Some X, None)  classes Qeq - {X}  {insert y X}
  | (None, Some Y)  classes Qeq - {Y}  {insert x Y}
  | (None, None)  classes Qeq  {{x,y}})"
proof ((cases "class x Qeq"; cases "class y Qeq"), goal_cases NN NS SN SS)
  case NN
  then have "classes (insert (x, y) Qeq) = classes Qeq  {{x, y}}"
    by (fastforce simp: class_None_eq classes_def transymcl_insert_both_new insert_Image_triv quotientI
      elim!: quotientE dest: FieldI1  intro: quotient_def[THEN Set.equalityD2, THEN set_mp] intro!: disjI1)
  with NN show ?case
    by auto
next
  case (NS Y)
  then have "insert x Y = transymcl (insert (x, y) Qeq) `` {x}"
    unfolding transymcl_insert using FieldI1[of x _ "transymcl Qeq"]
    relcompI[OF insertI1 relcompI[OF insertI1 insertI2[OF insertI2[OF transymcl_trans[OF transymcl_sym]]]],
      of _ y Qeq _ x x "insert (y,y) (transymcl Qeq)" "{(y,x)}" "(x, x)" "(y, y)"]
    by (auto simp: class_None_eq class_Some_eq classes_def
      dest: FieldI1 FieldI2 elim!: quotientE intro: transymcl_sym transymcl_trans)
  then have *: "insert x Y  classes (insert (x, y) Qeq)"
    by (auto simp: class_None_eq class_Some_eq classes_def  intro!: quotientI)
  moreover from * NS have "Y  classes (insert (x, y) Qeq)"
    using classes_disjoint[of Y "insert (x, y) Qeq" "insert x Y"] classes_cover[of Qeq]
    by (auto simp: class_None_eq class_Some_eq)
  moreover {
    fix Z
    assume Z: "Z  Y" "Z  classes Qeq"
    then obtain z where z: "z  Field Qeq" "Z = transymcl Qeq `` {z}"
      by (auto elim!: quotientE simp: classes_def)
    with NS Z have "z  Z" "z  x" "z  y" "(z, x)  transymcl Qeq" "(z, y)  transymcl Qeq"
      using classes_disjoint[of Z "Qeq" Y] classes_nonempty[of Qeq]
      by (auto simp: class_None_eq class_Some_eq disjoint_iff Field_transymcl_self
        dest: FieldI2 intro: transymcl_trans)
    with NS Z * have "transymcl Qeq `` {z} = transymcl (insert (x, y) Qeq) `` {z}"
      unfolding transymcl_insert
      by (intro trans[OF _ Un1_Image_triv[symmetric]]) (auto simp: class_None_eq class_Some_eq)
    with z have "Z  classes (insert (x, y) Qeq)"
      by (auto simp: classes_def intro!: quotientI)
  }
  moreover {
    fix Z
    assume Z: "Z  insert x Y" "Z  classes (insert (x, y) Qeq)"
    then obtain z where z: "z  Field (insert (x, y) Qeq)" "Z = transymcl (insert (x, y) Qeq) `` {z}"
      by (auto elim!: quotientE simp: classes_def)
    with NS Z * have "z  Z" "z  x" "z  y" "(z, x)  transymcl (insert (x, y) Qeq)" "(z, y)  transymcl (insert (x, y) Qeq)"
      using classes_disjoint[of Z "insert (x, y) Qeq" "insert x Y"] classes_nonempty[of "insert (x, y) Qeq"]
      by (auto simp: class_None_eq class_Some_eq Field_transymcl_self transymcl_into(2)
        intro: transymcl_trans)
    with NS Z * have "transymcl (insert (x, y) Qeq) `` {z} = transymcl Qeq `` {z}"
      unfolding transymcl_insert
      by (intro trans[OF Un1_Image_triv]) (auto simp: class_None_eq class_Some_eq)
    with z z  x z  y have "Z  classes Qeq"
      by (auto simp: classes_def intro!: quotientI)
  }
  ultimately have "classes (insert (x, y) Qeq) = classes Qeq - {Y}  {insert x Y}"
    by blast
  with NS show ?case
    by auto
next
  case (SN X)
  then have "insert y X = transymcl (insert (x, y) Qeq) `` {x}"
    unfolding transymcl_insert using FieldI1[of x _ "transymcl Qeq"]
    by (auto simp: class_None_eq class_Some_eq classes_def
      dest: FieldI1 FieldI2 elim!: quotientE intro: transymcl_sym transymcl_trans)
  then have *: "insert y X  classes (insert (x, y) Qeq)"
    by (auto simp: class_None_eq class_Some_eq classes_def  intro!: quotientI)
  moreover from * SN have "X  classes (insert (x, y) Qeq)"
    using classes_disjoint[of X "insert (x, y) Qeq" "insert y X"] classes_cover[of Qeq]
    by (auto simp: class_None_eq class_Some_eq)
  moreover {
    fix Z
    assume Z: "Z  X" "Z  classes Qeq"
    then obtain z where z: "z  Field Qeq" "Z = transymcl Qeq `` {z}"
      by (auto elim!: quotientE simp: classes_def)
    with SN Z have "z  Z" "z  x" "z  y" "(z, x)  transymcl Qeq" "(z, y)  transymcl Qeq"
      using classes_disjoint[of Z "Qeq" X] classes_nonempty[of Qeq]
      by (auto simp: class_None_eq class_Some_eq disjoint_iff Field_transymcl_self
        dest: FieldI2 intro: transymcl_trans)
    with SN Z * have "transymcl Qeq `` {z} = transymcl (insert (x, y) Qeq) `` {z}"
      unfolding transymcl_insert
      by (intro trans[OF _ Un1_Image_triv[symmetric]]) (auto simp: class_None_eq class_Some_eq)
    with z have "Z  classes (insert (x, y) Qeq)"
      by (auto simp: classes_def intro!: quotientI)
  }
  moreover {
    fix Z
    assume Z: "Z  insert y X" "Z  classes (insert (x, y) Qeq)"
    then obtain z where z: "z  Field (insert (x, y) Qeq)" "Z = transymcl (insert (x, y) Qeq) `` {z}"
      by (auto elim!: quotientE simp: classes_def)
    with SN Z * have "z  Z" "z  x" "z  y" "(z, x)  transymcl (insert (x, y) Qeq)" "(z, y)  transymcl (insert (x, y) Qeq)"
      using classes_disjoint[of Z "insert (x, y) Qeq" "insert y X"] classes_nonempty[of "insert (x, y) Qeq"]
      by (auto simp: class_None_eq class_Some_eq Field_transymcl_self transymcl_into(2)
        intro: transymcl_trans)
    with SN Z * have "transymcl (insert (x, y) Qeq) `` {z} = transymcl Qeq `` {z}"
      unfolding transymcl_insert
      by (intro trans[OF Un1_Image_triv]) (auto simp: class_None_eq class_Some_eq)
    with z z  x z  y have "Z  classes Qeq"
      by (auto simp: classes_def intro!: quotientI)
  }
  ultimately have "classes (insert (x, y) Qeq) = classes Qeq - {X}  {insert y X}"
    by blast
  with SN show ?case
    by auto
next
  case (SS X Y)
  moreover from SS have XY: "X  classes Qeq" "Y  classes Qeq" "x  X" "y  Y" "x  Field Qeq" "y  Field Qeq"
    using class_None_eq[of x Qeq] class_None_eq[of y Qeq] class_Some_eq[of x Qeq X] class_Some_eq[of y Qeq Y]
    by auto
  moreover from XY have "X = Y  classes (insert (x, y) Qeq) = classes Qeq"
    unfolding classes_def
    by (subst transymcl_insert_same_class)
      (auto simp: classes_def insert_absorb elim!: quotientE intro: transymcl_sym transymcl_trans)
  moreover
  {
    assume neq: "X  Y"
    from XY have "X = transymcl Qeq `` {x}" "Y = transymcl Qeq `` {y}"
      by (auto simp: classes_def elim!: quotientE intro: transymcl_sym transymcl_trans)
    with XY have XY_eq:
      "X  Y = transymcl (insert (x, y) Qeq) `` {x}" 
      "X  Y = transymcl (insert (x, y) Qeq) `` {y}"
      unfolding transymcl_insert by auto
    then have *: "X  Y  classes (insert (x, y) Qeq)"
      by (auto simp: classes_def quotientI)
    moreover
    from * XY neq have **: "X  classes (insert (x, y) Qeq)" "Y  classes (insert (x, y) Qeq)"
      using classes_disjoint[OF *, of X] classes_disjoint[OF *, of Y] classes_disjoint[of X Qeq Y]
      by auto
    moreover {
      fix Z
      assume Z: "Z  X" "Z  Y" "Z  classes Qeq"
      then obtain z where z: "z  Field Qeq" "Z = transymcl Qeq `` {z}"
        by (auto elim!: quotientE simp: classes_def)
      with XY Z have "z  Z" "z  x" "z  y" "(z, x)  transymcl Qeq" "(z, y)  transymcl Qeq"
        using classes_disjoint[of Z Qeq X] classes_disjoint[of Z Qeq Y] classes_nonempty[of Qeq]
        by (auto simp: disjoint_iff Field_transymcl_self dest: FieldI2 intro: transymcl_trans)
      with XY Z * have "transymcl Qeq `` {z} = transymcl (insert (x, y) Qeq) `` {z}"
        unfolding transymcl_insert
        by (intro trans[OF _ Un1_Image_triv[symmetric]]) (auto simp: class_None_eq class_Some_eq)
      with z have "Z  classes (insert (x, y) Qeq)"
        by (auto simp: classes_def intro!: quotientI)
    }
    moreover {
      fix Z
      assume Z: "Z  X  Y" "Z  classes (insert (x, y) Qeq)"
      then obtain z where z: "z  Field (insert (x, y) Qeq)" "Z = transymcl (insert (x, y) Qeq) `` {z}"
        by (auto elim!: quotientE simp: classes_def)
      with XY Z neq XY_eq have "z  Z" "z  x" "z  y" "(z, x)  transymcl (insert (x, y) Qeq)" "(z, y)  transymcl (insert (x, y) Qeq)"
        using classes_disjoint[OF *, of Z] classes_disjoint[of X Qeq Y]
        by (auto simp: Field_transymcl_self)
      with XY Z * have "transymcl (insert (x, y) Qeq) `` {z} = transymcl Qeq `` {z}"
        unfolding transymcl_insert
        by (intro trans[OF Un1_Image_triv]) (auto simp: class_None_eq class_Some_eq)
      with z z  x z  y have "Z  classes Qeq"
        by (auto simp: classes_def intro!: quotientI)
    }
    ultimately have "classes (insert (x, y) Qeq) = classes Qeq - {X, Y}  {X  Y}"
      by blast
  }
  ultimately show ?case
    by auto
qed

lemma classes_intersect_find_not_None:
  assumes "Vclasses (set xys). V  A  {}" "xys  []"
  shows "find (λ(x, y). x  A  y  A) xys  None"
proof -
  from assms(2) obtain x y where "(x, y)  set xys" by (cases xys) auto
  with assms(1) obtain X where x: "class x (set xys) = Some X" "X  A  {}"
    using ex_class[of "x" "set xys"]
    by (auto simp: class_Some_eq Field_def)
  then obtain a where "a  A" "a  X"
    by blast
  with x have "(a, x)  transymcl (set xys)"
    using equiv_class_eq[OF equiv_transymcl, of _ _ "set xys"]
    by (fastforce simp: class_Some_eq classes_def elim!: quotientE)
  then obtain b where "(a, b)  symcl (set xys)"
    by (auto simp: transymcl_def elim: converse_tranclE)
  with a  A show ?thesis
    by (auto simp: find_None_iff symcl_def)
qed

(*<*)
end
(*>*)