Final Version
This commit is contained in:
teddy
parent
846bbe2428
commit
a3fa988ff1
67
VerifyThis2024/Fibonacci.thy
Normal file
67
VerifyThis2024/Fibonacci.thy
Normal file
@ -0,0 +1,67 @@
|
||||
theory Fibonacci
|
||||
imports Main HOL.NthRoot
|
||||
begin
|
||||
|
||||
fun fib :: \<open>nat \<Rightarrow> nat\<close> where
|
||||
\<open>fib 0 = 0\<close>|
|
||||
\<open>fib (Suc 0) = Suc 0\<close>|
|
||||
\<open>fib (Suc (Suc n)) = fib (Suc n) + fib n\<close>
|
||||
|
||||
definition \<open>\<phi> = (1 + sqrt 5)/2\<close>
|
||||
definition \<open>\<psi> = (1 - sqrt 5)/2\<close>
|
||||
|
||||
definition fib_intvl :: \<open>nat \<Rightarrow> nat set\<close> where
|
||||
\<open>fib_intvl n = {fib n..<fib (Suc n)}\<close>
|
||||
|
||||
definition fib_intvl_seq :: \<open>nat \<Rightarrow> (nat set) list\<close> where
|
||||
\<open>fib_intvl_seq n = map (fib_intvl o nat) [2..int n]\<close>
|
||||
|
||||
lemma \<phi>_pow_2: \<open>\<phi>^2 = (1 + \<phi>)\<close> unfolding \<phi>_def
|
||||
proof-
|
||||
have *: \<open>(1+sqrt 5)\<^sup>2 = (1 + 2*sqrt 5 + 5)\<close> using power2_sum[of \<open>1\<close> \<open>sqrt 5\<close>] by auto
|
||||
have \<open>((1 + sqrt 5) / 2)\<^sup>2 = (1+sqrt 5)\<^sup>2 / 4\<close>
|
||||
by (simp add: power_divide)
|
||||
hence \<open>... = (1 + 2*sqrt 5 + 5) / 4\<close> using * by auto
|
||||
hence \<open>... = 2*(1 + sqrt 5)/4 + 1\<close> by simp
|
||||
thus \<open>((1 + sqrt 5) / 2)\<^sup>2= 1 + (1 + sqrt 5) / 2\<close>
|
||||
by (smt (z3) "*" field_sum_of_halves four_x_squared)
|
||||
qed
|
||||
|
||||
lemma \<psi>_pow_2: \<open>\<psi>^2 = (1 + \<psi>)\<close>
|
||||
proof-
|
||||
have *: \<open>(1-sqrt 5)\<^sup>2 = (1 - 2*sqrt 5 + 5)\<close> using power2_diff[of \<open>1\<close> \<open>sqrt 5\<close>] by auto
|
||||
hence \<open>(1-sqrt 5)\<^sup>2/4 = (1 - 2*sqrt 5 + 5)/4\<close> by auto
|
||||
hence \<open>... = 2*(1 - sqrt 5)/4 + 1\<close> by simp
|
||||
thus ?thesis
|
||||
by (smt (z3) "*" \<psi>_def field_sum_of_halves four_x_squared)
|
||||
qed
|
||||
|
||||
lemmas golden_ratios = \<phi>_def \<psi>_def
|
||||
|
||||
lemma golden_diff: \<open>(\<phi> - \<psi>) = sqrt 5\<close> unfolding golden_ratios
|
||||
by (smt (z3) field_sum_of_halves)
|
||||
|
||||
lemma fib_correct: \<open>fib n = (\<phi>^n - \<psi>^n) / sqrt 5\<close>
|
||||
proof(induction n rule: fib.induct)
|
||||
case 1
|
||||
then show ?case by simp
|
||||
next
|
||||
case 2
|
||||
then show ?case
|
||||
by (simp add: golden_diff)
|
||||
next
|
||||
case (3 n)
|
||||
then show ?case
|
||||
proof-
|
||||
have \<open>real (fib (Suc (Suc n))) = real (fib (Suc n)) + real (fib n)\<close> by auto
|
||||
moreover have \<open>... = (\<phi> ^ Suc n - \<psi> ^ Suc n) / sqrt 5 + (\<phi> ^ n - \<psi> ^ n) / sqrt 5\<close> using 3 by auto
|
||||
moreover have \<open>... = (\<phi> ^ Suc n + \<phi>^n - \<psi> ^ Suc n - \<psi> ^ n)/sqrt 5\<close>
|
||||
by (smt (verit, best) add_divide_distrib)
|
||||
moreover have \<open>... = (\<phi> ^ n * (\<phi> + 1) - \<psi> ^ n * (\<psi> + 1))/ sqrt 5\<close>
|
||||
by (simp add: distrib_right mult.commute)
|
||||
ultimately show ?case using \<psi>_pow_2 \<phi>_pow_2
|
||||
by (metis add.commute add_2_eq_Suc power_add)
|
||||
qed
|
||||
qed
|
||||
|
||||
end
|
||||
64
VerifyThis2024/Fibonacci.thy~
Normal file
64
VerifyThis2024/Fibonacci.thy~
Normal file
@ -0,0 +1,64 @@
|
||||
theory Fibonacci
|
||||
imports Main HOL.NthRoot
|
||||
begin
|
||||
|
||||
fun fib :: \<open>nat \<Rightarrow> nat\<close> where
|
||||
\<open>fib 0 = 0\<close>|
|
||||
\<open>fib (Suc 0) = Suc 0\<close>|
|
||||
\<open>fib (Suc (Suc n)) = fib (Suc n) + fib n\<close>
|
||||
|
||||
definition \<open>\<phi> = (1 + sqrt 5)/2\<close>
|
||||
definition \<open>\<psi> = (1 - sqrt 5)/2\<close>
|
||||
|
||||
definition fib_intvl :: \<open>nat \<Rightarrow> nat set\<close> where
|
||||
\<open>fib_intvl n = {fib n..<fib (Suc n)}\<close>
|
||||
|
||||
lemma \<phi>_pow_2: \<open>\<phi>^2 = (1 + \<phi>)\<close> unfolding \<phi>_def
|
||||
proof-
|
||||
have *: \<open>(1+sqrt 5)\<^sup>2 = (1 + 2*sqrt 5 + 5)\<close> using power2_sum[of \<open>1\<close> \<open>sqrt 5\<close>] by auto
|
||||
have \<open>((1 + sqrt 5) / 2)\<^sup>2 = (1+sqrt 5)\<^sup>2 / 4\<close>
|
||||
by (simp add: power_divide)
|
||||
hence \<open>... = (1 + 2*sqrt 5 + 5) / 4\<close> using * by auto
|
||||
hence \<open>... = 2*(1 + sqrt 5)/4 + 1\<close> by simp
|
||||
thus \<open>((1 + sqrt 5) / 2)\<^sup>2= 1 + (1 + sqrt 5) / 2\<close>
|
||||
by (smt (z3) "*" field_sum_of_halves four_x_squared)
|
||||
qed
|
||||
|
||||
lemma \<psi>_pow_2: \<open>\<psi>^2 = (1 + \<psi>)\<close>
|
||||
proof-
|
||||
have *: \<open>(1-sqrt 5)\<^sup>2 = (1 - 2*sqrt 5 + 5)\<close> using power2_diff[of \<open>1\<close> \<open>sqrt 5\<close>] by auto
|
||||
hence \<open>(1-sqrt 5)\<^sup>2/4 = (1 - 2*sqrt 5 + 5)/4\<close> by auto
|
||||
hence \<open>... = 2*(1 - sqrt 5)/4 + 1\<close> by simp
|
||||
thus ?thesis
|
||||
by (smt (z3) "*" \<psi>_def field_sum_of_halves four_x_squared)
|
||||
qed
|
||||
|
||||
lemmas golden_ratios = \<phi>_def \<psi>_def
|
||||
|
||||
lemma golden_diff: \<open>(\<phi> - \<psi>) = sqrt 5\<close> unfolding golden_ratios
|
||||
by (smt (z3) field_sum_of_halves)
|
||||
|
||||
lemma fib_correct: \<open>fib n = (\<phi>^n - \<psi>^n) / sqrt 5\<close>
|
||||
proof(induction n rule: fib.induct)
|
||||
case 1
|
||||
then show ?case by simp
|
||||
next
|
||||
case 2
|
||||
then show ?case
|
||||
by (simp add: golden_diff)
|
||||
next
|
||||
case (3 n)
|
||||
then show ?case
|
||||
proof-
|
||||
have \<open>real (fib (Suc (Suc n))) = real (fib (Suc n)) + real (fib n)\<close> by auto
|
||||
moreover have \<open>... = (\<phi> ^ Suc n - \<psi> ^ Suc n) / sqrt 5 + (\<phi> ^ n - \<psi> ^ n) / sqrt 5\<close> using 3 by auto
|
||||
moreover have \<open>... = (\<phi> ^ Suc n + \<phi>^n - \<psi> ^ Suc n - \<psi> ^ n)/sqrt 5\<close>
|
||||
by (smt (verit, best) add_divide_distrib)
|
||||
moreover have \<open>... = (\<phi> ^ n * (\<phi> + 1) - \<psi> ^ n * (\<psi> + 1))/ sqrt 5\<close>
|
||||
by (simp add: distrib_right mult.commute)
|
||||
ultimately show ?case using \<psi>_pow_2 \<phi>_pow_2
|
||||
by (metis add.commute add_2_eq_Suc power_add)
|
||||
qed
|
||||
qed
|
||||
|
||||
end
|
||||
@ -10,8 +10,6 @@ text\<open>The task is to implement a "Rope" ( \<^url>\<open>https://en.wikipedi
|
||||
originally published by Boehm - \<^url>\<open>https://www.cs.tufts.edu/comp/150FP/archive/hans-boehm/ropes.pdf\<close>
|
||||
- a special type of binary tree to represent a string (in honor of Billy who can't be here today).\<close>
|
||||
|
||||
definition \<open>hello_world_rope \<equiv> Node (Leaf (STR ''Hello '') 6) 6 (Leaf (STR ''World'') 5)\<close>
|
||||
|
||||
text\<open>A Rope stores a string as a tree of where leaves contain a specific sub string and a weight that is equal to the number of characters in the sub string (see example from wiki page).
|
||||
The corresponding parent node stores the sum of left children leaf weights (see example from wiki page).\<close>
|
||||
|
||||
@ -19,7 +17,6 @@ subsection\<open>Tasks\<close>
|
||||
|
||||
text\<open>Implement a function @{term \<open>valid_rope (r :: Rope) :: bool\<close>} which checks that a rope is well constructed\<close>
|
||||
|
||||
|
||||
lemma mk_leaf_valid: \<open>valid_rope (mk_leaf s)\<close> by simp
|
||||
|
||||
value \<open>to_str (Node (Leaf (STR ''Hello '') 6) 6 (Leaf (STR ''World'') 5))\<close>
|
||||
@ -231,4 +228,14 @@ value \<open>safe_rope_delete (Node (Leaf STR ''a'' 1) 1 (Leaf STR ''a'' 1)) 1 1
|
||||
lemma \<open>rope_insert (rope_delete r i len) i (to_str (rope_sub_str r i len)) = r\<close> oops
|
||||
text\<open>These methods are correct as is, but do not perform the most optimally. Optimize these operations by implementing
|
||||
a function @{term \<open>rebalance\<close>} that rebalances the the Rope.\<close>
|
||||
|
||||
value \<open>fib_intvl_seq 5\<close>
|
||||
|
||||
definition sequence_index_from_weight :: \<open>nat \<Rightarrow> (nat set) list \<Rightarrow> nat\<close> where
|
||||
\<open>sequence_index_from_weight _ [] = 0\<close>|
|
||||
\<open>sequence_index_from_weight 0 (x # xs) = \<close>
|
||||
|
||||
fun rebalance :: \<open>Rope \<Rightarrow> Rope\<close> where
|
||||
\<open>rebalance (Leaf s w) = Leaf s w\<close>|
|
||||
\<open>rebalance (Node l w r) = \<close>
|
||||
end
|
||||
235
VerifyThis2024/Ropes.thy~
Normal file
235
VerifyThis2024/Ropes.thy~
Normal file
@ -0,0 +1,235 @@
|
||||
theory Ropes
|
||||
imports Utils
|
||||
begin
|
||||
|
||||
section\<open>Challenge 0 from VerifyThis 2024: \<^url>\<open>https://www.pm.inf.ethz.ch/research/verifythis.html\<close>\<close>
|
||||
|
||||
subsection\<open>The Rope Data Structure\<close>
|
||||
|
||||
text\<open>The task is to implement a "Rope" ( \<^url>\<open>https://en.wikipedia.org/wiki/Rope_(data_structure)\<close> )
|
||||
originally published by Boehm - \<^url>\<open>https://www.cs.tufts.edu/comp/150FP/archive/hans-boehm/ropes.pdf\<close>
|
||||
- a special type of binary tree to represent a string (in honor of Billy who can't be here today).\<close>
|
||||
|
||||
text\<open>A Rope stores a string as a tree of where leaves contain a specific sub string and a weight that is equal to the number of characters in the sub string (see example from wiki page).
|
||||
The corresponding parent node stores the sum of left children leaf weights (see example from wiki page).\<close>
|
||||
|
||||
subsection\<open>Tasks\<close>
|
||||
|
||||
text\<open>Implement a function @{term \<open>valid_rope (r :: Rope) :: bool\<close>} which checks that a rope is well constructed\<close>
|
||||
|
||||
lemma mk_leaf_valid: \<open>valid_rope (mk_leaf s)\<close> by simp
|
||||
|
||||
value \<open>to_str (Node (Leaf (STR ''Hello '') 6) 6 (Leaf (STR ''World'') 5))\<close>
|
||||
|
||||
value \<open>valid_rope (Node (Leaf (STR ''Hello '') 6) 6 (Leaf (STR ''World'') 5))\<close>
|
||||
|
||||
text\<open>Implement a function @{term \<open>str_len (r :: Rope)\<close>} that can efficiently compute the length of the string. Further, prove its correctness\<close>
|
||||
|
||||
fun str_len :: \<open>Rope \<Rightarrow> nat\<close> where
|
||||
\<open>str_len (Leaf _ N) = N\<close>|
|
||||
\<open>str_len (Node l w r) = w + str_len r\<close>
|
||||
|
||||
value \<open>size (to_str hello_world_rope)\<close>
|
||||
|
||||
lemma sum_weights_eq_size:
|
||||
assumes \<open>valid_rope r\<close>
|
||||
shows \<open>sum_weights r = size (to_str r)\<close>
|
||||
using assms proof(induction r)
|
||||
case (Leaf s w)
|
||||
then show ?case by simp
|
||||
next
|
||||
case (Node l w r)
|
||||
have \<open>sum_weights (Node l w r) = sum_weights l + sum_weights r\<close> by simp
|
||||
moreover have \<open>... = size (to_str l) + size (to_str r)\<close> using Node by simp
|
||||
moreover have \<open>... = size (to_str l + to_str r)\<close> using literal_plus_size_eq by simp
|
||||
ultimately show ?case by simp
|
||||
qed
|
||||
|
||||
lemma str_len_eq_size:
|
||||
assumes \<open>valid_rope r\<close>
|
||||
shows \<open>str_len r = size (to_str r)\<close>
|
||||
using assms proof(induction r)
|
||||
case (Leaf s w)
|
||||
then show ?case by simp
|
||||
next
|
||||
case (Node l w r)
|
||||
hence left_valid: \<open>valid_rope l\<close> and right_valid: \<open>valid_rope r\<close> and w_def : \<open>w = sum_weights l\<close> by simp+
|
||||
hence \<open>str_len (Node l w r) = sum_weights l + str_len r\<close> by (simp add: Node)
|
||||
moreover have \<open>... = size (to_str l) + size (to_str r)\<close> by (simp add: sum_weights_eq_size left_valid right_valid Node)
|
||||
moreover have \<open>... = size (to_str l + to_str r)\<close> by (simp add: literal_plus_size_eq)
|
||||
ultimately show ?case by simp
|
||||
qed
|
||||
|
||||
lemma str_len_sum_weights_eq:
|
||||
assumes \<open>valid_rope r\<close>
|
||||
shows \<open>str_len r = sum_weights r\<close>
|
||||
using str_len_eq_size sum_weights_eq_size assms by auto
|
||||
|
||||
text\<open>Implement a function that computes the concatenation of two ropes @{term \<open>rope_concat (l::Rope) (r :: Rope)\<close>}\<close>
|
||||
|
||||
definition rope_concat :: \<open>Rope \<Rightarrow> Rope \<Rightarrow> Rope\<close> where
|
||||
\<open>rope_concat l r = Node l (str_len l) r\<close>
|
||||
|
||||
lemma valid_rope_concat:
|
||||
assumes \<open>valid_rope l\<close> \<open>valid_rope r\<close>
|
||||
shows \<open>valid_rope (rope_concat l r)\<close> by (simp add: assms str_len_sum_weights_eq rope_concat_def)
|
||||
|
||||
lemma rope_concat_eq: \<open>to_str (rope_concat l r) = to_str l + to_str r\<close> by (simp add: rope_concat_def)
|
||||
|
||||
text\<open>Implement a function @{term \<open>rope_delete (r :: Rope) (i :: nat) (len :: nat)\<close>} that returns a rope where the @{term \<open>len\<close>}
|
||||
characters starting from the position @{term \<open>i\<close>} have been removed.\<close>
|
||||
|
||||
|
||||
fun split :: \<open>Rope \<Rightarrow> nat \<Rightarrow> Rope \<times> Rope\<close> where
|
||||
\<open>split (Leaf s w) i = (mk_leaf (sub_str s {0..<i}), mk_leaf (sub_str s {i..size s}))\<close>|
|
||||
\<open>split (Node l w r) i = (if i < w then
|
||||
(let (left, right) = split l i
|
||||
in (left, rope_concat right r))
|
||||
else
|
||||
(if i > w then
|
||||
(let (left,right) = split r (i - w)
|
||||
in (rope_concat l left, right))
|
||||
else (l,r)))\<close>
|
||||
|
||||
value \<open>split (Node (Leaf (STR ''44'') 2) 2 (Leaf (STR ''44'') 2)) 0\<close>
|
||||
|
||||
value \<open>split (mk_leaf STR ''a'') 0\<close>
|
||||
|
||||
lemma valid_split:
|
||||
assumes \<open>valid_rope rope\<close>
|
||||
shows \<open>valid_rope (fst (split rope i)) \<and> valid_rope (snd (split rope i))\<close>
|
||||
using assms proof(induction \<open>rope\<close> arbitrary: i)
|
||||
case (Leaf x1 x2)
|
||||
then show ?case by simp
|
||||
next
|
||||
case (Node l' w r')
|
||||
hence l'_valid: \<open>valid_rope l'\<close> and r'_valid: \<open>valid_rope r'\<close> by auto
|
||||
hence l'_lsplit_valid: \<open>valid_rope (fst (split l' i))\<close> and l'_rsplit_valid: \<open>valid_rope (snd (split l' i))\<close>
|
||||
and r'_lsplit_valid: \<open>valid_rope (fst (split r' i))\<close> and r'_rsplit_valid: \<open>valid_rope (snd (split r' i))\<close>
|
||||
using Node by auto
|
||||
show ?case
|
||||
proof(cases \<open>i < w\<close>)
|
||||
case True
|
||||
then show ?thesis using l'_lsplit_valid l'_rsplit_valid
|
||||
by (simp add: r'_valid split_beta valid_rope_concat)
|
||||
next
|
||||
case False
|
||||
show ?thesis
|
||||
proof(cases \<open>i = w\<close>)
|
||||
case True
|
||||
then show ?thesis
|
||||
by (simp add: l'_valid r'_valid)
|
||||
next
|
||||
case False
|
||||
then show ?thesis
|
||||
by (simp add: Node.IH(2) l'_lsplit_valid l'_rsplit_valid l'_valid r'_valid split_beta valid_rope_concat)
|
||||
qed
|
||||
qed
|
||||
qed
|
||||
|
||||
fun short_rope :: \<open>Rope \<Rightarrow> bool\<close> where
|
||||
\<open>short_rope r = (str_len r \<le> 1)\<close>
|
||||
|
||||
fun is_empty :: \<open>Rope \<Rightarrow> bool\<close> where
|
||||
\<open>is_empty r = (str_len r = 0)\<close>
|
||||
|
||||
fun smart_rope_concat :: \<open>Rope \<Rightarrow> Rope \<Rightarrow> Rope\<close> where
|
||||
\<open>smart_rope_concat (Leaf l w_l) (Leaf r w_r) = (if w_r \<le> 1 then Leaf (l + r) (w_l + w_r) else (Node (Leaf l w_l) w_l (Leaf r w_r)))\<close>|
|
||||
\<open>smart_rope_concat (Node l w r) (Leaf r' w') = (if w' \<le> 1 then Node l w (smart_rope_concat r (Leaf r' w')) else (Node (Node l w r) w (Leaf r' w')))\<close>|
|
||||
\<open>smart_rope_concat (Leaf l w) (Node l' w' r) = (if w \<le> 1 then Node (smart_rope_concat (Leaf l w) l') (w + w') r else (Node (Leaf l w) w (Node l' w' r)))\<close>|
|
||||
\<open>smart_rope_concat (Node l w r) (Node l' w' r') = Node (Node l w r) w (Node l' w' r')\<close>
|
||||
|
||||
value \<open>smart_rope_concat (Node (mk_leaf STR ''?'') 1 (mk_leaf STR ''?'')) (mk_leaf STR '''')\<close>
|
||||
|
||||
lemma smart_rope_concat_eq:
|
||||
assumes \<open>valid_rope l\<close> \<open>valid_rope r\<close>
|
||||
shows \<open>to_str (smart_rope_concat l r) = to_str (rope_concat l r)\<close>
|
||||
using assms proof(induction l )
|
||||
case (Leaf l w_l)
|
||||
show ?case
|
||||
using assms(2) proof(induction \<open>r\<close>)
|
||||
case (Leaf r' w_r)
|
||||
then show ?case
|
||||
by (simp add: rope_concat_eq)
|
||||
next
|
||||
case (Node r_l w_r r')
|
||||
then show ?case
|
||||
by (simp add: add.assoc rope_concat_eq)
|
||||
qed
|
||||
next
|
||||
case (Node l1 x2 l2)
|
||||
then show ?case
|
||||
using assms(2) proof(induction r)
|
||||
case (Leaf x1 x2)
|
||||
then show ?case
|
||||
by (simp add: add.assoc rope_concat_eq)
|
||||
next
|
||||
case (Node r1 x2 r2)
|
||||
then show ?case
|
||||
by (simp add: rope_concat_def)
|
||||
qed
|
||||
qed
|
||||
|
||||
lemma smart_concat_lessThanEq_rope_concat:
|
||||
assumes \<open>valid_rope l\<close> \<open>valid_rope r\<close>
|
||||
shows \<open>size (smart_rope_concat l r) \<le> size(rope_concat l r)\<close>
|
||||
using assms proof(induction l)
|
||||
case (Leaf x1 x2)
|
||||
then show ?case
|
||||
using assms(2) proof(induction r)
|
||||
case (Leaf x1 x2)
|
||||
then show ?case
|
||||
by (simp add: rope_concat_def)
|
||||
next
|
||||
case (Node r1 x2 r2)
|
||||
then show ?case by (simp add: rope_concat_def)
|
||||
qed
|
||||
next
|
||||
case (Node l1 x2 l2)
|
||||
then show ?case using assms(2) by(induction r, simp_all add: rope_concat_def)
|
||||
qed
|
||||
|
||||
fun safe_rope_delete :: \<open>Rope \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (Rope \<times> Rope)\<close> where
|
||||
\<open>safe_rope_delete rope i len = (let (left,rem) = split rope i;
|
||||
(_, right) = split rem len;
|
||||
return = (if is_empty left then right else if is_empty right then left else rope_concat left right)
|
||||
in (rem, return))\<close>
|
||||
|
||||
definition rope_delete :: \<open>Rope \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> Rope\<close> where
|
||||
\<open>rope_delete r i len = snd (safe_rope_delete r i len)\<close>
|
||||
|
||||
definition rope_sub_str :: \<open>Rope \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> Rope\<close> where
|
||||
\<open>rope_sub_str r i len = fst (safe_rope_delete r i len)\<close>
|
||||
|
||||
|
||||
definition \<open>hello_my_rope \<equiv> rope_concat (Leaf STR ''Hello_'' 6) (Leaf STR ''my_'' 3)\<close>
|
||||
|
||||
definition \<open>name_i_rope \<equiv> rope_concat (Leaf STR ''na'' 2) (Leaf STR ''me_i'' 4)\<close>
|
||||
|
||||
definition \<open>s_Simon_rope \<equiv> rope_concat (Leaf STR ''s'' 1) (Leaf STR ''_Simon'' 6)\<close>
|
||||
|
||||
definition \<open>name_is_Simon_rope \<equiv> rope_concat name_i_rope s_Simon_rope\<close>
|
||||
|
||||
definition \<open>hello_my_name_is_Simon_rope \<equiv> rope_concat (rope_concat hello_my_rope name_is_Simon_rope) (Leaf STR '''' 0)\<close>
|
||||
|
||||
value \<open>to_str (rope_delete hello_my_name_is_Simon_rope (2) 15)\<close>
|
||||
|
||||
text\<open>Implement a function @{term \<open>rope_insert (r :: Rope) (i :: nat) (s :: String.literal)\<close>} that inserts the string @{term s} at position @{term \<open>i\<close>}.\<close>
|
||||
|
||||
fun rope_insert :: \<open>Rope \<Rightarrow> nat \<Rightarrow> String.literal \<Rightarrow> Rope\<close> where
|
||||
\<open>rope_insert r i s = (let (left, right) = split r i in rope_concat (rope_concat left (mk_leaf s)) right)\<close>
|
||||
|
||||
value \<open>to_str (rope_insert hello_my_name_is_Simon_rope 9 STR ''first_'')\<close>
|
||||
|
||||
definition \<open>test r i len = rope_insert (rope_delete r i len) i (to_str (rope_sub_str r i len))\<close>
|
||||
|
||||
value \<open>safe_rope_delete (Node (Leaf STR ''a'' 1) 1 (Leaf STR ''a'' 1)) 1 1 \<close>
|
||||
|
||||
lemma \<open>rope_insert (rope_delete r i len) i (to_str (rope_sub_str r i len)) = r\<close> oops
|
||||
text\<open>These methods are correct as is, but do not perform the most optimally. Optimize these operations by implementing
|
||||
a function @{term \<open>rebalance\<close>} that rebalances the the Rope.\<close>
|
||||
|
||||
fun rebalance :: \<open>Rope \<Rightarrow> Rope\<close> where
|
||||
\<open>rebalance (Leaf s w) = Leaf s w\<close>|
|
||||
\<open>rebalance (Node l w r) = \<close>
|
||||
end
|
||||
@ -1,5 +1,5 @@
|
||||
theory Ropes_Template
|
||||
imports Utils
|
||||
imports Utils
|
||||
begin
|
||||
|
||||
chapter\<open>Challenge 0 from VerifyThis 2024: \<^url>\<open>https://www.pm.inf.ethz.ch/research/verifythis.html\<close>\<close>
|
||||
@ -10,23 +10,24 @@ text\<open>The task is to implement a "Rope" ( \<^url>\<open>https://en.wikipedi
|
||||
originally published by Boehm - \<^url>\<open>https://www.cs.tufts.edu/comp/150FP/archive/hans-boehm/ropes.pdf\<close>
|
||||
- a special type of binary tree to efficiently store strings (in honor of Billy who can't be here today).\<close>
|
||||
|
||||
text\<open>Since the first half of this challenge is quite easy in Isabelle, we will skip the "trivial components" that can be found in \<^file>\<open>Utils.thy\<close>\<close>
|
||||
text\<open>Since the first half of this challenge is quite easy in HOL (termination and non crashing of basic functions),
|
||||
we will skip the "trivial components" that can be found in \<^file>\<open>Utils.thy\<close>\<close>
|
||||
|
||||
section\<open>Tasks\<close>
|
||||
|
||||
text\<open>The following are my play on ADTs using locales. We have three tiers:
|
||||
\<bullet> Basic
|
||||
\<bullet> Intermediate
|
||||
\<bullet> Advanced
|
||||
Basic ropes require the implementation of efficient length calculation,
|
||||
|
||||
\<bullet> Basic
|
||||
\<bullet> Intermediate
|
||||
\<bullet> Advanced
|
||||
|
||||
\<close>
|
||||
subsection\<open>Basic Ropes\<close>
|
||||
|
||||
text\<open>
|
||||
Basic ropes require the implementation of efficient length calculation,
|
||||
inefficient "naive" concatenation and finally splitting a rope into two across an index.
|
||||
|
||||
Intermediate Ropes require the implementation of "efficient" concatenation as similar to Boehm's \<^url>\<open>https://www.cs.tufts.edu/comp/150FP/archive/hans-boehm/ropes.pdf\<close>.
|
||||
and a(n) (naive) implementation of delete, sub string and insert. Naive in the sense that deleting then inserting in not structure preserving.
|
||||
However inserting then deleting should be structure preserving.
|
||||
|
||||
Advanced Ropes are really what makes them useful data structures.
|
||||
Before, all rope functions have been functionally correct, but not efficient due to the lack of rebalancing.
|
||||
These require the implementation of a rebalance function to balance a Rope, and a function mk_rope which constructs a non-trivially balanced Rope from a string.\<close>
|
||||
\<close>
|
||||
|
||||
locale Basic_Ropes =
|
||||
fixes str_len :: \<open>Rope \<Rightarrow> nat\<close>
|
||||
@ -36,22 +37,41 @@ assumes \<open>\<And>r. valid_rope r \<Longrightarrow> str_len r = size (to_str
|
||||
\<open>\<And>l r. \<lbrakk>valid_rope l; valid_rope r\<rbrakk> \<Longrightarrow> to_str (rope_concat l r) = to_str l + to_str r\<close>
|
||||
\<open>\<And>i r. valid_rope r \<Longrightarrow> valid_rope (fst (rope_split r i)) \<and> valid_rope (snd (rope_split r i))\<close>
|
||||
|
||||
subsection\<open>Intermediate Ropes\<close>
|
||||
|
||||
text\<open>Intermediate Ropes require the implementation of "efficient" concatenation as similar to Boehm's \<^url>\<open>https://www.cs.tufts.edu/comp/150FP/archive/hans-boehm/ropes.pdf\<close>.
|
||||
and a naive implementation of delete, sub string and insert. Naive in the sense that deleting then inserting the same string is not structure preserving.
|
||||
However inserting then deleting the same string should be structure preserving.
|
||||
\<close>
|
||||
|
||||
locale Intermediate_Ropes = Basic_Ropes +
|
||||
fixes boehm_concat :: \<open>Rope \<Rightarrow> Rope \<Rightarrow> Rope\<close>
|
||||
and rope_delete :: \<open>Rope \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> Rope\<close>
|
||||
and rope_delete :: \<open>Rope \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> Rope\<close>
|
||||
and rope_sub_str :: \<open>Rope \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> Rope\<close>
|
||||
and rope_insert :: \<open>Rope \<Rightarrow> nat \<Rightarrow> String.literal \<Rightarrow> Rope\<close>
|
||||
and rope_insert :: \<open>Rope \<Rightarrow> nat \<Rightarrow> String.literal \<Rightarrow> Rope\<close>
|
||||
assumes \<open>\<And>l r. \<lbrakk>valid_rope l; valid_rope r\<rbrakk> \<Longrightarrow> to_str (boehm_concat l r) = to_str l + to_str r\<close>
|
||||
\<open>\<And>l r. \<lbrakk>valid_rope l; valid_rope r\<rbrakk> \<Longrightarrow> size (boehm_concat l r) \<le> size (rope_concat l r)\<close>
|
||||
\<open>\<And>r i str. valid_rope r \<Longrightarrow> rope_delete (rope_insert r i str) i (size str) = r\<close>
|
||||
\<open>\<And>r i len. valid_rope r \<Longrightarrow> to_str (rope_insert (rope_delete r i len) i (to_str (rope_sub_str r i len))) = to_str r\<close>
|
||||
|
||||
subsection\<open>Advanced Ropes\<close>
|
||||
|
||||
text\<open>Advanced Ropes are really what makes them useful data structures.
|
||||
Before, all rope functions have been functionally correct, but not efficient due to the lack of rebalancing.
|
||||
These require the implementation of a rebalance function to balance a Rope, and a function mk_rope which constructs a non-trivially balanced Rope from a string.
|
||||
Using this rebalance function, implement efficient an efficient insert and delete which preserves the balancing of the tree\<close>
|
||||
|
||||
|
||||
locale Advanced_Ropes = Intermediate_Ropes +
|
||||
fixes rebalance :: \<open>Rope \<Rightarrow> Rope\<close>
|
||||
and mk_Rope :: \<open>String.literal \<Rightarrow> Rope\<close>
|
||||
fixes max_leaf_size :: \<open>nat\<close>
|
||||
and rebalance :: \<open>Rope \<Rightarrow> Rope\<close>
|
||||
and mk_Rope :: \<open>String.literal \<Rightarrow> Rope\<close>
|
||||
and efficient_delete :: \<open>Rope \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> Rope\<close>
|
||||
and efficient_insert :: \<open>Rope \<Rightarrow> nat \<Rightarrow> String.literal \<Rightarrow> Rope\<close>
|
||||
assumes \<open>\<And>r. \<not> is_balanced r \<and> valid_rope r \<Longrightarrow> is_balanced (rebalance r)\<close>
|
||||
\<open>\<And>s. is_balanced (mk_Rope s) \<and> 1 < str_len (mk_Rope s)\<close>
|
||||
\<open>\<And>r i len. rope_insert (rope_delete r i len) i (to_str (rope_sub_str r i len)) = r\<close>
|
||||
\<open>\<And>s. is_balanced (mk_Rope s)\<close>
|
||||
\<open>\<And>r i str. is_balanced r \<Longrightarrow> is_balanced (rope_insert r i str) \<and> (\<forall>leaf \<in># all_leaves (rope_insert r i str). str_len leaf \<in> {0<..max_leaf_size})\<close>
|
||||
\<open>\<And>r i len. is_balanced r \<Longrightarrow> is_balanced (efficient_delete r i len)\<close>
|
||||
|
||||
|
||||
end
|
||||
77
VerifyThis2024/Ropes_Template.thy~
Normal file
77
VerifyThis2024/Ropes_Template.thy~
Normal file
@ -0,0 +1,77 @@
|
||||
theory Ropes_Template
|
||||
imports Utils
|
||||
begin
|
||||
|
||||
chapter\<open>Challenge 0 from VerifyThis 2024: \<^url>\<open>https://www.pm.inf.ethz.ch/research/verifythis.html\<close>\<close>
|
||||
|
||||
section\<open>The Rope Data Structure\<close>
|
||||
|
||||
text\<open>The task is to implement a "Rope" ( \<^url>\<open>https://en.wikipedia.org/wiki/Rope_(data_structure)\<close> )
|
||||
originally published by Boehm - \<^url>\<open>https://www.cs.tufts.edu/comp/150FP/archive/hans-boehm/ropes.pdf\<close>
|
||||
- a special type of binary tree to efficiently store strings (in honor of Billy who can't be here today).\<close>
|
||||
|
||||
text\<open>Since the first half of this challenge is quite easy in HOL (termination and non crashing of basic functions),
|
||||
we will skip the "trivial components" that can be found in \<^file>\<open>Utils.thy\<close>\<close>
|
||||
|
||||
section\<open>Tasks\<close>
|
||||
|
||||
text\<open>The following are my play on ADTs using locales. We have three tiers:
|
||||
|
||||
\<bullet> Basic
|
||||
\<bullet> Intermediate
|
||||
\<bullet> Advanced
|
||||
|
||||
\<close>
|
||||
subsection\<open>Basic Ropes\<close>
|
||||
|
||||
text\<open>
|
||||
Basic ropes require the implementation of efficient length calculation,
|
||||
inefficient "naive" concatenation and finally splitting a rope into two across an index.
|
||||
\<close>
|
||||
|
||||
locale Basic_Ropes =
|
||||
fixes str_len :: \<open>Rope \<Rightarrow> nat\<close>
|
||||
and rope_concat :: \<open>Rope \<Rightarrow> Rope \<Rightarrow> Rope\<close>
|
||||
and rope_split :: \<open>Rope \<Rightarrow> nat \<Rightarrow> Rope \<times> Rope\<close>
|
||||
assumes \<open>\<And>r. valid_rope r \<Longrightarrow> str_len r = size (to_str r)\<close>
|
||||
\<open>\<And>l r. \<lbrakk>valid_rope l; valid_rope r\<rbrakk> \<Longrightarrow> to_str (rope_concat l r) = to_str l + to_str r\<close>
|
||||
\<open>\<And>i r. valid_rope r \<Longrightarrow> valid_rope (fst (rope_split r i)) \<and> valid_rope (snd (rope_split r i))\<close>
|
||||
|
||||
subsection\<open>Intermediate Ropes\<close>
|
||||
|
||||
text\<open>Intermediate Ropes require the implementation of "efficient" concatenation as similar to Boehm's \<^url>\<open>https://www.cs.tufts.edu/comp/150FP/archive/hans-boehm/ropes.pdf\<close>.
|
||||
and a naive implementation of delete, sub string and insert. Naive in the sense that deleting then inserting the same string is not structure preserving.
|
||||
However inserting then deleting the same string should be structure preserving.
|
||||
\<close>
|
||||
|
||||
locale Intermediate_Ropes = Basic_Ropes +
|
||||
fixes boehm_concat :: \<open>Rope \<Rightarrow> Rope \<Rightarrow> Rope\<close>
|
||||
and rope_delete :: \<open>Rope \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> Rope\<close>
|
||||
and rope_sub_str :: \<open>Rope \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> Rope\<close>
|
||||
and rope_insert :: \<open>Rope \<Rightarrow> nat \<Rightarrow> String.literal \<Rightarrow> Rope\<close>
|
||||
assumes \<open>\<And>l r. \<lbrakk>valid_rope l; valid_rope r\<rbrakk> \<Longrightarrow> to_str (boehm_concat l r) = to_str l + to_str r\<close>
|
||||
\<open>\<And>l r. \<lbrakk>valid_rope l; valid_rope r\<rbrakk> \<Longrightarrow> size (boehm_concat l r) \<le> size (rope_concat l r)\<close>
|
||||
\<open>\<And>r i str. valid_rope r \<Longrightarrow> rope_delete (rope_insert r i str) i (size str) = r\<close>
|
||||
\<open>\<And>r i len. valid_rope r \<Longrightarrow> to_str (rope_insert (rope_delete r i len) i (to_str (rope_sub_str r i len))) = to_str r\<close>
|
||||
|
||||
subsection\<open>Advanced Ropes\<close>
|
||||
|
||||
text\<open>Advanced Ropes are really what makes them useful data structures.
|
||||
Before, all rope functions have been functionally correct, but not efficient due to the lack of rebalancing.
|
||||
These require the implementation of a rebalance function to balance a Rope, and a function mk_rope which constructs a non-trivially balanced Rope from a string.
|
||||
Using this rebalance function, implement efficient an efficient insert and delete which preserves the balancing of the tree\<close>
|
||||
|
||||
|
||||
locale Advanced_Ropes = Intermediate_Ropes +
|
||||
fixes max_leaf_size :: \<open>nat\<close>
|
||||
and rebalance :: \<open>Rope \<Rightarrow> Rope\<close>
|
||||
and mk_Rope :: \<open>String.literal \<Rightarrow> Rope\<close>
|
||||
and efficient_delete :: \<open>Rope \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> Rope\<close>
|
||||
and efficient_insert :: \<open>Rope \<Rightarrow> nat \<Rightarrow> String.literal \<Rightarrow> Rope\<close>
|
||||
assumes \<open>\<And>r. \<not> is_balanced r \<and> valid_rope r \<Longrightarrow> is_balanced (rebalance r)\<close>
|
||||
\<open>\<And>s. is_balanced (mk_Rope s)\<close>
|
||||
\<open>\<And>r i str. is_balanced r \<Longrightarrow> is_balanced (rope_insert r i str) \<and> (\<forall>leaf \<in># all_leaves (rope_insert r i str). str_len leaf \<in> {0<..max_leaf_size})\<close>
|
||||
\<open>\<And>r i len. is_balanced r \<Longrightarrow> is_balanced (efficient_delete r i len)\<close>
|
||||
|
||||
|
||||
end
|
||||
@ -1,5 +1,5 @@
|
||||
theory Utils
|
||||
imports Main HOL.NthRoot
|
||||
imports Main Fibonacci "HOL-Library.Multiset" "List-Index.List_Index"
|
||||
begin
|
||||
|
||||
chapter\<open>Helper Lemmas, Functions and Definitions\<close>
|
||||
@ -52,6 +52,8 @@ subsection\<open>Basics\<close>
|
||||
|
||||
datatype Rope = Leaf String.literal nat | Node Rope nat Rope
|
||||
|
||||
definition \<open>hello_world_rope \<equiv> Node (Leaf (STR ''Hello '') 6) 6 (Leaf (STR ''World'') 5)\<close>
|
||||
|
||||
fun mk_leaf :: \<open>String.literal \<Rightarrow> Rope\<close> where
|
||||
\<open>mk_leaf s = Leaf s (size s)\<close>
|
||||
|
||||
@ -67,73 +69,21 @@ fun to_str :: \<open>Rope \<Rightarrow> String.literal\<close> where
|
||||
\<open>to_str (Leaf s _) = s\<close>|
|
||||
\<open>to_str (Node l _ r) = to_str l + to_str r\<close>
|
||||
|
||||
fun all_leaves :: \<open>Rope \<Rightarrow> Rope multiset\<close> where
|
||||
\<open>all_leaves (Leaf s w) = {# Leaf s w #}\<close>|
|
||||
\<open>all_leaves (Node l _ r) = all_leaves l \<union># all_leaves r\<close>
|
||||
|
||||
subsection\<open>Advanced\<close>
|
||||
|
||||
text\<open>The following formalises the definition of balanced from Boehm \<^url>\<open>https://www.cs.tufts.edu/comp/150FP/archive/hans-boehm/ropes.pdf\<close>\<close>
|
||||
|
||||
fun fib :: \<open>nat \<Rightarrow> nat\<close> where
|
||||
\<open>fib 0 = 0\<close>|
|
||||
\<open>fib (Suc 0) = Suc 0\<close>|
|
||||
\<open>fib (Suc (Suc n)) = fib (Suc n) + fib n\<close>
|
||||
|
||||
definition \<open>\<phi> = (1 + sqrt 5)/2\<close>
|
||||
definition \<open>\<psi> = (1 - sqrt 5)/2\<close>
|
||||
|
||||
lemma \<phi>_pow_2: \<open>\<phi>^2 = (1 + \<phi>)\<close> unfolding \<phi>_def
|
||||
proof-
|
||||
have *: \<open>(1+sqrt 5)\<^sup>2 = (1 + 2*sqrt 5 + 5)\<close> using power2_sum[of \<open>1\<close> \<open>sqrt 5\<close>] by auto
|
||||
have \<open>((1 + sqrt 5) / 2)\<^sup>2 = (1+sqrt 5)\<^sup>2 / 4\<close>
|
||||
by (simp add: power_divide)
|
||||
hence \<open>... = (1 + 2*sqrt 5 + 5) / 4\<close> using * by auto
|
||||
hence \<open>... = 2*(1 + sqrt 5)/4 + 1\<close> by simp
|
||||
thus \<open>((1 + sqrt 5) / 2)\<^sup>2= 1 + (1 + sqrt 5) / 2\<close>
|
||||
by (smt (z3) "*" field_sum_of_halves four_x_squared)
|
||||
qed
|
||||
|
||||
lemma \<psi>_pow_2: \<open>\<psi>^2 = (1 + \<psi>)\<close>
|
||||
proof-
|
||||
have *: \<open>(1-sqrt 5)\<^sup>2 = (1 - 2*sqrt 5 + 5)\<close> using power2_diff[of \<open>1\<close> \<open>sqrt 5\<close>] by auto
|
||||
hence \<open>(1-sqrt 5)\<^sup>2/4 = (1 - 2*sqrt 5 + 5)/4\<close> by auto
|
||||
hence \<open>... = 2*(1 - sqrt 5)/4 + 1\<close> by simp
|
||||
thus ?thesis
|
||||
by (smt (z3) "*" \<psi>_def field_sum_of_halves four_x_squared)
|
||||
qed
|
||||
|
||||
lemmas golden_ratios = \<phi>_def \<psi>_def
|
||||
|
||||
lemma golden_diff: \<open>(\<phi> - \<psi>) = sqrt 5\<close> unfolding golden_ratios
|
||||
by (smt (z3) field_sum_of_halves)
|
||||
|
||||
lemma fib_correct: \<open>fib n = (\<phi>^n - \<psi>^n) / sqrt 5\<close>
|
||||
proof(induction n rule: fib.induct)
|
||||
case 1
|
||||
then show ?case by simp
|
||||
next
|
||||
case 2
|
||||
then show ?case
|
||||
by (simp add: golden_diff)
|
||||
next
|
||||
case (3 n)
|
||||
then show ?case
|
||||
proof-
|
||||
have \<open>real (fib (Suc (Suc n))) = real (fib (Suc n)) + real (fib n)\<close> by auto
|
||||
moreover have \<open>... = (\<phi> ^ Suc n - \<psi> ^ Suc n) / sqrt 5 + (\<phi> ^ n - \<psi> ^ n) / sqrt 5\<close> using 3 by auto
|
||||
moreover have \<open>... = (\<phi> ^ Suc n + \<phi>^n - \<psi> ^ Suc n - \<psi> ^ n)/sqrt 5\<close>
|
||||
by (smt (verit, best) add_divide_distrib)
|
||||
moreover have \<open>... = (\<phi> ^ n * (\<phi> + 1) - \<psi> ^ n * (\<psi> + 1))/ sqrt 5\<close>
|
||||
by (simp add: distrib_right mult.commute)
|
||||
ultimately show ?case using \<psi>_pow_2 \<phi>_pow_2
|
||||
by (metis add.commute add_2_eq_Suc power_add)
|
||||
qed
|
||||
qed
|
||||
|
||||
text\<open>a bit overkill on the Fibonacci formalisation but I got carried away.\<close>
|
||||
|
||||
fun rope_length :: \<open>Rope \<Rightarrow> nat\<close> where
|
||||
\<open>rope_length (Leaf _ _) = Suc 0\<close>|
|
||||
\<open>rope_length (Node l _ r) = rope_length l + rope_length r\<close>
|
||||
definition rope_width :: \<open>Rope \<Rightarrow> nat\<close> where
|
||||
\<open>rope_width r = size (all_leaves r)\<close>
|
||||
|
||||
definition is_balanced :: \<open>Rope \<Rightarrow> bool\<close> where
|
||||
\<open>is_balanced r = (rope_length r \<le> fib (size r + 2))\<close>
|
||||
\<open>is_balanced r = (fib (size r + 2) \<le> sum_weights r)\<close>
|
||||
|
||||
value \<open>is_balanced hello_world_rope\<close>
|
||||
|
||||
value \<open>fib 5\<close>
|
||||
end
|
||||
89
VerifyThis2024/Utils.thy~
Normal file
89
VerifyThis2024/Utils.thy~
Normal file
@ -0,0 +1,89 @@
|
||||
theory Utils
|
||||
imports Main Fibonacci "HOL-Library.Multiset"
|
||||
begin
|
||||
|
||||
chapter\<open>Helper Lemmas, Functions and Definitions\<close>
|
||||
|
||||
section\<open>String Literal helper lemmas for Rope proofs\<close>
|
||||
|
||||
lemma literal_plus_size_eq: \<open>size ((l::String.literal) + r) = size l + size r\<close>
|
||||
by (simp add: plus_literal.rep_eq size_literal.rep_eq)
|
||||
|
||||
fun sub_str :: \<open>String.literal \<Rightarrow> nat set \<Rightarrow> String.literal\<close> where
|
||||
\<open>sub_str s I = String.implode (nths (literal.explode s) I)\<close>
|
||||
|
||||
lemma explode_sub_str: \<open>literal.explode (sub_str s I) = nths (literal.explode s) I\<close>
|
||||
by (metis String.implode_explode_eq implode.rep_eq nths_map sub_str.simps)
|
||||
|
||||
lemma size_implode_single: \<open>size (String.implode [x]) = Suc 0\<close> by (simp add: size_literal.rep_eq)
|
||||
|
||||
lemma size_implode: \<open>size (String.implode xs) = length xs\<close>
|
||||
proof(induction xs)
|
||||
case Nil
|
||||
then show ?case
|
||||
by (simp add: size_literal.rep_eq)
|
||||
next
|
||||
case (Cons a xs)
|
||||
have \<open>size (String.implode (a # xs)) = (size (String.implode [a] + String.implode xs))\<close>
|
||||
apply (simp add: String.implode_def)
|
||||
by (metis String.explode_implode_eq add_0 add_Suc implode.abs_eq length_Cons list.simps(8,9)
|
||||
list.size(3) literal_plus_size_eq size_literal.rep_eq)
|
||||
moreover have \<open>... = Suc (size (String.implode xs))\<close> by (simp add: literal_plus_size_eq size_implode_single)
|
||||
moreover have \<open>... = Suc (length xs)\<close> using Cons by blast
|
||||
ultimately show ?case by simp
|
||||
qed
|
||||
|
||||
lemma size_sub_str: \<open>size (sub_str s I) = card {i. i < size s \<and> i \<in> I}\<close>
|
||||
by(simp add: size_implode length_nths size_literal.rep_eq)
|
||||
|
||||
lemma atLeastLessThan_eq: \<open>{i..<size s} = {ia. ia < size s \<and> i \<le> ia}\<close> by auto
|
||||
|
||||
lemma atLeastAtMost_eq: \<open>(if i < size s then {..i} else {..<size s}) = {ia. ia < size s \<and> ia \<le> i}\<close> by auto
|
||||
|
||||
lemma size_sub_str_atLeast: \<open>size (sub_str s {i..}) = size s - i\<close> unfolding size_sub_str[of s \<open>{i..}\<close>]
|
||||
by (simp add: atLeastLessThan_eq[symmetric])
|
||||
|
||||
lemma size_sub_str_atMost: \<open>size (sub_str s {..i}) = (if i < size s then Suc i else size s)\<close> unfolding size_sub_str[of s \<open>{..i}\<close>]
|
||||
by (simp add: atLeastAtMost_eq[symmetric])
|
||||
|
||||
section\<open>Rope Definitions\<close>
|
||||
|
||||
subsection\<open>Basics\<close>
|
||||
|
||||
datatype Rope = Leaf String.literal nat | Node Rope nat Rope
|
||||
|
||||
definition \<open>hello_world_rope \<equiv> Node (Leaf (STR ''Hello '') 6) 6 (Leaf (STR ''World'') 5)\<close>
|
||||
|
||||
fun mk_leaf :: \<open>String.literal \<Rightarrow> Rope\<close> where
|
||||
\<open>mk_leaf s = Leaf s (size s)\<close>
|
||||
|
||||
fun sum_weights :: \<open>Rope \<Rightarrow> nat\<close> where
|
||||
\<open>sum_weights (Leaf _ s) = s\<close>|
|
||||
\<open>sum_weights (Node l w r) = sum_weights l + sum_weights r\<close>
|
||||
|
||||
fun valid_rope :: \<open>Rope \<Rightarrow> bool\<close> where
|
||||
\<open>valid_rope (Leaf s w) = (size s = w)\<close>|
|
||||
\<open>valid_rope (Node l w r) = (valid_rope l \<and> valid_rope r \<and> (w = sum_weights l))\<close>
|
||||
|
||||
fun to_str :: \<open>Rope \<Rightarrow> String.literal\<close> where
|
||||
\<open>to_str (Leaf s _) = s\<close>|
|
||||
\<open>to_str (Node l _ r) = to_str l + to_str r\<close>
|
||||
|
||||
fun all_leaves :: \<open>Rope \<Rightarrow> Rope multiset\<close> where
|
||||
\<open>all_leaves (Leaf s w) = {# Leaf s w #}\<close>|
|
||||
\<open>all_leaves (Node l _ r) = all_leaves l \<union># all_leaves r\<close>
|
||||
|
||||
subsection\<open>Advanced\<close>
|
||||
|
||||
text\<open>The following formalises the definition of balanced from Boehm \<^url>\<open>https://www.cs.tufts.edu/comp/150FP/archive/hans-boehm/ropes.pdf\<close>\<close>
|
||||
|
||||
definition rope_width :: \<open>Rope \<Rightarrow> nat\<close> where
|
||||
\<open>rope_width r = size (all_leaves r)\<close>
|
||||
|
||||
definition is_balanced :: \<open>Rope \<Rightarrow> bool\<close> where
|
||||
\<open>is_balanced r = (fib (size r + 2) \<le> sum_weights r)\<close>
|
||||
|
||||
value \<open>is_balanced hello_world_rope\<close>
|
||||
|
||||
value \<open>fib 5\<close>
|
||||
end
|
||||
Loading…
Reference in New Issue
Block a user