diff --git a/thys/Planarity_Certificates/Planarity/Executable_Permutations.thy b/thys/Planarity_Certificates/Planarity/Executable_Permutations.thy
--- a/thys/Planarity_Certificates/Planarity/Executable_Permutations.thy
+++ b/thys/Planarity_Certificates/Planarity/Executable_Permutations.thy
@@ -1,1034 +1,1033 @@
section \Permutations as Products of Disjoint Cycles\
theory Executable_Permutations
imports
- "HOL-Library.Rewrite"
"HOL-Combinatorics.Permutations"
Graph_Theory.Auxiliary
List_Aux
begin
subsection \Cyclic Permutations\
definition list_succ :: "'a list \ 'a \ 'a" where
"list_succ xs x = (if x \ set xs then xs ! ((index xs x + 1) mod length xs) else x)"
text \
We demonstrate the functions on the following simple lemmas
@{lemma "list_succ [1 :: int, 2, 3] 1 = 2" by code_simp}
@{lemma "list_succ [1 :: int, 2, 3] 2 = 3" by code_simp}
@{lemma "list_succ [1 :: int, 2, 3] 3 = 1" by code_simp}
\
lemma list_succ_altdef:
"list_succ xs x = (let n = index xs x in if n + 1 = length xs then xs ! 0 else if n + 1 < length xs then xs ! (n + 1) else x)"
using index_le_size[of xs x] unfolding list_succ_def index_less_size_conv[symmetric] by (auto simp: Let_def)
lemma list_succ_Nil:
"list_succ [] = id"
by (simp add: list_succ_def fun_eq_iff)
lemma list_succ_singleton:
"list_succ [x] = list_succ []"
by (simp add: fun_eq_iff list_succ_def)
lemma list_succ_short:
assumes "length xs < 2" shows "list_succ xs = id"
using assms
by (cases xs) (rename_tac [2] y ys, case_tac [2] ys, auto simp: list_succ_Nil list_succ_singleton)
lemma list_succ_simps:
"index xs x + 1 = length xs \ list_succ xs x = xs ! 0"
"index xs x + 1 < length xs \ list_succ xs x = xs ! (index xs x + 1)"
"length xs \ index xs x \ list_succ xs x = x"
by (auto simp: list_succ_altdef)
lemma list_succ_not_in:
assumes "x \ set xs" shows "list_succ xs x = x"
using assms by (auto simp: list_succ_def)
lemma list_succ_list_succ_rev:
assumes "distinct xs" shows "list_succ (rev xs) (list_succ xs x) = x"
proof -
{ assume "index xs x + 1 < length xs"
moreover then have "length xs - Suc (Suc (length xs - Suc (Suc (index xs x)))) = index xs x"
by linarith
ultimately have ?thesis using assms
by (simp add: list_succ_def index_rev index_nth_id rev_nth)
}
moreover
{ assume A: "index xs x + 1 = length xs"
moreover
from A have "xs \ []" by auto
moreover
with A have "last xs = xs ! index xs x" by (cases "length xs") (auto simp: last_conv_nth)
ultimately
have ?thesis
using assms
by (auto simp add: list_succ_def rev_nth index_rev index_nth_id last_conv_nth)
}
moreover
{ assume A: "index xs x \ length xs"
then have "x \ set xs" by (metis index_less less_irrefl)
then have ?thesis by (auto simp: list_succ_def) }
ultimately show ?thesis by (metis discrete le_less not_less)
qed
lemma inj_list_succ: "distinct xs \ inj (list_succ xs)"
by (metis injI list_succ_list_succ_rev)
lemma inv_list_succ_eq: "distinct xs \ inv (list_succ xs) = list_succ (rev xs)"
by (metis distinct_rev inj_imp_inv_eq inj_list_succ list_succ_list_succ_rev)
lemma bij_list_succ: "distinct xs \ bij (list_succ xs)"
by (metis bij_def inj_list_succ distinct_rev list_succ_list_succ_rev surj_def)
lemma list_succ_permutes:
assumes "distinct xs" shows "list_succ xs permutes set xs"
using assms by (auto simp: permutes_conv_has_dom bij_list_succ has_dom_def list_succ_def)
lemma permutation_list_succ:
assumes "distinct xs" shows "permutation (list_succ xs)"
using list_succ_permutes[OF assms] by (auto simp: permutation_permutes)
lemma list_succ_nth:
assumes "distinct xs" "n < length xs" shows "list_succ xs (xs ! n) = xs ! (Suc n mod length xs)"
using assms by (auto simp: list_succ_def index_nth_id)
lemma list_succ_last[simp]:
assumes "distinct xs" "xs \ []" shows "list_succ xs (last xs) = hd xs"
using assms by (auto simp: list_succ_def hd_conv_nth)
lemma list_succ_rotate1[simp]:
assumes "distinct xs" shows "list_succ (rotate1 xs) = list_succ xs"
proof (rule ext)
fix y show "list_succ (rotate1 xs) y = list_succ xs y"
using assms
proof (induct xs)
case Nil then show ?case by simp
next
case (Cons x xs)
show ?case
proof (cases "x = y")
case True
then have "index (xs @ [y]) y = length xs"
using \distinct (x # xs)\ by (simp add: index_append)
with True show ?thesis by (cases "xs=[]") (auto simp: list_succ_def nth_append)
next
case False
then show ?thesis
apply (cases "index xs y + 1 < length xs")
apply (auto simp:list_succ_def index_append nth_append)
by (metis Suc_lessI index_less_size_conv mod_self nth_Cons_0 nth_append nth_append_length)
qed
qed
qed
lemma list_succ_rotate[simp]:
assumes "distinct xs" shows "list_succ (rotate n xs) = list_succ xs"
using assms by (induct n) auto
lemma list_succ_in_conv:
"list_succ xs x \ set xs \ x \ set xs"
by (auto simp: list_succ_def not_nil_if_in_set )
lemma list_succ_in_conv1:
assumes "A \ set xs = {}"
shows "list_succ xs x \ A \ x \ A"
by (metis assms disjoint_iff_not_equal list_succ_in_conv list_succ_not_in)
lemma list_succ_commute:
assumes "set xs \ set ys = {}"
shows "list_succ xs (list_succ ys x) = list_succ ys (list_succ xs x)"
proof -
have "\x. x \ set xs \ list_succ ys x = x"
"\x. x \ set ys \ list_succ xs x = x"
using assms by (blast intro: list_succ_not_in)+
then show ?thesis
by (cases "x \ set xs \ set ys") (auto simp: list_succ_in_conv list_succ_not_in)
qed
subsection \Arbitrary Permutations\
fun lists_succ :: "'a list list \ 'a \ 'a" where
"lists_succ [] x = x"
| "lists_succ (xs # xss) x = list_succ xs (lists_succ xss x)"
definition distincts :: "'a list list \ bool" where
"distincts xss \ distinct xss \ (\xs \ set xss. distinct xs \ xs \ []) \ (\xs \ set xss. \ys \ set xss. xs \ ys \ set xs \ set ys = {})"
lemma distincts_distinct: "distincts xss \ distinct xss"
by (auto simp: distincts_def)
lemma distincts_Nil[simp]: "distincts []"
by (simp add: distincts_def)
lemma distincts_single: "distincts [xs] \ distinct xs \ xs \ []"
by (auto simp add: distincts_def)
lemma distincts_Cons: "distincts (xs # xss)
\ xs \ [] \ distinct xs \ distincts xss \ (set xs \ (\ys \ set xss. set ys)) = {}" (is "?L \ ?R")
proof
assume ?L then show ?R by (auto simp: distincts_def)
next
assume ?R
then have "distinct (xs # xss)"
apply (auto simp: disjoint_iff_not_equal distincts_distinct)
apply (metis length_greater_0_conv nth_mem)
done
moreover
from \?R\ have "\xs \ set (xs # xss). distinct xs \ xs \ []"
by (auto simp: distincts_def)
moreover
from \?R\ have "\xs' \ set (xs # xss). \ys \ set (xs # xss). xs' \ ys \ set xs' \ set ys = {}"
by (simp add: distincts_def) blast
ultimately show ?L unfolding distincts_def by (intro conjI)
qed
lemma distincts_Cons': "distincts (xs # xss)
\ xs \ [] \ distinct xs \ distincts xss \ (\ys \ set xss. set xs \ set ys = {})" (is "?L \ ?R")
unfolding distincts_Cons by blast
lemma distincts_rev:
"distincts (map rev xss) \ distincts xss"
by (simp add: distincts_def distinct_map)
lemma length_distincts:
assumes "distincts xss"
shows "length xss = card (set ` set xss)"
using assms
proof (induct xss)
case Nil then show ?case by simp
next
case (Cons xs xss)
then have "set xs \ set ` set xss"
using equals0I[of "set xs"] by (auto simp: distincts_Cons disjoint_iff_not_equal )
with Cons show ?case by (auto simp add: distincts_Cons)
qed
lemma distincts_remove1: "distincts xss \ distincts (remove1 xs xss)"
by (auto simp: distincts_def)
lemma distinct_Cons_remove1:
"x \ set xs \ distinct (x # remove1 x xs) = distinct xs"
by (induct xs) auto
lemma set_Cons_remove1:
"x \ set xs \ set (x # remove1 x xs) = set xs"
by (induct xs) auto
lemma distincts_Cons_remove1:
"xs \ set xss \ distincts (xs # remove1 xs xss) = distincts xss"
by (simp only: distinct_Cons_remove1 set_Cons_remove1 distincts_def)
lemma distincts_inj_on_set:
assumes "distincts xss" shows "inj_on set (set xss)"
by (rule inj_onI) (metis assms distincts_def inf.idem set_empty)
lemma distincts_distinct_set:
assumes "distincts xss" shows "distinct (map set xss)"
using assms by (auto simp: distinct_map distincts_distinct distincts_inj_on_set)
lemma distincts_distinct_nth:
assumes "distincts xss" "n < length xss" shows "distinct (xss ! n)"
using assms by (auto simp: distincts_def)
lemma lists_succ_not_in:
assumes "x \ (\xs\set xss. set xs)" shows "lists_succ xss x = x"
using assms by (induct xss) (auto simp: list_succ_not_in)
lemma lists_succ_in_conv:
"lists_succ xss x \ (\xs\set xss. set xs) \ x \ (\xs\set xss. set xs)"
by (induct xss) (auto simp: list_succ_in_conv lists_succ_not_in list_succ_not_in)
lemma lists_succ_in_conv1:
assumes "A \ (\xs\set xss. set xs) = {}"
shows "lists_succ xss x \ A \ x \ A"
by (metis Int_iff assms emptyE lists_succ_in_conv lists_succ_not_in)
lemma lists_succ_Cons_pf: "lists_succ (xs # xss) = list_succ xs o lists_succ xss"
by auto
lemma lists_succ_Nil_pf: "lists_succ [] = id"
by (simp add: fun_eq_iff)
lemmas lists_succ_simps_pf = lists_succ_Cons_pf lists_succ_Nil_pf
lemma lists_succ_permutes:
assumes "distincts xss"
shows "lists_succ xss permutes (\xs \ set xss. set xs)"
using assms
proof (induction xss)
case Nil then show ?case by auto
next
case (Cons xs xss)
have "list_succ xs permutes (set xs)"
using Cons by (intro list_succ_permutes) (simp add: distincts_def in_set_member)
moreover
have "lists_succ xss permutes (\ys \ set xss. set ys)"
using Cons by (auto simp: Cons distincts_def)
ultimately show "lists_succ (xs # xss) permutes (\ys \ set (xs # xss). set ys)"
using Cons by (auto simp: lists_succ_Cons_pf intro: permutes_compose permutes_subset)
qed
lemma bij_lists_succ: "distincts xss \ bij (lists_succ xss)"
by (induct xss) (auto simp: lists_succ_simps_pf bij_comp bij_list_succ distincts_Cons)
lemma lists_succ_snoc: "lists_succ (xss @ [xs]) = lists_succ xss o list_succ xs"
by (induct xss) auto
lemma inv_lists_succ_eq:
assumes "distincts xss"
shows "inv (lists_succ xss) = lists_succ (rev (map rev xss))"
proof -
have *: "\f g. inv (\b. f (g b)) = inv (f o g)" by (simp add: o_def)
have **: "lists_succ [] = id" by auto
show ?thesis
using assms by (induct xss) (auto simp: * ** lists_succ_snoc lists_succ_Cons_pf o_inv_distrib
inv_list_succ_eq distincts_Cons bij_list_succ bij_lists_succ)
qed
lemma lists_succ_remove1:
assumes "distincts xss" "xs \ set xss"
shows "lists_succ (xs # remove1 xs xss) = lists_succ xss"
using assms
proof (induct xss)
case Nil then show ?case by simp
next
case (Cons ys xss)
show ?case
proof cases
assume "xs = ys" then show ?case by simp
next
assume "xs \ ys"
with Cons.prems have inter: "set xs \ set ys = {}" and "xs \ set xss"
by (auto simp: distincts_Cons)
have dists:
"distincts (xs # remove1 xs xss)"
"distincts (xs # ys # remove1 xs xss)"
using \distincts (ys # xss)\ \xs \ set xss\ by (auto simp: distincts_def)
have "list_succ xs \ (list_succ ys \ lists_succ (remove1 xs xss))
= list_succ ys \ (list_succ xs \ lists_succ (remove1 xs xss))"
using inter unfolding fun_eq_iff comp_def
by (subst list_succ_commute) auto
also have "\ = list_succ ys o (lists_succ (xs # remove1 xs xss))"
using dists by (simp add: lists_succ_Cons_pf distincts_Cons)
also have "\ = list_succ ys o lists_succ xss"
using \xs \ set xss\ \distincts (ys # xss)\
by (simp add: distincts_Cons Cons.hyps)
finally
show "lists_succ (xs # remove1 xs (ys # xss)) = lists_succ (ys # xss)"
using Cons dists by (auto simp: lists_succ_Cons_pf distincts_Cons)
qed
qed
lemma lists_succ_no_order:
assumes "distincts xss" "distincts yss" "set xss = set yss"
shows "lists_succ xss = lists_succ yss"
using assms
proof (induct xss arbitrary: yss)
case Nil then show ?case by simp
next
case (Cons xs xss)
have "xs \ set xss" "xs \ set yss" using Cons.prems
by (auto dest: distincts_distinct)
have "lists_succ xss = lists_succ (remove1 xs yss)"
using Cons.prems \xs \ _\
by (intro Cons.hyps) (auto simp add: distincts_Cons distincts_remove1 distincts_distinct)
then have "lists_succ (xs # xss) = lists_succ (xs # remove1 xs yss)"
using Cons.prems \xs \ _\
by (simp add: lists_succ_Cons_pf distincts_Cons_remove1)
then show ?case
using Cons.prems \xs \ _\ by (simp add: lists_succ_remove1)
qed
section \List Orbits\
text \Computes the orbit of @{term x} under @{term f}\
definition orbit_list :: "('a \ 'a) \ 'a \ 'a list" where
"orbit_list f x \ iterate 0 (funpow_dist1 f x x) f x"
partial_function (tailrec)
orbit_list_impl :: "('a \ 'a) \ 'a \ 'a list \ 'a \ 'a list"
where
"orbit_list_impl f s acc x = (let x' = f x in if x' = s then rev (x # acc) else orbit_list_impl f s (x # acc) x')"
context notes [simp] = length_fold_remove1_le begin
text \Computes the list of orbits\
fun orbits_list :: "('a \ 'a) \ 'a list \ 'a list list" where
"orbits_list f [] = []"
| "orbits_list f (x # xs) =
orbit_list f x # orbits_list f (fold remove1 (orbit_list f x) xs)"
fun orbits_list_impl :: "('a \ 'a) \ 'a list \ 'a list list" where
"orbits_list_impl f [] = []"
| "orbits_list_impl f (x # xs) =
(let fc = orbit_list_impl f x [] x in fc # orbits_list_impl f (fold remove1 fc xs))"
declare orbit_list_impl.simps[code]
end
abbreviation sset :: "'a list list \ 'a set set" where
"sset xss \ set ` set xss"
lemma iterate_funpow_step:
assumes "f x \ y" "y \ orbit f x"
shows "iterate 0 (funpow_dist1 f x y) f x = x # iterate 0 (funpow_dist1 f (f x) y) f (f x)"
proof -
from assms have A: "y \ orbit f (f x)" by (simp add: orbit_step)
have "iterate 0 (funpow_dist1 f x y) f x = x # iterate 1 (funpow_dist1 f x y) f x" (is "_ = _ # ?it")
- unfolding iterate_def by (rewrite in "\ = _" upt_conv_Cons) auto
+ unfolding iterate_def by (simp add: upt_rec)
also have "?it = map (\n. (f ^^ n) x) (map Suc [0.. = map (\n. (f ^^ n) (f x)) [0.. = iterate 0 (funpow_dist1 f (f x) y) f (f x)"
unfolding iterate_def
unfolding iterate_def by (simp add: funpow_dist_step[OF assms(1) A])
finally show ?thesis .
qed
lemma orbit_list_impl_conv:
assumes "y \ orbit f x"
shows "orbit_list_impl f y acc x = rev acc @ iterate 0 (funpow_dist1 f x y) f x"
using assms
proof (induct n\"funpow_dist1 f x y" arbitrary: x acc)
case (Suc x)
show ?case
proof cases
assume "f x = y"
then show ?thesis by (subst orbit_list_impl.simps) (simp add: Let_def iterate_def funpow_dist_0)
next
assume not_y :"f x \ y"
have y_in_succ: "y \ orbit f (f x)"
by (intro orbit_step Suc.prems not_y)
have "orbit_list_impl f y acc x = orbit_list_impl f y (x # acc) (f x)"
using not_y by (subst orbit_list_impl.simps) simp
also have "\ = rev (x # acc) @ iterate 0 (funpow_dist1 f (f x) y) f (f x)" (is "_ = ?rev @ ?it")
by (intro Suc funpow_dist_step not_y y_in_succ)
also have "\ = rev acc @ iterate 0 (funpow_dist1 f x y) f x"
using not_y Suc.prems by (simp add: iterate_funpow_step)
finally show ?thesis .
qed
qed
lemma orbit_list_conv_impl:
assumes "x \ orbit f x"
shows "orbit_list f x = orbit_list_impl f x [] x"
unfolding orbit_list_impl_conv[OF assms] orbit_list_def by simp
lemma set_orbit_list:
assumes "x \ orbit f x"
shows "set (orbit_list f x) = orbit f x"
by (simp add: orbit_list_def orbit_conv_funpow_dist1[OF assms] set_iterate)
lemma set_orbit_list':
assumes "permutation f" shows "set (orbit_list f x) = orbit f x"
using assms by (simp add: permutation_self_in_orbit set_orbit_list)
lemma distinct_orbit_list:
assumes "x \ orbit f x"
shows "distinct (orbit_list f x)"
by (simp del: upt_Suc add: orbit_list_def iterate_def distinct_map inj_on_funpow_dist1[OF assms])
lemma distinct_orbit_list':
assumes "permutation f" shows "distinct (orbit_list f x)"
using assms by (simp add: permutation_self_in_orbit distinct_orbit_list)
lemma orbits_list_conv_impl:
assumes "permutation f"
shows "orbits_list f xs = orbits_list_impl f xs"
proof (induct "length xs" arbitrary: xs rule: less_induct)
case less show ?case
using assms by (cases xs) (auto simp: assms less less_Suc_eq_le length_fold_remove1_le
orbit_list_conv_impl permutation_self_in_orbit Let_def)
qed
lemma orbit_list_not_nil[simp]: "orbit_list f x \ []"
by (simp add: orbit_list_def)
lemma sset_orbits_list:
assumes "permutation f" shows "sset (orbits_list f xs) = (orbit f) ` set xs"
proof (induct "length xs" arbitrary: xs rule: less_induct)
case less
show ?case
proof (cases xs)
case Nil then show ?thesis by simp
next
case (Cons x' xs')
let ?xs'' = "fold remove1 (orbit_list f x') xs'"
have A: "sset (orbits_list f ?xs'') = orbit f ` set ?xs''"
using Cons by (simp add: less_Suc_eq_le length_fold_remove1_le less.hyps)
have B: "set (orbit_list f x') = orbit f x'"
by (rule set_orbit_list) (simp add: permutation_self_in_orbit assms)
have "orbit f ` set (fold remove1 (orbit_list f x') xs') \ orbit f ` set xs'"
using set_fold_remove1[of _ xs'] by auto
moreover
have "orbit f ` set xs' - {orbit f x'} \ (orbit f ` set (fold remove1 (orbit_list f x') xs'))" (is "?L \ ?R")
proof
fix A assume "A \ ?L"
then obtain y where "A = orbit f y" "y \ set xs'" by auto
have "A \ orbit f x'" using \A \ ?L\ by auto
from \A = _\ \A \ _\ have "y \ orbit f x'"
by (meson assms cyclic_on_orbit orbit_cyclic_eq3 permutation_permutes)
with \y \ _\ have "y \ set (fold remove1 (orbit_list f x') xs')"
by (auto simp: set_fold_remove1' set_orbit_list permutation_self_in_orbit assms)
then show "A \ ?R" using \A = _\ by auto
qed
ultimately
show ?thesis by (auto simp: A B Cons)
qed
qed
subsection \Relation to @{term cyclic_on}\
lemma list_succ_orbit_list:
assumes "s \ orbit f s" "\x. x \ orbit f s \ f x = x"
shows "list_succ (orbit_list f s) = f"
proof -
have "distinct (orbit_list f s)" "\x. x \ set (orbit_list f s) \ x = f x"
using assms by (simp_all add: distinct_orbit_list set_orbit_list)
moreover
have "\i. i < length (orbit_list f s) \ orbit_list f s ! (Suc i mod length (orbit_list f s)) = f (orbit_list f s ! i)"
using funpow_dist1_prop[OF \s \ orbit f s\] by (auto simp: orbit_list_def funpow_mod_eq)
ultimately show ?thesis
by (auto simp: list_succ_def fun_eq_iff)
qed
lemma list_succ_funpow_conv:
assumes A: "distinct xs" "x \ set xs"
shows "(list_succ xs ^^ n) x = xs ! ((index xs x + n) mod length xs)"
proof -
have "xs \ []" using assms by auto
then show ?thesis
by (induct n) (auto simp: hd_conv_nth A index_nth_id list_succ_def mod_simps)
qed
lemma orbit_list_succ:
assumes "distinct xs" "x \ set xs"
shows "orbit (list_succ xs) x = set xs"
proof (intro set_eqI iffI)
fix y assume "y \ orbit (list_succ xs) x"
then show "y \ set xs"
by induct (auto simp: list_succ_in_conv \x \ set xs\)
next
fix y assume "y \ set xs"
moreover
{ fix i j have "i < length xs \ j < length xs \ \n. xs ! j = xs ! ((i + n) mod length xs)"
using assms by (auto simp: exI[where x="j + (length xs - i)"])
}
ultimately
show "y \ orbit (list_succ xs) x"
using assms by (auto simp: orbit_altdef_permutation permutation_list_succ list_succ_funpow_conv index_nth_id in_set_conv_nth)
qed
lemma cyclic_on_list_succ:
assumes "distinct xs" "xs \ []" shows "cyclic_on (list_succ xs) (set xs)"
using assms last_in_set by (auto simp: cyclic_on_def orbit_list_succ)
lemma obtain_orbit_list_func:
assumes "s \ orbit f s" "\x. x \ orbit f s \ f x = x"
obtains xs where "f = list_succ xs" "set xs = orbit f s" "distinct xs" "hd xs = s"
proof -
{ from assms have "f = list_succ (orbit_list f s)" by (simp add: list_succ_orbit_list)
moreover
have "set (orbit_list f s) = orbit f s" "distinct (orbit_list f s)"
by (auto simp: set_orbit_list distinct_orbit_list assms)
moreover have "hd (orbit_list f s) = s"
by (simp add: orbit_list_def iterate_def hd_map del: upt_Suc)
ultimately have "\