33197
|
1 |
(* Title: HOL/Nitpick_Examples/Mono_Nits.thy
|
|
2 |
Author: Jasmin Blanchette, TU Muenchen
|
|
3 |
Copyright 2009
|
|
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 |
|
|
17 |
val defs = NitpickHOL.all_axioms_of @{theory} |> #1
|
|
18 |
val def_table = NitpickHOL.const_def_table @{context} defs
|
|
19 |
val ext_ctxt =
|
|
20 |
{thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [],
|
|
21 |
user_axioms = NONE, debug = false, wfs = [], destroy_constrs = false,
|
|
22 |
specialize = false, skolemize = false, star_linear_preds = false,
|
|
23 |
uncurry = false, fast_descrs = false, tac_timeout = NONE, evals = [],
|
|
24 |
case_names = [], def_table = def_table, nondef_table = Symtab.empty,
|
|
25 |
user_nondefs = [], simp_table = Unsynchronized.ref Symtab.empty,
|
|
26 |
psimp_table = Symtab.empty, intro_table = Symtab.empty,
|
|
27 |
ground_thm_table = Inttab.empty, ersatz_table = [],
|
|
28 |
skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
|
|
29 |
unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref []}
|
|
30 |
(* term -> bool *)
|
|
31 |
val is_mono = NitpickMono.formulas_monotonic ext_ctxt @{typ 'a} [] []
|
|
32 |
fun is_const t =
|
|
33 |
let val T = fastype_of t in
|
|
34 |
is_mono (Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t),
|
|
35 |
@{const False}))
|
|
36 |
end
|
|
37 |
fun mono t = is_mono t orelse raise FAIL
|
|
38 |
fun nonmono t = not (is_mono t) orelse raise FAIL
|
|
39 |
fun const t = is_const t orelse raise FAIL
|
|
40 |
fun nonconst t = not (is_const t) orelse raise FAIL
|
|
41 |
*}
|
|
42 |
|
|
43 |
ML {* const @{term "A::('a\<Rightarrow>'b)"} *}
|
|
44 |
ML {* const @{term "(A::'a set) = A"} *}
|
|
45 |
ML {* const @{term "(A::'a set set) = A"} *}
|
|
46 |
ML {* const @{term "(\<lambda>x::'a set. x a)"} *}
|
|
47 |
ML {* const @{term "{{a}} = C"} *}
|
|
48 |
ML {* const @{term "{f::'a\<Rightarrow>nat} = {g::'a\<Rightarrow>nat}"} *}
|
|
49 |
ML {* const @{term "A \<union> B"} *}
|
|
50 |
ML {* const @{term "P (a::'a)"} *}
|
|
51 |
ML {* const @{term "\<lambda>a::'a. b (c (d::'a)) (e::'a) (f::'a)"} *}
|
|
52 |
ML {* const @{term "\<forall>A::'a set. A a"} *}
|
|
53 |
ML {* const @{term "\<forall>A::'a set. P A"} *}
|
|
54 |
ML {* const @{term "P \<or> Q"} *}
|
|
55 |
ML {* const @{term "A \<union> B = C"} *}
|
|
56 |
ML {* const @{term "(if P then (A::'a set) else B) = C"} *}
|
|
57 |
ML {* const @{term "let A = C in A \<union> B"} *}
|
|
58 |
ML {* const @{term "THE x::'b. P x"} *}
|
|
59 |
ML {* const @{term "{}::'a set"} *}
|
|
60 |
ML {* const @{term "(\<lambda>x::'a. True)"} *}
|
|
61 |
ML {* const @{term "Let a A"} *}
|
|
62 |
ML {* const @{term "A (a::'a)"} *}
|
|
63 |
ML {* const @{term "insert a A = B"} *}
|
|
64 |
ML {* const @{term "- (A::'a set)"} *}
|
|
65 |
ML {* const @{term "finite A"} *}
|
|
66 |
ML {* const @{term "\<not> finite A"} *}
|
|
67 |
ML {* const @{term "finite (A::'a set set)"} *}
|
|
68 |
ML {* const @{term "\<lambda>a::'a. A a \<and> \<not> B a"} *}
|
|
69 |
ML {* const @{term "A < (B::'a set)"} *}
|
|
70 |
ML {* const @{term "A \<le> (B::'a set)"} *}
|
|
71 |
ML {* const @{term "[a::'a]"} *}
|
|
72 |
ML {* const @{term "[a::'a set]"} *}
|
|
73 |
ML {* const @{term "[A \<union> (B::'a set)]"} *}
|
|
74 |
ML {* const @{term "[A \<union> (B::'a set)] = [C]"} *}
|
|
75 |
ML {* const @{term "\<forall>P. P a"} *}
|
|
76 |
|
|
77 |
ML {* nonconst @{term "{%x. True}"} *}
|
|
78 |
ML {* nonconst @{term "{(%x. x = a)} = C"} *}
|
|
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"} *}
|
|
82 |
ML {* nonconst @{term "THE x. P x"} *}
|
|
83 |
ML {* nonconst @{term "SOME x. P x"} *}
|
|
84 |
|
|
85 |
ML {* mono @{prop "Q (\<forall>x::'a set. P x)"} *}
|
|
86 |
ML {* mono @{prop "P (a::'a)"} *}
|
|
87 |
ML {* mono @{prop "{a} = {b}"} *}
|
|
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)"} *}
|
|
92 |
ML {* mono @{prop "\<not> (\<forall>x. P x)"} *}
|
|
93 |
|
|
94 |
ML {* nonmono @{prop "\<forall>x. P x"} *}
|
|
95 |
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"} *}
|
|
96 |
ML {* nonmono @{prop "myall P = (P = (\<lambda>x. True))"} *}
|
|
97 |
|
|
98 |
end
|