src/HOL/Library/SCT_Misc.thy
author chaieb
Mon Jun 11 11:06:04 2007 +0200 (2007-06-11)
changeset 23315 df3a7e9ebadb
parent 23002 b469cf6dc531
child 23373 ead82c82da9e
permissions -rw-r--r--
tuned Proof
krauss@22371
     1
(*  Title:      HOL/Library/SCT_Misc.thy
krauss@22371
     2
    ID:         $Id$
krauss@22371
     3
    Author:     Alexander Krauss, TU Muenchen
krauss@22371
     4
*)
krauss@22371
     5
wenzelm@22665
     6
header ""
wenzelm@22665
     7
krauss@22359
     8
theory SCT_Misc
krauss@22359
     9
imports Main
krauss@22359
    10
begin
krauss@22359
    11
krauss@22359
    12
subsection {* Searching in lists *}
krauss@22359
    13
krauss@22359
    14
fun index_of :: "'a list \<Rightarrow> 'a \<Rightarrow> nat"
krauss@22359
    15
where
krauss@22359
    16
  "index_of [] c = 0"
krauss@22359
    17
| "index_of (x#xs) c = (if x = c then 0 else Suc (index_of xs c))"
krauss@22359
    18
krauss@22359
    19
lemma index_of_member: 
krauss@22359
    20
  "(x \<in> set l) \<Longrightarrow> (l ! index_of l x = x)"
krauss@22359
    21
  by (induct l) auto
krauss@22359
    22
krauss@22359
    23
lemma index_of_length:
krauss@22359
    24
  "(x \<in> set l) = (index_of l x < length l)"
krauss@22359
    25
  by (induct l) auto
krauss@22359
    26
krauss@22359
    27
subsection {* Some reasoning tools *}
krauss@22359
    28
krauss@22359
    29
lemma three_cases:
krauss@22359
    30
  assumes "a1 \<Longrightarrow> thesis"
krauss@22359
    31
  assumes "a2 \<Longrightarrow> thesis"
krauss@22359
    32
  assumes "a3 \<Longrightarrow> thesis"
krauss@22359
    33
  assumes "\<And>R. \<lbrakk>a1 \<Longrightarrow> R; a2 \<Longrightarrow> R; a3 \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
krauss@22359
    34
  shows "thesis"
krauss@22359
    35
  using prems
krauss@22359
    36
  by auto
krauss@22359
    37
wenzelm@22665
    38
wenzelm@22665
    39
subsection {* Sequences *}
krauss@22359
    40
krauss@22359
    41
types
krauss@22359
    42
  'a sequence = "nat \<Rightarrow> 'a"
krauss@22359
    43
wenzelm@22665
    44
wenzelm@22665
    45
subsubsection {* Increasing sequences *}
krauss@22359
    46
krauss@22359
    47
definition increasing :: "(nat \<Rightarrow> nat) \<Rightarrow> bool"
krauss@22359
    48
where
krauss@22359
    49
  "increasing s = (\<forall>i j. i < j \<longrightarrow> s i < s j)"
krauss@22359
    50
krauss@22359
    51
lemma increasing_strict:
krauss@22359
    52
  assumes "increasing s"
krauss@22359
    53
  assumes "i < j"
krauss@22359
    54
  shows "s i < s j"
krauss@22359
    55
  using prems
krauss@22359
    56
  unfolding increasing_def by simp
krauss@22359
    57
krauss@22359
    58
lemma increasing_weak:
krauss@22359
    59
  assumes "increasing s"
krauss@22359
    60
  assumes "i \<le> j"
krauss@22359
    61
  shows "s i \<le> s j"
krauss@22359
    62
  using prems increasing_strict[of s i j]
krauss@22359
    63
  by (cases "i<j") auto
krauss@22359
    64
krauss@22359
    65
lemma increasing_inc:
krauss@22359
    66
  assumes [simp]: "increasing s"
krauss@22359
    67
  shows "n \<le> s n"
krauss@22359
    68
proof (induct n)
krauss@22359
    69
  case (Suc n)
krauss@22359
    70
  with increasing_strict[of s n "Suc n"]
krauss@22359
    71
  show ?case by auto
krauss@22359
    72
qed auto
krauss@22359
    73
krauss@22359
    74
lemma increasing_bij:
krauss@22359
    75
  assumes [simp]: "increasing s"
krauss@22359
    76
  shows "(s i < s j) = (i < j)"
krauss@22359
    77
proof
krauss@22359
    78
  assume "s i < s j"
krauss@22359
    79
  show "i < j"
krauss@22359
    80
  proof (rule classical)
krauss@22359
    81
    assume "\<not> ?thesis"
krauss@22359
    82
    hence "j \<le> i" by arith
krauss@22359
    83
    with increasing_weak have "s j \<le> s i" by simp
krauss@22359
    84
    with `s i < s j` show ?thesis by simp
krauss@22359
    85
  qed
krauss@22359
    86
qed (simp add:increasing_strict)
krauss@22359
    87
wenzelm@22665
    88
wenzelm@22665
    89
subsubsection {* Sections induced by an increasing sequence *}
krauss@22359
    90
krauss@22359
    91
abbreviation
krauss@22359
    92
  "section s i == {s i ..< s (Suc i)}"
krauss@22359
    93
krauss@22359
    94
definition
krauss@22359
    95
  "section_of s n = (LEAST i. n < s (Suc i))"
krauss@22359
    96
krauss@22359
    97
lemma section_help:
krauss@22359
    98
  assumes [intro, simp]: "increasing s"
krauss@22359
    99
  shows "\<exists>i. n < s (Suc i)" 
krauss@22359
   100
proof -
krauss@22359
   101
  from increasing_inc have "n \<le> s n" .
krauss@22359
   102
  also from increasing_strict have "\<dots> < s (Suc n)" by simp
krauss@22359
   103
  finally show ?thesis ..
krauss@22359
   104
qed
krauss@22359
   105
krauss@22359
   106
lemma section_of2:
krauss@22359
   107
  assumes "increasing s"
krauss@22359
   108
  shows "n < s (Suc (section_of s n))"
krauss@22359
   109
  unfolding section_of_def
krauss@22359
   110
  by (rule LeastI_ex) (rule section_help)
krauss@22359
   111
krauss@22359
   112
lemma section_of1:
krauss@22359
   113
  assumes [simp, intro]: "increasing s"
krauss@22359
   114
  assumes "s i \<le> n"
krauss@22359
   115
  shows "s (section_of s n) \<le> n"
krauss@22359
   116
proof (rule classical)
krauss@22359
   117
  let ?m = "section_of s n"
krauss@22359
   118
krauss@22359
   119
  assume "\<not> ?thesis"
krauss@22359
   120
  hence a: "n < s ?m" by simp
krauss@22359
   121
  
krauss@22359
   122
  have nonzero: "?m \<noteq> 0"
krauss@22359
   123
  proof
krauss@22359
   124
    assume "?m = 0"
krauss@22359
   125
    from increasing_weak have "s 0 \<le> s i" by simp
krauss@22359
   126
    also note `\<dots> \<le> n`
krauss@22359
   127
    finally show False using `?m = 0` `n < s ?m` by simp 
krauss@22359
   128
  qed
krauss@22359
   129
  with a have "n < s (Suc (?m - 1))" by simp
krauss@22359
   130
  with Least_le have "?m \<le> ?m - 1"
krauss@22359
   131
    unfolding section_of_def .
krauss@22359
   132
  with nonzero show ?thesis by simp
krauss@22359
   133
qed
krauss@22359
   134
krauss@22359
   135
lemma section_of_known: 
krauss@22359
   136
  assumes [simp]: "increasing s"
krauss@22359
   137
  assumes in_sect: "k \<in> section s i"
krauss@22359
   138
  shows "section_of s k = i" (is "?s = i")
krauss@22359
   139
proof (rule classical)
krauss@22359
   140
  assume "\<not> ?thesis"
krauss@22359
   141
krauss@22359
   142
  hence "?s < i \<or> ?s > i" by arith
krauss@22359
   143
  thus ?thesis
krauss@22359
   144
  proof
krauss@22359
   145
    assume "?s < i"
krauss@22359
   146
    hence "Suc ?s \<le> i" by simp
krauss@22359
   147
    with increasing_weak have "s (Suc ?s) \<le> s i" by simp
krauss@22359
   148
    moreover have "k < s (Suc ?s)" using section_of2 by simp
krauss@22359
   149
    moreover from in_sect have "s i \<le> k" by simp
krauss@22359
   150
    ultimately show ?thesis by simp 
krauss@22359
   151
  next
krauss@22359
   152
    assume "i < ?s" hence "Suc i \<le> ?s" by simp
krauss@22359
   153
    with increasing_weak have "s (Suc i) \<le> s ?s" by simp
krauss@22359
   154
    moreover 
krauss@22359
   155
    from in_sect have "s i \<le> k" by simp
krauss@22359
   156
    with section_of1 have "s ?s \<le> k" by simp
krauss@22359
   157
    moreover from in_sect have "k < s (Suc i)" by simp
krauss@22359
   158
    ultimately show ?thesis by simp
krauss@22359
   159
  qed
krauss@22359
   160
qed 
krauss@22359
   161
  
krauss@22359
   162
lemma in_section_of: 
krauss@22359
   163
  assumes [simp, intro]: "increasing s"
krauss@22359
   164
  assumes "s i \<le> k"
krauss@22359
   165
  shows "k \<in> section s (section_of s k)"
krauss@22359
   166
  using prems
krauss@22359
   167
  by (auto intro:section_of1 section_of2)
krauss@22359
   168
krauss@22371
   169
end