products/Sources/formale Sprachen/Isabelle/HOL/ex image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: ProjectGroup1.~dsk   Sprache: Isabelle

Untersuchung Isabelle©

(* Author: Florian Haftmann, TU Muenchen *)

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

theory Perm_Fragments
imports "HOL-Library.Perm" "HOL-Library.Dlist"
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: comp_def Fun.swap_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


text \<open>Misc\<close>

lemma (in comm_monoid_list_set) sorted_list_of_set:
  assumes "finite A"
  shows "list.F (map h (sorted_list_of_set A)) = set.F h A"
proof -
  from distinct_sorted_list_of_set
  have "set.F h (set (sorted_list_of_set A)) = list.F (map h (sorted_list_of_set A))"
    by (rule distinct_set_conv_list)
  with \<open>finite A\<close> show ?thesis
    by (simp)
qed

primrec subtract :: "'a list \ 'a list \ 'a list"
where
  "subtract [] ys = ys"
"subtract (x # xs) ys = subtract xs (removeAll x ys)"

lemma length_subtract_less_eq [simp]:
  "length (subtract xs ys) \ length ys"
proof (induct xs arbitrary: ys)
  case Nil then show ?case by simp
next
  case (Cons x xs)
  then have "length (subtract xs (removeAll x ys)) \ length (removeAll x ys)" .
  also have "length (removeAll x ys) \ length ys"
    by simp
  finally show ?case
    by simp
qed

end

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.2Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤





Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff