Mercurialisabelle / file revision
summary | shortlog | changelog | graph | tags | branches | files | changeset | file | revisions | annotate | diff | raw
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
isabelle