(* Title: HOL/Nitpick_Examples/Mono_Nits.thy Author: Jasmin Blanchette, TU Muenchen Copyright 2009, 2010 Examples featuring Nitpick's monotonicity check. *) header {* Examples Featuring Nitpick's Monotonicity Check *} theory Mono_Nits imports Main begin ML {* exception FAIL val defs = Nitpick_HOL.all_axioms_of @{theory} |> #1 val def_table = Nitpick_HOL.const_def_table @{context} defs val hol_ctxt : Nitpick_HOL.hol_context = {thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [], stds = [(NONE, true)], wfs = [], user_axioms = NONE, debug = false, binary_ints = SOME false, destroy_constrs = false, specialize = false, skolemize = false, star_linear_preds = false, uncurry = false, fast_descrs = false, tac_timeout = NONE, evals = [], case_names = [], def_table = def_table, nondef_table = Symtab.empty, user_nondefs = [], simp_table = Unsynchronized.ref Symtab.empty, psimp_table = Symtab.empty, intro_table = Symtab.empty, ground_thm_table = Inttab.empty, ersatz_table = [], skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []} (* term -> bool *) val is_mono = Nitpick_Mono.formulas_monotonic hol_ctxt false @{typ 'a} Nitpick_Mono.Plus [] [] fun is_const t = let val T = fastype_of t in is_mono (Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t), @{const False})) end fun mono t = is_mono t orelse raise FAIL fun nonmono t = not (is_mono t) orelse raise FAIL fun const t = is_const t orelse raise FAIL fun nonconst t = not (is_const t) orelse raise FAIL *} ML {* const @{term "A::('a\'b)"} *} ML {* const @{term "(A::'a set) = A"} *} ML {* const @{term "(A::'a set set) = A"} *} ML {* const @{term "(\x::'a set. x a)"} *} ML {* const @{term "{{a}} = C"} *} ML {* const @{term "{f::'a\nat} = {g::'a\nat}"} *} ML {* const @{term "A \ B"} *} ML {* const @{term "P (a::'a)"} *} ML {* const @{term "\a::'a. b (c (d::'a)) (e::'a) (f::'a)"} *} ML {* const @{term "\A::'a set. A a"} *} ML {* const @{term "\A::'a set. P A"} *} ML {* const @{term "P \ Q"} *} ML {* const @{term "A \ B = C"} *} ML {* const @{term "(if P then (A::'a set) else B) = C"} *} ML {* const @{term "let A = C in A \ B"} *} ML {* const @{term "THE x::'b. P x"} *} ML {* const @{term "{}::'a set"} *} ML {* const @{term "(\x::'a. True)"} *} ML {* const @{term "Let a A"} *} ML {* const @{term "A (a::'a)"} *} ML {* const @{term "insert a A = B"} *} ML {* const @{term "- (A::'a set)"} *} ML {* const @{term "finite A"} *} ML {* const @{term "\ finite A"} *} ML {* const @{term "finite (A::'a set set)"} *} ML {* const @{term "\a::'a. A a \ \ B a"} *} ML {* const @{term "A < (B::'a set)"} *} ML {* const @{term "A \ (B::'a set)"} *} ML {* const @{term "[a::'a]"} *} ML {* const @{term "[a::'a set]"} *} ML {* const @{term "[A \ (B::'a set)]"} *} ML {* const @{term "[A \ (B::'a set)] = [C]"} *} ML {* const @{term "\P. P a"} *} ML {* nonconst @{term "{%x. True}"} *} ML {* nonconst @{term "{(%x. x = a)} = C"} *} ML {* nonconst @{term "\P (a::'a). P a"} *} ML {* nonconst @{term "\a::'a. P a"} *} ML {* nonconst @{term "(\a::'a. \ A a) = B"} *} ML {* nonconst @{term "THE x. P x"} *} ML {* nonconst @{term "SOME x. P x"} *} ML {* mono @{prop "Q (\x::'a set. P x)"} *} ML {* mono @{prop "P (a::'a)"} *} ML {* mono @{prop "{a} = {b}"} *} ML {* mono @{prop "P (a::'a) \ P \ P = P"} *} ML {* mono @{prop "\F::'a set set. P"} *} ML {* mono @{prop "\ (\F f g (h::'a set). F f \ F g \ \ f a \ g a \ F h)"} *} ML {* mono @{prop "\ Q (\x::'a set. P x)"} *} ML {* mono @{prop "\ (\x. P x)"} *} ML {* nonmono @{prop "\x. P x"} *} ML {* nonmono @{prop "\F f g (h::'a set). F f \ F g \ \ f a \ g a \ F h"} *} ML {* nonmono @{prop "myall P = (P = (\x. True))"} *} end