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

author | bulwahn |

Thu, 10 Nov 2011 17:26:17 +0100 | |

changeset 45441 | fb4ac1dd4fde |

parent 45440 | 9f4d3e68ae98 |

child 45442 | 2b91e27676b2 |

adding some test cases for preprocessing and narrowing

src/HOL/ex/Quickcheck_Examples.thy | file | annotate | diff | comparison | revisions | |

src/HOL/ex/Quickcheck_Narrowing_Examples.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/ex/Quickcheck_Examples.thy Thu Nov 10 17:26:15 2011 +0100 +++ b/src/HOL/ex/Quickcheck_Examples.thy Thu Nov 10 17:26:17 2011 +0100 @@ -380,4 +380,22 @@ end +subsection {* Examples with HOL quantifiers *} + +lemma + "\<forall> xs ys. xs = [] --> xs = ys" +quickcheck[exhaustive, expect = counterexample] +oops + +lemma + "ys = [] --> (\<forall>xs. xs = [] --> xs = y # ys)" +quickcheck[exhaustive, expect = counterexample] +oops + +lemma + "\<forall>xs. (\<exists> ys. ys = []) --> xs = ys" +quickcheck[exhaustive, expect = counterexample] +oops + + end

--- a/src/HOL/ex/Quickcheck_Narrowing_Examples.thy Thu Nov 10 17:26:15 2011 +0100 +++ b/src/HOL/ex/Quickcheck_Narrowing_Examples.thy Thu Nov 10 17:26:17 2011 +0100 @@ -66,6 +66,11 @@ quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample] oops +lemma "a # xs = ys @ [a] ==> EX zs. xs = zs @ [a] & ys = a#zs" +quickcheck[narrowing, expect = counterexample] +quickcheck[exhaustive, random, expect = no_counterexample] +oops + subsection {* Simple list examples *} lemma "rev xs = xs"