|
(* Title: HOL/Nitpick_Examples/Induct_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
Copyright 2009-2011
Examples featuring Nitpick applied to (co)inductive definitions.
*)
section \<open>Examples Featuring Nitpick Applied to (Co)inductive Definitions\<close>
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
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
