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

author | bulwahn |

Thu, 08 Dec 2011 13:53:28 +0100 | |

changeset 45790 | 3355c27c93a4 |

parent 45789 | 36ea69266e61 |

child 45791 | d985ec974815 |

adding examples for quickcheck narrowing about partial functions

--- a/src/HOL/ex/Quickcheck_Narrowing_Examples.thy Thu Dec 08 13:53:27 2011 +0100 +++ b/src/HOL/ex/Quickcheck_Narrowing_Examples.thy Thu Dec 08 13:53:28 2011 +0100 @@ -229,5 +229,42 @@ quickcheck[tester = narrowing, finite_types = false, default_type = nat, size = 6, expect = counterexample] oops +subsection {* Examples with hd and last *} + +lemma + "hd (xs @ ys) = hd ys" +quickcheck[narrowing, expect = counterexample] +oops + +lemma + "last(xs @ ys) = last xs" +quickcheck[narrowing, expect = counterexample] +oops + +subsection {* Examples with underspecified/partial functions *} + +lemma + "xs = [] ==> hd xs \<noteq> x" +quickcheck[narrowing, expect = no_counterexample] +oops + +lemma + "xs = [] ==> hd xs = x" +quickcheck[narrowing, expect = no_counterexample] +oops + +lemma "xs = [] ==> hd xs = x ==> x = y" +quickcheck[narrowing, expect = no_counterexample] +oops + +lemma + "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)" +quickcheck[narrowing, expect = no_counterexample] +oops + +lemma + "hd (map f xs) = f (hd xs)" +quickcheck[narrowing, expect = no_counterexample] +oops end