author | haftmann |
Thu, 11 Mar 2010 14:38:20 +0100 | |
changeset 35724 | 178ad68f93ed |
parent 35386 | 45a4e19d3ebd |
child 35807 | e4d1b5cbd429 |
permissions | -rw-r--r-- |
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 |
||
35339 | 17 |
val subst = [] |
18 |
val defs = Nitpick_HOL.all_axioms_of @{theory} subst |> #1 |
|
19 |
val def_table = Nitpick_HOL.const_def_table @{context} subst defs |
|
35071
3df45b0ce819
adapted example following previous Nitpick change and fixed minor optimization in Nitpick
blanchet
parents:
34982
diff
changeset
|
20 |
val hol_ctxt : Nitpick_HOL.hol_context = |
33197 | 21 |
{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
|
22 |
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
|
23 |
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
|
24 |
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
|
25 |
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
|
26 |
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
|
27 |
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
|
28 |
intro_table = Symtab.empty, ground_thm_table = Inttab.empty, |
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
33698
diff
changeset
|
29 |
ersatz_table = [], skolems = Unsynchronized.ref [], |
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
33698
diff
changeset
|
30 |
special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [], |
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
33698
diff
changeset
|
31 |
wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []} |
33197 | 32 |
(* term -> bool *) |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
33 |
fun is_mono t = Nitpick_Mono.formulas_monotonic hol_ctxt false @{typ 'a} ([t], []) |
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)"} *} |
|
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
49 |
ML {* const @{term "{{a::'a}} = C"} *} |
33197 | 50 |
ML {* const @{term "{f::'a\<Rightarrow>nat} = {g::'a\<Rightarrow>nat}"} *} |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
51 |
ML {* const @{term "A \<union> (B::'a set)"} *} |
33197 | 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"} *} |
|
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
57 |
ML {* const @{term "A \<union> B = (C::'a set)"} *} |
33197 | 58 |
ML {* const @{term "(if P then (A::'a set) else B) = C"} *} |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
59 |
ML {* const @{term "let A = (C::'a set) in A \<union> B"} *} |
33197 | 60 |
ML {* const @{term "THE x::'b. P x"} *} |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
61 |
ML {* const @{term "(\<lambda>x::'a. False)"} *} |
33197 | 62 |
ML {* const @{term "(\<lambda>x::'a. True)"} *} |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
63 |
ML {* const @{term "Let (a::'a) A"} *} |
33197 | 64 |
ML {* const @{term "A (a::'a)"} *} |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
65 |
ML {* const @{term "insert (a::'a) A = B"} *} |
33197 | 66 |
ML {* const @{term "- (A::'a set)"} *} |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
67 |
ML {* const @{term "finite (A::'a set)"} *} |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
68 |
ML {* const @{term "\<not> finite (A::'a set)"} *} |
33197 | 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 |
||
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
78 |
ML {* nonconst @{term "{(\<lambda>x::'a. x = a)} = C"} *} |
33197 | 79 |
ML {* nonconst @{term "\<forall>P (a::'a). P a"} *} |
80 |
ML {* nonconst @{term "\<forall>a::'a. P a"} *} |
|
81 |
ML {* nonconst @{term "(\<lambda>a::'a. \<not> A a) = B"} *} |
|
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
82 |
ML {* nonconst @{term "THE x::'a. P x"} *} |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
83 |
ML {* nonconst @{term "SOME x::'a. P x"} *} |
33197 | 84 |
|
85 |
ML {* mono @{prop "Q (\<forall>x::'a set. P x)"} *} |
|
86 |
ML {* mono @{prop "P (a::'a)"} *} |
|
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
87 |
ML {* mono @{prop "{a} = {b::'a}"} *} |
33197 | 88 |
ML {* mono @{prop "P (a::'a) \<and> P \<union> P = P"} *} |
89 |
ML {* mono @{prop "\<forall>F::'a set set. P"} *} |
|
90 |
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)"} *} |
|
91 |
ML {* mono @{prop "\<not> Q (\<forall>x::'a set. P x)"} *} |
|
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
92 |
ML {* mono @{prop "\<not> (\<forall>x::'a. P x)"} *} |
33197 | 93 |
|
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
94 |
ML {* nonmono @{prop "\<forall>x::'a. P x"} *} |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
95 |
ML {* nonmono @{prop "myall P = (P = (\<lambda>x::'a. True))"} *} |
33197 | 96 |
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"} *} |
97 |
||
98 |
end |