reactivate session Quickcheck_Examples
authorAndreas Lochbihler
Fri Jul 11 15:52:03 2014 +0200 (2014-07-11)
changeset 575448840fa17e17c
parent 57543 36041934e429
child 57548 278ab871319f
reactivate session Quickcheck_Examples
src/HOL/Library/Quickcheck_Types.thy
src/HOL/Quickcheck_Examples/Completeness.thy
src/HOL/Quickcheck_Examples/Hotel_Example.thy
src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
src/HOL/ROOT
     1.1 --- a/src/HOL/Library/Quickcheck_Types.thy	Fri Jul 11 15:35:11 2014 +0200
     1.2 +++ b/src/HOL/Library/Quickcheck_Types.thy	Fri Jul 11 15:52:03 2014 +0200
     1.3 @@ -466,12 +466,4 @@
     1.4  
     1.5  hide_type non_distrib_lattice flat_complete_lattice bot top
     1.6  
     1.7 -lemma "\<lbrakk> inf x z = inf y z; sup x z = sup y z \<rbrakk> \<Longrightarrow> x = y" 
     1.8 -quickcheck[exhaustive, expect=counterexample]
     1.9 -oops
    1.10 -
    1.11 -lemma "Inf {} = bot"
    1.12 -quickcheck[exhaustive, expect=counterexample]
    1.13 -oops
    1.14 -
    1.15  end
    1.16 \ No newline at end of file
     2.1 --- a/src/HOL/Quickcheck_Examples/Completeness.thy	Fri Jul 11 15:35:11 2014 +0200
     2.2 +++ b/src/HOL/Quickcheck_Examples/Completeness.thy	Fri Jul 11 15:52:03 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	Fri Jul 11 15:35:11 2014 +0200
     3.2 +++ b/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Fri Jul 11 15:52:03 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 -
     3.9 -lemma
    3.10 -  [code]: "cps_of_set (set xs) f = find_first f xs"
    3.11 -sorry
    3.12 -
    3.13 -consts pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => natural => (bool * term list) option"
    3.14 -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.15 +axiomatization cps_of_set :: "'a set => ('a => term list option) => term list option"
    3.16 +where cps_of_set_code [code]: "cps_of_set (set xs) f = find_first f xs"
    3.17  
    3.18 -lemma
    3.19 -  [code]: "pos_cps_of_set (set xs) f i = find_first f xs"
    3.20 -sorry
    3.21 +axiomatization pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => natural => (bool * term list) option"
    3.22 +where pos_cps_of_set_code [code]: "pos_cps_of_set (set xs) f i = find_first f xs"
    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	Fri Jul 11 15:35:11 2014 +0200
     4.2 +++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Fri Jul 11 15:52:03 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	Fri Jul 11 15:35:11 2014 +0200
     5.2 +++ b/src/HOL/ROOT	Fri Jul 11 15:52:03 2014 +0200
     5.3 @@ -884,11 +884,10 @@
     5.4    options [document = false]
     5.5    theories
     5.6      Quickcheck_Examples
     5.7 -  (* FIXME
     5.8      Quickcheck_Lattice_Examples
     5.9      Completeness
    5.10      Quickcheck_Interfaces
    5.11 -    Hotel_Example *)
    5.12 +    Hotel_Example
    5.13    theories [condition = ISABELLE_GHC]
    5.14      Quickcheck_Narrowing_Examples
    5.15