1.1 --- a/src/HOL/Library/Quickcheck_Types.thy Sat Jul 12 11:31:23 2014 +0200
1.2 +++ b/src/HOL/Library/Quickcheck_Types.thy Sat Jul 12 19:54:04 2014 +0200
1.3 @@ -4,7 +4,7 @@
1.4 *)
1.5
1.6 theory Quickcheck_Types
1.7 -imports Main
1.8 +imports "../Main"
1.9 begin
1.10
1.11 text {*
1.12 @@ -113,8 +113,7 @@
1.13
1.14 definition "bot = Bot"
1.15
1.16 -instance proof
1.17 -qed (simp add: bot_bot_def)
1.18 +instance ..
1.19
1.20 end
1.21
1.22 @@ -123,8 +122,7 @@
1.23
1.24 definition "top = Value top"
1.25
1.26 -instance proof
1.27 -qed (simp add: top_bot_def less_eq_bot_def split: bot.split)
1.28 +instance ..
1.29
1.30 end
1.31
1.32 @@ -152,7 +150,8 @@
1.33
1.34 end
1.35
1.36 -instance bot :: (lattice) bounded_lattice_bot ..
1.37 +instance bot :: (lattice) bounded_lattice_bot
1.38 +by(intro_classes)(simp add: bot_bot_def)
1.39
1.40 section {* Values extended by a top element *}
1.41
1.42 @@ -213,8 +212,7 @@
1.43
1.44 definition "top = Top"
1.45
1.46 -instance proof
1.47 -qed (simp add: top_top_def)
1.48 +instance ..
1.49
1.50 end
1.51
1.52 @@ -223,8 +221,7 @@
1.53
1.54 definition "bot = Value bot"
1.55
1.56 -instance proof
1.57 -qed (simp add: bot_top_def less_eq_top_def split: top.split)
1.58 +instance ..
1.59
1.60 end
1.61
1.62 @@ -252,7 +249,8 @@
1.63
1.64 end
1.65
1.66 -instance top :: (lattice) bounded_lattice_top ..
1.67 +instance top :: (lattice) bounded_lattice_top
1.68 +by(intro_classes)(simp add: top_top_def)
1.69
1.70
1.71 datatype 'a flat_complete_lattice = Value 'a | Bot | Top
1.72 @@ -294,8 +292,7 @@
1.73
1.74 definition "bot = Bot"
1.75
1.76 -instance proof
1.77 -qed (simp add: bot_flat_complete_lattice_def)
1.78 +instance ..
1.79
1.80 end
1.81
1.82 @@ -304,8 +301,7 @@
1.83
1.84 definition "top = Top"
1.85
1.86 -instance proof
1.87 -qed (auto simp add: less_eq_flat_complete_lattice_def top_flat_complete_lattice_def split: flat_complete_lattice.splits)
1.88 +instance ..
1.89
1.90 end
1.91
1.92 @@ -454,13 +450,19 @@
1.93 ultimately show "Sup A <= z"
1.94 unfolding Sup_flat_complete_lattice_def
1.95 by auto
1.96 +next
1.97 + show "Inf {} = (top :: 'a flat_complete_lattice)"
1.98 + by(simp add: Inf_flat_complete_lattice_def top_flat_complete_lattice_def)
1.99 +next
1.100 + show "Sup {} = (bot :: 'a flat_complete_lattice)"
1.101 + by(simp add: Sup_flat_complete_lattice_def bot_flat_complete_lattice_def)
1.102 qed
1.103
1.104 end
1.105
1.106 section {* Quickcheck configuration *}
1.107
1.108 -quickcheck_params[finite_types = false, default_type = ["int", "non_distrib_lattice", "int bot", "int top", "int flat_complete_lattice"]]
1.109 +quickcheck_params[finite_types = false, default_type = ["int", "non_distrib_lattice", "int bot", "int top", "Enum.finite_4 flat_complete_lattice"]]
1.110
1.111 hide_type non_distrib_lattice flat_complete_lattice bot top
1.112
2.1 --- a/src/HOL/Quickcheck_Examples/Completeness.thy Sat Jul 12 11:31:23 2014 +0200
2.2 +++ b/src/HOL/Quickcheck_Examples/Completeness.thy Sat Jul 12 19:54:04 2014 +0200
2.3 @@ -6,7 +6,7 @@
2.4 header {* Proving completeness of exhaustive generators *}
2.5
2.6 theory Completeness
2.7 -imports Main
2.8 +imports "../Main"
2.9 begin
2.10
2.11 subsection {* Preliminaries *}
3.1 --- a/src/HOL/Quickcheck_Examples/Hotel_Example.thy Sat Jul 12 11:31:23 2014 +0200
3.2 +++ b/src/HOL/Quickcheck_Examples/Hotel_Example.thy Sat Jul 12 19:54:04 2014 +0200
3.3 @@ -99,30 +99,20 @@
3.4 "find_first f [] = None"
3.5 | "find_first f (x # xs) = (case f x of Some y => Some y | None => find_first f xs)"
3.6
3.7 -consts cps_of_set :: "'a set => ('a => term list option) => term list option"
3.8 +axiomatization cps_of_set :: "'a set => ('a => term list option) => term list option"
3.9 +where cps_of_set_code [code]: "cps_of_set (set xs) f = find_first f xs"
3.10
3.11 -lemma
3.12 - [code]: "cps_of_set (set xs) f = find_first f xs"
3.13 -sorry
3.14 +axiomatization pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => natural => (bool * term list) option"
3.15 +where pos_cps_of_set_code [code]: "pos_cps_of_set (set xs) f i = find_first f xs"
3.16
3.17 -consts pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => natural => (bool * term list) option"
3.18 -consts neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => natural => term list Quickcheck_Exhaustive.three_valued"
3.19 -
3.20 -lemma
3.21 - [code]: "pos_cps_of_set (set xs) f i = find_first f xs"
3.22 -sorry
3.23 -
3.24 -consts find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued)
3.25 +axiomatization find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued)
3.26 => 'b list => 'a Quickcheck_Exhaustive.three_valued"
3.27 -
3.28 -lemma [code]:
3.29 +where find_first'_code [code]:
3.30 "find_first' f [] = Quickcheck_Exhaustive.No_value"
3.31 "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))"
3.32 -sorry
3.33
3.34 -lemma
3.35 - [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"
3.36 -sorry
3.37 +axiomatization neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => natural => term list Quickcheck_Exhaustive.three_valued"
3.38 +where neg_cps_of_set_code [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"
3.39
3.40 setup {*
3.41 let
4.1 --- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Sat Jul 12 11:31:23 2014 +0200
4.2 +++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Sat Jul 12 19:54:04 2014 +0200
4.3 @@ -6,7 +6,7 @@
4.4 header {* Examples for the 'quickcheck' command *}
4.5
4.6 theory Quickcheck_Examples
4.7 -imports Complex_Main "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/DAList_Multiset"
4.8 +imports "../Complex_Main" "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/DAList_Multiset"
4.9 begin
4.10
4.11 text {*
5.1 --- a/src/HOL/ROOT Sat Jul 12 11:31:23 2014 +0200
5.2 +++ b/src/HOL/ROOT Sat Jul 12 19:54:04 2014 +0200
5.3 @@ -52,6 +52,7 @@
5.4 (*legacy tools*)
5.5 Refute
5.6 Old_Recdef
5.7 + Quickcheck_Types
5.8 theories [condition = ISABELLE_FULL_TEST]
5.9 Sum_of_Squares_Remote
5.10 document_files "root.bib" "root.tex"
5.11 @@ -883,11 +884,10 @@
5.12 options [document = false]
5.13 theories
5.14 Quickcheck_Examples
5.15 - (* FIXME
5.16 Quickcheck_Lattice_Examples
5.17 Completeness
5.18 Quickcheck_Interfaces
5.19 - Hotel_Example *)
5.20 + Hotel_Example
5.21 theories [condition = ISABELLE_GHC]
5.22 Quickcheck_Narrowing_Examples
5.23