changeset 109:60e3bf58f227

An isabelle proof of correctness for binary search
author Sigurd Meldgaard <stm@daimi.au.dk>
date Mon, 10 Aug 2009 10:18:10 +0200
parents 9f212bdf4c5d
children fb3e0d320df6
files proof_binary.thy
diffstat 1 files changed, 341 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/proof_binary.thy	Mon Aug 10 10:18:10 2009 +0200
@@ -0,0 +1,341 @@
+theory Binary
+imports Main
+begin
+
+definition "mid l u \<equiv> (l + u) div (2::nat)"
+
+(* If f is monotone, this returns smallest natural
+ number x, s.t. l \<le> x < u where \<not> f x \<le> e*)
+function binsearch :: "(nat \<Rightarrow> ('b::linorder )) \<Rightarrow> 'b \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+"binsearch f e l u =
+ (if l \<ge> u then u else
+ (if f (mid l u) \<le> e then
+ (binsearch f e ((mid l u)+1) u) else
+ (binsearch f e l (mid l u))))"
+ by pat_completeness auto
+termination
+by (relation "measure (\<lambda>(f,e,l,u). u - l)") (auto simp add: mid_def)
+
+(* The simplifier easily loops if we allow it to unwrap this: *)
+declare binsearch.simps [simp del]
+
+lemma mid_less: "l < u \<Longrightarrow> (mid l u) + 1 \<le> u"
+ by (auto simp add: mid_def)
+
+lemma mid_less1: "l < u \<Longrightarrow> u - ((mid l u) + (1\<Colon>nat)) < u - l"
+ by (auto simp add: mid_def)
+
+lemma mid_less2: "l < u \<Longrightarrow> ((mid l u) - l) < u - l"
+ by (auto simp add: mid_def)
+
+lemma binsearch_less: "l < u \<Longrightarrow> binsearch f e l u \<le> u"
+ apply (induct h\<equiv>"(l,u)" arbitrary: u l rule: measure_induct [of
+"(\<lambda>((l::nat),u) . u-l)"])
+ apply clarify
+ apply (case_tac "f (mid l u) \<le> e")
+ apply (drule_tac x="(((mid l u)+1), u)" in spec)
+ apply (clarify)
+ apply (drule mid_less1)
+ apply (simp add: binsearch.simps)
+ apply (drule_tac x="(l, (mid l u))" in spec)
+ apply (clarify)
+ apply (frule mid_less2)
+ apply safe
+ apply (drule_tac x="(mid l u)" in spec)
+ apply (drule_tac x="l" in spec)
+ apply safe
+ by (simp_all add: binsearch.simps)
+
+lemma binsearch_greater: 
+  shows "l \<le> u \<Longrightarrow> l \<le> binsearch f e l u"
+proof (induct h\<equiv>"(l,u)" arbitrary: l u rule: measure_induct [of "(\<lambda>((l::nat),u) . u-l)"])
+  case 1
+  assume le: "l\<le>u"
+  thus ?case
+  proof -
+    have "l < u \<or> l = u" using le by auto
+    moreover {
+      assume eq: "l = u"
+      hence "binsearch f e l u = u" using binsearch.simps[of f e l u] by auto
+      hence "l \<le> binsearch f e l u" using eq by auto
+    } moreover {
+      assume less: "l < u"
+      hence "l \<le> binsearch f e l u"
+      proof cases
+        assume le_case: "f (mid l u) \<le> e"
+        have binsearch_in_case: "binsearch f e l u = binsearch f e (mid l u + 1) u"
+          using less binsearch.simps[of f e l u] le_case
+          by auto
+        have "l \<le> binsearch f e (mid l u + 1) u"
+          using 1 less mid_less1[of l u] mid_less2[of l u] mid_less[of l u]
+          apply (drule_tac x="(mid l u + 1, u)" in spec, clarify, simp)
+          apply (drule_tac x="mid l u + 1" in spec)
+          by (drule_tac x="u" in spec, clarify, auto)
+        thus ?thesis using binsearch_in_case by auto
+      next assume le_case: "\<not> f (mid l u) \<le> e"
+        have binsearch_in_case: "binsearch f e l u = binsearch f e l (mid l u)"
+          using less binsearch.simps[of f e l u] le_case
+          by auto
+        have "l \<le> binsearch f e l (mid l u)"
+          using 1 less mid_less1[of l u] mid_less2[of l u] mid_less[of l u]
+          by (drule_tac x="(l, mid l u)" in spec, clarify, simp)
+        thus ?thesis using binsearch_in_case by auto
+      qed
+    }
+    ultimately show "l \<le> binsearch f e l u" by auto
+  qed
+qed
+
+lemma mid_diff_2: "u = Suc (mid l u) \<Longrightarrow> l+2 = u \<or> l+1 = u"
+ by (auto simp add: mid_def)
+
+lemma l_plus_1_u:
+ assumes mono: "mono (f::nat \<Rightarrow> ('a::linorder))"
+ and all_less_l: "(\<forall>x<l. f x \<le> e)"
+ and all_greater_u: "e < f u"
+ and plus_1: "l+1 = u"
+ shows "e < f (binsearch f e l u) \<and> (\<forall>x<binsearch f e l u. f x \<le> e)"
+proof (cases)
+ have mid_val: "mid l (Suc l) = l"
+   by (insert plus_1, auto simp add: mid_def)
+ assume le_case: "f (mid l u) \<le> e"
+ have binsearch_u: "binsearch f e l u = u"
+   apply (insert plus_1)
+   apply (insert le_case)
+   apply (clarify, simp)
+   apply (subst (asm) mid_val)
+   apply (subst binsearch.simps, simp)
+   apply auto
+   apply (subst (asm) mid_val)+
+   apply (subst mid_val)
+   apply (subst binsearch.simps, simp)
+   apply (subst (asm) mid_val)+
+   apply (subst mid_val)
+   by auto
+ then have "e < f (binsearch f e l u)"
+   by (simp add: all_greater_u)
+ moreover have "(\<forall>x<binsearch f e l u. f x \<le> e)"
+   apply (simp add: binsearch_u)
+   apply (rule allI, rule impI)
+   apply (subst (asm) less_eq_Suc_le)
+   apply (subst (asm) plus_1[THEN sym])
+   apply (simp)
+   apply (case_tac "x=l")
+   apply (insert le_case)
+   apply (insert plus_1 mid_val)
+   apply (insert le_case)
+   apply (simp,clarify)
+   apply (insert all_less_l)
+   by auto
+ ultimately show ?thesis ..
+next assume greater_case: "\<not> f (mid l u) \<le> e"
+ have mid_val: "mid l (Suc l) = l"
+   by (insert plus_1, auto simp add: mid_def)
+ have binsearch_u: "binsearch f e l u = l"
+   apply (insert plus_1)
+   apply (insert greater_case)
+   apply (clarify, simp)
+   apply (subst (asm) mid_val)
+   apply (subst binsearch.simps, simp)
+   apply auto
+   apply (subst (asm) mid_val)+
+   apply (subst mid_val)
+   apply (subst binsearch.simps, simp)
+   apply (subst (asm) mid_val)+
+   apply (subst mid_val)
+   by (auto simp add: binsearch.simps)
+ then have "e < f (binsearch f e l u)"
+   apply (simp add: binsearch_u)
+   apply (insert  greater_case mid_val)
+   by (subst (asm) plus_1 [THEN sym], simp)
+ moreover have "(\<forall>x<binsearch f e l u. f x \<le> e)"
+   apply (insert all_less_l)
+   by (subst binsearch_u, auto)
+ ultimately show ?thesis ..
+qed
+
+lemma almost_there: assumes mono: "mono (f::nat \<Rightarrow> ('a::linorder))"
+ and all_less_l: "(\<forall>x<l. f x \<le> e)"
+ and all_greater_u: "e < f u"
+ and diff_1: "(mid l u)+1 = u"
+ shows "e < f (binsearch f e l u) \<and> (\<forall>x<binsearch f e l u. f x \<le> e)"
+proof -
+ have "l+2 = u \<or> l+1 = u" using diff_1 mid_diff_2[of u l] by (simp)
+ moreover
+ { assume plus_1: "l+1 = u"
+   hence plus_1_case: ?thesis using l_plus_1_u[of f l e u] assms by simp
+ }
+ moreover
+ {
+   assume plus_2: "l+2 = u"
+   hence less: "l < u" by simp
+   then moreover have mid_in_case: "mid l u = l + 1" using plus_2
+mid_def by auto
+   have ?thesis
+   proof cases
+     assume le_case: "f (mid l u) \<le> e"
+     then moreover have binsearch_in_case: "binsearch f e l u = u"
+       using binsearch.simps[of f e l u] binsearch.simps[of f e u u]
+         less plus_2 le_case diff_1 by simp
+     then moreover have all_less: "\<forall>x<binsearch f e l u. f x \<le> e"
+     proof -
+       { fix x assume x_le: "x<binsearch f e l u"
+         have "f x \<le> e" proof (cases)
+           assume "x < l"
+           thus "f x \<le> e" using all_less_l by blast
+         next assume x_case: "\<not> x < l"
+           have"x<u" using x_le binsearch_in_case by auto
+           hence "x = l \<or> x = l+1" using plus_2 x_case  by auto
+           thus "f x \<le> e" using mono mono_def[of f] le_case
+             mid_in_case apply (case_tac "x=l", simp)
+             apply (drule_tac x="l" in spec)
+             apply (drule_tac x="Suc l" in spec)
+             apply simp+
+             done
+         qed
+       }
+       thus ?thesis by blast
+     qed
+     thus ?thesis using all_less all_greater_u binsearch_in_case by(auto)
+   next
+     assume le_case: "\<not>f (mid l u) \<le> e"
+     then moreover have "e < f (mid l u)" by simp
+     then moreover have le_case_mod: "e < f (l + 1)" using mid_in_case by simp
+     then moreover have binsearch_in_case: "binsearch f e l u =
+binsearch f e l (l+1)"
+       using binsearch.simps[of f e l u] binsearch.simps[of f e "l+1" "(l+2)"]
+         less plus_2 le_case diff_1 mid_in_case by simp
+     thus ?thesis
+       using l_plus_1_u[of f "l" e "l+1"] assms le_case_mod by simp
+   qed
+   }
+ultimately show ?thesis by blast
+qed
+
+theorem binsearch_correct: assumes mono: "mono (f::nat \<Rightarrow> ('a::linorder))"
+ shows "e < f u \<longrightarrow> (\<forall>x<l. f x \<le> e) \<longrightarrow> e < f (binsearch f e l u) \<and>
+(\<forall>x<binsearch f e l u. f x \<le> e)"
+proof (induct x\<equiv>"(l, u)" arbitrary: l u rule: measure_induct [of
+"(\<lambda>((l::nat),u) . u-l)"])
+ case 1
+ thus ?case
+ proof cases
+   assume "u\<le>l"
+   thus ?thesis using assms
+     by (auto simp add: binsearch.simps)
+ next
+   assume "\<not>u\<le>l"
+   have less: "l < u" using `\<not>u\<le>l` by auto
+   then show ?case
+   proof (cases)
+     assume "mid l u + 1 = u"
+     thus ?case using mono almost_there by blast
+   next
+     assume not_one_diff: "\<not> mid l u + 1 = u"
+     hence mid_less_u: "(mid l u) + 1 < u" using less mid_less[of l u]
+       by simp
+     show ?thesis
+     proof (cases)
+       assume le_case: "f (mid l u) \<le> e"
+       hence "\<forall>x \<le> mid l u. f x \<le> e"
+         using mono
+         apply (subst (asm) mono_def)
+         apply rule+
+         apply (drule_tac x="x" in spec)
+         apply (drule_tac x="mid l u" in spec)
+         by simp
+       hence less_mid_all: "\<forall>x < mid l u + 1. f x \<le> e"
+         by auto
+       have binsearch_in_case: "binsearch f e l u = binsearch f e
+((mid l u)+1) u"
+         using binsearch.simps[of f e l u] less le_case
+         by (auto)
+       hence gr_u: "mid l u + 1 \<le> binsearch f e l u"
+         using less binsearch_greater[of "(mid l u + 1)" u f e] mid_less_u
+         by auto
+       thus ?case using 1
+         apply clarify
+         apply (drule_tac x="(mid l u + 1, u)" in spec, clarify)
+       proof
+         assume as0: "e < f u"
+         assume as1: "u - (mid l u + 1) < u - l \<longrightarrow>
+           (\<forall>x xa.
+           (mid l u + (1\<Colon>nat), u) = (x, xa) \<longrightarrow>
+           e < f xa \<longrightarrow>
+           (\<forall>xa<x. f xa \<le> e) \<longrightarrow>
+           e < f (binsearch f e x xa) \<and>
+           (\<forall>xb<binsearch f e x xa. f xb \<le> e))"
+         have ml: "u - (mid l u + 1) < u - l" using  less mid_less1
+           by (auto)
+         hence "\<forall>x xa.
+           (mid l u + 1, u) = (x, xa) \<longrightarrow>
+           e < f xa \<longrightarrow>
+           (\<forall>xa<x. f xa \<le> e) \<longrightarrow>
+           e < f (binsearch f e x xa) \<and>
+           (\<forall>xb<binsearch f e x xa. f xb \<le> e)" using as1 by safe
+         hence "e < f u \<longrightarrow>
+           (\<forall>xa<mid l u + 1. f xa \<le> e) \<longrightarrow>
+           e < f (binsearch f e (mid l u + 1) u) \<and>
+           (\<forall>xb<binsearch f e (mid l u + 1) u. f xb \<le> e)"
+           by blast
+         hence IH: "e < f (binsearch f e (mid l u + 1) u) \<and>
+           (\<forall>xb<binsearch f e (mid l u + 1) u. f xb \<le> e)"
+           using `e < f u` less_mid_all by auto
+         moreover have f_in_case: "f (binsearch f e l u) =  f
+(binsearch f e (mid l u + 1) u)"
+           using binsearch_in_case by auto
+         thus "e < f (binsearch f e l u)" using IH by simp
+         show "\<forall>x<binsearch f e l u. f x \<le> e" using IH
+binsearch_in_case mono by simp
+       qed
+     next
+       assume le_case: "\<not> f (mid l u) \<le> e"
+       hence le_case_mod: "e < f (mid l u)" by simp
+       have binsearch_in_case: "binsearch f e l u = binsearch f e l (mid l u)"
+         using binsearch.simps[of f e l u] less le_case
+         by (auto)
+       thus ?case using 1
+         apply clarify
+         apply (drule_tac x="(l, mid l u)" in spec, clarify)
+       proof
+         assume as0: "e < f u" "(\<forall>x<l. f x \<le> e)"
+         assume as1: "mid l u - l < u - l \<longrightarrow>
+           (\<forall>x xa.
+           (l, mid l u) = (x, xa) \<longrightarrow>
+           e < f xa \<longrightarrow>
+           (\<forall>xa<x. f xa \<le> e) \<longrightarrow>
+           e < f (binsearch f e x xa) \<and>
+           (\<forall>xb<binsearch f e x xa. f xb \<le> e))"
+         have "mid l u - l < u - l" using less mid_def by auto
+         hence "(\<forall>x xa.
+           (l, mid l u) = (x, xa) \<longrightarrow>
+           e < f xa \<longrightarrow>
+           (\<forall>xa<x. f xa \<le> e) \<longrightarrow>
+           e < f (binsearch f e x xa) \<and>
+           (\<forall>xb<binsearch f e x xa. f xb \<le> e))" using as1 by safe
+         hence "e < f (mid l u) \<longrightarrow>
+           (\<forall>xa<l. f xa \<le> e) \<longrightarrow>
+           e < f (binsearch f e l (mid l u)) \<and>
+           (\<forall>xb<binsearch f e l (mid l u). f xb \<le> e)" by blast
+         hence IH: "e < f (binsearch f e l (mid l u)) \<and>
+           (\<forall>xb<binsearch f e l (mid l u). f xb \<le> e)"
+           using as0 le_case_mod by blast
+         moreover have f_in_case: "f (binsearch f e l u) =  f
+(binsearch f e l (mid l u))"
+           using binsearch_in_case by auto
+         thus "e < f (binsearch f e l u)" using IH by simp
+         show "\<forall>x<binsearch f e l u. f x \<le> e" using IH
+binsearch_in_case mono by simp
+       qed
+     qed
+   qed
+ qed
+qed
+
+export_code * in SML module_name CodegenTest
+  in OCaml module_name CodegenTest file -
+  in Haskell file "~/leg"
+
+end
+