src/HOL/Nitpick_Examples/Induct_Nits.thy
 author blanchet Tue Aug 03 17:43:15 2010 +0200 (2010-08-03) changeset 38185 b51677438b3a parent 35671 ed2c3830d881 child 38186 c28018f5a1d6 permissions -rw-r--r--
speed up Nitpick examples a little bit
```     1 (*  Title:      HOL/Nitpick_Examples/Induct_Nits.thy
```
```     2     Author:     Jasmin Blanchette, TU Muenchen
```
```     3     Copyright   2009, 2010
```
```     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 [card = 1\<midarrow>6,  bits = 1,2,3,4,6,8,
```
```    15                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
```
```    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 = {}"
```
```    58 nitpick [expect = none]
```
```    59 nitpick [dont_star_linear_preds, expect = none]
```
```    60 sorry
```
```    61
```
```    62 lemma "q2 = {}"
```
```    63 nitpick [expect = genuine]
```
```    64 nitpick [dont_star_linear_preds, expect = genuine]
```
```    65 nitpick [wf, expect = quasi_genuine]
```
```    66 oops
```
```    67
```
```    68 lemma "p2 = UNIV"
```
```    69 nitpick [expect = genuine]
```
```    70 nitpick [dont_star_linear_preds, expect = genuine]
```
```    71 oops
```
```    72
```
```    73 lemma "q2 = UNIV"
```
```    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 [dont_star_linear_preds, expect = none]
```
```   119 nitpick [non_wf, expect = potential]
```
```   120 nitpick [non_wf, dont_box, expect = none]
```
```   121 nitpick [non_wf, dont_star_linear_preds, expect = none]
```
```   122 sorry
```
```   123
```
```   124 lemma "p4 = q4"
```
```   125 nitpick [expect = none]
```
```   126 nitpick [dont_star_linear_preds, expect = none]
```
```   127 nitpick [non_wf, expect = potential]
```
```   128 nitpick [non_wf, dont_box, expect = none]
```
```   129 nitpick [non_wf, dont_star_linear_preds, expect = none]
```
```   130 sorry
```
```   131
```
```   132 lemma "p3 = UNIV - p4"
```
```   133 nitpick [expect = none]
```
```   134 nitpick [dont_star_linear_preds, expect = none]
```
```   135 nitpick [non_wf, expect = potential]
```
```   136 nitpick [non_wf, dont_box, expect = none]
```
```   137 nitpick [non_wf, dont_star_linear_preds, expect = none]
```
```   138 sorry
```
```   139
```
```   140 lemma "q3 = UNIV - q4"
```
```   141 nitpick [expect = none]
```
```   142 nitpick [dont_star_linear_preds, expect = none]
```
```   143 nitpick [non_wf, expect = none]
```
```   144 nitpick [non_wf, dont_box, expect = none]
```
```   145 nitpick [non_wf, dont_star_linear_preds, expect = none]
```
```   146 sorry
```
```   147
```
```   148 lemma "p3 \<inter> q4 \<noteq> {}"
```
```   149 nitpick [expect = potential]
```
```   150 nitpick [non_wf, expect = potential]
```
```   151 nitpick [non_wf, dont_star_linear_preds, expect = potential]
```
```   152 sorry
```
```   153
```
```   154 lemma "q3 \<inter> p4 \<noteq> {}"
```
```   155 nitpick [expect = potential]
```
```   156 nitpick [non_wf, expect = potential]
```
```   157 nitpick [non_wf, dont_star_linear_preds, expect = potential]
```
```   158 sorry
```
```   159
```
```   160 lemma "p3 \<union> q4 \<noteq> UNIV"
```
```   161 nitpick [expect = potential]
```
```   162 nitpick [non_wf, expect = potential]
```
```   163 nitpick [non_wf, dont_star_linear_preds, expect = potential]
```
```   164 sorry
```
```   165
```
```   166 lemma "q3 \<union> p4 \<noteq> UNIV"
```
```   167 nitpick [expect = potential]
```
```   168 nitpick [non_wf, expect = potential]
```
```   169 nitpick [non_wf, dont_star_linear_preds, expect = potential]
```
```   170 sorry
```
```   171
```
```   172 end
```