--- a/src/HOL/Quickcheck_Examples/Completeness.thy Fri Feb 15 08:31:30 2013 +0100
+++ b/src/HOL/Quickcheck_Examples/Completeness.thy Fri Feb 15 08:31:31 2013 +0100
@@ -16,6 +16,10 @@
"is_some (Some t) = True"
| "is_some None = False"
+lemma is_some_is_not_None:
+ "is_some x \<longleftrightarrow> x \<noteq> None"
+ by (cases x) simp_all
+
setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *}
subsection {* Defining the size of values *}
@@ -36,12 +40,12 @@
end
-instantiation code_numeral :: size
+instantiation natural :: size
begin
-definition size_code_numeral :: "code_numeral => nat"
+definition size_natural :: "natural => nat"
where
- "size_code_numeral = Code_Numeral.nat_of"
+ "size_natural = nat_of_natural"
instance ..
@@ -74,96 +78,86 @@
class complete = exhaustive + size +
assumes
- complete: "(\<exists> v. size v \<le> n \<and> is_some (f v)) \<longleftrightarrow> is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat n))"
+ complete: "(\<exists> v. size v \<le> n \<and> is_some (f v)) \<longleftrightarrow> is_some (exhaustive_class.exhaustive f (natural_of_nat n))"
lemma complete_imp1:
- "size (v :: 'a :: complete) \<le> n \<Longrightarrow> is_some (f v) \<Longrightarrow> is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat n))"
+ "size (v :: 'a :: complete) \<le> n \<Longrightarrow> is_some (f v) \<Longrightarrow> is_some (exhaustive_class.exhaustive f (natural_of_nat n))"
by (metis complete)
lemma complete_imp2:
- assumes "is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat n))"
+ assumes "is_some (exhaustive_class.exhaustive f (natural_of_nat n))"
obtains v where "size (v :: 'a :: complete) \<le> n" "is_some (f v)"
using assms by (metis complete)
subsubsection {* Instance Proofs *}
-declare exhaustive'.simps [simp del]
+declare exhaustive_int'.simps [simp del]
lemma complete_exhaustive':
- "(\<exists> i. j <= i & i <= k & is_some (f i)) \<longleftrightarrow> is_some (Quickcheck_Exhaustive.exhaustive' f k j)"
-proof (induct rule: Quickcheck_Exhaustive.exhaustive'.induct[of _ f k j])
+ "(\<exists> i. j <= i & i <= k & is_some (f i)) \<longleftrightarrow> 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'.simps[of _ _ i] Quickcheck_Exhaustive.orelse_def
+ unfolding exhaustive_int'.simps[of _ _ i] Quickcheck_Exhaustive.orelse_def
+ apply (auto simp add: add1_zle_eq dest: less_imp_le)
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
+ unfolding exhaustive_int'.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 "(\<exists>v. size (v :: int) \<le> n \<and> is_some (f v)) = is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat n))"
+ show "(\<exists>v. size (v :: int) \<le> n \<and> 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 int_of_nat abs_le_iff minus_le_iff nat_le_iff)+
+ unfolding size_int_def by (metis abs_le_iff minus_le_iff nat_le_iff)+
qed
-declare exhaustive_code_numeral'.simps[simp del]
+declare exhaustive_natural'.simps[simp del]
-lemma complete_code_numeral':
+lemma complete_natural':
"(\<exists>n. j \<le> n \<and> n \<le> k \<and> 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])
+ 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 "(\<exists>n\<ge>j. n \<le> k \<and> 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
+ show "(\<exists>n\<ge>j. n \<le> k \<and> 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 (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)
+ 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 code_numeral :: complete
+instance natural :: complete
proof
fix n f
- show "(\<exists>v. size (v :: code_numeral) \<le> n \<and> is_some (f v)) \<longleftrightarrow> 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)
+ show "(\<exists>v. size (v :: natural) \<le> n \<and> is_some (f v)) \<longleftrightarrow> 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 "(\<exists>v. size (v :: nat) \<le> n \<and> is_some (f v)) \<longleftrightarrow> 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]
+ show "(\<exists>v. size (v :: nat) \<le> n \<and> is_some (f v)) \<longleftrightarrow> 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="Code_Numeral.of_nat v" in exI)
- apply (auto simp add: size_code_numeral_def size_nat_def) done
+ 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 "(\<exists> v. size (v :: 'a list) \<le> n \<and> is_some (f (v :: 'a list))) \<longleftrightarrow> is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat n))"
+ 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))"
proof (induct n arbitrary: f)
case 0
{ fix v have "size (v :: 'a list) > 0" by (induct v) auto }
@@ -174,25 +168,25 @@
proof
assume "\<exists>v. Completeness.size_class.size v \<le> Suc n \<and> is_some (f v)"
then obtain v where v: "size v \<le> Suc n" "is_some (f v)" by blast
- show "is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat (Suc n)))"
+ 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 _ "Code_Numeral.of_nat (Suc n)"] Quickcheck_Exhaustive.orelse_def
- by (auto split: option.split)
+ 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' \<le> n" by auto
- from Suc v Cons this have "is_some (exhaustive_class.exhaustive (\<lambda>xs. f (v' # xs)) (Code_Numeral.of_nat n))"
+ from Suc v Cons this have "is_some (exhaustive_class.exhaustive (\<lambda>xs. f (v' # xs)) (natural_of_nat n))"
by metis
- from complete_imp1[OF size_v', of "%x. (exhaustive_class.exhaustive (\<lambda>xs. f (x # xs)) (Code_Numeral.of_nat n))", OF this]
+ from complete_imp1[OF size_v', of "%x. (exhaustive_class.exhaustive (\<lambda>xs. f (x # xs)) (natural_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)
+ 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 (Code_Numeral.of_nat (Suc n)))"
+ assume is_some: "is_some (exhaustive_class.exhaustive f (natural_of_nat (Suc n)))"
show "\<exists>v. size v \<le> Suc n \<and> is_some (f v)"
proof (cases "f []")
case Some
@@ -201,12 +195,12 @@
next
case None
with is_some have
- "is_some (exhaustive_class.exhaustive (\<lambda>x. exhaustive_class.exhaustive (\<lambda>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
+ "is_some (exhaustive_class.exhaustive (\<lambda>x. exhaustive_class.exhaustive (\<lambda>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' \<le> n"
- "is_some (exhaustive_class.exhaustive (\<lambda>xs. f (v' # xs)) (Code_Numeral.of_nat n))"
+ "is_some (exhaustive_class.exhaustive (\<lambda>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' \<le> n" "is_some (f (v' # vs'))"
@@ -219,3 +213,4 @@
qed
end
+