Thys/Sparse_Binary_Numbers.thy
author nipkow
Mon, 31 Jul 2017 14:30:33 +0200
changeset 69882 f6d14918f41b
parent 69813 d7b714476f3f
permissions -rw-r--r--
.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
69813
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
     1
section \<open>Sparse Binary Numbers\<close>
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
     2
theory Sparse_Binary_Numbers
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
     3
imports Heap_Prelim
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
     4
begin
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
     5
 
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
     6
(*
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
     7
  Material for exercise:
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
     8
    Provide the definitions, let students prove the lemmas. 
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
     9
    Give a hint that they are analogous to binomial heap!
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    10
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    11
*)  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    12
  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    13
text \<open>
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    14
  We implement sparse binary numbers over ranks, 
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    15
  converting from the weight-based presentation of Okasaki.
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    16
\<close>
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    17
  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    18
(* TODO: borrow, decrement, sub *)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    19
subsection \<open>Datatype Definition\<close>  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    20
type_synonym rank = nat
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    21
type_synonym snat = "rank list"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    22
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    23
subsubsection \<open>Invariants\<close>  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    24
abbreviation invar :: "snat \<Rightarrow> bool" where "invar s \<equiv> strictly_ascending s"  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    25
definition \<alpha> :: "snat \<Rightarrow> nat" where "\<alpha> s = (\<Sum>i\<leftarrow>s. 2^i)"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    26
  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    27
lemma \<alpha>_Nil[simp]: "\<alpha> [] = 0"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    28
  unfolding \<alpha>_def by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    29
  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    30
lemma \<alpha>_Cons[simp]: "\<alpha> (r#rs) = 2^r + \<alpha> rs"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    31
  unfolding \<alpha>_def by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    32
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    33
lemma \<alpha>_append[simp]: "\<alpha> (rs\<^sub>1@rs\<^sub>2) = \<alpha> rs\<^sub>1 + \<alpha> rs\<^sub>2"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    34
  unfolding \<alpha>_def by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    35
    
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    36
subsection \<open>Operations\<close>    
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    37
    
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    38
fun carry :: "rank \<Rightarrow> snat \<Rightarrow> snat" where
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    39
  "carry r [] = [r]"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    40
| "carry r (r'#rest) = (if r<r' then r#r'#rest else carry (r+1) rest)"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    41
  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    42
lemma carry_invar[simp]:
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    43
  assumes "invar rs"  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    44
  shows "invar (carry r rs)"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    45
  using assms by (induction r rs rule: carry.induct) auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    46
    
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    47
lemma carry_\<alpha>:  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    48
  assumes "invar rs"  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    49
  assumes "\<forall>r'\<in>set rs. r\<le>r'"  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    50
  shows "\<alpha> (carry r rs) = 2^r + \<alpha> rs"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    51
  using assms
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    52
  by (induction r rs rule: carry.induct) force+
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    53
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    54
lemma carry_rank_bound:
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    55
  assumes "r' \<in> set (carry r rs)"  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    56
  assumes "\<forall>r'\<in>set rs. r\<^sub>0 < r'"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    57
  assumes "r\<^sub>0 < r"  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    58
  shows "r\<^sub>0 < r'"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    59
  using assms  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    60
  by (induction r rs rule: carry.induct) (auto split: if_splits)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    61
    
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    62
    
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    63
definition "inc rs = carry 0 rs"    
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    64
lemma inc_invar[simp]: "invar rs \<Longrightarrow> invar (inc rs)" 
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    65
  unfolding inc_def by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    66
  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    67
lemma inc_\<alpha>[simp]: "invar rs \<Longrightarrow> \<alpha> (inc rs) = Suc (\<alpha> rs)"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    68
  unfolding inc_def by (auto simp: carry_\<alpha>)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    69
  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    70
fun add :: "snat \<Rightarrow> snat \<Rightarrow> snat" where
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    71
  "add rs [] = rs"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    72
| "add [] rs = rs"  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    73
| "add (r\<^sub>1#rs\<^sub>1) (r\<^sub>2#rs\<^sub>2) = (
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    74
    if r\<^sub>1 < r\<^sub>2 then r\<^sub>1#add rs\<^sub>1 (r\<^sub>2#rs\<^sub>2)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    75
    else if r\<^sub>2<r\<^sub>1 then r\<^sub>2#add (r\<^sub>1#rs\<^sub>1) rs\<^sub>2
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    76
    else carry (r\<^sub>1 + 1) (add rs\<^sub>1 rs\<^sub>2)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    77
    )"  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    78
    
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    79
lemma add_rank_bound:
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    80
  assumes "r' \<in> set (add rs\<^sub>1 rs\<^sub>2)"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    81
  assumes "\<forall>r'\<in>set rs\<^sub>1. r < r'"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    82
  assumes "\<forall>r'\<in>set rs\<^sub>2. r < r'"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    83
  shows "r < r'"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    84
  using assms
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    85
  apply (induction rs\<^sub>1 rs\<^sub>2 arbitrary: r' rule: add.induct)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    86
  apply (auto split: if_splits simp: carry_rank_bound)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    87
  done
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    88
    
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    89
lemma add_invar[simp]:
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    90
  assumes "invar rs\<^sub>1"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    91
  assumes "invar rs\<^sub>2"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    92
  shows "invar (add rs\<^sub>1 rs\<^sub>2)"  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    93
  using assms
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    94
proof (induction rs\<^sub>1 rs\<^sub>2 rule: add.induct)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    95
  case (3 r\<^sub>1 rs\<^sub>1 r\<^sub>2 rs\<^sub>2)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    96
    
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    97
  consider (LT) "r\<^sub>1 < r\<^sub>2" 
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    98
         | (GT) "r\<^sub>1 > r\<^sub>2" 
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
    99
         | (EQ) "r\<^sub>1 = r\<^sub>2"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   100
    using antisym_conv3 by blast
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   101
  then show ?case proof cases
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   102
    case LT                          
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   103
    then show ?thesis using 3
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   104
      by (force elim!: add_rank_bound)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   105
  next
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   106
    case GT
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   107
    then show ?thesis using 3
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   108
      by (force elim!: add_rank_bound)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   109
  next
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   110
    case [simp]: EQ
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   111
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   112
    from "3.IH"(3) "3.prems" have [simp]: "invar (add rs\<^sub>1 rs\<^sub>2)"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   113
      by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   114
      
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   115
    have "r\<^sub>2 < r'" if "r' \<in> set (add rs\<^sub>1 rs\<^sub>2)" for r'
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   116
      using that
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   117
      apply (rule add_rank_bound)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   118
      using "3.prems" by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   119
    with EQ show ?thesis by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   120
  qed
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   121
qed simp_all
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   122
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   123
lemma add_\<alpha>[simp]:
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   124
  assumes "invar rs\<^sub>1"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   125
  assumes "invar rs\<^sub>2"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   126
  shows "\<alpha> (add rs\<^sub>1 rs\<^sub>2) = \<alpha> rs\<^sub>1 + \<alpha> rs\<^sub>2"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   127
  using assms
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   128
  apply (induction rs\<^sub>1 rs\<^sub>2 rule: add.induct)  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   129
  apply (auto simp: carry_\<alpha> Suc_leI add_rank_bound)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   130
  done  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   131
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   132
subsection \<open>Complexity\<close>
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   133
    
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   134
lemma size_snat:  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   135
  assumes "invar rs"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   136
  shows "2^length rs \<le> \<alpha> rs + 1"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   137
proof -
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   138
  have "(2::nat)^length rs = (\<Sum>i\<in>{0..<length rs}. 2^i) + 1" 
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   139
    by (simp add: power2sum)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   140
  also note strictly_ascending_sum_mono_lowerbound[OF \<open>invar rs\<close>, of "op ^ (2::nat)"]
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   141
  finally show "2 ^ length rs \<le> \<alpha> rs + 1" 
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   142
    unfolding \<alpha>_def by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   143
qed  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   144
  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   145
subsubsection \<open>Timing Functions\<close>
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   146
  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   147
fun t_carry :: "rank \<Rightarrow> snat \<Rightarrow> nat" where
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   148
  "t_carry r [] = 1"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   149
| "t_carry r (r'#rest) = (if r<r' then 1 else 1 + t_carry (r+1) rest)"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   150
  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   151
definition "t_inc rs = t_carry 0 rs"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   152
  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   153
lemma t_inc_bound: 
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   154
  assumes "invar rs"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   155
  shows "t_inc rs \<le> log 2 (\<alpha> rs + 1) + 1"  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   156
proof -
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   157
  have "t_carry r rs \<le> length rs + 1" for r 
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   158
    by (induction r rs rule: t_carry.induct) auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   159
  hence "t_inc rs \<le> length rs + 1" unfolding t_inc_def by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   160
  hence "(2::nat)^t_inc rs \<le> 2^(length rs + 1)" 
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   161
    by (rule power_increasing) auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   162
  also have "\<dots> \<le> 2*(\<alpha> rs + 1)" using size_snat[OF \<open>invar rs\<close>] by auto  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   163
  finally have "2 ^ t_inc rs \<le> 2 * (\<alpha> rs + 1)" .
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   164
  from le_log2_of_power[OF this] show ?thesis   
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   165
    by (simp only: log_mult of_nat_mult) auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   166
qed  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   167
  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   168
fun t_add :: "snat \<Rightarrow> snat \<Rightarrow> nat" where
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   169
  "t_add rs [] = 1"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   170
| "t_add [] rs = 1"  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   171
| "t_add (r\<^sub>1#rs\<^sub>1) (r\<^sub>2#rs\<^sub>2) = 1 + (
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   172
    if r\<^sub>1 < r\<^sub>2 then t_add rs\<^sub>1 (r\<^sub>2#rs\<^sub>2)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   173
    else if r\<^sub>2<r\<^sub>1 then t_add (r\<^sub>1#rs\<^sub>1) rs\<^sub>2
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   174
    else t_carry (r\<^sub>1 + 1) (add rs\<^sub>1 rs\<^sub>2) + t_add rs\<^sub>1 rs\<^sub>2
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   175
    )"  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   176
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   177
lemma l_carry_estimate: 
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   178
  "t_carry r rs + length (carry r rs) = 2 + length rs"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   179
  by (induction r rs rule: carry.induct) auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   180
  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   181
lemma l_add_estimate: 
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   182
  "length (add rs\<^sub>1 rs\<^sub>2) + t_add rs\<^sub>1 rs\<^sub>2 \<le> 2 * (length rs\<^sub>1 + length rs\<^sub>2) + 1"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   183
  apply (induction rs\<^sub>1 rs\<^sub>2 rule: t_add.induct)  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   184
  apply (auto simp: l_carry_estimate algebra_simps)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   185
  done
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   186
    
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   187
lemma t_add_bound:
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   188
  fixes rs\<^sub>1 rs\<^sub>2
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   189
  defines "n\<^sub>1 \<equiv> \<alpha> rs\<^sub>1"    
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   190
  defines "n\<^sub>2 \<equiv> \<alpha> rs\<^sub>2"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   191
  assumes INVARS: "invar rs\<^sub>1" "invar rs\<^sub>2"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   192
  shows "t_add rs\<^sub>1 rs\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 2"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   193
proof -
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   194
  define n where "n = n\<^sub>1 + n\<^sub>2"  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   195
      
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   196
  from l_add_estimate[of rs\<^sub>1 rs\<^sub>2] 
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   197
  have "t_add rs\<^sub>1 rs\<^sub>2 \<le> 2 * (length rs\<^sub>1 + length rs\<^sub>2) + 1" by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   198
  hence "(2::nat)^t_add rs\<^sub>1 rs\<^sub>2 \<le> 2^(2 * (length rs\<^sub>1 + length rs\<^sub>2) + 1)" 
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   199
    by (rule power_increasing) auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   200
  also have "\<dots> = 2*(2^length rs\<^sub>1)\<^sup>2*(2^length rs\<^sub>2)\<^sup>2"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   201
    by (auto simp: algebra_simps power_add power_mult)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   202
  also note INVARS(1)[THEN size_snat]
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   203
  also note INVARS(2)[THEN size_snat]
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   204
  finally have "2 ^ t_add rs\<^sub>1 rs\<^sub>2 \<le> 2 * (n\<^sub>1 + 1)\<^sup>2 * (n\<^sub>2 + 1)\<^sup>2" 
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   205
    by (auto simp: power2_nat_le_eq_le n\<^sub>1_def n\<^sub>2_def)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   206
  from le_log2_of_power[OF this] have "t_add rs\<^sub>1 rs\<^sub>2 \<le> log 2 \<dots>"    
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   207
    by simp
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   208
  also have "\<dots> = log 2 2 + 2*log 2 (n\<^sub>1 + 1) + 2*log 2 (n\<^sub>2 + 1)"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   209
    by (simp add: log_mult log_nat_power)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   210
  also have "n\<^sub>2 \<le> n" by (auto simp: n_def)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   211
  finally have "t_add rs\<^sub>1 rs\<^sub>2 \<le> log 2 2 + 2*log 2 (n\<^sub>1 + 1) + 2*log 2 (n + 1)"    
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   212
    by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   213
  also have "n\<^sub>1 \<le> n" by (auto simp: n_def)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   214
  finally have "t_add rs\<^sub>1 rs\<^sub>2 \<le> log 2 2 + 4*log 2 (n + 1)"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   215
    by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   216
  also have "log 2 2 \<le> 2" by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   217
  finally have "t_add rs\<^sub>1 rs\<^sub>2 \<le> 4*log 2 (n + 1) + 2" by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   218
  thus ?thesis unfolding n_def by (auto simp: algebra_simps)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   219
qed      
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   220
  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   221
subsection \<open>Representable Number\<close>
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   222
text \<open>
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   223
  Estimating the largest representable number if indices are bounded by \<open>K\<close>
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   224
\<close>  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   225
(* Exercise! *)  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   226
  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   227
definition "max_snat K = [0..<K]"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   228
lemma "invar (max_snat K)"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   229
  unfolding max_snat_def by (induction K) auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   230
  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   231
lemma \<alpha>_max_snat: "\<alpha> (max_snat K) = 2^K - 1"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   232
  unfolding \<alpha>_def max_snat_def
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   233
  by (simp add: interv_sum_list_conv_sum_set_nat power2sum)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   234
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   235
text \<open>Indices in @{term \<open>max_snat K\<close>} are actually bounded by @{term \<open>K\<close>}\<close>
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   236
lemma max_snat_bounded: "\<forall>r\<in>set (max_snat K). r<K"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   237
  unfolding max_snat_def by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   238
  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   239
text \<open>@{term \<open>max_snat K\<close>} is maximal\<close>
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   240
lemma max_snat_max:
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   241
  assumes "invar rs"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   242
  assumes "\<forall>r\<in>set rs. r<K"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   243
  shows "\<alpha> rs \<le> \<alpha> (max_snat K)"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   244
  unfolding \<alpha>_max_snat 
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   245
  using assms
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   246
proof (induction rs arbitrary: K rule: rev_induct)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   247
  case Nil
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   248
  then show ?case by simp
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   249
next
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   250
  case (snoc r rs)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   251
  from snoc.prems have "invar rs" "\<forall>r'\<in>set rs. r'<r" by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   252
  from snoc.IH[OF this] have IH: "\<alpha> rs \<le> 2 ^ r - 1" .    
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   253
    
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   254
  from snoc.prems have "r<K" by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   255
  hence "r+1 \<le> K" by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   256
      
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   257
  have "\<alpha> (rs @ [r]) = \<alpha> rs + 2^r" unfolding \<alpha>_def by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   258
  also have "\<dots> \<le> 2^r - 1 + 2^r" using IH by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   259
  also have "\<dots> = 2^(r+1) - 1" by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   260
  also note \<open>r+1 \<le> K\<close>
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   261
  finally show ?case by (auto simp: diff_le_mono)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   262
qed    
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   263
  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   264
subsubsection \<open>Injectivity\<close>    
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   265
  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   266
(* Bonus Exercise! *)  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   267
lemma \<alpha>_inj:
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   268
  assumes "invar rs\<^sub>1" "invar rs\<^sub>2"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   269
  shows "\<alpha> rs\<^sub>1 = \<alpha> rs\<^sub>2 \<longleftrightarrow> rs\<^sub>1 = rs\<^sub>2"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   270
proof safe  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   271
  assume "\<alpha> rs\<^sub>1 = \<alpha> rs\<^sub>2"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   272
  thus "rs\<^sub>1 = rs\<^sub>2" using assms
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   273
  proof (induction rs\<^sub>1 arbitrary: rs\<^sub>2 rule: rev_induct)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   274
    case Nil
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   275
    then show ?case by (cases rs\<^sub>2) auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   276
  next
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   277
    case (snoc r\<^sub>1 rs\<^sub>1 xrs\<^sub>2)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   278
      
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   279
    show ?case proof (cases xrs\<^sub>2 rule: rev_cases)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   280
      case Nil
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   281
      then show ?thesis using snoc.prems by simp
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   282
    next
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   283
      case snoc2[simp]: (snoc rs\<^sub>2 r\<^sub>2)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   284
        
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   285
      from snoc.prems have "invar rs\<^sub>1" "invar rs\<^sub>2" by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   286
        
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   287
      consider (EQ) "r\<^sub>1 = r\<^sub>2" | (LT) "r\<^sub>1 < r\<^sub>2" | (GT) "r\<^sub>1 > r\<^sub>2"
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   288
        using less_linear by blast
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   289
      thus ?thesis proof (cases)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   290
        case EQ
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   291
        then show ?thesis using snoc by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   292
      next
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   293
        case LT
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   294
        from snoc.prems have "\<forall>r\<in>set rs\<^sub>1. r<r\<^sub>1" by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   295
        from max_snat_max[unfolded \<alpha>_max_snat, OF \<open>invar rs\<^sub>1\<close> this] 
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   296
        have "\<alpha> rs\<^sub>1 < 2 ^ r\<^sub>1" 
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   297
          by auto (metis Suc_pred le_imp_less_Suc pos2 zero_less_power)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   298
        hence "\<alpha> (rs\<^sub>1@[r\<^sub>1]) < 2 ^ (r\<^sub>1 + 1)" by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   299
        also have \<open>r\<^sub>1 + 1 \<le> r\<^sub>2\<close> using LT by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   300
        finally have "\<alpha> (rs\<^sub>1 @ [r\<^sub>1]) < 2 ^ r\<^sub>2" by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   301
        also have "\<alpha> xrs\<^sub>2 \<ge> 2 ^ r\<^sub>2" by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   302
        finally have False using \<open>\<alpha> (rs\<^sub>1 @ [r\<^sub>1]) = \<alpha> xrs\<^sub>2\<close> by simp
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   303
        then show ?thesis ..
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   304
      next
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   305
        case GT
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   306
        text \<open>Analogously\<close>  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   307
        from snoc.prems have "\<forall>r\<in>set rs\<^sub>2. r<r\<^sub>2" by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   308
        from max_snat_max[unfolded \<alpha>_max_snat, OF \<open>invar rs\<^sub>2\<close> this] 
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   309
        have "\<alpha> rs\<^sub>2 < 2 ^ r\<^sub>2" 
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   310
          by auto (metis Suc_pred le_imp_less_Suc pos2 zero_less_power)
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   311
        hence "\<alpha> xrs\<^sub>2 < 2 ^ (r\<^sub>2 + 1)" by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   312
        also have \<open>r\<^sub>2 + 1 \<le> r\<^sub>1\<close> using GT by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   313
        finally have "\<alpha> (rs\<^sub>2 @ [r\<^sub>2]) < 2 ^ r\<^sub>1" by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   314
        also have "\<alpha> (rs\<^sub>1@[r\<^sub>1]) \<ge> 2 ^ r\<^sub>1" by auto
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   315
        finally have False using \<open>\<alpha> (rs\<^sub>1 @ [r\<^sub>1]) = \<alpha> xrs\<^sub>2\<close> by simp
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   316
        then show ?thesis ..
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   317
      qed  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   318
    qed
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   319
  qed
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   320
qed    
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   321
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   322
  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   323
  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   324
  
d7b714476f3f Revived exercises
lammich <lammich@in.tum.de>
parents:
diff changeset
   325
end