--- a/NEWS Mon Jul 04 20:48:55 2016 +0200
+++ b/NEWS Mon Jul 04 20:51:04 2016 +0200
@@ -146,6 +146,15 @@
*** HOL ***
+* Theory Library/Combinator_PER.thy: combinator to build partial
+equivalence relations from a predicate and an equivalence relation.
+
+* Theory Library/Perm.thy: basic facts about almost everywhere fix
+bijections.
+
+* Locale bijection establishes convenient default simp rules
+like "inv f (f a) = a" for total bijections.
+
* Former locale lifting_syntax is now a bundle, which is easier to
include in a local context or theorem statement, e.g. "context includes
lifting_syntax begin ... end". Minor INCOMPATIBILITY.
--- a/src/HOL/Binomial.thy Mon Jul 04 20:48:55 2016 +0200
+++ b/src/HOL/Binomial.thy Mon Jul 04 20:51:04 2016 +0200
@@ -6,7 +6,7 @@
Additional binomial identities by Chaitanya Mangla and Manuel Eberl
*)
-section\<open>Factorial Function, Binomial Coefficients and Binomial Theorem\<close>
+section \<open>Combinatorial Functions: Factorial Function, Rising Factorials, Binomial Coefficients and Binomial Theorem\<close>
theory Binomial
imports Main
@@ -170,7 +170,8 @@
text \<open>This development is based on the work of Andy Gordon and
Florian Kammueller.\<close>
-subsection \<open>Basic definitions and lemmas\<close>
+
+subsection \<open>Binomial coefficients\<close>
text \<open>Combinatorial definition\<close>
@@ -394,6 +395,12 @@
ultimately show ?ths by blast
qed
+lemma binomial_fact':
+ assumes "k \<le> n"
+ shows "n choose k = fact n div (fact k * fact (n - k))"
+ using binomial_fact_lemma [OF assms]
+ by (metis fact_nonzero mult_eq_0_iff nonzero_mult_divide_cancel_left)
+
lemma binomial_fact:
assumes kn: "k \<le> n"
shows "(of_nat (n choose k) :: 'a::field_char_0) =
@@ -465,7 +472,8 @@
finally show ?thesis .
qed
-subsection\<open>Pochhammer's symbol : generalized rising factorial\<close>
+
+subsection \<open>Pochhammer's symbol : generalized rising factorial\<close>
text \<open>See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"}\<close>
@@ -675,20 +683,24 @@
qed
-subsection\<open>Generalized binomial coefficients\<close>
+subsection \<open>Generalized binomial coefficients\<close>
-definition (in field_char_0) gbinomial :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
+definition gbinomial :: "'a :: {semidom_divide, semiring_char_0} \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
where
- "a gchoose n = setprod (\<lambda>i. a - of_nat i) {..<n} / fact n"
+ "a gchoose n = setprod (\<lambda>i. a - of_nat i) {..<n} div fact n"
lemma gbinomial_Suc:
"a gchoose (Suc k) = setprod (\<lambda>i. a - of_nat i) {..k} / fact (Suc k)"
by (simp add: gbinomial_def lessThan_Suc_atMost)
-lemma gbinomial_0 [simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0"
+lemma gbinomial_0 [simp]:
+ fixes a :: "'a::field_char_0"
+ shows "a gchoose 0 = 1" "(0::'a) gchoose (Suc n) = 0"
by (simp_all add: gbinomial_def)
-lemma gbinomial_pochhammer: "a gchoose n = (- 1) ^ n * pochhammer (- a) n / (fact n)"
+lemma gbinomial_pochhammer:
+ fixes a :: "'a::field_char_0"
+ shows "a gchoose n = (- 1) ^ n * pochhammer (- a) n / (fact n)"
proof (cases "n = 0")
case True
then show ?thesis by simp
@@ -710,6 +722,32 @@
finally show ?thesis by simp
qed
+lemma gbinomial_binomial:
+ "n gchoose k = n choose k"
+proof (cases "k \<le> n")
+ case False
+ then have "n < k" by (simp add: not_le)
+ then have "0 \<in> (op - n) ` {..<k}"
+ by auto
+ then have "setprod (op - n) {..<k} = 0"
+ by (auto intro: setprod_zero)
+ with \<open>n < k\<close> show ?thesis
+ by (simp add: binomial_eq_0 gbinomial_def setprod_zero)
+next
+ case True
+ then have "inj_on (op - n) {..<k}"
+ by (auto intro: inj_onI)
+ then have "\<Prod>(op - n ` {..<k}) = setprod (op - n) {..<k}"
+ by (auto dest: setprod.reindex)
+ also have "op - n ` {..<k} = {Suc (n - k)..n}"
+ using True by (auto simp add: image_def Bex_def) arith
+ finally have *: "setprod (\<lambda>q. n - q) {..<k} = \<Prod>{Suc (n - k)..n}" ..
+ from True have "(n choose k) = fact n div (fact k * fact (n - k))"
+ by (rule binomial_fact')
+ with * show ?thesis
+ by (simp add: gbinomial_def mult.commute [of "fact k"] div_mult2_eq fact_div_fact)
+qed
+
lemma binomial_gbinomial:
"of_nat (n choose k) = (of_nat n gchoose k :: 'a::field_char_0)"
proof -
@@ -752,6 +790,8 @@
ultimately show ?thesis by blast
qed
+setup \<open>Sign.add_const_constraint (@{const_name gbinomial}, SOME @{typ "'a::field_char_0 \<Rightarrow> nat \<Rightarrow> 'a"})\<close>
+
lemma gbinomial_1[simp]: "a gchoose 1 = a"
by (simp add: gbinomial_def lessThan_Suc)
@@ -1098,7 +1138,7 @@
thus ?case using gbinomial_Suc_Suc[of "(r + of_nat m + 1)" m] by (simp add: add_ac)
qed auto
-subsection \<open>Summation on the upper index\<close>
+subsubsection \<open>Summation on the upper index\<close>
text \<open>
Another summation formula is equation 5.10 of the reference material \cite[p.~160]{GKP},
aptly named \emph{summation on the upper index}:\[\sum_{0 \leq k \leq n} {k \choose m} =
@@ -1345,7 +1385,7 @@
by simp
-subsection \<open>Binomial coefficients\<close>
+subsection \<open>More on Binomial Coefficients\<close>
lemma choose_one: "(n::nat) choose 1 = n"
by simp
@@ -1547,6 +1587,9 @@
(simp_all only: ac_simps diff_Suc_Suc Suc_diff_le diff_add_inverse fact_Suc of_nat_id)
qed
+
+subsection \<open>Misc\<close>
+
lemma fact_code [code]:
"fact n = (of_nat (fold_atLeastAtMost_nat (op *) 2 n 1) :: 'a :: semiring_char_0)"
proof -
@@ -1562,7 +1605,6 @@
"setprod f {..<Suc n} = fold_atLeastAtMost_nat (times \<circ> f) 0 n 1"
by (simp add: lessThan_Suc_atMost atLeast0AtMost [symmetric] setprod_atLeastAtMost_code comp_def)
-
lemma pochhammer_code [code]:
"pochhammer a n = (if n = 0 then 1 else
fold_atLeastAtMost_nat (\<lambda>n acc. (a + of_nat n) * acc) 0 (n - 1) 1)"
--- a/src/HOL/Hilbert_Choice.thy Mon Jul 04 20:48:55 2016 +0200
+++ b/src/HOL/Hilbert_Choice.thy Mon Jul 04 20:51:04 2016 +0200
@@ -811,6 +811,73 @@
subsection \<open>More on injections, bijections, and inverses\<close>
+locale bijection =
+ fixes f :: "'a \<Rightarrow> 'a"
+ assumes bij: "bij f"
+begin
+
+lemma bij_inv:
+ "bij (inv f)"
+ using bij by (rule bij_imp_bij_inv)
+
+lemma surj [simp]:
+ "surj f"
+ using bij by (rule bij_is_surj)
+
+lemma inj:
+ "inj f"
+ using bij by (rule bij_is_inj)
+
+lemma surj_inv [simp]:
+ "surj (inv f)"
+ using inj by (rule inj_imp_surj_inv)
+
+lemma inj_inv:
+ "inj (inv f)"
+ using surj by (rule surj_imp_inj_inv)
+
+lemma eqI:
+ "f a = f b \<Longrightarrow> a = b"
+ using inj by (rule injD)
+
+lemma eq_iff [simp]:
+ "f a = f b \<longleftrightarrow> a = b"
+ by (auto intro: eqI)
+
+lemma eq_invI:
+ "inv f a = inv f b \<Longrightarrow> a = b"
+ using inj_inv by (rule injD)
+
+lemma eq_inv_iff [simp]:
+ "inv f a = inv f b \<longleftrightarrow> a = b"
+ by (auto intro: eq_invI)
+
+lemma inv_left [simp]:
+ "inv f (f a) = a"
+ using inj by (simp add: inv_f_eq)
+
+lemma inv_comp_left [simp]:
+ "inv f \<circ> f = id"
+ by (simp add: fun_eq_iff)
+
+lemma inv_right [simp]:
+ "f (inv f a) = a"
+ using surj by (simp add: surj_f_inv_f)
+
+lemma inv_comp_right [simp]:
+ "f \<circ> inv f = id"
+ by (simp add: fun_eq_iff)
+
+lemma inv_left_eq_iff [simp]:
+ "inv f a = b \<longleftrightarrow> f b = a"
+ by auto
+
+lemma inv_right_eq_iff [simp]:
+ "b = inv f a \<longleftrightarrow> f b = a"
+ by auto
+
+end
+
lemma infinite_imp_bij_betw:
assumes INF: "\<not> finite A"
shows "\<exists>h. bij_betw h A (A - {a})"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Combine_PER.thy Mon Jul 04 20:51:04 2016 +0200
@@ -0,0 +1,60 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+section \<open>A combinator to build partial equivalence relations from a predicate and an equivalence relation\<close>
+
+theory Combine_PER
+imports Main "~~/src/HOL/Library/Lattice_Syntax"
+begin
+
+definition combine_per :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+ "combine_per P R = (\<lambda>x y. P x \<and> P y) \<sqinter> R"
+
+lemma combine_per_simp [simp]:
+ fixes R (infixl "\<approx>" 50)
+ shows "combine_per P R x y \<longleftrightarrow> P x \<and> P y \<and> x \<approx> y"
+ by (simp add: combine_per_def)
+
+lemma combine_per_top [simp]:
+ "combine_per \<top> R = R"
+ by (simp add: fun_eq_iff)
+
+lemma combine_per_eq [simp]:
+ "combine_per P HOL.eq = HOL.eq \<sqinter> (\<lambda>x y. P x)"
+ by (auto simp add: fun_eq_iff)
+
+lemma symp_combine_per:
+ "symp R \<Longrightarrow> symp (combine_per P R)"
+ by (auto simp add: symp_def sym_def combine_per_def)
+
+lemma transp_combine_per:
+ "transp R \<Longrightarrow> transp (combine_per P R)"
+ by (auto simp add: transp_def trans_def combine_per_def)
+
+lemma combine_perI:
+ fixes R (infixl "\<approx>" 50)
+ shows "P x \<Longrightarrow> P y \<Longrightarrow> x \<approx> y \<Longrightarrow> combine_per P R x y"
+ by (simp add: combine_per_def)
+
+lemma symp_combine_per_symp:
+ "symp R \<Longrightarrow> symp (combine_per P R)"
+ by (auto intro!: sympI elim: sympE)
+
+lemma transp_combine_per_transp:
+ "transp R \<Longrightarrow> transp (combine_per P R)"
+ by (auto intro!: transpI elim: transpE)
+
+lemma equivp_combine_per_part_equivp:
+ fixes R (infixl "\<approx>" 50)
+ assumes "\<exists>x. P x" and "equivp R"
+ shows "part_equivp (combine_per P R)"
+proof -
+ from \<open>\<exists>x. P x\<close> obtain x where "P x" ..
+ moreover from \<open>equivp R\<close> have "x \<approx> x" by (rule equivp_reflp)
+ ultimately have "\<exists>x. P x \<and> x \<approx> x" by blast
+ with \<open>equivp R\<close> show ?thesis
+ by (auto intro!: part_equivpI symp_combine_per_symp transp_combine_per_transp
+ elim: equivpE)
+qed
+
+end
\ No newline at end of file
--- a/src/HOL/Library/Dlist.thy Mon Jul 04 20:48:55 2016 +0200
+++ b/src/HOL/Library/Dlist.thy Mon Jul 04 20:51:04 2016 +0200
@@ -67,6 +67,9 @@
qualified definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
"filter P dxs = Dlist (List.filter P (list_of_dlist dxs))"
+qualified definition rotate :: "nat \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
+ "rotate n dxs = Dlist (List.rotate n (list_of_dlist dxs))"
+
end
@@ -115,6 +118,10 @@
"list_of_dlist (Dlist.filter P dxs) = List.filter P (list_of_dlist dxs)"
by (simp add: Dlist.filter_def)
+lemma list_of_dlist_rotate [simp, code abstract]:
+ "list_of_dlist (Dlist.rotate n dxs) = List.rotate n (list_of_dlist dxs)"
+ by (simp add: Dlist.rotate_def)
+
text \<open>Explicit executable conversion\<close>
--- a/src/HOL/Library/Library.thy Mon Jul 04 20:48:55 2016 +0200
+++ b/src/HOL/Library/Library.thy Mon Jul 04 20:51:04 2016 +0200
@@ -12,6 +12,7 @@
Code_Test
ContNotDenum
Convex
+ Combine_PER
Complete_Partial_Order2
Countable
Countable_Complete_Lattices
@@ -55,6 +56,7 @@
Option_ord
Order_Continuity
Parallel
+ Perm
Permutation
Permutations
Polynomial
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Perm.thy Mon Jul 04 20:51:04 2016 +0200
@@ -0,0 +1,807 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+section \<open>Permutations as abstract type\<close>
+
+theory Perm
+imports Main
+begin
+
+text \<open>
+ This theory introduces basics about permutations, i.e. almost
+ everywhere fix bijections. But it is by no means complete.
+ Grieviously missing are cycles since these would require more
+ elaboration, e.g. the concept of distinct lists equivalent
+ under rotation, which maybe would also deserve its own theory.
+ But see theory @{text "src/HOL/ex/Perm_Fragments.thy"} for
+ fragments on that.
+\<close>
+
+subsection \<open>Abstract type of permutations\<close>
+
+typedef 'a perm = "{f :: 'a \<Rightarrow> 'a. bij f \<and> finite {a. f a \<noteq> a}}"
+ morphisms "apply" Perm
+ by (rule exI [of _ id]) simp
+
+setup_lifting type_definition_perm
+
+notation "apply" (infixl "\<langle>$\<rangle>" 999)
+no_notation "apply" ("op \<langle>$\<rangle>")
+
+lemma bij_apply [simp]:
+ "bij (apply f)"
+ using "apply" [of f] by simp
+
+lemma perm_eqI:
+ assumes "\<And>a. f \<langle>$\<rangle> a = g \<langle>$\<rangle> a"
+ shows "f = g"
+ using assms by transfer (simp add: fun_eq_iff)
+
+lemma perm_eq_iff:
+ "f = g \<longleftrightarrow> (\<forall>a. f \<langle>$\<rangle> a = g \<langle>$\<rangle> a)"
+ by (auto intro: perm_eqI)
+
+lemma apply_inj:
+ "f \<langle>$\<rangle> a = f \<langle>$\<rangle> b \<longleftrightarrow> a = b"
+ by (rule inj_eq) (rule bij_is_inj, simp)
+
+lift_definition affected :: "'a perm \<Rightarrow> 'a set"
+ is "\<lambda>f. {a. f a \<noteq> a}" .
+
+lemma in_affected:
+ "a \<in> affected f \<longleftrightarrow> f \<langle>$\<rangle> a \<noteq> a"
+ by transfer simp
+
+lemma finite_affected [simp]:
+ "finite (affected f)"
+ by transfer simp
+
+lemma apply_affected [simp]:
+ "f \<langle>$\<rangle> a \<in> affected f \<longleftrightarrow> a \<in> affected f"
+proof transfer
+ fix f :: "'a \<Rightarrow> 'a" and a :: 'a
+ assume "bij f \<and> finite {b. f b \<noteq> b}"
+ then have "bij f" by simp
+ interpret bijection f by standard (rule \<open>bij f\<close>)
+ have "f a \<in> {a. f a = a} \<longleftrightarrow> a \<in> {a. f a = a}" (is "?P \<longleftrightarrow> ?Q")
+ by auto
+ then show "f a \<in> {a. f a \<noteq> a} \<longleftrightarrow> a \<in> {a. f a \<noteq> a}"
+ by simp
+qed
+
+lemma card_affected_not_one:
+ "card (affected f) \<noteq> 1"
+proof
+ interpret bijection "apply f"
+ by standard (rule bij_apply)
+ assume "card (affected f) = 1"
+ then obtain a where *: "affected f = {a}"
+ by (rule card_1_singletonE)
+ then have "f \<langle>$\<rangle> a \<noteq> a"
+ by (simp add: in_affected [symmetric])
+ moreover with * have "f \<langle>$\<rangle> a \<notin> affected f"
+ by simp
+ then have "f \<langle>$\<rangle> (f \<langle>$\<rangle> a) = f \<langle>$\<rangle> a"
+ by (simp add: in_affected)
+ then have "inv (apply f) (f \<langle>$\<rangle> (f \<langle>$\<rangle> a)) = inv (apply f) (f \<langle>$\<rangle> a)"
+ by simp
+ ultimately show False by simp
+qed
+
+
+subsection \<open>Identity, composition and inversion\<close>
+
+instantiation Perm.perm :: (type) "{monoid_mult, inverse}"
+begin
+
+lift_definition one_perm :: "'a perm"
+ is id
+ by simp
+
+lemma apply_one [simp]:
+ "apply 1 = id"
+ by (fact one_perm.rep_eq)
+
+lemma affected_one [simp]:
+ "affected 1 = {}"
+ by transfer simp
+
+lemma affected_empty_iff [simp]:
+ "affected f = {} \<longleftrightarrow> f = 1"
+ by transfer auto
+
+lift_definition times_perm :: "'a perm \<Rightarrow> 'a perm \<Rightarrow> 'a perm"
+ is comp
+proof
+ fix f g :: "'a \<Rightarrow> 'a"
+ assume "bij f \<and> finite {a. f a \<noteq> a}"
+ "bij g \<and>finite {a. g a \<noteq> a}"
+ then have "finite ({a. f a \<noteq> a} \<union> {a. g a \<noteq> a})"
+ by simp
+ moreover have "{a. (f \<circ> g) a \<noteq> a} \<subseteq> {a. f a \<noteq> a} \<union> {a. g a \<noteq> a}"
+ by auto
+ ultimately show "finite {a. (f \<circ> g) a \<noteq> a}"
+ by (auto intro: finite_subset)
+qed (auto intro: bij_comp)
+
+lemma apply_times:
+ "apply (f * g) = apply f \<circ> apply g"
+ by (fact times_perm.rep_eq)
+
+lemma apply_sequence:
+ "f \<langle>$\<rangle> (g \<langle>$\<rangle> a) = apply (f * g) a"
+ by (simp add: apply_times)
+
+lemma affected_times [simp]:
+ "affected (f * g) \<subseteq> affected f \<union> affected g"
+ by transfer auto
+
+lift_definition inverse_perm :: "'a perm \<Rightarrow> 'a perm"
+ is inv
+proof transfer
+ fix f :: "'a \<Rightarrow> 'a" and a
+ assume "bij f \<and> finite {b. f b \<noteq> b}"
+ then have "bij f" and fin: "finite {b. f b \<noteq> b}"
+ by auto
+ interpret bijection f by standard (rule \<open>bij f\<close>)
+ from fin show "bij (inv f) \<and> finite {a. inv f a \<noteq> a}"
+ by (simp add: bij_inv)
+qed
+
+instance
+ by standard (transfer; simp add: comp_assoc)+
+
+end
+
+lemma apply_inverse:
+ "apply (inverse f) = inv (apply f)"
+ by (fact inverse_perm.rep_eq)
+
+lemma affected_inverse [simp]:
+ "affected (inverse f) = affected f"
+proof transfer
+ fix f :: "'a \<Rightarrow> 'a" and a
+ assume "bij f \<and> finite {b. f b \<noteq> b}"
+ then have "bij f" by simp
+ interpret bijection f by standard (rule \<open>bij f\<close>)
+ show "{a. inv f a \<noteq> a} = {a. f a \<noteq> a}"
+ by simp
+qed
+
+global_interpretation perm: group times "1::'a perm" inverse
+proof
+ fix f :: "'a perm"
+ show "1 * f = f"
+ by transfer simp
+ show "inverse f * f = 1"
+ proof transfer
+ fix f :: "'a \<Rightarrow> 'a" and a
+ assume "bij f \<and> finite {b. f b \<noteq> b}"
+ then have "bij f" by simp
+ interpret bijection f by standard (rule \<open>bij f\<close>)
+ show "inv f \<circ> f = id"
+ by simp
+ qed
+qed
+
+declare perm.inverse_distrib_swap [simp]
+
+lemma perm_mult_commute:
+ assumes "affected f \<inter> affected g = {}"
+ shows "g * f = f * g"
+proof (rule perm_eqI)
+ fix a
+ from assms have *: "a \<in> affected f \<Longrightarrow> a \<notin> affected g"
+ "a \<in> affected g \<Longrightarrow> a \<notin> affected f" for a
+ by auto
+ consider "a \<in> affected f \<and> a \<notin> affected g
+ \<and> f \<langle>$\<rangle> a \<in> affected f"
+ | "a \<notin> affected f \<and> a \<in> affected g
+ \<and> f \<langle>$\<rangle> a \<notin> affected f"
+ | "a \<notin> affected f \<and> a \<notin> affected g"
+ using assms by auto
+ then show "(g * f) \<langle>$\<rangle> a = (f * g) \<langle>$\<rangle> a"
+ proof cases
+ case 1 moreover with * have "f \<langle>$\<rangle> a \<notin> affected g"
+ by auto
+ ultimately show ?thesis by (simp add: in_affected apply_times)
+ next
+ case 2 moreover with * have "g \<langle>$\<rangle> a \<notin> affected f"
+ by auto
+ ultimately show ?thesis by (simp add: in_affected apply_times)
+ next
+ case 3 then show ?thesis by (simp add: in_affected apply_times)
+ qed
+qed
+
+lemma apply_power:
+ "apply (f ^ n) = apply f ^^ n"
+ by (induct n) (simp_all add: apply_times)
+
+lemma perm_power_inverse:
+ "inverse f ^ n = inverse ((f :: 'a perm) ^ n)"
+proof (induct n)
+ case 0 then show ?case by simp
+next
+ case (Suc n)
+ then show ?case
+ unfolding power_Suc2 [of f] by simp
+qed
+
+
+subsection \<open>Orbit and order of elements\<close>
+
+definition orbit :: "'a perm \<Rightarrow> 'a \<Rightarrow> 'a set"
+where
+ "orbit f a = range (\<lambda>n. (f ^ n) \<langle>$\<rangle> a)"
+
+lemma in_orbitI:
+ assumes "(f ^ n) \<langle>$\<rangle> a = b"
+ shows "b \<in> orbit f a"
+ using assms by (auto simp add: orbit_def)
+
+lemma apply_power_self_in_orbit [simp]:
+ "(f ^ n) \<langle>$\<rangle> a \<in> orbit f a"
+ by (rule in_orbitI) rule
+
+lemma in_orbit_self [simp]:
+ "a \<in> orbit f a"
+ using apply_power_self_in_orbit [of _ 0] by simp
+
+lemma apply_self_in_orbit [simp]:
+ "f \<langle>$\<rangle> a \<in> orbit f a"
+ using apply_power_self_in_orbit [of _ 1] by simp
+
+lemma orbit_not_empty [simp]:
+ "orbit f a \<noteq> {}"
+ using in_orbit_self [of a f] by blast
+
+lemma not_in_affected_iff_orbit_eq_singleton:
+ "a \<notin> affected f \<longleftrightarrow> orbit f a = {a}" (is "?P \<longleftrightarrow> ?Q")
+proof
+ assume ?P
+ then have "f \<langle>$\<rangle> a = a"
+ by (simp add: in_affected)
+ then have "(f ^ n) \<langle>$\<rangle> a = a" for n
+ by (induct n) (simp_all add: apply_times)
+ then show ?Q
+ by (auto simp add: orbit_def)
+next
+ assume ?Q
+ then show ?P
+ by (auto simp add: orbit_def in_affected dest: range_eq_singletonD [of _ _ 1])
+qed
+
+definition order :: "'a perm \<Rightarrow> 'a \<Rightarrow> nat"
+where
+ "order f = card \<circ> orbit f"
+
+lemma orbit_subset_eq_affected:
+ assumes "a \<in> affected f"
+ shows "orbit f a \<subseteq> affected f"
+proof (rule ccontr)
+ assume "\<not> orbit f a \<subseteq> affected f"
+ then obtain b where "b \<in> orbit f a" and "b \<notin> affected f"
+ by auto
+ then have "b \<in> range (\<lambda>n. (f ^ n) \<langle>$\<rangle> a)"
+ by (simp add: orbit_def)
+ then obtain n where "b = (f ^ n) \<langle>$\<rangle> a"
+ by blast
+ with \<open>b \<notin> affected f\<close>
+ have "(f ^ n) \<langle>$\<rangle> a \<notin> affected f"
+ by simp
+ then have "f \<langle>$\<rangle> a \<notin> affected f"
+ by (induct n) (simp_all add: apply_times)
+ with assms show False
+ by simp
+qed
+
+lemma finite_orbit [simp]:
+ "finite (orbit f a)"
+proof (cases "a \<in> affected f")
+ case False then show ?thesis
+ by (simp add: not_in_affected_iff_orbit_eq_singleton)
+next
+ case True then have "orbit f a \<subseteq> affected f"
+ by (rule orbit_subset_eq_affected)
+ then show ?thesis using finite_affected
+ by (rule finite_subset)
+qed
+
+lemma orbit_1 [simp]:
+ "orbit 1 a = {a}"
+ by (auto simp add: orbit_def)
+
+lemma order_1 [simp]:
+ "order 1 a = 1"
+ unfolding order_def by simp
+
+lemma card_orbit_eq [simp]:
+ "card (orbit f a) = order f a"
+ by (simp add: order_def)
+
+lemma order_greater_zero [simp]:
+ "order f a > 0"
+ by (simp only: card_gt_0_iff order_def comp_def) simp
+
+lemma order_eq_one_iff:
+ "order f a = Suc 0 \<longleftrightarrow> a \<notin> affected f" (is "?P \<longleftrightarrow> ?Q")
+proof
+ assume ?P then have "card (orbit f a) = 1"
+ by simp
+ then obtain b where "orbit f a = {b}"
+ by (rule card_1_singletonE)
+ with in_orbit_self [of a f]
+ have "b = a" by simp
+ with \<open>orbit f a = {b}\<close> show ?Q
+ by (simp add: not_in_affected_iff_orbit_eq_singleton)
+next
+ assume ?Q
+ then have "orbit f a = {a}"
+ by (simp add: not_in_affected_iff_orbit_eq_singleton)
+ then have "card (orbit f a) = 1"
+ by simp
+ then show ?P
+ by simp
+qed
+
+lemma order_greater_eq_two_iff:
+ "order f a \<ge> 2 \<longleftrightarrow> a \<in> affected f"
+ using order_eq_one_iff [of f a]
+ apply (auto simp add: neq_iff)
+ using order_greater_zero [of f a]
+ apply simp
+ done
+
+lemma order_less_eq_affected:
+ assumes "f \<noteq> 1"
+ shows "order f a \<le> card (affected f)"
+proof (cases "a \<in> affected f")
+ from assms have "affected f \<noteq> {}"
+ by simp
+ then obtain B b where "affected f = insert b B"
+ by blast
+ with finite_affected [of f] have "card (affected f) \<ge> 1"
+ by (simp add: card_insert)
+ case False then have "order f a = 1"
+ by (simp add: order_eq_one_iff)
+ with \<open>card (affected f) \<ge> 1\<close> show ?thesis
+ by simp
+next
+ case True
+ have "card (orbit f a) \<le> card (affected f)"
+ by (rule card_mono) (simp_all add: True orbit_subset_eq_affected card_mono)
+ then show ?thesis
+ by simp
+qed
+
+lemma affected_order_greater_eq_two:
+ assumes "a \<in> affected f"
+ shows "order f a \<ge> 2"
+proof (rule ccontr)
+ assume "\<not> 2 \<le> order f a"
+ then have "order f a < 2"
+ by (simp add: not_le)
+ with order_greater_zero [of f a] have "order f a = 1"
+ by arith
+ with assms show False
+ by (simp add: order_eq_one_iff)
+qed
+
+lemma order_witness_unfold:
+ assumes "n > 0" and "(f ^ n) \<langle>$\<rangle> a = a"
+ shows "order f a = card ((\<lambda>m. (f ^ m) \<langle>$\<rangle> a) ` {0..<n})"
+proof -
+ have "orbit f a = (\<lambda>m. (f ^ m) \<langle>$\<rangle> a) ` {0..<n}" (is "_ = ?B")
+ proof (rule set_eqI, rule)
+ fix b
+ assume "b \<in> orbit f a"
+ then obtain m where "(f ^ m) \<langle>$\<rangle> a = b"
+ by (auto simp add: orbit_def)
+ then have "b = (f ^ (m mod n + n * (m div n))) \<langle>$\<rangle> a"
+ by simp
+ also have "\<dots> = (f ^ (m mod n)) \<langle>$\<rangle> ((f ^ (n * (m div n))) \<langle>$\<rangle> a)"
+ by (simp only: power_add apply_times) simp
+ also have "(f ^ (n * q)) \<langle>$\<rangle> a = a" for q
+ by (induct q)
+ (simp_all add: power_add apply_times assms)
+ finally have "b = (f ^ (m mod n)) \<langle>$\<rangle> a" .
+ moreover from \<open>n > 0\<close>
+ have "m mod n < n"
+ by simp
+ ultimately show "b \<in> ?B"
+ by auto
+ next
+ fix b
+ assume "b \<in> ?B"
+ then obtain m where "(f ^ m) \<langle>$\<rangle> a = b"
+ by blast
+ then show "b \<in> orbit f a"
+ by (rule in_orbitI)
+ qed
+ then have "card (orbit f a) = card ?B"
+ by (simp only:)
+ then show ?thesis
+ by simp
+qed
+
+lemma inj_on_apply_range:
+ "inj_on (\<lambda>m. (f ^ m) \<langle>$\<rangle> a) {..<order f a}"
+proof -
+ have "inj_on (\<lambda>m. (f ^ m) \<langle>$\<rangle> a) {..<n}"
+ if "n \<le> order f a" for n
+ using that proof (induct n)
+ case 0 then show ?case by simp
+ next
+ case (Suc n)
+ then have prem: "n < order f a"
+ by simp
+ with Suc.hyps have hyp: "inj_on (\<lambda>m. (f ^ m) \<langle>$\<rangle> a) {..<n}"
+ by simp
+ have "(f ^ n) \<langle>$\<rangle> a \<notin> (\<lambda>m. (f ^ m) \<langle>$\<rangle> a) ` {..<n}"
+ proof
+ assume "(f ^ n) \<langle>$\<rangle> a \<in> (\<lambda>m. (f ^ m) \<langle>$\<rangle> a) ` {..<n}"
+ then obtain m where *: "(f ^ m) \<langle>$\<rangle> a = (f ^ n) \<langle>$\<rangle> a" and "m < n"
+ by auto
+ interpret bijection "apply (f ^ m)"
+ by standard simp
+ from \<open>m < n\<close> have "n = m + (n - m)"
+ and nm: "0 < n - m" "n - m \<le> n"
+ by arith+
+ with * have "(f ^ m) \<langle>$\<rangle> a = (f ^ (m + (n - m))) \<langle>$\<rangle> a"
+ by simp
+ then have "(f ^ m) \<langle>$\<rangle> a = (f ^ m) \<langle>$\<rangle> ((f ^ (n - m)) \<langle>$\<rangle> a)"
+ by (simp add: power_add apply_times)
+ then have "(f ^ (n - m)) \<langle>$\<rangle> a = a"
+ by simp
+ with \<open>n - m > 0\<close>
+ have "order f a = card ((\<lambda>m. (f ^ m) \<langle>$\<rangle> a) ` {0..<n - m})"
+ by (rule order_witness_unfold)
+ also have "card ((\<lambda>m. (f ^ m) \<langle>$\<rangle> a) ` {0..<n - m}) \<le> card {0..<n - m}"
+ by (rule card_image_le) simp
+ finally have "order f a \<le> n - m"
+ by simp
+ with prem show False by simp
+ qed
+ with hyp show ?case
+ by (simp add: lessThan_Suc)
+ qed
+ then show ?thesis by simp
+qed
+
+lemma orbit_unfold_image:
+ "orbit f a = (\<lambda>n. (f ^ n) \<langle>$\<rangle> a) ` {..<order f a}" (is "_ = ?A")
+proof (rule sym, rule card_subset_eq)
+ show "finite (orbit f a)"
+ by simp
+ show "?A \<subseteq> orbit f a"
+ by (auto simp add: orbit_def)
+ from inj_on_apply_range [of f a]
+ have "card ?A = order f a"
+ by (auto simp add: card_image)
+ then show "card ?A = card (orbit f a)"
+ by simp
+qed
+
+lemma in_orbitE:
+ assumes "b \<in> orbit f a"
+ obtains n where "b = (f ^ n) \<langle>$\<rangle> a" and "n < order f a"
+ using assms unfolding orbit_unfold_image by blast
+
+lemma apply_power_order [simp]:
+ "(f ^ order f a) \<langle>$\<rangle> a = a"
+proof -
+ have "(f ^ order f a) \<langle>$\<rangle> a \<in> orbit f a"
+ by simp
+ then obtain n where
+ *: "(f ^ order f a) \<langle>$\<rangle> a = (f ^ n) \<langle>$\<rangle> a"
+ and "n < order f a"
+ by (rule in_orbitE)
+ show ?thesis
+ proof (cases n)
+ case 0 with * show ?thesis by simp
+ next
+ case (Suc m)
+ from order_greater_zero [of f a]
+ have "Suc (order f a - 1) = order f a"
+ by arith
+ from Suc \<open>n < order f a\<close>
+ have "m < order f a"
+ by simp
+ with Suc *
+ have "(inverse f) \<langle>$\<rangle> ((f ^ Suc (order f a - 1)) \<langle>$\<rangle> a) =
+ (inverse f) \<langle>$\<rangle> ((f ^ Suc m) \<langle>$\<rangle> a)"
+ by simp
+ then have "(f ^ (order f a - 1)) \<langle>$\<rangle> a =
+ (f ^ m) \<langle>$\<rangle> a"
+ by (simp only: power_Suc apply_times)
+ (simp add: apply_sequence mult.assoc [symmetric])
+ with inj_on_apply_range
+ have "order f a - 1 = m"
+ by (rule inj_onD)
+ (simp_all add: \<open>m < order f a\<close>)
+ with Suc have "n = order f a"
+ by auto
+ with \<open>n < order f a\<close>
+ show ?thesis by simp
+ qed
+qed
+
+lemma apply_power_left_mult_order [simp]:
+ "(f ^ (n * order f a)) \<langle>$\<rangle> a = a"
+ by (induct n) (simp_all add: power_add apply_times)
+
+lemma apply_power_right_mult_order [simp]:
+ "(f ^ (order f a * n)) \<langle>$\<rangle> a = a"
+ by (simp add: ac_simps)
+
+lemma apply_power_mod_order_eq [simp]:
+ "(f ^ (n mod order f a)) \<langle>$\<rangle> a = (f ^ n) \<langle>$\<rangle> a"
+proof -
+ have "(f ^ n) \<langle>$\<rangle> a = (f ^ (n mod order f a + order f a * (n div order f a))) \<langle>$\<rangle> a"
+ by simp
+ also have "\<dots> = (f ^ (n mod order f a) * f ^ (order f a * (n div order f a))) \<langle>$\<rangle> a"
+ by (simp add: power_add [symmetric])
+ finally show ?thesis
+ by (simp add: apply_times)
+qed
+
+lemma apply_power_eq_iff:
+ "(f ^ m) \<langle>$\<rangle> a = (f ^ n) \<langle>$\<rangle> a \<longleftrightarrow> m mod order f a = n mod order f a" (is "?P \<longleftrightarrow> ?Q")
+proof
+ assume ?Q
+ then have "(f ^ (m mod order f a)) \<langle>$\<rangle> a = (f ^ (n mod order f a)) \<langle>$\<rangle> a"
+ by simp
+ then show ?P
+ by simp
+next
+ assume ?P
+ then have "(f ^ (m mod order f a)) \<langle>$\<rangle> a = (f ^ (n mod order f a)) \<langle>$\<rangle> a"
+ by simp
+ with inj_on_apply_range
+ show ?Q
+ by (rule inj_onD) simp_all
+qed
+
+lemma apply_inverse_eq_apply_power_order_minus_one:
+ "(inverse f) \<langle>$\<rangle> a = (f ^ (order f a - 1)) \<langle>$\<rangle> a"
+proof (cases "order f a")
+ case 0 with order_greater_zero [of f a] show ?thesis
+ by simp
+next
+ case (Suc n)
+ moreover have "(f ^ order f a) \<langle>$\<rangle> a = a"
+ by simp
+ then have *: "(inverse f) \<langle>$\<rangle> ((f ^ order f a) \<langle>$\<rangle> a) = (inverse f) \<langle>$\<rangle> a"
+ by simp
+ ultimately show ?thesis
+ by (simp add: apply_sequence mult.assoc [symmetric])
+qed
+
+lemma apply_inverse_self_in_orbit [simp]:
+ "(inverse f) \<langle>$\<rangle> a \<in> orbit f a"
+ using apply_inverse_eq_apply_power_order_minus_one [symmetric]
+ by (rule in_orbitI)
+
+lemma apply_inverse_power_eq:
+ "(inverse (f ^ n)) \<langle>$\<rangle> a = (f ^ (order f a - n mod order f a)) \<langle>$\<rangle> a"
+proof (induct n)
+ case 0 then show ?case by simp
+next
+ case (Suc n)
+ define m where "m = order f a - n mod order f a - 1"
+ moreover have "order f a - n mod order f a > 0"
+ by simp
+ ultimately have "order f a - n mod order f a = Suc m"
+ by arith
+ moreover from this have m2: "order f a - Suc n mod order f a = (if m = 0 then order f a else m)"
+ by (auto simp add: mod_Suc)
+ ultimately show ?case
+ using Suc
+ by (simp_all add: apply_times power_Suc2 [of _ n] power_Suc [of _ m] del: power_Suc)
+ (simp add: apply_sequence mult.assoc [symmetric])
+qed
+
+lemma apply_power_eq_self_iff:
+ "(f ^ n) \<langle>$\<rangle> a = a \<longleftrightarrow> order f a dvd n"
+ using apply_power_eq_iff [of f n a 0]
+ by (simp add: mod_eq_0_iff_dvd)
+
+lemma orbit_equiv:
+ assumes "b \<in> orbit f a"
+ shows "orbit f b = orbit f a" (is "?B = ?A")
+proof
+ from assms obtain n where "n < order f a" and b: "b = (f ^ n) \<langle>$\<rangle> a"
+ by (rule in_orbitE)
+ then show "?B \<subseteq> ?A"
+ by (auto simp add: apply_sequence power_add [symmetric] intro: in_orbitI elim!: in_orbitE)
+ from b have "(inverse (f ^ n)) \<langle>$\<rangle> b = (inverse (f ^ n)) \<langle>$\<rangle> ((f ^ n) \<langle>$\<rangle> a)"
+ by simp
+ then have a: "a = (inverse (f ^ n)) \<langle>$\<rangle> b"
+ by (simp add: apply_sequence)
+ then show "?A \<subseteq> ?B"
+ apply (auto simp add: apply_sequence power_add [symmetric] intro: in_orbitI elim!: in_orbitE)
+ unfolding apply_times comp_def apply_inverse_power_eq
+ unfolding apply_sequence power_add [symmetric]
+ apply (rule in_orbitI) apply rule
+ done
+qed
+
+lemma orbit_apply [simp]:
+ "orbit f (f \<langle>$\<rangle> a) = orbit f a"
+ by (rule orbit_equiv) simp
+
+lemma order_apply [simp]:
+ "order f (f \<langle>$\<rangle> a) = order f a"
+ by (simp only: order_def comp_def orbit_apply)
+
+lemma orbit_apply_inverse [simp]:
+ "orbit f (inverse f \<langle>$\<rangle> a) = orbit f a"
+ by (rule orbit_equiv) simp
+
+lemma order_apply_inverse [simp]:
+ "order f (inverse f \<langle>$\<rangle> a) = order f a"
+ by (simp only: order_def comp_def orbit_apply_inverse)
+
+lemma orbit_apply_power [simp]:
+ "orbit f ((f ^ n) \<langle>$\<rangle> a) = orbit f a"
+ by (rule orbit_equiv) simp
+
+lemma order_apply_power [simp]:
+ "order f ((f ^ n) \<langle>$\<rangle> a) = order f a"
+ by (simp only: order_def comp_def orbit_apply_power)
+
+lemma orbit_inverse [simp]:
+ "orbit (inverse f) = orbit f"
+proof (rule ext, rule set_eqI, rule)
+ fix b a
+ assume "b \<in> orbit f a"
+ then obtain n where b: "b = (f ^ n) \<langle>$\<rangle> a" "n < order f a"
+ by (rule in_orbitE)
+ then have "b = apply (inverse (inverse f) ^ n) a"
+ by simp
+ then have "b = apply (inverse (inverse f ^ n)) a"
+ by (simp add: perm_power_inverse)
+ then have "b = apply (inverse f ^ (n * (order (inverse f ^ n) a - 1))) a"
+ by (simp add: apply_inverse_eq_apply_power_order_minus_one power_mult)
+ then show "b \<in> orbit (inverse f) a"
+ by simp
+next
+ fix b a
+ assume "b \<in> orbit (inverse f) a"
+ then show "b \<in> orbit f a"
+ by (rule in_orbitE)
+ (simp add: apply_inverse_eq_apply_power_order_minus_one
+ perm_power_inverse power_mult [symmetric])
+qed
+
+lemma order_inverse [simp]:
+ "order (inverse f) = order f"
+ by (simp add: order_def)
+
+lemma orbit_disjoint:
+ assumes "orbit f a \<noteq> orbit f b"
+ shows "orbit f a \<inter> orbit f b = {}"
+proof (rule ccontr)
+ assume "orbit f a \<inter> orbit f b \<noteq> {}"
+ then obtain c where "c \<in> orbit f a \<inter> orbit f b"
+ by blast
+ then have "c \<in> orbit f a" and "c \<in> orbit f b"
+ by auto
+ then obtain m n where "c = (f ^ m) \<langle>$\<rangle> a"
+ and "c = apply (f ^ n) b" by (blast elim!: in_orbitE)
+ then have "(f ^ m) \<langle>$\<rangle> a = apply (f ^ n) b"
+ by simp
+ then have "apply (inverse f ^ m) ((f ^ m) \<langle>$\<rangle> a) =
+ apply (inverse f ^ m) (apply (f ^ n) b)"
+ by simp
+ then have *: "apply (inverse f ^ m * f ^ n) b = a"
+ by (simp add: apply_sequence perm_power_inverse)
+ have "a \<in> orbit f b"
+ proof (cases n m rule: linorder_cases)
+ case equal with * show ?thesis
+ by (simp add: perm_power_inverse)
+ next
+ case less
+ moreover define q where "q = m - n"
+ ultimately have "m = q + n" by arith
+ with * have "apply (inverse f ^ q) b = a"
+ by (simp add: power_add mult.assoc perm_power_inverse)
+ then have "a \<in> orbit (inverse f) b"
+ by (rule in_orbitI)
+ then show ?thesis
+ by simp
+ next
+ case greater
+ moreover define q where "q = n - m"
+ ultimately have "n = m + q" by arith
+ with * have "apply (f ^ q) b = a"
+ by (simp add: power_add mult.assoc [symmetric] perm_power_inverse)
+ then show ?thesis
+ by (rule in_orbitI)
+ qed
+ with assms show False
+ by (auto dest: orbit_equiv)
+qed
+
+
+subsection \<open>Swaps\<close>
+
+lift_definition swap :: "'a \<Rightarrow> 'a \<Rightarrow> 'a perm" ("\<langle>_\<leftrightarrow>_\<rangle>")
+ is "\<lambda>a b. Fun.swap a b id"
+proof
+ fix a b :: 'a
+ have "{c. Fun.swap a b id c \<noteq> c} \<subseteq> {a, b}"
+ by (auto simp add: Fun.swap_def)
+ then show "finite {c. Fun.swap a b id c \<noteq> c}"
+ by (rule finite_subset) simp
+qed simp
+
+lemma apply_swap_simp [simp]:
+ "\<langle>a\<leftrightarrow>b\<rangle> \<langle>$\<rangle> a = b"
+ "\<langle>a\<leftrightarrow>b\<rangle> \<langle>$\<rangle> b = a"
+ by (transfer; simp)+
+
+lemma apply_swap_same [simp]:
+ "c \<noteq> a \<Longrightarrow> c \<noteq> b \<Longrightarrow> \<langle>a\<leftrightarrow>b\<rangle> \<langle>$\<rangle> c = c"
+ by transfer simp
+
+lemma apply_swap_eq_iff [simp]:
+ "\<langle>a\<leftrightarrow>b\<rangle> \<langle>$\<rangle> c = a \<longleftrightarrow> c = b"
+ "\<langle>a\<leftrightarrow>b\<rangle> \<langle>$\<rangle> c = b \<longleftrightarrow> c = a"
+ by (transfer; auto simp add: Fun.swap_def)+
+
+lemma swap_1 [simp]:
+ "\<langle>a\<leftrightarrow>a\<rangle> = 1"
+ by transfer simp
+
+lemma swap_sym:
+ "\<langle>b\<leftrightarrow>a\<rangle> = \<langle>a\<leftrightarrow>b\<rangle>"
+ by (transfer; auto simp add: Fun.swap_def)+
+
+lemma swap_self [simp]:
+ "\<langle>a\<leftrightarrow>b\<rangle> * \<langle>a\<leftrightarrow>b\<rangle> = 1"
+ by transfer (simp add: Fun.swap_def fun_eq_iff)
+
+lemma affected_swap:
+ "a \<noteq> b \<Longrightarrow> affected \<langle>a\<leftrightarrow>b\<rangle> = {a, b}"
+ by transfer (auto simp add: Fun.swap_def)
+
+lemma inverse_swap [simp]:
+ "inverse \<langle>a\<leftrightarrow>b\<rangle> = \<langle>a\<leftrightarrow>b\<rangle>"
+ by transfer (auto intro: inv_equality simp: Fun.swap_def)
+
+
+subsection \<open>Permutations specified by cycles\<close>
+
+fun cycle :: "'a list \<Rightarrow> 'a perm" ("\<langle>_\<rangle>")
+where
+ "\<langle>[]\<rangle> = 1"
+| "\<langle>[a]\<rangle> = 1"
+| "\<langle>a # b # as\<rangle> = \<langle>a # as\<rangle> * \<langle>a\<leftrightarrow>b\<rangle>"
+
+text \<open>
+ We do not continue and restrict ourselves to syntax from here.
+ See also introductory note.
+\<close>
+
+
+subsection \<open>Syntax\<close>
+
+bundle no_permutation_syntax
+begin
+ no_notation swap ("\<langle>_\<leftrightarrow>_\<rangle>")
+ no_notation cycle ("\<langle>_\<rangle>")
+ no_notation "apply" (infixl "\<langle>$\<rangle>" 999)
+end
+
+bundle permutation_syntax
+begin
+ notation swap ("\<langle>_\<leftrightarrow>_\<rangle>")
+ notation cycle ("\<langle>_\<rangle>")
+ notation "apply" (infixl "\<langle>$\<rangle>" 999)
+ no_notation "apply" ("op \<langle>$\<rangle>")
+end
+
+unbundle no_permutation_syntax
+
+end
--- a/src/HOL/ROOT Mon Jul 04 20:48:55 2016 +0200
+++ b/src/HOL/ROOT Mon Jul 04 20:51:04 2016 +0200
@@ -619,6 +619,7 @@
Sum_of_Powers
Sudoku
Code_Timing
+ Perm_Fragments
theories [skip_proofs = false]
Meson_Test
document_files "root.bib" "root.tex"
--- a/src/HOL/Relation.thy Mon Jul 04 20:48:55 2016 +0200
+++ b/src/HOL/Relation.thy Mon Jul 04 20:51:04 2016 +0200
@@ -51,6 +51,7 @@
declare Sup2_E [elim!]
declare SUP2_E [elim!]
+
subsection \<open>Fundamental\<close>
subsubsection \<open>Relations as sets of pairs\<close>
@@ -141,6 +142,7 @@
lemma SUP_Sup_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Union>S)"
by (simp add: fun_eq_iff)
+
subsection \<open>Properties of relations\<close>
subsubsection \<open>Reflexivity\<close>
@@ -161,7 +163,7 @@
"reflp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> refl r"
by (simp add: refl_on_def reflp_def)
-lemma refl_onI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl_on A r"
+lemma refl_onI [intro?]: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl_on A r"
by (unfold refl_on_def) (iprover intro!: ballI)
lemma refl_onD: "refl_on A r ==> a : A ==> (a, a) : r"
@@ -173,7 +175,7 @@
lemma refl_onD2: "refl_on A r ==> (x, y) : r ==> y : A"
by (unfold refl_on_def) blast
-lemma reflpI:
+lemma reflpI [intro?]:
"(\<And>x. r x x) \<Longrightarrow> reflp r"
by (auto intro: refl_onI simp add: reflp_def)
@@ -182,7 +184,7 @@
obtains "r x x"
using assms by (auto dest: refl_onD simp add: reflp_def)
-lemma reflpD:
+lemma reflpD [dest?]:
assumes "reflp r"
shows "r x x"
using assms by (auto elim: reflpE)
@@ -222,6 +224,7 @@
lemma reflp_mono: "\<lbrakk> reflp R; \<And>x y. R x y \<longrightarrow> Q x y \<rbrakk> \<Longrightarrow> reflp Q"
by(auto intro: reflpI dest: reflpD)
+
subsubsection \<open>Irreflexivity\<close>
definition irrefl :: "'a rel \<Rightarrow> bool"
@@ -236,11 +239,11 @@
"irreflp (\<lambda>a b. (a, b) \<in> R) \<longleftrightarrow> irrefl R"
by (simp add: irrefl_def irreflp_def)
-lemma irreflI:
+lemma irreflI [intro?]:
"(\<And>a. (a, a) \<notin> R) \<Longrightarrow> irrefl R"
by (simp add: irrefl_def)
-lemma irreflpI:
+lemma irreflpI [intro?]:
"(\<And>a. \<not> R a a) \<Longrightarrow> irreflp R"
by (fact irreflI [to_pred])
@@ -278,11 +281,11 @@
"symp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> sym r"
by (simp add: sym_def symp_def)
-lemma symI:
+lemma symI [intro?]:
"(\<And>a b. (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r) \<Longrightarrow> sym r"
by (unfold sym_def) iprover
-lemma sympI:
+lemma sympI [intro?]:
"(\<And>a b. r a b \<Longrightarrow> r b a) \<Longrightarrow> symp r"
by (fact symI [to_pred])
@@ -296,12 +299,12 @@
obtains "r a b"
using assms by (rule symE [to_pred])
-lemma symD:
+lemma symD [dest?]:
assumes "sym r" and "(b, a) \<in> r"
shows "(a, b) \<in> r"
using assms by (rule symE)
-lemma sympD:
+lemma sympD [dest?]:
assumes "symp r" and "r b a"
shows "r a b"
using assms by (rule symD [to_pred])
@@ -346,14 +349,14 @@
"antisym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r \<longrightarrow> x = y)"
abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
-where
+where -- \<open>FIXME proper logical operation\<close>
"antisymP r \<equiv> antisym {(x, y). r x y}"
-lemma antisymI:
+lemma antisymI [intro?]:
"(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym r"
by (unfold antisym_def) iprover
-lemma antisymD: "antisym r ==> (a, b) : r ==> (b, a) : r ==> a = b"
+lemma antisymD [dest?]: "antisym r ==> (a, b) : r ==> (b, a) : r ==> a = b"
by (unfold antisym_def) iprover
lemma antisym_subset: "r \<subseteq> s ==> antisym s ==> antisym r"
@@ -365,6 +368,7 @@
lemma antisymP_equality [simp]: "antisymP op ="
by(auto intro: antisymI)
+
subsubsection \<open>Transitivity\<close>
definition trans :: "'a rel \<Rightarrow> bool"
@@ -379,15 +383,11 @@
"transp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> trans r"
by (simp add: trans_def transp_def)
-abbreviation transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
-where \<comment> \<open>FIXME drop\<close>
- "transP r \<equiv> trans {(x, y). r x y}"
-
-lemma transI:
+lemma transI [intro?]:
"(\<And>x y z. (x, y) \<in> r \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> (x, z) \<in> r) \<Longrightarrow> trans r"
by (unfold trans_def) iprover
-lemma transpI:
+lemma transpI [intro?]:
"(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r"
by (fact transI [to_pred])
@@ -401,12 +401,12 @@
obtains "r x z"
using assms by (rule transE [to_pred])
-lemma transD:
+lemma transD [dest?]:
assumes "trans r" and "(x, y) \<in> r" and "(y, z) \<in> r"
shows "(x, z) \<in> r"
using assms by (rule transE)
-lemma transpD:
+lemma transpD [dest?]:
assumes "transp r" and "r x y" and "r y z"
shows "r x z"
using assms by (rule transD [to_pred])
@@ -436,6 +436,7 @@
lemma transp_equality [simp]: "transp op ="
by(auto intro: transpI)
+
subsubsection \<open>Totality\<close>
definition total_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
@@ -454,7 +455,8 @@
where
"single_valued r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (\<forall>z. (x, z) \<in> r \<longrightarrow> y = z))"
-abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
+abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
+where -- \<open>FIXME proper logical operation\<close>
"single_valuedP r \<equiv> single_valued {(x, y). r x y}"
lemma single_valuedI:
@@ -518,6 +520,7 @@
lemma Id_fstsnd_eq: "Id = {x. fst x = snd x}"
by force
+
subsubsection \<open>Diagonal: identity over a set\<close>
definition Id_on :: "'a set \<Rightarrow> 'a rel"
@@ -684,6 +687,7 @@
lemma OO_eq: "R OO op = = R"
by blast
+
subsubsection \<open>Converse\<close>
inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set" ("(_\<inverse>)" [1000] 999)
@@ -838,8 +842,6 @@
where
DomainI [intro]: "(a, b) \<in> r \<Longrightarrow> a \<in> Domain r"
-abbreviation (input) "DomainP \<equiv> Domainp"
-
lemmas DomainPI = Domainp.DomainI
inductive_cases DomainE [elim!]: "a \<in> Domain r"
@@ -850,8 +852,6 @@
where
RangeI [intro]: "(a, b) \<in> r \<Longrightarrow> b \<in> Range r"
-abbreviation (input) "RangeP \<equiv> Rangep"
-
lemmas RangePI = Rangep.RangeI
inductive_cases RangeE [elim!]: "b \<in> Range r"
@@ -1079,6 +1079,7 @@
lemma relcomp_Image: "(X O Y) `` Z = Y `` (X `` Z)"
by auto
+
subsubsection \<open>Inverse image\<close>
definition inv_image :: "'b rel \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a rel"
@@ -1122,6 +1123,7 @@
lemmas Powp_mono [mono] = Pow_mono [to_pred]
+
subsubsection \<open>Expressing relation operations via @{const Finite_Set.fold}\<close>
lemma Id_on_fold:
@@ -1196,4 +1198,17 @@
(auto simp: comp_fun_commute.fold_insert comp_fun_commute_relcomp_fold insert_relcomp_fold
cong: if_cong)
+text \<open>Misc\<close>
+
+abbreviation (input) transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
+where \<comment> \<open>FIXME drop\<close>
+ "transP r \<equiv> trans {(x, y). r x y}"
+
+abbreviation (input)
+ "RangeP \<equiv> Rangep"
+
+abbreviation (input)
+ "DomainP \<equiv> Domainp"
+
+
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Perm_Fragments.thy Mon Jul 04 20:51:04 2016 +0200
@@ -0,0 +1,293 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+section \<open>Fragments on permuations\<close>
+
+theory Perm_Fragments
+imports "~~/src/HOL/Library/Perm" "~~/src/HOL/Library/Dlist"
+begin
+
+unbundle permutation_syntax
+
+
+text \<open>On cycles\<close>
+
+lemma cycle_listprod:
+ "\<langle>a # as\<rangle> = listprod (map (\<lambda>b. \<langle>a\<leftrightarrow>b\<rangle>) (rev as))"
+ by (induct as) simp_all
+
+lemma cycle_append [simp]:
+ "\<langle>a # as @ bs\<rangle> = \<langle>a # bs\<rangle> * \<langle>a # as\<rangle>"
+proof (induct as rule: cycle.induct)
+ case (3 b c as)
+ then have "\<langle>a # (b # as) @ bs\<rangle> = \<langle>a # bs\<rangle> * \<langle>a # b # as\<rangle>"
+ by simp
+ then have "\<langle>a # as @ bs\<rangle> * \<langle>a\<leftrightarrow>b\<rangle> =
+ \<langle>a # bs\<rangle> * \<langle>a # as\<rangle> * \<langle>a\<leftrightarrow>b\<rangle>"
+ by (simp add: ac_simps)
+ then have "\<langle>a # as @ bs\<rangle> * \<langle>a\<leftrightarrow>b\<rangle> * \<langle>a\<leftrightarrow>b\<rangle> =
+ \<langle>a # bs\<rangle> * \<langle>a # as\<rangle> * \<langle>a\<leftrightarrow>b\<rangle> * \<langle>a\<leftrightarrow>b\<rangle>"
+ by simp
+ then have "\<langle>a # as @ bs\<rangle> = \<langle>a # bs\<rangle> * \<langle>a # as\<rangle>"
+ by (simp add: ac_simps)
+ then show "\<langle>a # (b # c # as) @ bs\<rangle> =
+ \<langle>a # bs\<rangle> * \<langle>a # b # c # as\<rangle>"
+ by (simp add: ac_simps)
+qed simp_all
+
+lemma affected_cycle:
+ "affected \<langle>as\<rangle> \<subseteq> set as"
+proof (induct as rule: cycle.induct)
+ case (3 a b as)
+ from affected_times
+ have "affected (\<langle>a # as\<rangle> * \<langle>a\<leftrightarrow>b\<rangle>)
+ \<subseteq> affected \<langle>a # as\<rangle> \<union> affected \<langle>a\<leftrightarrow>b\<rangle>" .
+ moreover from 3
+ have "affected (\<langle>a # as\<rangle>) \<subseteq> insert a (set as)"
+ by simp
+ moreover
+ have "affected \<langle>a\<leftrightarrow>b\<rangle> \<subseteq> {a, b}"
+ by (cases "a = b") (simp_all add: affected_swap)
+ ultimately have "affected (\<langle>a # as\<rangle> * \<langle>a\<leftrightarrow>b\<rangle>)
+ \<subseteq> insert a (insert b (set as))"
+ by blast
+ then show ?case by auto
+qed simp_all
+
+lemma orbit_cycle_non_elem:
+ assumes "a \<notin> set as"
+ shows "orbit \<langle>as\<rangle> 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 \<langle>as\<rangle> = \<langle>rev as\<rangle>"
+using assms proof (induct as rule: cycle.induct)
+ case (3 a b as)
+ then have *: "inverse \<langle>a # as\<rangle> = \<langle>rev (a # as)\<rangle>"
+ and distinct: "distinct (a # b # as)"
+ by simp_all
+ show " inverse \<langle>a # b # as\<rangle> = \<langle>rev (a # b # as)\<rangle>"
+ 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 **: "\<langle>a\<leftrightarrow>b\<rangle> * \<langle>c\<leftrightarrow>a\<rangle> = \<langle>c\<leftrightarrow>a\<rangle> * \<langle>c\<leftrightarrow>b\<rangle>"
+ 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 \<notin> set as"
+ shows "order \<langle>as\<rangle> a = 1"
+proof -
+ from assms have "orbit \<langle>as\<rangle> a = {a}"
+ by (rule orbit_cycle_non_elem)
+ then have "card (orbit \<langle>as\<rangle> a) = card {a}"
+ by simp
+ then show ?thesis
+ by simp
+qed
+
+lemma orbit_cycle_elem:
+ assumes "distinct as" and "a \<in> set as"
+ shows "orbit \<langle>as\<rangle> a = set as"
+ oops -- \<open>(we need rotation here\<close>
+
+lemma order_cycle_elem:
+ assumes "distinct as" and "a \<in> set as"
+ shows "order \<langle>as\<rangle> a = length as"
+ oops
+
+
+text \<open>Adding fixpoints\<close>
+
+definition fixate :: "'a \<Rightarrow> 'a perm \<Rightarrow> 'a perm"
+where
+ "fixate a f = (if a \<in> affected f then f * \<langle>apply (inverse f) a\<leftrightarrow>a\<rangle> else f)"
+
+lemma affected_fixate_trivial:
+ assumes "a \<notin> 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 \<in> affected f"
+ by simp
+ moreover have "apply (f ^ 2) a = a"
+ by (simp add: assms [symmetric])
+ ultimately show "b \<in> ?A \<longleftrightarrow> b \<in> ?B"
+ by (cases "b \<in> {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 \<in> affected f"
+ by simp
+ moreover from assms
+ have "apply f (apply f a) \<noteq> a"
+ using apply_power_eq_iff [of f 2 a 0]
+ by (simp add: power2_eq_square apply_times)
+ ultimately show "b \<in> ?A \<longleftrightarrow> b \<in> ?B"
+ by (cases "b \<in> {a, apply (inverse f) a}")
+ (auto simp add: in_affected apply_inverse apply_times fixate_def)
+qed
+
+lemma affected_fixate:
+ "affected (fixate a f) \<subseteq> affected f - {a}"
+proof -
+ have "a \<notin> affected f \<or> order f a = 2 \<or> order f a > 2"
+ by (auto simp add: not_less dest: affected_order_greater_eq_two)
+ then consider "a \<notin> 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 \<notin> orbit f a"
+ shows "orbit (fixate b f) a = orbit f a"
+ oops
+
+lemma
+ assumes "b \<in> orbit f a" and "b \<noteq> a"
+ shows "orbit (fixate b f) a = orbit f a - {b}"
+ oops
+
+
+text \<open>Distilling cycles from permutations\<close>
+
+inductive_set orbits :: "'a perm \<Rightarrow> 'a set set" for f
+where
+ in_orbitsI: "a \<in> affected f \<Longrightarrow> orbit f a \<in> 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 \<in> orbit f a"
+ assumes "a \<in> affected f"
+ shows "b \<in> affected f"
+proof (cases "a = b")
+ case True with assms show ?thesis by simp
+next
+ case False with assms have "{a, b} \<subseteq> orbit f a"
+ by auto
+ also from assms have "orbit f a \<subseteq> affected f"
+ by (blast intro!: orbit_subset_eq_affected)
+ finally show ?thesis by simp
+qed
+
+lemma Union_orbits [simp]:
+ "\<Union>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 \<in> orbits f"
+ shows "card A \<ge> 2"
+ using assms by cases
+ (auto dest: affected_order_greater_eq_two)
+
+lemma disjoint_orbits:
+ assumes "A \<in> orbits f" and "B \<in> orbits f" and "A \<noteq> B"
+ shows "A \<inter> 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 \<Rightarrow> 'a perm \<Rightarrow> 'a list"
+where
+ "trace a f = map (\<lambda>n. apply (f ^ n) a) [0..<order f a]"
+
+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 \<Rightarrow> 'a::linorder list"
+where
+ "seeds f = sorted_list_of_set (Min ` orbits f)"
+
+definition cycles :: "'a perm \<Rightarrow> 'a::linorder list list"
+where
+ "cycles f = map (\<lambda>a. trace a f) (seeds f)"
+
+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 add: sorted_list_of_set)
+qed
+
+
+text \<open>Misc\<close>
+
+primrec subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> '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) \<le> 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)) \<le> length (removeAll x ys)" .
+ also have "length (removeAll x ys) \<le> length ys"
+ by simp
+ finally show ?case
+ by simp
+qed
+
+end