97 fun find_first :: "('a => 'b option) => 'a list => 'b option" |
97 fun find_first :: "('a => 'b option) => 'a list => 'b option" |
98 where |
98 where |
99 "find_first f [] = None" |
99 "find_first f [] = None" |
100 | "find_first f (x # xs) = (case f x of Some y => Some y | None => find_first f xs)" |
100 | "find_first f (x # xs) = (case f x of Some y => Some y | None => find_first f xs)" |
101 |
101 |
102 consts cps_of_set :: "'a set => ('a => term list option) => term list option" |
102 axiomatization cps_of_set :: "'a set => ('a => term list option) => term list option" |
|
103 where cps_of_set_code [code]: "cps_of_set (set xs) f = find_first f xs" |
103 |
104 |
104 lemma |
105 axiomatization pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => natural => (bool * term list) option" |
105 [code]: "cps_of_set (set xs) f = find_first f xs" |
106 where pos_cps_of_set_code [code]: "pos_cps_of_set (set xs) f i = find_first f xs" |
106 sorry |
|
107 |
107 |
108 consts pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => natural => (bool * term list) option" |
108 axiomatization find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued) |
109 consts neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => natural => term list Quickcheck_Exhaustive.three_valued" |
|
110 |
|
111 lemma |
|
112 [code]: "pos_cps_of_set (set xs) f i = find_first f xs" |
|
113 sorry |
|
114 |
|
115 consts find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued) |
|
116 => 'b list => 'a Quickcheck_Exhaustive.three_valued" |
109 => 'b list => 'a Quickcheck_Exhaustive.three_valued" |
117 |
110 where find_first'_code [code]: |
118 lemma [code]: |
|
119 "find_first' f [] = Quickcheck_Exhaustive.No_value" |
111 "find_first' f [] = Quickcheck_Exhaustive.No_value" |
120 "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))" |
112 "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))" |
121 sorry |
|
122 |
113 |
123 lemma |
114 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 [code]: "neg_cps_of_set (set xs) f i = find_first' f xs" |
115 where neg_cps_of_set_code [code]: "neg_cps_of_set (set xs) f i = find_first' f xs" |
125 sorry |
|
126 |
116 |
127 setup {* |
117 setup {* |
128 let |
118 let |
129 val Fun = Predicate_Compile_Aux.Fun |
119 val Fun = Predicate_Compile_Aux.Fun |
130 val Input = Predicate_Compile_Aux.Input |
120 val Input = Predicate_Compile_Aux.Input |