src/HOL/Nitpick_Examples/Mono_Nits.thy
author blanchet
Fri Feb 05 14:27:21 2010 +0100 (2010-02-05)
changeset 35076 cc19e2aef17e
parent 35071 3df45b0ce819
child 35191 69fa4c39dab2
permissions -rw-r--r--
added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
     1 (*  Title:      HOL/Nitpick_Examples/Mono_Nits.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2009, 2010
     4 
     5 Examples featuring Nitpick's monotonicity check.
     6 *)
     7 
     8 header {* Examples Featuring Nitpick's Monotonicity Check *}
     9 
    10 theory Mono_Nits
    11 imports Main
    12 begin
    13 
    14 ML {*
    15 exception FAIL
    16 
    17 val defs = Nitpick_HOL.all_axioms_of @{theory} |> #1
    18 val def_table = Nitpick_HOL.const_def_table @{context} defs
    19 val hol_ctxt : Nitpick_HOL.hol_context =
    20   {thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [],
    21    stds = [(NONE, true)], wfs = [], user_axioms = NONE, debug = false,
    22    binary_ints = SOME false, destroy_constrs = false, specialize = false,
    23    skolemize = false, star_linear_preds = false, uncurry = false,
    24    fast_descrs = false, tac_timeout = NONE, evals = [], case_names = [],
    25    def_table = def_table, nondef_table = Symtab.empty, user_nondefs = [],
    26    simp_table = Unsynchronized.ref Symtab.empty, psimp_table = Symtab.empty,
    27    intro_table = Symtab.empty, ground_thm_table = Inttab.empty,
    28    ersatz_table = [], skolems = Unsynchronized.ref [],
    29    special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
    30    wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
    31 (* term -> bool *)
    32 val is_mono = Nitpick_Mono.formulas_monotonic hol_ctxt @{typ 'a}
    33                                               Nitpick_Mono.Plus [] []
    34 fun is_const t =
    35   let val T = fastype_of t in
    36     is_mono (Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t),
    37                                @{const False}))
    38   end
    39 fun mono t = is_mono t orelse raise FAIL
    40 fun nonmono t = not (is_mono t) orelse raise FAIL
    41 fun const t = is_const t orelse raise FAIL
    42 fun nonconst t = not (is_const t) orelse raise FAIL
    43 *}
    44 
    45 ML {* const @{term "A::('a\<Rightarrow>'b)"} *}
    46 ML {* const @{term "(A::'a set) = A"} *}
    47 ML {* const @{term "(A::'a set set) = A"} *}
    48 ML {* const @{term "(\<lambda>x::'a set. x a)"} *}
    49 ML {* const @{term "{{a}} = C"} *}
    50 ML {* const @{term "{f::'a\<Rightarrow>nat} = {g::'a\<Rightarrow>nat}"} *}
    51 ML {* const @{term "A \<union> B"} *}
    52 ML {* const @{term "P (a::'a)"} *}
    53 ML {* const @{term "\<lambda>a::'a. b (c (d::'a)) (e::'a) (f::'a)"} *}
    54 ML {* const @{term "\<forall>A::'a set. A a"} *}
    55 ML {* const @{term "\<forall>A::'a set. P A"} *}
    56 ML {* const @{term "P \<or> Q"} *}
    57 ML {* const @{term "A \<union> B = C"} *}
    58 ML {* const @{term "(if P then (A::'a set) else B) = C"} *}
    59 ML {* const @{term "let A = C in A \<union> B"} *}
    60 ML {* const @{term "THE x::'b. P x"} *}
    61 ML {* const @{term "{}::'a set"} *}
    62 ML {* const @{term "(\<lambda>x::'a. True)"} *}
    63 ML {* const @{term "Let a A"} *}
    64 ML {* const @{term "A (a::'a)"} *}
    65 ML {* const @{term "insert a A = B"} *}
    66 ML {* const @{term "- (A::'a set)"} *}
    67 ML {* const @{term "finite A"} *}
    68 ML {* const @{term "\<not> finite A"} *}
    69 ML {* const @{term "finite (A::'a set set)"} *}
    70 ML {* const @{term "\<lambda>a::'a. A a \<and> \<not> B a"} *}
    71 ML {* const @{term "A < (B::'a set)"} *}
    72 ML {* const @{term "A \<le> (B::'a set)"} *}
    73 ML {* const @{term "[a::'a]"} *}
    74 ML {* const @{term "[a::'a set]"} *}
    75 ML {* const @{term "[A \<union> (B::'a set)]"} *}
    76 ML {* const @{term "[A \<union> (B::'a set)] = [C]"} *}
    77 ML {* const @{term "\<forall>P. P a"} *}
    78 
    79 ML {* nonconst @{term "{%x. True}"} *}
    80 ML {* nonconst @{term "{(%x. x = a)} = C"} *}
    81 ML {* nonconst @{term "\<forall>P (a::'a). P a"} *}
    82 ML {* nonconst @{term "\<forall>a::'a. P a"} *}
    83 ML {* nonconst @{term "(\<lambda>a::'a. \<not> A a) = B"} *}
    84 ML {* nonconst @{term "THE x. P x"} *}
    85 ML {* nonconst @{term "SOME x. P x"} *}
    86 
    87 ML {* mono @{prop "Q (\<forall>x::'a set. P x)"} *}
    88 ML {* mono @{prop "P (a::'a)"} *}
    89 ML {* mono @{prop "{a} = {b}"} *}
    90 ML {* mono @{prop "P (a::'a) \<and> P \<union> P = P"} *}
    91 ML {* mono @{prop "\<forall>F::'a set set. P"} *}
    92 ML {* mono @{prop "\<not> (\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> F h)"} *}
    93 ML {* mono @{prop "\<not> Q (\<forall>x::'a set. P x)"} *}
    94 ML {* mono @{prop "\<not> (\<forall>x. P x)"} *}
    95 
    96 ML {* nonmono @{prop "\<forall>x. P x"} *}
    97 ML {* nonmono @{prop "\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> F h"} *}
    98 ML {* nonmono @{prop "myall P = (P = (\<lambda>x. True))"} *}
    99 
   100 end