src/HOL/Nitpick_Examples/Induct_Nits.thy
 author wenzelm Tue Oct 10 19:23:03 2017 +0200 (2017-10-10) changeset 66831 29ea2b900a05 parent 63167 0909deb8059b permissions -rw-r--r--
tuned: each session has at most one defining entry;
 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` wenzelm@63167 ` 8` ```section \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@55893 ` 14` ```nitpick_params [verbose, card = 1-8, unary_ints, ``` blanchet@54680 ` 15` ``` sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240] ``` blanchet@33197 ` 16` blanchet@33197 ` 17` ```inductive p1 :: "nat \ bool" where ``` blanchet@33197 ` 18` ```"p1 0" | ``` blanchet@33197 ` 19` ```"p1 n \ p1 (n + 2)" ``` blanchet@33197 ` 20` blanchet@33197 ` 21` ```coinductive q1 :: "nat \ bool" where ``` blanchet@33197 ` 22` ```"q1 0" | ``` blanchet@33197 ` 23` ```"q1 n \ 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 \ 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) \ 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) \ 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 \ bool" where ``` blanchet@33197 ` 52` ```"p2 n \ p2 n" ``` blanchet@33197 ` 53` blanchet@33197 ` 54` ```coinductive q2 :: "nat \ bool" where ``` blanchet@33197 ` 55` ```"q2 n \ q2 n" ``` blanchet@33197 ` 56` haftmann@45970 ` 57` ```lemma "p2 = bot" ``` blanchet@33197 ` 58` ```nitpick [expect = none] ``` blanchet@33197 ` 59` ```nitpick [dont_star_linear_preds, expect = none] ``` blanchet@33197 ` 60` ```sorry ``` blanchet@33197 ` 61` haftmann@45970 ` 62` ```lemma "q2 = bot" ``` 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` haftmann@45970 ` 68` ```lemma "p2 = top" ``` blanchet@33197 ` 69` ```nitpick [expect = genuine] ``` blanchet@33197 ` 70` ```nitpick [dont_star_linear_preds, expect = genuine] ``` blanchet@33197 ` 71` ```oops ``` blanchet@33197 ` 72` haftmann@45970 ` 73` ```lemma "q2 = top" ``` 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 "\ 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 "\ 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 \ p4 (Suc n)" | ``` blanchet@33197 ` 109` ```"p4 n \ p3 (Suc n)" ``` blanchet@33197 ` 110` blanchet@33197 ` 111` ```coinductive q3 and q4 where ``` blanchet@33197 ` 112` ```"q3 0" | ``` blanchet@33197 ` 113` ```"q3 n \ q4 (Suc n)" | ``` blanchet@33197 ` 114` ```"q4 n \ 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` haftmann@45970 ` 126` ```lemma "p3 = top - p4" ``` blanchet@33197 ` 127` ```nitpick [expect = none] ``` blanchet@38186 ` 128` ```nitpick [non_wf, expect = none] ``` blanchet@33197 ` 129` ```sorry ``` blanchet@33197 ` 130` haftmann@45970 ` 131` ```lemma "q3 = top - q4" ``` blanchet@33197 ` 132` ```nitpick [expect = none] ``` blanchet@33197 ` 133` ```nitpick [non_wf, expect = none] ``` blanchet@33197 ` 134` ```sorry ``` blanchet@33197 ` 135` haftmann@45970 ` 136` ```lemma "inf p3 q4 \ bot" ``` blanchet@33197 ` 137` ```nitpick [expect = potential] ``` blanchet@33197 ` 138` ```nitpick [non_wf, expect = potential] ``` blanchet@33197 ` 139` ```sorry ``` blanchet@33197 ` 140` haftmann@45970 ` 141` ```lemma "inf q3 p4 \ bot" ``` blanchet@33197 ` 142` ```nitpick [expect = potential] ``` blanchet@33197 ` 143` ```nitpick [non_wf, expect = potential] ``` blanchet@33197 ` 144` ```sorry ``` blanchet@33197 ` 145` haftmann@45970 ` 146` ```lemma "sup p3 q4 \ top" ``` blanchet@33197 ` 147` ```nitpick [expect = potential] ``` blanchet@33197 ` 148` ```nitpick [non_wf, expect = potential] ``` blanchet@33197 ` 149` ```sorry ``` blanchet@33197 ` 150` haftmann@45970 ` 151` ```lemma "sup q3 p4 \ top" ``` 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 ```