subsection \<open>Defining the size of values\<close>
hide_const size
class size = fixes size :: "'a => nat"
instantiation int :: size begin
definition size_int :: "int => nat" where "size_int n = nat (abs n)"
instance ..
end
instantiation natural :: size begin
definition size_natural :: "natural => nat" where "size_natural = nat_of_natural"
instance ..
end
instantiation nat :: size begin
definition size_nat :: "nat => nat" where "size_nat n = n"
instance ..
end
instantiation list :: (size) size begin
primrec size_list :: "'a list => nat" where "size [] = 1"
| "size (x # xs) = max (size x) (size xs) + 1"
instance ..
end
subsection \<open>Completeness\<close>
class complete = exhaustive + size + assumes
complete: "(\ v. size v \ n \ is_some (f v)) \ is_some (exhaustive_class.exhaustive f (natural_of_nat n))"
lemma complete_imp1: "size (v :: 'a :: complete) \ n \ is_some (f v) \ is_some (exhaustive_class.exhaustive f (natural_of_nat n))" by (metis complete)
lemma complete_imp2: assumes"is_some (exhaustive_class.exhaustive f (natural_of_nat n))" obtains v where"size (v :: 'a :: complete) \ n" "is_some (f v)" using assms by (metis complete)
subsubsection \<open>Instance Proofs\<close>
declare exhaustive_int'.simps [simp del]
lemma complete_exhaustive': "(\ i. j <= i & i <= k & is_some (f i)) \ is_some (Quickcheck_Exhaustive.exhaustive_int' f k j)" proof (induct rule: Quickcheck_Exhaustive.exhaustive_int'.induct[of _ f k j]) case (1 f d i) show ?case proof (cases "f i") case None from this 1 show ?thesis unfolding exhaustive_int'.simps[of _ _ i] Quickcheck_Exhaustive.orelse_def apply (auto simp add: add1_zle_eq dest: less_imp_le) apply auto done next case Some from this show ?thesis unfolding exhaustive_int'.simps[of _ _ i] Quickcheck_Exhaustive.orelse_def by auto qed qed
instance int :: complete proof fix n f show"(\v. size (v :: int) \ n \ is_some (f v)) = is_some (exhaustive_class.exhaustive f (natural_of_nat n))" unfolding exhaustive_int_def complete_exhaustive'[symmetric] apply auto apply (rule_tac x="v"in exI) unfolding size_int_def by (metis abs_le_iff minus_le_iff nat_le_iff)+ qed
declare exhaustive_natural'.simps[simp del]
lemma complete_natural': "(\n. j \ n \ n \ k \ is_some (f n)) =
is_some (Quickcheck_Exhaustive.exhaustive_natural' f k j)" proof (induct rule: exhaustive_natural'.induct[of _ f k j]) case (1 f k j) show"(\n\j. n \ k \ is_some (f n)) = is_some (Quickcheck_Exhaustive.exhaustive_natural' f k j)" unfolding exhaustive_natural'.simps [of f k j] Quickcheck_Exhaustive.orelse_def apply (auto split: option.split) apply (auto simp add: less_eq_natural_def less_natural_def 1 [symmetric] dest: Suc_leD) apply (metis is_some.simps(2) natural_eqI not_less_eq_eq order_antisym) done qed
instance natural :: complete proof fix n f show"(\v. size (v :: natural) \ n \ is_some (f v)) \ is_some (exhaustive_class.exhaustive f (natural_of_nat n))" unfolding exhaustive_natural_def complete_natural' [symmetric] by (auto simp add: size_natural_def less_eq_natural_def) qed
instance nat :: complete proof fix n f show"(\v. size (v :: nat) \ n \ is_some (f v)) \ is_some (exhaustive_class.exhaustive f (natural_of_nat n))" unfolding exhaustive_nat_def complete[of n "%x. f (nat_of_natural x)", symmetric] apply auto apply (rule_tac x="natural_of_nat v"in exI) apply (auto simp add: size_natural_def size_nat_def) done qed
instance list :: (complete) complete proof fix n f show"(\ v. size (v :: 'a list) \ n \ is_some (f (v :: 'a list))) \ is_some (exhaustive_class.exhaustive f (natural_of_nat n))" proof (induct n arbitrary: f) case 0
{ fix v have"size (v :: 'a list) > 0"by (induct v) auto } from this show ?caseby (simp add: list.exhaustive_list.simps) next case (Suc n) show ?case proof assume"\v. Completeness.size_class.size v \ Suc n \ is_some (f v)" thenobtain v where v: "size v \ Suc n" "is_some (f v)" by blast show"is_some (exhaustive_class.exhaustive f (natural_of_nat (Suc n)))" proof (cases "v") case Nil from this v show ?thesis unfolding list.exhaustive_list.simps[of _ "natural_of_nat (Suc n)"] Quickcheck_Exhaustive.orelse_def by (auto split: option.split simp add: less_natural_def) next case (Cons v' vs') from Cons v have size_v': "Completeness.size_class.size v'\<le> n" and"Completeness.size_class.size vs' \ n" by auto from Suc v Cons this have"is_some (exhaustive_class.exhaustive (\xs. f (v' # xs)) (natural_of_nat n))" by metis from complete_imp1[OF size_v', of "%x. (exhaustive_class.exhaustive (\xs. f (x # xs)) (natural_of_nat n))", OF this] show ?thesis unfolding list.exhaustive_list.simps[of _ "natural_of_nat (Suc n)"] Quickcheck_Exhaustive.orelse_def by (auto split: option.split simp add: less_natural_def) qed next assume is_some: "is_some (exhaustive_class.exhaustive f (natural_of_nat (Suc n)))" show"\v. size v \ Suc n \ is_some (f v)" proof (cases "f []") case Some thenshow ?thesis by (metis Suc_eq_plus1 is_some.simps(1) le_add2 size_list.simps(1)) next case None with is_some have "is_some (exhaustive_class.exhaustive (\x. exhaustive_class.exhaustive (\xs. f (x # xs)) (natural_of_nat n)) (natural_of_nat n))" unfolding list.exhaustive_list.simps[of _ "natural_of_nat (Suc n)"] Quickcheck_Exhaustive.orelse_def by (simp add: less_natural_def) thenobtain v' where
v: "size v' \ n" "is_some (exhaustive_class.exhaustive (\xs. f (v' # xs)) (natural_of_nat n))" by (rule complete_imp2) with Suc[of "%xs. f (v' # xs)"] obtain vs' where vs': "size vs' \ n" "is_some (f (v' # vs'))" by metis with v have"size (v' # vs') \ Suc n" by auto with vs' v show ?thesis by metis qed qed qed qed
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
