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