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