# HG changeset patch
# User blanchet
# Date 1405187644 -7200
# Node ID 278ab871319f4642863729f4da6dd4fd09bafefe
# Parent  677b07d777c3caba72c05301c2851e9d864e6c7a# Parent  8840fa17e17c27635846ddc39e67a1cf20cf684a
merge

diff -r 677b07d777c3 -r 278ab871319f src/HOL/Library/Quickcheck_Types.thy
--- a/src/HOL/Library/Quickcheck_Types.thy	Sat Jul 12 11:31:23 2014 +0200
+++ b/src/HOL/Library/Quickcheck_Types.thy	Sat Jul 12 19:54:04 2014 +0200
@@ -4,7 +4,7 @@
 *)
 
 theory Quickcheck_Types
-imports Main
+imports "../Main"
 begin
 
 text {*
@@ -113,8 +113,7 @@
 
 definition "bot = Bot"
 
-instance proof
-qed (simp add: bot_bot_def)
+instance ..
 
 end
 
@@ -123,8 +122,7 @@
 
 definition "top = Value top"
 
-instance proof
-qed (simp add: top_bot_def less_eq_bot_def split: bot.split)
+instance ..
 
 end
 
@@ -152,7 +150,8 @@
 
 end
 
-instance bot :: (lattice) bounded_lattice_bot ..
+instance bot :: (lattice) bounded_lattice_bot
+by(intro_classes)(simp add: bot_bot_def)
 
 section {* Values extended by a top element *}
 
@@ -213,8 +212,7 @@
 
 definition "top = Top"
 
-instance proof
-qed (simp add: top_top_def)
+instance ..
 
 end
 
@@ -223,8 +221,7 @@
 
 definition "bot = Value bot"
 
-instance proof
-qed (simp add: bot_top_def less_eq_top_def split: top.split)
+instance ..
 
 end
 
@@ -252,7 +249,8 @@
 
 end
 
-instance top :: (lattice) bounded_lattice_top ..
+instance top :: (lattice) bounded_lattice_top
+by(intro_classes)(simp add: top_top_def)
 
 
 datatype 'a flat_complete_lattice = Value 'a | Bot | Top
@@ -294,8 +292,7 @@
 
 definition "bot = Bot"
 
-instance proof
-qed (simp add: bot_flat_complete_lattice_def)
+instance ..
 
 end
 
@@ -304,8 +301,7 @@
 
 definition "top = Top"
 
-instance proof
-qed (auto simp add: less_eq_flat_complete_lattice_def top_flat_complete_lattice_def split: flat_complete_lattice.splits)
+instance ..
 
 end
 
@@ -454,13 +450,19 @@
   ultimately show "Sup A <= z"
     unfolding Sup_flat_complete_lattice_def
     by auto
+next
+  show "Inf {} = (top :: 'a flat_complete_lattice)"
+    by(simp add: Inf_flat_complete_lattice_def top_flat_complete_lattice_def)
+next
+  show "Sup {} = (bot :: 'a flat_complete_lattice)"
+    by(simp add: Sup_flat_complete_lattice_def bot_flat_complete_lattice_def)
 qed
 
 end
 
 section {* Quickcheck configuration *}
 
-quickcheck_params[finite_types = false, default_type = ["int", "non_distrib_lattice", "int bot", "int top", "int flat_complete_lattice"]]
+quickcheck_params[finite_types = false, default_type = ["int", "non_distrib_lattice", "int bot", "int top", "Enum.finite_4 flat_complete_lattice"]]
 
 hide_type non_distrib_lattice flat_complete_lattice bot top
 
diff -r 677b07d777c3 -r 278ab871319f src/HOL/Quickcheck_Examples/Completeness.thy
--- a/src/HOL/Quickcheck_Examples/Completeness.thy	Sat Jul 12 11:31:23 2014 +0200
+++ b/src/HOL/Quickcheck_Examples/Completeness.thy	Sat Jul 12 19:54:04 2014 +0200
@@ -6,7 +6,7 @@
 header {* Proving completeness of exhaustive generators *}
 
 theory Completeness
-imports Main
+imports "../Main"
 begin
 
 subsection {* Preliminaries *}
diff -r 677b07d777c3 -r 278ab871319f src/HOL/Quickcheck_Examples/Hotel_Example.thy
--- a/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Sat Jul 12 11:31:23 2014 +0200
+++ b/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Sat Jul 12 19:54:04 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
diff -r 677b07d777c3 -r 278ab871319f src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Sat Jul 12 11:31:23 2014 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Sat Jul 12 19:54:04 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 {*
diff -r 677b07d777c3 -r 278ab871319f src/HOL/ROOT
--- a/src/HOL/ROOT	Sat Jul 12 11:31:23 2014 +0200
+++ b/src/HOL/ROOT	Sat Jul 12 19:54:04 2014 +0200
@@ -52,6 +52,7 @@
     (*legacy tools*)
     Refute
     Old_Recdef
+    Quickcheck_Types
   theories [condition = ISABELLE_FULL_TEST]
     Sum_of_Squares_Remote
   document_files "root.bib" "root.tex"
@@ -883,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