src/HOL/Library/Diagonal_Subsequence.thy
 author Andreas Lochbihler Fri Sep 20 10:09:16 2013 +0200 (2013-09-20) changeset 53745 788730ab7da4 parent 52681 8cc7f76b827a child 57862 8f074e6e22fc permissions -rw-r--r--
prefer Code.abort over code_abort
 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@52681 ` 14` ```definition reduce where "reduce s n = (SOME r'. subseq r' \ P n (s o r'))" ``` immler@52681 ` 15` immler@52681 ` 16` ```lemma subseq_reduce[intro, simp]: ``` immler@52681 ` 17` ``` "subseq s \ subseq (reduce s n)" ``` immler@52681 ` 18` ``` unfolding reduce_def by (rule someI2_ex[OF ex_subseq]) auto ``` immler@52681 ` 19` immler@52681 ` 20` ```lemma reduce_holds: ``` immler@52681 ` 21` ``` "subseq s \ P n (s o reduce s n)" ``` immler@52681 ` 22` ``` unfolding reduce_def by (rule someI2_ex[OF ex_subseq]) (auto simp: o_def) ``` immler@52681 ` 23` immler@50087 ` 24` ```primrec seqseq where ``` immler@50087 ` 25` ``` "seqseq 0 = id" ``` immler@52681 ` 26` ```| "seqseq (Suc n) = seqseq n o reduce (seqseq n) n" ``` immler@50087 ` 27` immler@52681 ` 28` ```lemma subseq_seqseq[intro, simp]: "subseq (seqseq n)" ``` immler@50087 ` 29` ```proof (induct n) ``` immler@52681 ` 30` ``` case (Suc n) thus ?case by (subst seqseq.simps) (auto simp: subseq_reduce intro!: subseq_o) ``` immler@52681 ` 31` ```qed (simp add: subseq_def) ``` immler@52681 ` 32` immler@52681 ` 33` ```lemma seqseq_holds: ``` immler@52681 ` 34` ``` "P n (seqseq (Suc n))" ``` immler@52681 ` 35` ```proof - ``` immler@52681 ` 36` ``` have "P n (seqseq n o reduce (seqseq n) n)" ``` immler@52681 ` 37` ``` by (intro reduce_holds subseq_seqseq) ``` immler@52681 ` 38` ``` thus ?thesis by simp ``` immler@50087 ` 39` ```qed ``` immler@50087 ` 40` immler@50087 ` 41` ```definition diagseq where "diagseq i = seqseq i i" ``` immler@50087 ` 42` immler@52681 ` 43` ```lemma subseq_mono: "subseq f \ a \ b \ f a \ f b" ``` immler@52681 ` 44` ``` by (metis le_eq_less_or_eq subseq_mono) ``` immler@52681 ` 45` immler@52681 ` 46` ```lemma subseq_strict_mono: "subseq f \ a < b \ f a < f b" ``` immler@52681 ` 47` ``` by (simp add: subseq_def) ``` immler@52681 ` 48` immler@50087 ` 49` ```lemma diagseq_mono: "diagseq n < diagseq (Suc n)" ``` immler@52681 ` 50` ```proof - ``` immler@52681 ` 51` ``` have "diagseq n < seqseq n (Suc n)" ``` immler@52681 ` 52` ``` using subseq_seqseq[of n] by (simp add: diagseq_def subseq_def) ``` immler@52681 ` 53` ``` also have "\ \ seqseq n (reduce (seqseq n) n (Suc n))" ``` immler@52681 ` 54` ``` by (auto intro: subseq_mono seq_suble) ``` immler@52681 ` 55` ``` also have "\ = diagseq (Suc n)" by (simp add: diagseq_def) ``` immler@52681 ` 56` ``` finally show ?thesis . ``` immler@52681 ` 57` ```qed ``` immler@50087 ` 58` immler@50087 ` 59` ```lemma subseq_diagseq: "subseq diagseq" ``` immler@50087 ` 60` ``` using diagseq_mono by (simp add: subseq_Suc_iff diagseq_def) ``` immler@50087 ` 61` immler@50087 ` 62` ```primrec fold_reduce where ``` immler@50087 ` 63` ``` "fold_reduce n 0 = id" ``` immler@52681 ` 64` ```| "fold_reduce n (Suc k) = fold_reduce n k o reduce (seqseq (n + k)) (n + k)" ``` immler@50087 ` 65` immler@52681 ` 66` ```lemma subseq_fold_reduce[intro, simp]: "subseq (fold_reduce n k)" ``` immler@50087 ` 67` ```proof (induct k) ``` immler@52681 ` 68` ``` case (Suc k) from subseq_o[OF this subseq_reduce] show ?case by (simp add: o_def) ``` immler@50087 ` 69` ```qed (simp add: subseq_def) ``` immler@50087 ` 70` immler@50087 ` 71` ```lemma ex_subseq_reduce_index: "seqseq (n + k) = seqseq n o fold_reduce n k" ``` immler@50087 ` 72` ``` by (induct k) simp_all ``` immler@50087 ` 73` immler@50087 ` 74` ```lemma seqseq_fold_reduce: "seqseq n = fold_reduce 0 n" ``` immler@50087 ` 75` ``` by (induct n) (simp_all) ``` immler@50087 ` 76` immler@50087 ` 77` ```lemma diagseq_fold_reduce: "diagseq n = fold_reduce 0 n n" ``` immler@50087 ` 78` ``` using seqseq_fold_reduce by (simp add: diagseq_def) ``` immler@50087 ` 79` immler@50087 ` 80` ```lemma fold_reduce_add: "fold_reduce 0 (m + n) = fold_reduce 0 m o fold_reduce m n" ``` immler@50087 ` 81` ``` by (induct n) simp_all ``` immler@50087 ` 82` immler@50087 ` 83` ```lemma diagseq_add: "diagseq (k + n) = (seqseq k o (fold_reduce k n)) (k + n)" ``` immler@50087 ` 84` ```proof - ``` immler@50087 ` 85` ``` have "diagseq (k + n) = fold_reduce 0 (k + n) (k + n)" ``` immler@50087 ` 86` ``` by (simp add: diagseq_fold_reduce) ``` immler@50087 ` 87` ``` also have "\ = (seqseq k o fold_reduce k n) (k + n)" ``` immler@50087 ` 88` ``` unfolding fold_reduce_add seqseq_fold_reduce .. ``` immler@50087 ` 89` ``` finally show ?thesis . ``` immler@50087 ` 90` ```qed ``` immler@50087 ` 91` immler@50087 ` 92` ```lemma diagseq_sub: ``` immler@50087 ` 93` ``` assumes "m \ n" shows "diagseq n = (seqseq m o (fold_reduce m (n - m))) n" ``` immler@50087 ` 94` ``` using diagseq_add[of m "n - m"] assms by simp ``` immler@50087 ` 95` immler@50087 ` 96` ```lemma subseq_diagonal_rest: "subseq (\x. fold_reduce k x (k + x))" ``` immler@50087 ` 97` ``` unfolding subseq_Suc_iff fold_reduce.simps o_def ``` immler@52681 ` 98` ```proof ``` immler@52681 ` 99` ``` fix n ``` immler@52681 ` 100` ``` have "fold_reduce k n (k + n) < fold_reduce k n (k + Suc n)" (is "?lhs < _") ``` immler@52681 ` 101` ``` by (auto intro: subseq_strict_mono) ``` immler@52681 ` 102` ``` also have "\ \ fold_reduce k n (reduce (seqseq (k + n)) (k + n) (k + Suc n))" ``` immler@52681 ` 103` ``` by (rule subseq_mono) (auto intro!: seq_suble subseq_mono) ``` immler@52681 ` 104` ``` finally show "?lhs < \" . ``` immler@52681 ` 105` ```qed ``` immler@50087 ` 106` immler@50087 ` 107` ```lemma diagseq_seqseq: "diagseq o (op + k) = (seqseq k o (\x. fold_reduce k x (k + x)))" ``` immler@50087 ` 108` ``` by (auto simp: o_def diagseq_add) ``` immler@50087 ` 109` immler@52681 ` 110` ```lemma diagseq_holds: ``` immler@52681 ` 111` ``` assumes subseq_stable: "\r s n. subseq r \ P n s \ P n (s o r)" ``` immler@52681 ` 112` ``` shows "P k (diagseq o (op + (Suc k)))" ``` immler@52681 ` 113` ``` unfolding diagseq_seqseq by (intro subseq_stable subseq_diagonal_rest seqseq_holds) ``` immler@52681 ` 114` immler@50087 ` 115` ```end ``` immler@50087 ` 116` immler@50087 ` 117` ```end ```