author | wenzelm |
Sat, 25 Feb 2012 12:34:56 +0100 | |
changeset 46665 | 919dfcdf6d8a |
parent 46082 | 1c436a920730 |
child 46711 | f745bcc4a1e5 |
permissions | -rw-r--r-- |
33197 | 1 |
(* Title: HOL/Nitpick_Examples/Mono_Nits.thy |
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
45035 | 3 |
Copyright 2009-2011 |
33197 | 4 |
|
5 |
Examples featuring Nitpick's monotonicity check. |
|
6 |
*) |
|
7 |
||
8 |
header {* Examples Featuring Nitpick's Monotonicity Check *} |
|
9 |
||
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 | 14 |
begin |
15 |
||
16 |
ML {* |
|
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 | 19 |
open Nitpick_Preproc |
41008
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
20 |
|
40992 | 21 |
exception BUG |
33197 | 22 |
|
41008
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
23 |
val thy = @{theory} |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
24 |
val ctxt = @{context} |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
25 |
val stds = [(NONE, true)] |
35339 | 26 |
val subst = [] |
41008
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
27 |
val case_names = case_const_names ctxt stds |
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 | 38 |
val hol_ctxt as {thy, ...} : hol_context = |
41008
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
39 |
{thy = thy, ctxt = ctxt, max_bisim_depth = ~1, boxes = [], |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
40 |
stds = stds, wfs = [], user_axioms = NONE, debug = false, |
41010 | 41 |
whacks = [], binary_ints = SOME false, destroy_constrs = true, |
41871
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41805
diff
changeset
|
42 |
specialize = false, star_linear_preds = false, total_consts = NONE, |
41876 | 43 |
needs = NONE, tac_timeout = NONE, evals = [], case_names = case_names, |
42415
10accf397ab6
use "Spec_Rules" for finding axioms -- more reliable and cleaner
blanchet
parents:
41876
diff
changeset
|
44 |
def_tables = def_tables, nondef_table = nondef_table, nondefs = nondefs, |
10accf397ab6
use "Spec_Rules" for finding axioms -- more reliable and cleaner
blanchet
parents:
41876
diff
changeset
|
45 |
simp_table = simp_table, psimp_table = psimp_table, |
10accf397ab6
use "Spec_Rules" for finding axioms -- more reliable and cleaner
blanchet
parents:
41876
diff
changeset
|
46 |
choice_spec_table = choice_spec_table, intro_table = intro_table, |
10accf397ab6
use "Spec_Rules" for finding axioms -- more reliable and cleaner
blanchet
parents:
41876
diff
changeset
|
47 |
ground_thm_table = ground_thm_table, ersatz_table = ersatz_table, |
10accf397ab6
use "Spec_Rules" for finding axioms -- more reliable and cleaner
blanchet
parents:
41876
diff
changeset
|
48 |
skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [], |
10accf397ab6
use "Spec_Rules" for finding axioms -- more reliable and cleaner
blanchet
parents:
41876
diff
changeset
|
49 |
unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [], |
10accf397ab6
use "Spec_Rules" for finding axioms -- more reliable and cleaner
blanchet
parents:
41876
diff
changeset
|
50 |
constr_cache = Unsynchronized.ref []} |
41008
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
51 |
val binarize = false |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
52 |
|
35812
394fe2b064cd
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
blanchet
parents:
35807
diff
changeset
|
53 |
fun is_mono t = |
41008
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
54 |
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
|
55 |
|
33197 | 56 |
fun is_const t = |
46082
1c436a920730
reintroduced failing examples now that they work again, after reintroduction of "set"
blanchet
parents:
45972
diff
changeset
|
57 |
let val T = fastype_of t in |
1c436a920730
reintroduced failing examples now that they work again, after reintroduction of "set"
blanchet
parents:
45972
diff
changeset
|
58 |
Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t), @{const False}) |
1c436a920730
reintroduced failing examples now that they work again, after reintroduction of "set"
blanchet
parents:
45972
diff
changeset
|
59 |
|> is_mono |
33197 | 60 |
end |
41008
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
61 |
|
40992 | 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 |
|
33197 | 66 |
*} |
67 |
||
41006
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
68 |
ML {* Nitpick_Mono.trace := false *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
69 |
|
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
70 |
ML {* const @{term "A\<Colon>('a\<Rightarrow>'b)"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
71 |
ML {* const @{term "(A\<Colon>'a set) = A"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
72 |
ML {* const @{term "(A\<Colon>'a set set) = A"} *} |
45972
deda685ba210
commented out examples which choke on strict set/pred distinction
haftmann
parents:
45704
diff
changeset
|
73 |
ML {* const @{term "(\<lambda>x\<Colon>'a set. a \<in> x)"} *} |
41006
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
74 |
ML {* const @{term "{{a\<Colon>'a}} = C"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
75 |
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
|
76 |
ML {* const @{term "A \<union> (B\<Colon>'a set)"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
77 |
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
|
78 |
ML {* const @{term "P (a\<Colon>'a)"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
79 |
ML {* const @{term "\<lambda>a\<Colon>'a. b (c (d\<Colon>'a)) (e\<Colon>'a) (f\<Colon>'a)"} *} |
45972
deda685ba210
commented out examples which choke on strict set/pred distinction
haftmann
parents:
45704
diff
changeset
|
80 |
ML {* const @{term "\<forall>A\<Colon>'a set. a \<in> A"} *} |
41006
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
81 |
ML {* const @{term "\<forall>A\<Colon>'a set. P A"} *} |
33197 | 82 |
ML {* const @{term "P \<or> Q"} *} |
41006
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
83 |
ML {* const @{term "A \<union> B = (C\<Colon>'a set)"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
84 |
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
|
85 |
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
|
86 |
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
|
87 |
ML {* const @{term "THE x\<Colon>'b. P x"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
88 |
ML {* const @{term "(\<lambda>x\<Colon>'a. False)"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
89 |
ML {* const @{term "(\<lambda>x\<Colon>'a. True)"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
90 |
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
|
91 |
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
|
92 |
ML {* const @{term "Let (a\<Colon>'a) A"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
93 |
ML {* const @{term "A (a\<Colon>'a)"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
94 |
ML {* const @{term "insert (a\<Colon>'a) A = B"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
95 |
ML {* const @{term "- (A\<Colon>'a set)"} *} |
46082
1c436a920730
reintroduced failing examples now that they work again, after reintroduction of "set"
blanchet
parents:
45972
diff
changeset
|
96 |
ML {* const @{term "finite (A\<Colon>'a set)"} *} |
1c436a920730
reintroduced failing examples now that they work again, after reintroduction of "set"
blanchet
parents:
45972
diff
changeset
|
97 |
ML {* const @{term "\<not> finite (A\<Colon>'a set)"} *} |
1c436a920730
reintroduced failing examples now that they work again, after reintroduction of "set"
blanchet
parents:
45972
diff
changeset
|
98 |
ML {* const @{term "finite (A\<Colon>'a set set)"} *} |
41006
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
99 |
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
|
100 |
ML {* const @{term "A < (B\<Colon>'a set)"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
101 |
ML {* const @{term "A \<le> (B\<Colon>'a set)"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
102 |
ML {* const @{term "[a\<Colon>'a]"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
103 |
ML {* const @{term "[a\<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)]"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
105 |
ML {* const @{term "[A \<union> (B\<Colon>'a set)] = [C]"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
106 |
ML {* const @{term "{(\<lambda>x\<Colon>'a. x = a)} = C"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
107 |
ML {* const @{term "(\<lambda>a\<Colon>'a. \<not> A a) = B"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
108 |
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
|
109 |
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
|
110 |
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
|
111 |
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
|
112 |
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
|
113 |
ML {* const @{term "p = (\<lambda>y. x \<noteq> y)"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
114 |
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
|
115 |
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
|
116 |
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
|
117 |
ML {* const @{term "\<forall>a\<Colon>'a. P a"} *} |
33197 | 118 |
|
41006
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
119 |
ML {* nonconst @{term "\<forall>P (a\<Colon>'a). P a"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
120 |
ML {* nonconst @{term "THE x\<Colon>'a. P x"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
121 |
ML {* nonconst @{term "SOME x\<Colon>'a. P x"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
122 |
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
|
123 |
ML {* nonconst @{term "(\<lambda>x\<Colon>'a. False) = (\<lambda>x\<Colon>'a. True)"} *} |
46082
1c436a920730
reintroduced failing examples now that they work again, after reintroduction of "set"
blanchet
parents:
45972
diff
changeset
|
124 |
ML {* 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"} *} |
33197 | 125 |
|
41006
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
126 |
ML {* mono @{prop "Q (\<forall>x\<Colon>'a set. P x)"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
127 |
ML {* mono @{prop "P (a\<Colon>'a)"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
128 |
ML {* mono @{prop "{a} = {b\<Colon>'a}"} *} |
46082
1c436a920730
reintroduced failing examples now that they work again, after reintroduction of "set"
blanchet
parents:
45972
diff
changeset
|
129 |
ML {* mono @{prop "(\<lambda>x. x = a) = (\<lambda>y. y = (b\<Colon>'a))"} *} |
45972
deda685ba210
commented out examples which choke on strict set/pred distinction
haftmann
parents:
45704
diff
changeset
|
130 |
ML {* mono @{prop "(a\<Colon>'a) \<in> P \<and> P \<union> P = P"} *} |
41006
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
131 |
ML {* mono @{prop "\<forall>F\<Colon>'a set set. P"} *} |
45972
deda685ba210
commented out examples which choke on strict set/pred distinction
haftmann
parents:
45704
diff
changeset
|
132 |
ML {* 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)"} *} |
41006
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
133 |
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
|
134 |
ML {* mono @{prop "\<not> (\<forall>x\<Colon>'a. P x)"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
135 |
ML {* mono @{prop "myall P = (P = (\<lambda>x\<Colon>'a. True))"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
136 |
ML {* mono @{prop "myall P = (P = (\<lambda>x\<Colon>'a. False))"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
137 |
ML {* mono @{prop "\<forall>x\<Colon>'a. P x"} *} |
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
138 |
ML {* mono @{term "(\<lambda>A B x\<Colon>'a. A x \<or> B x) \<noteq> myunion"} *} |
33197 | 139 |
|
41006
000ca46429cd
added examples to exercise new monotonicity code
blanchet
parents:
40992
diff
changeset
|
140 |
ML {* nonmono @{prop "A = (\<lambda>x::'a. True) \<and> A = (\<lambda>x. False)"} *} |
46082
1c436a920730
reintroduced failing examples now that they work again, after reintroduction of "set"
blanchet
parents:
45972
diff
changeset
|
141 |
ML {* 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"} *} |
33197 | 142 |
|
41008
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
143 |
ML {* |
41010 | 144 |
val preproc_timeout = SOME (seconds 5.0) |
145 |
val mono_timeout = SOME (seconds 1.0) |
|
41008
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
146 |
|
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
147 |
fun all_unconcealed_theorems_of thy = |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
148 |
let val facts = Global_Theory.facts_of thy in |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
149 |
Facts.fold_static |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
150 |
(fn (name, ths) => |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
151 |
if Facts.is_concealed facts name then I |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
152 |
else append (map (`(Thm.get_name_hint)) ths)) |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
153 |
facts [] |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
154 |
end |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
155 |
|
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
156 |
fun is_forbidden_theorem name = |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
157 |
length (space_explode "." name) <> 2 orelse |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
158 |
String.isPrefix "type_definition" (List.last (space_explode "." name)) orelse |
45704 | 159 |
String.isPrefix "arity_" (List.last (space_explode "." name)) orelse |
41008
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
160 |
String.isSuffix "_def" name orelse |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
161 |
String.isSuffix "_raw" name |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
162 |
|
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
163 |
fun theorems_of thy = |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
164 |
filter (fn (name, th) => |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
165 |
not (is_forbidden_theorem name) andalso |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
166 |
(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
|
167 |
(all_unconcealed_theorems_of thy) |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
168 |
|
41010 | 169 |
fun check_formulas tsp = |
41008
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
170 |
let |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
171 |
fun is_type_actually_monotonic T = |
41010 | 172 |
Nitpick_Mono.formulas_monotonic hol_ctxt binarize T tsp |
173 |
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
|
174 |
val (mono_free_Ts, nonmono_free_Ts) = |
41010 | 175 |
time_limit mono_timeout (List.partition is_type_actually_monotonic) |
176 |
free_Ts |
|
41008
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
177 |
in |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
178 |
if not (null mono_free_Ts) then "MONO" |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
179 |
else if not (null nonmono_free_Ts) then "NONMONO" |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
180 |
else "NIX" |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
181 |
end |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
182 |
handle TimeLimit.TimeOut => "TIMEOUT" |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
183 |
| NOT_SUPPORTED _ => "UNSUP" |
41523 | 184 |
| 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
|
185 |
|
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
186 |
fun check_theory thy = |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
187 |
let |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
188 |
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
|
189 |
val _ = File.write path "" |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
190 |
fun check_theorem (name, th) = |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
191 |
let |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
192 |
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
|
193 |
val neg_t = Logic.mk_implies (t, @{prop False}) |
41805 | 194 |
val (nondef_ts, def_ts, _, _, _, _) = |
41054
e58d1cdda832
simplify monotonicity code after killing "fin_fun" optimization
blanchet
parents:
41015
diff
changeset
|
195 |
time_limit preproc_timeout (preprocess_formulas hol_ctxt []) neg_t |
41010 | 196 |
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
|
197 |
in File.append path (res ^ "\n"); writeln res end |
41010 | 198 |
handle TimeLimit.TimeOut => () |
41008
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
199 |
in thy |> theorems_of |> List.app check_theorem end |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
200 |
*} |
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
201 |
|
41015 | 202 |
(* |
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
|
203 |
ML {* check_theory @{theory AVL2} *} |
41010 | 204 |
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
|
205 |
ML {* check_theory @{theory Huffman} *} |
41008
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
206 |
ML {* check_theory @{theory List} *} |
41010 | 207 |
ML {* check_theory @{theory Map} *} |
208 |
ML {* check_theory @{theory Relation} *} |
|
41015 | 209 |
*) |
210 |
||
211 |
ML {* getenv "ISABELLE_TMP" *} |
|
41008
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset
|
212 |
|
33197 | 213 |
end |