Theory Induct_Nits

(*  Title:      HOL/Nitpick_Examples/Induct_Nits.thy
    Author:     Jasmin Blanchette, TU Muenchen
    Copyright   2009-2011

Examples featuring Nitpick applied to (co)inductive definitions.
*)

section ‹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, 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