src/HOL/Nitpick_Examples/Mono_Nits.thy
changeset 35191 69fa4c39dab2
parent 35076 cc19e2aef17e
child 35339 34819133c75e
equal deleted inserted replaced
35190:ce653cc27a94 35191:69fa4c39dab2
    27    intro_table = Symtab.empty, ground_thm_table = Inttab.empty,
    27    intro_table = Symtab.empty, ground_thm_table = Inttab.empty,
    28    ersatz_table = [], skolems = Unsynchronized.ref [],
    28    ersatz_table = [], skolems = Unsynchronized.ref [],
    29    special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
    29    special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
    30    wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
    30    wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
    31 (* term -> bool *)
    31 (* term -> bool *)
    32 val is_mono = Nitpick_Mono.formulas_monotonic hol_ctxt @{typ 'a}
    32 val is_mono = Nitpick_Mono.formulas_monotonic hol_ctxt false @{typ 'a}
    33                                               Nitpick_Mono.Plus [] []
    33                                               Nitpick_Mono.Plus [] []
    34 fun is_const t =
    34 fun is_const t =
    35   let val T = fastype_of t in
    35   let val T = fastype_of t in
    36     is_mono (Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t),
    36     is_mono (Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t),
    37                                @{const False}))
    37                                @{const False}))