src/HOL/Library/Diagonal_Subsequence.thy
author Manuel Eberl <eberlm@in.tum.de>
Mon Mar 26 16:14:16 2018 +0200 (19 months ago)
changeset 67951 655aa11359dc
parent 67399 eab6ce8368fa
permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
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"
wenzelm@67091
    11
  assumes ex_subseq: "\<And>n s. strict_mono (s::nat\<Rightarrow>nat) \<Longrightarrow> \<exists>r'. strict_mono r' \<and> P n (s \<circ> r')"
immler@50087
    12
begin
immler@50087
    13
wenzelm@67091
    14
definition reduce where "reduce s n = (SOME r'::nat\<Rightarrow>nat. strict_mono r' \<and> P n (s \<circ> r'))"
immler@52681
    15
immler@52681
    16
lemma subseq_reduce[intro, simp]:
eberlm@66447
    17
  "strict_mono s \<Longrightarrow> strict_mono (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:
wenzelm@67091
    21
  "strict_mono s \<Longrightarrow> P n (s \<circ> reduce s n)"
immler@52681
    22
  unfolding reduce_def by (rule someI2_ex[OF ex_subseq]) (auto simp: o_def)
immler@52681
    23
eberlm@66447
    24
primrec seqseq :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
immler@50087
    25
  "seqseq 0 = id"
wenzelm@67091
    26
| "seqseq (Suc n) = seqseq n \<circ> reduce (seqseq n) n"
immler@50087
    27
eberlm@66447
    28
lemma subseq_seqseq[intro, simp]: "strict_mono (seqseq n)"
immler@50087
    29
proof (induct n)
eberlm@66447
    30
  case 0 thus ?case by (simp add: strict_mono_def)
wenzelm@57862
    31
next
eberlm@66447
    32
  case (Suc n) thus ?case by (subst seqseq.simps) (auto intro!: strict_mono_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 -
wenzelm@67091
    38
  have "P n (seqseq n \<circ> 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
eberlm@66447
    43
definition diagseq :: "nat \<Rightarrow> nat" where "diagseq i = seqseq i i"
immler@52681
    44
immler@50087
    45
lemma diagseq_mono: "diagseq n < diagseq (Suc n)"
immler@52681
    46
proof -
immler@52681
    47
  have "diagseq n < seqseq n (Suc n)"
eberlm@66447
    48
    using subseq_seqseq[of n] by (simp add: diagseq_def strict_mono_def)
immler@52681
    49
  also have "\<dots> \<le> seqseq n (reduce (seqseq n) n (Suc n))"
eberlm@66447
    50
    using strict_mono_less_eq seq_suble by blast
immler@52681
    51
  also have "\<dots> = diagseq (Suc n)" by (simp add: diagseq_def)
immler@52681
    52
  finally show ?thesis .
immler@52681
    53
qed
immler@50087
    54
eberlm@66447
    55
lemma subseq_diagseq: "strict_mono diagseq"
eberlm@66447
    56
  using diagseq_mono by (simp add: strict_mono_Suc_iff diagseq_def)
immler@50087
    57
immler@50087
    58
primrec fold_reduce where
immler@50087
    59
  "fold_reduce n 0 = id"
wenzelm@67091
    60
| "fold_reduce n (Suc k) = fold_reduce n k \<circ> reduce (seqseq (n + k)) (n + k)"
immler@50087
    61
eberlm@66447
    62
lemma subseq_fold_reduce[intro, simp]: "strict_mono (fold_reduce n k)"
immler@50087
    63
proof (induct k)
eberlm@66447
    64
  case (Suc k) from strict_mono_o[OF this subseq_reduce] show ?case by (simp add: o_def)
eberlm@66447
    65
qed (simp add: strict_mono_def)
immler@50087
    66
wenzelm@67091
    67
lemma ex_subseq_reduce_index: "seqseq (n + k) = seqseq n \<circ> fold_reduce n k"
immler@50087
    68
  by (induct k) simp_all
immler@50087
    69
immler@50087
    70
lemma seqseq_fold_reduce: "seqseq n = fold_reduce 0 n"
immler@50087
    71
  by (induct n) (simp_all)
immler@50087
    72
immler@50087
    73
lemma diagseq_fold_reduce: "diagseq n = fold_reduce 0 n n"
immler@50087
    74
  using seqseq_fold_reduce by (simp add: diagseq_def)
immler@50087
    75
wenzelm@67091
    76
lemma fold_reduce_add: "fold_reduce 0 (m + n) = fold_reduce 0 m \<circ> fold_reduce m n"
immler@50087
    77
  by (induct n) simp_all
immler@50087
    78
wenzelm@67091
    79
lemma diagseq_add: "diagseq (k + n) = (seqseq k \<circ> (fold_reduce k n)) (k + n)"
immler@50087
    80
proof -
immler@50087
    81
  have "diagseq (k + n) = fold_reduce 0 (k + n) (k + n)"
immler@50087
    82
    by (simp add: diagseq_fold_reduce)
wenzelm@67091
    83
  also have "\<dots> = (seqseq k \<circ> fold_reduce k n) (k + n)"
immler@50087
    84
    unfolding fold_reduce_add seqseq_fold_reduce ..
immler@50087
    85
  finally show ?thesis .
immler@50087
    86
qed
immler@50087
    87
immler@50087
    88
lemma diagseq_sub:
wenzelm@67091
    89
  assumes "m \<le> n" shows "diagseq n = (seqseq m \<circ> (fold_reduce m (n - m))) n"
immler@50087
    90
  using diagseq_add[of m "n - m"] assms by simp
immler@50087
    91
eberlm@66447
    92
lemma subseq_diagonal_rest: "strict_mono (\<lambda>x. fold_reduce k x (k + x))"
eberlm@66447
    93
  unfolding strict_mono_Suc_iff fold_reduce.simps o_def
immler@52681
    94
proof
immler@52681
    95
  fix n
immler@52681
    96
  have "fold_reduce k n (k + n) < fold_reduce k n (k + Suc n)" (is "?lhs < _")
eberlm@66447
    97
    by (auto intro: strict_monoD)
immler@52681
    98
  also have "\<dots> \<le> fold_reduce k n (reduce (seqseq (k + n)) (k + n) (k + Suc n))"
eberlm@66447
    99
    by (auto intro: less_mono_imp_le_mono seq_suble strict_monoD)
immler@52681
   100
  finally show "?lhs < \<dots>" .
immler@52681
   101
qed
immler@50087
   102
nipkow@67399
   103
lemma diagseq_seqseq: "diagseq \<circ> ((+) k) = (seqseq k \<circ> (\<lambda>x. fold_reduce k x (k + x)))"
immler@50087
   104
  by (auto simp: o_def diagseq_add)
immler@50087
   105
immler@52681
   106
lemma diagseq_holds:
wenzelm@67091
   107
  assumes subseq_stable: "\<And>r s n. strict_mono r \<Longrightarrow> P n s \<Longrightarrow> P n (s \<circ> r)"
nipkow@67399
   108
  shows "P k (diagseq \<circ> ((+) (Suc k)))"
immler@52681
   109
  unfolding diagseq_seqseq by (intro subseq_stable subseq_diagonal_rest seqseq_holds)
immler@52681
   110
immler@50087
   111
end
immler@50087
   112
immler@50087
   113
end