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