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