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