# HG changeset patch # User bulwahn # Date 1333089841 -7200 # Node ID 34e8b7347ddae5904e386ba9f21d58cde130a14f # Parent 6212bcc94bb08ca2ddb9004af734831127da93bb adding theory to prove completeness of the exhaustive generators diff -r 6212bcc94bb0 -r 34e8b7347dda src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Mar 30 08:19:31 2012 +0200 +++ b/src/HOL/IsaMakefile Fri Mar 30 08:44:01 2012 +0200 @@ -1605,6 +1605,7 @@ HOL-Quickcheck_Examples: HOL $(LOG)/HOL-Quickcheck_Examples.gz $(LOG)/HOL-Quickcheck_Examples.gz: $(OUT)/HOL \ + Quickcheck_Examples/Completeness.thy \ Quickcheck_Examples/Find_Unused_Assms_Examples.thy \ Quickcheck_Examples/Quickcheck_Examples.thy \ Quickcheck_Examples/Quickcheck_Lattice_Examples.thy \ diff -r 6212bcc94bb0 -r 34e8b7347dda src/HOL/Quickcheck_Examples/Completeness.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Quickcheck_Examples/Completeness.thy Fri Mar 30 08:44:01 2012 +0200 @@ -0,0 +1,218 @@ +(* Title: HOL/Quickcheck_Examples/Completeness.thy + Author: Lukas Bulwahn + Copyright 2012 TU Muenchen +*) + +header {* Proving completeness of exhaustive generators *} + +theory Completeness +imports Main +begin + +subsection {* Preliminaries *} + +primrec is_some +where + "is_some (Some t) = True" +| "is_some None = False" + +setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *} + +subsection {* Defining the size of values *} + +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 code_numeral :: size +begin + +definition size_code_numeral :: "code_numeral => nat" +where + "size_code_numeral = Code_Numeral.nat_of" + +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 {* Completeness *} + +class complete = exhaustive + size + +assumes + complete: "(\ v. size v \ n \ is_some (f v)) \ is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat n))" + +lemma complete_imp1: + "size (v :: 'a :: complete) \ n \ is_some (f v) \ is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat n))" +by (metis complete) + +lemma complete_imp2: + assumes "is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat n))" + obtains v where "size (v :: 'a :: complete) \ n" "is_some (f v)" +using assms by (metis complete) + +subsubsection {* Instance Proofs *} + +declare exhaustive'.simps [simp del] + +lemma complete_exhaustive': + "(\ i. j <= i & i <= k & is_some (f i)) \ is_some (Quickcheck_Exhaustive.exhaustive' f k j)" +proof (induct rule: Quickcheck_Exhaustive.exhaustive'.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'.simps[of _ _ i] Quickcheck_Exhaustive.orelse_def + apply auto + apply (metis is_some.simps(2) order_le_neq_trans zless_imp_add1_zle) + apply (metis add1_zle_eq less_int_def) + done + next + case Some + from this show ?thesis + unfolding exhaustive'.simps[of _ _ i] Quickcheck_Exhaustive.orelse_def by auto + qed +qed + +lemma int_of_nat: + "Code_Numeral.int_of (Code_Numeral.of_nat n) = int n" +unfolding int_of_def by simp + +instance int :: complete +proof + fix n f + show "(\v. size (v :: int) \ n \ is_some (f v)) = is_some (exhaustive_class.exhaustive f (Code_Numeral.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 int_of_nat abs_le_iff minus_le_iff nat_le_iff)+ +qed + +declare exhaustive_code_numeral'.simps[simp del] + +lemma complete_code_numeral': + "(\n. j \ n \ n \ k \ is_some (f n)) = + is_some (Quickcheck_Exhaustive.exhaustive_code_numeral' f k j)" +proof (induct rule: exhaustive_code_numeral'.induct[of _ f k j]) + case (1 f k j) + show "(\n\j. n \ k \ is_some (f n)) = is_some (Quickcheck_Exhaustive.exhaustive_code_numeral' f k j)" + unfolding exhaustive_code_numeral'.simps[of f k j] Quickcheck_Exhaustive.orelse_def + apply auto + apply (auto split: option.split) + apply (insert 1[symmetric]) + apply simp + apply (metis is_some.simps(2) less_eq_code_numeral_def not_less_eq_eq order_antisym) + apply simp + apply (split option.split_asm) + defer apply fastforce + apply simp by (metis Suc_leD) +qed + +instance code_numeral :: complete +proof + fix n f + show "(\v. size (v :: code_numeral) \ n \ is_some (f v)) \ is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat n))" + unfolding exhaustive_code_numeral_def complete_code_numeral'[symmetric] + by (auto simp add: size_code_numeral_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 (Code_Numeral.of_nat n))" + unfolding exhaustive_nat_def complete[of n "%x. f (Code_Numeral.nat_of x)", symmetric] + apply auto + apply (rule_tac x="Code_Numeral.of_nat v" in exI) + apply (auto simp add: size_code_numeral_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 (Code_Numeral.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)" + from this guess v .. note v = this + show "is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat (Suc n)))" + proof (cases "v") + case Nil + from this v show ?thesis + unfolding list.exhaustive_list.simps[of _ "Code_Numeral.of_nat (Suc n)"] Quickcheck_Exhaustive.orelse_def + by (auto split: option.split) + next + case (Cons v' vs') + from Cons v have size_v': "Completeness.size_class.size v' \ 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)) (Code_Numeral.of_nat n))" + by metis + from complete_imp1[OF size_v', of "%x. (exhaustive_class.exhaustive (\xs. f (x # xs)) (Code_Numeral.of_nat n))", OF this] + show ?thesis + unfolding list.exhaustive_list.simps[of _ "Code_Numeral.of_nat (Suc n)"] Quickcheck_Exhaustive.orelse_def + by (auto split: option.split) + qed + next + assume is_some: "is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat (Suc n)))" + show "\v. size v \ Suc n \ is_some (f v)" + proof (cases "f []") + case Some + from this show ?thesis + by (metis Suc_eq_plus1 is_some.simps(1) le_add2 size_list.simps(1)) + next + case None + from this is_some have + "is_some (exhaustive_class.exhaustive (\x. exhaustive_class.exhaustive (\xs. f (x # xs)) (Code_Numeral.of_nat n)) (Code_Numeral.of_nat n))" + unfolding list.exhaustive_list.simps[of _ "Code_Numeral.of_nat (Suc n)"] Quickcheck_Exhaustive.orelse_def + by simp + from complete_imp2[OF this] guess v' . note v = this + from Suc[of "%xs. f (v' # xs)"] this(2) obtain vs' where "size vs' \ n" "is_some (f (v' # vs'))" + by metis + note vs' = this + from this v have "size (v' # vs') \ Suc n" by auto + from this vs' v show ?thesis by metis + qed + qed + qed +qed + +end diff -r 6212bcc94bb0 -r 34e8b7347dda src/HOL/Quickcheck_Examples/ROOT.ML --- a/src/HOL/Quickcheck_Examples/ROOT.ML Fri Mar 30 08:19:31 2012 +0200 +++ b/src/HOL/Quickcheck_Examples/ROOT.ML Fri Mar 30 08:44:01 2012 +0200 @@ -1,7 +1,8 @@ use_thys [ "Find_Unused_Assms_Examples", "Quickcheck_Examples", - "Quickcheck_Lattice_Examples" + "Quickcheck_Lattice_Examples", + "Completeness" ]; if getenv "ISABELLE_GHC" = "" then ()