author | blanchet |
Thu, 11 Sep 2014 19:32:36 +0200 | |
changeset 58310 | 91ea607a34d8 |
parent 58305 | 57752a91eec4 |
child 58889 | 5b7a9633cfa8 |
permissions | -rw-r--r-- |
14350 | 1 |
(* Title: HOL/ex/Refute_Examples.thy |
2 |
Author: Tjark Weber |
|
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21559
diff
changeset
|
3 |
Copyright 2003-2007 |
32968 | 4 |
|
5 |
See HOL/Refute.thy for help. |
|
14350 | 6 |
*) |
7 |
||
8 |
header {* Examples for the 'refute' command *} |
|
9 |
||
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
10 |
theory Refute_Examples |
49988 | 11 |
imports "~~/src/HOL/Library/Refute" |
15297 | 12 |
begin |
14350 | 13 |
|
56851
35ff4ede3409
renamed 'dpll_p' to 'cdclite', to avoid confusion with the old 'dpll' and to reflect the idea that the new prover implements some ideas from CDCL not in DPLL -- this follows its author's, Sascha B.'s, wish
blanchet
parents:
56845
diff
changeset
|
14 |
refute_params [satsolver = "cdclite"] |
18774 | 15 |
|
14350 | 16 |
lemma "P \<and> Q" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
17 |
apply (rule conjI) |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
18 |
refute [expect = genuine] 1 -- {* refutes @{term "P"} *} |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
19 |
refute [expect = genuine] 2 -- {* refutes @{term "Q"} *} |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
20 |
refute [expect = genuine] -- {* equivalent to 'refute 1' *} |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
21 |
-- {* here 'refute 3' would cause an exception, since we only have 2 subgoals *} |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
22 |
refute [maxsize = 5, expect = genuine] -- {* we can override parameters ... *} |
56851
35ff4ede3409
renamed 'dpll_p' to 'cdclite', to avoid confusion with the old 'dpll' and to reflect the idea that the new prover implements some ideas from CDCL not in DPLL -- this follows its author's, Sascha B.'s, wish
blanchet
parents:
56845
diff
changeset
|
23 |
refute [satsolver = "cdclite", expect = genuine] 2 |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
24 |
-- {* ... and specify a subgoal at the same time *} |
14350 | 25 |
oops |
26 |
||
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
27 |
(*****************************************************************************) |
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21559
diff
changeset
|
28 |
|
23219 | 29 |
subsection {* Examples and Test Cases *} |
14350 | 30 |
|
23219 | 31 |
subsubsection {* Propositional logic *} |
14350 | 32 |
|
33 |
lemma "True" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
34 |
refute [expect = none] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
35 |
by auto |
14350 | 36 |
|
37 |
lemma "False" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
38 |
refute [expect = genuine] |
14350 | 39 |
oops |
40 |
||
41 |
lemma "P" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
42 |
refute [expect = genuine] |
14350 | 43 |
oops |
44 |
||
45 |
lemma "~ P" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
46 |
refute [expect = genuine] |
14350 | 47 |
oops |
48 |
||
49 |
lemma "P & Q" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
50 |
refute [expect = genuine] |
14350 | 51 |
oops |
52 |
||
53 |
lemma "P | Q" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
54 |
refute [expect = genuine] |
14350 | 55 |
oops |
56 |
||
57 |
lemma "P \<longrightarrow> Q" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
58 |
refute [expect = genuine] |
14350 | 59 |
oops |
60 |
||
61 |
lemma "(P::bool) = Q" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
62 |
refute [expect = genuine] |
14350 | 63 |
oops |
64 |
||
65 |
lemma "(P | Q) \<longrightarrow> (P & Q)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
66 |
refute [expect = genuine] |
14350 | 67 |
oops |
68 |
||
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
69 |
(*****************************************************************************) |
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21559
diff
changeset
|
70 |
|
23219 | 71 |
subsubsection {* Predicate logic *} |
14350 | 72 |
|
14455 | 73 |
lemma "P x y z" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
74 |
refute [expect = genuine] |
14350 | 75 |
oops |
76 |
||
77 |
lemma "P x y \<longrightarrow> P y x" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
78 |
refute [expect = genuine] |
14350 | 79 |
oops |
80 |
||
14455 | 81 |
lemma "P (f (f x)) \<longrightarrow> P x \<longrightarrow> P (f x)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
82 |
refute [expect = genuine] |
14455 | 83 |
oops |
84 |
||
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
85 |
(*****************************************************************************) |
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21559
diff
changeset
|
86 |
|
23219 | 87 |
subsubsection {* Equality *} |
14350 | 88 |
|
89 |
lemma "P = True" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
90 |
refute [expect = genuine] |
14350 | 91 |
oops |
92 |
||
93 |
lemma "P = False" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
94 |
refute [expect = genuine] |
14350 | 95 |
oops |
96 |
||
97 |
lemma "x = y" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
98 |
refute [expect = genuine] |
14350 | 99 |
oops |
100 |
||
101 |
lemma "f x = g x" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
102 |
refute [expect = genuine] |
14350 | 103 |
oops |
104 |
||
105 |
lemma "(f::'a\<Rightarrow>'b) = g" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
106 |
refute [expect = genuine] |
14350 | 107 |
oops |
108 |
||
109 |
lemma "(f::('d\<Rightarrow>'d)\<Rightarrow>('c\<Rightarrow>'d)) = g" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
110 |
refute [expect = genuine] |
14350 | 111 |
oops |
112 |
||
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
113 |
lemma "distinct [a, b]" |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
114 |
(* refute *) |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
115 |
apply simp |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
116 |
refute [expect = genuine] |
14350 | 117 |
oops |
118 |
||
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
119 |
(*****************************************************************************) |
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21559
diff
changeset
|
120 |
|
23219 | 121 |
subsubsection {* First-Order Logic *} |
14350 | 122 |
|
123 |
lemma "\<exists>x. P x" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
124 |
refute [expect = genuine] |
14350 | 125 |
oops |
126 |
||
127 |
lemma "\<forall>x. P x" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
128 |
refute [expect = genuine] |
14350 | 129 |
oops |
130 |
||
131 |
lemma "EX! x. P x" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
132 |
refute [expect = genuine] |
14350 | 133 |
oops |
134 |
||
135 |
lemma "Ex P" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
136 |
refute [expect = genuine] |
14350 | 137 |
oops |
138 |
||
139 |
lemma "All P" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
140 |
refute [expect = genuine] |
14350 | 141 |
oops |
142 |
||
143 |
lemma "Ex1 P" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
144 |
refute [expect = genuine] |
14350 | 145 |
oops |
146 |
||
147 |
lemma "(\<exists>x. P x) \<longrightarrow> (\<forall>x. P x)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
148 |
refute [expect = genuine] |
14350 | 149 |
oops |
150 |
||
151 |
lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
152 |
refute [expect = genuine] |
14350 | 153 |
oops |
154 |
||
155 |
lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
156 |
refute [expect = genuine] |
14350 | 157 |
oops |
158 |
||
159 |
text {* A true statement (also testing names of free and bound variables being identical) *} |
|
160 |
||
161 |
lemma "(\<forall>x y. P x y \<longrightarrow> P y x) \<longrightarrow> (\<forall>x. P x y) \<longrightarrow> P y x" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
162 |
refute [maxsize = 4, expect = none] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
163 |
by fast |
14350 | 164 |
|
18789 | 165 |
text {* "A type has at most 4 elements." *} |
14350 | 166 |
|
18789 | 167 |
lemma "a=b | a=c | a=d | a=e | b=c | b=d | b=e | c=d | c=e | d=e" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
168 |
refute [expect = genuine] |
14455 | 169 |
oops |
170 |
||
18789 | 171 |
lemma "\<forall>a b c d e. a=b | a=c | a=d | a=e | b=c | b=d | b=e | c=d | c=e | d=e" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
172 |
refute [expect = genuine] |
14350 | 173 |
oops |
174 |
||
175 |
text {* "Every reflexive and symmetric relation is transitive." *} |
|
176 |
||
177 |
lemma "\<lbrakk> \<forall>x. P x x; \<forall>x y. P x y \<longrightarrow> P y x \<rbrakk> \<Longrightarrow> P x y \<longrightarrow> P y z \<longrightarrow> P x z" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
178 |
refute [expect = genuine] |
14350 | 179 |
oops |
180 |
||
14465 | 181 |
text {* The "Drinker's theorem" ... *} |
14350 | 182 |
|
183 |
lemma "\<exists>x. f x = g x \<longrightarrow> f = g" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
184 |
refute [maxsize = 4, expect = none] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
185 |
by (auto simp add: ext) |
14350 | 186 |
|
14465 | 187 |
text {* ... and an incorrect version of it *} |
14350 | 188 |
|
189 |
lemma "(\<exists>x. f x = g x) \<longrightarrow> f = g" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
190 |
refute [expect = genuine] |
14350 | 191 |
oops |
192 |
||
193 |
text {* "Every function has a fixed point." *} |
|
194 |
||
195 |
lemma "\<exists>x. f x = x" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
196 |
refute [expect = genuine] |
14350 | 197 |
oops |
198 |
||
199 |
text {* "Function composition is commutative." *} |
|
200 |
||
201 |
lemma "f (g x) = g (f x)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
202 |
refute [expect = genuine] |
14350 | 203 |
oops |
204 |
||
205 |
text {* "Two functions that are equivalent wrt.\ the same predicate 'P' are equal." *} |
|
206 |
||
207 |
lemma "((P::('a\<Rightarrow>'b)\<Rightarrow>bool) f = P g) \<longrightarrow> (f x = g x)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
208 |
refute [expect = genuine] |
14350 | 209 |
oops |
210 |
||
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
211 |
(*****************************************************************************) |
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21559
diff
changeset
|
212 |
|
23219 | 213 |
subsubsection {* Higher-Order Logic *} |
14350 | 214 |
|
215 |
lemma "\<exists>P. P" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
216 |
refute [expect = none] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
217 |
by auto |
14350 | 218 |
|
219 |
lemma "\<forall>P. P" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
220 |
refute [expect = genuine] |
14350 | 221 |
oops |
222 |
||
223 |
lemma "EX! P. P" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
224 |
refute [expect = none] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
225 |
by auto |
14350 | 226 |
|
227 |
lemma "EX! P. P x" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
228 |
refute [expect = genuine] |
14350 | 229 |
oops |
230 |
||
231 |
lemma "P Q | Q x" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
232 |
refute [expect = genuine] |
14350 | 233 |
oops |
234 |
||
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21559
diff
changeset
|
235 |
lemma "x \<noteq> All" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
236 |
refute [expect = genuine] |
14455 | 237 |
oops |
238 |
||
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21559
diff
changeset
|
239 |
lemma "x \<noteq> Ex" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
240 |
refute [expect = genuine] |
14455 | 241 |
oops |
242 |
||
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21559
diff
changeset
|
243 |
lemma "x \<noteq> Ex1" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
244 |
refute [expect = genuine] |
14455 | 245 |
oops |
246 |
||
14350 | 247 |
text {* "The transitive closure 'T' of an arbitrary relation 'P' is non-empty." *} |
248 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset
|
249 |
definition "trans" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where |
14350 | 250 |
"trans P == (ALL x y z. P x y \<longrightarrow> P y z \<longrightarrow> P x z)" |
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset
|
251 |
|
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset
|
252 |
definition "subset" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where |
14350 | 253 |
"subset P Q == (ALL x y. P x y \<longrightarrow> Q x y)" |
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset
|
254 |
|
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset
|
255 |
definition "trans_closure" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where |
14350 | 256 |
"trans_closure P Q == (subset Q P) & (trans P) & (ALL R. subset Q R \<longrightarrow> trans R \<longrightarrow> subset P R)" |
257 |
||
258 |
lemma "trans_closure T P \<longrightarrow> (\<exists>x y. T x y)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
259 |
refute [expect = genuine] |
14350 | 260 |
oops |
261 |
||
262 |
text {* "The union of transitive closures is equal to the transitive closure of unions." *} |
|
263 |
||
264 |
lemma "(\<forall>x y. (P x y | R x y) \<longrightarrow> T x y) \<longrightarrow> trans T \<longrightarrow> (\<forall>Q. (\<forall>x y. (P x y | R x y) \<longrightarrow> Q x y) \<longrightarrow> trans Q \<longrightarrow> subset T Q) |
|
265 |
\<longrightarrow> trans_closure TP P |
|
266 |
\<longrightarrow> trans_closure TR R |
|
267 |
\<longrightarrow> (T x y = (TP x y | TR x y))" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
268 |
refute [expect = genuine] |
14350 | 269 |
oops |
270 |
||
271 |
text {* "Every surjective function is invertible." *} |
|
272 |
||
273 |
lemma "(\<forall>y. \<exists>x. y = f x) \<longrightarrow> (\<exists>g. \<forall>x. g (f x) = x)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
274 |
refute [expect = genuine] |
14350 | 275 |
oops |
276 |
||
277 |
text {* "Every invertible function is surjective." *} |
|
278 |
||
279 |
lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
280 |
refute [expect = genuine] |
14350 | 281 |
oops |
282 |
||
283 |
text {* Every point is a fixed point of some function. *} |
|
284 |
||
285 |
lemma "\<exists>f. f x = x" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
286 |
refute [maxsize = 4, expect = none] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
287 |
apply (rule_tac x="\<lambda>x. x" in exI) |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
288 |
by simp |
14350 | 289 |
|
14465 | 290 |
text {* Axiom of Choice: first an incorrect version ... *} |
14350 | 291 |
|
292 |
lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
293 |
refute [expect = genuine] |
14350 | 294 |
oops |
295 |
||
14465 | 296 |
text {* ... and now two correct ones *} |
14350 | 297 |
|
298 |
lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>f. \<forall>x. P x (f x))" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
299 |
refute [maxsize = 4, expect = none] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
300 |
by (simp add: choice) |
14350 | 301 |
|
302 |
lemma "(\<forall>x. EX!y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
303 |
refute [maxsize = 2, expect = none] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
304 |
apply auto |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
305 |
apply (simp add: ex1_implies_ex choice) |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
306 |
by (fast intro: ext) |
14350 | 307 |
|
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
308 |
(*****************************************************************************) |
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21559
diff
changeset
|
309 |
|
23219 | 310 |
subsubsection {* Meta-logic *} |
14350 | 311 |
|
312 |
lemma "!!x. P x" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
313 |
refute [expect = genuine] |
14350 | 314 |
oops |
315 |
||
316 |
lemma "f x == g x" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
317 |
refute [expect = genuine] |
14350 | 318 |
oops |
319 |
||
320 |
lemma "P \<Longrightarrow> Q" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
321 |
refute [expect = genuine] |
14350 | 322 |
oops |
323 |
||
324 |
lemma "\<lbrakk> P; Q; R \<rbrakk> \<Longrightarrow> S" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
325 |
refute [expect = genuine] |
14350 | 326 |
oops |
327 |
||
56245 | 328 |
lemma "(x == Pure.all) \<Longrightarrow> False" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
329 |
refute [expect = genuine] |
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21559
diff
changeset
|
330 |
oops |
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21559
diff
changeset
|
331 |
|
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21559
diff
changeset
|
332 |
lemma "(x == (op ==)) \<Longrightarrow> False" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
333 |
refute [expect = genuine] |
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21559
diff
changeset
|
334 |
oops |
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21559
diff
changeset
|
335 |
|
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21559
diff
changeset
|
336 |
lemma "(x == (op \<Longrightarrow>)) \<Longrightarrow> False" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
337 |
refute [expect = genuine] |
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21559
diff
changeset
|
338 |
oops |
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21559
diff
changeset
|
339 |
|
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
340 |
(*****************************************************************************) |
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21559
diff
changeset
|
341 |
|
23219 | 342 |
subsubsection {* Schematic variables *} |
14350 | 343 |
|
36319 | 344 |
schematic_lemma "?P" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
345 |
refute [expect = none] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
346 |
by auto |
14350 | 347 |
|
36319 | 348 |
schematic_lemma "x = ?y" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
349 |
refute [expect = none] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
350 |
by auto |
14350 | 351 |
|
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21559
diff
changeset
|
352 |
(******************************************************************************) |
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21559
diff
changeset
|
353 |
|
23219 | 354 |
subsubsection {* Abstractions *} |
14350 | 355 |
|
356 |
lemma "(\<lambda>x. x) = (\<lambda>x. y)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
357 |
refute [expect = genuine] |
14350 | 358 |
oops |
359 |
||
360 |
lemma "(\<lambda>f. f x) = (\<lambda>f. True)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
361 |
refute [expect = genuine] |
14350 | 362 |
oops |
363 |
||
364 |
lemma "(\<lambda>x. x) = (\<lambda>y. y)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
365 |
refute |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
366 |
by simp |
14350 | 367 |
|
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
368 |
(*****************************************************************************) |
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21559
diff
changeset
|
369 |
|
23219 | 370 |
subsubsection {* Sets *} |
14350 | 371 |
|
372 |
lemma "P (A::'a set)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
373 |
refute |
14350 | 374 |
oops |
375 |
||
376 |
lemma "P (A::'a set set)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
377 |
refute |
14350 | 378 |
oops |
379 |
||
380 |
lemma "{x. P x} = {y. P y}" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
381 |
refute |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
382 |
by simp |
14350 | 383 |
|
384 |
lemma "x : {x. P x}" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
385 |
refute |
14350 | 386 |
oops |
387 |
||
14455 | 388 |
lemma "P op:" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
389 |
refute |
14455 | 390 |
oops |
391 |
||
392 |
lemma "P (op: x)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
393 |
refute |
14455 | 394 |
oops |
395 |
||
396 |
lemma "P Collect" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
397 |
refute |
14455 | 398 |
oops |
399 |
||
14350 | 400 |
lemma "A Un B = A Int B" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
401 |
refute |
14350 | 402 |
oops |
403 |
||
404 |
lemma "(A Int B) Un C = (A Un C) Int B" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
405 |
refute |
14350 | 406 |
oops |
407 |
||
408 |
lemma "Ball A P \<longrightarrow> Bex A P" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
409 |
refute |
14455 | 410 |
oops |
411 |
||
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
412 |
(*****************************************************************************) |
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21559
diff
changeset
|
413 |
|
28524 | 414 |
subsubsection {* undefined *} |
14455 | 415 |
|
28524 | 416 |
lemma "undefined" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
417 |
refute [expect = genuine] |
14455 | 418 |
oops |
419 |
||
28524 | 420 |
lemma "P undefined" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
421 |
refute [expect = genuine] |
14455 | 422 |
oops |
423 |
||
28524 | 424 |
lemma "undefined x" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
425 |
refute [expect = genuine] |
14455 | 426 |
oops |
427 |
||
28524 | 428 |
lemma "undefined undefined" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
429 |
refute [expect = genuine] |
14455 | 430 |
oops |
431 |
||
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
432 |
(*****************************************************************************) |
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21559
diff
changeset
|
433 |
|
23219 | 434 |
subsubsection {* The *} |
14455 | 435 |
|
436 |
lemma "The P" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
437 |
refute [expect = genuine] |
14455 | 438 |
oops |
439 |
||
440 |
lemma "P The" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
441 |
refute [expect = genuine] |
14350 | 442 |
oops |
443 |
||
14455 | 444 |
lemma "P (The P)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
445 |
refute [expect = genuine] |
14455 | 446 |
oops |
447 |
||
448 |
lemma "(THE x. x=y) = z" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
449 |
refute [expect = genuine] |
14455 | 450 |
oops |
451 |
||
452 |
lemma "Ex P \<longrightarrow> P (The P)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
453 |
refute [expect = genuine] |
14455 | 454 |
oops |
455 |
||
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
456 |
(*****************************************************************************) |
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21559
diff
changeset
|
457 |
|
23219 | 458 |
subsubsection {* Eps *} |
14455 | 459 |
|
460 |
lemma "Eps P" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
461 |
refute [expect = genuine] |
14455 | 462 |
oops |
463 |
||
464 |
lemma "P Eps" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
465 |
refute [expect = genuine] |
14455 | 466 |
oops |
467 |
||
468 |
lemma "P (Eps P)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
469 |
refute [expect = genuine] |
14455 | 470 |
oops |
471 |
||
472 |
lemma "(SOME x. x=y) = z" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
473 |
refute [expect = genuine] |
14455 | 474 |
oops |
475 |
||
476 |
lemma "Ex P \<longrightarrow> P (Eps P)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
477 |
refute [maxsize = 3, expect = none] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
478 |
by (auto simp add: someI) |
14455 | 479 |
|
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
480 |
(*****************************************************************************) |
15767
8ed9fcc004fe
support for recursion over mutually recursive IDTs
webertj
parents:
15547
diff
changeset
|
481 |
|
23219 | 482 |
subsubsection {* Subtypes (typedef), typedecl *} |
14809 | 483 |
|
15161 | 484 |
text {* A completely unspecified non-empty subset of @{typ "'a"}: *} |
485 |
||
45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
37388
diff
changeset
|
486 |
definition "myTdef = insert (undefined::'a) (undefined::'a set)" |
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
37388
diff
changeset
|
487 |
|
49834 | 488 |
typedef 'a myTdef = "myTdef :: 'a set" |
45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
37388
diff
changeset
|
489 |
unfolding myTdef_def by auto |
14809 | 490 |
|
491 |
lemma "(x::'a myTdef) = y" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
492 |
refute |
14809 | 493 |
oops |
494 |
||
495 |
typedecl myTdecl |
|
496 |
||
45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
37388
diff
changeset
|
497 |
definition "T_bij = {(f::'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}" |
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
37388
diff
changeset
|
498 |
|
49834 | 499 |
typedef 'a T_bij = "T_bij :: ('a \<Rightarrow> 'a) set" |
45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
37388
diff
changeset
|
500 |
unfolding T_bij_def by auto |
14809 | 501 |
|
502 |
lemma "P (f::(myTdecl myTdef) T_bij)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
503 |
refute |
14809 | 504 |
oops |
505 |
||
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
506 |
(*****************************************************************************) |
15767
8ed9fcc004fe
support for recursion over mutually recursive IDTs
webertj
parents:
15547
diff
changeset
|
507 |
|
23219 | 508 |
subsubsection {* Inductive datatypes *} |
14350 | 509 |
|
23219 | 510 |
text {* unit *} |
14350 | 511 |
|
512 |
lemma "P (x::unit)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
513 |
refute [expect = genuine] |
14350 | 514 |
oops |
515 |
||
516 |
lemma "\<forall>x::unit. P x" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
517 |
refute [expect = genuine] |
14350 | 518 |
oops |
519 |
||
520 |
lemma "P ()" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
521 |
refute [expect = genuine] |
14350 | 522 |
oops |
523 |
||
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
524 |
lemma "P (case x of () \<Rightarrow> u)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
525 |
refute [expect = genuine] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
526 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
527 |
|
23219 | 528 |
text {* option *} |
14455 | 529 |
|
530 |
lemma "P (x::'a option)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
531 |
refute [expect = genuine] |
14455 | 532 |
oops |
533 |
||
534 |
lemma "\<forall>x::'a option. P x" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
535 |
refute [expect = genuine] |
14455 | 536 |
oops |
537 |
||
14809 | 538 |
lemma "P None" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
539 |
refute [expect = genuine] |
14809 | 540 |
oops |
541 |
||
14455 | 542 |
lemma "P (Some x)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
543 |
refute [expect = genuine] |
14455 | 544 |
oops |
545 |
||
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
546 |
lemma "P (case x of None \<Rightarrow> n | Some u \<Rightarrow> s u)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
547 |
refute [expect = genuine] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
548 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
549 |
|
23219 | 550 |
text {* * *} |
14350 | 551 |
|
552 |
lemma "P (x::'a*'b)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
553 |
refute [expect = genuine] |
14350 | 554 |
oops |
555 |
||
556 |
lemma "\<forall>x::'a*'b. P x" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
557 |
refute [expect = genuine] |
14350 | 558 |
oops |
559 |
||
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
560 |
lemma "P (x, y)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
561 |
refute [expect = genuine] |
14350 | 562 |
oops |
563 |
||
564 |
lemma "P (fst x)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
565 |
refute [expect = genuine] |
14350 | 566 |
oops |
567 |
||
568 |
lemma "P (snd x)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
569 |
refute [expect = genuine] |
14455 | 570 |
oops |
571 |
||
572 |
lemma "P Pair" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
573 |
refute [expect = genuine] |
14350 | 574 |
oops |
575 |
||
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
576 |
lemma "P (case x of Pair a b \<Rightarrow> p a b)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
577 |
refute [expect = genuine] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
578 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
579 |
|
23219 | 580 |
text {* + *} |
14350 | 581 |
|
582 |
lemma "P (x::'a+'b)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
583 |
refute [expect = genuine] |
14350 | 584 |
oops |
585 |
||
586 |
lemma "\<forall>x::'a+'b. P x" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
587 |
refute [expect = genuine] |
14350 | 588 |
oops |
589 |
||
590 |
lemma "P (Inl x)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
591 |
refute [expect = genuine] |
14350 | 592 |
oops |
593 |
||
594 |
lemma "P (Inr x)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
595 |
refute [expect = genuine] |
14455 | 596 |
oops |
597 |
||
598 |
lemma "P Inl" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
599 |
refute [expect = genuine] |
14350 | 600 |
oops |
601 |
||
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
602 |
lemma "P (case x of Inl a \<Rightarrow> l a | Inr b \<Rightarrow> r b)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
603 |
refute [expect = genuine] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
604 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
605 |
|
23219 | 606 |
text {* Non-recursive datatypes *} |
14350 | 607 |
|
58310 | 608 |
datatype T1 = A | B |
14350 | 609 |
|
610 |
lemma "P (x::T1)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
611 |
refute [expect = genuine] |
14350 | 612 |
oops |
613 |
||
614 |
lemma "\<forall>x::T1. P x" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
615 |
refute [expect = genuine] |
14350 | 616 |
oops |
617 |
||
14455 | 618 |
lemma "P A" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
619 |
refute [expect = genuine] |
14350 | 620 |
oops |
621 |
||
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
622 |
lemma "P B" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
623 |
refute [expect = genuine] |
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
624 |
oops |
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
625 |
|
55416 | 626 |
lemma "rec_T1 a b A = a" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
627 |
refute [expect = none] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
628 |
by simp |
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
629 |
|
55416 | 630 |
lemma "rec_T1 a b B = b" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
631 |
refute [expect = none] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
632 |
by simp |
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
633 |
|
55416 | 634 |
lemma "P (rec_T1 a b x)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
635 |
refute [expect = genuine] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
636 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
637 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
638 |
lemma "P (case x of A \<Rightarrow> a | B \<Rightarrow> b)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
639 |
refute [expect = genuine] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
640 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
641 |
|
58310 | 642 |
datatype 'a T2 = C T1 | D 'a |
14455 | 643 |
|
644 |
lemma "P (x::'a T2)" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
645 |
refute [expect = genuine] |
14350 | 646 |
oops |
647 |
||
14455 | 648 |
lemma "\<forall>x::'a T2. P x" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
649 |
refute [expect = genuine] |
14350 | 650 |
oops |
651 |
||
14455 | 652 |
lemma "P D" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
653 |
refute [expect = genuine] |
14350 | 654 |
oops |
655 |
||
55416 | 656 |
lemma "rec_T2 c d (C x) = c x" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
657 |
refute [maxsize = 4, expect = none] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
658 |
by simp |
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
659 |
|
55416 | 660 |
lemma "rec_T2 c d (D x) = d x" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
661 |
refute [maxsize = 4, expect = none] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
662 |
by simp |
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
663 |
|
55416 | 664 |
lemma "P (rec_T2 c d x)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
665 |
refute [expect = genuine] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
666 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
667 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
668 |
lemma "P (case x of C u \<Rightarrow> c u | D v \<Rightarrow> d v)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
669 |
refute [expect = genuine] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
670 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
671 |
|
58310 | 672 |
datatype ('a,'b) T3 = E "'a \<Rightarrow> 'b" |
14455 | 673 |
|
14809 | 674 |
lemma "P (x::('a,'b) T3)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
675 |
refute [expect = genuine] |
14809 | 676 |
oops |
677 |
||
678 |
lemma "\<forall>x::('a,'b) T3. P x" |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
679 |
refute [expect = genuine] |
14809 | 680 |
oops |
681 |
||
14455 | 682 |
lemma "P E" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
683 |
refute [expect = genuine] |
14350 | 684 |
oops |
685 |
||
55416 | 686 |
lemma "rec_T3 e (E x) = e x" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
687 |
refute [maxsize = 2, expect = none] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
688 |
by simp |
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
689 |
|
55416 | 690 |
lemma "P (rec_T3 e x)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
691 |
refute [expect = genuine] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
692 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
693 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
694 |
lemma "P (case x of E f \<Rightarrow> e f)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
695 |
refute [expect = genuine] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
696 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
697 |
|
23219 | 698 |
text {* Recursive datatypes *} |
14350 | 699 |
|
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
700 |
text {* nat *} |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
701 |
|
14809 | 702 |
lemma "P (x::nat)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
703 |
refute [expect = potential] |
14809 | 704 |
oops |
14350 | 705 |
|
14809 | 706 |
lemma "\<forall>x::nat. P x" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
707 |
refute [expect = potential] |
14350 | 708 |
oops |
709 |
||
14809 | 710 |
lemma "P (Suc 0)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
711 |
refute [expect = potential] |
14350 | 712 |
oops |
713 |
||
14809 | 714 |
lemma "P Suc" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
715 |
refute [maxsize = 3, expect = none] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
716 |
-- {* @{term Suc} is a partial function (regardless of the size |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
717 |
of the model), hence @{term "P Suc"} is undefined and no |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
718 |
model will be found *} |
14350 | 719 |
oops |
720 |
||
55415 | 721 |
lemma "rec_nat zero suc 0 = zero" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
722 |
refute [expect = none] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
723 |
by simp |
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
724 |
|
55415 | 725 |
lemma "rec_nat zero suc (Suc x) = suc x (rec_nat zero suc x)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
726 |
refute [maxsize = 2, expect = none] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
727 |
by simp |
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
728 |
|
55415 | 729 |
lemma "P (rec_nat zero suc x)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
730 |
refute [expect = potential] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
731 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
732 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
733 |
lemma "P (case x of 0 \<Rightarrow> zero | Suc n \<Rightarrow> suc n)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
734 |
refute [expect = potential] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
735 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
736 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
737 |
text {* 'a list *} |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
738 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
739 |
lemma "P (xs::'a list)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
740 |
refute [expect = potential] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
741 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
742 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
743 |
lemma "\<forall>xs::'a list. P xs" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
744 |
refute [expect = potential] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
745 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
746 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
747 |
lemma "P [x, y]" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
748 |
refute [expect = potential] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
749 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
750 |
|
55413
a8e96847523c
adapted theories to '{case,rec}_{list,option}' names
blanchet
parents:
55395
diff
changeset
|
751 |
lemma "rec_list nil cons [] = nil" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
752 |
refute [maxsize = 3, expect = none] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
753 |
by simp |
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
754 |
|
55413
a8e96847523c
adapted theories to '{case,rec}_{list,option}' names
blanchet
parents:
55395
diff
changeset
|
755 |
lemma "rec_list nil cons (x#xs) = cons x xs (rec_list nil cons xs)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
756 |
refute [maxsize = 2, expect = none] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
757 |
by simp |
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
758 |
|
55413
a8e96847523c
adapted theories to '{case,rec}_{list,option}' names
blanchet
parents:
55395
diff
changeset
|
759 |
lemma "P (rec_list nil cons xs)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
760 |
refute [expect = potential] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
761 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
762 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
763 |
lemma "P (case x of Nil \<Rightarrow> nil | Cons a b \<Rightarrow> cons a b)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
764 |
refute [expect = potential] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
765 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
766 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
767 |
lemma "(xs::'a list) = ys" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
768 |
refute [expect = potential] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
769 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
770 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
771 |
lemma "a # xs = b # xs" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
772 |
refute [expect = potential] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
773 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
774 |
|
58310 | 775 |
datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList |
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
776 |
|
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
777 |
lemma "P (x::BitList)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
778 |
refute [expect = potential] |
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
779 |
oops |
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
780 |
|
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
781 |
lemma "\<forall>x::BitList. P x" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
782 |
refute [expect = potential] |
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
783 |
oops |
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
784 |
|
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
785 |
lemma "P (Bit0 (Bit1 BitListNil))" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
786 |
refute [expect = potential] |
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
787 |
oops |
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
788 |
|
55416 | 789 |
lemma "rec_BitList nil bit0 bit1 BitListNil = nil" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
790 |
refute [maxsize = 4, expect = none] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
791 |
by simp |
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
792 |
|
55416 | 793 |
lemma "rec_BitList nil bit0 bit1 (Bit0 xs) = bit0 xs (rec_BitList nil bit0 bit1 xs)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
794 |
refute [maxsize = 2, expect = none] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
795 |
by simp |
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
796 |
|
55416 | 797 |
lemma "rec_BitList nil bit0 bit1 (Bit1 xs) = bit1 xs (rec_BitList nil bit0 bit1 xs)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
798 |
refute [maxsize = 2, expect = none] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
799 |
by simp |
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
800 |
|
55416 | 801 |
lemma "P (rec_BitList nil bit0 bit1 x)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
802 |
refute [expect = potential] |
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
803 |
oops |
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
804 |
|
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
805 |
(*****************************************************************************) |
15767
8ed9fcc004fe
support for recursion over mutually recursive IDTs
webertj
parents:
15547
diff
changeset
|
806 |
|
23219 | 807 |
subsubsection {* Examples involving special functions *} |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
808 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
809 |
lemma "card x = 0" |
58143 | 810 |
refute [expect = potential] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
811 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
812 |
|
15767
8ed9fcc004fe
support for recursion over mutually recursive IDTs
webertj
parents:
15547
diff
changeset
|
813 |
lemma "finite x" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
814 |
refute -- {* no finite countermodel exists *} |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
815 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
816 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
817 |
lemma "(x::nat) + y = 0" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
818 |
refute [expect = potential] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
819 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
820 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
821 |
lemma "(x::nat) = x + x" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
822 |
refute [expect = potential] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
823 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
824 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
825 |
lemma "(x::nat) - y + y = x" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
826 |
refute [expect = potential] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
827 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
828 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
829 |
lemma "(x::nat) = x * x" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
830 |
refute [expect = potential] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
831 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
832 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
833 |
lemma "(x::nat) < x + y" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
834 |
refute [expect = potential] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
835 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
836 |
|
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21559
diff
changeset
|
837 |
lemma "xs @ [] = ys @ []" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
838 |
refute [expect = potential] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
839 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
840 |
|
21985
acfb13e8819e
constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents:
21559
diff
changeset
|
841 |
lemma "xs @ ys = ys @ xs" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
842 |
refute [expect = potential] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
843 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
844 |
|
25014
b711b0af178e
significant code overhaul, bugfix for inductive data types
webertj
parents:
24447
diff
changeset
|
845 |
(*****************************************************************************) |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
846 |
|
35315 | 847 |
subsubsection {* Type classes and overloading *} |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
848 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
849 |
text {* A type class without axioms: *} |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
850 |
|
35315 | 851 |
class classA |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
852 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
853 |
lemma "P (x::'a::classA)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
854 |
refute [expect = genuine] |
14809 | 855 |
oops |
856 |
||
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
857 |
text {* An axiom with a type variable (denoting types which have at least two elements): *} |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
858 |
|
35315 | 859 |
class classC = |
860 |
assumes classC_ax: "\<exists>x y. x \<noteq> y" |
|
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
861 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
862 |
lemma "P (x::'a::classC)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
863 |
refute [expect = genuine] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
864 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
865 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
866 |
lemma "\<exists>x y. (x::'a::classC) \<noteq> y" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
867 |
(* refute [expect = none] FIXME *) |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
868 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
869 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
870 |
text {* A type class for which a constant is defined: *} |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
871 |
|
35315 | 872 |
class classD = |
873 |
fixes classD_const :: "'a \<Rightarrow> 'a" |
|
874 |
assumes classD_ax: "classD_const (classD_const x) = classD_const x" |
|
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
875 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
876 |
lemma "P (x::'a::classD)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
877 |
refute [expect = genuine] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
878 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
879 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
880 |
text {* A type class with multiple superclasses: *} |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
881 |
|
35315 | 882 |
class classE = classC + classD |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
883 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
884 |
lemma "P (x::'a::classE)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
885 |
refute [expect = genuine] |
14809 | 886 |
oops |
887 |
||
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
888 |
text {* OFCLASS: *} |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
889 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
890 |
lemma "OFCLASS('a::type, type_class)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
891 |
refute [expect = none] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
892 |
by intro_classes |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
893 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
894 |
lemma "OFCLASS('a::classC, type_class)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
895 |
refute [expect = none] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
896 |
by intro_classes |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
897 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
898 |
lemma "OFCLASS('a::type, classC_class)" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
899 |
refute [expect = genuine] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
900 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
901 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
902 |
text {* Overloading: *} |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
903 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
904 |
consts inverse :: "'a \<Rightarrow> 'a" |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
905 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
906 |
defs (overloaded) |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
907 |
inverse_bool: "inverse (b::bool) == ~ b" |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
908 |
inverse_set : "inverse (S::'a set) == -S" |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
909 |
inverse_pair: "inverse p == (inverse (fst p), inverse (snd p))" |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
910 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
911 |
lemma "inverse b" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
912 |
refute [expect = genuine] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
913 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
914 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
915 |
lemma "P (inverse (S::'a set))" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
916 |
refute [expect = genuine] |
15547
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
917 |
oops |
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
918 |
|
f08e2d83681e
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents:
15297
diff
changeset
|
919 |
lemma "P (inverse (p::'a\<times>'b))" |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
920 |
refute [expect = genuine] |
14350 | 921 |
oops |
922 |
||
34120
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
32968
diff
changeset
|
923 |
text {* Structured proofs *} |
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
32968
diff
changeset
|
924 |
|
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
32968
diff
changeset
|
925 |
lemma "x = y" |
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
32968
diff
changeset
|
926 |
proof cases |
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
32968
diff
changeset
|
927 |
assume "x = y" |
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
32968
diff
changeset
|
928 |
show ?thesis |
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
929 |
refute [expect = none] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
930 |
refute [no_assms, expect = genuine] |
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
931 |
refute [no_assms = false, expect = none] |
34120
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
32968
diff
changeset
|
932 |
oops |
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
32968
diff
changeset
|
933 |
|
46099
40ac5ae6d16f
reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents:
45972
diff
changeset
|
934 |
refute_params [satsolver = "auto"] |
18774 | 935 |
|
14350 | 936 |
end |