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