src/HOL/Nitpick_Examples/Induct_Nits.thy
author blanchet
Wed Sep 21 15:55:16 2011 +0200 (2011-09-21)
changeset 45035 60d2c03d5c70
parent 42959 ee829022381d
child 45970 b6d0cff57d96
permissions -rw-r--r--
reintroduced Minipick as Nitpick example
blanchet@33197
     1
(*  Title:      HOL/Nitpick_Examples/Induct_Nits.thy
blanchet@33197
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@45035
     3
    Copyright   2009-2011
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@42959
    14
nitpick_params [verbose, card = 1\<emdash>8, unary_ints,
krauss@42208
    15
                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
blanchet@33197
    16
blanchet@33197
    17
inductive p1 :: "nat \<Rightarrow> bool" where
blanchet@33197
    18
"p1 0" |
blanchet@33197
    19
"p1 n \<Longrightarrow> p1 (n + 2)"
blanchet@33197
    20
blanchet@33197
    21
coinductive q1 :: "nat \<Rightarrow> bool" where
blanchet@33197
    22
"q1 0" |
blanchet@33197
    23
"q1 n \<Longrightarrow> q1 (n + 2)"
blanchet@33197
    24
blanchet@33197
    25
lemma "p1 = q1"
blanchet@33197
    26
nitpick [expect = none]
blanchet@33197
    27
nitpick [wf, expect = none]
blanchet@33197
    28
nitpick [non_wf, expect = none]
blanchet@33197
    29
nitpick [non_wf, dont_star_linear_preds, expect = none]
blanchet@33197
    30
oops
blanchet@33197
    31
blanchet@33197
    32
lemma "p1 \<noteq> q1"
blanchet@33197
    33
nitpick [expect = potential]
blanchet@33197
    34
nitpick [wf, expect = potential]
blanchet@33197
    35
nitpick [non_wf, expect = potential]
blanchet@33197
    36
nitpick [non_wf, dont_star_linear_preds, expect = potential]
blanchet@33197
    37
oops
blanchet@33197
    38
blanchet@33197
    39
lemma "p1 (n - 2) \<Longrightarrow> p1 n"
blanchet@33197
    40
nitpick [expect = genuine]
blanchet@33197
    41
nitpick [non_wf, expect = genuine]
blanchet@33197
    42
nitpick [non_wf, dont_star_linear_preds, expect = genuine]
blanchet@33197
    43
oops
blanchet@33197
    44
blanchet@33197
    45
lemma "q1 (n - 2) \<Longrightarrow> q1 n"
blanchet@33197
    46
nitpick [expect = genuine]
blanchet@33197
    47
nitpick [non_wf, expect = genuine]
blanchet@33197
    48
nitpick [non_wf, dont_star_linear_preds, expect = genuine]
blanchet@33197
    49
oops
blanchet@33197
    50
blanchet@33197
    51
inductive p2 :: "nat \<Rightarrow> bool" where
blanchet@33197
    52
"p2 n \<Longrightarrow> p2 n"
blanchet@33197
    53
blanchet@33197
    54
coinductive q2 :: "nat \<Rightarrow> bool" where
blanchet@33197
    55
"q2 n \<Longrightarrow> q2 n"
blanchet@33197
    56
blanchet@33197
    57
lemma "p2 = {}"
blanchet@33197
    58
nitpick [expect = none]
blanchet@33197
    59
nitpick [dont_star_linear_preds, expect = none]
blanchet@33197
    60
sorry
blanchet@33197
    61
blanchet@33197
    62
lemma "q2 = {}"
blanchet@33197
    63
nitpick [expect = genuine]
blanchet@33197
    64
nitpick [dont_star_linear_preds, expect = genuine]
blanchet@35671
    65
nitpick [wf, expect = quasi_genuine]
blanchet@33197
    66
oops
blanchet@33197
    67
blanchet@33197
    68
lemma "p2 = UNIV"
blanchet@33197
    69
nitpick [expect = genuine]
blanchet@33197
    70
nitpick [dont_star_linear_preds, expect = genuine]
blanchet@33197
    71
oops
blanchet@33197
    72
blanchet@33197
    73
lemma "q2 = UNIV"
blanchet@33197
    74
nitpick [expect = none]
blanchet@33197
    75
nitpick [dont_star_linear_preds, expect = none]
blanchet@35671
    76
nitpick [wf, expect = quasi_genuine]
blanchet@33197
    77
sorry
blanchet@33197
    78
blanchet@33197
    79
lemma "p2 = q2"
blanchet@33197
    80
nitpick [expect = genuine]
blanchet@33197
    81
nitpick [dont_star_linear_preds, expect = genuine]
blanchet@33197
    82
oops
blanchet@33197
    83
blanchet@33197
    84
lemma "p2 n"
blanchet@33197
    85
nitpick [expect = genuine]
blanchet@33197
    86
nitpick [dont_star_linear_preds, expect = genuine]
blanchet@33197
    87
nitpick [dont_specialize, expect = genuine]
blanchet@33197
    88
oops
blanchet@33197
    89
blanchet@33197
    90
lemma "q2 n"
blanchet@33197
    91
nitpick [expect = none]
blanchet@33197
    92
nitpick [dont_star_linear_preds, expect = none]
blanchet@33197
    93
sorry
blanchet@33197
    94
blanchet@33197
    95
lemma "\<not> p2 n"
blanchet@33197
    96
nitpick [expect = none]
blanchet@33197
    97
nitpick [dont_star_linear_preds, expect = none]
blanchet@33197
    98
sorry
blanchet@33197
    99
blanchet@33197
   100
lemma "\<not> q2 n"
blanchet@33197
   101
nitpick [expect = genuine]
blanchet@33197
   102
nitpick [dont_star_linear_preds, expect = genuine]
blanchet@33197
   103
nitpick [dont_specialize, expect = genuine]
blanchet@33197
   104
oops
blanchet@33197
   105
blanchet@33197
   106
inductive p3 and p4 where
blanchet@33197
   107
"p3 0" |
blanchet@33197
   108
"p3 n \<Longrightarrow> p4 (Suc n)" |
blanchet@33197
   109
"p4 n \<Longrightarrow> p3 (Suc n)"
blanchet@33197
   110
blanchet@33197
   111
coinductive q3 and q4 where
blanchet@33197
   112
"q3 0" |
blanchet@33197
   113
"q3 n \<Longrightarrow> q4 (Suc n)" |
blanchet@33197
   114
"q4 n \<Longrightarrow> q3 (Suc n)"
blanchet@33197
   115
blanchet@33197
   116
lemma "p3 = q3"
blanchet@33197
   117
nitpick [expect = none]
blanchet@38186
   118
nitpick [non_wf, expect = none]
blanchet@33197
   119
sorry
blanchet@33197
   120
blanchet@33197
   121
lemma "p4 = q4"
blanchet@33197
   122
nitpick [expect = none]
blanchet@38186
   123
nitpick [non_wf, expect = none]
blanchet@33197
   124
sorry
blanchet@33197
   125
blanchet@33197
   126
lemma "p3 = UNIV - p4"
blanchet@33197
   127
nitpick [expect = none]
blanchet@38186
   128
nitpick [non_wf, expect = none]
blanchet@33197
   129
sorry
blanchet@33197
   130
blanchet@33197
   131
lemma "q3 = UNIV - q4"
blanchet@33197
   132
nitpick [expect = none]
blanchet@33197
   133
nitpick [non_wf, expect = none]
blanchet@33197
   134
sorry
blanchet@33197
   135
blanchet@33197
   136
lemma "p3 \<inter> q4 \<noteq> {}"
blanchet@33197
   137
nitpick [expect = potential]
blanchet@33197
   138
nitpick [non_wf, expect = potential]
blanchet@33197
   139
sorry
blanchet@33197
   140
blanchet@33197
   141
lemma "q3 \<inter> p4 \<noteq> {}"
blanchet@33197
   142
nitpick [expect = potential]
blanchet@33197
   143
nitpick [non_wf, expect = potential]
blanchet@33197
   144
sorry
blanchet@33197
   145
blanchet@33197
   146
lemma "p3 \<union> q4 \<noteq> UNIV"
blanchet@33197
   147
nitpick [expect = potential]
blanchet@33197
   148
nitpick [non_wf, expect = potential]
blanchet@33197
   149
sorry
blanchet@33197
   150
blanchet@33197
   151
lemma "q3 \<union> p4 \<noteq> UNIV"
blanchet@33197
   152
nitpick [expect = potential]
blanchet@33197
   153
nitpick [non_wf, expect = potential]
blanchet@33197
   154
sorry
blanchet@33197
   155
blanchet@33197
   156
end