src/HOL/Library/Diagonal_Subsequence.thy
author wenzelm
Mon Dec 28 01:28:28 2015 +0100 (2015-12-28)
changeset 61945 1135b8de26c3
parent 60500 903bb1495239
child 66447 a1f5c5c26fa6
permissions -rw-r--r--
more symbols;
immler@50087
     1
(* Author: Fabian Immler, TUM *)
immler@50087
     2
wenzelm@60500
     3
section \<open>Sequence of Properties on Subsequences\<close>
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\<Rightarrow>(nat\<Rightarrow>nat)\<Rightarrow>bool"
immler@50087
    11
  assumes ex_subseq: "\<And>n s. subseq s \<Longrightarrow> \<exists>r'. subseq r' \<and> 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' \<and> P n (s o r'))"
immler@52681
    15
immler@52681
    16
lemma subseq_reduce[intro, simp]:
immler@52681
    17
  "subseq s \<Longrightarrow> 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 \<Longrightarrow> 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)
wenzelm@57862
    30
  case 0 thus ?case by (simp add: subseq_def)
wenzelm@57862
    31
next
wenzelm@57862
    32
  case (Suc n) thus ?case by (subst seqseq.simps) (auto intro!: subseq_o)
wenzelm@57862
    33
qed
immler@52681
    34
immler@52681
    35
lemma seqseq_holds:
immler@52681
    36
  "P n (seqseq (Suc n))"
immler@52681
    37
proof -
immler@52681
    38
  have "P n (seqseq n o reduce (seqseq n) n)"
immler@52681
    39
    by (intro reduce_holds subseq_seqseq)
immler@52681
    40
  thus ?thesis by simp
immler@50087
    41
qed
immler@50087
    42
immler@50087
    43
definition diagseq where "diagseq i = seqseq i i"
immler@50087
    44
immler@52681
    45
lemma subseq_mono: "subseq f \<Longrightarrow> a \<le> b \<Longrightarrow> f a \<le> f b"
immler@52681
    46
  by (metis le_eq_less_or_eq subseq_mono)
immler@52681
    47
immler@52681
    48
lemma subseq_strict_mono: "subseq f \<Longrightarrow> a < b \<Longrightarrow> f a < f b"
immler@52681
    49
  by (simp add: subseq_def)
immler@52681
    50
immler@50087
    51
lemma diagseq_mono: "diagseq n < diagseq (Suc n)"
immler@52681
    52
proof -
immler@52681
    53
  have "diagseq n < seqseq n (Suc n)"
immler@52681
    54
    using subseq_seqseq[of n] by (simp add: diagseq_def subseq_def)
immler@52681
    55
  also have "\<dots> \<le> seqseq n (reduce (seqseq n) n (Suc n))"
immler@52681
    56
    by (auto intro: subseq_mono seq_suble)
immler@52681
    57
  also have "\<dots> = diagseq (Suc n)" by (simp add: diagseq_def)
immler@52681
    58
  finally show ?thesis .
immler@52681
    59
qed
immler@50087
    60
immler@50087
    61
lemma subseq_diagseq: "subseq diagseq"
immler@50087
    62
  using diagseq_mono by (simp add: subseq_Suc_iff diagseq_def)
immler@50087
    63
immler@50087
    64
primrec fold_reduce where
immler@50087
    65
  "fold_reduce n 0 = id"
immler@52681
    66
| "fold_reduce n (Suc k) = fold_reduce n k o reduce (seqseq (n + k)) (n + k)"
immler@50087
    67
immler@52681
    68
lemma subseq_fold_reduce[intro, simp]: "subseq (fold_reduce n k)"
immler@50087
    69
proof (induct k)
immler@52681
    70
  case (Suc k) from subseq_o[OF this subseq_reduce] show ?case by (simp add: o_def)
immler@50087
    71
qed (simp add: subseq_def)
immler@50087
    72
immler@50087
    73
lemma ex_subseq_reduce_index: "seqseq (n + k) = seqseq n o fold_reduce n k"
immler@50087
    74
  by (induct k) simp_all
immler@50087
    75
immler@50087
    76
lemma seqseq_fold_reduce: "seqseq n = fold_reduce 0 n"
immler@50087
    77
  by (induct n) (simp_all)
immler@50087
    78
immler@50087
    79
lemma diagseq_fold_reduce: "diagseq n = fold_reduce 0 n n"
immler@50087
    80
  using seqseq_fold_reduce by (simp add: diagseq_def)
immler@50087
    81
immler@50087
    82
lemma fold_reduce_add: "fold_reduce 0 (m + n) = fold_reduce 0 m o fold_reduce m n"
immler@50087
    83
  by (induct n) simp_all
immler@50087
    84
immler@50087
    85
lemma diagseq_add: "diagseq (k + n) = (seqseq k o (fold_reduce k n)) (k + n)"
immler@50087
    86
proof -
immler@50087
    87
  have "diagseq (k + n) = fold_reduce 0 (k + n) (k + n)"
immler@50087
    88
    by (simp add: diagseq_fold_reduce)
immler@50087
    89
  also have "\<dots> = (seqseq k o fold_reduce k n) (k + n)"
immler@50087
    90
    unfolding fold_reduce_add seqseq_fold_reduce ..
immler@50087
    91
  finally show ?thesis .
immler@50087
    92
qed
immler@50087
    93
immler@50087
    94
lemma diagseq_sub:
immler@50087
    95
  assumes "m \<le> n" shows "diagseq n = (seqseq m o (fold_reduce m (n - m))) n"
immler@50087
    96
  using diagseq_add[of m "n - m"] assms by simp
immler@50087
    97
immler@50087
    98
lemma subseq_diagonal_rest: "subseq (\<lambda>x. fold_reduce k x (k + x))"
immler@50087
    99
  unfolding subseq_Suc_iff fold_reduce.simps o_def
immler@52681
   100
proof
immler@52681
   101
  fix n
immler@52681
   102
  have "fold_reduce k n (k + n) < fold_reduce k n (k + Suc n)" (is "?lhs < _")
immler@52681
   103
    by (auto intro: subseq_strict_mono)
immler@52681
   104
  also have "\<dots> \<le> fold_reduce k n (reduce (seqseq (k + n)) (k + n) (k + Suc n))"
immler@52681
   105
    by (rule subseq_mono) (auto intro!: seq_suble subseq_mono)
immler@52681
   106
  finally show "?lhs < \<dots>" .
immler@52681
   107
qed
immler@50087
   108
immler@50087
   109
lemma diagseq_seqseq: "diagseq o (op + k) = (seqseq k o (\<lambda>x. fold_reduce k x (k + x)))"
immler@50087
   110
  by (auto simp: o_def diagseq_add)
immler@50087
   111
immler@52681
   112
lemma diagseq_holds:
immler@52681
   113
  assumes subseq_stable: "\<And>r s n. subseq r \<Longrightarrow> P n s \<Longrightarrow> P n (s o r)"
immler@52681
   114
  shows "P k (diagseq o (op + (Suc k)))"
immler@52681
   115
  unfolding diagseq_seqseq by (intro subseq_stable subseq_diagonal_rest seqseq_holds)
immler@52681
   116
immler@50087
   117
end
immler@50087
   118
immler@50087
   119
end