src/HOL/Nitpick_Examples/Mono_Nits.thy
author blanchet
Mon, 21 Feb 2011 18:28:28 +0100
changeset 41805 a96684499e85
parent 41791 01d722707a36
child 41871 394eef237bd1
permissions -rw-r--r--
adjust example
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
35076
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35071
diff changeset
     3
    Copyright   2009, 2010
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
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
     8
header {* Examples Featuring Nitpick's Monotonicity Check *}
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
41015
3eeb25d953d2 cleanup example
blanchet
parents: 41014
diff changeset
    11
imports Main (* "~/afp/thys/AVL-Trees/AVL2" "~/afp/thys/Huffman/Huffman" *)
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    12
begin
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    13
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    14
ML {*
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    15
open Nitpick_Util
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    16
open Nitpick_HOL
41010
1e5f382c48cc more work on the monotonicity evaluation driver
blanchet
parents: 41008
diff changeset
    17
open Nitpick_Preproc
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    18
40992
blanchet
parents: 39359
diff changeset
    19
exception BUG
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    20
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    21
val thy = @{theory}
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    22
val ctxt = @{context}
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    23
val stds = [(NONE, true)]
35339
34819133c75e make example compile
blanchet
parents: 35191
diff changeset
    24
val subst = []
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    25
val case_names = case_const_names ctxt stds
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    26
val (defs, built_in_nondefs, user_nondefs) = all_axioms_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
    27
val def_tables = const_def_tables ctxt subst defs
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    28
val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    29
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
    30
val psimp_table = const_psimp_table ctxt subst
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    31
val choice_spec_table = const_choice_spec_table ctxt subst
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    32
val user_nondefs =
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    33
  user_nondefs |> filter_out (is_choice_spec_axiom thy choice_spec_table)
41791
01d722707a36 always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp"
blanchet
parents: 41523
diff changeset
    34
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
    35
val ground_thm_table = ground_theorem_table thy
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    36
val ersatz_table = ersatz_table ctxt
41410
3d99be274463 made SML/NJ happy;
wenzelm
parents: 41054
diff changeset
    37
val hol_ctxt as {thy, ...} : hol_context =
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    38
  {thy = thy, ctxt = ctxt, max_bisim_depth = ~1, boxes = [],
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    39
   stds = stds, wfs = [], user_axioms = NONE, debug = false,
41010
1e5f382c48cc more work on the monotonicity evaluation driver
blanchet
parents: 41008
diff changeset
    40
   whacks = [], binary_ints = SOME false, destroy_constrs = true,
41805
a96684499e85 adjust example
blanchet
parents: 41791
diff changeset
    41
   specialize = false, star_linear_preds = false, preconstrs = [],
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    42
   tac_timeout = NONE, evals = [], case_names = case_names,
41791
01d722707a36 always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp"
blanchet
parents: 41523
diff changeset
    43
   def_tables = def_tables, nondef_table = nondef_table,
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    44
   user_nondefs = user_nondefs, simp_table = simp_table,
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    45
   psimp_table = psimp_table, choice_spec_table = choice_spec_table,
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    46
   intro_table = intro_table, ground_thm_table = ground_thm_table,
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    47
   ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    48
   special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    49
   wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
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 =
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
    53
  Nitpick_Mono.formulas_monotonic hol_ctxt binarize @{typ 'a} ([t], [])
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 =
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    56
  let val T = fastype_of t in
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    57
    is_mono (Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t),
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    58
                               @{const False}))
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
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    65
*}
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    66
41006
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    67
ML {* Nitpick_Mono.trace := false *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    68
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    69
ML {* const @{term "A\<Colon>('a\<Rightarrow>'b)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    70
ML {* const @{term "(A\<Colon>'a set) = A"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    71
ML {* const @{term "(A\<Colon>'a set set) = A"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    72
ML {* const @{term "(\<lambda>x\<Colon>'a set. x a)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    73
ML {* const @{term "{{a\<Colon>'a}} = C"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    74
ML {* const @{term "{f\<Colon>'a\<Rightarrow>nat} = {g\<Colon>'a\<Rightarrow>nat}"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    75
ML {* const @{term "A \<union> (B\<Colon>'a set)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    76
ML {* const @{term "\<lambda>A B x\<Colon>'a. A x \<or> B x"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    77
ML {* const @{term "P (a\<Colon>'a)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    78
ML {* const @{term "\<lambda>a\<Colon>'a. b (c (d\<Colon>'a)) (e\<Colon>'a) (f\<Colon>'a)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    79
ML {* const @{term "\<forall>A\<Colon>'a set. A a"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    80
ML {* const @{term "\<forall>A\<Colon>'a set. P A"} *}
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    81
ML {* const @{term "P \<or> Q"} *}
41006
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    82
ML {* const @{term "A \<union> B = (C\<Colon>'a set)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    83
ML {* const @{term "(\<lambda>A B x\<Colon>'a. A x \<or> B x) A B = C"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    84
ML {* const @{term "(if P then (A\<Colon>'a set) else B) = C"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    85
ML {* const @{term "let A = (C\<Colon>'a set) in A \<union> B"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    86
ML {* const @{term "THE x\<Colon>'b. P x"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    87
ML {* const @{term "(\<lambda>x\<Colon>'a. False)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    88
ML {* const @{term "(\<lambda>x\<Colon>'a. True)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    89
ML {* const @{term "(\<lambda>x\<Colon>'a. False) = (\<lambda>x\<Colon>'a. False)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    90
ML {* const @{term "(\<lambda>x\<Colon>'a. True) = (\<lambda>x\<Colon>'a. True)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    91
ML {* const @{term "Let (a\<Colon>'a) A"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    92
ML {* const @{term "A (a\<Colon>'a)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    93
ML {* const @{term "insert (a\<Colon>'a) A = B"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    94
ML {* const @{term "- (A\<Colon>'a set)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    95
ML {* const @{term "finite (A\<Colon>'a set)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    96
ML {* const @{term "\<not> finite (A\<Colon>'a set)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    97
ML {* const @{term "finite (A\<Colon>'a set set)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    98
ML {* const @{term "\<lambda>a\<Colon>'a. A a \<and> \<not> B a"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
    99
ML {* const @{term "A < (B\<Colon>'a set)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   100
ML {* const @{term "A \<le> (B\<Colon>'a set)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   101
ML {* const @{term "[a\<Colon>'a]"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   102
ML {* const @{term "[a\<Colon>'a set]"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   103
ML {* const @{term "[A \<union> (B\<Colon>'a set)]"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   104
ML {* const @{term "[A \<union> (B\<Colon>'a set)] = [C]"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   105
ML {* const @{term "{(\<lambda>x\<Colon>'a. x = a)} = C"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   106
ML {* const @{term "(\<lambda>a\<Colon>'a. \<not> A a) = B"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   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"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   108
ML {* const @{term "\<lambda>A B x\<Colon>'a. A x \<and> B x \<and> A = B"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   109
ML {* const @{term "p = (\<lambda>(x\<Colon>'a) (y\<Colon>'a). P x \<or> \<not> Q y)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   110
ML {* const @{term "p = (\<lambda>(x\<Colon>'a) (y\<Colon>'a). p x y \<Colon> bool)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   111
ML {* const @{term "p = (\<lambda>A B x. A x \<and> \<not> B x) (\<lambda>x. True) (\<lambda>y. x \<noteq> y)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   112
ML {* const @{term "p = (\<lambda>y. x \<noteq> y)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   113
ML {* const @{term "(\<lambda>x. (p\<Colon>'a\<Rightarrow>bool\<Rightarrow>bool) x False)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   114
ML {* const @{term "(\<lambda>x y. (p\<Colon>'a\<Rightarrow>'a\<Rightarrow>bool\<Rightarrow>bool) x y False)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   115
ML {* const @{term "f = (\<lambda>x\<Colon>'a. P x \<longrightarrow> Q x)"} *}
41012
e5a23ffb5524 improve precision of forall in constancy part of the monotonicity calculus
blanchet
parents: 41010
diff changeset
   116
ML {* const @{term "\<forall>a\<Colon>'a. P a"} *}
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   117
41006
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   118
ML {* nonconst @{term "\<forall>P (a\<Colon>'a). P a"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   119
ML {* nonconst @{term "THE x\<Colon>'a. P x"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   120
ML {* nonconst @{term "SOME x\<Colon>'a. P x"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   121
ML {* nonconst @{term "(\<lambda>A B x\<Colon>'a. A x \<or> B x) = myunion"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   122
ML {* nonconst @{term "(\<lambda>x\<Colon>'a. False) = (\<lambda>x\<Colon>'a. True)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   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"} *}
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   124
41006
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   125
ML {* mono @{prop "Q (\<forall>x\<Colon>'a set. P x)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   126
ML {* mono @{prop "P (a\<Colon>'a)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   127
ML {* mono @{prop "{a} = {b\<Colon>'a}"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   128
ML {* mono @{prop "P (a\<Colon>'a) \<and> P \<union> P = P"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   129
ML {* mono @{prop "\<forall>F\<Colon>'a set set. P"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   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)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   131
ML {* mono @{prop "\<not> Q (\<forall>x\<Colon>'a set. P x)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   132
ML {* mono @{prop "\<not> (\<forall>x\<Colon>'a. P x)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   133
ML {* mono @{prop "myall P = (P = (\<lambda>x\<Colon>'a. True))"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   134
ML {* mono @{prop "myall P = (P = (\<lambda>x\<Colon>'a. False))"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   135
ML {* mono @{prop "\<forall>x\<Colon>'a. P x"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   136
ML {* mono @{term "(\<lambda>A B x\<Colon>'a. A x \<or> B x) \<noteq> myunion"} *}
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   137
41006
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   138
ML {* nonmono @{prop "A = (\<lambda>x::'a. True) \<and> A = (\<lambda>x. False)"} *}
000ca46429cd added examples to exercise new monotonicity code
blanchet
parents: 40992
diff changeset
   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"} *}
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   140
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   141
ML {*
41010
1e5f382c48cc more work on the monotonicity evaluation driver
blanchet
parents: 41008
diff changeset
   142
val preproc_timeout = SOME (seconds 5.0)
1e5f382c48cc more work on the monotonicity evaluation driver
blanchet
parents: 41008
diff changeset
   143
val mono_timeout = SOME (seconds 1.0)
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   144
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   145
fun all_unconcealed_theorems_of thy =
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   146
  let val facts = Global_Theory.facts_of thy in
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   147
    Facts.fold_static
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   148
        (fn (name, ths) =>
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   149
            if Facts.is_concealed facts name then I
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   150
            else append (map (`(Thm.get_name_hint)) ths))
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   151
        facts []
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   152
  end
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   153
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   154
fun is_forbidden_theorem name =
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   155
  length (space_explode "." name) <> 2 orelse
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   156
  String.isPrefix "type_definition" (List.last (space_explode "." name)) orelse
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   157
  String.isSuffix "_def" name orelse
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   158
  String.isSuffix "_raw" name
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   159
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   160
fun theorems_of thy =
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   161
  filter (fn (name, th) =>
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   162
             not (is_forbidden_theorem name) andalso
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   163
             (theory_of_thm th, thy) |> pairself Context.theory_name |> op =)
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   164
         (all_unconcealed_theorems_of thy)
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   165
41010
1e5f382c48cc more work on the monotonicity evaluation driver
blanchet
parents: 41008
diff changeset
   166
fun check_formulas tsp =
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   167
  let
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   168
    fun is_type_actually_monotonic T =
41010
1e5f382c48cc more work on the monotonicity evaluation driver
blanchet
parents: 41008
diff changeset
   169
      Nitpick_Mono.formulas_monotonic hol_ctxt binarize T tsp
1e5f382c48cc more work on the monotonicity evaluation driver
blanchet
parents: 41008
diff changeset
   170
    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
   171
    val (mono_free_Ts, nonmono_free_Ts) =
41010
1e5f382c48cc more work on the monotonicity evaluation driver
blanchet
parents: 41008
diff changeset
   172
      time_limit mono_timeout (List.partition is_type_actually_monotonic)
1e5f382c48cc more work on the monotonicity evaluation driver
blanchet
parents: 41008
diff changeset
   173
                 free_Ts
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   174
  in
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   175
    if not (null mono_free_Ts) then "MONO"
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   176
    else if not (null nonmono_free_Ts) then "NONMONO"
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   177
    else "NIX"
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   178
  end
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   179
  handle TimeLimit.TimeOut => "TIMEOUT"
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   180
       | NOT_SUPPORTED _ => "UNSUP"
41523
6c7f5d5b7e9a compile;
wenzelm
parents: 41520
diff changeset
   181
       | exn => if Exn.is_interrupt exn then reraise exn else "UNKNOWN"
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   182
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   183
fun check_theory thy =
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   184
  let
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   185
    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
   186
    val _ = File.write path ""
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   187
    fun check_theorem (name, th) =
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   188
      let
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   189
        val t = th |> prop_of |> Type.legacy_freeze |> close_form
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   190
        val neg_t = Logic.mk_implies (t, @{prop False})
41805
a96684499e85 adjust example
blanchet
parents: 41791
diff changeset
   191
        val (nondef_ts, def_ts, _, _, _, _) =
41054
e58d1cdda832 simplify monotonicity code after killing "fin_fun" optimization
blanchet
parents: 41015
diff changeset
   192
          time_limit preproc_timeout (preprocess_formulas hol_ctxt []) neg_t
41010
1e5f382c48cc more work on the monotonicity evaluation driver
blanchet
parents: 41008
diff changeset
   193
        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
   194
      in File.append path (res ^ "\n"); writeln res end
41010
1e5f382c48cc more work on the monotonicity evaluation driver
blanchet
parents: 41008
diff changeset
   195
      handle TimeLimit.TimeOut => ()
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   196
  in thy |> theorems_of |> List.app check_theorem end
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   197
*}
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   198
41015
3eeb25d953d2 cleanup example
blanchet
parents: 41014
diff changeset
   199
(*
41014
e538a4f9dd86 add more flexibility to the monotonicity calculus: instead of hardcoding F-arrows, also allow G-arrows, simulating applications of the Sub rule
blanchet
parents: 41012
diff changeset
   200
ML {* check_theory @{theory AVL2} *}
41010
1e5f382c48cc more work on the monotonicity evaluation driver
blanchet
parents: 41008
diff changeset
   201
ML {* check_theory @{theory Fun} *}
41014
e538a4f9dd86 add more flexibility to the monotonicity calculus: instead of hardcoding F-arrows, also allow G-arrows, simulating applications of the Sub rule
blanchet
parents: 41012
diff changeset
   202
ML {* check_theory @{theory Huffman} *}
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   203
ML {* check_theory @{theory List} *}
41010
1e5f382c48cc more work on the monotonicity evaluation driver
blanchet
parents: 41008
diff changeset
   204
ML {* check_theory @{theory Map} *}
1e5f382c48cc more work on the monotonicity evaluation driver
blanchet
parents: 41008
diff changeset
   205
ML {* check_theory @{theory Relation} *}
41015
3eeb25d953d2 cleanup example
blanchet
parents: 41014
diff changeset
   206
*)
3eeb25d953d2 cleanup example
blanchet
parents: 41014
diff changeset
   207
3eeb25d953d2 cleanup example
blanchet
parents: 41014
diff changeset
   208
ML {* getenv "ISABELLE_TMP" *}
41008
298226ba5606 added ML code for testing entire theories for monotonicity
blanchet
parents: 41006
diff changeset
   209
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   210
end