diff options
Diffstat (limited to 'Verification.thy')
| -rw-r--r-- | Verification.thy | 122 |
1 files changed, 122 insertions, 0 deletions
diff --git a/Verification.thy b/Verification.thy new file mode 100644 index 0000000..bdb1743 --- /dev/null +++ b/Verification.thy @@ -0,0 +1,122 @@ +theory Verification imports + Notraits +begin + + +fun height_of_node :: "AVLNode option \<Rightarrow> nat" where + "height_of_node None = 0" +| "height_of_node (Some (mkAVLNode _ l r)) = + max (height_of_node l) (height_of_node r) + 1" + + + +fun is_ok :: "'a result \<Rightarrow> bool" where + "is_ok (Ok _) = True" +| "is_ok _ = False" + + +lemma[simp]: "is_ok (cmp a b)" + by simp + + +(* nicer induction rule for type AVLNode option *) +lemma AVLNode_option_induct: + assumes "\<And>v l r. (\<And>x. x \<in> set_option l \<Longrightarrow> P (Some x)) + \<Longrightarrow> (\<And>x. x \<in> set_option r \<Longrightarrow> P (Some x)) + \<Longrightarrow> P (Some (mkAVLNode v l r))" + and "P None" + shows "P AVLNodeOption" +proof (cases AVLNodeOption) + case None + then show ?thesis using assms by simp +next + case (Some a) + then show ?thesis + apply (induction a arbitrary: AVLNodeOption) + using Some assms(1) by blast +qed + + +lemma right_is_smaller: "height_of_node r < height_of_node (Some (mkAVLNode v l r))" + by (cases l) auto + +lemma left_is_smaller: "height_of_node l < height_of_node (Some (mkAVLNode v l r))" + by (cases r) auto + + +(* the loop in find always terminates (important for using \<open>obtain\<close> further down *) +termination aVLTreeSet_find_loop +proof (relation "measure (\<lambda>(v, t). height_of_node t)") + show "wf (measure (\<lambda>(v, t). height_of_node t))" by simp +next + fix value1 current_tree and x2 :: "AVLNode" + assume "current_tree = Some x2" + then show "((value1, right x2), value1, current_tree) \<in> measure (\<lambda>(v, t). height_of_node t)" + using right_is_smaller in_measure + by (metis AVLNode.collapse case_prod_conv) +next + fix value1 current_tree and x2 :: "AVLNode" + assume "current_tree = Some x2" + then show "((value1, left x2), value1, current_tree) \<in> measure (\<lambda>(v, t). height_of_node t)" + using left_is_smaller in_measure + by (metis AVLNode.collapse case_prod_conv) +qed + + +value "cmp (u32 1) (u32 1)" + +value "left (mkAVLNode (u32 0) None (Some (mkAVLNode (u32 0) None None)))" + +lemma find_loop_ok: "is_ok (aVLTreeSet_find_loop v n)" +proof (induction n arbitrary: v rule: AVLNode_option_induct) + case (1 u l r) + obtain ordering where order: "Ok ordering = cmp u v" + by force + then show ?case + proof (cases ordering) + case Ordering_Less + hence "is_ok (aVLTreeSet_find_loop v r)" + using 1 by (simp add: option.split_sel_asm) + then obtain b r' where a: "Ok (b, r') = aVLTreeSet_find_loop v r" + by (auto elim: is_ok.elims) + hence "aVLTreeSet_find_loop v (Some (mkAVLNode u l r)) = + Ok (b, Some (mkAVLNode u l r'))" + using Ordering_Less order apply simp + by (smt (verit) AVLNode.expand AVLNode.record_simps(12) AVLNode.record_simps(13) AVLNode.record_simps(14) AVLNode.sel(1) AVLNode.sel(2) AVLNode.sel(3) case_prod_conv result.simps(4)) + then show ?thesis by simp + next + case Ordering_Equal + hence "aVLTreeSet_find_loop v (Some (mkAVLNode u l r)) = Ok (True, Some (mkAVLNode u l r))" + using 1 order by simp + then show ?thesis by simp + next + case Ordering_Greater + hence "is_ok (aVLTreeSet_find_loop v l)" + using 1 by (simp add: option.split_sel_asm) + then obtain b l' where a: "Ok (b, l') = aVLTreeSet_find_loop v l" + by (auto elim: is_ok.elims) + hence "aVLTreeSet_find_loop v (Some (mkAVLNode u l r)) = + Ok (b, Some (mkAVLNode u l' r))" + using Ordering_Greater order apply simp + by (smt (verit, ccfv_threshold) AVLNode.expand AVLNode.record_simps(6) AVLNode.record_simps(7) AVLNode.record_simps(8) AVLNode.sel(1) AVLNode.sel(2) AVLNode.sel(3) case_prod_conv result.simps(4)) + then show ?thesis by simp + qed +next + case 2 + then show ?case by simp +qed + +(* find never produces an error *) +lemma find_ok: "\<exists>res. aVLTreeSet_find t v = Ok res" +proof - + obtain b as where "Ok (b, as) = aVLTreeSet_find_loop v (root t)" + using find_loop_ok by (metis is_ok.elims(2) old.prod.exhaust) + then have "aVLTreeSet_find t v = Ok (b, \<lparr> root = as \<rparr>)" + apply simp unfolding bind_def + by (metis old.prod.case result.simps(4)) + thus ?thesis + by simp +qed + + +end
\ No newline at end of file |