(* Title: HOL/Nitpick_Examples/Induct_Nits.thy Author: Jasmin Blanchette, TU Muenchen Copyright 2009-2011 Examples featuring Nitpick applied to (co)inductive definitions. *) header {* Examples Featuring Nitpick Applied to (Co)inductive Definitions *} theory Induct_Nits imports Main begin nitpick_params [verbose, card = 1-8, unary_ints, sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240] inductive p1 :: "nat => bool" where "p1 0" | "p1 n ==> p1 (n + 2)" coinductive q1 :: "nat => bool" where "q1 0" | "q1 n ==> q1 (n + 2)" lemma "p1 = q1" nitpick [expect = none] nitpick [wf, expect = none] nitpick [non_wf, expect = none] nitpick [non_wf, dont_star_linear_preds, expect = none] oops lemma "p1 ≠ q1" nitpick [expect = potential] nitpick [wf, expect = potential] nitpick [non_wf, expect = potential] nitpick [non_wf, dont_star_linear_preds, expect = potential] oops lemma "p1 (n - 2) ==> p1 n" nitpick [expect = genuine] nitpick [non_wf, expect = genuine] nitpick [non_wf, dont_star_linear_preds, expect = genuine] oops lemma "q1 (n - 2) ==> q1 n" nitpick [expect = genuine] nitpick [non_wf, expect = genuine] nitpick [non_wf, dont_star_linear_preds, expect = genuine] oops inductive p2 :: "nat => bool" where "p2 n ==> p2 n" coinductive q2 :: "nat => bool" where "q2 n ==> q2 n" lemma "p2 = bot" nitpick [expect = none] nitpick [dont_star_linear_preds, expect = none] sorry lemma "q2 = bot" nitpick [expect = genuine] nitpick [dont_star_linear_preds, expect = genuine] nitpick [wf, expect = quasi_genuine] oops lemma "p2 = top" nitpick [expect = genuine] nitpick [dont_star_linear_preds, expect = genuine] oops lemma "q2 = top" nitpick [expect = none] nitpick [dont_star_linear_preds, expect = none] nitpick [wf, expect = quasi_genuine] sorry lemma "p2 = q2" nitpick [expect = genuine] nitpick [dont_star_linear_preds, expect = genuine] oops lemma "p2 n" nitpick [expect = genuine] nitpick [dont_star_linear_preds, expect = genuine] nitpick [dont_specialize, expect = genuine] oops lemma "q2 n" nitpick [expect = none] nitpick [dont_star_linear_preds, expect = none] sorry lemma "¬ p2 n" nitpick [expect = none] nitpick [dont_star_linear_preds, expect = none] sorry lemma "¬ q2 n" nitpick [expect = genuine] nitpick [dont_star_linear_preds, expect = genuine] nitpick [dont_specialize, expect = genuine] oops inductive p3 and p4 where "p3 0" | "p3 n ==> p4 (Suc n)" | "p4 n ==> p3 (Suc n)" coinductive q3 and q4 where "q3 0" | "q3 n ==> q4 (Suc n)" | "q4 n ==> q3 (Suc n)" lemma "p3 = q3" nitpick [expect = none] nitpick [non_wf, expect = none] sorry lemma "p4 = q4" nitpick [expect = none] nitpick [non_wf, expect = none] sorry lemma "p3 = top - p4" nitpick [expect = none] nitpick [non_wf, expect = none] sorry lemma "q3 = top - q4" nitpick [expect = none] nitpick [non_wf, expect = none] sorry lemma "inf p3 q4 ≠ bot" nitpick [expect = potential] nitpick [non_wf, expect = potential] sorry lemma "inf q3 p4 ≠ bot" nitpick [expect = potential] nitpick [non_wf, expect = potential] sorry lemma "sup p3 q4 ≠ top" nitpick [expect = potential] nitpick [non_wf, expect = potential] sorry lemma "sup q3 p4 ≠ top" nitpick [expect = potential] nitpick [non_wf, expect = potential] sorry end