src/HOL/Nitpick_Examples/Induct_Nits.thy
 author hoelzl Fri Mar 22 10:41:43 2013 +0100 (2013-03-22) changeset 51474 1e9e68247ad1 parent 45970 b6d0cff57d96 child 54633 86e0b402994c permissions -rw-r--r--
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
```     1 (*  Title:      HOL/Nitpick_Examples/Induct_Nits.thy
```
```     2     Author:     Jasmin Blanchette, TU Muenchen
```
```     3     Copyright   2009-2011
```
```     4
```
```     5 Examples featuring Nitpick applied to (co)inductive definitions.
```
```     6 *)
```
```     7
```
```     8 header {* Examples Featuring Nitpick Applied to (Co)inductive Definitions *}
```
```     9
```
```    10 theory Induct_Nits
```
```    11 imports Main
```
```    12 begin
```
```    13
```
```    14 nitpick_params [verbose, card = 1\<emdash>8, unary_ints,
```
```    15                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
```
```    16
```
```    17 inductive p1 :: "nat \<Rightarrow> bool" where
```
```    18 "p1 0" |
```
```    19 "p1 n \<Longrightarrow> p1 (n + 2)"
```
```    20
```
```    21 coinductive q1 :: "nat \<Rightarrow> bool" where
```
```    22 "q1 0" |
```
```    23 "q1 n \<Longrightarrow> q1 (n + 2)"
```
```    24
```
```    25 lemma "p1 = q1"
```
```    26 nitpick [expect = none]
```
```    27 nitpick [wf, expect = none]
```
```    28 nitpick [non_wf, expect = none]
```
```    29 nitpick [non_wf, dont_star_linear_preds, expect = none]
```
```    30 oops
```
```    31
```
```    32 lemma "p1 \<noteq> q1"
```
```    33 nitpick [expect = potential]
```
```    34 nitpick [wf, expect = potential]
```
```    35 nitpick [non_wf, expect = potential]
```
```    36 nitpick [non_wf, dont_star_linear_preds, expect = potential]
```
```    37 oops
```
```    38
```
```    39 lemma "p1 (n - 2) \<Longrightarrow> p1 n"
```
```    40 nitpick [expect = genuine]
```
```    41 nitpick [non_wf, expect = genuine]
```
```    42 nitpick [non_wf, dont_star_linear_preds, expect = genuine]
```
```    43 oops
```
```    44
```
```    45 lemma "q1 (n - 2) \<Longrightarrow> q1 n"
```
```    46 nitpick [expect = genuine]
```
```    47 nitpick [non_wf, expect = genuine]
```
```    48 nitpick [non_wf, dont_star_linear_preds, expect = genuine]
```
```    49 oops
```
```    50
```
```    51 inductive p2 :: "nat \<Rightarrow> bool" where
```
```    52 "p2 n \<Longrightarrow> p2 n"
```
```    53
```
```    54 coinductive q2 :: "nat \<Rightarrow> bool" where
```
```    55 "q2 n \<Longrightarrow> q2 n"
```
```    56
```
```    57 lemma "p2 = bot"
```
```    58 nitpick [expect = none]
```
```    59 nitpick [dont_star_linear_preds, expect = none]
```
```    60 sorry
```
```    61
```
```    62 lemma "q2 = bot"
```
```    63 nitpick [expect = genuine]
```
```    64 nitpick [dont_star_linear_preds, expect = genuine]
```
```    65 nitpick [wf, expect = quasi_genuine]
```
```    66 oops
```
```    67
```
```    68 lemma "p2 = top"
```
```    69 nitpick [expect = genuine]
```
```    70 nitpick [dont_star_linear_preds, expect = genuine]
```
```    71 oops
```
```    72
```
```    73 lemma "q2 = top"
```
```    74 nitpick [expect = none]
```
```    75 nitpick [dont_star_linear_preds, expect = none]
```
```    76 nitpick [wf, expect = quasi_genuine]
```
```    77 sorry
```
```    78
```
```    79 lemma "p2 = q2"
```
```    80 nitpick [expect = genuine]
```
```    81 nitpick [dont_star_linear_preds, expect = genuine]
```
```    82 oops
```
```    83
```
```    84 lemma "p2 n"
```
```    85 nitpick [expect = genuine]
```
```    86 nitpick [dont_star_linear_preds, expect = genuine]
```
```    87 nitpick [dont_specialize, expect = genuine]
```
```    88 oops
```
```    89
```
```    90 lemma "q2 n"
```
```    91 nitpick [expect = none]
```
```    92 nitpick [dont_star_linear_preds, expect = none]
```
```    93 sorry
```
```    94
```
```    95 lemma "\<not> p2 n"
```
```    96 nitpick [expect = none]
```
```    97 nitpick [dont_star_linear_preds, expect = none]
```
```    98 sorry
```
```    99
```
```   100 lemma "\<not> q2 n"
```
```   101 nitpick [expect = genuine]
```
```   102 nitpick [dont_star_linear_preds, expect = genuine]
```
```   103 nitpick [dont_specialize, expect = genuine]
```
```   104 oops
```
```   105
```
```   106 inductive p3 and p4 where
```
```   107 "p3 0" |
```
```   108 "p3 n \<Longrightarrow> p4 (Suc n)" |
```
```   109 "p4 n \<Longrightarrow> p3 (Suc n)"
```
```   110
```
```   111 coinductive q3 and q4 where
```
```   112 "q3 0" |
```
```   113 "q3 n \<Longrightarrow> q4 (Suc n)" |
```
```   114 "q4 n \<Longrightarrow> q3 (Suc n)"
```
```   115
```
```   116 lemma "p3 = q3"
```
```   117 nitpick [expect = none]
```
```   118 nitpick [non_wf, expect = none]
```
```   119 sorry
```
```   120
```
```   121 lemma "p4 = q4"
```
```   122 nitpick [expect = none]
```
```   123 nitpick [non_wf, expect = none]
```
```   124 sorry
```
```   125
```
```   126 lemma "p3 = top - p4"
```
```   127 nitpick [expect = none]
```
```   128 nitpick [non_wf, expect = none]
```
```   129 sorry
```
```   130
```
```   131 lemma "q3 = top - q4"
```
```   132 nitpick [expect = none]
```
```   133 nitpick [non_wf, expect = none]
```
```   134 sorry
```
```   135
```
```   136 lemma "inf p3 q4 \<noteq> bot"
```
```   137 nitpick [expect = potential]
```
```   138 nitpick [non_wf, expect = potential]
```
```   139 sorry
```
```   140
```
```   141 lemma "inf q3 p4 \<noteq> bot"
```
```   142 nitpick [expect = potential]
```
```   143 nitpick [non_wf, expect = potential]
```
```   144 sorry
```
```   145
```
```   146 lemma "sup p3 q4 \<noteq> top"
```
```   147 nitpick [expect = potential]
```
```   148 nitpick [non_wf, expect = potential]
```
```   149 sorry
```
```   150
```
```   151 lemma "sup q3 p4 \<noteq> top"
```
```   152 nitpick [expect = potential]
```
```   153 nitpick [non_wf, expect = potential]
```
```   154 sorry
```
```   155
```
```   156 end
```