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