--- a/src/HOL/Library/Quickcheck_Types.thy Fri Jul 11 15:35:11 2014 +0200
+++ b/src/HOL/Library/Quickcheck_Types.thy Fri Jul 11 15:52:03 2014 +0200
@@ -466,12 +466,4 @@
hide_type non_distrib_lattice flat_complete_lattice bot top
-lemma "\<lbrakk> inf x z = inf y z; sup x z = sup y z \<rbrakk> \<Longrightarrow> x = y"
-quickcheck[exhaustive, expect=counterexample]
-oops
-
-lemma "Inf {} = bot"
-quickcheck[exhaustive, expect=counterexample]
-oops
-
end
\ No newline at end of file
--- a/src/HOL/Quickcheck_Examples/Completeness.thy Fri Jul 11 15:35:11 2014 +0200
+++ b/src/HOL/Quickcheck_Examples/Completeness.thy Fri Jul 11 15:52:03 2014 +0200
@@ -6,7 +6,7 @@
header {* Proving completeness of exhaustive generators *}
theory Completeness
-imports Main
+imports "../Main"
begin
subsection {* Preliminaries *}
--- a/src/HOL/Quickcheck_Examples/Hotel_Example.thy Fri Jul 11 15:35:11 2014 +0200
+++ b/src/HOL/Quickcheck_Examples/Hotel_Example.thy Fri Jul 11 15:52:03 2014 +0200
@@ -99,30 +99,20 @@
"find_first f [] = None"
| "find_first f (x # xs) = (case f x of Some y => Some y | None => find_first f xs)"
-consts cps_of_set :: "'a set => ('a => term list option) => term list option"
-
-lemma
- [code]: "cps_of_set (set xs) f = find_first f xs"
-sorry
-
-consts pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => natural => (bool * term list) option"
-consts neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => natural => term list Quickcheck_Exhaustive.three_valued"
+axiomatization cps_of_set :: "'a set => ('a => term list option) => term list option"
+where cps_of_set_code [code]: "cps_of_set (set xs) f = find_first f xs"
-lemma
- [code]: "pos_cps_of_set (set xs) f i = find_first f xs"
-sorry
+axiomatization pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => natural => (bool * term list) option"
+where pos_cps_of_set_code [code]: "pos_cps_of_set (set xs) f i = find_first f xs"
-consts find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued)
+axiomatization find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued)
=> 'b list => 'a Quickcheck_Exhaustive.three_valued"
-
-lemma [code]:
+where find_first'_code [code]:
"find_first' f [] = Quickcheck_Exhaustive.No_value"
"find_first' f (x # xs) = (case f (Quickcheck_Exhaustive.Known x) of Quickcheck_Exhaustive.No_value => find_first' f xs | Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | Quickcheck_Exhaustive.Unknown_value => (case find_first' f xs of Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | _ => Quickcheck_Exhaustive.Unknown_value))"
-sorry
-lemma
- [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"
-sorry
+axiomatization neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => natural => term list Quickcheck_Exhaustive.three_valued"
+where neg_cps_of_set_code [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"
setup {*
let
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Fri Jul 11 15:35:11 2014 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Fri Jul 11 15:52:03 2014 +0200
@@ -6,7 +6,7 @@
header {* Examples for the 'quickcheck' command *}
theory Quickcheck_Examples
-imports Complex_Main "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/DAList_Multiset"
+imports "../Complex_Main" "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/DAList_Multiset"
begin
text {*
--- a/src/HOL/ROOT Fri Jul 11 15:35:11 2014 +0200
+++ b/src/HOL/ROOT Fri Jul 11 15:52:03 2014 +0200
@@ -884,11 +884,10 @@
options [document = false]
theories
Quickcheck_Examples
- (* FIXME
Quickcheck_Lattice_Examples
Completeness
Quickcheck_Interfaces
- Hotel_Example *)
+ Hotel_Example
theories [condition = ISABELLE_GHC]
Quickcheck_Narrowing_Examples