src/HOL/Nitpick_Examples/Mono_Nits.thy
 author hoelzl Tue Jan 18 21:37:23 2011 +0100 (2011-01-18) changeset 41654 32fe42892983 parent 41523 6c7f5d5b7e9a child 41791 01d722707a36 permissions -rw-r--r--
Gauge measure removed
```     1 (*  Title:      HOL/Nitpick_Examples/Mono_Nits.thy
```
```     2     Author:     Jasmin Blanchette, TU Muenchen
```
```     3     Copyright   2009, 2010
```
```     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 (* "~/afp/thys/AVL-Trees/AVL2" "~/afp/thys/Huffman/Huffman" *)
```
```    12 begin
```
```    13
```
```    14 ML {*
```
```    15 open Nitpick_Util
```
```    16 open Nitpick_HOL
```
```    17 open Nitpick_Preproc
```
```    18
```
```    19 exception BUG
```
```    20
```
```    21 val thy = @{theory}
```
```    22 val ctxt = @{context}
```
```    23 val stds = [(NONE, true)]
```
```    24 val subst = []
```
```    25 val case_names = case_const_names ctxt stds
```
```    26 val (defs, built_in_nondefs, user_nondefs) = all_axioms_of ctxt subst
```
```    27 val def_table = const_def_table ctxt subst defs
```
```    28 val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
```
```    29 val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
```
```    30 val psimp_table = const_psimp_table ctxt subst
```
```    31 val choice_spec_table = const_choice_spec_table ctxt subst
```
```    32 val user_nondefs =
```
```    33   user_nondefs |> filter_out (is_choice_spec_axiom thy choice_spec_table)
```
```    34 val intro_table = inductive_intro_table ctxt subst def_table
```
```    35 val ground_thm_table = ground_theorem_table thy
```
```    36 val ersatz_table = ersatz_table ctxt
```
```    37 val hol_ctxt as {thy, ...} : hol_context =
```
```    38   {thy = thy, ctxt = ctxt, max_bisim_depth = ~1, boxes = [],
```
```    39    stds = stds, wfs = [], user_axioms = NONE, debug = false,
```
```    40    whacks = [], binary_ints = SOME false, destroy_constrs = true,
```
```    41    specialize = false, star_linear_preds = false,
```
```    42    tac_timeout = NONE, evals = [], case_names = case_names,
```
```    43    def_table = def_table, nondef_table = nondef_table,
```
```    44    user_nondefs = user_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     is_mono (Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t),
```
```    58                                @{const False}))
```
```    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 *}
```
```    66
```
```    67 ML {* Nitpick_Mono.trace := false *}
```
```    68
```
```    69 ML {* const @{term "A\<Colon>('a\<Rightarrow>'b)"} *}
```
```    70 ML {* const @{term "(A\<Colon>'a set) = A"} *}
```
```    71 ML {* const @{term "(A\<Colon>'a set set) = A"} *}
```
```    72 ML {* const @{term "(\<lambda>x\<Colon>'a set. x a)"} *}
```
```    73 ML {* const @{term "{{a\<Colon>'a}} = C"} *}
```
```    74 ML {* const @{term "{f\<Colon>'a\<Rightarrow>nat} = {g\<Colon>'a\<Rightarrow>nat}"} *}
```
```    75 ML {* const @{term "A \<union> (B\<Colon>'a set)"} *}
```
```    76 ML {* const @{term "\<lambda>A B x\<Colon>'a. A x \<or> B x"} *}
```
```    77 ML {* const @{term "P (a\<Colon>'a)"} *}
```
```    78 ML {* const @{term "\<lambda>a\<Colon>'a. b (c (d\<Colon>'a)) (e\<Colon>'a) (f\<Colon>'a)"} *}
```
```    79 ML {* const @{term "\<forall>A\<Colon>'a set. A a"} *}
```
```    80 ML {* const @{term "\<forall>A\<Colon>'a set. P A"} *}
```
```    81 ML {* const @{term "P \<or> Q"} *}
```
```    82 ML {* const @{term "A \<union> B = (C\<Colon>'a set)"} *}
```
```    83 ML {* const @{term "(\<lambda>A B x\<Colon>'a. A x \<or> B x) A B = C"} *}
```
```    84 ML {* const @{term "(if P then (A\<Colon>'a set) else B) = C"} *}
```
```    85 ML {* const @{term "let A = (C\<Colon>'a set) in A \<union> B"} *}
```
```    86 ML {* const @{term "THE x\<Colon>'b. P x"} *}
```
```    87 ML {* const @{term "(\<lambda>x\<Colon>'a. False)"} *}
```
```    88 ML {* const @{term "(\<lambda>x\<Colon>'a. True)"} *}
```
```    89 ML {* const @{term "(\<lambda>x\<Colon>'a. False) = (\<lambda>x\<Colon>'a. False)"} *}
```
```    90 ML {* const @{term "(\<lambda>x\<Colon>'a. True) = (\<lambda>x\<Colon>'a. True)"} *}
```
```    91 ML {* const @{term "Let (a\<Colon>'a) A"} *}
```
```    92 ML {* const @{term "A (a\<Colon>'a)"} *}
```
```    93 ML {* const @{term "insert (a\<Colon>'a) A = B"} *}
```
```    94 ML {* const @{term "- (A\<Colon>'a set)"} *}
```
```    95 ML {* const @{term "finite (A\<Colon>'a set)"} *}
```
```    96 ML {* const @{term "\<not> finite (A\<Colon>'a set)"} *}
```
```    97 ML {* const @{term "finite (A\<Colon>'a set set)"} *}
```
```    98 ML {* const @{term "\<lambda>a\<Colon>'a. A a \<and> \<not> B a"} *}
```
```    99 ML {* const @{term "A < (B\<Colon>'a set)"} *}
```
```   100 ML {* const @{term "A \<le> (B\<Colon>'a set)"} *}
```
```   101 ML {* const @{term "[a\<Colon>'a]"} *}
```
```   102 ML {* const @{term "[a\<Colon>'a set]"} *}
```
```   103 ML {* const @{term "[A \<union> (B\<Colon>'a set)]"} *}
```
```   104 ML {* const @{term "[A \<union> (B\<Colon>'a set)] = [C]"} *}
```
```   105 ML {* const @{term "{(\<lambda>x\<Colon>'a. x = a)} = C"} *}
```
```   106 ML {* const @{term "(\<lambda>a\<Colon>'a. \<not> A a) = B"} *}
```
```   107 ML {* 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"} *}
```
```   108 ML {* const @{term "\<lambda>A B x\<Colon>'a. A x \<and> B x \<and> A = B"} *}
```
```   109 ML {* const @{term "p = (\<lambda>(x\<Colon>'a) (y\<Colon>'a). P x \<or> \<not> Q y)"} *}
```
```   110 ML {* const @{term "p = (\<lambda>(x\<Colon>'a) (y\<Colon>'a). p x y \<Colon> bool)"} *}
```
```   111 ML {* const @{term "p = (\<lambda>A B x. A x \<and> \<not> B x) (\<lambda>x. True) (\<lambda>y. x \<noteq> y)"} *}
```
```   112 ML {* const @{term "p = (\<lambda>y. x \<noteq> y)"} *}
```
```   113 ML {* const @{term "(\<lambda>x. (p\<Colon>'a\<Rightarrow>bool\<Rightarrow>bool) x False)"} *}
```
```   114 ML {* const @{term "(\<lambda>x y. (p\<Colon>'a\<Rightarrow>'a\<Rightarrow>bool\<Rightarrow>bool) x y False)"} *}
```
```   115 ML {* const @{term "f = (\<lambda>x\<Colon>'a. P x \<longrightarrow> Q x)"} *}
```
```   116 ML {* const @{term "\<forall>a\<Colon>'a. P a"} *}
```
```   117
```
```   118 ML {* nonconst @{term "\<forall>P (a\<Colon>'a). P a"} *}
```
```   119 ML {* nonconst @{term "THE x\<Colon>'a. P x"} *}
```
```   120 ML {* nonconst @{term "SOME x\<Colon>'a. P x"} *}
```
```   121 ML {* nonconst @{term "(\<lambda>A B x\<Colon>'a. A x \<or> B x) = myunion"} *}
```
```   122 ML {* nonconst @{term "(\<lambda>x\<Colon>'a. False) = (\<lambda>x\<Colon>'a. True)"} *}
```
```   123 ML {* nonconst @{prop "\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> F h"} *}
```
```   124
```
```   125 ML {* mono @{prop "Q (\<forall>x\<Colon>'a set. P x)"} *}
```
```   126 ML {* mono @{prop "P (a\<Colon>'a)"} *}
```
```   127 ML {* mono @{prop "{a} = {b\<Colon>'a}"} *}
```
```   128 ML {* mono @{prop "P (a\<Colon>'a) \<and> P \<union> P = P"} *}
```
```   129 ML {* mono @{prop "\<forall>F\<Colon>'a set set. P"} *}
```
```   130 ML {* mono @{prop "\<not> (\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> F h)"} *}
```
```   131 ML {* mono @{prop "\<not> Q (\<forall>x\<Colon>'a set. P x)"} *}
```
```   132 ML {* mono @{prop "\<not> (\<forall>x\<Colon>'a. P x)"} *}
```
```   133 ML {* mono @{prop "myall P = (P = (\<lambda>x\<Colon>'a. True))"} *}
```
```   134 ML {* mono @{prop "myall P = (P = (\<lambda>x\<Colon>'a. False))"} *}
```
```   135 ML {* mono @{prop "\<forall>x\<Colon>'a. P x"} *}
```
```   136 ML {* mono @{term "(\<lambda>A B x\<Colon>'a. A x \<or> B x) \<noteq> myunion"} *}
```
```   137
```
```   138 ML {* nonmono @{prop "A = (\<lambda>x::'a. True) \<and> A = (\<lambda>x. False)"} *}
```
```   139 ML {* nonmono @{prop "\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> F h"} *}
```
```   140
```
```   141 ML {*
```
```   142 val preproc_timeout = SOME (seconds 5.0)
```
```   143 val mono_timeout = SOME (seconds 1.0)
```
```   144
```
```   145 fun all_unconcealed_theorems_of thy =
```
```   146   let val facts = Global_Theory.facts_of thy in
```
```   147     Facts.fold_static
```
```   148         (fn (name, ths) =>
```
```   149             if Facts.is_concealed facts name then I
```
```   150             else append (map (`(Thm.get_name_hint)) ths))
```
```   151         facts []
```
```   152   end
```
```   153
```
```   154 fun is_forbidden_theorem name =
```
```   155   length (space_explode "." name) <> 2 orelse
```
```   156   String.isPrefix "type_definition" (List.last (space_explode "." name)) orelse
```
```   157   String.isSuffix "_def" name orelse
```
```   158   String.isSuffix "_raw" name
```
```   159
```
```   160 fun theorems_of thy =
```
```   161   filter (fn (name, th) =>
```
```   162              not (is_forbidden_theorem name) andalso
```
```   163              (theory_of_thm th, thy) |> pairself Context.theory_name |> op =)
```
```   164          (all_unconcealed_theorems_of thy)
```
```   165
```
```   166 fun check_formulas tsp =
```
```   167   let
```
```   168     fun is_type_actually_monotonic T =
```
```   169       Nitpick_Mono.formulas_monotonic hol_ctxt binarize T tsp
```
```   170     val free_Ts = fold Term.add_tfrees (op @ tsp) [] |> map TFree
```
```   171     val (mono_free_Ts, nonmono_free_Ts) =
```
```   172       time_limit mono_timeout (List.partition is_type_actually_monotonic)
```
```   173                  free_Ts
```
```   174   in
```
```   175     if not (null mono_free_Ts) then "MONO"
```
```   176     else if not (null nonmono_free_Ts) then "NONMONO"
```
```   177     else "NIX"
```
```   178   end
```
```   179   handle TimeLimit.TimeOut => "TIMEOUT"
```
```   180        | NOT_SUPPORTED _ => "UNSUP"
```
```   181        | exn => if Exn.is_interrupt exn then reraise exn else "UNKNOWN"
```
```   182
```
```   183 fun check_theory thy =
```
```   184   let
```
```   185     val path = File.tmp_path (Context.theory_name thy ^ ".out" |> Path.explode)
```
```   186     val _ = File.write path ""
```
```   187     fun check_theorem (name, th) =
```
```   188       let
```
```   189         val t = th |> prop_of |> Type.legacy_freeze |> close_form
```
```   190         val neg_t = Logic.mk_implies (t, @{prop False})
```
```   191         val (nondef_ts, def_ts, _, _, _) =
```
```   192           time_limit preproc_timeout (preprocess_formulas hol_ctxt []) neg_t
```
```   193         val res = name ^ ": " ^ check_formulas (nondef_ts, def_ts)
```
```   194       in File.append path (res ^ "\n"); writeln res end
```
```   195       handle TimeLimit.TimeOut => ()
```
```   196   in thy |> theorems_of |> List.app check_theorem end
```
```   197 *}
```
```   198
```
```   199 (*
```
```   200 ML {* check_theory @{theory AVL2} *}
```
```   201 ML {* check_theory @{theory Fun} *}
```
```   202 ML {* check_theory @{theory Huffman} *}
```
```   203 ML {* check_theory @{theory List} *}
```
```   204 ML {* check_theory @{theory Map} *}
```
```   205 ML {* check_theory @{theory Relation} *}
```
```   206 *)
```
```   207
```
```   208 ML {* getenv "ISABELLE_TMP" *}
```
```   209
```
```   210 end
```