# HG changeset patch # User Lars Hupel # Date 1467705020 -7200 # Node ID 0d6adf2d5035be8c2cc5d8ce624769cc32d0fa73 # Parent 370cce7ad9b9aa21d85e1d89be4d0225dfe833a2# Parent bf894d31ed0f8256955256d88829c01117c1e8e3 merged diff -r 370cce7ad9b9 -r 0d6adf2d5035 NEWS --- a/NEWS Mon Jul 04 18:20:51 2016 +0200 +++ b/NEWS Tue Jul 05 09:50:20 2016 +0200 @@ -49,6 +49,9 @@ context. Unlike "context includes ... begin", the effect of 'unbundle' on the target context persists, until different declarations are given. +* Proof method "blast" is more robust wrt. corner cases of Pure +statements without object-logic judgment. + *** Prover IDE -- Isabelle/Scala/jEdit *** @@ -84,6 +87,13 @@ *** Isar *** +* The defining position of a literal fact \prop\ is maintained more +carefully, and made accessible as hyperlink in the Prover IDE. + +* Commands 'finally' and 'ultimately' used to expose the result as +literal fact: this accidental behaviour has been discontinued. Rare +INCOMPATIBILITY, use more explicit means to refer to facts in Isar. + * Command 'axiomatization' has become more restrictive to correspond better to internal axioms as singleton facts with mandatory name. Minor INCOMPATIBILITY. @@ -136,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. diff -r 370cce7ad9b9 -r 0d6adf2d5035 src/HOL/Binomial.thy --- a/src/HOL/Binomial.thy Mon Jul 04 18:20:51 2016 +0200 +++ b/src/HOL/Binomial.thy Tue Jul 05 09:50:20 2016 +0200 @@ -6,7 +6,7 @@ Additional binomial identities by Chaitanya Mangla and Manuel Eberl *) -section\Factorial Function, Binomial Coefficients and Binomial Theorem\ +section \Combinatorial Functions: Factorial Function, Rising Factorials, Binomial Coefficients and Binomial Theorem\ theory Binomial imports Main @@ -170,7 +170,8 @@ text \This development is based on the work of Andy Gordon and Florian Kammueller.\ -subsection \Basic definitions and lemmas\ + +subsection \Binomial coefficients\ text \Combinatorial definition\ @@ -394,6 +395,12 @@ ultimately show ?ths by blast qed +lemma binomial_fact': + assumes "k \ 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 \ n" shows "(of_nat (n choose k) :: 'a::field_char_0) = @@ -465,7 +472,8 @@ finally show ?thesis . qed -subsection\Pochhammer's symbol : generalized rising factorial\ + +subsection \Pochhammer's symbol : generalized rising factorial\ text \See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"}\ @@ -675,20 +683,24 @@ qed -subsection\Generalized binomial coefficients\ +subsection \Generalized binomial coefficients\ -definition (in field_char_0) gbinomial :: "'a \ nat \ 'a" (infixl "gchoose" 65) +definition gbinomial :: "'a :: {semidom_divide, semiring_char_0} \ nat \ 'a" (infixl "gchoose" 65) where - "a gchoose n = setprod (\i. a - of_nat i) {..i. a - of_nat i) {..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 \ n") + case False + then have "n < k" by (simp add: not_le) + then have "0 \ (op - n) ` {..n < k\ show ?thesis + by (simp add: binomial_eq_0 gbinomial_def setprod_zero) +next + case True + then have "inj_on (op - n) {..(op - n ` {..q. n - q) {..{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 \Sign.add_const_constraint (@{const_name gbinomial}, SOME @{typ "'a::field_char_0 \ nat \ 'a"})\ + 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 \Summation on the upper index\ +subsubsection \Summation on the upper index\ text \ 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 \Binomial coefficients\ +subsection \More on Binomial Coefficients\ 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 \Misc\ + 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 {.. 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 (\n acc. (a + of_nat n) * acc) 0 (n - 1) 1)" diff -r 370cce7ad9b9 -r 0d6adf2d5035 src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Mon Jul 04 18:20:51 2016 +0200 +++ b/src/HOL/Hilbert_Choice.thy Tue Jul 05 09:50:20 2016 +0200 @@ -811,6 +811,73 @@ subsection \More on injections, bijections, and inverses\ +locale bijection = + fixes f :: "'a \ '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 \ a = b" + using inj by (rule injD) + +lemma eq_iff [simp]: + "f a = f b \ a = b" + by (auto intro: eqI) + +lemma eq_invI: + "inv f a = inv f b \ a = b" + using inj_inv by (rule injD) + +lemma eq_inv_iff [simp]: + "inv f a = inv f b \ 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 \ 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 \ inv f = id" + by (simp add: fun_eq_iff) + +lemma inv_left_eq_iff [simp]: + "inv f a = b \ f b = a" + by auto + +lemma inv_right_eq_iff [simp]: + "b = inv f a \ f b = a" + by auto + +end + lemma infinite_imp_bij_betw: assumes INF: "\ finite A" shows "\h. bij_betw h A (A - {a})" diff -r 370cce7ad9b9 -r 0d6adf2d5035 src/HOL/Library/Combine_PER.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Combine_PER.thy Tue Jul 05 09:50:20 2016 +0200 @@ -0,0 +1,60 @@ +(* Author: Florian Haftmann, TU Muenchen *) + +section \A combinator to build partial equivalence relations from a predicate and an equivalence relation\ + +theory Combine_PER +imports Main "~~/src/HOL/Library/Lattice_Syntax" +begin + +definition combine_per :: "('a \ bool) \ ('a \ 'a \ bool) \ 'a \ 'a \ bool" +where + "combine_per P R = (\x y. P x \ P y) \ R" + +lemma combine_per_simp [simp]: + fixes R (infixl "\" 50) + shows "combine_per P R x y \ P x \ P y \ x \ y" + by (simp add: combine_per_def) + +lemma combine_per_top [simp]: + "combine_per \ R = R" + by (simp add: fun_eq_iff) + +lemma combine_per_eq [simp]: + "combine_per P HOL.eq = HOL.eq \ (\x y. P x)" + by (auto simp add: fun_eq_iff) + +lemma symp_combine_per: + "symp R \ symp (combine_per P R)" + by (auto simp add: symp_def sym_def combine_per_def) + +lemma transp_combine_per: + "transp R \ transp (combine_per P R)" + by (auto simp add: transp_def trans_def combine_per_def) + +lemma combine_perI: + fixes R (infixl "\" 50) + shows "P x \ P y \ x \ y \ combine_per P R x y" + by (simp add: combine_per_def) + +lemma symp_combine_per_symp: + "symp R \ symp (combine_per P R)" + by (auto intro!: sympI elim: sympE) + +lemma transp_combine_per_transp: + "transp R \ transp (combine_per P R)" + by (auto intro!: transpI elim: transpE) + +lemma equivp_combine_per_part_equivp: + fixes R (infixl "\" 50) + assumes "\x. P x" and "equivp R" + shows "part_equivp (combine_per P R)" +proof - + from \\x. P x\ obtain x where "P x" .. + moreover from \equivp R\ have "x \ x" by (rule equivp_reflp) + ultimately have "\x. P x \ x \ x" by blast + with \equivp R\ 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 diff -r 370cce7ad9b9 -r 0d6adf2d5035 src/HOL/Library/Dlist.thy --- a/src/HOL/Library/Dlist.thy Mon Jul 04 18:20:51 2016 +0200 +++ b/src/HOL/Library/Dlist.thy Tue Jul 05 09:50:20 2016 +0200 @@ -67,6 +67,9 @@ qualified definition filter :: "('a \ bool) \ 'a dlist \ 'a dlist" where "filter P dxs = Dlist (List.filter P (list_of_dlist dxs))" +qualified definition rotate :: "nat \ 'a dlist \ '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 \Explicit executable conversion\ diff -r 370cce7ad9b9 -r 0d6adf2d5035 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Mon Jul 04 18:20:51 2016 +0200 +++ b/src/HOL/Library/Library.thy Tue Jul 05 09:50:20 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 diff -r 370cce7ad9b9 -r 0d6adf2d5035 src/HOL/Library/Perm.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Perm.thy Tue Jul 05 09:50:20 2016 +0200 @@ -0,0 +1,807 @@ +(* Author: Florian Haftmann, TU Muenchen *) + +section \Permutations as abstract type\ + +theory Perm +imports Main +begin + +text \ + 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. +\ + +subsection \Abstract type of permutations\ + +typedef 'a perm = "{f :: 'a \ 'a. bij f \ finite {a. f a \ a}}" + morphisms "apply" Perm + by (rule exI [of _ id]) simp + +setup_lifting type_definition_perm + +notation "apply" (infixl "\$\" 999) +no_notation "apply" ("op \$\") + +lemma bij_apply [simp]: + "bij (apply f)" + using "apply" [of f] by simp + +lemma perm_eqI: + assumes "\a. f \$\ a = g \$\ a" + shows "f = g" + using assms by transfer (simp add: fun_eq_iff) + +lemma perm_eq_iff: + "f = g \ (\a. f \$\ a = g \$\ a)" + by (auto intro: perm_eqI) + +lemma apply_inj: + "f \$\ a = f \$\ b \ a = b" + by (rule inj_eq) (rule bij_is_inj, simp) + +lift_definition affected :: "'a perm \ 'a set" + is "\f. {a. f a \ a}" . + +lemma in_affected: + "a \ affected f \ f \$\ a \ a" + by transfer simp + +lemma finite_affected [simp]: + "finite (affected f)" + by transfer simp + +lemma apply_affected [simp]: + "f \$\ a \ affected f \ a \ affected f" +proof transfer + fix f :: "'a \ 'a" and a :: 'a + assume "bij f \ finite {b. f b \ b}" + then have "bij f" by simp + interpret bijection f by standard (rule \bij f\) + have "f a \ {a. f a = a} \ a \ {a. f a = a}" (is "?P \ ?Q") + by auto + then show "f a \ {a. f a \ a} \ a \ {a. f a \ a}" + by simp +qed + +lemma card_affected_not_one: + "card (affected f) \ 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 \$\ a \ a" + by (simp add: in_affected [symmetric]) + moreover with * have "f \$\ a \ affected f" + by simp + then have "f \$\ (f \$\ a) = f \$\ a" + by (simp add: in_affected) + then have "inv (apply f) (f \$\ (f \$\ a)) = inv (apply f) (f \$\ a)" + by simp + ultimately show False by simp +qed + + +subsection \Identity, composition and inversion\ + +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 = {} \ f = 1" + by transfer auto + +lift_definition times_perm :: "'a perm \ 'a perm \ 'a perm" + is comp +proof + fix f g :: "'a \ 'a" + assume "bij f \ finite {a. f a \ a}" + "bij g \finite {a. g a \ a}" + then have "finite ({a. f a \ a} \ {a. g a \ a})" + by simp + moreover have "{a. (f \ g) a \ a} \ {a. f a \ a} \ {a. g a \ a}" + by auto + ultimately show "finite {a. (f \ g) a \ a}" + by (auto intro: finite_subset) +qed (auto intro: bij_comp) + +lemma apply_times: + "apply (f * g) = apply f \ apply g" + by (fact times_perm.rep_eq) + +lemma apply_sequence: + "f \$\ (g \$\ a) = apply (f * g) a" + by (simp add: apply_times) + +lemma affected_times [simp]: + "affected (f * g) \ affected f \ affected g" + by transfer auto + +lift_definition inverse_perm :: "'a perm \ 'a perm" + is inv +proof transfer + fix f :: "'a \ 'a" and a + assume "bij f \ finite {b. f b \ b}" + then have "bij f" and fin: "finite {b. f b \ b}" + by auto + interpret bijection f by standard (rule \bij f\) + from fin show "bij (inv f) \ finite {a. inv f a \ 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 \ 'a" and a + assume "bij f \ finite {b. f b \ b}" + then have "bij f" by simp + interpret bijection f by standard (rule \bij f\) + show "{a. inv f a \ a} = {a. f a \ 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 \ 'a" and a + assume "bij f \ finite {b. f b \ b}" + then have "bij f" by simp + interpret bijection f by standard (rule \bij f\) + show "inv f \ f = id" + by simp + qed +qed + +declare perm.inverse_distrib_swap [simp] + +lemma perm_mult_commute: + assumes "affected f \ affected g = {}" + shows "g * f = f * g" +proof (rule perm_eqI) + fix a + from assms have *: "a \ affected f \ a \ affected g" + "a \ affected g \ a \ affected f" for a + by auto + consider "a \ affected f \ a \ affected g + \ f \$\ a \ affected f" + | "a \ affected f \ a \ affected g + \ f \$\ a \ affected f" + | "a \ affected f \ a \ affected g" + using assms by auto + then show "(g * f) \$\ a = (f * g) \$\ a" + proof cases + case 1 moreover with * have "f \$\ a \ affected g" + by auto + ultimately show ?thesis by (simp add: in_affected apply_times) + next + case 2 moreover with * have "g \$\ a \ 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 \Orbit and order of elements\ + +definition orbit :: "'a perm \ 'a \ 'a set" +where + "orbit f a = range (\n. (f ^ n) \$\ a)" + +lemma in_orbitI: + assumes "(f ^ n) \$\ a = b" + shows "b \ orbit f a" + using assms by (auto simp add: orbit_def) + +lemma apply_power_self_in_orbit [simp]: + "(f ^ n) \$\ a \ orbit f a" + by (rule in_orbitI) rule + +lemma in_orbit_self [simp]: + "a \ orbit f a" + using apply_power_self_in_orbit [of _ 0] by simp + +lemma apply_self_in_orbit [simp]: + "f \$\ a \ orbit f a" + using apply_power_self_in_orbit [of _ 1] by simp + +lemma orbit_not_empty [simp]: + "orbit f a \ {}" + using in_orbit_self [of a f] by blast + +lemma not_in_affected_iff_orbit_eq_singleton: + "a \ affected f \ orbit f a = {a}" (is "?P \ ?Q") +proof + assume ?P + then have "f \$\ a = a" + by (simp add: in_affected) + then have "(f ^ n) \$\ 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 \ 'a \ nat" +where + "order f = card \ orbit f" + +lemma orbit_subset_eq_affected: + assumes "a \ affected f" + shows "orbit f a \ affected f" +proof (rule ccontr) + assume "\ orbit f a \ affected f" + then obtain b where "b \ orbit f a" and "b \ affected f" + by auto + then have "b \ range (\n. (f ^ n) \$\ a)" + by (simp add: orbit_def) + then obtain n where "b = (f ^ n) \$\ a" + by blast + with \b \ affected f\ + have "(f ^ n) \$\ a \ affected f" + by simp + then have "f \$\ a \ 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 \ 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 \ 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 \ a \ affected f" (is "?P \ ?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 \orbit f a = {b}\ 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 \ 2 \ a \ 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 \ 1" + shows "order f a \ card (affected f)" +proof (cases "a \ affected f") + from assms have "affected f \ {}" + by simp + then obtain B b where "affected f = insert b B" + by blast + with finite_affected [of f] have "card (affected f) \ 1" + by (simp add: card_insert) + case False then have "order f a = 1" + by (simp add: order_eq_one_iff) + with \card (affected f) \ 1\ show ?thesis + by simp +next + case True + have "card (orbit f a) \ 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 \ affected f" + shows "order f a \ 2" +proof (rule ccontr) + assume "\ 2 \ 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) \$\ a = a" + shows "order f a = card ((\m. (f ^ m) \$\ a) ` {0..m. (f ^ m) \$\ a) ` {0.. orbit f a" + then obtain m where "(f ^ m) \$\ a = b" + by (auto simp add: orbit_def) + then have "b = (f ^ (m mod n + n * (m div n))) \$\ a" + by simp + also have "\ = (f ^ (m mod n)) \$\ ((f ^ (n * (m div n))) \$\ a)" + by (simp only: power_add apply_times) simp + also have "(f ^ (n * q)) \$\ a = a" for q + by (induct q) + (simp_all add: power_add apply_times assms) + finally have "b = (f ^ (m mod n)) \$\ a" . + moreover from \n > 0\ + have "m mod n < n" + by simp + ultimately show "b \ ?B" + by auto + next + fix b + assume "b \ ?B" + then obtain m where "(f ^ m) \$\ a = b" + by blast + then show "b \ 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 (\m. (f ^ m) \$\ a) {..m. (f ^ m) \$\ a) {.. 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 (\m. (f ^ m) \$\ a) {..$\ a \ (\m. (f ^ m) \$\ a) ` {..$\ a \ (\m. (f ^ m) \