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