src/HOL/Nitpick_Examples/Induct_Nits.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 35078 6fd1052fe463
child 35671 ed2c3830d881
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
blanchet@33197
     1
(*  Title:      HOL/Nitpick_Examples/Induct_Nits.thy
blanchet@33197
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@35076
     3
    Copyright   2009, 2010
blanchet@33197
     4
blanchet@33197
     5
Examples featuring Nitpick applied to (co)inductive definitions.
blanchet@33197
     6
*)
blanchet@33197
     7
blanchet@33197
     8
header {* Examples Featuring Nitpick Applied to (Co)inductive Definitions *}
blanchet@33197
     9
blanchet@33197
    10
theory Induct_Nits
blanchet@33197
    11
imports Main
blanchet@33197
    12
begin
blanchet@33197
    13
blanchet@35078
    14
nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
blanchet@33197
    15
blanchet@33197
    16
inductive p1 :: "nat \<Rightarrow> bool" where
blanchet@33197
    17
"p1 0" |
blanchet@33197
    18
"p1 n \<Longrightarrow> p1 (n + 2)"
blanchet@33197
    19
blanchet@33197
    20
coinductive q1 :: "nat \<Rightarrow> bool" where
blanchet@33197
    21
"q1 0" |
blanchet@33197
    22
"q1 n \<Longrightarrow> q1 (n + 2)"
blanchet@33197
    23
blanchet@33197
    24
lemma "p1 = q1"
blanchet@33197
    25
nitpick [expect = none]
blanchet@33197
    26
nitpick [wf, expect = none]
blanchet@33197
    27
nitpick [non_wf, expect = none]
blanchet@33197
    28
nitpick [non_wf, dont_star_linear_preds, expect = none]
blanchet@33197
    29
oops
blanchet@33197
    30
blanchet@33197
    31
lemma "p1 \<noteq> q1"
blanchet@33197
    32
nitpick [expect = potential]
blanchet@33197
    33
nitpick [wf, expect = potential]
blanchet@33197
    34
nitpick [non_wf, expect = potential]
blanchet@33197
    35
nitpick [non_wf, dont_star_linear_preds, expect = potential]
blanchet@33197
    36
oops
blanchet@33197
    37
blanchet@33197
    38
lemma "p1 (n - 2) \<Longrightarrow> p1 n"
blanchet@33197
    39
nitpick [expect = genuine]
blanchet@33197
    40
nitpick [non_wf, expect = genuine]
blanchet@33197
    41
nitpick [non_wf, dont_star_linear_preds, expect = genuine]
blanchet@33197
    42
oops
blanchet@33197
    43
blanchet@33197
    44
lemma "q1 (n - 2) \<Longrightarrow> q1 n"
blanchet@33197
    45
nitpick [expect = genuine]
blanchet@33197
    46
nitpick [non_wf, expect = genuine]
blanchet@33197
    47
nitpick [non_wf, dont_star_linear_preds, expect = genuine]
blanchet@33197
    48
oops
blanchet@33197
    49
blanchet@33197
    50
inductive p2 :: "nat \<Rightarrow> bool" where
blanchet@33197
    51
"p2 n \<Longrightarrow> p2 n"
blanchet@33197
    52
blanchet@33197
    53
coinductive q2 :: "nat \<Rightarrow> bool" where
blanchet@33197
    54
"q2 n \<Longrightarrow> q2 n"
blanchet@33197
    55
blanchet@33197
    56
lemma "p2 = {}"
blanchet@33197
    57
nitpick [expect = none]
blanchet@33197
    58
nitpick [dont_star_linear_preds, expect = none]
blanchet@33197
    59
sorry
blanchet@33197
    60
blanchet@33197
    61
lemma "q2 = {}"
blanchet@33197
    62
nitpick [expect = genuine]
blanchet@33197
    63
nitpick [dont_star_linear_preds, expect = genuine]
blanchet@33197
    64
nitpick [wf, expect = likely_genuine]
blanchet@33197
    65
oops
blanchet@33197
    66
blanchet@33197
    67
lemma "p2 = UNIV"
blanchet@33197
    68
nitpick [expect = genuine]
blanchet@33197
    69
nitpick [dont_star_linear_preds, expect = genuine]
blanchet@33197
    70
oops
blanchet@33197
    71
blanchet@33197
    72
lemma "q2 = UNIV"
blanchet@33197
    73
nitpick [expect = none]
blanchet@33197
    74
nitpick [dont_star_linear_preds, expect = none]
blanchet@33197
    75
nitpick [wf, expect = likely_genuine]
blanchet@33197
    76
sorry
blanchet@33197
    77
blanchet@33197
    78
lemma "p2 = q2"
blanchet@33197
    79
nitpick [expect = genuine]
blanchet@33197
    80
nitpick [dont_star_linear_preds, expect = genuine]
blanchet@33197
    81
oops
blanchet@33197
    82
blanchet@33197
    83
lemma "p2 n"
blanchet@33197
    84
nitpick [expect = genuine]
blanchet@33197
    85
nitpick [dont_star_linear_preds, expect = genuine]
blanchet@33197
    86
nitpick [dont_specialize, expect = genuine]
blanchet@33197
    87
oops
blanchet@33197
    88
blanchet@33197
    89
lemma "q2 n"
blanchet@33197
    90
nitpick [expect = none]
blanchet@33197
    91
nitpick [dont_star_linear_preds, expect = none]
blanchet@33197
    92
sorry
blanchet@33197
    93
blanchet@33197
    94
lemma "\<not> p2 n"
blanchet@33197
    95
nitpick [expect = none]
blanchet@33197
    96
nitpick [dont_star_linear_preds, expect = none]
blanchet@33197
    97
sorry
blanchet@33197
    98
blanchet@33197
    99
lemma "\<not> q2 n"
blanchet@33197
   100
nitpick [expect = genuine]
blanchet@33197
   101
nitpick [dont_star_linear_preds, expect = genuine]
blanchet@33197
   102
nitpick [dont_specialize, expect = genuine]
blanchet@33197
   103
oops
blanchet@33197
   104
blanchet@33197
   105
inductive p3 and p4 where
blanchet@33197
   106
"p3 0" |
blanchet@33197
   107
"p3 n \<Longrightarrow> p4 (Suc n)" |
blanchet@33197
   108
"p4 n \<Longrightarrow> p3 (Suc n)"
blanchet@33197
   109
blanchet@33197
   110
coinductive q3 and q4 where
blanchet@33197
   111
"q3 0" |
blanchet@33197
   112
"q3 n \<Longrightarrow> q4 (Suc n)" |
blanchet@33197
   113
"q4 n \<Longrightarrow> q3 (Suc n)"
blanchet@33197
   114
blanchet@33197
   115
lemma "p3 = q3"
blanchet@33197
   116
nitpick [expect = none]
blanchet@33197
   117
nitpick [dont_star_linear_preds, expect = none]
blanchet@33197
   118
nitpick [non_wf, expect = potential]
blanchet@33197
   119
nitpick [non_wf, dont_box, expect = none]
blanchet@33197
   120
nitpick [non_wf, dont_star_linear_preds, expect = none]
blanchet@33197
   121
sorry
blanchet@33197
   122
blanchet@33197
   123
lemma "p4 = q4"
blanchet@33197
   124
nitpick [expect = none]
blanchet@33197
   125
nitpick [dont_star_linear_preds, expect = none]
blanchet@33197
   126
nitpick [non_wf, expect = potential]
blanchet@33197
   127
nitpick [non_wf, dont_box, expect = none]
blanchet@33197
   128
nitpick [non_wf, dont_star_linear_preds, expect = none]
blanchet@33197
   129
sorry
blanchet@33197
   130
blanchet@33197
   131
lemma "p3 = UNIV - p4"
blanchet@33197
   132
nitpick [expect = none]
blanchet@33197
   133
nitpick [dont_star_linear_preds, expect = none]
blanchet@33197
   134
nitpick [non_wf, expect = potential]
blanchet@33197
   135
nitpick [non_wf, dont_box, expect = none]
blanchet@33197
   136
nitpick [non_wf, dont_star_linear_preds, expect = none]
blanchet@33197
   137
sorry
blanchet@33197
   138
blanchet@33197
   139
lemma "q3 = UNIV - q4"
blanchet@33197
   140
nitpick [expect = none]
blanchet@33197
   141
nitpick [dont_star_linear_preds, expect = none]
blanchet@33197
   142
nitpick [non_wf, expect = none]
blanchet@33197
   143
nitpick [non_wf, dont_box, expect = none]
blanchet@33197
   144
nitpick [non_wf, dont_star_linear_preds, expect = none]
blanchet@33197
   145
sorry
blanchet@33197
   146
blanchet@33197
   147
lemma "p3 \<inter> q4 \<noteq> {}"
blanchet@33197
   148
nitpick [expect = potential]
blanchet@33197
   149
nitpick [non_wf, expect = potential]
blanchet@33197
   150
nitpick [non_wf, dont_star_linear_preds, expect = potential]
blanchet@33197
   151
sorry
blanchet@33197
   152
blanchet@33197
   153
lemma "q3 \<inter> p4 \<noteq> {}"
blanchet@33197
   154
nitpick [expect = potential]
blanchet@33197
   155
nitpick [non_wf, expect = potential]
blanchet@33197
   156
nitpick [non_wf, dont_star_linear_preds, expect = potential]
blanchet@33197
   157
sorry
blanchet@33197
   158
blanchet@33197
   159
lemma "p3 \<union> q4 \<noteq> UNIV"
blanchet@33197
   160
nitpick [expect = potential]
blanchet@33197
   161
nitpick [non_wf, expect = potential]
blanchet@33197
   162
nitpick [non_wf, dont_star_linear_preds, expect = potential]
blanchet@33197
   163
sorry
blanchet@33197
   164
blanchet@33197
   165
lemma "q3 \<union> p4 \<noteq> UNIV"
blanchet@33197
   166
nitpick [expect = potential]
blanchet@33197
   167
nitpick [non_wf, expect = potential]
blanchet@33197
   168
nitpick [non_wf, dont_star_linear_preds, expect = potential]
blanchet@33197
   169
sorry
blanchet@33197
   170
blanchet@33197
   171
end