author  blanchet 
Wed, 17 Feb 2010 20:50:14 +0100  
changeset 35191  69fa4c39dab2 
parent 35076  cc19e2aef17e 
child 35339  34819133c75e 
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 

11 
imports Main 

12 
begin 

13 

14 
ML {* 

15 
exception FAIL 

16 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33197
diff
changeset

17 
val defs = Nitpick_HOL.all_axioms_of @{theory} > #1 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33197
diff
changeset

18 
val def_table = Nitpick_HOL.const_def_table @{context} defs 
35071
3df45b0ce819
adapted example following previous Nitpick change and fixed minor optimization in Nitpick
blanchet
parents:
34982
diff
changeset

19 
val hol_ctxt : Nitpick_HOL.hol_context = 
33197  20 
{thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [], 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34124
diff
changeset

21 
stds = [(NONE, true)], wfs = [], user_axioms = NONE, debug = false, 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34124
diff
changeset

22 
binary_ints = SOME false, destroy_constrs = false, specialize = false, 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34124
diff
changeset

23 
skolemize = false, star_linear_preds = false, uncurry = false, 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34124
diff
changeset

24 
fast_descrs = false, tac_timeout = NONE, evals = [], case_names = [], 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34124
diff
changeset

25 
def_table = def_table, nondef_table = Symtab.empty, user_nondefs = [], 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
33698
diff
changeset

26 
simp_table = Unsynchronized.ref Symtab.empty, psimp_table = Symtab.empty, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
33698
diff
changeset

27 
intro_table = Symtab.empty, ground_thm_table = Inttab.empty, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
33698
diff
changeset

28 
ersatz_table = [], skolems = Unsynchronized.ref [], 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
33698
diff
changeset

29 
special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [], 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
33698
diff
changeset

30 
wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []} 
33197  31 
(* term > bool *) 
35191
69fa4c39dab2
fix example to reflect change in function signature
blanchet
parents:
35076
diff
changeset

32 
val is_mono = Nitpick_Mono.formulas_monotonic hol_ctxt false @{typ 'a} 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34124
diff
changeset

33 
Nitpick_Mono.Plus [] [] 
33197  34 
fun is_const t = 
35 
let val T = fastype_of t in 

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

37 
@{const False})) 

38 
end 

39 
fun mono t = is_mono t orelse raise FAIL 

40 
fun nonmono t = not (is_mono t) orelse raise FAIL 

41 
fun const t = is_const t orelse raise FAIL 

42 
fun nonconst t = not (is_const t) orelse raise FAIL 

43 
*} 

44 

45 
ML {* const @{term "A::('a\<Rightarrow>'b)"} *} 

46 
ML {* const @{term "(A::'a set) = A"} *} 

47 
ML {* const @{term "(A::'a set set) = A"} *} 

48 
ML {* const @{term "(\<lambda>x::'a set. x a)"} *} 

49 
ML {* const @{term "{{a}} = C"} *} 

50 
ML {* const @{term "{f::'a\<Rightarrow>nat} = {g::'a\<Rightarrow>nat}"} *} 

51 
ML {* const @{term "A \<union> B"} *} 

52 
ML {* const @{term "P (a::'a)"} *} 

53 
ML {* const @{term "\<lambda>a::'a. b (c (d::'a)) (e::'a) (f::'a)"} *} 

54 
ML {* const @{term "\<forall>A::'a set. A a"} *} 

55 
ML {* const @{term "\<forall>A::'a set. P A"} *} 

56 
ML {* const @{term "P \<or> Q"} *} 

57 
ML {* const @{term "A \<union> B = C"} *} 

58 
ML {* const @{term "(if P then (A::'a set) else B) = C"} *} 

59 
ML {* const @{term "let A = C in A \<union> B"} *} 

60 
ML {* const @{term "THE x::'b. P x"} *} 

61 
ML {* const @{term "{}::'a set"} *} 

62 
ML {* const @{term "(\<lambda>x::'a. True)"} *} 

63 
ML {* const @{term "Let a A"} *} 

64 
ML {* const @{term "A (a::'a)"} *} 

65 
ML {* const @{term "insert a A = B"} *} 

66 
ML {* const @{term " (A::'a set)"} *} 

67 
ML {* const @{term "finite A"} *} 

68 
ML {* const @{term "\<not> finite A"} *} 

69 
ML {* const @{term "finite (A::'a set set)"} *} 

70 
ML {* const @{term "\<lambda>a::'a. A a \<and> \<not> B a"} *} 

71 
ML {* const @{term "A < (B::'a set)"} *} 

72 
ML {* const @{term "A \<le> (B::'a set)"} *} 

73 
ML {* const @{term "[a::'a]"} *} 

74 
ML {* const @{term "[a::'a set]"} *} 

75 
ML {* const @{term "[A \<union> (B::'a set)]"} *} 

76 
ML {* const @{term "[A \<union> (B::'a set)] = [C]"} *} 

77 
ML {* const @{term "\<forall>P. P a"} *} 

78 

79 
ML {* nonconst @{term "{%x. True}"} *} 

80 
ML {* nonconst @{term "{(%x. x = a)} = C"} *} 

81 
ML {* nonconst @{term "\<forall>P (a::'a). P a"} *} 

82 
ML {* nonconst @{term "\<forall>a::'a. P a"} *} 

83 
ML {* nonconst @{term "(\<lambda>a::'a. \<not> A a) = B"} *} 

84 
ML {* nonconst @{term "THE x. P x"} *} 

85 
ML {* nonconst @{term "SOME x. P x"} *} 

86 

87 
ML {* mono @{prop "Q (\<forall>x::'a set. P x)"} *} 

88 
ML {* mono @{prop "P (a::'a)"} *} 

89 
ML {* mono @{prop "{a} = {b}"} *} 

90 
ML {* mono @{prop "P (a::'a) \<and> P \<union> P = P"} *} 

91 
ML {* mono @{prop "\<forall>F::'a set set. P"} *} 

92 
ML {* mono @{prop "\<not> (\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> F h)"} *} 

93 
ML {* mono @{prop "\<not> Q (\<forall>x::'a set. P x)"} *} 

94 
ML {* mono @{prop "\<not> (\<forall>x. P x)"} *} 

95 

96 
ML {* nonmono @{prop "\<forall>x. P x"} *} 

97 
ML {* nonmono @{prop "\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> F h"} *} 

98 
ML {* nonmono @{prop "myall P = (P = (\<lambda>x. True))"} *} 

99 

100 
end 