author  blanchet 
Mon, 21 Feb 2011 18:28:28 +0100  
changeset 41805  a96684499e85 
parent 41791  01d722707a36 
child 41871  394eef237bd1 
permissions  rwrr 
33197  1 
(* Title: HOL/Nitpick_Examples/Mono_Nits.thy 
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  4 

5 
Examples featuring Nitpick's monotonicity check. 

6 
*) 

7 

8 
header {* Examples Featuring Nitpick's Monotonicity Check *} 

9 

10 
theory Mono_Nits 

41015  11 
imports Main (* "~/afp/thys/AVLTrees/AVL2" "~/afp/thys/Huffman/Huffman" *) 
33197  12 
begin 
13 

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  17 
open Nitpick_Preproc 
41008
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset

18 

40992  19 
exception BUG 
33197  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  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  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  40 
whacks = [], binary_ints = SOME false, destroy_constrs = true, 
41805  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  55 
fun is_const t = 
56 
let val T = fastype_of t in 

57 
is_mono (Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t), 

58 
@{const False})) 

59 
end 

41008
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset

60 

40992  61 
fun mono t = is_mono t orelse raise BUG 
62 
fun nonmono t = not (is_mono t) orelse raise BUG 

63 
fun const t = is_const t orelse raise BUG 

64 
fun nonconst t = not (is_const t) orelse raise BUG 

33197  65 
*} 
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  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  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  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  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  140 

41008
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset

141 
ML {* 
41010  142 
val preproc_timeout = SOME (seconds 5.0) 
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  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  169 
Nitpick_Mono.formulas_monotonic hol_ctxt binarize T tsp 
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  172 
time_limit mono_timeout (List.partition is_type_actually_monotonic) 
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  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  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  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  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  199 
(* 
41014
e538a4f9dd86
add more flexibility to the monotonicity calculus: instead of hardcoding Farrows, also allow Garrows, simulating applications of the Sub rule
blanchet
parents:
41012
diff
changeset

200 
ML {* check_theory @{theory AVL2} *} 
41010  201 
ML {* check_theory @{theory Fun} *} 
41014
e538a4f9dd86
add more flexibility to the monotonicity calculus: instead of hardcoding Farrows, also allow Garrows, 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  204 
ML {* check_theory @{theory Map} *} 
205 
ML {* check_theory @{theory Relation} *} 

41015  206 
*) 
207 

208 
ML {* getenv "ISABELLE_TMP" *} 

41008
298226ba5606
added ML code for testing entire theories for monotonicity
blanchet
parents:
41006
diff
changeset

209 

33197  210 
end 