Theory Jordan_Normal_Form.Missing_Misc

(*  
    Author:      René Thiemann 
                 Akihisa Yamada
    License:     BSD
*)
section ‹Material missing in the distribution›

text ‹This theory provides some definitions and lemmas which we did not find in the 
  Isabelle distribution.›

theory Missing_Misc
  imports
    "HOL-Library.FuncSet"
    "HOL-Combinatorics.Permutations"
begin

declare finite_image_iff [simp]

lemma inj_on_finite:
  finite (f ` A)  finite A if inj_on f A
  using that by (fact finite_image_iff)

text ‹The following lemma is slightly generalized from Determinants.thy in HMA.›

lemma finite_bounded_functions:
  assumes fS: "finite S"
  shows "finite T  finite {f. (i  T. f i  S)  (i. i  T  f i = i)}"
proof (induct T rule: finite_induct)
  case empty
  have th: "{f. i. f i = i} = {id}"
    by auto
  show ?case
    by (auto simp add: th)
next
  case (insert a T)
  let ?f = "λ(y,g) i. if i = a then y else g i"
  let ?S = "?f ` (S × {f. (iT. f i  S)  (i. i  T  f i = i)})"
  have "?S = {f. (i insert a T. f i  S)  (i. i  insert a T  f i = i)}"
    apply (auto simp add: image_iff)
    apply (rule_tac x="x a" in bexI)
    apply (rule_tac x = "λi. if i = a then i else x i" in exI)
    apply (insert insert, auto)
    done
  with finite_imageI[OF finite_cartesian_product[OF fS insert.hyps(3)], of ?f]
  show ?case
    by metis
qed

lemma finite_bounded_functions':
  assumes fS: "finite S"
  shows "finite T  finite {f. (i  T. f i  S)  (i. i  T  f i = j)}"
proof (induct T rule: finite_induct)
  case empty
  have th: "{f. i. f i = j} = {(λ x. j)}"
    by auto
  show ?case
    by (auto simp add: th)
next
  case (insert a T)
  let ?f = "λ(y,g) i. if i = a then y else g i"
  let ?S = "?f ` (S × {f. (iT. f i  S)  (i. i  T  f i = j)})"
  have "?S = {f. (i insert a T. f i  S)  (i. i  insert a T  f i = j)}"
    apply (auto simp add: image_iff)
    apply (rule_tac x="x a" in bexI)
    apply (rule_tac x = "λi. if i = a then j else x i" in exI)
    apply (insert insert, auto)
    done
  with finite_imageI[OF finite_cartesian_product[OF fS insert.hyps(3)], of ?f]
  show ?case
    by metis
qed

lemma permutes_less [simp]:
  assumes p: "p permutes {0..<(n :: nat)}"
  shows
    "i < n  p i < n"
    "i < n  inv p i < n" 
    "p (inv p i) = i"
    "inv p (p i) = i"
  using assms
  by (simp_all add: permutes_inverses permutes_nat_less permutes_nat_inv_less)

lemma permutes_prod:
  assumes p: "p permutes S"
  shows "(sS. f (p s) s) = (sS. f s (inv p s))"
    (is "?l = ?r")
  using assms by (fact prod.permutes_inv)

lemma permutes_sum:
  assumes p: "p permutes S"
  shows "(sS. f (p s) s) = (sS. f s (inv p s))"
    (is "?l = ?r")
  using assms by (fact sum.permutes_inv)

context
  fixes A :: "'a set" 
    and B :: "'b set"
    and a_to_b :: "'a  'b"
    and b_to_a :: "'b  'a"
  assumes ab: " a. a  A  a_to_b a  B"
    and ba: " b. b  B  b_to_a b  A"
    and ab_ba: " a. a  A  b_to_a (a_to_b a) = a"
    and ba_ab: " b. b  B  a_to_b (b_to_a b) = b"
begin

qualified lemma permutes_memb: fixes p :: "'b  'b"
  assumes p: "p permutes B"
  and a: "a  A"
  defines "ip  Hilbert_Choice.inv p"
  shows "a  A" "a_to_b a  B" "ip (a_to_b a)  B" "p (a_to_b a)  B" 
    "b_to_a (p (a_to_b a))  A" "b_to_a (ip (a_to_b a))  A"
proof -
  let ?b = "a_to_b a"
  from p have ip: "ip permutes B" unfolding ip_def by (rule permutes_inv)
  note in_ip = permutes_in_image[OF ip]
  note in_p = permutes_in_image[OF p]
  show a: "a  A" by fact
  show b: "?b  B" by (rule ab[OF a])
  show pb: "p ?b  B" unfolding in_p by (rule b)
  show ipb: "ip ?b  B" unfolding in_ip by (rule b)
  show "b_to_a (p ?b)  A" by (rule ba[OF pb])
  show "b_to_a (ip ?b)  A" by (rule ba[OF ipb])
qed

lemma permutes_bij_main: 
  "{p . p permutes A}  (λ p a. if a  A then b_to_a (p (a_to_b a)) else a) ` {p . p permutes B}" 
  (is "?A  ?f ` ?B")
proof 
  note d = permutes_def
  let ?g = "λ q b. if b  B then a_to_b (q (b_to_a b)) else b"
  let ?inv = "Hilbert_Choice.inv"
  fix p
  assume p: "p  ?f ` ?B"
  then obtain q where q: "q permutes B" and p: "p = ?f q" by auto    
  let ?iq = "?inv q"
  from q have iq: "?iq permutes B" by (rule permutes_inv)
  note in_iq = permutes_in_image[OF iq]
  note in_q = permutes_in_image[OF q]
  have qiB: " b. b  B  q (?iq b) = b" using q by (rule permutes_inverses)
  have iqB: " b. b  B  ?iq (q b) = b" using q by (rule permutes_inverses)
  from q[unfolded d] 
  have q1: " b. b  B  q b = b" 
   and q2: " b. ∃!b'. q b' = b" by auto
  note memb = permutes_memb[OF q]
  show "p  ?A" unfolding p d
  proof (rule, intro conjI impI allI, force)
    fix a
    show "∃!a'. ?f q a' = a"
    proof (cases "a  A")
      case True
      note a = memb[OF True]
      let ?a = "b_to_a (?iq (a_to_b a))"
      show ?thesis
      proof 
        show "?f q ?a = a" using a by (simp add: ba_ab qiB ab_ba)
      next
        fix a'
        assume id: "?f q a' = a"
        show "a' = ?a"
        proof (cases "a'  A")
          case False
          thus ?thesis using id a by auto
        next
          case True
          note a' = memb[OF this]
          from id True have "b_to_a (q (a_to_b a')) = a" by simp
          from arg_cong[OF this, of "a_to_b"] a' a
          have "q (a_to_b a') = a_to_b a" by (simp add: ba_ab)
          from arg_cong[OF this, of ?iq]
          have "a_to_b a' = ?iq (a_to_b a)" unfolding iqB[OF a'(2)] .
          from arg_cong[OF this, of b_to_a] show ?thesis unfolding ab_ba[OF True] .
        qed
      qed
    next
      case False note a = this
      show ?thesis
      proof
        show "?f q a = a" using a by simp
      next
        fix a'
        assume id: "?f q a' = a"
        show "a' = a"
        proof (cases "a'  A")
          case False
          with id show ?thesis by simp
        next
          case True
          note a' = memb[OF True]
          with id False show ?thesis by auto
        qed
      qed
    qed
  qed
qed

end

lemma permutes_bij': assumes ab: " a. a  A  a_to_b a  B"
    and ba: " b. b  B  b_to_a b  A"
    and ab_ba: " a. a  A  b_to_a (a_to_b a) = a"
    and ba_ab: " b. b  B  a_to_b (b_to_a b) = b"
  shows "{p . p permutes A} = (λ p a. if a  A then b_to_a (p (a_to_b a)) else a) ` {p . p permutes B}" 
  (is "?A = ?f ` ?B")
proof -
  note one_dir = ab ba ab_ba ba_ab
  note other_dir = ba ab ba_ab ab_ba
  let ?g = "(λ p b. if b  B then a_to_b (p (b_to_a b)) else b)"
  define PA where "PA = ?A"
  define f where "f = ?f"
  define g where "g = ?g"
  {
    fix p
    assume "p  PA"
    hence p: "p permutes A" unfolding PA_def by simp
    from p[unfolded permutes_def] have pnA: " a. a  A  p a = a" by auto
    have "?f (?g p) = p"
    proof (rule ext)
      fix a
      show "?f (?g p) a = p a"
      proof (cases "a  A")
        case False
        thus ?thesis by (simp add: pnA)
      next
        case True note a = this
        hence "p a  A" unfolding permutes_in_image[OF p] .
        thus ?thesis using a by (simp add: ab_ba ba_ab ab)
      qed
    qed
    hence "f (g p) = p" unfolding f_def g_def .
  }
  hence "f ` g ` PA = PA" by force
  hence id: "?f ` ?g ` ?A = ?A" unfolding PA_def f_def g_def .
  have "?f ` ?B  ?A" by (rule permutes_bij_main[OF one_dir])
  moreover have "?g ` ?A  ?B" by (rule permutes_bij_main[OF ba ab ba_ab ab_ba])
  hence "?f ` ?g ` ?A  ?f ` ?B" by auto
  hence "?A  ?f ` ?B" unfolding id .
  ultimately show ?thesis by blast
qed    

lemma permutes_others:
  assumes p: "p permutes S" and x: "x  S" shows "p x = x"
  using p x by (rule permutes_not_in)

lemma inj_on_nat_permutes: assumes i: "inj_on f (S :: nat set)"
  and fS: "f  S  S"
  and fin: "finite S"
  and f: " i. i  S  f i = i"
  shows "f permutes S"
  unfolding permutes_def
proof (intro conjI allI impI, rule f)
  fix y
  from endo_inj_surj[OF fin _ i] fS have fs: "f ` S = S" by auto
  show "∃!x. f x = y"
  proof (cases "y  S")
    case False
    thus ?thesis by (intro ex1I[of _ y], insert fS f, auto)
  next
    case True
    with fs obtain x where x: "x  S" and fx: "f x = y" by force
    show ?thesis
    proof (rule ex1I, rule fx)
      fix x'
      assume fx': "f x' = y"
      with True f[of x'] have "x'  S" by metis
      from inj_onD[OF i fx[folded fx'] x this]
      show "x' = x" by simp
    qed
  qed
qed

abbreviation (input) signof :: (nat  nat)  'a :: ring_1
  where signof p  of_int (sign p)

lemma signof_id:
  "signof id = 1"
  "signof (λx. x) = 1"
  by simp_all

lemma signof_inv: "finite S  p permutes S  signof (inv p) = signof p"
  by (simp add: permutes_imp_permutation sign_inverse)
  
lemma signof_pm_one: "signof p  {1, - 1}"
  by (simp add: sign_def)
  
lemma signof_compose:
  assumes "p permutes {0..<(n :: nat)}"
  and "q permutes {0 ..<(m :: nat)}"
  shows "signof (p o q) = signof p * signof q"
proof -
  from assms have pp: "permutation p" "permutation q"
    by (auto simp: permutation_permutes)
  then show "signof (p o q) = signof p * signof q"
    by (simp add: sign_compose)
qed 

end