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

author | blanchet |

Tue, 01 Jun 2010 17:45:28 +0200 | |

changeset 37270 | c0f36d44de33 |

parent 37269 | 49c45156c9e1 |

child 37271 | 694aebcd602b |

added examples/tests for THE and SOME

--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Tue Jun 01 17:28:16 2010 +0200 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Tue Jun 01 17:45:28 2010 +0200 @@ -1051,6 +1051,52 @@ nitpick [expect = none] sorry +lemma "(THE j. j > Suc 10 \<and> j \<le> 11) \<noteq> 0" +nitpick [card nat = 4, full_descrs, unary_ints, expect = potential] +nitpick [card nat = 14, full_descrs, unary_ints, expect = potential] (* unfortunate *) +oops + +lemma "(THE j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x \<noteq> 0" +nitpick [card nat = 4, full_descrs, unary_ints, expect = potential] +nitpick [card nat = 14, full_descrs, unary_ints, expect = none] +sorry + +lemma "(THE j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x = 12" +nitpick [card nat = 4, full_descrs, unary_ints, expect = potential] +nitpick [card nat = 14, full_descrs, unary_ints, expect = none] +sorry + +lemma "(THE j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12" +nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine] +oops + +lemma "(THE j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12 \<or> x = 13" +nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine] +oops + +lemma "(SOME j. j > Suc 10 \<and> j \<le> 11) \<noteq> 0" +nitpick [card nat = 4, full_descrs, unary_ints, expect = potential] +nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine] +oops + +lemma "(SOME j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x \<noteq> 0" +nitpick [card nat = 4, full_descrs, unary_ints, expect = potential] +nitpick [card nat = 14, full_descrs, unary_ints, expect = none] +oops + +lemma "(SOME j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x = 12" +nitpick [card nat = 4, full_descrs, unary_ints, expect = potential] +nitpick [card nat = 14, full_descrs, unary_ints, expect = none] +sorry + +lemma "(SOME j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12" +nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine] +oops + +lemma "(SOME j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12 \<or> x = 13" +nitpick [card nat = 14, full_descrs, unary_ints, expect = none] +sorry + subsection {* Destructors and Recursors *} lemma "(x\<Colon>'a) = (case True of True \<Rightarrow> x | False \<Rightarrow> x)"