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> 