src/HOL/Library/Diagonal_Subsequence.thy
 author hoelzl Tue Mar 26 12:20:58 2013 +0100 (2013-03-26) changeset 51526 155263089e7b parent 50087 635d73673b5e child 52681 8cc7f76b827a permissions -rw-r--r--
move SEQ.thy and Lim.thy to Limits.thy
 immler@50087 ` 1` ```(* Author: Fabian Immler, TUM *) ``` immler@50087 ` 2` immler@50087 ` 3` ```header {* Sequence of Properties on Subsequences *} ``` immler@50087 ` 4` immler@50087 ` 5` ```theory Diagonal_Subsequence ``` hoelzl@51526 ` 6` ```imports Complex_Main ``` immler@50087 ` 7` ```begin ``` immler@50087 ` 8` immler@50087 ` 9` ```locale subseqs = ``` immler@50087 ` 10` ``` fixes P::"nat\(nat\nat)\bool" ``` immler@50087 ` 11` ``` assumes ex_subseq: "\n s. subseq s \ \r'. subseq r' \ P n (s o r')" ``` immler@50087 ` 12` ```begin ``` immler@50087 ` 13` immler@50087 ` 14` ```primrec seqseq where ``` immler@50087 ` 15` ``` "seqseq 0 = id" ``` immler@50087 ` 16` ```| "seqseq (Suc n) = seqseq n o (SOME r'. subseq r' \ P n (seqseq n o r'))" ``` immler@50087 ` 17` immler@50087 ` 18` ```lemma seqseq_ex: ``` immler@50087 ` 19` ``` shows "subseq (seqseq n) \ ``` immler@50087 ` 20` ``` (\r'. seqseq (Suc n) = seqseq n o r' \ subseq r' \ P n (seqseq n o r'))" ``` immler@50087 ` 21` ```proof (induct n) ``` immler@50087 ` 22` ``` case 0 ``` immler@50087 ` 23` ``` let ?P = "\r'. subseq r' \ P 0 r'" ``` immler@50087 ` 24` ``` let ?r = "Eps ?P" ``` immler@50087 ` 25` ``` have "?P ?r" using ex_subseq[of id 0] by (intro someI_ex[of ?P]) (auto simp: subseq_def) ``` immler@50087 ` 26` ``` thus ?case by (auto simp: subseq_def) ``` immler@50087 ` 27` ```next ``` immler@50087 ` 28` ``` case (Suc n) ``` immler@50087 ` 29` ``` then obtain r' where ``` immler@50087 ` 30` ``` Suc': "seqseq (Suc n) = seqseq n \ r'" "subseq (seqseq n)" "subseq r'" ``` immler@50087 ` 31` ``` "P n (seqseq n o r')" ``` immler@50087 ` 32` ``` by blast ``` immler@50087 ` 33` ``` let ?P = "\r'a. subseq (r'a ) \ P (Suc n) (seqseq n o r' o r'a)" ``` immler@50087 ` 34` ``` let ?r = "Eps ?P" ``` immler@50087 ` 35` ``` have "?P ?r" using ex_subseq[of "seqseq n o r'" "Suc n"] Suc' ``` immler@50087 ` 36` ``` by (intro someI_ex[of ?P]) (auto intro: subseq_o simp: o_assoc) ``` immler@50087 ` 37` ``` moreover have "seqseq (Suc (Suc n)) = seqseq n \ r' \ ?r" ``` immler@50087 ` 38` ``` by (subst seqseq.simps) (simp only: Suc' o_assoc) ``` immler@50087 ` 39` ``` moreover note subseq_o[OF `subseq (seqseq n)` `subseq r'`] ``` immler@50087 ` 40` ``` ultimately show ?case unfolding Suc' by (auto simp: o_def) ``` immler@50087 ` 41` ```qed ``` immler@50087 ` 42` immler@50087 ` 43` ```lemma subseq_seqseq: ``` immler@50087 ` 44` ``` shows "subseq (seqseq n)" using seqseq_ex[OF assms] by auto ``` immler@50087 ` 45` immler@50087 ` 46` ```definition reducer where "reducer n = (SOME r'. subseq r' \ P n (seqseq n o r'))" ``` immler@50087 ` 47` immler@50087 ` 48` ```lemma subseq_reducer: "subseq (reducer n)" and reducer_reduces: "P n (seqseq n o reducer n)" ``` immler@50087 ` 49` ``` unfolding atomize_conj unfolding reducer_def using subseq_seqseq ``` immler@50087 ` 50` ``` by (rule someI_ex[OF ex_subseq]) ``` immler@50087 ` 51` immler@50087 ` 52` ```lemma seqseq_reducer[simp]: ``` immler@50087 ` 53` ``` "seqseq (Suc n) = seqseq n o reducer n" ``` immler@50087 ` 54` ``` by (simp add: reducer_def) ``` immler@50087 ` 55` immler@50087 ` 56` ```declare seqseq.simps(2)[simp del] ``` immler@50087 ` 57` immler@50087 ` 58` ```definition diagseq where "diagseq i = seqseq i i" ``` immler@50087 ` 59` immler@50087 ` 60` ```lemma diagseq_mono: "diagseq n < diagseq (Suc n)" ``` immler@50087 ` 61` ``` unfolding diagseq_def seqseq_reducer o_def ``` immler@50087 ` 62` ``` by (metis subseq_mono[OF subseq_seqseq] less_le_trans lessI seq_suble subseq_reducer) ``` immler@50087 ` 63` immler@50087 ` 64` ```lemma subseq_diagseq: "subseq diagseq" ``` immler@50087 ` 65` ``` using diagseq_mono by (simp add: subseq_Suc_iff diagseq_def) ``` immler@50087 ` 66` immler@50087 ` 67` ```primrec fold_reduce where ``` immler@50087 ` 68` ``` "fold_reduce n 0 = id" ``` immler@50087 ` 69` ```| "fold_reduce n (Suc k) = fold_reduce n k o reducer (n + k)" ``` immler@50087 ` 70` immler@50087 ` 71` ```lemma subseq_fold_reduce: "subseq (fold_reduce n k)" ``` immler@50087 ` 72` ```proof (induct k) ``` immler@50087 ` 73` ``` case (Suc k) from subseq_o[OF this subseq_reducer] show ?case by (simp add: o_def) ``` immler@50087 ` 74` ```qed (simp add: subseq_def) ``` immler@50087 ` 75` immler@50087 ` 76` ```lemma ex_subseq_reduce_index: "seqseq (n + k) = seqseq n o fold_reduce n k" ``` immler@50087 ` 77` ``` by (induct k) simp_all ``` immler@50087 ` 78` immler@50087 ` 79` ```lemma seqseq_fold_reduce: "seqseq n = fold_reduce 0 n" ``` immler@50087 ` 80` ``` by (induct n) (simp_all) ``` immler@50087 ` 81` immler@50087 ` 82` ```lemma diagseq_fold_reduce: "diagseq n = fold_reduce 0 n n" ``` immler@50087 ` 83` ``` using seqseq_fold_reduce by (simp add: diagseq_def) ``` immler@50087 ` 84` immler@50087 ` 85` ```lemma fold_reduce_add: "fold_reduce 0 (m + n) = fold_reduce 0 m o fold_reduce m n" ``` immler@50087 ` 86` ``` by (induct n) simp_all ``` immler@50087 ` 87` immler@50087 ` 88` ```lemma diagseq_add: "diagseq (k + n) = (seqseq k o (fold_reduce k n)) (k + n)" ``` immler@50087 ` 89` ```proof - ``` immler@50087 ` 90` ``` have "diagseq (k + n) = fold_reduce 0 (k + n) (k + n)" ``` immler@50087 ` 91` ``` by (simp add: diagseq_fold_reduce) ``` immler@50087 ` 92` ``` also have "\ = (seqseq k o fold_reduce k n) (k + n)" ``` immler@50087 ` 93` ``` unfolding fold_reduce_add seqseq_fold_reduce .. ``` immler@50087 ` 94` ``` finally show ?thesis . ``` immler@50087 ` 95` ```qed ``` immler@50087 ` 96` immler@50087 ` 97` ```lemma diagseq_sub: ``` immler@50087 ` 98` ``` assumes "m \ n" shows "diagseq n = (seqseq m o (fold_reduce m (n - m))) n" ``` immler@50087 ` 99` ``` using diagseq_add[of m "n - m"] assms by simp ``` immler@50087 ` 100` immler@50087 ` 101` ```lemma subseq_diagonal_rest: "subseq (\x. fold_reduce k x (k + x))" ``` immler@50087 ` 102` ``` unfolding subseq_Suc_iff fold_reduce.simps o_def ``` immler@50087 ` 103` ``` by (metis subseq_mono[OF subseq_fold_reduce] less_le_trans lessI add_Suc_right seq_suble ``` immler@50087 ` 104` ``` subseq_reducer) ``` immler@50087 ` 105` immler@50087 ` 106` ```lemma diagseq_seqseq: "diagseq o (op + k) = (seqseq k o (\x. fold_reduce k x (k + x)))" ``` immler@50087 ` 107` ``` by (auto simp: o_def diagseq_add) ``` immler@50087 ` 108` immler@50087 ` 109` ```end ``` immler@50087 ` 110` immler@50087 ` 111` ```end ```