src/HOL/Nitpick_Examples/Mono_Nits.thy
author hoelzl
Fri Mar 22 10:41:43 2013 +0100 (2013-03-22)
changeset 51474 1e9e68247ad1
parent 51272 9c8d63b4b6be
child 54833 68c8f88af87e
permissions -rw-r--r--
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
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
blanchet@33197
     8
header {* Examples Featuring Nitpick's Monotonicity Check *}
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
blanchet@33197
    16
ML {*
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@41008
    25
val stds = [(NONE, true)]
blanchet@35339
    26
val subst = []
blanchet@41008
    27
val case_names = case_const_names ctxt stds
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@41008
    39
  {thy = thy, ctxt = ctxt, max_bisim_depth = ~1, boxes = [],
blanchet@41008
    40
   stds = stds, wfs = [], user_axioms = NONE, debug = false,
blanchet@41010
    41
   whacks = [], binary_ints = SOME false, destroy_constrs = true,
blanchet@41871
    42
   specialize = false, star_linear_preds = false, total_consts = NONE,
blanchet@41876
    43
   needs = NONE, tac_timeout = NONE, evals = [], case_names = case_names,
blanchet@42415
    44
   def_tables = def_tables, nondef_table = nondef_table, nondefs = nondefs,
blanchet@42415
    45
   simp_table = simp_table, psimp_table = psimp_table,
blanchet@42415
    46
   choice_spec_table = choice_spec_table, intro_table = intro_table,
blanchet@42415
    47
   ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
blanchet@42415
    48
   skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
blanchet@42415
    49
   unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
blanchet@42415
    50
   constr_cache = Unsynchronized.ref []}
blanchet@41008
    51
val binarize = false
blanchet@41008
    52
blanchet@35812
    53
fun is_mono t =
blanchet@41008
    54
  Nitpick_Mono.formulas_monotonic hol_ctxt binarize @{typ 'a} ([t], [])
blanchet@41008
    55
blanchet@33197
    56
fun is_const t =
blanchet@46082
    57
  let val T = fastype_of t in
blanchet@46082
    58
    Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t), @{const False})
blanchet@46082
    59
    |> is_mono
blanchet@33197
    60
  end
blanchet@41008
    61
blanchet@40992
    62
fun mono t = is_mono t orelse raise BUG
blanchet@40992
    63
fun nonmono t = not (is_mono t) orelse raise BUG
blanchet@40992
    64
fun const t = is_const t orelse raise BUG
blanchet@40992
    65
fun nonconst t = not (is_const t) orelse raise BUG
blanchet@33197
    66
*}
blanchet@33197
    67
blanchet@41006
    68
ML {* Nitpick_Mono.trace := false *}
blanchet@41006
    69
wenzelm@51272
    70
ML_val {* const @{term "A\<Colon>('a\<Rightarrow>'b)"} *}
wenzelm@51272
    71
ML_val {* const @{term "(A\<Colon>'a set) = A"} *}
wenzelm@51272
    72
ML_val {* const @{term "(A\<Colon>'a set set) = A"} *}
wenzelm@51272
    73
ML_val {* const @{term "(\<lambda>x\<Colon>'a set. a \<in> x)"} *}
wenzelm@51272
    74
ML_val {* const @{term "{{a\<Colon>'a}} = C"} *}
wenzelm@51272
    75
ML_val {* const @{term "{f\<Colon>'a\<Rightarrow>nat} = {g\<Colon>'a\<Rightarrow>nat}"} *}
wenzelm@51272
    76
ML_val {* const @{term "A \<union> (B\<Colon>'a set)"} *}
wenzelm@51272
    77
ML_val {* const @{term "\<lambda>A B x\<Colon>'a. A x \<or> B x"} *}
wenzelm@51272
    78
ML_val {* const @{term "P (a\<Colon>'a)"} *}
wenzelm@51272
    79
ML_val {* const @{term "\<lambda>a\<Colon>'a. b (c (d\<Colon>'a)) (e\<Colon>'a) (f\<Colon>'a)"} *}
wenzelm@51272
    80
ML_val {* const @{term "\<forall>A\<Colon>'a set. a \<in> A"} *}
wenzelm@51272
    81
ML_val {* const @{term "\<forall>A\<Colon>'a set. P A"} *}
wenzelm@51272
    82
ML_val {* const @{term "P \<or> Q"} *}
wenzelm@51272
    83
ML_val {* const @{term "A \<union> B = (C\<Colon>'a set)"} *}
wenzelm@51272
    84
ML_val {* const @{term "(\<lambda>A B x\<Colon>'a. A x \<or> B x) A B = C"} *}
wenzelm@51272
    85
ML_val {* const @{term "(if P then (A\<Colon>'a set) else B) = C"} *}
wenzelm@51272
    86
ML_val {* const @{term "let A = (C\<Colon>'a set) in A \<union> B"} *}
wenzelm@51272
    87
ML_val {* const @{term "THE x\<Colon>'b. P x"} *}
wenzelm@51272
    88
ML_val {* const @{term "(\<lambda>x\<Colon>'a. False)"} *}
wenzelm@51272
    89
ML_val {* const @{term "(\<lambda>x\<Colon>'a. True)"} *}
wenzelm@51272
    90
ML_val {* const @{term "(\<lambda>x\<Colon>'a. False) = (\<lambda>x\<Colon>'a. False)"} *}
wenzelm@51272
    91
ML_val {* const @{term "(\<lambda>x\<Colon>'a. True) = (\<lambda>x\<Colon>'a. True)"} *}
wenzelm@51272
    92
ML_val {* const @{term "Let (a\<Colon>'a) A"} *}
wenzelm@51272
    93
ML_val {* const @{term "A (a\<Colon>'a)"} *}
wenzelm@51272
    94
ML_val {* const @{term "insert (a\<Colon>'a) A = B"} *}
wenzelm@51272
    95
ML_val {* const @{term "- (A\<Colon>'a set)"} *}
wenzelm@51272
    96
ML_val {* const @{term "finite (A\<Colon>'a set)"} *}
wenzelm@51272
    97
ML_val {* const @{term "\<not> finite (A\<Colon>'a set)"} *}
wenzelm@51272
    98
ML_val {* const @{term "finite (A\<Colon>'a set set)"} *}
wenzelm@51272
    99
ML_val {* const @{term "\<lambda>a\<Colon>'a. A a \<and> \<not> B a"} *}
wenzelm@51272
   100
ML_val {* const @{term "A < (B\<Colon>'a set)"} *}
wenzelm@51272
   101
ML_val {* const @{term "A \<le> (B\<Colon>'a set)"} *}
wenzelm@51272
   102
ML_val {* const @{term "[a\<Colon>'a]"} *}
wenzelm@51272
   103
ML_val {* const @{term "[a\<Colon>'a set]"} *}
wenzelm@51272
   104
ML_val {* const @{term "[A \<union> (B\<Colon>'a set)]"} *}
wenzelm@51272
   105
ML_val {* const @{term "[A \<union> (B\<Colon>'a set)] = [C]"} *}
wenzelm@51272
   106
ML_val {* const @{term "{(\<lambda>x\<Colon>'a. x = a)} = C"} *}
wenzelm@51272
   107
ML_val {* const @{term "(\<lambda>a\<Colon>'a. \<not> A a) = B"} *}
wenzelm@51272
   108
ML_val {* const @{prop "\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> \<not> f a"} *}
wenzelm@51272
   109
ML_val {* const @{term "\<lambda>A B x\<Colon>'a. A x \<and> B x \<and> A = B"} *}
wenzelm@51272
   110
ML_val {* const @{term "p = (\<lambda>(x\<Colon>'a) (y\<Colon>'a). P x \<or> \<not> Q y)"} *}
wenzelm@51272
   111
ML_val {* const @{term "p = (\<lambda>(x\<Colon>'a) (y\<Colon>'a). p x y \<Colon> bool)"} *}
wenzelm@51272
   112
ML_val {* const @{term "p = (\<lambda>A B x. A x \<and> \<not> B x) (\<lambda>x. True) (\<lambda>y. x \<noteq> y)"} *}
wenzelm@51272
   113
ML_val {* const @{term "p = (\<lambda>y. x \<noteq> y)"} *}
wenzelm@51272
   114
ML_val {* const @{term "(\<lambda>x. (p\<Colon>'a\<Rightarrow>bool\<Rightarrow>bool) x False)"} *}
wenzelm@51272
   115
ML_val {* const @{term "(\<lambda>x y. (p\<Colon>'a\<Rightarrow>'a\<Rightarrow>bool\<Rightarrow>bool) x y False)"} *}
wenzelm@51272
   116
ML_val {* const @{term "f = (\<lambda>x\<Colon>'a. P x \<longrightarrow> Q x)"} *}
wenzelm@51272
   117
ML_val {* const @{term "\<forall>a\<Colon>'a. P a"} *}
blanchet@33197
   118
wenzelm@51272
   119
ML_val {* nonconst @{term "\<forall>P (a\<Colon>'a). P a"} *}
wenzelm@51272
   120
ML_val {* nonconst @{term "THE x\<Colon>'a. P x"} *}
wenzelm@51272
   121
ML_val {* nonconst @{term "SOME x\<Colon>'a. P x"} *}
wenzelm@51272
   122
ML_val {* nonconst @{term "(\<lambda>A B x\<Colon>'a. A x \<or> B x) = myunion"} *}
wenzelm@51272
   123
ML_val {* nonconst @{term "(\<lambda>x\<Colon>'a. False) = (\<lambda>x\<Colon>'a. True)"} *}
wenzelm@51272
   124
ML_val {* nonconst @{prop "\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h"} *}
blanchet@33197
   125
wenzelm@51272
   126
ML_val {* mono @{prop "Q (\<forall>x\<Colon>'a set. P x)"} *}
wenzelm@51272
   127
ML_val {* mono @{prop "P (a\<Colon>'a)"} *}
wenzelm@51272
   128
ML_val {* mono @{prop "{a} = {b\<Colon>'a}"} *}
wenzelm@51272
   129
ML_val {* mono @{prop "(\<lambda>x. x = a) = (\<lambda>y. y = (b\<Colon>'a))"} *}
wenzelm@51272
   130
ML_val {* mono @{prop "(a\<Colon>'a) \<in> P \<and> P \<union> P = P"} *}
wenzelm@51272
   131
ML_val {* mono @{prop "\<forall>F\<Colon>'a set set. P"} *}
wenzelm@51272
   132
ML_val {* mono @{prop "\<not> (\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h)"} *}
wenzelm@51272
   133
ML_val {* mono @{prop "\<not> Q (\<forall>x\<Colon>'a set. P x)"} *}
wenzelm@51272
   134
ML_val {* mono @{prop "\<not> (\<forall>x\<Colon>'a. P x)"} *}
wenzelm@51272
   135
ML_val {* mono @{prop "myall P = (P = (\<lambda>x\<Colon>'a. True))"} *}
wenzelm@51272
   136
ML_val {* mono @{prop "myall P = (P = (\<lambda>x\<Colon>'a. False))"} *}
wenzelm@51272
   137
ML_val {* mono @{prop "\<forall>x\<Colon>'a. P x"} *}
wenzelm@51272
   138
ML_val {* mono @{term "(\<lambda>A B x\<Colon>'a. A x \<or> B x) \<noteq> myunion"} *}
blanchet@33197
   139
wenzelm@51272
   140
ML_val {* nonmono @{prop "A = (\<lambda>x::'a. True) \<and> A = (\<lambda>x. False)"} *}
wenzelm@51272
   141
ML_val {* nonmono @{prop "\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h"} *}
blanchet@33197
   142
blanchet@41008
   143
ML {*
blanchet@41010
   144
val preproc_timeout = SOME (seconds 5.0)
blanchet@41010
   145
val mono_timeout = SOME (seconds 1.0)
blanchet@41008
   146
blanchet@41008
   147
fun all_unconcealed_theorems_of thy =
blanchet@41008
   148
  let val facts = Global_Theory.facts_of thy in
blanchet@41008
   149
    Facts.fold_static
blanchet@41008
   150
        (fn (name, ths) =>
blanchet@41008
   151
            if Facts.is_concealed facts name then I
blanchet@41008
   152
            else append (map (`(Thm.get_name_hint)) ths))
blanchet@41008
   153
        facts []
blanchet@41008
   154
  end
blanchet@41008
   155
blanchet@41008
   156
fun is_forbidden_theorem name =
wenzelm@46711
   157
  length (Long_Name.explode name) <> 2 orelse
wenzelm@46711
   158
  String.isPrefix "type_definition" (List.last (Long_Name.explode name)) orelse
wenzelm@46711
   159
  String.isPrefix "arity_" (List.last (Long_Name.explode name)) orelse
blanchet@41008
   160
  String.isSuffix "_def" name orelse
blanchet@41008
   161
  String.isSuffix "_raw" name
blanchet@41008
   162
blanchet@41008
   163
fun theorems_of thy =
blanchet@41008
   164
  filter (fn (name, th) =>
blanchet@41008
   165
             not (is_forbidden_theorem name) andalso
blanchet@41008
   166
             (theory_of_thm th, thy) |> pairself Context.theory_name |> op =)
blanchet@41008
   167
         (all_unconcealed_theorems_of thy)
blanchet@41008
   168
blanchet@41010
   169
fun check_formulas tsp =
blanchet@41008
   170
  let
blanchet@41008
   171
    fun is_type_actually_monotonic T =
blanchet@41010
   172
      Nitpick_Mono.formulas_monotonic hol_ctxt binarize T tsp
blanchet@41010
   173
    val free_Ts = fold Term.add_tfrees (op @ tsp) [] |> map TFree
blanchet@41008
   174
    val (mono_free_Ts, nonmono_free_Ts) =
blanchet@41010
   175
      time_limit mono_timeout (List.partition is_type_actually_monotonic)
blanchet@41010
   176
                 free_Ts
blanchet@41008
   177
  in
blanchet@41008
   178
    if not (null mono_free_Ts) then "MONO"
blanchet@41008
   179
    else if not (null nonmono_free_Ts) then "NONMONO"
blanchet@41008
   180
    else "NIX"
blanchet@41008
   181
  end
blanchet@41008
   182
  handle TimeLimit.TimeOut => "TIMEOUT"
blanchet@41008
   183
       | NOT_SUPPORTED _ => "UNSUP"
wenzelm@41523
   184
       | exn => if Exn.is_interrupt exn then reraise exn else "UNKNOWN"
blanchet@41008
   185
blanchet@41008
   186
fun check_theory thy =
blanchet@41008
   187
  let
blanchet@41008
   188
    val path = File.tmp_path (Context.theory_name thy ^ ".out" |> Path.explode)
blanchet@41008
   189
    val _ = File.write path ""
blanchet@41008
   190
    fun check_theorem (name, th) =
blanchet@41008
   191
      let
blanchet@41008
   192
        val t = th |> prop_of |> Type.legacy_freeze |> close_form
blanchet@41008
   193
        val neg_t = Logic.mk_implies (t, @{prop False})
blanchet@41805
   194
        val (nondef_ts, def_ts, _, _, _, _) =
blanchet@41054
   195
          time_limit preproc_timeout (preprocess_formulas hol_ctxt []) neg_t
blanchet@41010
   196
        val res = name ^ ": " ^ check_formulas (nondef_ts, def_ts)
blanchet@41008
   197
      in File.append path (res ^ "\n"); writeln res end
blanchet@41010
   198
      handle TimeLimit.TimeOut => ()
blanchet@41008
   199
  in thy |> theorems_of |> List.app check_theorem end
blanchet@41008
   200
*}
blanchet@41008
   201
blanchet@41015
   202
(*
wenzelm@51272
   203
ML_val {* check_theory @{theory AVL2} *}
wenzelm@51272
   204
ML_val {* check_theory @{theory Fun} *}
wenzelm@51272
   205
ML_val {* check_theory @{theory Huffman} *}
wenzelm@51272
   206
ML_val {* check_theory @{theory List} *}
wenzelm@51272
   207
ML_val {* check_theory @{theory Map} *}
wenzelm@51272
   208
ML_val {* check_theory @{theory Relation} *}
blanchet@41015
   209
*)
blanchet@41015
   210
blanchet@41015
   211
ML {* getenv "ISABELLE_TMP" *}
blanchet@41008
   212
blanchet@33197
   213
end