src/HOL/Nitpick_Examples/Mono_Nits.thy
author wenzelm
Tue Oct 10 19:23:03 2017 +0200 (2017-10-10)
changeset 66831 29ea2b900a05
parent 65458 cf504b7a7aa7
child 67399 eab6ce8368fa
permissions -rw-r--r--
tuned: each session has at most one defining entry;
blanchet@33197
     1
(*  Title:      HOL/Nitpick_Examples/Mono_Nits.thy
blanchet@33197
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@45035
     3
    Copyright   2009-2011
blanchet@33197
     4
blanchet@33197
     5
Examples featuring Nitpick's monotonicity check.
blanchet@33197
     6
*)
blanchet@33197
     7
wenzelm@63167
     8
section \<open>Examples Featuring Nitpick's Monotonicity Check\<close>
blanchet@33197
     9
blanchet@33197
    10
theory Mono_Nits
blanchet@46082
    11
imports Main
blanchet@46082
    12
        (* "~/afp/thys/DPT-SAT-Solver/DPT_SAT_Solver" *)
blanchet@46082
    13
        (* "~/afp/thys/AVL-Trees/AVL2" "~/afp/thys/Huffman/Huffman" *)
blanchet@33197
    14
begin
blanchet@33197
    15
wenzelm@63167
    16
ML \<open>
blanchet@41008
    17
open Nitpick_Util
blanchet@41008
    18
open Nitpick_HOL
blanchet@41010
    19
open Nitpick_Preproc
blanchet@41008
    20
blanchet@40992
    21
exception BUG
blanchet@33197
    22
blanchet@41008
    23
val thy = @{theory}
blanchet@41008
    24
val ctxt = @{context}
blanchet@35339
    25
val subst = []
blanchet@54833
    26
val tac_timeout = seconds 1.0
blanchet@55888
    27
val case_names = case_const_names ctxt
blanchet@42415
    28
val defs = all_defs_of thy subst
blanchet@42415
    29
val nondefs = all_nondefs_of ctxt subst
blanchet@41791
    30
val def_tables = const_def_tables ctxt subst defs
blanchet@42415
    31
val nondef_table = const_nondef_table nondefs
blanchet@41008
    32
val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
blanchet@41008
    33
val psimp_table = const_psimp_table ctxt subst
blanchet@41008
    34
val choice_spec_table = const_choice_spec_table ctxt subst
blanchet@41791
    35
val intro_table = inductive_intro_table ctxt subst def_tables
blanchet@41008
    36
val ground_thm_table = ground_theorem_table thy
blanchet@41008
    37
val ersatz_table = ersatz_table ctxt
wenzelm@41410
    38
val hol_ctxt as {thy, ...} : hol_context =
blanchet@55888
    39
  {thy = thy, ctxt = ctxt, max_bisim_depth = ~1, boxes = [], wfs = [],
blanchet@55888
    40
   user_axioms = NONE, debug = false, whacks = [], binary_ints = SOME false,
blanchet@55888
    41
   destroy_constrs = true, specialize = false, star_linear_preds = false,
blanchet@55888
    42
   total_consts = NONE, needs = NONE, tac_timeout = tac_timeout, evals = [],
blanchet@55888
    43
   case_names = case_names, def_tables = def_tables,
blanchet@55888
    44
   nondef_table = nondef_table, nondefs = nondefs, simp_table = simp_table,
blanchet@55888
    45
   psimp_table = psimp_table, choice_spec_table = choice_spec_table,
blanchet@55888
    46
   intro_table = intro_table, ground_thm_table = ground_thm_table,
blanchet@55888
    47
   ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
blanchet@55888
    48
   special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
blanchet@55888
    49
   wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
blanchet@41008
    50
val binarize = false
blanchet@41008
    51
blanchet@35812
    52
fun is_mono t =
blanchet@41008
    53
  Nitpick_Mono.formulas_monotonic hol_ctxt binarize @{typ 'a} ([t], [])
blanchet@41008
    54
blanchet@33197
    55
fun is_const t =
blanchet@46082
    56
  let val T = fastype_of t in
blanchet@46082
    57
    Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t), @{const False})
blanchet@46082
    58
    |> is_mono
blanchet@33197
    59
  end
blanchet@41008
    60
blanchet@40992
    61
fun mono t = is_mono t orelse raise BUG
blanchet@40992
    62
fun nonmono t = not (is_mono t) orelse raise BUG
blanchet@40992
    63
fun const t = is_const t orelse raise BUG
blanchet@40992
    64
fun nonconst t = not (is_const t) orelse raise BUG
wenzelm@63167
    65
\<close>
blanchet@33197
    66
wenzelm@63167
    67
ML \<open>Nitpick_Mono.trace := false\<close>
blanchet@41006
    68
wenzelm@63167
    69
ML_val \<open>const @{term "A::('a\<Rightarrow>'b)"}\<close>
wenzelm@63167
    70
ML_val \<open>const @{term "(A::'a set) = A"}\<close>
wenzelm@63167
    71
ML_val \<open>const @{term "(A::'a set set) = A"}\<close>
wenzelm@63167
    72
ML_val \<open>const @{term "(\<lambda>x::'a set. a \<in> x)"}\<close>
wenzelm@63167
    73
ML_val \<open>const @{term "{{a::'a}} = C"}\<close>
wenzelm@63167
    74
ML_val \<open>const @{term "{f::'a\<Rightarrow>nat} = {g::'a\<Rightarrow>nat}"}\<close>
wenzelm@63167
    75
ML_val \<open>const @{term "A \<union> (B::'a set)"}\<close>
wenzelm@63167
    76
ML_val \<open>const @{term "\<lambda>A B x::'a. A x \<or> B x"}\<close>
wenzelm@63167
    77
ML_val \<open>const @{term "P (a::'a)"}\<close>
wenzelm@63167
    78
ML_val \<open>const @{term "\<lambda>a::'a. b (c (d::'a)) (e::'a) (f::'a)"}\<close>
wenzelm@63167
    79
ML_val \<open>const @{term "\<forall>A::'a set. a \<in> A"}\<close>
wenzelm@63167
    80
ML_val \<open>const @{term "\<forall>A::'a set. P A"}\<close>
wenzelm@63167
    81
ML_val \<open>const @{term "P \<or> Q"}\<close>
wenzelm@63167
    82
ML_val \<open>const @{term "A \<union> B = (C::'a set)"}\<close>
wenzelm@63167
    83
ML_val \<open>const @{term "(\<lambda>A B x::'a. A x \<or> B x) A B = C"}\<close>
wenzelm@63167
    84
ML_val \<open>const @{term "(if P then (A::'a set) else B) = C"}\<close>
wenzelm@63167
    85
ML_val \<open>const @{term "let A = (C::'a set) in A \<union> B"}\<close>
wenzelm@63167
    86
ML_val \<open>const @{term "THE x::'b. P x"}\<close>
wenzelm@63167
    87
ML_val \<open>const @{term "(\<lambda>x::'a. False)"}\<close>
wenzelm@63167
    88
ML_val \<open>const @{term "(\<lambda>x::'a. True)"}\<close>
wenzelm@63167
    89
ML_val \<open>const @{term "(\<lambda>x::'a. False) = (\<lambda>x::'a. False)"}\<close>
wenzelm@63167
    90
ML_val \<open>const @{term "(\<lambda>x::'a. True) = (\<lambda>x::'a. True)"}\<close>
wenzelm@63167
    91
ML_val \<open>const @{term "Let (a::'a) A"}\<close>
wenzelm@63167
    92
ML_val \<open>const @{term "A (a::'a)"}\<close>
wenzelm@63167
    93
ML_val \<open>const @{term "insert (a::'a) A = B"}\<close>
wenzelm@63167
    94
ML_val \<open>const @{term "- (A::'a set)"}\<close>
wenzelm@63167
    95
ML_val \<open>const @{term "finite (A::'a set)"}\<close>
wenzelm@63167
    96
ML_val \<open>const @{term "\<not> finite (A::'a set)"}\<close>
wenzelm@63167
    97
ML_val \<open>const @{term "finite (A::'a set set)"}\<close>
wenzelm@63167
    98
ML_val \<open>const @{term "\<lambda>a::'a. A a \<and> \<not> B a"}\<close>
wenzelm@63167
    99
ML_val \<open>const @{term "A < (B::'a set)"}\<close>
wenzelm@63167
   100
ML_val \<open>const @{term "A \<le> (B::'a set)"}\<close>
wenzelm@63167
   101
ML_val \<open>const @{term "[a::'a]"}\<close>
wenzelm@63167
   102
ML_val \<open>const @{term "[a::'a set]"}\<close>
wenzelm@63167
   103
ML_val \<open>const @{term "[A \<union> (B::'a set)]"}\<close>
wenzelm@63167
   104
ML_val \<open>const @{term "[A \<union> (B::'a set)] = [C]"}\<close>
wenzelm@63167
   105
ML_val \<open>const @{term "{(\<lambda>x::'a. x = a)} = C"}\<close>
wenzelm@63167
   106
ML_val \<open>const @{term "(\<lambda>a::'a. \<not> A a) = B"}\<close>
wenzelm@63167
   107
ML_val \<open>const @{prop "\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> \<not> f a"}\<close>
wenzelm@63167
   108
ML_val \<open>const @{term "\<lambda>A B x::'a. A x \<and> B x \<and> A = B"}\<close>
wenzelm@63167
   109
ML_val \<open>const @{term "p = (\<lambda>(x::'a) (y::'a). P x \<or> \<not> Q y)"}\<close>
wenzelm@63167
   110
ML_val \<open>const @{term "p = (\<lambda>(x::'a) (y::'a). p x y :: bool)"}\<close>
wenzelm@63167
   111
ML_val \<open>const @{term "p = (\<lambda>A B x. A x \<and> \<not> B x) (\<lambda>x. True) (\<lambda>y. x \<noteq> y)"}\<close>
wenzelm@63167
   112
ML_val \<open>const @{term "p = (\<lambda>y. x \<noteq> y)"}\<close>
wenzelm@63167
   113
ML_val \<open>const @{term "(\<lambda>x. (p::'a\<Rightarrow>bool\<Rightarrow>bool) x False)"}\<close>
wenzelm@63167
   114
ML_val \<open>const @{term "(\<lambda>x y. (p::'a\<Rightarrow>'a\<Rightarrow>bool\<Rightarrow>bool) x y False)"}\<close>
wenzelm@63167
   115
ML_val \<open>const @{term "f = (\<lambda>x::'a. P x \<longrightarrow> Q x)"}\<close>
wenzelm@63167
   116
ML_val \<open>const @{term "\<forall>a::'a. P a"}\<close>
blanchet@33197
   117
wenzelm@63167
   118
ML_val \<open>nonconst @{term "\<forall>P (a::'a). P a"}\<close>
wenzelm@63167
   119
ML_val \<open>nonconst @{term "THE x::'a. P x"}\<close>
wenzelm@63167
   120
ML_val \<open>nonconst @{term "SOME x::'a. P x"}\<close>
wenzelm@63167
   121
ML_val \<open>nonconst @{term "(\<lambda>A B x::'a. A x \<or> B x) = myunion"}\<close>
wenzelm@63167
   122
ML_val \<open>nonconst @{term "(\<lambda>x::'a. False) = (\<lambda>x::'a. True)"}\<close>
wenzelm@63167
   123
ML_val \<open>nonconst @{prop "\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h"}\<close>
blanchet@33197
   124
wenzelm@63167
   125
ML_val \<open>mono @{prop "Q (\<forall>x::'a set. P x)"}\<close>
wenzelm@63167
   126
ML_val \<open>mono @{prop "P (a::'a)"}\<close>
wenzelm@63167
   127
ML_val \<open>mono @{prop "{a} = {b::'a}"}\<close>
wenzelm@63167
   128
ML_val \<open>mono @{prop "(\<lambda>x. x = a) = (\<lambda>y. y = (b::'a))"}\<close>
wenzelm@63167
   129
ML_val \<open>mono @{prop "(a::'a) \<in> P \<and> P \<union> P = P"}\<close>
wenzelm@63167
   130
ML_val \<open>mono @{prop "\<forall>F::'a set set. P"}\<close>
wenzelm@63167
   131
ML_val \<open>mono @{prop "\<not> (\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h)"}\<close>
wenzelm@63167
   132
ML_val \<open>mono @{prop "\<not> Q (\<forall>x::'a set. P x)"}\<close>
wenzelm@63167
   133
ML_val \<open>mono @{prop "\<not> (\<forall>x::'a. P x)"}\<close>
wenzelm@63167
   134
ML_val \<open>mono @{prop "myall P = (P = (\<lambda>x::'a. True))"}\<close>
wenzelm@63167
   135
ML_val \<open>mono @{prop "myall P = (P = (\<lambda>x::'a. False))"}\<close>
wenzelm@63167
   136
ML_val \<open>mono @{prop "\<forall>x::'a. P x"}\<close>
wenzelm@63167
   137
ML_val \<open>mono @{term "(\<lambda>A B x::'a. A x \<or> B x) \<noteq> myunion"}\<close>
blanchet@33197
   138
wenzelm@63167
   139
ML_val \<open>nonmono @{prop "A = (\<lambda>x::'a. True) \<and> A = (\<lambda>x. False)"}\<close>
wenzelm@63167
   140
ML_val \<open>nonmono @{prop "\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h"}\<close>
blanchet@33197
   141
wenzelm@63167
   142
ML \<open>
blanchet@54833
   143
val preproc_timeout = seconds 5.0
blanchet@54833
   144
val mono_timeout = seconds 1.0
blanchet@41008
   145
blanchet@41008
   146
fun is_forbidden_theorem name =
wenzelm@46711
   147
  length (Long_Name.explode name) <> 2 orelse
wenzelm@46711
   148
  String.isPrefix "type_definition" (List.last (Long_Name.explode name)) orelse
wenzelm@46711
   149
  String.isPrefix "arity_" (List.last (Long_Name.explode name)) orelse
blanchet@41008
   150
  String.isSuffix "_def" name orelse
blanchet@41008
   151
  String.isSuffix "_raw" name
blanchet@41008
   152
blanchet@41008
   153
fun theorems_of thy =
blanchet@41008
   154
  filter (fn (name, th) =>
blanchet@41008
   155
             not (is_forbidden_theorem name) andalso
wenzelm@65458
   156
             Thm.theory_name th = Context.theory_name thy)
blanchet@56374
   157
         (Global_Theory.all_thms_of thy true)
blanchet@41008
   158
blanchet@41010
   159
fun check_formulas tsp =
blanchet@41008
   160
  let
blanchet@41008
   161
    fun is_type_actually_monotonic T =
blanchet@41010
   162
      Nitpick_Mono.formulas_monotonic hol_ctxt binarize T tsp
blanchet@41010
   163
    val free_Ts = fold Term.add_tfrees (op @ tsp) [] |> map TFree
blanchet@41008
   164
    val (mono_free_Ts, nonmono_free_Ts) =
wenzelm@62519
   165
      Timeout.apply mono_timeout
blanchet@54833
   166
          (List.partition is_type_actually_monotonic) free_Ts
blanchet@41008
   167
  in
blanchet@41008
   168
    if not (null mono_free_Ts) then "MONO"
blanchet@41008
   169
    else if not (null nonmono_free_Ts) then "NONMONO"
blanchet@41008
   170
    else "NIX"
blanchet@41008
   171
  end
wenzelm@62519
   172
  handle Timeout.TIMEOUT _ => "TIMEOUT"
blanchet@41008
   173
       | NOT_SUPPORTED _ => "UNSUP"
wenzelm@62505
   174
       | exn => if Exn.is_interrupt exn then Exn.reraise exn else "UNKNOWN"
blanchet@41008
   175
blanchet@41008
   176
fun check_theory thy =
blanchet@41008
   177
  let
blanchet@41008
   178
    val path = File.tmp_path (Context.theory_name thy ^ ".out" |> Path.explode)
blanchet@41008
   179
    val _ = File.write path ""
blanchet@41008
   180
    fun check_theorem (name, th) =
blanchet@41008
   181
      let
wenzelm@59582
   182
        val t = th |> Thm.prop_of |> Type.legacy_freeze |> close_form
blanchet@41008
   183
        val neg_t = Logic.mk_implies (t, @{prop False})
blanchet@41805
   184
        val (nondef_ts, def_ts, _, _, _, _) =
wenzelm@62519
   185
          Timeout.apply preproc_timeout (preprocess_formulas hol_ctxt [])
blanchet@54833
   186
                              neg_t
blanchet@41010
   187
        val res = name ^ ": " ^ check_formulas (nondef_ts, def_ts)
blanchet@41008
   188
      in File.append path (res ^ "\n"); writeln res end
wenzelm@62519
   189
      handle Timeout.TIMEOUT _ => ()
blanchet@41008
   190
  in thy |> theorems_of |> List.app check_theorem end
wenzelm@63167
   191
\<close>
blanchet@41008
   192
blanchet@41015
   193
(*
wenzelm@51272
   194
ML_val {* check_theory @{theory AVL2} *}
wenzelm@51272
   195
ML_val {* check_theory @{theory Fun} *}
wenzelm@51272
   196
ML_val {* check_theory @{theory Huffman} *}
wenzelm@51272
   197
ML_val {* check_theory @{theory List} *}
wenzelm@51272
   198
ML_val {* check_theory @{theory Map} *}
wenzelm@51272
   199
ML_val {* check_theory @{theory Relation} *}
blanchet@41015
   200
*)
blanchet@41015
   201
wenzelm@63167
   202
ML \<open>getenv "ISABELLE_TMP"\<close>
blanchet@41008
   203
blanchet@33197
   204
end