Theory Pigeonholeprinciple

(*  Title:      RSAPSS/Pigeonholeprinciple.thy
    Author:     Christina Lindenberg, Kai Wirt, Technische Universität Darmstadt
    Copyright:  2005 - Technische Universität Darmstadt 
*)

header "Pigeon hole principle"

theory Pigeonholeprinciple
imports Productdivides
begin

text {*
  This theory is a formal proof for the pigeon hole principle. The
  basic principle is, that if you have to put @{text "n + 1"} pigeons
  in n holes there is at least one hole with more than one pigeon.
*}

abbreviation (input) "alldistinct ≡ distinct"
abbreviation (input) mem (infixl "mem" 55) where "x mem xs ≡ x ∈ set xs"

primrec alllesseq :: "nat list => nat => bool"
where
  "alllesseq [] n = True"
| "alllesseq (x # xs) n = (x ≤ n ∧ alllesseq xs n)"

primrec allnonzero :: "nat list => bool"
where
  "allnonzero [] = True"
| "allnonzero (x # xs) = (x ≠ 0 ∧ allnonzero xs)"

primrec positives :: "nat => nat list"
where
  "positives 0 = []"
| "positives (Suc n) = Suc n # positives n"

primrec timeslist :: "nat list => nat"
where
  "timeslist [] = 1"
| "timeslist (x # xs) = x * timeslist xs"

primrec fac :: "nat => nat"
where
  "fac 0 = 1"
| "fac (Suc n) = Suc n * fac n"

primrec del :: "nat => nat list => nat list"
where
  "del a [] = []"
| "del a (x # xs) = (if a ≠ x then x # del a xs else xs)" 

lemma length_del: "x mem xs ==> length (del x xs) < length xs"
  by (induct xs) auto

function pigeonholeinduction
where
  "pigeonholeinduction [] = True"
| "pigeonholeinduction (x#xs) =
    (if ((length (x#xs)) mem xs)
     then (pigeonholeinduction (del (length (x#xs)) (x#xs)))
     else (pigeonholeinduction xs))"
by pat_completeness auto

termination by (relation "measure size") (auto simp add: length_del)

lemma old_pig_induct:
  fixes P
  assumes "P []"
    and "(!!(x::nat) xs::nat list.
    ¬ length (x # xs) mem xs --> P xs ==>
    length (x # xs) mem xs --> P (del (length (x # xs)) (x # xs)) ==>
    P (x # xs))"
  shows "P x"
  apply (rule pigeonholeinduction.induct)
  using assms apply auto
  done

definition
  perm :: "nat list => nat list => bool" where
  "perm xs ys <-> sort xs = sort ys"

lemma allnonzerodelete: "allnonzero xs ==> allnonzero (del x xs)"
  by (induct xs) auto

lemma notmemnotdelmem: "x ≠ a ==> ¬ a mem xs ==> ¬ a mem (del x xs)"
  by (induct xs) auto

lemma alldistinctdelete: "alldistinct xs ==> alldistinct (del x xs)"
  apply (induct xs)
   apply auto
  apply (insert notmemnotdelmem)
  apply auto
  done

lemma pigeonholeprinciple_lemma2: "¬ (Suc n) mem xs ==> alllesseq xs (Suc n) ==> alllesseq xs n"
  apply (atomize (full))
  apply (induct xs)
   apply auto
  done

lemma pigeonholeprinciple_lemma1:
    "alldistinct xs ==> alllesseq xs (Suc n) ==> alllesseq (del (Suc n) xs) n"
  apply (induct xs)
   apply auto
  apply (rule pigeonholeprinciple_lemma2)
   apply auto
  done

lemma anotinsort: "a ≠ x ==> a mem b = a mem (insort x b)"
  by (induct b) auto

lemma ainsort: "a mem (insort a b)"
  by (induct b) auto

lemma memeqsort: "x mem xs = x mem (sort xs)"
  by (simp add: set_sort)

lemma permmember: "[|perm xs ys; x mem xs|] ==> x mem ys"
  by (simp only: perm_def memeqsort [of x xs] memeqsort [of x ys])

lemma alllesseqdelete: "[|alldistinct (x#xs); alllesseq (x#xs) (length(x#xs))|]
    ==> alllesseq (del (length(x#xs)) (x#xs)) (length (xs))"
  apply (insert pigeonholeprinciple_lemma1 [of "x#xs" "length xs"])
  apply simp
  done

lemma perminsert: "perm xs ys ==> perm (a#xs) (a#ys)"
  by (simp add: perm_def)

lemma lengthdel2: "a mem xs ==> length (del a (x#xs)) = length xs"
  by (induct xs) auto

lemma dellengthinalllesseq:
  "[|alldistinct (x#xs); alllesseq (x#xs) (length (x#xs)); length (x#xs) mem xs |]
  ==> alllesseq (del (length (x#xs)) (x#xs))(length (del (length (x#xs)) (x#xs)))"
  apply (drule alllesseqdelete)
   apply simp
  apply (insert lengthdel2 [of "length (x#xs)" xs x])
  apply simp
  done

lemma lengthmem: "[|length (x#xs) mem (xs)|] ==> length (x#xs) mem (x#xs)"
  by auto

lemma permSuclengthdel:
  "[|Suc (length xs) mem xs;
    perm (positives (length xs)) (x # del (Suc (length xs)) xs);
    x ≠ Suc (length xs)|] ==>
  perm (Suc (length xs) # positives (length xs)) ((Suc (length xs))#(x # del (Suc (length xs)) xs))"
  apply (rule perminsert)
  apply simp
  done

lemma insortsym: "insort a (insort x xs) = insort x (insort a xs)"
  by (induct xs) auto

lemma insortsortdel: "x mem xs ==> insort x (sort (del  x xs)) = (sort xs)"
  apply (induct xs)
   apply auto
  apply (subst insortsym)
  apply simp
  done

lemma permSuclengthdel2:
  "[|Suc (length xs) mem xs; x ≠ Suc (length xs);
    perm (Suc (length xs) # positives (length xs)) ((Suc (length xs))#(x # del (Suc (length xs)) xs))|]
  ==> perm (Suc (length xs) # positives (length xs)) (x # xs)"
  apply (simp add: perm_def)
  apply (subst insortsym)
  apply (insert insortsortdel [of "Suc (length xs)" xs, symmetric])
  apply auto
  done

lemma dellengthinperm:
  "[| length (x # xs) mem (x#xs);
  perm (positives (length (del (length (x # xs)) (x # xs))))(del (length (x # xs)) (x # xs))|]
    ==> perm (positives (length (x # xs))) (x # xs)"
  apply (cases "x = Suc (length xs)")
   apply simp
   apply (drule perminsert)
   apply simp
  apply (insert lengthdel2 [of "length (x # xs)" xs x])
  apply (simp del: perm_def positives.simps)
  apply (simp only: positives.simps)
  apply (frule permSuclengthdel)
    apply simp
   apply simp
  apply (rule permSuclengthdel2)
    apply simp_all
  done

lemma positiveseq: "positives (length xs) = rev ([1 ..< Suc(length xs)])"
  by (induct xs) auto

lemma memsetpositives:
  "[|perm (positives (length xs)) xs; 0 < x; x ≤ length xs|] ==> x ∈ set (positives (length xs))"
  apply (subst positiveseq)
  apply (simp add:set_upt)
  apply auto
  done

lemmas seteqmem = List.member_def [symmetric]

lemma pigeonholeprinciple:
  "allnonzero xs ==> alldistinct xs ==> alllesseq xs (length xs) ==> perm (positives (length xs)) xs"
  apply (atomize (full))
  apply (induct xs rule: old_pig_induct)
  apply (simp add: perm_def)
  apply safe
  apply (erule_tac P="allnonzero (del (length (x # xs)) (x # xs))" in notE)
  apply (rule allnonzerodelete)
  apply (simp)
  apply (erule_tac P="alldistinct (del (length (x # xs)) (x # xs))" in notE)
  apply (rule alldistinctdelete)
  apply (simp)
  apply (erule_tac P="alllesseq (del (length (x # xs)) (x # xs))(length (del (length (x # xs)) (x # xs)))" in notE)
  apply (rule dellengthinalllesseq)
  apply (simp)
  apply (simp)
  apply (simp)
  apply (erule_tac P="perm (positives (length (x # xs))) (x # xs)" in notE)
  apply (drule lengthmem)  
  apply (drule dellengthinperm)
  apply (simp)+  
  apply (erule conjE)+
  apply (erule_tac P="alllesseq xs (length xs)" in notE)
  apply (erule pigeonholeprinciple_lemma2)
  apply (simp)+
  apply (erule conjE)+
  apply (case_tac "x=Suc(length xs)")
  apply (simp)
  apply (rule perminsert)
  apply (simp)
  apply (drule le_neq_implies_less)
  apply (simp add:less_Suc_eq_le)
  apply (erule_tac P="x mem xs" in notE)
  apply (simp add:seteqmem [symmetric])
  apply (frule memsetpositives)
  apply simp+
  apply (rule permmember)
  apply (simp)
  apply (simp)
  apply (simp)
  apply (simp)
  apply (simp)
  apply (simp)
  apply (simp)
  apply (erule_tac P="allnonzero (del (length (x # xs)) (x # xs))" in notE, rule allnonzerodelete, simp)+
  apply (simp)
  apply (simp)
  apply (simp)
  apply (erule_tac P="alldistinct (del (length (x # xs)) (x # xs))" in notE, rule alldistinctdelete, simp)+
  apply (erule_tac P="alllesseq (del (length (x # xs)) (x # xs))(length (del (length (x # xs)) (x # xs)))" in notE)
  apply (case_tac "length (x#xs) mem xs")
  apply (erule dellengthinalllesseq, simp, simp)+
  apply (erule_tac P="alllesseq xs (length xs)" in notE)
  apply (rule pigeonholeprinciple_lemma2)
  apply (simp)+
  apply (case_tac "length (x#xs) mem (x#xs)")
  apply (frule dellengthinperm)
  apply (simp)+
  apply (case_tac "Suc (length xs) ≠ x")
  apply (simp)
  apply (erule conjE)+
  apply (erule_tac P="alllesseq xs (length xs)" in notE)
  apply (drule pigeonholeprinciple_lemma2)
  apply (simp)
  apply (simp)
  apply (erule conjE)+
  apply (simp)+
  apply (case_tac "Suc (length xs) = x")
  apply (drule perminsert)
  apply (simp)+
  apply (erule conjE)+
  apply (drule le_neq_implies_less)
  apply (simp add:less_Suc_eq_le)+
  apply (erule_tac P="x mem xs" in notE)
  apply (frule memsetpositives)
  apply simp+
  apply (rule permmember)
  apply (simp)+
  apply (case_tac "Suc (length xs) = x")
  apply (drule perminsert)
  apply (simp)+
  apply (erule conjE)+
  apply (drule le_neq_implies_less)
  apply (simp add:less_Suc_eq_le)+
  apply (erule_tac P="x mem xs" in notE)
  apply (frule memsetpositives)
  apply simp+
  apply (rule permmember)
  apply (simp)+
  done

lemma equaltimeslist: "[|sort xs = sort ys|] ==> timeslist (sort xs) = timeslist (sort ys)"
  by auto

lemma timeslistmultkom: "timeslist (xs) * x = x * timeslist (xs)"
  by simp

lemma timeslistinsort: "timeslist (insort a xs) = timeslist (a#xs)" 
  by (induct xs) auto

lemma timeslisteq: "timeslist (sort xs) = timeslist xs"
  apply (induct xs)
   apply auto
  apply (simp add: timeslistmultkom [symmetric])
  apply (simp add:timeslistinsort)
  done

lemma permtimeslist: "perm xs ys ==> timeslist xs = timeslist ys"
  apply (simp only:perm_def)
  apply (insert equaltimeslist [of xs ys])
  apply (simplesubst timeslisteq [symmetric])
  apply (simplesubst timeslisteq [of xs, symmetric])
  apply auto
  done

lemma timeslistpositives: "timeslist (positives n) = fac n"
  by (induct n) auto

lemma pdvdnot: "[|prime p; ¬ p dvd x; ¬ p dvd y|] ==> ¬ p dvd x*y"
  apply (auto)
  apply (insert prime_dvd_mult [of p x y])
  apply simp
  done

lemma lessdvdnot: "[|Suc (x::nat) < p|] ==> ¬ p dvd Suc x"
  apply auto
  apply (frule mod_less)
  apply (frule dvd_imp_le)
  apply auto
  done

lemma pnotdvdall:"[|prime p; p dvd (Suc n)*(fac n); ¬ p dvd fac n; Suc n < p|] ==> False"
  apply (insert lessdvdnot [of n p])
  apply (insert pdvdnot [of p "Suc n" "fac n"])
  apply auto
  done

lemma primefact: "prime p ==> (n::nat) < p ==> fac n mod p ≠ 0"
  apply (induct n)
   apply (simp add: prime_def)
  apply (simp only: fac.simps dvd_eq_mod_eq_0 [symmetric])
  apply clarify
  apply (drule meta_mp)
   apply simp
  apply (insert lessdvdnot pdvdnot [of "p" "fac n" "Suc n"] pnotdvdall)
  apply auto
  done

end