summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sat, 28 May 2016 17:35:12 +0200 | |

changeset 63177 | 6c05c4632949 |

parent 63176 | 878bd5922f3b |

child 63178 | b9e1d53124f5 |

clarified axiomatization;

--- a/src/HOL/Quickcheck_Examples/Hotel_Example.thy Sat May 28 17:34:28 2016 +0200 +++ b/src/HOL/Quickcheck_Examples/Hotel_Example.thy Sat May 28 17:35:12 2016 +0200 @@ -109,9 +109,17 @@ axiomatization find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued) => 'b list => 'a Quickcheck_Exhaustive.three_valued" -where find_first'_code [code]: - "find_first' f [] = Quickcheck_Exhaustive.No_value" - "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))" +where find_first'_Nil: "find_first' f [] = Quickcheck_Exhaustive.No_value" + and find_first'_Cons: "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))" + +lemmas find_first'_code [code] = find_first'_Nil find_first'_Cons axiomatization neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => natural => term list Quickcheck_Exhaustive.three_valued" where neg_cps_of_set_code [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"