(* Title: HOL/Quickcheck_Examples/Completeness.thy
Author: Lukas Bulwahn
Copyright 2012 TU Muenchen
*)
section \<open>Proving completeness of exhaustive generators\<close>
theory Completeness
imports Main
begin
subsection \<open>Preliminaries\<close>
primrec is_some
where
"is_some (Some t) = True"
| "is_some None = False"
lemma is_some_is_not_None:
"is_some x \ x \ None"
by (cases x) simp_all
setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation
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 ?case by (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)"
then obtain 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
then show ?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)
then obtain 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
end
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|
