src/HOL/Quickcheck_Examples/Completeness.thy
author paulson <lp15@cam.ac.uk>
Tue Apr 25 16:39:54 2017 +0100 (2017-04-25)
changeset 65578 e4997c181cce
parent 63167 0909deb8059b
permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
     1 (*  Title:      HOL/Quickcheck_Examples/Completeness.thy
     2     Author:     Lukas Bulwahn
     3     Copyright   2012 TU Muenchen
     4 *)
     5 
     6 section \<open>Proving completeness of exhaustive generators\<close>
     7 
     8 theory Completeness
     9 imports Main
    10 begin
    11 
    12 subsection \<open>Preliminaries\<close>
    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 \<open>Defining the size of values\<close>
    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 \<open>Completeness\<close>
    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 \<open>Instance Proofs\<close>
    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