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