src/HOL/Quickcheck_Examples/Completeness.thy
 author huffman Sun Apr 01 16:09:58 2012 +0200 (2012-04-01) changeset 47255 30a1692557b0 parent 47230 6584098d5378 child 51143 0a2371e7ced3 permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
 bulwahn@47205 1 (* Title: HOL/Quickcheck_Examples/Completeness.thy bulwahn@47205 2 Author: Lukas Bulwahn bulwahn@47205 3 Copyright 2012 TU Muenchen bulwahn@47205 4 *) bulwahn@47205 5 bulwahn@47205 6 header {* Proving completeness of exhaustive generators *} bulwahn@47205 7 bulwahn@47205 8 theory Completeness bulwahn@47205 9 imports Main bulwahn@47205 10 begin bulwahn@47205 11 bulwahn@47205 12 subsection {* Preliminaries *} bulwahn@47205 13 bulwahn@47205 14 primrec is_some bulwahn@47205 15 where bulwahn@47205 16 "is_some (Some t) = True" bulwahn@47205 17 | "is_some None = False" bulwahn@47205 18 bulwahn@47205 19 setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *} bulwahn@47205 20 bulwahn@47205 21 subsection {* Defining the size of values *} bulwahn@47205 22 bulwahn@47205 23 hide_const size bulwahn@47205 24 bulwahn@47205 25 class size = bulwahn@47205 26 fixes size :: "'a => nat" bulwahn@47205 27 bulwahn@47205 28 instantiation int :: size bulwahn@47205 29 begin bulwahn@47205 30 bulwahn@47205 31 definition size_int :: "int => nat" bulwahn@47205 32 where bulwahn@47205 33 "size_int n = nat (abs n)" bulwahn@47205 34 bulwahn@47205 35 instance .. bulwahn@47205 36 bulwahn@47205 37 end bulwahn@47205 38 bulwahn@47205 39 instantiation code_numeral :: size bulwahn@47205 40 begin bulwahn@47205 41 bulwahn@47205 42 definition size_code_numeral :: "code_numeral => nat" bulwahn@47205 43 where bulwahn@47205 44 "size_code_numeral = Code_Numeral.nat_of" bulwahn@47205 45 bulwahn@47205 46 instance .. bulwahn@47205 47 bulwahn@47205 48 end bulwahn@47205 49 bulwahn@47205 50 instantiation nat :: size bulwahn@47205 51 begin bulwahn@47205 52 bulwahn@47205 53 definition size_nat :: "nat => nat" bulwahn@47205 54 where bulwahn@47205 55 "size_nat n = n" bulwahn@47205 56 bulwahn@47205 57 instance .. bulwahn@47205 58 bulwahn@47205 59 end bulwahn@47205 60 bulwahn@47205 61 instantiation list :: (size) size bulwahn@47205 62 begin bulwahn@47205 63 bulwahn@47205 64 primrec size_list :: "'a list => nat" bulwahn@47205 65 where bulwahn@47205 66 "size [] = 1" bulwahn@47205 67 | "size (x # xs) = max (size x) (size xs) + 1" bulwahn@47205 68 bulwahn@47205 69 instance .. bulwahn@47205 70 bulwahn@47205 71 end bulwahn@47205 72 bulwahn@47205 73 subsection {* Completeness *} bulwahn@47205 74 bulwahn@47205 75 class complete = exhaustive + size + bulwahn@47205 76 assumes bulwahn@47205 77 complete: "(\ v. size v \ n \ is_some (f v)) \ is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat n))" bulwahn@47205 78 bulwahn@47205 79 lemma complete_imp1: bulwahn@47205 80 "size (v :: 'a :: complete) \ n \ is_some (f v) \ is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat n))" bulwahn@47205 81 by (metis complete) bulwahn@47205 82 bulwahn@47205 83 lemma complete_imp2: bulwahn@47205 84 assumes "is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat n))" bulwahn@47205 85 obtains v where "size (v :: 'a :: complete) \ n" "is_some (f v)" bulwahn@47205 86 using assms by (metis complete) bulwahn@47205 87 bulwahn@47205 88 subsubsection {* Instance Proofs *} bulwahn@47205 89 bulwahn@47205 90 declare exhaustive'.simps [simp del] bulwahn@47205 91 bulwahn@47205 92 lemma complete_exhaustive': bulwahn@47205 93 "(\ i. j <= i & i <= k & is_some (f i)) \ is_some (Quickcheck_Exhaustive.exhaustive' f k j)" bulwahn@47205 94 proof (induct rule: Quickcheck_Exhaustive.exhaustive'.induct[of _ f k j]) bulwahn@47205 95 case (1 f d i) bulwahn@47205 96 show ?case bulwahn@47205 97 proof (cases "f i") bulwahn@47205 98 case None bulwahn@47205 99 from this 1 show ?thesis bulwahn@47205 100 unfolding exhaustive'.simps[of _ _ i] Quickcheck_Exhaustive.orelse_def bulwahn@47205 101 apply auto bulwahn@47205 102 apply (metis is_some.simps(2) order_le_neq_trans zless_imp_add1_zle) bulwahn@47205 103 apply (metis add1_zle_eq less_int_def) bulwahn@47205 104 done bulwahn@47205 105 next bulwahn@47205 106 case Some bulwahn@47205 107 from this show ?thesis bulwahn@47205 108 unfolding exhaustive'.simps[of _ _ i] Quickcheck_Exhaustive.orelse_def by auto bulwahn@47205 109 qed bulwahn@47205 110 qed bulwahn@47205 111 bulwahn@47205 112 lemma int_of_nat: bulwahn@47205 113 "Code_Numeral.int_of (Code_Numeral.of_nat n) = int n" bulwahn@47205 114 unfolding int_of_def by simp bulwahn@47205 115 bulwahn@47205 116 instance int :: complete bulwahn@47205 117 proof bulwahn@47205 118 fix n f bulwahn@47205 119 show "(\v. size (v :: int) \ n \ is_some (f v)) = is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat n))" bulwahn@47205 120 unfolding exhaustive_int_def complete_exhaustive'[symmetric] bulwahn@47205 121 apply auto apply (rule_tac x="v" in exI) bulwahn@47205 122 unfolding size_int_def by (metis int_of_nat abs_le_iff minus_le_iff nat_le_iff)+ bulwahn@47205 123 qed bulwahn@47205 124 bulwahn@47205 125 declare exhaustive_code_numeral'.simps[simp del] bulwahn@47205 126 bulwahn@47205 127 lemma complete_code_numeral': bulwahn@47205 128 "(\n. j \ n \ n \ k \ is_some (f n)) = bulwahn@47205 129 is_some (Quickcheck_Exhaustive.exhaustive_code_numeral' f k j)" bulwahn@47205 130 proof (induct rule: exhaustive_code_numeral'.induct[of _ f k j]) bulwahn@47205 131 case (1 f k j) bulwahn@47205 132 show "(\n\j. n \ k \ is_some (f n)) = is_some (Quickcheck_Exhaustive.exhaustive_code_numeral' f k j)" bulwahn@47205 133 unfolding exhaustive_code_numeral'.simps[of f k j] Quickcheck_Exhaustive.orelse_def bulwahn@47205 134 apply auto bulwahn@47205 135 apply (auto split: option.split) bulwahn@47205 136 apply (insert 1[symmetric]) bulwahn@47205 137 apply simp bulwahn@47205 138 apply (metis is_some.simps(2) less_eq_code_numeral_def not_less_eq_eq order_antisym) bulwahn@47205 139 apply simp bulwahn@47205 140 apply (split option.split_asm) bulwahn@47205 141 defer apply fastforce bulwahn@47205 142 apply simp by (metis Suc_leD) bulwahn@47205 143 qed bulwahn@47205 144 bulwahn@47205 145 instance code_numeral :: complete bulwahn@47205 146 proof bulwahn@47205 147 fix n f bulwahn@47205 148 show "(\v. size (v :: code_numeral) \ n \ is_some (f v)) \ is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat n))" bulwahn@47205 149 unfolding exhaustive_code_numeral_def complete_code_numeral'[symmetric] bulwahn@47205 150 by (auto simp add: size_code_numeral_def) bulwahn@47205 151 qed bulwahn@47205 152 bulwahn@47205 153 instance nat :: complete bulwahn@47205 154 proof bulwahn@47205 155 fix n f bulwahn@47205 156 show "(\v. size (v :: nat) \ n \ is_some (f v)) \ is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat n))" bulwahn@47205 157 unfolding exhaustive_nat_def complete[of n "%x. f (Code_Numeral.nat_of x)", symmetric] bulwahn@47205 158 apply auto bulwahn@47205 159 apply (rule_tac x="Code_Numeral.of_nat v" in exI) bulwahn@47205 160 apply (auto simp add: size_code_numeral_def size_nat_def) done bulwahn@47205 161 qed bulwahn@47205 162 bulwahn@47205 163 instance list :: (complete) complete bulwahn@47205 164 proof bulwahn@47205 165 fix n f bulwahn@47205 166 show "(\ v. size (v :: 'a list) \ n \ is_some (f (v :: 'a list))) \ is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat n))" bulwahn@47205 167 proof (induct n arbitrary: f) bulwahn@47205 168 case 0 bulwahn@47205 169 { fix v have "size (v :: 'a list) > 0" by (induct v) auto } bulwahn@47205 170 from this show ?case by (simp add: list.exhaustive_list.simps) bulwahn@47205 171 next bulwahn@47205 172 case (Suc n) bulwahn@47205 173 show ?case bulwahn@47205 174 proof bulwahn@47205 175 assume "\v. Completeness.size_class.size v \ Suc n \ is_some (f v)" wenzelm@47230 176 then obtain v where v: "size v \ Suc n" "is_some (f v)" by blast bulwahn@47205 177 show "is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat (Suc n)))" bulwahn@47205 178 proof (cases "v") bulwahn@47205 179 case Nil bulwahn@47205 180 from this v show ?thesis bulwahn@47205 181 unfolding list.exhaustive_list.simps[of _ "Code_Numeral.of_nat (Suc n)"] Quickcheck_Exhaustive.orelse_def bulwahn@47205 182 by (auto split: option.split) bulwahn@47205 183 next bulwahn@47205 184 case (Cons v' vs') bulwahn@47205 185 from Cons v have size_v': "Completeness.size_class.size v' \ n" bulwahn@47205 186 and "Completeness.size_class.size vs' \ n" by auto bulwahn@47205 187 from Suc v Cons this have "is_some (exhaustive_class.exhaustive (\xs. f (v' # xs)) (Code_Numeral.of_nat n))" bulwahn@47205 188 by metis bulwahn@47205 189 from complete_imp1[OF size_v', of "%x. (exhaustive_class.exhaustive (\xs. f (x # xs)) (Code_Numeral.of_nat n))", OF this] bulwahn@47205 190 show ?thesis bulwahn@47205 191 unfolding list.exhaustive_list.simps[of _ "Code_Numeral.of_nat (Suc n)"] Quickcheck_Exhaustive.orelse_def bulwahn@47205 192 by (auto split: option.split) bulwahn@47205 193 qed bulwahn@47205 194 next bulwahn@47205 195 assume is_some: "is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat (Suc n)))" bulwahn@47205 196 show "\v. size v \ Suc n \ is_some (f v)" bulwahn@47205 197 proof (cases "f []") bulwahn@47205 198 case Some wenzelm@47230 199 then show ?thesis bulwahn@47205 200 by (metis Suc_eq_plus1 is_some.simps(1) le_add2 size_list.simps(1)) bulwahn@47205 201 next bulwahn@47205 202 case None wenzelm@47230 203 with is_some have bulwahn@47205 204 "is_some (exhaustive_class.exhaustive (\x. exhaustive_class.exhaustive (\xs. f (x # xs)) (Code_Numeral.of_nat n)) (Code_Numeral.of_nat n))" bulwahn@47205 205 unfolding list.exhaustive_list.simps[of _ "Code_Numeral.of_nat (Suc n)"] Quickcheck_Exhaustive.orelse_def bulwahn@47205 206 by simp wenzelm@47230 207 then obtain v' where wenzelm@47230 208 v: "size v' \ n" wenzelm@47230 209 "is_some (exhaustive_class.exhaustive (\xs. f (v' # xs)) (Code_Numeral.of_nat n))" wenzelm@47230 210 by (rule complete_imp2) wenzelm@47230 211 with Suc[of "%xs. f (v' # xs)"] wenzelm@47230 212 obtain vs' where vs': "size vs' \ n" "is_some (f (v' # vs'))" bulwahn@47205 213 by metis wenzelm@47230 214 with v have "size (v' # vs') \ Suc n" by auto wenzelm@47230 215 with vs' v show ?thesis by metis bulwahn@47205 216 qed bulwahn@47205 217 qed bulwahn@47205 218 qed bulwahn@47205 219 qed bulwahn@47205 220 bulwahn@47205 221 end