Quelle Array_Braun.thy Sprache: Isabelle

(* Author: Tobias Nipkow, with contributions by Thomas Sewell *)

section "Arrays via Braun Trees"

theory Array_Braun
imports
  "HOL-Library.Time_Functions"
  Array_Specs
  Braun_Tree
begin

subsection "Array"

fun lookup1 :: "'a tree \ nat \ 'a" where
  "lookup1 (Node l x r) n = (if n=1 then x else lookup1 (if even n then l else r) (n div 2))"

fun update1 :: "nat \ 'a \ 'a tree \ 'a tree" where
  "update1 n x Leaf = Node Leaf x Leaf" |
  "update1 n x (Node l a r) =
  (if n=1 then Node l x r else
   if even n then Node (update1 (n div 2) x l) a r
            else Node l a (update1 (n div 2) x r))"

fun adds :: "'a list \ nat \ 'a tree \ 'a tree" where
  "adds [] n t = t" |
  "adds (x#xs) n t = adds xs (n+1) (update1 (n+1) x t)"

fun list :: "'a tree \ 'a list" where
  "list Leaf = []" |
  "list (Node l x r) = x # splice (list l) (list r)"

subsubsection "Functional Correctness"

lemma size_list: "size(list t) = size t"
  by(induction t)(auto)

lemma minus1_div2: "(n - Suc 0) div 2 = (if odd n then n div 2 else n div 2 - 1)"
  by auto arith

lemma nth_splice: "\ n < size xs + size ys; size ys \ size xs; size xs \ size ys + 1 \
  \<Longrightarrow> splice xs ys ! n = (if even n then xs else ys) ! (n div 2)"
proof(induction xs ys arbitrary: n rule: splice.induct)
qed (auto simp: nth_Cons' minus1_div2)

lemma div2_in_bounds:
  "\ braun (Node l x r); n \ {1..size(Node l x r)}; n > 1 \ \
   (odd n \<longrightarrow> n div 2 \<in> {1..size r}) \<and> (even n \<longrightarrow> n div 2 \<in> {1..size l})"
  by auto arith

declare upt_Suc[simp del]

paragraph \<open>\<^const>\<open>lookup1\<close>\<close>

lemma nth_list_lookup1: "\braun t; i < size t\ \ list t ! i = lookup1 t (i+1)"
proof(induction t arbitrary: i)
  case Leaf thus ?case by simp
next
  case Node
  thus ?case using div2_in_bounds[OF Node.prems(1), of "i+1"]
    by (auto simp: nth_splice minus1_div2 size_list)
qed

lemma list_eq_map_lookup1: "braun t \ list t = map (lookup1 t) [1..
  by(auto simp add: list_eq_iff_nth_eq size_list nth_list_lookup1)

paragraph \<open>\<^const>\<open>update1\<close>\<close>

lemma size_update1: "\ braun t; n \ {1.. size t} \ \ size(update1 n x t) = size t"
proof(induction t arbitrary: n)
  case Leaf thus ?case by simp
next
  case Node thus ?case using div2_in_bounds[OF Node.prems] by simp
qed

lemma braun_update1: "\braun t; n \ {1.. size t} \ \ braun(update1 n x t)"
proof(induction t arbitrary: n)
  case Leaf thus ?case by simp
next
  case Node thus ?case
    using div2_in_bounds[OF Node.prems] by (simp add: size_update1)
qed

lemma lookup1_update1: "\ braun t; n \ {1.. size t} \ \
  lookup1 (update1 n x t) m = (if n=m then x else lookup1 t m)"
proof(induction t arbitrary: m n)
  case Leaf
  then show ?case by simp
next
  have aux: "\ odd n; odd m \ \ n div 2 = (m::nat) div 2 \ m=n" for m n
    using odd_two_times_div_two_succ by fastforce
  case Node
  thus ?case using div2_in_bounds[OF Node.prems] by (auto simp: aux)
qed

lemma list_update1: "\ braun t; n \ {1.. size t} \ \ list(update1 n x t) = (list t)[n-1 := x]"
  by(auto simp add: list_eq_map_lookup1 list_eq_iff_nth_eq lookup1_update1 size_update1 braun_update1)

text \<open>A second proof of @{thm list_update1}:\<close>

lemma diff1_eq_iff: "n > 0 \ n - Suc 0 = m \ n = m+1"
  by arith

lemma list_update_splice:
  "\ n < size xs + size ys; size ys \ size xs; size xs \ size ys + 1 \ \
  (splice xs ys) [n := x] =
  (if even n then splice (xs[n div 2 := x]) ys else splice xs (ys[n div 2 := x]))"
  by(induction xs ys arbitrary: n rule: splice.induct) (auto split: nat.split)

lemma list_update2: "\ braun t; n \ {1.. size t} \ \ list(update1 n x t) = (list t)[n-1 := x]"
proof(induction t arbitrary: n)
  case Leaf thus ?case by simp
next
  case (Node l a r) thus ?case using div2_in_bounds[OF Node.prems]
    by(auto simp: list_update_splice diff1_eq_iff size_list split: nat.split)
qed

paragraph \<open>\<^const>\<open>adds\<close>\<close>

lemma splice_last: shows
  "size ys \ size xs \ splice (xs @ [x]) ys = splice xs ys @ [x]"
  and "size ys+1 \ size xs \ splice xs (ys @ [y]) = splice xs ys @ [y]"
  by(induction xs ys arbitrary: x y rule: splice.induct) (auto)

lemma list_add_hi: "braun t \ list(update1 (Suc(size t)) x t) = list t @ [x]"
  by(induction t)(auto simp: splice_last size_list)

lemma size_add_hi: "braun t \ m = size t \ size(update1 (Suc m) x t) = size t + 1"
  by(induction t arbitrary: m)(auto)

lemma braun_add_hi: "braun t \ braun(update1 (Suc(size t)) x t)"
  by(induction t)(auto simp: size_add_hi)

lemma size_braun_adds:
  "\ braun t; size t = n \ \ size(adds xs n t) = size t + length xs \ braun (adds xs n t)"
  by(induction xs arbitrary: t n)(auto simp: braun_add_hi size_add_hi)

lemma list_adds: "\ braun t; size t = n \ \ list(adds xs n t) = list t @ xs"
  by(induction xs arbitrary: t n)(auto simp: size_braun_adds list_add_hi size_add_hi braun_add_hi)

subsubsection "Array Implementation"

interpretation A: Array
  where lookup = "\(t,l) n. lookup1 t (n+1)"
    and update = "\n x (t,l). (update1 (n+1) x t, l)"
    and len = "\(t,l). l"
    and array = "\xs. (adds xs 0 Leaf, length xs)"
    and invar = "\(t,l). braun t \ l = size t"
    and list = "\(t,l). list t"
proof (standard, goal_cases)
  case 1 thus ?case by (simp add: nth_list_lookup1 split: prod.splits)
next
  case 2 thus ?case by (simp add: list_update1 split: prod.splits)
next
  case 3 thus ?case by (simp add: size_list split: prod.splits)
next
  case 4 thus ?case by (simp add: list_adds)
next
  case 5 thus ?case by (simp add: braun_update1 size_update1 split: prod.splits)
next
  case 6 thus ?case by (simp add: size_braun_adds split: prod.splits)
qed

subsection "Flexible Array"

fun add_lo where
  "add_lo x Leaf = Node Leaf x Leaf" |
  "add_lo x (Node l a r) = Node (add_lo a r) x l"

fun merge where
  "merge Leaf r = r" |
  "merge (Node l a r) rr = Node rr a (merge l r)"

fun del_lo where
  "del_lo Leaf = Leaf" |
  "del_lo (Node l a r) = merge l r"

fun del_hi :: "nat \ 'a tree \ 'a tree" where
  "del_hi n Leaf = Leaf" |
  "del_hi n (Node l x r) =
  (if n = 1 then Leaf
   else if even n
       then Node (del_hi (n div 2) l) x r
       else Node l x (del_hi (n div 2) r))"

subsubsection "Functional Correctness"

paragraph \<open>\<^const>\<open>add_lo\<close>\<close>

lemma list_add_lo: "braun t \ list (add_lo a t) = a # list t"
  by(induction t arbitrary: a) auto

lemma braun_add_lo: "braun t \ braun(add_lo x t)"
  by(induction t arbitrary: x) (auto simp add: list_add_lo simp flip: size_list)

paragraph \<open>\<^const>\<open>del_lo\<close>\<close>

lemma list_merge: "braun (Node l x r) \ list(merge l r) = splice (list l) (list r)"
  by (induction l r rule: merge.induct) auto

lemma braun_merge: "braun (Node l x r) \ braun(merge l r)"
  by (induction l r rule: merge.induct)(auto simp add: list_merge simp flip: size_list)

lemma list_del_lo: "braun t \ list(del_lo t) = tl (list t)"
  by (cases t) (simp_all add: list_merge)

lemma braun_del_lo: "braun t \ braun(del_lo t)"
  by (cases t) (simp_all add: braun_merge)

paragraph \<open>\<^const>\<open>del_hi\<close>\<close>

lemma list_Nil_iff: "list t = [] \ t = Leaf"
  by(cases t) simp_all

lemma butlast_splice: "butlast (splice xs ys) =
  (if size xs > size ys then splice (butlast xs) ys else splice xs (butlast ys))"
  by(induction xs ys rule: splice.induct) (auto)

lemma list_del_hi: "braun t \ size t = st \ list(del_hi st t) = butlast(list t)"
  by (induction t arbitrary: st) (auto simp: list_Nil_iff size_list butlast_splice)

lemma braun_del_hi: "braun t \ size t = st \ braun(del_hi st t)"
  by (induction t arbitrary: st) (auto simp: list_del_hi simp flip: size_list)

subsubsection "Flexible Array Implementation"

interpretation AF: Array_Flex
  where lookup = "\(t,l) n. lookup1 t (n+1)"
    and update = "\n x (t,l). (update1 (n+1) x t, l)"
    and len = "\(t,l). l"
    and array = "\xs. (adds xs 0 Leaf, length xs)"
    and invar = "\(t,l). braun t \ l = size t"
    and list = "\(t,l). list t"
    and add_lo = "\x (t,l). (add_lo x t, l+1)"
    and del_lo = "\(t,l). (del_lo t, l-1)"
    and add_hi = "\x (t,l). (update1 (Suc l) x t, l+1)"
    and del_hi = "\(t,l). (del_hi l t, l-1)"
proof (standard, goal_cases)
  case 1 thus ?case by (simp add: list_add_lo split: prod.splits)
next
  case 2 thus ?case by (simp add: list_del_lo split: prod.splits)
next
  case 3 thus ?case by (simp add: list_add_hi braun_add_hi split: prod.splits)
next
  case 4 thus ?case by (simp add: list_del_hi split: prod.splits)
next
  case 5 thus ?case by (simp add: braun_add_lo list_add_lo flip: size_list split: prod.splits)
next
  case 6 thus ?case by (simp add: braun_del_lo list_del_lo flip: size_list split: prod.splits)
next
  case 7 thus ?case by (simp add: size_add_hi braun_add_hi split: prod.splits)
next
  case 8 thus ?case by (simp add: braun_del_hi list_del_hi flip: size_list split: prod.splits)
qed

subsection "Faster"

subsubsection \<open>Size\<close>

fun diff :: "'a tree \ nat \ nat" where
  "diff Leaf _ = 0" |
  "diff (Node l x r) n = (if n=0 then 1 else if even n then diff r (n div 2 - 1) else diff l (n div 2))"

fun size_fast :: "'a tree \ nat" where
  "size_fast Leaf = 0" |
  "size_fast (Node l x r) = (let n = size_fast r in 1 + 2*n + diff l n)"

declare Let_def[simp]

lemma diff: "braun t \ size t : {n, n + 1} \ diff t n = size t - n"
  by (induction t arbitrary: n) auto

lemma size_fast: "braun t \ size_fast t = size t"
  by (induction t) (auto simp add: diff)

subsubsection \<open>Initialization with 1 element\<close>

fun braun_of_naive :: "'a \ nat \ 'a tree" where
  "braun_of_naive x n = (if n=0 then Leaf
  else let m = (n-1) div 2
       in if odd n then Node (braun_of_naive x m) x (braun_of_naive x m)
       else Node (braun_of_naive x (m + 1)) x (braun_of_naive x m))"

fun braun2_of :: "'a \ nat \ 'a tree * 'a tree" where
  "braun2_of x n = (if n = 0 then (Leaf, Node Leaf x Leaf)
  else let (s,t) = braun2_of x ((n-1) div 2)
       in if odd n then (Node s x s, Node t x s) else (Node t x s, Node t x t))"

definition braun_of :: "'a \ nat \ 'a tree" where
  "braun_of x n = fst (braun2_of x n)"

declare braun2_of.simps [simp del]

lemma braun2_of_size_braun: "braun2_of x n = (s,t) \ size s = n \ size t = n+1 \ braun s \ braun t"
proof(induction x n arbitrary: s t rule: braun2_of.induct)
  case (1 x n)
  then show ?case
    by (auto simp: braun2_of.simps[of x n] split: prod.splits if_splits) presburger+
qed

lemma braun2_of_replicate:
  "braun2_of x n = (s,t) \ list s = replicate n x \ list t = replicate (n+1) x"
proof(induction x n arbitrary: s t rule: braun2_of.induct)
  case (1 x n)
  have "x # replicate m x = replicate (m+1) x" for m by simp
  with 1 show ?case
    apply (auto simp: braun2_of.simps[of x n] replicate.simps(2)[of 0 x]
        simp del: replicate.simps(2) split: prod.splits if_splits)
    by presburger+
qed

corollary braun_braun_of: "braun(braun_of x n)"
  unfolding braun_of_def by (metis eq_fst_iff braun2_of_size_braun)

corollary list_braun_of: "list(braun_of x n) = replicate n x"
  unfolding braun_of_def by (metis eq_fst_iff braun2_of_replicate)

subsubsection "Proof Infrastructure"

text \<open>Originally due to Thomas Sewell.\<close>

paragraph \<open>\<open>take_nths\<close>\<close>

fun take_nths :: "nat \ nat \ 'a list \ 'a list" where
  "take_nths i k [] = []" |
  "take_nths i k (x # xs) = (if i = 0 then x # take_nths (2^k - 1) k xs
  else take_nths (i - 1) k xs)"

text \<open>This is the more concise definition but seems to complicate the proofs:\<close>

lemma take_nths_eq_nths: "take_nths i k xs = nths xs (\n. {n*2^k + i})"
proof(induction xs arbitrary: i)
  case Nil
  then show ?case by simp
next
  case (Cons x xs)
  show ?case
  proof cases
    assume [simp]: "i = 0"
    have "\x n. Suc x = n * 2 ^ k \ \xa. x = Suc xa * 2 ^ k - Suc 0"
      by (metis diff_Suc_Suc diff_zero mult_eq_0_iff not0_implies_Suc)
    then have "(\n. {(n+1) * 2 ^ k - 1}) = {m. \n. Suc m = n * 2 ^ k}"
      by (auto simp del: mult_Suc)
    thus ?thesis by (simp add: Cons.IH ac_simps nths_Cons)
  next
    assume [arith]: "i \ 0"
    have "\x n. Suc x = n * 2 ^ k + i \ \xa. x = xa * 2 ^ k + i - Suc 0"
      by (metis diff_Suc_Suc diff_zero)
    then have "(\n. {n * 2 ^ k + i - 1}) = {m. \n. Suc m = n * 2 ^ k + i}"
      by auto
    thus ?thesis by (simp add: Cons.IH nths_Cons)
  qed
qed

lemma take_nths_drop:
  "take_nths i k (drop j xs) = take_nths (i + j) k xs"
  by (induct xs arbitrary: i j; simp add: drop_Cons split: nat.split)

lemma take_nths_00:
  "take_nths 0 0 xs = xs"
  by (induct xs; simp)

lemma splice_take_nths:
  "splice (take_nths 0 (Suc 0) xs) (take_nths (Suc 0) (Suc 0) xs) = xs"
  by (induct xs; simp)

lemma take_nths_take_nths:
  "take_nths i m (take_nths j n xs) = take_nths ((i * 2^n) + j) (m + n) xs"
  by (induct xs arbitrary: i j; simp add: algebra_simps power_add)

lemma take_nths_empty:
  "(take_nths i k xs = []) = (length xs \ i)"
  by (induction xs arbitrary: i k) auto

lemma hd_take_nths:
  "i < length xs \ hd(take_nths i k xs) = xs ! i"
  by (induction xs arbitrary: i k) auto

lemma take_nths_01_splice:
  "\ length xs = length ys \ length xs = length ys + 1 \ \
   take_nths 0 (Suc 0) (splice xs ys) = xs \<and>
   take_nths (Suc 0) (Suc 0) (splice xs ys) = ys"
  by (induct xs arbitrary: ys; case_tac ys; simp)

lemma length_take_nths_00:
  "length (take_nths 0 (Suc 0) xs) = length (take_nths (Suc 0) (Suc 0) xs) \
   length (take_nths 0 (Suc 0) xs) = length (take_nths (Suc 0) (Suc 0) xs) + 1"
  by (induct xs) auto

paragraph \<open>\<open>braun_list\<close>\<close>

fun braun_list :: "'a tree \ 'a list \ bool" where
  "braun_list Leaf xs = (xs = [])" |
  "braun_list (Node l x r) xs = (xs \ [] \ x = hd xs \
    braun_list l (take_nths 1 1 xs) \<and>
    braun_list r (take_nths 2 1 xs))"

lemma braun_list_eq:
  "braun_list t xs = (braun t \ xs = list t)"
proof (induct t arbitrary: xs)
  case Leaf
  show ?case by simp
next
  case Node
  show ?case
    using length_take_nths_00[of xs] splice_take_nths[of xs]
    by (auto simp: neq_Nil_conv Node.hyps size_list[symmetric] take_nths_01_splice)
qed

subsubsection \<open>Converting a list of elements into a Braun tree\<close>

fun nodes :: "'a tree list \ 'a list \ 'a tree list \ 'a tree list" where
  "nodes (l#ls) (x#xs) (r#rs) = Node l x r # nodes ls xs rs" |
  "nodes (l#ls) (x#xs) [] = Node l x Leaf # nodes ls xs []" |
  "nodes [] (x#xs) (r#rs) = Node Leaf x r # nodes [] xs rs" |
  "nodes [] (x#xs) [] = Node Leaf x Leaf # nodes [] xs []" |
  "nodes ls [] rs = []"

fun brauns :: "nat \ 'a list \ 'a tree list" where
  "brauns k xs = (if xs = [] then [] else
   let ys = take (2^k) xs;
       zs = drop (2^k) xs;
       ts = brauns (k+1) zs
   in nodes ts ys (drop (2^k) ts))"

declare brauns.simps[simp del]

definition brauns1 :: "'a list \ 'a tree" where
  "brauns1 xs = (if xs = [] then Leaf else brauns 0 xs ! 0)"

paragraph "Functional correctness"

text \<open>The proof is originally due to Thomas Sewell.\<close>

lemma length_nodes:
  "length (nodes ls xs rs) = length xs"
  by (induct ls xs rs rule: nodes.induct; simp)

lemma nth_nodes:
  "i < length xs \ nodes ls xs rs ! i =
  Node (if i < length ls then ls ! i else Leaf) (xs ! i)
    (if i < length rs then rs ! i else Leaf)"
  by (induct ls xs rs arbitrary: i rule: nodes.induct;
      simp add: nth_Cons split: nat.split)

theorem length_brauns:
  "length (brauns k xs) = min (length xs) (2 ^ k)"
proof (induct xs arbitrary: k rule: measure_induct_rule[where f=length])
  case (less xs) thus ?case by (simp add: brauns.simps[of k xs] length_nodes)
qed

theorem brauns_correct:
  "i < min (length xs) (2 ^ k) \ braun_list (brauns k xs ! i) (take_nths i k xs)"
proof (induct xs arbitrary: i k rule: measure_induct_rule[where f=length])
  case (less xs)
  have "xs \ []" using less.prems by auto
  let ?zs = "drop (2^k) xs"
  let ?ts = "brauns (Suc k) ?zs"
  from less.hyps[of ?zs _ "Suc k"]
  have IH: "\ j = i + 2 ^ k; i < min (length ?zs) (2 ^ (k+1)) \ \
    braun_list (?ts ! i) (take_nths j (Suc k) xs)" for i j
    using \<open>xs \<noteq> []\<close> by (simp add: take_nths_drop)
  show ?case
    using less.prems
    by (auto simp: brauns.simps[of k xs] nth_nodes take_nths_take_nths
        IH take_nths_empty hd_take_nths length_brauns)
qed

corollary brauns1_correct:
  "braun (brauns1 xs) \ list (brauns1 xs) = xs"
  using brauns_correct[of 0 xs 0]
  by (simp add: brauns1_def braun_list_eq take_nths_00)

paragraph "Running Time Analysis"

time_fun_0 "(^)"

time_fun nodes

lemma T_nodes: "T_nodes ls xs rs = length xs + 1"
by(induction ls xs rs rule: T_nodes.induct) auto

time_fun brauns

lemma T_brauns_simple: "T_brauns k xs = (if xs = [] then 0 else
   3 * (min (2^k) (length xs) + 1) + (min (2^k) (length xs - 2^k) + 1) + T_brauns (k+1) (drop (2^k) xs)) + 1"
by(simp add: T_nodes T_take T_drop length_brauns min_def)

theorem T_brauns_ub:
  "T_brauns k xs \ 9 * (length xs + 1)"
proof (induction xs arbitrary: k rule: measure_induct_rule[where f = length])
  case (less xs)
  show ?case
  proof cases
    assume "xs = []"
    thus ?thesis by(simp)
  next
    assume "xs \ []"
    let ?n = "length xs" let ?zs = "drop (2^k) xs"
    have *: "?n - 2^k + 1 \ ?n"
      using \<open>xs \<noteq> []\<close> less_eq_Suc_le by fastforce
    have "T_brauns k xs =
      3 * (min (2^k) ?n + 1) + (min (2^k) (?n - 2^k) + 1) + T_brauns (k+1) ?zs + 1"
      unfolding T_brauns_simple[of k xs] using \<open>xs \<noteq> []\<close> by(simp del: T_brauns.simps)
    also have "\ \ 4 * min (2^k) ?n + T_brauns (k+1) ?zs + 5"
      by(simp add: min_def)
    also have "\ \ 4 * min (2^k) ?n + 9 * (length ?zs + 1) + 5"
      using less[of ?zs "k+1"] \<open>xs \<noteq> []\<close>
      by (simp del: T_brauns.simps)
    also have "\ = 4 * min (2^k) ?n + 9 * (?n - 2^k + 1) + 5"
      by(simp)
    also have "\ = 4 * min (2^k) ?n + 4 * (?n - 2^k) + 5 * (?n - 2^k + 1) + 9"
      by(simp)
    also have "\ = 4 * ?n + 5 * (?n - 2^k + 1) + 9"
      by(simp)
    also have "\ \ 4 * ?n + 5 * ?n + 9"
      using * by(simp)
    also have "\ = 9 * (?n + 1)"
      by (simp add: Suc_leI)
    finally show ?thesis .
  qed
qed

subsubsection \<open>Converting a Braun Tree into a List of Elements\<close>

text \<open>The code and the proof are originally due to Thomas Sewell (except running time).\<close>

function list_fast_rec :: "'a tree list \ 'a list" where
  "list_fast_rec ts = (let us = filter (\t. t \ Leaf) ts in
  if us = [] then [] else
  map value us @ list_fast_rec (map left us @ map right us))"
  by (pat_completeness, auto)

lemma list_fast_rec_term1: "ts \ [] \ Leaf \ set ts \
  sum_list (map (size o left) ts) + sum_list (map (size o right) ts) < sum_list (map size ts)"
  apply (clarsimp simp: sum_list_addf[symmetric] sum_list_map_filter')
  apply (rule sum_list_strict_mono; clarsimp?)
  apply (case_tac x; simp)
  done

lemma list_fast_rec_term: "us \ [] \ us = filter (\t. t \ \\) ts \
  sum_list (map (size o left) us) + sum_list (map (size o right) us) < sum_list (map size ts)"
  apply (rule order_less_le_trans, rule list_fast_rec_term1, simp_all)
  apply (rule sum_list_filter_le_nat)
  done

termination
  by (relation "measure (sum_list o map size)"; simp add: list_fast_rec_term)

declare list_fast_rec.simps[simp del]

definition list_fast :: "'a tree \ 'a list" where
  "list_fast t = list_fast_rec [t]"

(* TODO: map and filter are a problem!
- The automatically generated T_map is slightly more complicated than needed.
- We cannot use the manually defined T_map directly because the automatic translation
  assumes that T_map has a more complicated type and generates a "wrong" call.
Therefore we hide map/filter at the moment.
*)

definition "filter_not_Leaf = filter (\t. t \ Leaf)"

definition "map_left = map left"
definition "map_right = map right"
definition "map_value = map value"

definition "T_filter_not_Leaf ts = length ts + 1"
definition "T_map_left ts = length ts + 1"
definition "T_map_right ts = length ts + 1"
definition "T_map_value ts = length ts + 1"
(*
time_fun "tree.value"
time_fun "left"
time_fun "right"
*)

lemmas defs = filter_not_Leaf_def map_left_def map_right_def map_value_def
  T_filter_not_Leaf_def T_map_value_def T_map_left_def T_map_right_def

(* A variant w/o explicit map/filter; T_list_fast_rec is generated from it *)
lemma list_fast_rec_simp:
"list_fast_rec ts = (let us = filter_not_Leaf ts in
  if us = [] then [] else
  map_value us @ list_fast_rec (map_left us @ map_right us))"
unfolding defs list_fast_rec.simps[of ts] by(rule refl)

time_function list_fast_rec equations list_fast_rec_simp
termination
  by (relation "measure (sum_list o map size)"; simp add: list_fast_rec_term defs)

declare T_list_fast_rec.simps[simp del]

paragraph "Functional Correctness"

lemma list_fast_rec_all_Leaf:
  "\t \ set ts. t = Leaf \ list_fast_rec ts = []"
  by (simp add: filter_empty_conv list_fast_rec.simps)

lemma take_nths_eq_single:
  "length xs - i < 2^n \ take_nths i n xs = take 1 (drop i xs)"
  by (induction xs arbitrary: i n; simp add: drop_Cons')

lemma braun_list_Nil:
  "braun_list t [] = (t = Leaf)"
  by (cases t; simp)

lemma braun_list_not_Nil: "xs \ [] \
  braun_list t xs =
     (\<exists>l x r. t = Node l x r \<and> x = hd xs \<and>
        braun_list l (take_nths 1 1 xs) \<and>
        braun_list r (take_nths 2 1 xs))"
  by(cases t; simp)

theorem list_fast_rec_correct:
  "\ length ts = 2 ^ k; \i < 2 ^ k. braun_list (ts ! i) (take_nths i k xs) \
    \<Longrightarrow> list_fast_rec ts = xs"
proof (induct xs arbitrary: k ts rule: measure_induct_rule[where f=length])
  case (less xs)
  show ?case
  proof (cases "length xs < 2 ^ k")
    case True
    from less.prems True have filter:
      "\n. ts = map (\x. Node Leaf x Leaf) xs @ replicate n Leaf"
      apply (rule_tac x="length ts - length xs" in exI)
      apply (clarsimp simp: list_eq_iff_nth_eq)
      apply(auto simp: nth_append braun_list_not_Nil take_nths_eq_single braun_list_Nil hd_drop_conv_nth)
      done
    thus ?thesis
      by (clarsimp simp: list_fast_rec.simps[of ts] o_def list_fast_rec_all_Leaf)
  next
    case False
    with less.prems(2) have *:
      "\i < 2 ^ k. ts ! i \ Leaf
         \<and> value (ts ! i) = xs ! i
         \<and> braun_list (left (ts ! i)) (take_nths (i + 2 ^ k) (Suc k) xs)
         \<and> (\<forall>ys. ys = take_nths (i + 2 * 2 ^ k) (Suc k) xs
                 \<longrightarrow> braun_list (right (ts ! i)) ys)"
      by (auto simp: take_nths_empty hd_take_nths braun_list_not_Nil take_nths_take_nths
          algebra_simps)
    have 1: "map value ts = take (2 ^ k) xs"
      using less.prems(1) False by (simp add: list_eq_iff_nth_eq *)
    have 2: "list_fast_rec (map left ts @ map right ts) = drop (2 ^ k) xs"
      using less.prems(1) False
      by (auto intro!: Nat.diff_less less.hyps[where k= "Suc k"]
          simp: nth_append * take_nths_drop algebra_simps)
    from less.prems(1) False show ?thesis
      by (auto simp: list_fast_rec.simps[of ts] 1 2 * all_set_conv_all_nth)
  qed
qed

corollary list_fast_correct:
  "braun t \ list_fast t = list t"
  by (simp add: list_fast_def take_nths_00 braun_list_eq list_fast_rec_correct[where k=0])

paragraph "Running Time Analysis"

lemma sum_tree_list_children: "\t \ set ts. t \ Leaf \
  (\<Sum>t\<leftarrow>ts. k * size t) = (\<Sum>t \<leftarrow> map left ts @ map right ts. k * size t) + k * length ts"
  by(induction ts)(auto simp add: neq_Leaf_iff algebra_simps)

theorem T_list_fast_rec_ub:
  "T_list_fast_rec ts \ sum_list (map (\t. 14*size t + 1) ts) + 2"
proof (induction ts rule: measure_induct_rule[where f="sum_list o map size"])
  case (less ts)
  let ?us = "filter (\t. t \ Leaf) ts"
  show ?case
  proof cases
    assume "?us = []"
    thus ?thesis using T_list_fast_rec.simps[of ts]
      by(simp add: defs sum_list_Suc)
  next
    assume "?us \ []"
    let ?children = "map left ?us @ map right ?us"
    have 1: "1 \ length ?us"
      using \<open>?us \<noteq> []\<close> linorder_not_less by auto
    have "T_list_fast_rec ts = T_list_fast_rec ?children + 5 * length ?us + length ts + 7"
      using \<open>?us \<noteq> []\<close> T_list_fast_rec.simps[of ts] by(simp add: defs T_append)
    also have "\ \ (\t\?children. 14 * size t + 1) + 5 * length ?us + length ts + 9"
      using less[of "?children"] list_fast_rec_term[of "?us"] \<open>?us \<noteq> []\<close>
      by (simp)
    also have "\ = (\t\?children. 14 * size t) + 7 * length ?us + length ts + 9"
      by(simp add: sum_list_Suc o_def)
    also have "\ \ (\t\?children. 14 * size t) + 14 * length ?us + length ts + 2"
      using 1 by(simp add: sum_list_Suc o_def)
    also have "\ = (\t\?us. 14 * size t) + length ts + 2"
      by(simp add: sum_tree_list_children)
    also have "\ \ (\t\ts. 14 * size t) + length ts + 2"
      by(simp add: sum_list_filter_le_nat)
    also have "\ = (\t\ts. 14 * size t + 1) + 2"
      by(simp add: sum_list_Suc)
    finally show ?case .
  qed
qed

end

quality100%

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.