src/HOL/Quickcheck_Examples/Hotel_Example.thy
changeset 63177 6c05c4632949
parent 63167 0909deb8059b
child 66453 cc19f7ca2ed6
equal deleted inserted replaced
63176:878bd5922f3b 63177:6c05c4632949
   107 axiomatization pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => natural => (bool * term list) option"
   107 axiomatization pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => natural => (bool * term list) option"
   108 where pos_cps_of_set_code [code]: "pos_cps_of_set (set xs) f i = find_first f xs"
   108 where pos_cps_of_set_code [code]: "pos_cps_of_set (set xs) f i = find_first f xs"
   109 
   109 
   110 axiomatization find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued)
   110 axiomatization find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued)
   111     => 'b list => 'a Quickcheck_Exhaustive.three_valued"
   111     => 'b list => 'a Quickcheck_Exhaustive.three_valued"
   112 where find_first'_code [code]:
   112 where find_first'_Nil: "find_first' f [] = Quickcheck_Exhaustive.No_value"
   113   "find_first' f [] = Quickcheck_Exhaustive.No_value"
   113   and find_first'_Cons: "find_first' f (x # xs) =
   114   "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))"
   114     (case f (Quickcheck_Exhaustive.Known x) of
       
   115       Quickcheck_Exhaustive.No_value => find_first' f xs
       
   116     | Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x
       
   117     | Quickcheck_Exhaustive.Unknown_value =>
       
   118         (case find_first' f xs of Quickcheck_Exhaustive.Value x =>
       
   119           Quickcheck_Exhaustive.Value x
       
   120         | _ => Quickcheck_Exhaustive.Unknown_value))"
       
   121 
       
   122 lemmas find_first'_code [code] = find_first'_Nil find_first'_Cons
   115 
   123 
   116 axiomatization neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => natural => term list Quickcheck_Exhaustive.three_valued"
   124 axiomatization neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => natural => term list Quickcheck_Exhaustive.three_valued"
   117 where neg_cps_of_set_code [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"
   125 where neg_cps_of_set_code [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"
   118 
   126 
   119 setup \<open>
   127 setup \<open>