Quelle Perm_Fragments.thy Sprache: Isabelle

(* Author: Florian Haftmann, TU Muenchen *)

section \<open>Fragments on permuations\<close>

theory Perm_Fragments
imports "HOL-Library.Dlist" "HOL-Combinatorics.Perm"
begin

text \<open>On cycles\<close>

context
  includes permutation_syntax
begin

lemma cycle_prod_list:
  "\a # as\ = prod_list (map (\b. \a \ b\) (rev as))"
  by (induct as) simp_all

lemma cycle_append [simp]:
  "\a # as @ bs\ = \a # bs\ * \a # as\"
proof (induct as rule: cycle.induct)
  case (3 b c as)
  then have "\a # (b # as) @ bs\ = \a # bs\ * \a # b # as\"
    by simp
  then have "\a # as @ bs\ * \a \ b\ =
    \<langle>a # bs\<rangle> * \<langle>a # as\<rangle> * \<langle>a \<leftrightarrow> b\<rangle>"
    by (simp add: ac_simps)
  then have "\a # as @ bs\ * \a \ b\ * \a \ b\ =
    \<langle>a # bs\<rangle> * \<langle>a # as\<rangle> * \<langle>a \<leftrightarrow> b\<rangle> * \<langle>a \<leftrightarrow> b\<rangle>"
    by simp
  then have "\a # as @ bs\ = \a # bs\ * \a # as\"
    by (simp add: ac_simps)
  then show "\a # (b # c # as) @ bs\ =
    \<langle>a # bs\<rangle> * \<langle>a # b # c # as\<rangle>"
    by (simp add: ac_simps)
qed simp_all

lemma affected_cycle:
  "affected \as\ \ set as"
proof (induct as rule: cycle.induct)
  case (3 a b as)
  from affected_times
  have "affected (\a # as\ * \a \ b\)
    \<subseteq> affected \<langle>a # as\<rangle> \<union> affected \<langle>a \<leftrightarrow> b\<rangle>" .
  moreover from 3
  have "affected (\a # as\) \ insert a (set as)"
    by simp
  moreover
  have "affected \a \ b\ \ {a, b}"
    by (cases "a = b") (simp_all add: affected_swap)
  ultimately have "affected (\a # as\ * \a \ b\)
    \<subseteq> insert a (insert b (set as))"
    by blast
  then show ?case by auto
qed simp_all

lemma orbit_cycle_non_elem:
  assumes "a \ set as"
  shows "orbit \as\ a = {a}"
  unfolding not_in_affected_iff_orbit_eq_singleton [symmetric]
  using assms affected_cycle [of as] by blast

lemma inverse_cycle:
  assumes "distinct as"
  shows "inverse \as\ = \rev as\"
using assms proof (induct as rule: cycle.induct)
  case (3 a b as)
  then have *: "inverse \a # as\ = \rev (a # as)\"
    and distinct: "distinct (a # b # as)"
    by simp_all
  show " inverse \a # b # as\ = \rev (a # b # as)\"
  proof (cases as rule: rev_cases)
    case Nil with * show ?thesis
      by (simp add: swap_sym)
  next
    case (snoc cs c)
    with distinct have "distinct (a # b # cs @ [c])"
      by simp
    then have **: "\a \ b\ * \c \ a\ = \c \ a\ * \c \ b\"
      by transfer (auto simp add: fun_eq_iff transpose_def)
    with snoc * show ?thesis
      by (simp add: mult.assoc [symmetric])
  qed
qed simp_all

lemma order_cycle_non_elem:
  assumes "a \ set as"
  shows "order \as\ a = 1"
proof -
  from assms have "orbit \as\ a = {a}"
    by (rule orbit_cycle_non_elem)
  then have "card (orbit \as\ a) = card {a}"
    by simp
  then show ?thesis
    by simp
qed

lemma orbit_cycle_elem:
  assumes "distinct as" and "a \ set as"
  shows "orbit \as\ a = set as"
  oops \<comment> \<open>(we need rotation here\<close>

lemma order_cycle_elem:
  assumes "distinct as" and "a \ set as"
  shows "order \as\ a = length as"
  oops

text \<open>Adding fixpoints\<close>

definition fixate :: "'a \ 'a perm \ 'a perm"
where
  "fixate a f = (if a \ affected f then f * \inverse f \$\ a \ a\ else f)"

lemma affected_fixate_trivial:
  assumes "a \ affected f"
  shows "affected (fixate a f) = affected f"
  using assms by (simp add: fixate_def)

lemma affected_fixate_binary_circle:
  assumes "order f a = 2"
  shows "affected (fixate a f) = affected f - {a, apply f a}" (is "?A = ?B")
proof (rule set_eqI)
  interpret bijection "apply f"
    by standard simp
  fix b
  from assms order_greater_eq_two_iff [of f a] have "a \ affected f"
    by simp
  moreover have "apply (f ^ 2) a = a"
    by (simp add: assms [symmetric])
  ultimately show "b \ ?A \ b \ ?B"
    by (cases "b \ {a, apply (inverse f) a}")
      (auto simp add: in_affected power2_eq_square apply_inverse apply_times fixate_def)
qed

lemma affected_fixate_no_binary_circle:
  assumes "order f a > 2"
  shows "affected (fixate a f) = affected f - {a}" (is "?A = ?B")
proof (rule set_eqI)
  interpret bijection "apply f"
    by standard simp
  fix b
  from assms order_greater_eq_two_iff [of f a]
  have "a \ affected f"
    by simp
  moreover from assms
  have "apply f (apply f a) \ a"
    using apply_power_eq_iff [of f 2 a 0]
    by (simp add: power2_eq_square apply_times)
  ultimately show "b \ ?A \ b \ ?B"
    by (cases "b \ {a, apply (inverse f) a}")
      (auto simp add: in_affected apply_inverse apply_times fixate_def)
qed

lemma affected_fixate:
  "affected (fixate a f) \ affected f - {a}"
proof -
  have "a \ affected f \ order f a = 2 \ order f a > 2"
    by (auto simp add: not_less dest: affected_order_greater_eq_two)
  then consider "a \ affected f" | "order f a = 2" | "order f a > 2"
    by blast
  then show ?thesis apply cases
  using affected_fixate_trivial [of a f]
    affected_fixate_binary_circle [of f a]
    affected_fixate_no_binary_circle [of f a]
    by auto
qed

lemma orbit_fixate_self [simp]:
  "orbit (fixate a f) a = {a}"
proof -
  have "apply (f * inverse f) a = a"
    by simp
  then have "apply f (apply (inverse f) a) = a"
    by (simp only: apply_times comp_apply)
  then show ?thesis
    by (simp add: fixate_def not_in_affected_iff_orbit_eq_singleton [symmetric] in_affected apply_times)
qed

lemma order_fixate_self [simp]:
  "order (fixate a f) a = 1"
proof -
  have "card (orbit (fixate a f) a) = card {a}"
    by simp
  then show ?thesis
    by (simp only: card_orbit_eq) simp
qed

lemma
  assumes "b \ orbit f a"
  shows "orbit (fixate b f) a = orbit f a"
  oops

lemma
  assumes "b \ orbit f a" and "b \ a"
  shows "orbit (fixate b f) a = orbit f a - {b}"
  oops


text \<open>Distilling cycles from permutations\<close>

inductive_set orbits :: "'a perm \ 'a set set" for f
where
  in_orbitsI: "a \ affected f \ orbit f a \ orbits f"

lemma orbits_unfold:
  "orbits f = orbit f ` affected f"
  by (auto intro: in_orbitsI elim: orbits.cases)

lemma in_orbit_affected:
  assumes "b \ orbit f a"
  assumes "a \ affected f"
  shows "b \ affected f"
proof (cases "a = b")
  case True with assms show ?thesis by simp
next
  case False with assms have "{a, b} \ orbit f a"
    by auto
  also from assms have "orbit f a \ affected f"
    by (blast intro!: orbit_subset_eq_affected)
  finally show ?thesis by simp
qed

lemma Union_orbits [simp]:
  "\(orbits f) = affected f"
  by (auto simp add: orbits.simps intro: in_orbitsI in_orbit_affected)

lemma finite_orbits [simp]:
  "finite (orbits f)"
  by (simp add: orbits_unfold)

lemma card_in_orbits:
  assumes "A \ orbits f"
  shows "card A \ 2"
  using assms by cases
    (auto dest: affected_order_greater_eq_two)

lemma disjoint_orbits:
  assumes "A \ orbits f" and "B \ orbits f" and "A \ B"
  shows "A \ B = {}"
  using \<open>A \<in> orbits f\<close> apply cases
  using \<open>B \<in> orbits f\<close> apply cases
  using \<open>A \<noteq> B\<close> apply (simp_all add: orbit_disjoint)
  done

definition trace :: "'a \ 'a perm \ 'a list"
where
  "trace a f = map (\n. apply (f ^ n) a) [0..

lemma set_trace_eq [simp]:
  "set (trace a f) = orbit f a"
  by (auto simp add: trace_def orbit_unfold_image)

definition seeds :: "'a perm \ 'a::linorder list"
where
  "seeds f = sorted_list_of_set (Min ` orbits f)"

definition cycles :: "'a perm \ 'a::linorder list list"
where
  "cycles f = map (\a. trace a f) (seeds f)"

end

end

quality100%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.