src/HOL/Nitpick_Examples/Mono_Nits.thy
author wenzelm
Thu, 28 Mar 2019 21:22:44 +0100
changeset 70008 7aaebfcf3134
parent 69597 ff784d5a5bfb
child 74399 a1d33d1bfb6d
permissions -rw-r--r--
removed junk;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
     1
(*  Title:      HOL/Nitpick_Examples/Mono_Nits.thy
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
45035
60d2c03d5c70 reintroduced Minipick as Nitpick example
blanchet
parents: 42415
diff changeset
     3
    Copyright   2009-2011
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
     4
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
     5
Examples featuring Nitpick's monotonicity check.
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
     6
*)
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
     7
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62519
diff changeset
     8
section \<open>Examples Featuring Nitpick's Monotonicity Check\<close>
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
     9
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    10
theory Mono_Nits
46082
1c436a920730 reintroduced failing examples now that they work again, after reintroduction of "set"
blanchet
parents: 45972
diff changeset
    11
imports Main
1c436a920730 reintroduced failing examples now that they work again, after reintroduction of "set"
blanchet
parents: 45972
diff changeset
    12
        (* "~/afp/thys/DPT-SAT-Solver/DPT_SAT_Solver" *)
1c436a920730 reintroduced failing examples now that they work again, after reintroduction of "set"
blanchet
parents: 45972
diff changeset
    13
        (* "~/afp/thys/AVL-Trees/AVL2" "~/afp/thys/Huffman/Huffman" *)
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    14
begin
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    15
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62519
diff changeset
    16
ML \<open>
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    17
open Nitpick_Util
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    18
open Nitpick_HOL
41010
1e5f382c48cc more work on the monotonicity evaluation driver
blanchet
parents: 41008
diff changeset
    19
open Nitpick_Preproc
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    20
40992
blanchet
parents: 39359
diff changeset
    21
exception BUG
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    22
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    23
val thy = \<^theory>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    24
val ctxt = \<^context>
35339
34819133c75e make example compile
blanchet
parents: 35191
diff changeset
    25
val subst = []
54833
68c8f88af87e compile
blanchet
parents: 51272
diff changeset
    26
val tac_timeout = seconds 1.0
55888
cac1add157e8 removed nonstandard models from Nitpick
blanchet
parents: 54833
diff changeset
    27
val case_names = case_const_names ctxt
42415
10accf397ab6 use "Spec_Rules" for finding axioms -- more reliable and cleaner
blanchet
parents: 41876
diff changeset
    28
val defs = all_defs_of thy subst
10accf397ab6 use "Spec_Rules" for finding axioms -- more reliable and cleaner
blanchet
parents: 41876
diff changeset
    29
val nondefs = all_nondefs_of ctxt subst
41791
01d722707a36 always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp"
blanchet
parents: 41523
diff changeset
    30
val def_tables = const_def_tables ctxt subst defs
42415
10accf397ab6 use "Spec_Rules" for finding axioms -- more reliable and cleaner
blanchet
parents: 41876
diff changeset
    31
val nondef_table = const_nondef_table nondefs
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    32
val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    33
val psimp_table = const_psimp_table ctxt subst
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    34
val choice_spec_table = const_choice_spec_table ctxt subst
41791
01d722707a36 always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp"
blanchet
parents: 41523
diff changeset
    35
val intro_table = inductive_intro_table ctxt subst def_tables
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    36
val ground_thm_table = ground_theorem_table thy
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    37
val ersatz_table = ersatz_table ctxt
41410
3d99be274463 made SML/NJ happy;
wenzelm
parents: 41054
diff changeset
    38
val hol_ctxt as {thy, ...} : hol_context =
55888
cac1add157e8 removed nonstandard models from Nitpick
blanchet
parents: 54833
diff changeset
    39
  {thy = thy, ctxt = ctxt, max_bisim_depth = ~1, boxes = [], wfs = [],
cac1add157e8 removed nonstandard models from Nitpick
blanchet
parents: 54833
diff changeset
    40
   user_axioms = NONE, debug = false, whacks = [], binary_ints = SOME false,
cac1add157e8 removed nonstandard models from Nitpick
blanchet
parents: 54833
diff changeset
    41
   destroy_constrs = true, specialize = false, star_linear_preds = false,
cac1add157e8 removed nonstandard models from Nitpick
blanchet
parents: 54833
diff changeset
    42
   total_consts = NONE, needs = NONE, tac_timeout = tac_timeout, evals = [],
cac1add157e8 removed nonstandard models from Nitpick
blanchet
parents: 54833
diff changeset
    43
   case_names = case_names, def_tables = def_tables,
cac1add157e8 removed nonstandard models from Nitpick
blanchet
parents: 54833
diff changeset
    44
   nondef_table = nondef_table, nondefs = nondefs, simp_table = simp_table,
cac1add157e8 removed nonstandard models from Nitpick
blanchet
parents: 54833
diff changeset
    45
   psimp_table = psimp_table, choice_spec_table = choice_spec_table,
cac1add157e8 removed nonstandard models from Nitpick
blanchet
parents: 54833
diff changeset
    46
   intro_table = intro_table, ground_thm_table = ground_thm_table,
cac1add157e8 removed nonstandard models from Nitpick
blanchet
parents: 54833
diff changeset
    47
   ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
cac1add157e8 removed nonstandard models from Nitpick
blanchet
parents: 54833
diff changeset
    48
   special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
cac1add157e8 removed nonstandard models from Nitpick
blanchet
parents: 54833
diff changeset
    49
   wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    50
val binarize = false
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    51
35812
394fe2b064cd solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents: 35807
diff changeset
    52
fun is_mono t =
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    53
  Nitpick_Mono.formulas_monotonic hol_ctxt binarize \<^typ>\<open>'a\<close> ([t], [])
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    54
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    55
fun is_const t =
46082
1c436a920730 reintroduced failing examples now that they work again, after reintroduction of "set"
blanchet
parents: 45972
diff changeset
    56
  let val T = fastype_of t in
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    57
    Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t), \<^const>\<open>False\<close>)
46082
1c436a920730 reintroduced failing examples now that they work again, after reintroduction of "set"
blanchet
parents: 45972
diff changeset
    58
    |> is_mono
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    59
  end
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    60
40992
blanchet
parents: 39359
diff changeset
    61
fun mono t = is_mono t orelse raise BUG
blanchet
parents: 39359
diff changeset
    62
fun nonmono t = not (is_mono t) orelse raise BUG
blanchet
parents: 39359
diff changeset
    63
fun const t = is_const t orelse raise BUG
blanchet
parents: 39359
diff changeset
    64
fun nonconst t = not (is_const t) orelse raise BUG
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62519
diff changeset
    65
\<close>
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    66
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62519
diff changeset
    67
ML \<open>Nitpick_Mono.trace := false\<close>
41006
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    68
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    69
ML_val \<open>const \<^term>\<open>A::('a\<Rightarrow>'b)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    70
ML_val \<open>const \<^term>\<open>(A::'a set) = A\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    71
ML_val \<open>const \<^term>\<open>(A::'a set set) = A\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    72
ML_val \<open>const \<^term>\<open>(\<lambda>x::'a set. a \<in> x)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    73
ML_val \<open>const \<^term>\<open>{{a::'a}} = C\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    74
ML_val \<open>const \<^term>\<open>{f::'a\<Rightarrow>nat} = {g::'a\<Rightarrow>nat}\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    75
ML_val \<open>const \<^term>\<open>A \<union> (B::'a set)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    76
ML_val \<open>const \<^term>\<open>\<lambda>A B x::'a. A x \<or> B x\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    77
ML_val \<open>const \<^term>\<open>P (a::'a)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    78
ML_val \<open>const \<^term>\<open>\<lambda>a::'a. b (c (d::'a)) (e::'a) (f::'a)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    79
ML_val \<open>const \<^term>\<open>\<forall>A::'a set. a \<in> A\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    80
ML_val \<open>const \<^term>\<open>\<forall>A::'a set. P A\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    81
ML_val \<open>const \<^term>\<open>P \<or> Q\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    82
ML_val \<open>const \<^term>\<open>A \<union> B = (C::'a set)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    83
ML_val \<open>const \<^term>\<open>(\<lambda>A B x::'a. A x \<or> B x) A B = C\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    84
ML_val \<open>const \<^term>\<open>(if P then (A::'a set) else B) = C\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    85
ML_val \<open>const \<^term>\<open>let A = (C::'a set) in A \<union> B\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    86
ML_val \<open>const \<^term>\<open>THE x::'b. P x\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    87
ML_val \<open>const \<^term>\<open>(\<lambda>x::'a. False)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    88
ML_val \<open>const \<^term>\<open>(\<lambda>x::'a. True)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    89
ML_val \<open>const \<^term>\<open>(\<lambda>x::'a. False) = (\<lambda>x::'a. False)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    90
ML_val \<open>const \<^term>\<open>(\<lambda>x::'a. True) = (\<lambda>x::'a. True)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    91
ML_val \<open>const \<^term>\<open>Let (a::'a) A\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    92
ML_val \<open>const \<^term>\<open>A (a::'a)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    93
ML_val \<open>const \<^term>\<open>insert (a::'a) A = B\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    94
ML_val \<open>const \<^term>\<open>- (A::'a set)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    95
ML_val \<open>const \<^term>\<open>finite (A::'a set)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    96
ML_val \<open>const \<^term>\<open>\<not> finite (A::'a set)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    97
ML_val \<open>const \<^term>\<open>finite (A::'a set set)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    98
ML_val \<open>const \<^term>\<open>\<lambda>a::'a. A a \<and> \<not> B a\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
    99
ML_val \<open>const \<^term>\<open>A < (B::'a set)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   100
ML_val \<open>const \<^term>\<open>A \<le> (B::'a set)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   101
ML_val \<open>const \<^term>\<open>[a::'a]\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   102
ML_val \<open>const \<^term>\<open>[a::'a set]\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   103
ML_val \<open>const \<^term>\<open>[A \<union> (B::'a set)]\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   104
ML_val \<open>const \<^term>\<open>[A \<union> (B::'a set)] = [C]\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   105
ML_val \<open>const \<^term>\<open>{(\<lambda>x::'a. x = a)} = C\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   106
ML_val \<open>const \<^term>\<open>(\<lambda>a::'a. \<not> A a) = B\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   107
ML_val \<open>const \<^prop>\<open>\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> \<not> f a\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   108
ML_val \<open>const \<^term>\<open>\<lambda>A B x::'a. A x \<and> B x \<and> A = B\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   109
ML_val \<open>const \<^term>\<open>p = (\<lambda>(x::'a) (y::'a). P x \<or> \<not> Q y)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   110
ML_val \<open>const \<^term>\<open>p = (\<lambda>(x::'a) (y::'a). p x y :: bool)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   111
ML_val \<open>const \<^term>\<open>p = (\<lambda>A B x. A x \<and> \<not> B x) (\<lambda>x. True) (\<lambda>y. x \<noteq> y)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   112
ML_val \<open>const \<^term>\<open>p = (\<lambda>y. x \<noteq> y)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   113
ML_val \<open>const \<^term>\<open>(\<lambda>x. (p::'a\<Rightarrow>bool\<Rightarrow>bool) x False)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   114
ML_val \<open>const \<^term>\<open>(\<lambda>x y. (p::'a\<Rightarrow>'a\<Rightarrow>bool\<Rightarrow>bool) x y False)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   115
ML_val \<open>const \<^term>\<open>f = (\<lambda>x::'a. P x \<longrightarrow> Q x)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   116
ML_val \<open>const \<^term>\<open>\<forall>a::'a. P a\<close>\<close>
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   117
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   118
ML_val \<open>nonconst \<^term>\<open>\<forall>P (a::'a). P a\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   119
ML_val \<open>nonconst \<^term>\<open>THE x::'a. P x\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   120
ML_val \<open>nonconst \<^term>\<open>SOME x::'a. P x\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   121
ML_val \<open>nonconst \<^term>\<open>(\<lambda>A B x::'a. A x \<or> B x) = myunion\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   122
ML_val \<open>nonconst \<^term>\<open>(\<lambda>x::'a. False) = (\<lambda>x::'a. True)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   123
ML_val \<open>nonconst \<^prop>\<open>\<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>\<close>
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   124
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   125
ML_val \<open>mono \<^prop>\<open>Q (\<forall>x::'a set. P x)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   126
ML_val \<open>mono \<^prop>\<open>P (a::'a)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   127
ML_val \<open>mono \<^prop>\<open>{a} = {b::'a}\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   128
ML_val \<open>mono \<^prop>\<open>(\<lambda>x. x = a) = (\<lambda>y. y = (b::'a))\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   129
ML_val \<open>mono \<^prop>\<open>(a::'a) \<in> P \<and> P \<union> P = P\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   130
ML_val \<open>mono \<^prop>\<open>\<forall>F::'a set set. P\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   131
ML_val \<open>mono \<^prop>\<open>\<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>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   132
ML_val \<open>mono \<^prop>\<open>\<not> Q (\<forall>x::'a set. P x)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   133
ML_val \<open>mono \<^prop>\<open>\<not> (\<forall>x::'a. P x)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   134
ML_val \<open>mono \<^prop>\<open>myall P = (P = (\<lambda>x::'a. True))\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   135
ML_val \<open>mono \<^prop>\<open>myall P = (P = (\<lambda>x::'a. False))\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   136
ML_val \<open>mono \<^prop>\<open>\<forall>x::'a. P x\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   137
ML_val \<open>mono \<^term>\<open>(\<lambda>A B x::'a. A x \<or> B x) \<noteq> myunion\<close>\<close>
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   138
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   139
ML_val \<open>nonmono \<^prop>\<open>A = (\<lambda>x::'a. True) \<and> A = (\<lambda>x. False)\<close>\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   140
ML_val \<open>nonmono \<^prop>\<open>\<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>\<close>
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   141
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62519
diff changeset
   142
ML \<open>
54833
68c8f88af87e compile
blanchet
parents: 51272
diff changeset
   143
val preproc_timeout = seconds 5.0
68c8f88af87e compile
blanchet
parents: 51272
diff changeset
   144
val mono_timeout = seconds 1.0
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   145
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   146
fun is_forbidden_theorem name =
46711
f745bcc4a1e5 more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
wenzelm
parents: 46082
diff changeset
   147
  length (Long_Name.explode name) <> 2 orelse
f745bcc4a1e5 more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
wenzelm
parents: 46082
diff changeset
   148
  String.isPrefix "type_definition" (List.last (Long_Name.explode name)) orelse
f745bcc4a1e5 more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
wenzelm
parents: 46082
diff changeset
   149
  String.isPrefix "arity_" (List.last (Long_Name.explode name)) orelse
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   150
  String.isSuffix "_def" name orelse
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   151
  String.isSuffix "_raw" name
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   152
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   153
fun theorems_of thy =
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   154
  filter (fn (name, th) =>
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   155
             not (is_forbidden_theorem name) andalso
65458
cf504b7a7aa7 tuned signature;
wenzelm
parents: 63167
diff changeset
   156
             Thm.theory_name th = Context.theory_name thy)
56374
dfc7a46c2900 removed clone (cf. 300f613060b0)
blanchet
parents: 55888
diff changeset
   157
         (Global_Theory.all_thms_of thy true)
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   158
41010
1e5f382c48cc more work on the monotonicity evaluation driver
blanchet
parents: 41008
diff changeset
   159
fun check_formulas tsp =
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   160
  let
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   161
    fun is_type_actually_monotonic T =
41010
1e5f382c48cc more work on the monotonicity evaluation driver
blanchet
parents: 41008
diff changeset
   162
      Nitpick_Mono.formulas_monotonic hol_ctxt binarize T tsp
67405
e9ab4ad7bd15 uniform use of Standard ML op-infix -- eliminated warnings;
wenzelm
parents: 67399
diff changeset
   163
    val free_Ts = fold Term.add_tfrees ((op @) tsp) [] |> map TFree
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   164
    val (mono_free_Ts, nonmono_free_Ts) =
62519
a564458f94db tuned signature -- clarified modules;
wenzelm
parents: 62505
diff changeset
   165
      Timeout.apply mono_timeout
54833
68c8f88af87e compile
blanchet
parents: 51272
diff changeset
   166
          (List.partition is_type_actually_monotonic) free_Ts
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   167
  in
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   168
    if not (null mono_free_Ts) then "MONO"
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   169
    else if not (null nonmono_free_Ts) then "NONMONO"
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   170
    else "NIX"
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   171
  end
62519
a564458f94db tuned signature -- clarified modules;
wenzelm
parents: 62505
diff changeset
   172
  handle Timeout.TIMEOUT _ => "TIMEOUT"
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   173
       | NOT_SUPPORTED _ => "UNSUP"
62505
9e2a65912111 clarified modules;
wenzelm
parents: 61076
diff changeset
   174
       | exn => if Exn.is_interrupt exn then Exn.reraise exn else "UNKNOWN"
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   175
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   176
fun check_theory thy =
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   177
  let
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   178
    val path = File.tmp_path (Context.theory_name thy ^ ".out" |> Path.explode)
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   179
    val _ = File.write path ""
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   180
    fun check_theorem (name, th) =
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   181
      let
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59058
diff changeset
   182
        val t = th |> Thm.prop_of |> Type.legacy_freeze |> close_form
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67405
diff changeset
   183
        val neg_t = Logic.mk_implies (t, \<^prop>\<open>False\<close>)
41805
a96684499e85 adjust example
blanchet
parents: 41791
diff changeset
   184
        val (nondef_ts, def_ts, _, _, _, _) =
62519
a564458f94db tuned signature -- clarified modules;
wenzelm
parents: 62505
diff changeset
   185
          Timeout.apply preproc_timeout (preprocess_formulas hol_ctxt [])
54833
68c8f88af87e compile
blanchet
parents: 51272
diff changeset
   186
                              neg_t
41010
1e5f382c48cc more work on the monotonicity evaluation driver
blanchet
parents: 41008
diff changeset
   187
        val res = name ^ ": " ^ check_formulas (nondef_ts, def_ts)
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   188
      in File.append path (res ^ "\n"); writeln res end
62519
a564458f94db tuned signature -- clarified modules;
wenzelm
parents: 62505
diff changeset
   189
      handle Timeout.TIMEOUT _ => ()
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   190
  in thy |> theorems_of |> List.app check_theorem end
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62519
diff changeset
   191
\<close>
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   192
41015
3eeb25d953d2 cleanup example
blanchet
parents: 41014
diff changeset
   193
(*
51272
9c8d63b4b6be prefer stateless 'ML_val' for tests;
wenzelm
parents: 46711
diff changeset
   194
ML_val {* check_theory @{theory AVL2} *}
9c8d63b4b6be prefer stateless 'ML_val' for tests;
wenzelm
parents: 46711
diff changeset
   195
ML_val {* check_theory @{theory Fun} *}
9c8d63b4b6be prefer stateless 'ML_val' for tests;
wenzelm
parents: 46711
diff changeset
   196
ML_val {* check_theory @{theory Huffman} *}
9c8d63b4b6be prefer stateless 'ML_val' for tests;
wenzelm
parents: 46711
diff changeset
   197
ML_val {* check_theory @{theory List} *}
9c8d63b4b6be prefer stateless 'ML_val' for tests;
wenzelm
parents: 46711
diff changeset
   198
ML_val {* check_theory @{theory Map} *}
9c8d63b4b6be prefer stateless 'ML_val' for tests;
wenzelm
parents: 46711
diff changeset
   199
ML_val {* check_theory @{theory Relation} *}
41015
3eeb25d953d2 cleanup example
blanchet
parents: 41014
diff changeset
   200
*)
3eeb25d953d2 cleanup example
blanchet
parents: 41014
diff changeset
   201
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   202
end