# Theory PlaneGraphIso

Up to index of Isabelle/HOL/Tame

theory PlaneGraphIso
imports Main
begin

```(*  ID:         \$Id: PlaneGraphIso.thy,v 1.2 2006/01/13 19:18:53 nipkow Exp \$
Author:     Tobias Nipkow
*)

header{* Isomorphisms Between Plane Graphs *}

theory PlaneGraphIso
imports Main
begin

declare not_None_eq [iff] not_Some_eq [iff]

text{* The symbols @{text "≅"} and @{text "\<simeq>"} are overloaded.  They
denote congruence and isomorphism on arbitrary types. On lists
(representing faces of graphs), @{text "≅"} means congruence modulo
rotation; @{text "\<simeq>"} is currently unused. On graphs, @{text "\<simeq>"}
means isomorphism and is a weaker version of @{text "≅"} (proper
isomorphism): @{text "\<simeq>"} also allows to reverse the orientation of
all faces. *}

consts
pr_isomorphic  :: "'a => 'a => bool" (infix "≅" 60)
isomorphic :: "'a => 'a => bool" (infix "\<simeq>" 60)

constdefs
Iso :: "('a * 'a) set" ("{≅}")
"{≅} ≡ {(f1, f2). f1 ≅ f2}"

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

text{* A plane graph is a set or list (for executability) of faces
(hence @{text Fgraph} and @{text fgraph}) and a face is a list of
nodes: *}

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

subsection{* Equivalence of faces *}

text{* Two faces are equivalent modulo rotation: *}

"F1 ≅ (F2::'a list) ≡ ∃n. F2 = rotate n F1"

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

lemma congs_sym: assumes A: "(xs::'a list) ≅ ys" shows "ys ≅ xs"
let ?l = "length xs"
from A obtain n where ys: "ys = rotate n xs" by(fastsimp 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)"
also have "rotate (n mod ?l) xs = rotate n xs"
by(rule rotate_conv_mod[symmetric])
finally show "∃m. xs = rotate m ys" by(fastsimp 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)
done

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

lemma congs_distinct:
"F1 ≅ F2 ==> distinct F2 = distinct F1"
by (auto simp: congs_def)

lemma congs_length:
"F1 ≅ F2 ==> length F2 = length F1"
by (auto simp: congs_def)

lemma congs_pres_nodes: "F1 ≅ F2 ==> set F1 = set F2"
by(clarsimp simp:congs_def)

lemma congs_map:
"inj_on f (set xs ∪ set ys) ==> (map f xs ≅ map f ys) = (xs ≅ ys)"
apply(rule iffI)
apply(clarsimp simp: rotate_map)
apply(drule map_inj_on)
apply (fastsimp)
apply clarsimp
apply(fastsimp simp: rotate_map)
done

lemma list_cong_rev_iff[simp]:
"(rev xs ≅ rev ys) = (xs ≅ ys)"
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)
done

lemma singleton_list_cong_eq_iff[simp]:
"({xs::'a list} // {≅} = {ys} // {≅}) = (xs ≅ ys)"

subsection{* Homomorphism and isomorphism *}

constdefs
is_Hom :: "('a => 'b) => 'a Fgraph => 'b Fgraph => bool"
"is_Hom φ Fs1 Fs2 ≡ (map φ ` Fs1)//{≅} = Fs2 //{≅}"

is_pr_Iso :: "('a => 'b) => 'a Fgraph => 'b Fgraph => bool"
"is_pr_Iso φ Fs1 Fs2 ≡ is_Hom φ Fs1 Fs2 ∧ inj_on φ (\<Union>F ∈ Fs1. set F)"

is_hom :: "('a => 'b) => 'a fgraph => 'b fgraph => bool"
"is_hom φ Fs1 Fs2 ≡ is_Hom φ (set Fs1) (set Fs2)"

is_pr_iso :: "('a => 'b) => 'a fgraph => 'b fgraph => bool"
"is_pr_iso φ Fs1 Fs2 ≡ is_pr_Iso φ (set Fs1) (set Fs2)"

text{* Homomorphisms preserve the set of nodes. *}

lemma UN_subset_iff: "((\<Union>i∈I. f i) ⊆ B) = (∀i∈I. f i ⊆ B)"
by blast

declare Image_Collect_split[simp del]

lemma Hom_pres_face_nodes:
"is_Hom φ Fs1 Fs2 ==> (\<Union>F∈Fs1. {φ ` (set F)}) = (\<Union>F∈Fs2. {set F})"
apply(clarsimp simp:is_Hom_def quotient_def)
apply auto
apply(subgoal_tac "EX F' : Fs2. {≅} `` {map φ F} = {≅} `` {F'}")
prefer 2 apply blast
apply (fastsimp simp: eq_equiv_class_iff[OF equiv_EqF] dest!:congs_pres_nodes)
apply(subgoal_tac "EX F' : Fs1. {≅} `` {map φ F'} = {≅} `` {F}")
apply (fastsimp simp: eq_equiv_class_iff[OF equiv_EqF] dest!:congs_pres_nodes)
apply (erule equalityE)
apply(fastsimp simp:UN_subset_iff)
done

lemma Hom_pres_nodes:
"is_Hom φ Fs1 Fs2 ==> φ ` (\<Union>F∈Fs1. set F) = (\<Union>F∈Fs2. set F)"
apply(drule Hom_pres_face_nodes)
apply(rule equalityI)
apply blast
apply(clarsimp)
apply(subgoal_tac "set F : (\<Union>F∈Fs2. {set F})")
prefer 2 apply blast
apply(subgoal_tac "set F : (\<Union>F∈Fs1. {φ ` set F})")
prefer 2 apply blast
apply(subgoal_tac "EX F':Fs1. φ ` set F' = set F")
prefer 2 apply blast
apply blast
done

text{* Therefore isomorphisms preserve cardinality of node set. *}

lemma pr_Iso_same_no_nodes:
"[| is_pr_Iso φ Fs1 Fs2; finite Fs1 |]
==> card(\<Union>F∈Fs1. set F) = card(\<Union>F∈Fs2. set F)"
by(clarsimp simp add: is_pr_Iso_def Hom_pres_nodes[symmetric] card_image)

lemma pr_iso_same_no_nodes:
"is_pr_iso φ Fs1 Fs2 ==> card(\<Union>F∈set Fs1. set F) = card(\<Union>F∈set Fs2. set F)"

text{* Isomorphisms preserve the number of faces. *}

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

lemma is_Hom_distinct:
"[| is_Hom φ Fs1 Fs2; ∀F∈Fs1. distinct F; ∀F∈Fs2. distinct F |]
==> ∀F∈Fs1. distinct(map φ F)"
apply(subgoal_tac "∃ F' ∈ Fs2. (map φ F, F') : {≅}")
apply(subgoal_tac "∃ F' ∈ Fs2. {map φ F}//{≅} = {F'}//{≅}")
apply clarify
apply(rule_tac x = F' in bexI)
apply(rule eq_equiv_class[OF _ equiv_EqF])
apply blast
apply assumption
apply(rotate_tac 1)
apply blast
done

text{* A kind of recursion rule, a first step towards executability: *}

lemma is_pr_Iso_rec:
"[| inj_on (%xs. {xs}//{≅}) Fs1; inj_on (%xs. {xs}//{≅}) Fs2; F1 ∈ Fs1 |] ==>
is_pr_Iso φ Fs1 Fs2 =
(∃F2 ∈ Fs2. length F1 = length F2 ∧ is_pr_Iso φ (Fs1 - {F1}) (Fs2 - {F2})
∧ (∃n. map φ F1 = rotate n F2)
∧ inj_on φ (\<Union>F∈Fs1. set F))"
apply(drule mk_disjoint_insert[of F1])
apply clarify
apply(rename_tac Fs1')
apply(rule iffI)

apply(clarsimp simp:is_Hom_def quotient_diff1)
apply(drule sym)
apply(clarsimp)
apply(subgoal_tac "{≅} `` {map φ F1} : Fs2 // {≅}")
apply(erule quotientE)
apply(rename_tac F2)
apply(drule eq_equiv_class[OF _ equiv_EqF])
apply blast
apply(rule_tac x = F2 in bexI)
prefer 2 apply assumption
apply(rule conjI)
apply(clarsimp simp: congs_def)
apply(rule conjI)
apply(subgoal_tac "{≅} `` {F2} = {≅} `` {map φ F1}")
prefer 2
apply(rule equiv_class_eq[OF equiv_EqF])
apply(fastsimp intro: congs_sym)
apply(subgoal_tac "{F2}//{≅} = {map φ F1}//{≅}")
apply(subgoal_tac "∀F∈Fs1'. ¬ (map φ F) ≅ (map φ F1)")
apply(fastsimp simp:Iso_def quotient_def Image_Collect_split
dest!: eq_equiv_class[OF _ equiv_EqF])
apply clarify
apply(subgoal_tac "inj_on φ (set F ∪ set F1)")
prefer 2
apply(erule subset_inj_on)
apply(blast)
apply(subgoal_tac "{≅} `` {F1} = {≅} `` {F}")
apply(rule equiv_class_eq[OF equiv_EqF])
apply(blast intro:congs_sym)
apply(subgoal_tac "F2 ≅ (map φ F1)")
apply(clarsimp intro!:congs_sym)

apply(clarsimp simp add: is_pr_Iso_def is_Hom_def quotient_diff1)
apply(subgoal_tac "F2 ≅ (map φ F1)")
apply(subgoal_tac "{≅}``{map φ F1} = {≅}``{F2}")
prefer 2
apply(rule equiv_class_eq[OF equiv_EqF])
apply(fastsimp intro:congs_sym)
apply(subgoal_tac "{≅}``{F2} ∈ Fs2 // {≅}")
prefer 2 apply(erule quotientI)
done

lemma is_iso_Cons:
"[| distinct (F1#Fs1'); distinct Fs2;
inj_on (%xs.{xs}//{≅}) (set(F1#Fs1')); inj_on (%xs.{xs}//{≅}) (set Fs2) |]
==>
is_pr_iso φ (F1#Fs1') Fs2 =
(∃F2 ∈ set Fs2. length F1 = length F2 ∧ is_pr_iso φ Fs1' (remove1 F2 Fs2)
∧ (∃n. map φ F1 = rotate n F2)
∧ inj_on φ (set F1 ∪ (\<Union>F∈set Fs1'. set F)))"
apply(subst is_pr_Iso_rec[where ?F1.0 = F1])
apply(simp_all)
done

subsection{* Isomorphism tests *}

lemma map_upd_submap:
"x ∉ dom m ==> (m(x \<mapsto> y) ⊆m m') = (m' x = Some y ∧ m ⊆m m')"
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 o 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

consts
pr_iso_test0 :: "('a ~=> 'b) => 'a fgraph => 'b fgraph => bool"

primrec
"pr_iso_test0 m [] Fs2 = (Fs2 = [])"
"pr_iso_test0 m (F1#Fs1) Fs2 =
(∃F2 ∈ set Fs2. length F1 = length F2 ∧
(∃n. let m' = map_of(zip F1 (rotate n F2)) in
if m ⊆m m ++ m' ∧ inj_on (m++m') (dom(m++m'))
then pr_iso_test0 (m ++ m') Fs1 (remove1 F2 Fs2) else False))"

lemma map_compatI: "[| f ⊆m Some o h; g ⊆m Some o h |] ==> f ⊆m f++g"

"[| inj_on m A; m ⊆m m++m'; A ⊆ dom m |] ==> inj_on (m++m') A"
split:option.splits)
apply(rule conjI)
apply fastsimp
apply auto
apply fastsimp
apply(subgoal_tac "m x = Some a")
prefer 2 apply (fastsimp)
apply(subgoal_tac "m y = Some a")
prefer 2 apply (fastsimp)
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)

"[| inj_on m (dom m); inj_on m' (dom m'); m ⊆m Some o f; m' ⊆m Some o f;
inj_on f (dom m' ∪ dom m); A = dom m'; B = dom m |]
==> inj_on (m ++ m') (A ∪ B)"
apply(rule conjI)
apply(clarify)
apply(subgoal_tac "m ++ m' ⊆m Some o f")
apply(subgoal_tac "dom m' - dom m ⊆ dom(m++m')")
prefer 2 apply(fastsimp)
apply(insert map_image_eq[of "dom m' - dom m" "m++m'" "Some o f"])
apply(subgoal_tac "dom m - dom m' ⊆ dom(m++m')")
prefer 2 apply(fastsimp)
apply(insert map_image_eq[of "dom m - dom m'" "m++m'" "Some o f"])
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(rule conjI)
apply(erule inj_on_fun_updI)
apply clarsimp
apply(drule (1) map_of_zip_eq_SomeD[OF _ sym])
apply fast
apply(drule (1) map_of_zip_eq_SomeD[OF _ sym])
apply fast
done

lemma pr_iso_test0_correct: "!!m Fs2.
[| ∀F∈set Fs1. distinct F; ∀F∈set Fs2. distinct F;
distinct Fs1; inj_on (%xs.{xs}//{≅}) (set Fs1);
distinct Fs2; inj_on (%xs.{xs}//{≅}) (set Fs2); inj_on m (dom m) |] ==>
pr_iso_test0 m Fs1 Fs2 =
(∃φ. is_pr_iso φ Fs1 Fs2 ∧ m ⊆m Some o φ ∧
inj_on φ (dom m ∪ (\<Union>F∈set Fs1. set F)))"
apply(induct Fs1)
apply(rule iffI)
apply(rule_tac x = "the o m" in exI)
apply (fastsimp simp: map_le_def)
apply (clarsimp simp:is_pr_iso_def is_pr_Iso_def is_Hom_def)
apply(rename_tac F1 Fs1' m Fs2)
apply(clarsimp simp:Let_def Ball_def)
apply(rule iffI)

apply clarify
apply(rule_tac x = φ in exI)
apply(rule conjI)
apply(rule_tac x = F2 in bexI)
prefer 2 apply assumption
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 = F2 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(rule context_conjI)
apply(erule (1) map_compatI)
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 Fs1. distinct F; ∀F∈set Fs2. distinct F;
distinct Fs1; inj_on (%xs.{xs}//{≅}) (set Fs1);
distinct Fs2; inj_on (%xs.{xs}//{≅}) (set Fs2) |] ==>
pr_iso_test0 empty Fs1 Fs2 = (∃φ. is_pr_iso φ Fs1 Fs2)"
apply(subst pr_iso_test0_correct)
apply assumption+
apply simp
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). *}

consts
pr_iso_test1 :: "('a ~=> 'b) => 'a fgraph => 'b fgraph => bool"

primrec
"pr_iso_test1 m [] Fs2 = (Fs2 = [])"
"pr_iso_test1 m (F1#Fs1) Fs2 =
(∃F2 ∈ set Fs2. length F1 = length F2 ∧
(∃n < length F2. let m' = map_of(zip F1 (rotate n F2)) in
if  m ⊆m m ++ m' ∧ inj_on (m++m') (dom(m++m'))
then pr_iso_test1 (m ++ m') Fs1 (remove1 F2 Fs2) else False))"

lemma test0_conv_test1:
"!!m Fs2. [] ∉ set Fs2 ==> pr_iso_test1 m Fs1 Fs2 = pr_iso_test0 m Fs1 Fs2"
apply(induct Fs1)
apply simp
apply simp
apply(rule iffI)
apply blast
apply (clarsimp simp:Let_def)
apply(rule_tac x = F2 in bexI)
prefer 2 apply assumption
apply simp
apply(subgoal_tac "F2 ≠ []")
prefer 2 apply blast
apply(rule_tac x = "n mod length F2" in exI)
done

text{* Thus correctness carries over to @{text pr_iso_test1}: *}

corollary pr_iso_test1_corr:
"[| ∀F∈set Fs1. distinct F; ∀F∈set Fs2. distinct F; [] ∉ set Fs2;
distinct Fs1; inj_on (%xs.{xs}//{≅}) (set Fs1);
distinct Fs2; inj_on (%xs.{xs}//{≅}) (set Fs2) |] ==>
pr_iso_test1 empty Fs1 Fs2 = (∃φ. is_pr_iso φ Fs1 Fs2)"

subsubsection{* Implementing maps by lists *}

text{* The representation are lists of pairs with no repetition in the
first or second component. *}

constdefs
oneone :: "('a * 'b)list => bool"
"oneone xys  ≡  distinct(map fst xys) ∧ distinct(map snd xys)"
declare oneone_def[simp]

types
('a,'b)tester = "('a * 'b)list => ('a * 'b)list => bool"
('a,'b)merger = "('a * 'b)list => ('a * 'b)list => ('a * 'b)list"

consts
pr_iso_test2 :: "('a,'b)tester => ('a,'b)merger =>
('a * 'b)list => 'a fgraph => 'b fgraph => bool"

primrec
"pr_iso_test2 tst mrg I [] Fs2 = (Fs2 = [])"
"pr_iso_test2 tst mrg I (F1#Fs1) Fs2 =
(∃F2 ∈ set Fs2. length F1 = length F2 ∧
(∃n < length F2. let I' = zip F1 (rotate n F2) in
if  tst I' I
then pr_iso_test2 tst mrg (mrg I' I) Fs1 (remove1 F2 Fs2) else False))"

lemma notin_range_map_of:
"y ∉ snd ` set xys ==> Some y ∉ range(map_of xys)"
apply(induct xys)
apply(clarsimp split:if_splits)
done

lemma inj_on_map_upd:
"[| inj_on m (dom m); Some y ∉ range m |] ==> inj_on (m(x\<mapsto>y)) (dom m)"
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(drule map_of_is_SomeD)
apply fastsimp
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 Fs2.
[| ∀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 Fs1. distinct F; ∀F ∈ set Fs2. distinct F |] ==>
pr_iso_test2 tst mrg I Fs1 Fs2 = pr_iso_test1 (map_of I) Fs1 Fs2"
apply(induct Fs1)
apply simp
apply(simp add:Let_def lem inj_on_map_of_zip del:mod_less distinct_map
cong:conj_cong)
done

text{* A simple implementation *}

constdefs
test :: "('a,'b)tester"
"test I I' ==
∀xy ∈ set I. ∀xy' ∈ set I'. (fst xy = fst xy') = (snd xy = snd xy')"

lemma image_map_upd:
"x ∉ dom m ==> m(x\<mapsto>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})"
apply (induct xys)
apply blast
apply(erule thin_rl)
apply (clarsimp simp:image_def Image_def)
apply((rule conjI, clarify)+, fastsimp)
apply fastsimp
apply(clarify)
apply((rule conjI, clarify)+, fastsimp)
apply fastsimp
apply fastsimp
apply fastsimp
done

lemma [simp]: "m++m' ` (dom m' - A) = m' ` (dom m' - A)"
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 test_correct:
"[| oneone I; oneone I' |] ==>
test I' I = (let m = map_of I; m' = map_of I'
in m ⊆m m ++ m' ∧ inj_on (m++m') (dom(m++m')))"
apply(rule iffI)
apply(rule context_conjI)
apply(rule ext)
apply(drule sym)
apply simp
apply fastsimp
apply clarsimp
apply(rename_tac a b aa ba)
apply(rule iffI)
apply (clarsimp simp:expand_fun_eq)
apply(erule_tac x = aa in allE)
apply (clarsimp simp:dom_map_of_conv_image_fst)
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 test_corr:
"∀I I'. oneone I --> oneone I' -->
test I' I = (let m = map_of I; m' = map_of I'
in m ⊆m m ++ m' ∧ inj_on (m++m') (dom(m++m')))"

constdefs
merge :: "('a,'b)merger"
"merge 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 force
done

lemma merge_correct:
"∀I I'. oneone I --> oneone I' --> test I' I
--> map_of(merge I' I) = map_of I ++ map_of I'"
apply fastsimp
done

lemma merge_inv:
"∀I I'. oneone I ∧ oneone I' --> test I' I --> oneone (merge I' I)"
apply(blast intro:subset_inj_on)+
done

corollary pr_iso_test2_corr:
"[| ∀F∈set Fs1. distinct F; ∀F∈set Fs2. distinct F; [] ∉ set Fs2;
distinct Fs1; inj_on (%xs.{xs}//{≅}) (set Fs1);
distinct Fs2; inj_on (%xs.{xs}//{≅}) (set Fs2) |] ==>
pr_iso_test2 test merge [] Fs1 Fs2 = (∃φ. is_pr_iso φ Fs1 Fs2)"
by(simp add: pr_iso_test2_conv_1[OF test_corr merge_correct merge_inv]
pr_iso_test1_corr)

text{* The final stage: implementing test and merge as recursive functions. *}

constdefs
test2 :: "('a,'b)tester"
"test2 I I' == list_all (%(x,y). list_all (%(x',y'). (x=x') = (y=y')) I') I"

lemma test2_conv_test: "test2 I I' = test I I'"
by (simp add:test_def test2_def list_all_iff split_def)

consts
merge2 :: "('a,'b)merger"
primrec
"merge2 [] I = I"
"merge2 (xy#xys) I = (let (x,y) = xy in
if list_all (%(x',y'). x ≠ x') I then xy # merge2 xys I
else merge2 xys I)"

lemma merge2_conv_merge: "merge2 I' I = merge I' I"
apply(induct I')
done

consts
pr_iso_test3 :: "('a * 'b)list => 'a fgraph => 'b fgraph => bool"

primrec
"pr_iso_test3 I [] Fs2 = (Fs2 = [])"
"pr_iso_test3 I (F1#Fs1) Fs2 =
list_ex (%F2. length F1 = length F2 ∧
list_ex (%n. let I' = zip F1 (rotate n F2) in
if  test2 I' I
then pr_iso_test3 (merge2 I' I) Fs1 (remove1 F2 Fs2) else False)
(upt 0 (length F2))) Fs2"

lemma pr_iso_test3_conv_2:
"!!I Fs2. pr_iso_test3 I Fs1 Fs2 = pr_iso_test2 test merge I Fs1 Fs2"
apply(induct Fs1)
apply simp
done

corollary pr_iso_test3_corr:
"[| ∀F∈set Fs1. distinct F; ∀F∈set Fs2. distinct F; [] ∉ set Fs2;
distinct Fs1; inj_on (%xs.{xs}//{≅}) (set Fs1);
distinct Fs2; inj_on (%xs.{xs}//{≅}) (set Fs2) |] ==>
pr_iso_test3 [] Fs1 Fs2 = (∃φ. is_pr_iso φ Fs1 Fs2)"

text{* A final optimization. *}

constdefs
pr_iso_test :: "(nat * 'a fgraph) => (nat * 'b fgraph) => bool"
"pr_iso_test ≡ λ(n1,Fs1) (n2,Fs2). n1 = n2 ∧ length Fs1 = length Fs2
∧ pr_iso_test3 [] Fs1 Fs2"

corollary pr_iso_test_correct:
"[| ∀F∈set Fs1. distinct F; ∀F∈set Fs2. distinct F; [] ∉ set Fs2;
distinct Fs1; inj_on (%xs.{xs}//{≅}) (set Fs1);
distinct Fs2; inj_on (%xs.{xs}//{≅}) (set Fs2);
n1 = card(\<Union>F∈set Fs1. set F); n2 = card(\<Union>F∈set Fs2. set F) |] ==>
pr_iso_test (n1,Fs1) (n2,Fs2) = (∃φ. is_pr_iso φ Fs1 Fs2)"
apply(blast intro:pr_iso_same_no_faces pr_iso_same_no_nodes)
done

subsubsection{* `Improper' Isomorphisms *}

constdefs
is_Iso :: "('a => 'b) => 'a Fgraph => 'b Fgraph => bool"
"is_Iso φ Fs1 Fs2 ≡ is_pr_Iso φ Fs1 Fs2 ∨ is_pr_Iso φ Fs1 (rev ` Fs2)"

is_iso :: "('a => 'b) => 'a fgraph => 'b fgraph => bool"
"is_iso φ Fs1 Fs2 ≡ is_Iso φ (set Fs1) (set Fs2)"

"g1 \<simeq> g2  ≡  ∃φ. is_iso φ g1 g2"

constdefs
iso_test :: "(nat * 'a fgraph) => (nat * 'b fgraph) => bool"
"iso_test ≡ %g1 g2. pr_iso_test g1 g2 ∨ pr_iso_test g1 (fst g2,map rev (snd g2))"

lemma inj_on_image_iff: "[| ALL x:A. ALL y:A. (g(f x) = g(f y)) = (g x = g y);
inj_on f A |] ==> inj_on g (f ` A) = inj_on g A"
apply(unfold inj_on_def)
apply blast
done

theorem iso_correct:
"[| ∀F∈set Fs1. distinct F; ∀F∈set Fs2. distinct F; [] ∉ set Fs2;
distinct Fs1; inj_on (%xs.{xs}//{≅}) (set Fs1);
distinct Fs2; inj_on (%xs.{xs}//{≅}) (set Fs2);
n1 = card(\<Union>F∈set Fs1. set F); n2 = card(\<Union>F∈set Fs2. set F) |] ==>
iso_test (n1,Fs1) (n2,Fs2) = (Fs1 \<simeq> Fs2)"
apply(subst pr_iso_test_correct)
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply blast
done

subsection{* Elementhood and containment modulo *}

constdefs
pr_iso_in :: "'a => 'a set => bool"  (infix "∈≅" 60)
"x ∈≅ M ≡ ∃y ∈ M. x ≅ y"

pr_iso_subseteq :: "'a set => 'a set => bool" (infix "⊆≅" 60)
"M ⊆≅ N ≡ ∀x ∈ M. x ∈≅ N"

iso_in :: "'a => 'a set => bool"  (infix "∈\<simeq>" 60)
"x ∈\<simeq> M ≡ ∃y ∈ M. x \<simeq> y"

iso_subseteq :: "'a set => 'a set => bool" (infix "⊆\<simeq>" 60)
"M ⊆\<simeq> N ≡ ∀x ∈ M. x ∈\<simeq> N"

end```

lemma

`  ((x, y) ∈ {≅}) = x ≅ y`

### Equivalence of faces

lemma congs_refl:

`  xs ≅ xs`

lemma congs_sym:

`  xs ≅ ys ==> ys ≅ xs`

lemma congs_trans:

`  [| xs ≅ ys; ys ≅ zs |] ==> xs ≅ zs`

lemma equiv_EqF:

`  equiv UNIV {≅}`

lemma congs_distinct:

`  F1 ≅ F2 ==> distinct F2 = distinct F1`

lemma congs_length:

`  F1 ≅ F2 ==> length F2 = length F1`

lemma congs_pres_nodes:

`  F1 ≅ F2 ==> set F1 = set F2`

lemma congs_map:

`  inj_on f (set xs ∪ set ys) ==> map f xs ≅ map f ys = xs ≅ ys`

lemma list_cong_rev_iff:

`  rev xs ≅ rev ys = xs ≅ ys`

lemma singleton_list_cong_eq_iff:

`  ({xs} // {≅} = {ys} // {≅}) = xs ≅ ys`

### Homomorphism and isomorphism

lemma UN_subset_iff:

`  ((UN i:I. f i) ⊆ B) = (∀i∈I. f i ⊆ B)`

lemma Hom_pres_face_nodes:

`  is_Hom φ Fs1 Fs2 ==> (UN F:Fs1. {φ ` set F}) = (UN F:Fs2. {set F})`

lemma Hom_pres_nodes:

`  is_Hom φ Fs1 Fs2 ==> φ ` (UN F:Fs1. set F) = (UN F:Fs2. set F)`

lemma pr_Iso_same_no_nodes:

```  [| is_pr_Iso φ Fs1 Fs2; finite Fs1 |]
==> card (UN F:Fs1. set F) = card (UN F:Fs2. set F)```

lemma pr_iso_same_no_nodes:

`  is_pr_iso φ Fs1 Fs2 ==> card (UN F:set Fs1. set F) = card (UN F:set Fs2. set F)`

lemma pr_iso_same_no_faces:

```  [| distinct Fs1; distinct Fs2; inj_on (λxs. {xs} // {≅}) (set Fs1);
inj_on (λxs. {xs} // {≅}) (set Fs2); is_pr_iso φ Fs1 Fs2 |]
==> length Fs1 = length Fs2```

lemma is_Hom_distinct:

```  [| is_Hom φ Fs1 Fs2; ∀F∈Fs1. distinct F; ∀F∈Fs2. distinct F |]
==> ∀F∈Fs1. distinct (map φ F)```

lemma is_pr_Iso_rec:

```  [| inj_on (λxs. {xs} // {≅}) Fs1; inj_on (λxs. {xs} // {≅}) Fs2; F1 ∈ Fs1 |]
==> is_pr_Iso φ Fs1 Fs2 =
(∃F2∈Fs2.
length F1 = length F2 ∧
is_pr_Iso φ (Fs1 - {F1}) (Fs2 - {F2}) ∧
(∃n. map φ F1 = rotate n F2) ∧ inj_on φ (UN F:Fs1. set F))```

lemma is_iso_Cons:

```  [| distinct (F1 # Fs1'); distinct Fs2;
inj_on (λxs. {xs} // {≅}) (set (F1 # Fs1'));
inj_on (λxs. {xs} // {≅}) (set Fs2) |]
==> is_pr_iso φ (F1 # Fs1') Fs2 =
(∃F2∈set Fs2.
length F1 = length F2 ∧
is_pr_iso φ Fs1' (remove1 F2 Fs2) ∧
(∃n. map φ F1 = rotate n F2) ∧
inj_on φ (set F1 ∪ (UN F:set Fs1'. set F)))```

### Isomorphism tests

lemma map_upd_submap:

`  x ∉ dom m ==> (m(x |-> y) ⊆m m') = (m' x = Some y ∧ m ⊆m m')`

lemma map_of_zip_submap:

```  [| length xs = length ys; distinct xs |]
==> (map_of (zip xs ys) ⊆m Some o f) = (map f xs = ys)```

lemma map_compatI:

`  [| f ⊆m Some o h; g ⊆m Some o h |] ==> f ⊆m f ++ g`

`  [| inj_on m A; m ⊆m m ++ m'; A ⊆ dom m |] ==> inj_on (m ++ m') A`

lemma map_image_eq:

`  [| A ⊆ dom m; m ⊆m m' |] ==> m ` A = m' ` A`

```  [| inj_on m (dom m); inj_on m' (dom m'); m ⊆m Some o f; m' ⊆m Some o f;
inj_on f (dom m' ∪ dom m); A = dom m'; B = dom m |]
==> inj_on (m ++ m') (A ∪ B)```

lemma map_of_zip_eq_SomeD:

`  [| length xs = length ys; map_of (zip xs ys) x = Some y |] ==> y ∈ set ys`

lemma inj_on_map_of_zip:

```  [| length xs = length ys; distinct ys |]
==> inj_on (map_of (zip xs ys)) (set xs)```

lemma pr_iso_test0_correct:

```  [| ∀F∈set Fs1. distinct F; ∀F∈set Fs2. distinct F; distinct Fs1;
inj_on (λxs. {xs} // {≅}) (set Fs1); distinct Fs2;
inj_on (λxs. {xs} // {≅}) (set Fs2); inj_on m (dom m) |]
==> pr_iso_test0 m Fs1 Fs2 =
(∃φ. is_pr_iso φ Fs1 Fs2 ∧
m ⊆m Some o φ ∧ inj_on φ (dom m ∪ (UN F:set Fs1. set F)))```

corollary pr_iso_test0_corr:

```  [| ∀F∈set Fs1. distinct F; ∀F∈set Fs2. distinct F; distinct Fs1;
inj_on (λxs. {xs} // {≅}) (set Fs1); distinct Fs2;
inj_on (λxs. {xs} // {≅}) (set Fs2) |]
==> pr_iso_test0 empty Fs1 Fs2 = (∃φ. is_pr_iso φ Fs1 Fs2)```

lemma test0_conv_test1:

`  [] ∉ set Fs2 ==> pr_iso_test1 m Fs1 Fs2 = pr_iso_test0 m Fs1 Fs2`

corollary pr_iso_test1_corr:

```  [| ∀F∈set Fs1. distinct F; ∀F∈set Fs2. distinct F; [] ∉ set Fs2; distinct Fs1;
inj_on (λxs. {xs} // {≅}) (set Fs1); distinct Fs2;
inj_on (λxs. {xs} // {≅}) (set Fs2) |]
==> pr_iso_test1 empty Fs1 Fs2 = (∃φ. is_pr_iso φ Fs1 Fs2)```

#### Implementing maps by lists

lemma notin_range_map_of:

`  y ∉ snd ` set xys ==> Some y ∉ range (map_of xys)`

lemma inj_on_map_upd:

`  [| inj_on m (dom m); Some y ∉ range m |] ==> inj_on (m(x |-> y)) (dom m)`

lemma

`  distinct (map snd xys) ==> inj_on (map_of xys) (dom (map_of xys))`

lemma lem:

`  Ball (set xs) P ==> Ball (set (remove1 x xs)) P = True`

lemma pr_iso_test2_conv_1:

```  [| ∀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 Fs1. distinct F; ∀F∈set Fs2. distinct F |]
==> pr_iso_test2 tst mrg I Fs1 Fs2 = pr_iso_test1 (map_of I) Fs1 Fs2```

lemma image_map_upd:

`  x ∉ dom m ==> m(x |-> y) ` A = m ` (A - {x}) ∪ (if x ∈ A then {Some y} else {})`

lemma image_map_of_conv_Image:

```  distinct (map fst xys)
==> map_of xys ` A =
Some ` set xys `` A ∪ (if A ⊆ fst ` set xys then {} else {None})```

lemma

`  m ++ m' ` (dom m' - A) = m' ` (dom m' - A)`

lemma test_correct:

```  [| oneone I; oneone I' |]
==> test I' I =
(let m = map_of I; m' = map_of I'
in m ⊆m m ++ m' ∧ inj_on (m ++ m') (dom (m ++ m')))```

corollary test_corr:

```  ∀I I'. oneone I -->
oneone I' -->
test I' I =
(let m = map_of I; m' = map_of I'
in m ⊆m m ++ m' ∧ inj_on (m ++ m') (dom (m ++ m')))```

lemma help1:

```  distinct (map fst xys)
==> map_of (filter P xys) = map_of xys |` {x. ∃y. (x, y) ∈ set xys ∧ P (x, y)}```

lemma merge_correct:

```  ∀I I'. oneone I -->
oneone I' --> test I' I --> map_of (merge I' I) = map_of I ++ map_of I'```

lemma merge_inv:

`  ∀I I'. oneone I ∧ oneone I' --> test I' I --> oneone (merge I' I)`

corollary pr_iso_test2_corr:

```  [| ∀F∈set Fs1. distinct F; ∀F∈set Fs2. distinct F; [] ∉ set Fs2; distinct Fs1;
inj_on (λxs. {xs} // {≅}) (set Fs1); distinct Fs2;
inj_on (λxs. {xs} // {≅}) (set Fs2) |]
==> pr_iso_test2 test merge [] Fs1 Fs2 = (∃φ. is_pr_iso φ Fs1 Fs2)```

lemma test2_conv_test:

`  test2 I I' = test I I'`

lemma merge2_conv_merge:

`  merge2 I' I = merge I' I`

lemma pr_iso_test3_conv_2:

`  pr_iso_test3 I Fs1 Fs2 = pr_iso_test2 test merge I Fs1 Fs2`

corollary pr_iso_test3_corr:

```  [| ∀F∈set Fs1. distinct F; ∀F∈set Fs2. distinct F; [] ∉ set Fs2; distinct Fs1;
inj_on (λxs. {xs} // {≅}) (set Fs1); distinct Fs2;
inj_on (λxs. {xs} // {≅}) (set Fs2) |]
==> pr_iso_test3 [] Fs1 Fs2 = (∃φ. is_pr_iso φ Fs1 Fs2)```

corollary pr_iso_test_correct:

```  [| ∀F∈set Fs1. distinct F; ∀F∈set Fs2. distinct F; [] ∉ set Fs2; distinct Fs1;
inj_on (λxs. {xs} // {≅}) (set Fs1); distinct Fs2;
inj_on (λxs. {xs} // {≅}) (set Fs2); n1 = card (UN F:set Fs1. set F);
n2 = card (UN F:set Fs2. set F) |]
==> pr_iso_test (n1, Fs1) (n2, Fs2) = (∃φ. is_pr_iso φ Fs1 Fs2)```

#### `Improper' Isomorphisms

lemma inj_on_image_iff:

```  [| ∀x∈A. ∀y∈A. (g (f x) = g (f y)) = (g x = g y); inj_on f A |]
==> inj_on g (f ` A) = inj_on g A```

theorem iso_correct:

```  [| ∀F∈set Fs1. distinct F; ∀F∈set Fs2. distinct F; [] ∉ set Fs2; distinct Fs1;
inj_on (λxs. {xs} // {≅}) (set Fs1); distinct Fs2;
inj_on (λxs. {xs} // {≅}) (set Fs2); n1 = card (UN F:set Fs1. set F);
n2 = card (UN F:set Fs2. set F) |]
==> iso_test (n1, Fs1) (n2, Fs2) = Fs1 \<simeq> Fs2```