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: "(\<exists> v. size v \<le> n \<and> is_some (f v)) \<longleftrightarrow> 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) \<le> n \<Longrightarrow> is_some (f v) \<Longrightarrow> 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) \<le> 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
  "(\<exists> i. j <= i & i <= k & is_some (f i)) \<longleftrightarrow> 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 "(\<exists>v. size (v :: int) \<le> n \<and> 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
  "(\<exists>n. j \<le> n \<and> n \<le> k \<and> 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 "(\<exists>n\<ge>j. n \<le> k \<and> 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 "(\<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))"
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 "(\<exists>v. size (v :: nat) \<le> n \<and> is_some (f v)) \<longleftrightarrow> 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 "(\<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))"
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 "\<exists>v. Completeness.size_class.size v \<le> Suc n \<and> is_some (f v)"
wenzelm@47230
   176
      then obtain v where v: "size v \<le> 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' \<le> n"
bulwahn@47205
   186
          and "Completeness.size_class.size vs' \<le> n" by auto
bulwahn@47205
   187
        from Suc v Cons this have "is_some (exhaustive_class.exhaustive (\<lambda>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 (\<lambda>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 "\<exists>v. size v \<le> Suc n \<and> 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 (\<lambda>x. exhaustive_class.exhaustive (\<lambda>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' \<le> n"
wenzelm@47230
   209
              "is_some (exhaustive_class.exhaustive (\<lambda>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' \<le> n" "is_some (f (v' # vs'))"
bulwahn@47205
   213
          by metis
wenzelm@47230
   214
        with v have "size (v' # vs') \<le> 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