Exercises/ex12/ex12.thy
changeset 69840 0c9bba1e8e97
child 69841 d2283b15d2ca
equal deleted inserted replaced
69839:ae4cb99d9ca2 69840:0c9bba1e8e97
       
     1 theory ex12
       
     2 imports Complex_Main
       
     3 begin
       
     4 
       
     5 subsection "Uebungsaufgabe"
       
     6 
       
     7 text \<open>Consider locale \<open>Queue\<close> in file \<open>Thys/Amortized_Examples\<close>. A call of \<open>deq (xs,[])\<close>
       
     8 requires the reversal of \<open>xs\<close>, which may be very long. We can reduce that impact
       
     9 by shifting \<open>xs\<close> over to \<open>ys\<close> whenever \<open>length xs > length ys\<close>. This does not improve
       
    10 the amortized complexity (in fact it increases it by 1) but reduces the worst case complexity
       
    11 of individual calls of \<open>deq\<close>. Modify local \<open>Queue\<close> as follows:\<close>
       
    12 
       
    13 locale Queue
       
    14 begin
       
    15 
       
    16 type_synonym 'a queue = "'a list * 'a list"
       
    17 
       
    18 fun balance :: "'a queue \<Rightarrow> 'a queue" where
       
    19 "balance(xs,ys) = (if size xs \<le> size ys then (xs,ys) else ([], ys @ rev xs))"
       
    20 
       
    21 fun enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
       
    22 "enq a (xs,ys) = balance (a#xs, ys)"
       
    23 
       
    24 fun deq :: "'a queue \<Rightarrow> 'a queue" where
       
    25 "deq (xs,ys) = balance (xs, tl ys)"
       
    26 
       
    27 fun t_enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> nat" where
       
    28 "t_enq a (xs,ys) = 1 + (if size xs + 1 \<le> size ys then 0 else size xs + 1 + size ys)"
       
    29 
       
    30 fun t_deq :: "'a queue \<Rightarrow> nat" where
       
    31 "t_deq (xs,ys) = (if size xs \<le> size ys - 1 then 0 else size xs + (size ys - 1))"
       
    32 
       
    33 end
       
    34 
       
    35 text \<open>You will also have to modify \<open>invar\<close> and \<open>\<Phi>\<close>. In the end you should be able to prove
       
    36 that the amortized complexity of \<open>enq\<close> is \<open> \<le> 3\<close> and of \<open>deq\<close> is \<open>= 0\<close>.\<close>
       
    37 
       
    38 (* hide *)
       
    39 context Queue
       
    40 begin
       
    41 
       
    42 definition "init = ([],[])"
       
    43 
       
    44 fun invar where
       
    45 "invar (xs,ys) = (size xs \<le> size ys)"
       
    46 
       
    47 fun \<Phi> :: "'a queue \<Rightarrow> nat" where
       
    48 "\<Phi> (xs,ys) = 2 * size xs"
       
    49 
       
    50 lemma "\<Phi> t \<ge> 0"
       
    51 apply(cases t)
       
    52 apply(auto)
       
    53 done
       
    54 
       
    55 lemma "\<Phi> init = 0"
       
    56 by(simp add: init_def)
       
    57 
       
    58 lemma a_enq: "invar q \<Longrightarrow> t_enq a q + \<Phi>(enq a q) - \<Phi> q \<le> 3"
       
    59 apply(cases q)
       
    60 apply(auto)
       
    61 done
       
    62 
       
    63 lemma a_deq: "invar q \<Longrightarrow> t_deq q + \<Phi>(deq q) - \<Phi> q = 0"
       
    64 apply(cases q)
       
    65 apply(auto)
       
    66 done
       
    67 
       
    68 end
       
    69 (* end hide *)
       
    70 
       
    71 subsection "Homework"
       
    72 
       
    73 type_synonym tab = "nat \<times> nat"
       
    74 
       
    75 text \<open>In file \<open>Thys/Amortized_Examples\<close> in the repository there is a formalization
       
    76 of dynamic tables in locale \<open>Dyn_Tab\<close> with the potential function \<open>\<Phi> (n,l) = 2*n - l\<close>
       
    77 and a discussion of why this is tricky. The standard definition you find in textbooks
       
    78 does not rely on cut-off subtraction on \<open>nat\<close> but uses standard real numbers:\<close>
       
    79 
       
    80 fun \<Phi> :: "tab \<Rightarrow> real" where
       
    81 "\<Phi> (n,l) = 2*(real n) - real l"
       
    82 
       
    83 text \<open>Start with the locale \<open>Dyn_Tab\<close> in file \<open>Thys/Amortized_Examples\<close>
       
    84 but use the above definition of \<open>\<Phi> :: tab \<Rightarrow> real\<close>. A number of proofs will now fail
       
    85 because the invariant is now too weak.
       
    86 Find a stronger invariant such that all the proofs work again.\<close>
       
    87 
       
    88 (* hide *)
       
    89 locale Dyn_Tab
       
    90 begin
       
    91 
       
    92 type_synonym tab = "nat \<times> nat"
       
    93 
       
    94 fun invar :: "tab \<Rightarrow> bool" where
       
    95 "invar (n,l) = (n=0 \<and> l = 0 \<or> l < 2*n \<and> n \<le> l)"
       
    96 
       
    97 definition init :: tab where
       
    98 "init = (0,0)"
       
    99 
       
   100 text\<open>Insertion: the element does not matter\<close>
       
   101 fun ins :: "tab \<Rightarrow> tab" where
       
   102 "ins (n,l) = (n+1, if n<l then l else if l=0 then 1 else 2*l)"
       
   103 
       
   104 text\<open>Time: if the table overflows, we count only the time for copying elements\<close>
       
   105 fun t_ins :: "nat \<times> nat \<Rightarrow> nat" where
       
   106 "t_ins (n,l) = (if n<l then 1 else n+1)"
       
   107 
       
   108 lemma "invar init"
       
   109 by(simp add: init_def)
       
   110 
       
   111 lemma "invar t \<Longrightarrow> invar(ins t)"
       
   112 apply(cases t)
       
   113 apply(auto)
       
   114 done
       
   115 
       
   116 fun \<Phi> :: "tab \<Rightarrow> real" where
       
   117 "\<Phi> (n,l) = 2*(real n) - real l"
       
   118 
       
   119 lemma "invar t \<Longrightarrow> \<Phi> t \<ge> 0"
       
   120 apply(cases t)
       
   121 apply(auto)
       
   122 done
       
   123 
       
   124 lemma "\<Phi> init = 0"
       
   125 by(simp add: init_def)
       
   126 
       
   127 lemma a_ins: "invar t \<Longrightarrow> t_ins t + \<Phi>(ins t) - \<Phi> t \<le> 3"
       
   128 apply(cases t)
       
   129 apply(auto split: if_splits)
       
   130 done
       
   131 
       
   132 end
       
   133 (* end hide *)
       
   134 
       
   135 end