Theory PlaneGraphIso

(*  Author: Tobias Nipkow  *)

section‹Isomorphisms Between Plane Graphs›

theory PlaneGraphIso
imports Main Quasi_Order
begin

(* FIXME globalize *)
lemma image_image_id_if[simp]: "(⋀x. f(f x) = x) ⟹ f ` f ` M = M"
by (auto simp: image_iff)


declare not_None_eq [iff] not_Some_eq [iff]


text‹The symbols ‹≅› and ‹≃› are overloaded.  They
denote congruence and isomorphism on arbitrary types. On lists
(representing faces of graphs), ‹≅› means congruence modulo
rotation; ‹≃› is currently unused. On graphs, ‹≃›
means isomorphism and is a weaker version of ‹≅› (proper
isomorphism): ‹≃› also allows to reverse the orientation of
all faces.›

consts
 pr_isomorphic  :: "'a ⇒ 'a ⇒ bool" (infix "≅" 60)
(* isomorphic :: "'a ⇒ 'a ⇒ bool" (infix "≃" 60)
*)
(*
definition "congs"  :: "'a list ⇒ 'a list ⇒ bool" (infix "≅" 60) where
 "F⇩1 ≅ (F⇩2::'a list) ≡ ∃n. F⇩2 = rotate n F⇩1"
*)
definition Iso :: "('a list * 'a list) set" ("{≅}") where
 "{≅} ≡ {(F⇩1, F⇩2). F⇩1 ≅ F⇩2}"

lemma [iff]: "((x,y) ∈ {≅}) = x ≅ y"
by(simp add:Iso_def)

text‹A plane graph is a set or list (for executability) of faces
(hence ‹Fgraph› and ‹fgraph›) and a face is a list of
nodes:›

type_synonym 'a Fgraph = "'a list set"
type_synonym 'a fgraph = "'a list list"

subsection‹Equivalence of faces›

text‹Two faces are equivalent modulo rotation:›

overloading "congs" ≡ "pr_isomorphic :: 'a list ⇒ 'a list ⇒ bool"
begin
  definition "F⇩1 ≅ (F⇩2::'a list) ≡ ∃n. F⇩2 = rotate n F⇩1"
end

lemma congs_refl[iff]: "(xs::'a list) ≅ xs"
apply(simp add:congs_def)
apply(rule_tac x = 0 in exI)
apply (simp)
done

lemma congs_sym: assumes A: "(xs::'a list) ≅ ys" shows "ys ≅ xs"
proof (simp add:congs_def)
  let ?l = "length xs"
  from A obtain n where ys: "ys = rotate n xs" by(fastforce simp add:congs_def)
  have "xs = rotate ?l xs" by simp
  also have "… = rotate (?l - n mod ?l + n mod ?l) xs"
  proof (cases)
    assume "xs = []" thus ?thesis by simp
  next
    assume "xs ≠ []"
    hence "n mod ?l < ?l" by simp
    hence "?l = ?l - n mod ?l + n mod ?l" by arith
    thus ?thesis by simp
  qed
  also have "… = rotate (?l - n mod ?l) (rotate (n mod ?l) xs)"
    by(simp add:rotate_rotate)
  also have "rotate (n mod ?l) xs = rotate n xs"
    by(rule rotate_conv_mod[symmetric])
  finally show "∃m. xs = rotate m ys" by(fastforce simp add:ys)
qed

lemma congs_trans: "(xs::'a list) ≅ ys ⟹ ys ≅ zs ⟹ xs ≅ zs"
apply(clarsimp simp:congs_def rotate_def)
apply(rename_tac m n)
apply(rule_tac x = "n+m" in exI)
apply (simp add:funpow_add)
done

lemma equiv_EqF: "equiv (UNIV::'a list set) {≅}"
apply(unfold equiv_def sym_def trans_def refl_on_def)
apply(rule conjI)
 apply simp
apply(rule conjI)
 apply(fastforce intro:congs_sym)
apply(fastforce intro:congs_trans)
done

lemma congs_distinct:
  "F⇩1 ≅ F⇩2 ⟹ distinct F⇩2 = distinct F⇩1"
by (auto simp: congs_def)

lemma congs_length:
  "F⇩1 ≅ F⇩2 ⟹ length F⇩2 = length F⇩1"
by (auto simp: congs_def)

lemma congs_pres_nodes: "F⇩1 ≅ F⇩2 ⟹ set F⇩1 = set F⇩2"
by(clarsimp simp:congs_def)

lemma congs_map:
  "F⇩1 ≅ F⇩2 ⟹ map f F⇩1 ≅ map f F⇩2"
by (auto simp: congs_def rotate_map)

lemma congs_map_eq_iff:
 "inj_on f (set xs ∪ set ys) ⟹ (map f xs ≅ map f ys) = (xs ≅ ys)"
apply(simp add:congs_def)
apply(rule iffI)
 apply(clarsimp simp: rotate_map)
 apply(drule map_inj_on)
  apply(simp add:Un_commute)
 apply (fastforce)
apply clarsimp
apply(fastforce simp: rotate_map)
done


lemma list_cong_rev_iff[simp]:
  "(rev xs ≅ rev ys) = (xs ≅ ys)"
apply(simp add:congs_def rotate_rev)
apply(rule iffI)
 apply fast
apply clarify
apply(cases "length xs = 0")
 apply simp
apply(case_tac "n mod length xs = 0")
 apply(rule_tac x = "n" in exI)
 apply simp
apply(subst rotate_conv_mod)
apply(rule_tac x = "length xs - n mod length xs" in exI)
apply simp
done


lemma singleton_list_cong_eq_iff[simp]:
  "({xs::'a list} // {≅} = {ys} // {≅}) = (xs ≅ ys)"
by(simp add: eq_equiv_class_iff2[OF equiv_EqF])


subsection‹Homomorphism and isomorphism›

definition is_pr_Hom :: "('a ⇒ 'b) ⇒ 'a Fgraph ⇒ 'b Fgraph ⇒ bool" where
"is_pr_Hom φ Fs⇩1 Fs⇩2 ≡ (map φ ` Fs⇩1)//{≅} = Fs⇩2 //{≅}"

definition is_pr_Iso :: "('a ⇒ 'b) ⇒ 'a Fgraph ⇒ 'b Fgraph ⇒ bool" where
"is_pr_Iso φ Fs⇩1 Fs⇩2 ≡ is_pr_Hom φ Fs⇩1 Fs⇩2 ∧ inj_on φ (⋃F ∈ Fs⇩1. set F)"

definition is_pr_iso :: "('a ⇒ 'b) ⇒ 'a fgraph ⇒ 'b fgraph ⇒ bool" where
"is_pr_iso φ Fs⇩1 Fs⇩2 ≡ is_pr_Iso φ (set Fs⇩1) (set Fs⇩2)"

text‹Homomorphisms preserve the set of nodes.›

lemma UN_subset_iff: "((⋃i∈I. f i) ⊆ B) = (∀i∈I. f i ⊆ B)"
by blast

declare Image_Collect_case_prod[simp del]

lemma pr_Hom_pres_face_nodes:
 "is_pr_Hom φ Fs⇩1 Fs⇩2 ⟹ (⋃F∈Fs⇩1. {φ ` (set F)}) = (⋃F∈Fs⇩2. {set F})"
supply image_cong_simp [cong del]
apply(clarsimp simp:is_pr_Hom_def quotient_def)
apply auto
apply(subgoal_tac "∃F' ∈ Fs⇩2. {≅} `` {map φ F} = {≅} `` {F'}")
 prefer 2 apply blast
apply (fastforce simp: eq_equiv_class_iff[OF equiv_EqF] dest!:congs_pres_nodes)
apply(subgoal_tac "∃F' ∈ Fs⇩1. {≅} `` {map φ F'} = {≅} `` {F}")
 apply (fastforce simp: eq_equiv_class_iff[OF equiv_EqF] dest!:congs_pres_nodes)
apply (erule equalityE)
apply(fastforce simp:UN_subset_iff)
done

lemma pr_Hom_pres_nodes:
  assumes "is_pr_Hom φ Fs⇩1 Fs⇩2"
  shows "φ ` (⋃F∈Fs⇩1. set F) = (⋃F∈Fs⇩2. set F)"
proof
  from assms have *: "(⋃F∈Fs⇩1. {φ ` set F}) = (⋃F∈Fs⇩2. {set F})"
    by (rule pr_Hom_pres_face_nodes)
  then show "φ ` (⋃F∈Fs⇩1. set F) ⊆ (⋃F∈Fs⇩2. set F)"
    by blast
  show "(⋃F∈Fs⇩2. set F) ⊆ φ ` (⋃F∈Fs⇩1. set F)"
  proof
    fix x
    assume "x ∈ (⋃F∈Fs⇩2. set F)"
    then obtain F where "F ∈ Fs⇩2" and "x ∈ set F" ..
    then have "set F ∈ (⋃F∈Fs⇩2. {set F})"
      by blast
    then have "set F ∈ (⋃F∈Fs⇩1. {φ ` set F})"
      using * by simp
    then obtain F' where "F' ∈ Fs⇩1" and "set F ∈ {φ ` set F'}" ..
    with ‹x ∈ set F› show "x ∈ φ ` (⋃F∈Fs⇩1. set F)"
      by auto
  qed
qed

text‹Therefore isomorphisms preserve cardinality of node set.›

lemma pr_Iso_same_no_nodes:
  "⟦ is_pr_Iso φ Fs⇩1 Fs⇩2; finite Fs⇩1 ⟧
   ⟹ card(⋃F∈Fs⇩1. set F) = card(⋃F∈Fs⇩2. set F)"
by(clarsimp simp add: is_pr_Iso_def pr_Hom_pres_nodes[symmetric] card_image)

lemma pr_iso_same_no_nodes:
  "is_pr_iso φ Fs⇩1 Fs⇩2 ⟹ card(⋃F∈set Fs⇩1. set F) = card(⋃F∈set Fs⇩2. set F)"
by(simp add: is_pr_iso_def pr_Iso_same_no_nodes)

text‹Isomorphisms preserve the number of faces.›

lemma pr_iso_same_no_faces:
  assumes dist1: "distinct Fs⇩1" and dist2: "distinct Fs⇩2"
  and inj1: "inj_on (λxs.{xs}//{≅}) (set Fs⇩1)"
  and inj2: "inj_on (λxs.{xs}//{≅}) (set Fs⇩2)" and iso: "is_pr_iso φ Fs⇩1 Fs⇩2"
  shows "length Fs⇩1 = length Fs⇩2"
proof -
  have injphi: "∀F∈set Fs⇩1. ∀F'∈set Fs⇩1. inj_on φ (set F ∪ set F')" using iso
    by(auto simp:is_pr_iso_def is_pr_Iso_def is_pr_Hom_def inj_on_def)
  have inj1': "inj_on (λxs. {xs} // {≅}) (map φ ` set Fs⇩1)"
    apply(rule inj_on_imageI)
    apply(simp add:inj_on_def quotient_def eq_equiv_class_iff[OF equiv_EqF])
    apply(simp add: congs_map_eq_iff injphi)
    using inj1
    apply(simp add:inj_on_def quotient_def eq_equiv_class_iff[OF equiv_EqF])
    done
  have "length Fs⇩1 = card(set Fs⇩1)" by(simp add:distinct_card[OF dist1])
  also have "… = card(map φ ` set Fs⇩1)" using iso
    by(auto simp:is_pr_iso_def is_pr_Iso_def is_pr_Hom_def inj_on_mapI card_image)
  also have "… = card((map φ ` set Fs⇩1) // {≅})"
    by(simp add: card_quotient_disjoint[OF _ inj1'])
  also have "(map φ ` set Fs⇩1)//{≅} = set Fs⇩2 // {≅}"
    using iso by(simp add: is_pr_iso_def is_pr_Iso_def is_pr_Hom_def)
  also have "card(…) = card(set Fs⇩2)"
    by(simp add: card_quotient_disjoint[OF _ inj2])
  also have "… = length Fs⇩2" by(simp add:distinct_card[OF dist2])
  finally show ?thesis .
qed


lemma is_Hom_distinct:
 "⟦ is_pr_Hom φ Fs⇩1 Fs⇩2; ∀F∈Fs⇩1. distinct F; ∀F∈Fs⇩2. distinct F ⟧
  ⟹ ∀F∈Fs⇩1. distinct(map φ F)"
apply(clarsimp simp add:is_pr_Hom_def)
apply(subgoal_tac "∃ F' ∈ Fs⇩2. (map φ F, F') : {≅}")
 apply(fastforce simp add: congs_def)
apply(subgoal_tac "∃ F' ∈ Fs⇩2. {map φ F}//{≅} = {F'}//{≅}")
 apply clarify
 apply(rule_tac x = F' in bexI)
  apply(rule eq_equiv_class[OF _ equiv_EqF])
   apply(simp add:singleton_quotient)
  apply blast
 apply assumption
apply(simp add:quotient_def)
apply(rotate_tac 1)
apply blast
done


lemma Collect_congs_eq_iff[simp]:
  "Collect ((≅) x) = Collect ((≅) y) ⟷ (x ≅ (y::'a list))"
using eq_equiv_class_iff2[OF equiv_EqF]
apply(simp add: quotient_def Iso_def)
apply blast
done

lemma is_pr_Hom_trans: assumes f: "is_pr_Hom f A B" and g: "is_pr_Hom g B C"
shows "is_pr_Hom (g ∘ f) A C"
proof-
  from f have f1: "∀a∈A. ∃b∈B. map f a ≅ b"
    apply(simp add: is_pr_Hom_def quotient_def Iso_def)
    apply(erule equalityE)
    apply blast
    done
  from f have f2: "∀b∈B. ∃a∈A. map f a ≅ b"
    apply(simp add: is_pr_Hom_def quotient_def Iso_def)
    apply(erule equalityE)
    apply blast
    done
  from g have g1: "∀b∈B. ∃c∈C. map g b ≅ c"
    apply(simp add: is_pr_Hom_def quotient_def Iso_def)
    apply(erule equalityE)
    apply blast
    done
  from g have g2: "∀c∈C. ∃b∈B. map g b ≅ c"
    apply(simp add: is_pr_Hom_def quotient_def Iso_def)
    apply(erule equalityE)
    apply blast
    done
  show ?thesis
    apply(auto simp add: is_pr_Hom_def quotient_def Iso_def Image_def
      map_comp_map[symmetric] image_comp simp del: map_map map_comp_map)
    apply (metis congs_map[of _ _ g] congs_trans f1 g1)
    by (metis congs_map[of _ _ g] congs_sym congs_trans f2 g2)
qed

lemma is_pr_Hom_rev:
  "is_pr_Hom φ A B ⟹ is_pr_Hom φ (rev ` A) (rev ` B)"
apply(auto simp add: is_pr_Hom_def quotient_def Image_def Iso_def rev_map[symmetric])
 apply(erule equalityE)
 apply blast
apply(erule equalityE)
apply blast
done


text‹A kind of recursion rule, a first step towards executability:›

lemma is_pr_Iso_rec:
 "⟦ inj_on (λxs. {xs}//{≅}) Fs⇩1; inj_on (λxs. {xs}//{≅}) Fs⇩2; F⇩1 ∈ Fs⇩1 ⟧ ⟹
 is_pr_Iso φ Fs⇩1 Fs⇩2 =
 (∃F⇩2 ∈ Fs⇩2. length F⇩1 = length F⇩2 ∧ is_pr_Iso φ (Fs⇩1 - {F⇩1}) (Fs⇩2 - {F⇩2})
    ∧ (∃n. map φ F⇩1 = rotate n F⇩2)
    ∧ inj_on φ (⋃F∈Fs⇩1. set F))"
apply(drule mk_disjoint_insert[of F⇩1])
apply clarify
apply(rename_tac Fs⇩1')
apply(rule iffI)

apply (clarsimp simp add:is_pr_Iso_def)
apply(clarsimp simp:is_pr_Hom_def quotient_diff1)
apply(drule_tac s="a // b" for a b in sym)
apply(clarsimp)
apply(subgoal_tac "{≅} `` {map φ F⇩1} : Fs⇩2 // {≅}")
 prefer 2 apply(simp add:quotient_def)
apply(erule quotientE)
apply(rename_tac F⇩2)
apply(drule eq_equiv_class[OF _ equiv_EqF])
 apply blast
apply(rule_tac x = F⇩2 in bexI)
 prefer 2 apply assumption
apply(rule conjI)
 apply(clarsimp simp: congs_def)
apply(rule conjI)
 apply(subgoal_tac "{≅} `` {F⇩2} = {≅} `` {map φ F⇩1}")
  prefer 2
  apply(rule equiv_class_eq[OF equiv_EqF])
  apply(fastforce intro: congs_sym)
 apply(subgoal_tac "{F⇩2}//{≅} = {map φ F⇩1}//{≅}")
  prefer 2 apply(simp add:singleton_quotient)
 apply(subgoal_tac "∀F∈Fs⇩1'. ¬ (map φ F) ≅ (map φ F⇩1)")
  apply(fastforce simp:Iso_def quotient_def Image_Collect_case_prod simp del: Collect_congs_eq_iff
                 dest!: eq_equiv_class[OF _ equiv_EqF])
 apply clarify
 apply(subgoal_tac "inj_on φ (set F ∪ set F⇩1)")
  prefer 2
  apply(erule subset_inj_on)
  apply(blast)
 apply(clarsimp simp add:congs_map_eq_iff)
 apply(subgoal_tac "{≅} `` {F⇩1} = {≅} `` {F}")
  apply(simp add:singleton_quotient)
 apply(rule equiv_class_eq[OF equiv_EqF])
 apply(blast intro:congs_sym)
apply(subgoal_tac "F⇩2 ≅ (map φ F⇩1)")
 apply (simp add:congs_def inj_on_Un)
apply(clarsimp intro!:congs_sym)

apply(clarsimp simp add: is_pr_Iso_def is_pr_Hom_def quotient_diff1)
apply (simp add:singleton_quotient)
apply(subgoal_tac "F⇩2 ≅ (map φ F⇩1)")
 prefer 2 apply(fastforce simp add:congs_def)
apply(subgoal_tac "{≅}``{map φ F⇩1} = {≅}``{F⇩2}")
 prefer 2
 apply(rule equiv_class_eq[OF equiv_EqF])
 apply(fastforce intro:congs_sym)
apply(subgoal_tac "{≅}``{F⇩2} ∈ Fs⇩2 // {≅}")
 prefer 2 apply(erule quotientI)
apply (simp add:insert_absorb quotient_def)
done


lemma is_iso_Cons:
 "⟦ distinct (F⇩1#Fs⇩1'); distinct Fs⇩2;
    inj_on (λxs.{xs}//{≅}) (set(F⇩1#Fs⇩1')); inj_on (λxs.{xs}//{≅}) (set Fs⇩2) ⟧
  ⟹
 is_pr_iso φ (F⇩1#Fs⇩1') Fs⇩2 =
 (∃F⇩2 ∈ set Fs⇩2. length F⇩1 = length F⇩2 ∧ is_pr_iso φ Fs⇩1' (remove1 F⇩2 Fs⇩2)
    ∧ (∃n. map φ F⇩1 = rotate n F⇩2)
    ∧ inj_on φ (set F⇩1 ∪ (⋃F∈set Fs⇩1'. set F)))"
apply(simp add:is_pr_iso_def)
apply(subst is_pr_Iso_rec[where ?F⇩1.0 = F⇩1])
apply(simp_all)
done


subsection‹Isomorphism tests›

lemma map_upd_submap:
  "x ∉ dom m ⟹ (m(x ↦ y) ⊆⇩m m') = (m' x = Some y ∧ m ⊆⇩m m')"
apply(simp add:map_le_def dom_def)
apply(rule iffI)
 apply(rule conjI) apply (blast intro:sym)
 apply clarify
 apply(case_tac "a=x")
  apply auto
done

lemma map_of_zip_submap: "⟦ length xs = length ys; distinct xs ⟧ ⟹
 (map_of (zip xs ys) ⊆⇩m Some ∘ f) = (map f xs = ys)"
apply(induct rule: list_induct2)
 apply(simp)
apply (clarsimp simp: map_upd_submap simp del:o_apply fun_upd_apply)
apply simp
done

primrec pr_iso_test0 :: "('a ⇀ 'b) ⇒ 'a fgraph ⇒ 'b fgraph ⇒ bool" where
  "pr_iso_test0 m [] Fs⇩2 = (Fs⇩2 = [])"
| "pr_iso_test0 m (F⇩1#Fs⇩1) Fs⇩2 =
   (∃F⇩2 ∈ set Fs⇩2. length F⇩1 = length F⇩2 ∧
      (∃n. let m' = map_of(zip F⇩1 (rotate n F⇩2)) in
          if m ⊆⇩m m ++ m' ∧ inj_on (m++m') (dom(m++m'))
          then pr_iso_test0 (m ++ m') Fs⇩1 (remove1 F⇩2 Fs⇩2) else False))"

lemma map_compatI: "⟦ f ⊆⇩m Some ∘ h; g ⊆⇩m Some ∘ h ⟧ ⟹ f ⊆⇩m f++g"
by (fastforce simp add: map_le_def map_add_def dom_def split:option.splits)

lemma inj_on_map_addI1:
 "⟦ inj_on m A; m ⊆⇩m m++m'; A ⊆ dom m ⟧ ⟹ inj_on (m++m') A"
apply (clarsimp simp add: inj_on_def map_add_def map_le_def dom_def
                split:option.splits)
apply(rule conjI)
 apply fastforce
apply auto
 apply fastforce
apply (rename_tac x a y)
apply(subgoal_tac "m x = Some a")
 prefer 2 apply (fastforce)
apply(subgoal_tac "m y = Some a")
 prefer 2 apply (fastforce)
apply(subgoal_tac "m x = m y")
 prefer 2 apply simp
apply (blast)
done

lemma map_image_eq: "⟦ A ⊆ dom m; m ⊆⇩m m' ⟧ ⟹ m ` A = m' ` A"
by(force simp:map_le_def dom_def split:option.splits)

lemma inj_on_map_add_Un:
 "⟦ inj_on m (dom m); inj_on m' (dom m'); m ⊆⇩m Some ∘ f; m' ⊆⇩m Some ∘ f;
    inj_on f (dom m' ∪ dom m); A = dom m'; B = dom m ⟧
  ⟹ inj_on (m ++ m') (A ∪ B)"
apply(simp add:inj_on_Un)
apply(rule conjI)
 apply(fastforce intro!: inj_on_map_addI1 map_compatI)
apply(clarify)
apply(subgoal_tac "m ++ m' ⊆⇩m Some ∘ f")
 prefer 2 apply(fast intro:map_add_le_mapI map_compatI)
apply(subgoal_tac "dom m' - dom m ⊆ dom(m++m')")
 prefer 2 apply(fastforce)
apply(insert map_image_eq[of "dom m' - dom m" "m++m'" "Some ∘ f"])
apply(subgoal_tac "dom m - dom m' ⊆ dom(m++m')")
 prefer 2 apply(fastforce)
apply(insert map_image_eq[of "dom m - dom m'" "m++m'" "Some ∘ f"])
apply (clarsimp simp add: image_comp [symmetric])
apply blast
done

lemma map_of_zip_eq_SomeD: "length xs = length ys ⟹
  map_of (zip xs ys) x = Some y ⟹ y ∈ set ys"
apply(induct rule:list_induct2)
 apply simp
apply (auto split:if_splits)
done

lemma inj_on_map_of_zip:
  "⟦ length xs = length ys; distinct ys ⟧
   ⟹ inj_on (map_of (zip xs ys)) (set xs)"
apply(induct rule:list_induct2)
 apply simp
apply clarsimp
apply(rule conjI)
 apply(erule inj_on_fun_updI)
 apply(simp add:image_def)
 apply clarsimp
 apply(drule (1) map_of_zip_eq_SomeD[OF _ sym])
 apply fast
apply(clarsimp simp add:image_def)
apply(drule (1) map_of_zip_eq_SomeD[OF _ sym])
apply fast
done

lemma pr_iso_test0_correct: "⋀m Fs⇩2.
 ⟦ ∀F∈set Fs⇩1. distinct F; ∀F∈set Fs⇩2. distinct F;
   distinct Fs⇩1; inj_on (λxs.{xs}//{≅}) (set Fs⇩1);
   distinct Fs⇩2; inj_on (λxs.{xs}//{≅}) (set Fs⇩2); inj_on m (dom m) ⟧ ⟹
       pr_iso_test0 m Fs⇩1 Fs⇩2 =
       (∃φ. is_pr_iso φ Fs⇩1 Fs⇩2 ∧ m ⊆⇩m Some ∘ φ ∧
            inj_on φ (dom m ∪ (⋃F∈set Fs⇩1. set F)))"
apply(induct Fs⇩1)
 apply(simp add:inj_on_def dom_def)
 apply(rule iffI)
  apply (simp add:is_pr_iso_def is_pr_Iso_def is_pr_Hom_def)
  apply(rule_tac x = "the ∘ m" in exI)
  apply (fastforce simp: map_le_def)
 apply (clarsimp simp:is_pr_iso_def is_pr_Iso_def is_pr_Hom_def)
apply(rename_tac F⇩1 Fs⇩1' m Fs⇩2)
apply(clarsimp simp:Let_def Ball_def)
apply(simp add: is_iso_Cons)
apply(rule iffI)

apply clarify
apply(clarsimp simp add:map_of_zip_submap inj_on_diff)
apply(rule_tac x = φ in exI)
apply(rule conjI)
 apply(rule_tac x = F⇩2 in bexI)
  prefer 2 apply assumption
 apply(frule map_add_le_mapE)
 apply(simp add:map_of_zip_submap is_pr_iso_def is_pr_Iso_def)
 apply(rule conjI)
  apply blast
 apply(erule subset_inj_on)
 apply blast
 apply(rule conjI)
  apply(blast intro: map_le_trans)
 apply(erule subset_inj_on)
 apply blast

apply(clarsimp simp: inj_on_diff)
apply(rule_tac x = F⇩2 in bexI)
 prefer 2 apply assumption
apply simp
apply(rule_tac x = n in exI)
apply(rule conjI)
apply clarsimp
apply(rule_tac x = φ in exI)
apply simp
apply(rule conjI)
 apply(fastforce intro!:map_add_le_mapI simp:map_of_zip_submap)
apply(simp add:Un_ac)
apply(rule context_conjI)
apply(simp add:map_of_zip_submap[symmetric])
apply(erule (1) map_compatI)
apply(simp add:map_of_zip_submap[symmetric])
apply(erule inj_on_map_add_Un)
     apply(simp add:inj_on_map_of_zip)
    apply assumption
   apply assumption
  apply simp
  apply(erule subset_inj_on)
  apply fast
 apply simp
apply(rule refl)
done

corollary pr_iso_test0_corr:
 "⟦ ∀F∈set Fs⇩1. distinct F; ∀F∈set Fs⇩2. distinct F;
   distinct Fs⇩1; inj_on (λxs.{xs}//{≅}) (set Fs⇩1);
   distinct Fs⇩2; inj_on (λxs.{xs}//{≅}) (set Fs⇩2) ⟧ ⟹
       pr_iso_test0 Map.empty Fs⇩1 Fs⇩2 = (∃φ. is_pr_iso φ Fs⇩1 Fs⇩2)"
apply(subst pr_iso_test0_correct)
 apply assumption+
 apply simp
apply (simp add:is_pr_iso_def is_pr_Iso_def)
done

text‹Now we bound the number of rotations needed. We have to exclude
the empty face @{term"[]"} to be able to restrict the search to
@{prop"n < length xs"} (which would otherwise be vacuous).›

primrec pr_iso_test1 :: "('a ⇀ 'b) ⇒ 'a fgraph ⇒ 'b fgraph ⇒ bool" where
  "pr_iso_test1 m [] Fs⇩2 = (Fs⇩2 = [])"
| "pr_iso_test1 m (F⇩1#Fs⇩1) Fs⇩2 =
   (∃F⇩2 ∈ set Fs⇩2. length F⇩1 = length F⇩2 ∧
      (∃n < length F⇩2. let m' = map_of(zip F⇩1 (rotate n F⇩2)) in
          if  m ⊆⇩m m ++ m' ∧ inj_on (m++m') (dom(m++m'))
          then pr_iso_test1 (m ++ m') Fs⇩1 (remove1 F⇩2 Fs⇩2) else False))"

lemma test0_conv_test1:
 "⋀m Fs⇩2. [] ∉ set Fs⇩2 ⟹ pr_iso_test1 m Fs⇩1 Fs⇩2 = pr_iso_test0 m Fs⇩1 Fs⇩2"
apply(induct Fs⇩1)
 apply simp
apply simp
apply(rule iffI)
 apply blast
apply (clarsimp simp:Let_def)
apply(rule_tac x = F⇩2 in bexI)
 prefer 2 apply assumption
apply simp
apply(subgoal_tac "F⇩2 ≠ []")
 prefer 2 apply blast
apply(rule_tac x = "n mod length F⇩2" in exI)
apply(simp add:rotate_conv_mod[symmetric])
done

text‹Thus correctness carries over to ‹pr_iso_test1›:›

corollary pr_iso_test1_corr:
 "⟦ ∀F∈set Fs⇩1. distinct F; ∀F∈set Fs⇩2. distinct F; [] ∉ set Fs⇩2;
   distinct Fs⇩1; inj_on (λxs.{xs}//{≅}) (set Fs⇩1);
   distinct Fs⇩2; inj_on (λxs.{xs}//{≅}) (set Fs⇩2) ⟧ ⟹
       pr_iso_test1 Map.empty Fs⇩1 Fs⇩2 = (∃φ. is_pr_iso φ Fs⇩1 Fs⇩2)"
by(simp add: test0_conv_test1 pr_iso_test0_corr)

subsubsection‹Implementing maps by lists›

text‹The representation are lists of pairs with no repetition in the
first or second component.›

definition oneone :: "('a * 'b)list ⇒ bool" where
"oneone xys  ≡  distinct(map fst xys) ∧ distinct(map snd xys)"
declare oneone_def[simp]

type_synonym
  ('a,'b)tester = "('a * 'b)list ⇒ ('a * 'b)list ⇒ bool"
type_synonym
  ('a,'b)merger = "('a * 'b)list ⇒ ('a * 'b)list ⇒ ('a * 'b)list"

primrec pr_iso_test2 :: "('a,'b)tester ⇒ ('a,'b)merger ⇒
                ('a * 'b)list ⇒ 'a fgraph ⇒ 'b fgraph ⇒ bool" where
  "pr_iso_test2 tst mrg I [] Fs⇩2 = (Fs⇩2 = [])"
| "pr_iso_test2 tst mrg I (F⇩1#Fs⇩1) Fs⇩2 =
   (∃F⇩2 ∈ set Fs⇩2. length F⇩1 = length F⇩2 ∧
      (∃n < length F⇩2. let I' = zip F⇩1 (rotate n F⇩2) in
          if  tst I' I
          then pr_iso_test2 tst mrg (mrg I' I) Fs⇩1 (remove1 F⇩2 Fs⇩2) else False))"

lemma notin_range_map_of:
 "y ∉ snd ` set xys ⟹ Some y ∉ range(map_of xys)"
apply(induct xys)
 apply (simp add:image_def)
apply(clarsimp split:if_splits)
done


lemma inj_on_map_upd:
  "⟦ inj_on m (dom m); Some y ∉ range m ⟧ ⟹ inj_on (m(x↦y)) (dom m)"
apply(simp add:inj_on_def dom_def image_def)
apply (blast intro:sym)
done

lemma [simp]:
 "distinct(map snd xys) ⟹ inj_on (map_of xys) (dom(map_of xys))"
apply(induct xys)
 apply simp
apply (simp add: notin_range_map_of inj_on_map_upd)
apply(clarsimp simp add:image_def)
apply(drule map_of_SomeD)
apply fastforce
done

lemma lem: "Ball (set xs) P ⟹ Ball (set (remove1 x xs)) P = True"
by(induct xs) simp_all

lemma pr_iso_test2_conv_1:
  "⋀I Fs⇩2.
  ⟦ ∀I I'. oneone I ⟶ oneone I' ⟶
           tst I' I = (let m = map_of I; m' = map_of I'
                       in m ⊆⇩m m ++ m' ∧ inj_on (m++m') (dom(m++m')));
   ∀I I'. oneone I ⟶ oneone I' ⟶ tst I' I
          ⟶ map_of(mrg I' I) = map_of I ++ map_of I';
   ∀I I'. oneone I ∧ oneone I' ⟶ tst I' I ⟶ oneone (mrg I' I);
   oneone I;
   ∀F ∈ set Fs⇩1. distinct F; ∀F ∈ set Fs⇩2. distinct F ⟧ ⟹
  pr_iso_test2 tst mrg I Fs⇩1 Fs⇩2 = pr_iso_test1 (map_of I) Fs⇩1 Fs⇩2"
apply(induct Fs⇩1)
 apply simp
apply(simp add:Let_def lem inj_on_map_of_zip del: mod_less cong: conj_cong)
done

text‹A simple implementation›

definition compat :: "('a,'b)tester" where
 "compat I I' ==
  ∀(x,y) ∈ set I. ∀(x',y') ∈ set I'. (x = x') = (y = y')"

lemma image_map_upd:
  "x ∉ dom m ⟹ m(x↦y) ` A = m ` (A-{x}) ∪ (if x ∈ A then {Some y} else {})"
by(auto simp:image_def dom_def)


lemma image_map_of_conv_Image:
 "⋀A. ⟦ distinct(map fst xys) ⟧
 ⟹ map_of xys ` A = Some ` (set xys `` A) ∪ (if A ⊆ fst ` set xys then {} else {None})"
supply image_cong_simp [cong del]
apply (induct xys)
 apply (simp add:image_def Image_def Collect_conv_if)
apply (simp add:image_map_upd dom_map_of_conv_image_fst)
apply(erule thin_rl)
apply (clarsimp simp:image_def Image_def)
apply((rule conjI, clarify)+, fastforce)
apply fastforce
apply(clarify)
apply((rule conjI, clarify)+, fastforce)
apply fastforce
apply fastforce
apply fastforce
done


lemma [simp]: "m++m' ` (dom m' - A) = m' ` (dom m' - A)"
apply(clarsimp simp add:map_add_def image_def dom_def inj_on_def split:option.splits)
apply auto
apply (blast intro:sym)
apply (blast intro:sym)
apply (rule_tac x = xa in bexI)
prefer 2 apply blast
apply simp
done

declare Diff_subset [iff]

lemma compat_correct:
 "⟦ oneone I; oneone I' ⟧ ⟹
  compat I' I = (let m = map_of I; m' = map_of I'
                 in m ⊆⇩m m ++ m' ∧ inj_on (m++m') (dom(m++m')))"
apply(simp add: compat_def Let_def map_le_iff_map_add_commute)
apply(rule iffI)
 apply(rule context_conjI)
  apply(rule ext)
  apply (fastforce simp add:map_add_def split:option.split)
 apply(simp add:inj_on_Un)
 apply(drule sym)
 apply simp
 apply(simp add: dom_map_of_conv_image_fst image_map_of_conv_Image)
 apply(simp add: image_def Image_def)
 apply fastforce
apply clarsimp
apply(rename_tac a b aa ba)
apply(rule iffI)
 apply (clarsimp simp: fun_eq_iff)
 apply(erule_tac x = aa in allE)
 apply (simp add:map_add_def)
apply (clarsimp simp:dom_map_of_conv_image_fst)
apply(simp (no_asm_use) add:inj_on_def)
apply(drule_tac x = a in bspec)
 apply force
apply(drule_tac x = aa in bspec)
 apply force
apply(erule mp)
apply simp
apply(drule sym)
apply simp
done

corollary compat_corr:
 "∀I I'. oneone I ⟶ oneone I' ⟶
         compat I' I = (let m = map_of I; m' = map_of I'
                      in m ⊆⇩m m ++ m' ∧ inj_on (m++m') (dom(m++m')))"
by(simp add: compat_correct)

definition merge0 :: "('a,'b)merger" where
"merge0 I' I  ≡  [xy ← I'. fst xy ∉ fst ` set I] @ I"


lemma help1:
"distinct(map fst xys) ⟹ map_of (filter P xys) =
 map_of xys |` {x. ∃y. (x,y) ∈ set xys ∧ P(x,y)}"
apply(induct xys)
 apply simp
apply(rule ext)
apply (simp add:restrict_map_def)
apply force
done

lemma merge0_correct:
  "∀I I'. oneone I ⟶ oneone I' ⟶ compat I' I
  ⟶ map_of(merge0 I' I) = map_of I ++ map_of I'"
apply(simp add:compat_def merge0_def help1 fun_eq_iff map_add_def restrict_map_def split:option.split)
apply fastforce
done

lemma merge0_inv:
  "∀I I'. oneone I ∧ oneone I' ⟶ compat I' I ⟶ oneone (merge0 I' I)"
apply(auto simp add:merge0_def distinct_map compat_def split_def)
apply(blast intro:subset_inj_on)+
done

corollary pr_iso_test2_corr:
 "⟦ ∀F∈set Fs⇩1. distinct F; ∀F∈set Fs⇩2. distinct F; [] ∉ set Fs⇩2;
   distinct Fs⇩1; inj_on (λxs.{xs}//{≅}) (set Fs⇩1);
   distinct Fs⇩2; inj_on (λxs.{xs}//{≅}) (set Fs⇩2) ⟧ ⟹
       pr_iso_test2 compat merge0 [] Fs⇩1 Fs⇩2 = (∃φ. is_pr_iso φ Fs⇩1 Fs⇩2)"
by(simp add: pr_iso_test2_conv_1[OF compat_corr merge0_correct merge0_inv]
             pr_iso_test1_corr)

text‹Implementing merge as a recursive function:›

primrec merge :: "('a,'b)merger" where
  "merge [] I = I"
| "merge (xy#xys) I = (let (x,y) = xy in
    if ∀ (x',y') ∈ set I. x ≠ x' then xy # merge xys I else merge xys I)"

lemma merge_conv_merge0: "merge I' I = merge0 I' I"
apply(induct I')
 apply(simp add:merge0_def)
apply(force simp add:Let_def list_all_iff merge0_def)
done


primrec pr_iso_test_rec :: "('a * 'b)list ⇒ 'a fgraph ⇒ 'b fgraph ⇒ bool" where
  "pr_iso_test_rec I [] Fs⇩2 = (Fs⇩2 = [])"
| "pr_iso_test_rec I (F⇩1#Fs⇩1) Fs⇩2 =
   (∃ F⇩2 ∈ set Fs⇩2. length F⇩1 = length F⇩2 ∧
      (∃n < length F⇩2. let I' = zip F⇩1 (rotate n F⇩2) in
          compat I' I ∧ pr_iso_test_rec (merge I' I) Fs⇩1 (remove1 F⇩2 Fs⇩2)))"

lemma pr_iso_test_rec_conv_2:
  "⋀I Fs⇩2. pr_iso_test_rec I Fs⇩1 Fs⇩2 = pr_iso_test2 compat merge0 I Fs⇩1 Fs⇩2"
apply(induct Fs⇩1)
 apply simp
apply(auto simp: merge_conv_merge0 list_ex_iff Bex_def Let_def)
done

corollary pr_iso_test_rec_corr:
 "⟦ ∀F∈set Fs⇩1. distinct F; ∀F∈set Fs⇩2. distinct F; [] ∉ set Fs⇩2;
   distinct Fs⇩1; inj_on (λxs.{xs}//{≅}) (set Fs⇩1);
   distinct Fs⇩2; inj_on (λxs.{xs}//{≅}) (set Fs⇩2) ⟧ ⟹
       pr_iso_test_rec [] Fs⇩1 Fs⇩2 = (∃φ. is_pr_iso φ Fs⇩1 Fs⇩2)"
by(simp add: pr_iso_test_rec_conv_2 pr_iso_test2_corr)

definition pr_iso_test :: "'a fgraph ⇒ 'b fgraph ⇒ bool" where
"pr_iso_test Fs⇩1 Fs⇩2 = pr_iso_test_rec [] Fs⇩1 Fs⇩2"

corollary pr_iso_test_correct:
 "⟦ ∀F∈set Fs⇩1. distinct F; ∀F∈set Fs⇩2. distinct F; [] ∉ set Fs⇩2;
   distinct Fs⇩1; inj_on (λxs.{xs}//{≅}) (set Fs⇩1);
   distinct Fs⇩2; inj_on (λxs.{xs}//{≅}) (set Fs⇩2) ⟧ ⟹
  pr_iso_test Fs⇩1 Fs⇩2 = (∃φ. is_pr_iso φ Fs⇩1 Fs⇩2)"
apply(simp add:pr_iso_test_def pr_iso_test_rec_corr)
done

subsubsection‹`Improper' Isomorphisms›

definition is_Iso :: "('a ⇒ 'b) ⇒ 'a Fgraph ⇒ 'b Fgraph ⇒ bool" where
"is_Iso φ Fs⇩1 Fs⇩2 ≡ is_pr_Iso φ Fs⇩1 Fs⇩2 ∨ is_pr_Iso φ Fs⇩1 (rev ` Fs⇩2)"

definition is_iso :: "('a ⇒ 'b) ⇒ 'a fgraph ⇒ 'b fgraph ⇒ bool" where
"is_iso φ Fs⇩1 Fs⇩2 ≡ is_Iso φ (set Fs⇩1) (set Fs⇩2)"

definition iso_fgraph :: "'a fgraph ⇒ 'a fgraph ⇒ bool" (infix "≃" 60) where
"g⇩1 ≃ g⇩2  ≡  ∃φ. is_iso φ g⇩1 g⇩2"


lemma iso_fgraph_trans: assumes "f ≃ (g::'a fgraph)" and "g ≃ h" shows "f ≃ h"
proof-
  { fix φ φ' assume "is_pr_Hom φ (set f) (set g)" "inj_on φ (⋃F∈set f. set F)"
    "is_pr_Hom φ' (set g) (set h)" "inj_on φ' (⋃F∈set g. set F)"
    hence "is_pr_Hom (φ' ∘ φ) (set f) (set h) ∧
          inj_on (φ' ∘ φ) (⋃F∈set f. set F)"
      by(simp add: is_pr_Hom_trans comp_inj_on pr_Hom_pres_nodes)
  } moreover
  { fix φ φ' assume "is_pr_Hom φ (set f) (set g)" "inj_on φ (⋃F∈set f. set F)"
    "is_pr_Hom φ' (set g) (rev ` set h)" "inj_on φ' (⋃F∈set g. set F)"
    hence "is_pr_Hom (φ' ∘ φ) (set f) (rev ` set h) ∧
          inj_on (φ' ∘ φ) (⋃F∈set f. set F)"
      by(simp add: is_pr_Hom_trans comp_inj_on pr_Hom_pres_nodes)
  } moreover
  { fix φ φ' assume "is_pr_Hom φ (set f) (rev ` set g)" "inj_on φ (⋃F∈set f. set F)"
    "is_pr_Hom φ' (set g) (set h)" "inj_on φ' (⋃F∈set g. set F)"
    with this(3)[THEN is_pr_Hom_rev]
    have "is_pr_Hom (φ' ∘ φ) (set f) (rev ` set h) ∧
          inj_on (φ' ∘ φ) (⋃F∈set f. set F)"
      by(simp add: is_pr_Hom_trans comp_inj_on pr_Hom_pres_nodes)
  } moreover
  { fix φ φ' assume "is_pr_Hom φ (set f) (rev ` set g)" "inj_on φ (⋃F∈set f. set F)"
    "is_pr_Hom φ' (set g) (rev ` set h)" "inj_on φ' (⋃F∈set g. set F)"
    with this(3)[THEN is_pr_Hom_rev]
    have "is_pr_Hom (φ' ∘ φ) (set f) (set h) ∧
          inj_on (φ' ∘ φ) (⋃F∈set f. set F)"
      by(simp add: is_pr_Hom_trans comp_inj_on pr_Hom_pres_nodes)
  } ultimately show ?thesis using assms
    by(simp add: iso_fgraph_def is_iso_def is_Iso_def is_pr_Iso_def) blast
qed



definition iso_test :: "'a fgraph ⇒ 'b fgraph ⇒ bool" where
"iso_test g⇩1 g⇩2 ⟷ pr_iso_test g⇩1 g⇩2 ∨ pr_iso_test g⇩1 (map rev g⇩2)"

theorem iso_correct:
 "⟦ ∀F∈set Fs⇩1. distinct F; ∀F∈set Fs⇩2. distinct F; [] ∉ set Fs⇩2;
   distinct Fs⇩1; inj_on (λxs.{xs}//{≅}) (set Fs⇩1);
   distinct Fs⇩2; inj_on (λxs.{xs}//{≅}) (set Fs⇩2) ⟧ ⟹
  iso_test Fs⇩1 Fs⇩2 = (Fs⇩1 ≃ Fs⇩2)"
apply(simp add:iso_test_def pr_iso_test_correct iso_fgraph_def)
apply(subst pr_iso_test_correct)
       apply simp
      apply simp
     apply (simp add:image_def)
    apply simp
   apply simp
  apply (simp add:distinct_map)
 apply (simp add:inj_on_image_iff)
apply(simp add:is_iso_def is_Iso_def is_pr_iso_def)
apply blast
done

lemma iso_fgraph_refl[iff]: "g ≃ g"
apply(simp add: iso_fgraph_def)
apply(rule_tac x = "id" in exI)
apply(simp add: is_iso_def is_Iso_def is_pr_Iso_def is_pr_Hom_def id_def)
done


subsection‹Elementhood and containment modulo›

interpretation qle_gr: quasi_order "(≃)"
proof qed (auto intro:iso_fgraph_trans)

abbreviation qle_gr_in :: "'a fgraph ⇒ 'a fgraph set ⇒ bool"  (infix "∈⇩≃" 60)
where "x ∈⇩≃ M ≡ qle_gr.in_qle x M"
abbreviation qle_gr_sub :: "'a fgraph set ⇒ 'a fgraph set ⇒ bool"  (infix "⊆⇩≃" 60)
where "x ⊆⇩≃ M ≡ qle_gr.subseteq_qle x M"
abbreviation qle_gr_eq :: "'a fgraph set ⇒ 'a fgraph set ⇒ bool"  (infix "=⇩≃" 60)
where "x =⇩≃ M ≡ qle_gr.seteq_qle x M"

end