Theory Pigeonholeprinciple

Up to index of Isabelle/HOL/RSAPSS

theory Pigeonholeprinciple
imports Productdivides
`(*  Title:      RSAPSS/Pigeonholeprinciple.thy    Author:     Christina Lindenberg, Kai Wirt, Technische Universität Darmstadt    Copyright:  2005 - Technische Universität Darmstadt *)header "Pigeon hole principle"theory Pigeonholeprincipleimports Productdividesbegintext {*  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) autofunction pigeonholeinductionwhere  "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 autotermination 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  donedefinition  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) autolemma notmemnotdelmem: "x ≠ a ==> ¬ a mem xs ==> ¬ a mem (del x xs)"  by (induct xs) autolemma alldistinctdelete: "alldistinct xs ==> alldistinct (del x xs)"  apply (induct xs)   apply auto  apply (insert notmemnotdelmem)  apply auto  donelemma pigeonholeprinciple_lemma2: "¬ (Suc n) mem xs ==> alllesseq xs (Suc n) ==> alllesseq xs n"  apply (atomize (full))  apply (induct xs)   apply auto  donelemma 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  donelemma anotinsort: "a ≠ x ==> a mem b = a mem (insort x b)"  by (induct b) autolemma ainsort: "a mem (insort a b)"  by (induct b) autolemma 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  donelemma 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) autolemma 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  donelemma lengthmem: "[|length (x#xs) mem (xs)|] ==> length (x#xs) mem (x#xs)"  by autolemma 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  donelemma insortsym: "insort a (insort x xs) = insort x (insort a xs)"  by (induct xs) autolemma insortsortdel: "x mem xs ==> insort x (sort (del  x xs)) = (sort xs)"  apply (induct xs)   apply auto  apply (subst insortsym)  apply simp  donelemma 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  donelemma 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  donelemma positiveseq: "positives (length xs) = rev ([1 ..< Suc(length xs)])"  by (induct xs) autolemma 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  donelemmas 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)+  donelemma equaltimeslist: "[|sort xs = sort ys|] ==> timeslist (sort xs) = timeslist (sort ys)"  by autolemma timeslistmultkom: "timeslist (xs) * x = x * timeslist (xs)"  by simplemma timeslistinsort: "timeslist (insort a xs) = timeslist (a#xs)"   by (induct xs) autolemma timeslisteq: "timeslist (sort xs) = timeslist xs"  apply (induct xs)   apply auto  apply (simp add: timeslistmultkom [symmetric])  apply (simp add:timeslistinsort)  donelemma 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  donelemma timeslistpositives: "timeslist (positives n) = fac n"  by (induct n) autolemma 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  donelemma lessdvdnot: "[|Suc (x::nat) < p|] ==> ¬ p dvd Suc x"  apply auto  apply (frule mod_less)  apply (frule dvd_imp_le)  apply auto  donelemma 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  donelemma 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  doneend`