author  haftmann 
Fri, 20 Jul 2007 14:27:56 +0200  
changeset 23878  bd651ecd4b8a 
parent 23566  b65692d4adcd 
child 23948  261bd4678076 
permissions  rwrr 
923  1 
(* Title: HOL/HOL.thy 
2 
ID: $Id$ 

11750  3 
Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson 
4 
*) 

923  5 

11750  6 
header {* The basis of HigherOrder Logic *} 
923  7 

15131  8 
theory HOL 
15140  9 
imports CPure 
23163  10 
uses 
23247  11 
"~~/src/Tools/integer.ML" 
23553  12 
("hologic.ML") 
23171  13 
"~~/src/Tools/IsaPlanner/zipper.ML" 
14 
"~~/src/Tools/IsaPlanner/isand.ML" 

15 
"~~/src/Tools/IsaPlanner/rw_tools.ML" 

16 
"~~/src/Tools/IsaPlanner/rw_inst.ML" 

23263  17 
"~~/src/Provers/project_rule.ML" 
23163  18 
"~~/src/Provers/induct_method.ML" 
23263  19 
"~~/src/Provers/hypsubst.ML" 
20 
"~~/src/Provers/splitter.ML" 

23163  21 
"~~/src/Provers/classical.ML" 
22 
"~~/src/Provers/blast.ML" 

23 
"~~/src/Provers/clasimp.ML" 

23263  24 
"~~/src/Provers/eqsubst.ML" 
23163  25 
"~~/src/Provers/quantifier1.ML" 
26 
("simpdata.ML") 

23263  27 
"Tools/res_atpset.ML" 
23247  28 
("~~/src/HOL/Tools/recfun_codegen.ML") 
15131  29 
begin 
2260  30 

11750  31 
subsection {* Primitive logic *} 
32 

33 
subsubsection {* Core syntax *} 

2260  34 

14854  35 
classes type 
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12281
diff
changeset

36 
defaultsort type 
3947  37 

12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12281
diff
changeset

38 
global 
923  39 

7357  40 
typedecl bool 
923  41 

42 
arities 

12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12281
diff
changeset

43 
bool :: type 
20590
bf92900995f8
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
haftmann
parents:
20453
diff
changeset

44 
"fun" :: (type, type) type 
923  45 

11750  46 
judgment 
47 
Trueprop :: "bool => prop" ("(_)" 5) 

923  48 

11750  49 
consts 
7357  50 
Not :: "bool => bool" ("~ _" [40] 40) 
51 
True :: bool 

52 
False :: bool 

3947  53 
arbitrary :: 'a 
923  54 

11432
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
10489
diff
changeset

55 
The :: "('a => bool) => 'a" 
7357  56 
All :: "('a => bool) => bool" (binder "ALL " 10) 
57 
Ex :: "('a => bool) => bool" (binder "EX " 10) 

58 
Ex1 :: "('a => bool) => bool" (binder "EX! " 10) 

59 
Let :: "['a, 'a => 'b] => 'b" 

923  60 

22839  61 
"op =" :: "['a, 'a] => bool" (infixl "=" 50) 
62 
"op &" :: "[bool, bool] => bool" (infixr "&" 35) 

63 
"op " :: "[bool, bool] => bool" (infixr "" 30) 

64 
"op >" :: "[bool, bool] => bool" (infixr ">" 25) 

923  65 

10432
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset

66 
local 
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset

67 

16587  68 
consts 
69 
If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) 

2260  70 

19656
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

71 

11750  72 
subsubsection {* Additional concrete syntax *} 
2260  73 

21210  74 
notation (output) 
19656
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

75 
"op =" (infix "=" 50) 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

76 

09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

77 
abbreviation 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21250
diff
changeset

78 
not_equal :: "['a, 'a] => bool" (infixl "~=" 50) where 
19656
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

79 
"x ~= y == ~ (x = y)" 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

80 

21210  81 
notation (output) 
19656
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

82 
not_equal (infix "~=" 50) 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

83 

21210  84 
notation (xsymbols) 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21250
diff
changeset

85 
Not ("\<not> _" [40] 40) and 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21250
diff
changeset

86 
"op &" (infixr "\<and>" 35) and 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21250
diff
changeset

87 
"op " (infixr "\<or>" 30) and 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21250
diff
changeset

88 
"op >" (infixr "\<longrightarrow>" 25) and 
19656
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

89 
not_equal (infix "\<noteq>" 50) 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

90 

21210  91 
notation (HTML output) 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21250
diff
changeset

92 
Not ("\<not> _" [40] 40) and 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21250
diff
changeset

93 
"op &" (infixr "\<and>" 35) and 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21250
diff
changeset

94 
"op " (infixr "\<or>" 30) and 
19656
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

95 
not_equal (infix "\<noteq>" 50) 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

96 

09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

97 
abbreviation (iff) 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21250
diff
changeset

98 
iff :: "[bool, bool] => bool" (infixr "<>" 25) where 
19656
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

99 
"A <> B == A = B" 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

100 

21210  101 
notation (xsymbols) 
19656
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

102 
iff (infixr "\<longleftrightarrow>" 25) 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

103 

09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

104 

4868  105 
nonterminals 
923  106 
letbinds letbind 
107 
case_syn cases_syn 

108 

109 
syntax 

11432
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
10489
diff
changeset

110 
"_The" :: "[pttrn, bool] => 'a" ("(3THE _./ _)" [0, 10] 10) 
923  111 

7357  112 
"_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) 
113 
"" :: "letbind => letbinds" ("_") 

114 
"_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") 

115 
"_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) 

923  116 

9060
b0dd884b1848
rename @case to _case_syntax (improves on lowlevel errors);
wenzelm
parents:
8959
diff
changeset

117 
"_case_syntax":: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10) 
b0dd884b1848
rename @case to _case_syntax (improves on lowlevel errors);
wenzelm
parents:
8959
diff
changeset

118 
"_case1" :: "['a, 'b] => case_syn" ("(2_ =>/ _)" 10) 
7357  119 
"" :: "case_syn => cases_syn" ("_") 
9060
b0dd884b1848
rename @case to _case_syntax (improves on lowlevel errors);
wenzelm
parents:
8959
diff
changeset

120 
"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/  _") 
923  121 

122 
translations 

13764  123 
"THE x. P" == "The (%x. P)" 
923  124 
"_Let (_binds b bs) e" == "_Let b (_Let bs e)" 
1114  125 
"let x = a in e" == "Let a (%x. e)" 
923  126 

13763
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset

127 
print_translation {* 
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset

128 
(* To avoid etacontraction of body: *) 
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset

129 
[("The", fn [Abs abs] => 
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset

130 
let val (x,t) = atomic_abs_tr' abs 
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset

131 
in Syntax.const "_The" $ x $ t end)] 
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset

132 
*} 
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset

133 

12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
12023
diff
changeset

134 
syntax (xsymbols) 
11687  135 
"_case1" :: "['a, 'b] => case_syn" ("(2_ \<Rightarrow>/ _)" 10) 
21524  136 

137 
notation (xsymbols) 

138 
All (binder "\<forall>" 10) and 

139 
Ex (binder "\<exists>" 10) and 

140 
Ex1 (binder "\<exists>!" 10) 

2372  141 

21524  142 
notation (HTML output) 
143 
All (binder "\<forall>" 10) and 

144 
Ex (binder "\<exists>" 10) and 

145 
Ex1 (binder "\<exists>!" 10) 

6340  146 

21524  147 
notation (HOL) 
148 
All (binder "! " 10) and 

149 
Ex (binder "? " 10) and 

150 
Ex1 (binder "?! " 10) 

7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7220
diff
changeset

151 

36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7220
diff
changeset

152 

11750  153 
subsubsection {* Axioms and basic definitions *} 
2260  154 

7357  155 
axioms 
15380  156 
eq_reflection: "(x=y) ==> (x==y)" 
923  157 

15380  158 
refl: "t = (t::'a)" 
6289  159 

15380  160 
ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)" 
161 
 {*Extensionality is built into the metalogic, and this rule expresses 

162 
a related property. It is an etaexpanded version of the traditional 

163 
rule, and similar to the ABS rule of HOL*} 

6289  164 

11432
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
10489
diff
changeset

165 
the_eq_trivial: "(THE x. x = a) = (a::'a)" 
923  166 

15380  167 
impI: "(P ==> Q) ==> P>Q" 
168 
mp: "[ P>Q; P ] ==> Q" 

169 

170 

923  171 
defs 
7357  172 
True_def: "True == ((%x::bool. x) = (%x. x))" 
173 
All_def: "All(P) == (P = (%x. True))" 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11438
diff
changeset

174 
Ex_def: "Ex(P) == !Q. (!x. P x > Q) > Q" 
7357  175 
False_def: "False == (!P. P)" 
176 
not_def: "~ P == P>False" 

177 
and_def: "P & Q == !R. (P>Q>R) > R" 

178 
or_def: "P  Q == !R. (P>R) > (Q>R) > R" 

179 
Ex1_def: "Ex1(P) == ? x. P(x) & (! y. P(y) > y=x)" 

923  180 

7357  181 
axioms 
182 
iff: "(P>Q) > (Q>P) > (P=Q)" 

183 
True_or_False: "(P=True)  (P=False)" 

923  184 

185 
defs 

22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22481
diff
changeset

186 
Let_def [code func]: "Let s f == f(s)" 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11438
diff
changeset

187 
if_def: "If P x y == THE z::'a. (P=True > z=x) & (P=False > z=y)" 
5069  188 

14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14208
diff
changeset

189 
finalconsts 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14208
diff
changeset

190 
"op =" 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14208
diff
changeset

191 
"op >" 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14208
diff
changeset

192 
The 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14208
diff
changeset

193 
arbitrary 
22481
79c2724c36b5
added class "default" and expansion axioms for undefined
haftmann
parents:
22473
diff
changeset

194 

79c2724c36b5
added class "default" and expansion axioms for undefined
haftmann
parents:
22473
diff
changeset

195 
axiomatization 
79c2724c36b5
added class "default" and expansion axioms for undefined
haftmann
parents:
22473
diff
changeset

196 
undefined :: 'a 
79c2724c36b5
added class "default" and expansion axioms for undefined
haftmann
parents:
22473
diff
changeset

197 

22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22481
diff
changeset

198 
axiomatization where 
22481
79c2724c36b5
added class "default" and expansion axioms for undefined
haftmann
parents:
22473
diff
changeset

199 
undefined_fun: "undefined x = undefined" 
3320  200 

19656
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

201 

22481
79c2724c36b5
added class "default" and expansion axioms for undefined
haftmann
parents:
22473
diff
changeset

202 
subsubsection {* Generic classes and algebraic operations *} 
79c2724c36b5
added class "default" and expansion axioms for undefined
haftmann
parents:
22473
diff
changeset

203 

79c2724c36b5
added class "default" and expansion axioms for undefined
haftmann
parents:
22473
diff
changeset

204 
class default = type + 
79c2724c36b5
added class "default" and expansion axioms for undefined
haftmann
parents:
22473
diff
changeset

205 
fixes default :: "'a" 
4868  206 

22473  207 
class zero = type + 
21524  208 
fixes zero :: "'a" ("\<^loc>0") 
20713
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset

209 

22473  210 
class one = type + 
21524  211 
fixes one :: "'a" ("\<^loc>1") 
20713
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset

212 

823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset

213 
hide (open) const zero one 
20590
bf92900995f8
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
haftmann
parents:
20453
diff
changeset

214 

22473  215 
class plus = type + 
21524  216 
fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>+" 65) 
11750  217 

22473  218 
class minus = type + 
20590
bf92900995f8
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
haftmann
parents:
20453
diff
changeset

219 
fixes uminus :: "'a \<Rightarrow> 'a" 
21524  220 
and minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>" 65) 
20590
bf92900995f8
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
haftmann
parents:
20453
diff
changeset

221 

22473  222 
class times = type + 
20713
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset

223 
fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>*" 70) 
20590
bf92900995f8
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
haftmann
parents:
20453
diff
changeset

224 

22473  225 
class inverse = type + 
20590
bf92900995f8
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
haftmann
parents:
20453
diff
changeset

226 
fixes inverse :: "'a \<Rightarrow> 'a" 
21524  227 
and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>'/" 70) 
228 

23878  229 
class abs = type + 
230 
fixes abs :: "'a \<Rightarrow> 'a" 

231 

21524  232 
notation 
233 
uminus (" _" [81] 80) 

234 

235 
notation (xsymbols) 

236 
abs ("\<bar>_\<bar>") 

237 
notation (HTML output) 

238 
abs ("\<bar>_\<bar>") 

11750  239 

23878  240 
class ord = type + 
241 
fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50) 

242 
and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubset>" 50) 

243 
begin 

244 

245 
notation 

246 
less_eq ("op \<^loc><=") and 

247 
less_eq ("(_/ \<^loc><= _)" [51, 51] 50) and 

248 
less ("op \<^loc><") and 

249 
less ("(_/ \<^loc>< _)" [51, 51] 50) 

250 

251 
notation (xsymbols) 

252 
less_eq ("op \<^loc>\<le>") and 

253 
less_eq ("(_/ \<^loc>\<le> _)" [51, 51] 50) 

254 

255 
notation (HTML output) 

256 
less_eq ("op \<^loc>\<le>") and 

257 
less_eq ("(_/ \<^loc>\<le> _)" [51, 51] 50) 

258 

259 
abbreviation (input) 

260 
greater (infix "\<^loc>>" 50) where 

261 
"x \<^loc>> y \<equiv> y \<^loc>< x" 

262 

263 
abbreviation (input) 

264 
greater_eq (infix "\<^loc>>=" 50) where 

265 
"x \<^loc>>= y \<equiv> y \<^loc><= x" 

266 

267 
notation (input) 

268 
greater_eq (infix "\<^loc>\<ge>" 50) 

269 

270 
definition 

271 
Least :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "\<^loc>LEAST " 10) 

272 
where 

273 
"Least P == (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> x \<^loc>\<le> y))" 

274 

275 
end 

276 

277 
notation 

278 
less_eq ("op <=") and 

279 
less_eq ("(_/ <= _)" [51, 51] 50) and 

280 
less ("op <") and 

281 
less ("(_/ < _)" [51, 51] 50) 

282 

283 
notation (xsymbols) 

284 
less_eq ("op \<le>") and 

285 
less_eq ("(_/ \<le> _)" [51, 51] 50) 

286 

287 
notation (HTML output) 

288 
less_eq ("op \<le>") and 

289 
less_eq ("(_/ \<le> _)" [51, 51] 50) 

290 

291 
abbreviation (input) 

292 
greater (infix ">" 50) where 

293 
"x > y \<equiv> y < x" 

294 

295 
abbreviation (input) 

296 
greater_eq (infix ">=" 50) where 

297 
"x >= y \<equiv> y <= x" 

298 

299 
notation (input) 

300 
greater_eq (infix "\<ge>" 50) 

301 

302 
lemmas Least_def = Least_def [folded ord_class.Least] 

303 

13456
42601eb7553f
special syntax for index "1" (plain numeral hidden by "1" symbol in HOL);
wenzelm
parents:
13438
diff
changeset

304 
syntax 
42601eb7553f
special syntax for index "1" (plain numeral hidden by "1" symbol in HOL);
wenzelm
parents:
13438
diff
changeset

305 
"_index1" :: index ("\<^sub>1") 
42601eb7553f
special syntax for index "1" (plain numeral hidden by "1" symbol in HOL);
wenzelm
parents:
13438
diff
changeset

306 
translations 
14690  307 
(index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>" 
13456
42601eb7553f
special syntax for index "1" (plain numeral hidden by "1" symbol in HOL);
wenzelm
parents:
13438
diff
changeset

308 

11750  309 
typed_print_translation {* 
20713
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset

310 
let 
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset

311 
fun tr' c = (c, fn show_sorts => fn T => fn ts => 
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset

312 
if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match 
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset

313 
else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T); 
22993  314 
in map tr' [@{const_syntax HOL.one}, @{const_syntax HOL.zero}] end; 
11750  315 
*}  {* show types that are presumably too general *} 
316 

317 

20944  318 
subsection {* Fundamental rules *} 
319 

20973  320 
subsubsection {* Equality *} 
20944  321 

322 
text {* Thanks to Stephan Merz *} 

323 
lemma subst: 

324 
assumes eq: "s = t" and p: "P s" 

325 
shows "P t" 

326 
proof  

327 
from eq have meta: "s \<equiv> t" 

328 
by (rule eq_reflection) 

329 
from p show ?thesis 

330 
by (unfold meta) 

331 
qed 

15411  332 

18457  333 
lemma sym: "s = t ==> t = s" 
334 
by (erule subst) (rule refl) 

15411  335 

18457  336 
lemma ssubst: "t = s ==> P s ==> P t" 
337 
by (drule sym) (erule subst) 

15411  338 

339 
lemma trans: "[ r=s; s=t ] ==> r=t" 

18457  340 
by (erule subst) 
15411  341 

20944  342 
lemma meta_eq_to_obj_eq: 
343 
assumes meq: "A == B" 

344 
shows "A = B" 

345 
by (unfold meq) (rule refl) 

15411  346 

21502  347 
text {* Useful with @{text erule} for proving equalities from known equalities. *} 
20944  348 
(* a = b 
15411  349 
  
350 
c = d *) 

351 
lemma box_equals: "[ a=b; a=c; b=d ] ==> c=d" 

352 
apply (rule trans) 

353 
apply (rule trans) 

354 
apply (rule sym) 

355 
apply assumption+ 

356 
done 

357 

15524
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset

358 
text {* For calculational reasoning: *} 
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset

359 

2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset

360 
lemma forw_subst: "a = b ==> P b ==> P a" 
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset

361 
by (rule ssubst) 
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset

362 

2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset

363 
lemma back_subst: "P a ==> a = b ==> P b" 
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset

364 
by (rule subst) 
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset

365 

15411  366 

20944  367 
subsubsection {*Congruence rules for application*} 
15411  368 

369 
(*similar to AP_THM in Gordon's HOL*) 

370 
lemma fun_cong: "(f::'a=>'b) = g ==> f(x)=g(x)" 

371 
apply (erule subst) 

372 
apply (rule refl) 

373 
done 

374 

375 
(*similar to AP_TERM in Gordon's HOL and FOL's subst_context*) 

376 
lemma arg_cong: "x=y ==> f(x)=f(y)" 

377 
apply (erule subst) 

378 
apply (rule refl) 

379 
done 

380 

15655  381 
lemma arg_cong2: "\<lbrakk> a = b; c = d \<rbrakk> \<Longrightarrow> f a c = f b d" 
382 
apply (erule ssubst)+ 

383 
apply (rule refl) 

384 
done 

385 

15411  386 
lemma cong: "[ f = g; (x::'a) = y ] ==> f(x) = g(y)" 
387 
apply (erule subst)+ 

388 
apply (rule refl) 

389 
done 

390 

391 

20944  392 
subsubsection {*Equality of booleans  iff*} 
15411  393 

21504  394 
lemma iffI: assumes "P ==> Q" and "Q ==> P" shows "P=Q" 
395 
by (iprover intro: iff [THEN mp, THEN mp] impI assms) 

15411  396 

397 
lemma iffD2: "[ P=Q; Q ] ==> P" 

18457  398 
by (erule ssubst) 
15411  399 

400 
lemma rev_iffD2: "[ Q; P=Q ] ==> P" 

18457  401 
by (erule iffD2) 
15411  402 

21504  403 
lemma iffD1: "Q = P \<Longrightarrow> Q \<Longrightarrow> P" 
404 
by (drule sym) (rule iffD2) 

405 

406 
lemma rev_iffD1: "Q \<Longrightarrow> Q = P \<Longrightarrow> P" 

407 
by (drule sym) (rule rev_iffD2) 

15411  408 

409 
lemma iffE: 

410 
assumes major: "P=Q" 

21504  411 
and minor: "[ P > Q; Q > P ] ==> R" 
18457  412 
shows R 
413 
by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1]) 

15411  414 

415 

20944  416 
subsubsection {*True*} 
15411  417 

418 
lemma TrueI: "True" 

21504  419 
unfolding True_def by (rule refl) 
15411  420 

21504  421 
lemma eqTrueI: "P ==> P = True" 
18457  422 
by (iprover intro: iffI TrueI) 
15411  423 

21504  424 
lemma eqTrueE: "P = True ==> P" 
425 
by (erule iffD2) (rule TrueI) 

15411  426 

427 

20944  428 
subsubsection {*Universal quantifier*} 
15411  429 

21504  430 
lemma allI: assumes "!!x::'a. P(x)" shows "ALL x. P(x)" 
431 
unfolding All_def by (iprover intro: ext eqTrueI assms) 

15411  432 

433 
lemma spec: "ALL x::'a. P(x) ==> P(x)" 

434 
apply (unfold All_def) 

435 
apply (rule eqTrueE) 

436 
apply (erule fun_cong) 

437 
done 

438 

439 
lemma allE: 

440 
assumes major: "ALL x. P(x)" 

21504  441 
and minor: "P(x) ==> R" 
442 
shows R 

443 
by (iprover intro: minor major [THEN spec]) 

15411  444 

445 
lemma all_dupE: 

446 
assumes major: "ALL x. P(x)" 

21504  447 
and minor: "[ P(x); ALL x. P(x) ] ==> R" 
448 
shows R 

449 
by (iprover intro: minor major major [THEN spec]) 

15411  450 

451 

21504  452 
subsubsection {* False *} 
453 

454 
text {* 

455 
Depends upon @{text spec}; it is impossible to do propositional 

456 
logic before quantifiers! 

457 
*} 

15411  458 

459 
lemma FalseE: "False ==> P" 

21504  460 
apply (unfold False_def) 
461 
apply (erule spec) 

462 
done 

15411  463 

21504  464 
lemma False_neq_True: "False = True ==> P" 
465 
by (erule eqTrueE [THEN FalseE]) 

15411  466 

467 

21504  468 
subsubsection {* Negation *} 
15411  469 

470 
lemma notI: 

21504  471 
assumes "P ==> False" 
15411  472 
shows "~P" 
21504  473 
apply (unfold not_def) 
474 
apply (iprover intro: impI assms) 

475 
done 

15411  476 

477 
lemma False_not_True: "False ~= True" 

21504  478 
apply (rule notI) 
479 
apply (erule False_neq_True) 

480 
done 

15411  481 

482 
lemma True_not_False: "True ~= False" 

21504  483 
apply (rule notI) 
484 
apply (drule sym) 

485 
apply (erule False_neq_True) 

486 
done 

15411  487 

488 
lemma notE: "[ ~P; P ] ==> R" 

21504  489 
apply (unfold not_def) 
490 
apply (erule mp [THEN FalseE]) 

491 
apply assumption 

492 
done 

15411  493 

21504  494 
lemma notI2: "(P \<Longrightarrow> \<not> Pa) \<Longrightarrow> (P \<Longrightarrow> Pa) \<Longrightarrow> \<not> P" 
495 
by (erule notE [THEN notI]) (erule meta_mp) 

15411  496 

497 

20944  498 
subsubsection {*Implication*} 
15411  499 

500 
lemma impE: 

501 
assumes "P>Q" "P" "Q ==> R" 

502 
shows "R" 

23553  503 
by (iprover intro: assms mp) 
15411  504 

505 
(* Reduces Q to P>Q, allowing substitution in P. *) 

506 
lemma rev_mp: "[ P; P > Q ] ==> Q" 

17589  507 
by (iprover intro: mp) 
15411  508 

509 
lemma contrapos_nn: 

510 
assumes major: "~Q" 

511 
and minor: "P==>Q" 

512 
shows "~P" 

17589  513 
by (iprover intro: notI minor major [THEN notE]) 
15411  514 

515 
(*not used at all, but we already have the other 3 combinations *) 

516 
lemma contrapos_pn: 

517 
assumes major: "Q" 

518 
and minor: "P ==> ~Q" 

519 
shows "~P" 

17589  520 
by (iprover intro: notI minor major notE) 
15411  521 

522 
lemma not_sym: "t ~= s ==> s ~= t" 

21250  523 
by (erule contrapos_nn) (erule sym) 
524 

525 
lemma eq_neq_eq_imp_neq: "[ x = a ; a ~= b; b = y ] ==> x ~= y" 

526 
by (erule subst, erule ssubst, assumption) 

15411  527 

528 
(*still used in HOLCF*) 

529 
lemma rev_contrapos: 

530 
assumes pq: "P ==> Q" 

531 
and nq: "~Q" 

532 
shows "~P" 

533 
apply (rule nq [THEN contrapos_nn]) 

534 
apply (erule pq) 

535 
done 

536 

20944  537 
subsubsection {*Existential quantifier*} 
15411  538 

539 
lemma exI: "P x ==> EX x::'a. P x" 

540 
apply (unfold Ex_def) 

17589  541 
apply (iprover intro: allI allE impI mp) 
15411  542 
done 
543 

544 
lemma exE: 

545 
assumes major: "EX x::'a. P(x)" 

546 
and minor: "!!x. P(x) ==> Q" 

547 
shows "Q" 

548 
apply (rule major [unfolded Ex_def, THEN spec, THEN mp]) 

17589  549 
apply (iprover intro: impI [THEN allI] minor) 
15411  550 
done 
551 

552 

20944  553 
subsubsection {*Conjunction*} 
15411  554 

555 
lemma conjI: "[ P; Q ] ==> P&Q" 

556 
apply (unfold and_def) 

17589  557 
apply (iprover intro: impI [THEN allI] mp) 
15411  558 
done 
559 

560 
lemma conjunct1: "[ P & Q ] ==> P" 

561 
apply (unfold and_def) 

17589  562 
apply (iprover intro: impI dest: spec mp) 
15411  563 
done 
564 

565 
lemma conjunct2: "[ P & Q ] ==> Q" 

566 
apply (unfold and_def) 

17589  567 
apply (iprover intro: impI dest: spec mp) 
15411  568 
done 
569 

570 
lemma conjE: 

571 
assumes major: "P&Q" 

572 
and minor: "[ P; Q ] ==> R" 

573 
shows "R" 

574 
apply (rule minor) 

575 
apply (rule major [THEN conjunct1]) 

576 
apply (rule major [THEN conjunct2]) 

577 
done 

578 

579 
lemma context_conjI: 

23553  580 
assumes "P" "P ==> Q" shows "P & Q" 
581 
by (iprover intro: conjI assms) 

15411  582 

583 

20944  584 
subsubsection {*Disjunction*} 
15411  585 

586 
lemma disjI1: "P ==> PQ" 

587 
apply (unfold or_def) 

17589  588 
apply (iprover intro: allI impI mp) 
15411  589 
done 
590 

591 
lemma disjI2: "Q ==> PQ" 

592 
apply (unfold or_def) 

17589  593 
apply (iprover intro: allI impI mp) 
15411  594 
done 
595 

596 
lemma disjE: 

597 
assumes major: "PQ" 

598 
and minorP: "P ==> R" 

599 
and minorQ: "Q ==> R" 

600 
shows "R" 

17589  601 
by (iprover intro: minorP minorQ impI 
15411  602 
major [unfolded or_def, THEN spec, THEN mp, THEN mp]) 
603 

604 

20944  605 
subsubsection {*Classical logic*} 
15411  606 

607 
lemma classical: 

608 
assumes prem: "~P ==> P" 

609 
shows "P" 

610 
apply (rule True_or_False [THEN disjE, THEN eqTrueE]) 

611 
apply assumption 

612 
apply (rule notI [THEN prem, THEN eqTrueI]) 

613 
apply (erule subst) 

614 
apply assumption 

615 
done 

616 

617 
lemmas ccontr = FalseE [THEN classical, standard] 

618 

619 
(*notE with premises exchanged; it discharges ~R so that it can be used to 

620 
make elimination rules*) 

621 
lemma rev_notE: 

622 
assumes premp: "P" 

623 
and premnot: "~R ==> ~P" 

624 
shows "R" 

625 
apply (rule ccontr) 

626 
apply (erule notE [OF premnot premp]) 

627 
done 

628 

629 
(*Double negation law*) 

630 
lemma notnotD: "~~P ==> P" 

631 
apply (rule classical) 

632 
apply (erule notE) 

633 
apply assumption 

634 
done 

635 

636 
lemma contrapos_pp: 

637 
assumes p1: "Q" 

638 
and p2: "~P ==> ~Q" 

639 
shows "P" 

17589  640 
by (iprover intro: classical p1 p2 notE) 
15411  641 

642 

20944  643 
subsubsection {*Unique existence*} 
15411  644 

645 
lemma ex1I: 

23553  646 
assumes "P a" "!!x. P(x) ==> x=a" 
15411  647 
shows "EX! x. P(x)" 
23553  648 
by (unfold Ex1_def, iprover intro: assms exI conjI allI impI) 
15411  649 

650 
text{*Sometimes easier to use: the premises have no shared variables. Safe!*} 

651 
lemma ex_ex1I: 

652 
assumes ex_prem: "EX x. P(x)" 

653 
and eq: "!!x y. [ P(x); P(y) ] ==> x=y" 

654 
shows "EX! x. P(x)" 

17589  655 
by (iprover intro: ex_prem [THEN exE] ex1I eq) 
15411  656 

657 
lemma ex1E: 

658 
assumes major: "EX! x. P(x)" 

659 
and minor: "!!x. [ P(x); ALL y. P(y) > y=x ] ==> R" 

660 
shows "R" 

661 
apply (rule major [unfolded Ex1_def, THEN exE]) 

662 
apply (erule conjE) 

17589  663 
apply (iprover intro: minor) 
15411  664 
done 
665 

666 
lemma ex1_implies_ex: "EX! x. P x ==> EX x. P x" 

667 
apply (erule ex1E) 

668 
apply (rule exI) 

669 
apply assumption 

670 
done 

671 

672 

20944  673 
subsubsection {*THE: definite description operator*} 
15411  674 

675 
lemma the_equality: 

676 
assumes prema: "P a" 

677 
and premx: "!!x. P x ==> x=a" 

678 
shows "(THE x. P x) = a" 

679 
apply (rule trans [OF _ the_eq_trivial]) 

680 
apply (rule_tac f = "The" in arg_cong) 

681 
apply (rule ext) 

682 
apply (rule iffI) 

683 
apply (erule premx) 

684 
apply (erule ssubst, rule prema) 

685 
done 

686 

687 
lemma theI: 

688 
assumes "P a" and "!!x. P x ==> x=a" 

689 
shows "P (THE x. P x)" 

23553  690 
by (iprover intro: assms the_equality [THEN ssubst]) 
15411  691 

692 
lemma theI': "EX! x. P x ==> P (THE x. P x)" 

693 
apply (erule ex1E) 

694 
apply (erule theI) 

695 
apply (erule allE) 

696 
apply (erule mp) 

697 
apply assumption 

698 
done 

699 

700 
(*Easier to apply than theI: only one occurrence of P*) 

701 
lemma theI2: 

702 
assumes "P a" "!!x. P x ==> x=a" "!!x. P x ==> Q x" 

703 
shows "Q (THE x. P x)" 

23553  704 
by (iprover intro: assms theI) 
15411  705 

18697  706 
lemma the1_equality [elim?]: "[ EX!x. P x; P a ] ==> (THE x. P x) = a" 
15411  707 
apply (rule the_equality) 
708 
apply assumption 

709 
apply (erule ex1E) 

710 
apply (erule all_dupE) 

711 
apply (drule mp) 

712 
apply assumption 

713 
apply (erule ssubst) 

714 
apply (erule allE) 

715 
apply (erule mp) 

716 
apply assumption 

717 
done 

718 

719 
lemma the_sym_eq_trivial: "(THE y. x=y) = x" 

720 
apply (rule the_equality) 

721 
apply (rule refl) 

722 
apply (erule sym) 

723 
done 

724 

725 

20944  726 
subsubsection {*Classical intro rules for disjunction and existential quantifiers*} 
15411  727 

728 
lemma disjCI: 

729 
assumes "~Q ==> P" shows "PQ" 

730 
apply (rule classical) 

23553  731 
apply (iprover intro: assms disjI1 disjI2 notI elim: notE) 
15411  732 
done 
733 

734 
lemma excluded_middle: "~P  P" 

17589  735 
by (iprover intro: disjCI) 
15411  736 

20944  737 
text {* 
738 
case distinction as a natural deduction rule. 

739 
Note that @{term "~P"} is the second case, not the first 

740 
*} 

15411  741 
lemma case_split_thm: 
742 
assumes prem1: "P ==> Q" 

743 
and prem2: "~P ==> Q" 

744 
shows "Q" 

745 
apply (rule excluded_middle [THEN disjE]) 

746 
apply (erule prem2) 

747 
apply (erule prem1) 

748 
done 

20944  749 
lemmas case_split = case_split_thm [case_names True False] 
15411  750 

751 
(*Classical implies (>) elimination. *) 

752 
lemma impCE: 

753 
assumes major: "P>Q" 

754 
and minor: "~P ==> R" "Q ==> R" 

755 
shows "R" 

756 
apply (rule excluded_middle [of P, THEN disjE]) 

17589  757 
apply (iprover intro: minor major [THEN mp])+ 
15411  758 
done 
759 

760 
(*This version of > elimination works on Q before P. It works best for 

761 
those cases in which P holds "almost everywhere". Can't install as 

762 
default: would break old proofs.*) 

763 
lemma impCE': 

764 
assumes major: "P>Q" 

765 
and minor: "Q ==> R" "~P ==> R" 

766 
shows "R" 

767 
apply (rule excluded_middle [of P, THEN disjE]) 

17589  768 
apply (iprover intro: minor major [THEN mp])+ 
15411  769 
done 
770 

771 
(*Classical <> elimination. *) 

772 
lemma iffCE: 

773 
assumes major: "P=Q" 

774 
and minor: "[ P; Q ] ==> R" "[ ~P; ~Q ] ==> R" 

775 
shows "R" 

776 
apply (rule major [THEN iffE]) 

17589  777 
apply (iprover intro: minor elim: impCE notE) 
15411  778 
done 
779 

780 
lemma exCI: 

781 
assumes "ALL x. ~P(x) ==> P(a)" 

782 
shows "EX x. P(x)" 

783 
apply (rule ccontr) 

23553  784 
apply (iprover intro: assms exI allI notI notE [of "\<exists>x. P x"]) 
15411  785 
done 
786 

787 

12386  788 
subsubsection {* Intuitionistic Reasoning *} 
789 

790 
lemma impE': 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

791 
assumes 1: "P > Q" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

792 
and 2: "Q ==> R" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

793 
and 3: "P > Q ==> P" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

794 
shows R 
12386  795 
proof  
796 
from 3 and 1 have P . 

797 
with 1 have Q by (rule impE) 

798 
with 2 show R . 

799 
qed 

800 

801 
lemma allE': 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

802 
assumes 1: "ALL x. P x" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

803 
and 2: "P x ==> ALL x. P x ==> Q" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

804 
shows Q 
12386  805 
proof  
806 
from 1 have "P x" by (rule spec) 

807 
from this and 1 show Q by (rule 2) 

808 
qed 

809 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

810 
lemma notE': 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

811 
assumes 1: "~ P" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

812 
and 2: "~ P ==> P" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

813 
shows R 
12386  814 
proof  
815 
from 2 and 1 have P . 

816 
with 1 show R by (rule notE) 

817 
qed 

818 

22444
fb80fedd192d
added safe intro rules for removing "True" subgoals as well as "~ False" ones.
dixon
parents:
22377
diff
changeset

819 
lemma TrueE: "True ==> P ==> P" . 
fb80fedd192d
added safe intro rules for removing "True" subgoals as well as "~ False" ones.
dixon
parents:
22377
diff
changeset

820 
lemma notFalseE: "~ False ==> P ==> P" . 
fb80fedd192d
added safe intro rules for removing "True" subgoals as well as "~ False" ones.
dixon
parents:
22377
diff
changeset

821 

22467
c9357ef01168
TrueElim and notTrueElim tested and added as safe elim rules.
dixon
parents:
22445
diff
changeset

822 
lemmas [Pure.elim!] = disjE iffE FalseE conjE exE TrueE notFalseE 
15801  823 
and [Pure.intro!] = iffI conjI impI TrueI notI allI refl 
824 
and [Pure.elim 2] = allE notE' impE' 

825 
and [Pure.intro] = exI disjI2 disjI1 

12386  826 

827 
lemmas [trans] = trans 

828 
and [sym] = sym not_sym 

15801  829 
and [Pure.elim?] = iffD1 iffD2 impE 
11750  830 

23553  831 
use "hologic.ML" 
832 

11438
3d9222b80989
declare trans [trans] (*overridden in theory Calculation*);
wenzelm
parents:
11432
diff
changeset

833 

11750  834 
subsubsection {* Atomizing metalevel connectives *} 
835 

836 
lemma atomize_all [atomize]: "(!!x. P x) == Trueprop (ALL x. P x)" 

12003  837 
proof 
9488  838 
assume "!!x. P x" 
23389  839 
then show "ALL x. P x" .. 
9488  840 
next 
841 
assume "ALL x. P x" 

23553  842 
then show "!!x. P x" by (rule allE) 
9488  843 
qed 
844 

11750  845 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
12003  846 
proof 
9488  847 
assume r: "A ==> B" 
10383  848 
show "A > B" by (rule impI) (rule r) 
9488  849 
next 
850 
assume "A > B" and A 

23553  851 
then show B by (rule mp) 
9488  852 
qed 
853 

14749  854 
lemma atomize_not: "(A ==> False) == Trueprop (~A)" 
855 
proof 

856 
assume r: "A ==> False" 

857 
show "~A" by (rule notI) (rule r) 

858 
next 

859 
assume "~A" and A 

23553  860 
then show False by (rule notE) 
14749  861 
qed 
862 

11750  863 
lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)" 
12003  864 
proof 
10432
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset

865 
assume "x == y" 
23553  866 
show "x = y" by (unfold `x == y`) (rule refl) 
10432
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset

867 
next 
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset

868 
assume "x = y" 
23553  869 
then show "x == y" by (rule eq_reflection) 
10432
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset

870 
qed 
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset

871 

12023  872 
lemma atomize_conj [atomize]: 
19121  873 
includes meta_conjunction_syntax 
874 
shows "(A && B) == Trueprop (A & B)" 

12003  875 
proof 
19121  876 
assume conj: "A && B" 
877 
show "A & B" 

878 
proof (rule conjI) 

879 
from conj show A by (rule conjunctionD1) 

880 
from conj show B by (rule conjunctionD2) 

881 
qed 

11953  882 
next 
19121  883 
assume conj: "A & B" 
884 
show "A && B" 

885 
proof  

886 
from conj show A .. 

887 
from conj show B .. 

11953  888 
qed 
889 
qed 

890 

12386  891 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
18832  892 
and [symmetric, defn] = atomize_all atomize_imp atomize_eq 
12386  893 

11750  894 

20944  895 
subsection {* Package setup *} 
896 

11750  897 
subsubsection {* Classical Reasoner setup *} 
9529  898 

20944  899 
lemma thin_refl: 
900 
"\<And>X. \<lbrakk> x=x; PROP W \<rbrakk> \<Longrightarrow> PROP W" . 

901 

21151  902 
ML {* 
903 
structure Hypsubst = HypsubstFun( 

904 
struct 

905 
structure Simplifier = Simplifier 

21218  906 
val dest_eq = HOLogic.dest_eq 
21151  907 
val dest_Trueprop = HOLogic.dest_Trueprop 
908 
val dest_imp = HOLogic.dest_imp 

22129  909 
val eq_reflection = @{thm HOL.eq_reflection} 
22218  910 
val rev_eq_reflection = @{thm HOL.meta_eq_to_obj_eq} 
22129  911 
val imp_intr = @{thm HOL.impI} 
912 
val rev_mp = @{thm HOL.rev_mp} 

913 
val subst = @{thm HOL.subst} 

914 
val sym = @{thm HOL.sym} 

915 
val thin_refl = @{thm thin_refl}; 

21151  916 
end); 
21671  917 
open Hypsubst; 
21151  918 

919 
structure Classical = ClassicalFun( 

920 
struct 

22129  921 
val mp = @{thm HOL.mp} 
922 
val not_elim = @{thm HOL.notE} 

923 
val classical = @{thm HOL.classical} 

21151  924 
val sizef = Drule.size_of_thm 
925 
val hyp_subst_tacs = [Hypsubst.hyp_subst_tac] 

926 
end); 

927 

928 
structure BasicClassical: BASIC_CLASSICAL = Classical; 

21671  929 
open BasicClassical; 
22129  930 

931 
ML_Context.value_antiq "claset" 

932 
(Scan.succeed ("claset", "Classical.local_claset_of (ML_Context.the_local_context ())")); 

21151  933 
*} 
934 

21009  935 
setup {* 
936 
let 

937 
(*prevent substitution on bool*) 

938 
fun hyp_subst_tac' i thm = if i <= Thm.nprems_of thm andalso 

939 
Term.exists_Const (fn ("op =", Type (_, [T, _])) => T <> Type ("bool", [])  _ => false) 

940 
(nth (Thm.prems_of thm) (i  1)) then Hypsubst.hyp_subst_tac i thm else no_tac thm; 

941 
in 

21151  942 
Hypsubst.hypsubst_setup 
943 
#> ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac) 

944 
#> Classical.setup 

945 
#> ResAtpset.setup 

21009  946 
end 
947 
*} 

948 

949 
declare iffI [intro!] 

950 
and notI [intro!] 

951 
and impI [intro!] 

952 
and disjCI [intro!] 

953 
and conjI [intro!] 

954 
and TrueI [intro!] 

955 
and refl [intro!] 

956 

957 
declare iffCE [elim!] 

958 
and FalseE [elim!] 

959 
and impCE [elim!] 

960 
and disjE [elim!] 

961 
and conjE [elim!] 

962 
and conjE [elim!] 

963 

964 
declare ex_ex1I [intro!] 

965 
and allI [intro!] 

966 
and the_equality [intro] 

967 
and exI [intro] 

968 

969 
declare exE [elim!] 

970 
allE [elim] 

971 

22377  972 
ML {* val HOL_cs = @{claset} *} 
19162  973 

20223  974 
lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P" 
975 
apply (erule swap) 

976 
apply (erule (1) meta_mp) 

977 
done 

10383  978 

18689
a50587cd8414
prefer ex1I over ex_ex1I in singlestep reasoning;
wenzelm
parents:
18595
diff
changeset

979 
declare ex_ex1I [rule del, intro! 2] 
a50587cd8414
prefer ex1I over ex_ex1I in singlestep reasoning;
wenzelm
parents:
18595
diff
changeset

980 
and ex1I [intro] 
a50587cd8414
prefer ex1I over ex_ex1I in singlestep reasoning;
wenzelm
parents:
18595
diff
changeset

981 

12386  982 
lemmas [intro?] = ext 
983 
and [elim?] = ex1_implies_ex 

11977  984 

20944  985 
(*Better then ex1E for classical reasoner: needs no quantifier duplication!*) 
20973  986 
lemma alt_ex1E [elim!]: 
20944  987 
assumes major: "\<exists>!x. P x" 
988 
and prem: "\<And>x. \<lbrakk> P x; \<forall>y y'. P y \<and> P y' \<longrightarrow> y = y' \<rbrakk> \<Longrightarrow> R" 

989 
shows R 

990 
apply (rule ex1E [OF major]) 

991 
apply (rule prem) 

22129  992 
apply (tactic {* ares_tac @{thms allI} 1 *})+ 
993 
apply (tactic {* etac (Classical.dup_elim @{thm allE}) 1 *}) 

994 
apply iprover 

995 
done 

20944  996 

21151  997 
ML {* 
998 
structure Blast = BlastFun( 

999 
struct 

1000 
type claset = Classical.claset 

22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22481
diff
changeset

1001 
val equality_name = @{const_name "op ="} 
22993  1002 
val not_name = @{const_name Not} 
22129  1003 
val notE = @{thm HOL.notE} 
1004 
val ccontr = @{thm HOL.ccontr} 

21151  1005 
val contr_tac = Classical.contr_tac 
1006 
val dup_intr = Classical.dup_intr 

1007 
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac 

21671  1008 
val claset = Classical.claset 
21151  1009 
val rep_cs = Classical.rep_cs 
1010 
val cla_modifiers = Classical.cla_modifiers 

1011 
val cla_meth' = Classical.cla_meth' 

1012 
end); 

21671  1013 
val Blast_tac = Blast.Blast_tac; 
1014 
val blast_tac = Blast.blast_tac; 

20944  1015 
*} 
1016 

21151  1017 
setup Blast.setup 
1018 

20944  1019 

1020 
subsubsection {* Simplifier *} 

12281  1021 

1022 
lemma eta_contract_eq: "(%s. f s) = f" .. 

1023 

1024 
lemma simp_thms: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

1025 
shows not_not: "(~ ~ P) = P" 
15354  1026 
and Not_eq_iff: "((~P) = (~Q)) = (P = Q)" 
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

1027 
and 
12436
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

1028 
"(P ~= Q) = (P = (~Q))" 
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

1029 
"(P  ~P) = True" "(~P  P) = True" 
12281  1030 
"(x = x) = True" 
20944  1031 
and not_True_eq_False: "(\<not> True) = False" 
1032 
and not_False_eq_True: "(\<not> False) = True" 

1033 
and 

12436
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

1034 
"(~P) ~= P" "P ~= (~P)" 
20944  1035 
"(True=P) = P" 
1036 
and eq_True: "(P = True) = P" 

1037 
and "(False=P) = (~P)" 

1038 
and eq_False: "(P = False) = (\<not> P)" 

1039 
and 

12281  1040 
"(True > P) = P" "(False > P) = True" 
1041 
"(P > True) = True" "(P > P) = True" 

1042 
"(P > False) = (~P)" "(P > ~P) = (~P)" 

1043 
"(P & True) = P" "(True & P) = P" 

1044 
"(P & False) = False" "(False & P) = False" 

1045 
"(P & P) = P" "(P & (P & Q)) = (P & Q)" 

1046 
"(P & ~P) = False" "(~P & P) = False" 

1047 
"(P  True) = True" "(True  P) = True" 

1048 
"(P  False) = P" "(False  P) = P" 

12436
a2df07fefed7
Replaced several occurrences of "blast" by "rules".
berghofe
parents:
12386
diff
changeset

1049 
"(P  P) = P" "(P  (P  Q)) = (P  Q)" and 
12281  1050 
"(ALL x. P) = P" "(EX x. P) = P" "EX x. x=t" "EX x. t=x" 
1051 
 {* needed for the onepointrule quantifier simplification procs *} 

1052 
 {* essential for termination!! *} and 

1053 
"!!P. (EX x. x=t & P(x)) = P(t)" 

1054 
"!!P. (EX x. t=x & P(x)) = P(t)" 

1055 
"!!P. (ALL x. x=t > P(x)) = P(t)" 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

1056 
"!!P. (ALL x. t=x > P(x)) = P(t)" 
17589  1057 
by (blast, blast, blast, blast, blast, iprover+) 
13421  1058 

14201  1059 
lemma disj_absorb: "(A  A) = A" 
1060 
by blast 

1061 

1062 
lemma disj_left_absorb: "(A  (A  B)) = (A  B)" 

1063 
by blast 

1064 

1065 
lemma conj_absorb: "(A & A) = A" 

1066 
by blast 

1067 

1068 
lemma conj_left_absorb: "(A & (A & B)) = (A & B)" 

1069 
by blast 

1070 

12281  1071 
lemma eq_ac: 
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

1072 
shows eq_commute: "(a=b) = (b=a)" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

1073 
and eq_left_commute: "(P=(Q=R)) = (Q=(P=R))" 
17589  1074 
and eq_assoc: "((P=Q)=R) = (P=(Q=R))" by (iprover, blast+) 
1075 
lemma neq_commute: "(a~=b) = (b~=a)" by iprover 

12281  1076 

1077 
lemma conj_comms: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

1078 
shows conj_commute: "(P&Q) = (Q&P)" 
17589  1079 
and conj_left_commute: "(P&(Q&R)) = (Q&(P&R))" by iprover+ 
1080 
lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by iprover 

12281  1081 

19174  1082 
lemmas conj_ac = conj_commute conj_left_commute conj_assoc 
1083 

12281  1084 
lemma disj_comms: 
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12892
diff
changeset

1085 
shows disj_commute: "(PQ) = (QP)" 
17589  1086 
and disj_left_commute: "(P(QR)) = (Q(PR))" by iprover+ 
1087 
lemma disj_assoc: "((PQ)R) = (P(QR))" by iprover 

12281  1088 

19174  1089 
lemmas disj_ac = disj_commute disj_left_commute disj_assoc 
1090 

17589  1091 
lemma conj_disj_distribL: "(P&(QR)) = (P&Q  P&R)" by iprover 
1092 
lemma conj_disj_distribR: "((PQ)&R) = (P&R  Q&R)" by iprover 

12281  1093 

17589  1094 
lemma disj_conj_distribL: "(P(Q&R)) = ((PQ) & (PR))" by iprover 
1095 
lemma disj_conj_distribR: "((P&Q)R) = ((PR) & (QR))" by iprover 

12281  1096 

17589  1097 
lemma imp_conjR: "(P > (Q&R)) = ((P>Q) & (P>R))" by iprover 
1098 
lemma imp_conjL: "((P&Q) >R) = (P > (Q > R))" by iprover 

1099 
lemma imp_disjL: "((PQ) > R) = ((P>R)&(Q>R))" by iprover 

12281  1100 

1101 
text {* These two are specialized, but @{text imp_disj_not1} is useful in @{text "Auth/Yahalom"}. *} 

1102 
lemma imp_disj_not1: "(P > Q  R) = (~Q > P > R)" by blast 

1103 
lemma imp_disj_not2: "(P > Q  R) = (~R > P > Q)" by blast 

1104 

1105 
lemma imp_disj1: "((P>Q)R) = (P> QR)" by blast 

1106 
lemma imp_disj2: "(Q(P>R)) = (P> QR)" by blast 

1107 

21151  1108 
lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P > Q) = (P' > Q'))" 
1109 
by iprover 

1110 

17589  1111 
lemma de_Morgan_disj: "(~(P  Q)) = (~P & ~Q)" by iprover 
12281  1112 
lemma de_Morgan_conj: "(~(P & Q)) = (~P  ~Q)" by blast 
1113 
lemma not_imp: "(~(P > Q)) = (P & ~Q)" by blast 

1114 
lemma not_iff: "(P~=Q) = (P = (~Q))" by blast 

1115 
lemma disj_not1: "(~P  Q) = (P > Q)" by blast 

1116 
lemma disj_not2: "(P  ~Q) = (Q > P)"  {* changes orientation :( *} 

1117 
by blast 

1118 
lemma imp_conv_disj: "(P > Q) = ((~P)  Q)" by blast 

1119 

17589  1120 
lemma iff_conv_conj_imp: "(P = Q) = ((P > Q) & (Q > P))" by iprover 
12281  1121 

1122 

1123 
lemma cases_simp: "((P > Q) & (~P > Q)) = Q" 

1124 
 {* Avoids duplication of subgoals after @{text split_if}, when the true and false *} 

1125 
 {* cases boil down to the same thing. *} 

1126 
by blast 

1127 

1128 
lemma not_all: "(~ (! x. P(x))) = (? x.~P(x))" by blast 

1129 
lemma imp_all: "((! x. P x) > Q) = (? x. P x > Q)" by blast 

17589  1130 
lemma not_ex: "(~ (? x. P(x))) = (! x.~P(x))" by iprover 
1131 
lemma imp_ex: "((? x. P x) > Q) = (! x. P x > Q)" by iprover 

23403  1132 
lemma all_not_ex: "(ALL x. P x) = (~ (EX x. ~ P x ))" by blast 
12281  1133 

17589  1134 
lemma ex_disj_distrib: "(? x. P(x)  Q(x)) = ((? x. P(x))  (? x. Q(x)))" by iprover 
1135 
lemma all_conj_distrib: "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))" by iprover 

12281  1136 

1137 
text {* 

1138 
\medskip The @{text "&"} congruence rule: not included by default! 

1139 
May slow rewrite proofs down by as much as 50\% *} 

1140 

1141 
lemma conj_cong: 

1142 
"(P = P') ==> (P' ==> (Q = Q')) ==> ((P & Q) = (P' & Q'))" 

17589  1143 
by iprover 
12281  1144 

1145 
lemma rev_conj_cong: 

1146 
"(Q = Q') ==> (Q' ==> (P = P')) ==> ((P & Q) = (P' & Q'))" 

17589  1147 
by iprover 
12281  1148 

1149 
text {* The @{text ""} congruence rule: not included by default! *} 

1150 

1151 
lemma disj_cong: 

1152 
"(P = P') ==> (~P' ==> (Q = Q')) ==> ((P  Q) = (P'  Q'))" 

1153 
by blast 

1154 

1155 

1156 
text {* \medskip ifthenelse rules *} 

1157 

1158 
lemma if_True: "(if True then x else y) = x" 

1159 
by (unfold if_def) blast 

1160 

1161 
lemma if_False: "(if False then x else y) = y" 

1162 
by (unfold if_def) blast 

1163 

1164 
lemma if_P: "P ==> (if P then x else y) = x" 

1165 
by (unfold if_def) blast 

1166 

1167 
lemma if_not_P: "~P ==> (if P then x else y) = y" 

1168 
by (unfold if_def) blast 

1169 

1170 
lemma split_if: "P (if Q then x else y) = ((Q > P(x)) & (~Q > P(y)))" 

1171 
apply (rule case_split [of Q]) 

15481  1172 
apply (simplesubst if_P) 
1173 
prefer 3 apply (simplesubst if_not_P, blast+) 

12281  1174 
done 
1175 

1176 
lemma split_if_asm: "P (if Q then x else y) = (~((Q & ~P x)  (~Q & ~P y)))" 

15481  1177 
by (simplesubst split_if, blast) 
12281  1178 

1179 
lemmas if_splits = split_if split_if_asm 

1180 

1181 
lemma if_cancel: "(if c then x else x) = x" 

15481  1182 
by (simplesubst split_if, blast) 
12281  1183 

1184 
lemma if_eq_cancel: "(if x = y then y else x) = x" 

15481  1185 
by (simplesubst split_if, blast) 
12281  1186 

1187 
lemma if_bool_eq_conj: "(if P then Q else R) = ((P>Q) & (~P>R))" 

19796  1188 
 {* This form is useful for expanding @{text "if"}s on the RIGHT of the @{text "==>"} symbol. *} 
12281  1189 
by (rule split_if) 
1190 

1191 
lemma if_bool_eq_disj: "(if P then Q else R) = ((P&Q)  (~P&R))" 

19796  1192 
 {* And this form is useful for expanding @{text "if"}s on the LEFT. *} 
15481  1193 
apply (simplesubst split_if, blast) 
12281  1194 
done 
1195 

17589  1196 
lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) iprover 
1197 
lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) iprover 

12281  1198 

15423  1199 
text {* \medskip let rules for simproc *} 
1200 

1201 
lemma Let_folded: "f x \<equiv> g x \<Longrightarrow> Let x f \<equiv> Let x g" 

1202 
by (unfold Let_def) 

1203 

1204 
lemma Let_unfold: "f x \<equiv> g \<Longrightarrow> Let x f \<equiv> g" 

1205 
by (unfold Let_def) 

1206 

16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1207 
text {* 
16999  1208 
The following copy of the implication operator is useful for 
1209 
finetuning congruence rules. It instructs the simplifier to simplify 

1210 
its premise. 

16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1211 
*} 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1212 

17197  1213 
constdefs 
1214 
simp_implies :: "[prop, prop] => prop" (infixr "=simp=>" 1) 

1215 
"simp_implies \<equiv> op ==>" 

16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1216 

18457  1217 
lemma simp_impliesI: 
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1218 
assumes PQ: "(PROP P \<Longrightarrow> PROP Q)" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1219 
shows "PROP P =simp=> PROP Q" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1220 
apply (unfold simp_implies_def) 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1221 
apply (rule PQ) 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1222 
apply assumption 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1223 
done 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1224 

208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1225 
lemma simp_impliesE: 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1226 
assumes PQ:"PROP P =simp=> PROP Q" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1227 
and P: "PROP P" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1228 
and QR: "PROP Q \<Longrightarrow> PROP R" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1229 
shows "PROP R" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1230 
apply (rule QR) 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1231 
apply (rule PQ [unfolded simp_implies_def]) 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1232 
apply (rule P) 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1233 
done 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1234 

208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1235 
lemma simp_implies_cong: 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1236 
assumes PP' :"PROP P == PROP P'" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1237 
and P'QQ': "PROP P' ==> (PROP Q == PROP Q')" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1238 
shows "(PROP P =simp=> PROP Q) == (PROP P' =simp=> PROP Q')" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1239 
proof (unfold simp_implies_def, rule equal_intr_rule) 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1240 
assume PQ: "PROP P \<Longrightarrow> PROP Q" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1241 
and P': "PROP P'" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1242 
from PP' [symmetric] and P' have "PROP P" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1243 
by (rule equal_elim_rule1) 
23553  1244 
then have "PROP Q" by (rule PQ) 
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1245 
with P'QQ' [OF P'] show "PROP Q'" by (rule equal_elim_rule1) 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1246 
next 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1247 
assume P'Q': "PROP P' \<Longrightarrow> PROP Q'" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1248 
and P: "PROP P" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1249 
from PP' and P have P': "PROP P'" by (rule equal_elim_rule1) 
23553  1250 
then have "PROP Q'" by (rule P'Q') 
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1251 
with P'QQ' [OF P', symmetric] show "PROP Q" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1252 
by (rule equal_elim_rule1) 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1253 
qed 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1254 

20944  1255 
lemma uncurry: 
1256 
assumes "P \<longrightarrow> Q \<longrightarrow> R" 

1257 
shows "P \<and> Q \<longrightarrow> R" 

23553  1258 
using assms by blast 
20944  1259 

1260 
lemma iff_allI: 

1261 
assumes "\<And>x. P x = Q x" 

1262 
shows "(\<forall>x. P x) = (\<forall>x. Q x)" 

23553  1263 
using assms by blast 
20944  1264 

1265 
lemma iff_exI: 

1266 
assumes "\<And>x. P x = Q x" 

1267 
shows "(\<exists>x. P x) = (\<exists>x. Q x)" 

23553  1268 
using assms by blast 
20944  1269 

1270 
lemma all_comm: 

1271 
"(\<forall>x y. P x y) = (\<forall>y x. P x y)" 

1272 
by blast 

1273 

1274 
lemma ex_comm: 

1275 
"(\<exists>x y. P x y) = (\<exists>y x. P x y)" 

1276 
by blast 

1277 

9869  1278 
use "simpdata.ML" 
21671  1279 
ML {* open Simpdata *} 
1280 

21151  1281 
setup {* 
1282 
Simplifier.method_setup Splitter.split_modifiers 

21547
9c9fdf4c2949
moved order arities for fun and bool to Fun/Orderings
haftmann
parents:
21524
diff
changeset

1283 
#> (fn thy => (change_simpset_of thy (fn _ => Simpdata.simpset_simprocs); thy)) 
21151  1284 
#> Splitter.setup 
1285 
#> Clasimp.setup 

1286 
#> EqSubst.setup 

1287 
*} 

1288 

1289 
lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P" 

1290 
proof 

23389  1291 
assume "True \<Longrightarrow> PROP P" 
1292 
from this [OF TrueI] show "PROP P" . 

21151  1293 
next 
1294 
assume "PROP P" 

23389  1295 
then show "PROP P" . 
21151  1296 
qed 
1297 

1298 
lemma ex_simps: 

1299 
"!!P Q. (EX x. P x & Q) = ((EX x. P x) & Q)" 

1300 
"!!P Q. (EX x. P & Q x) = (P & (EX x. Q x))" 

1301 
"!!P Q. (EX x. P x  Q) = ((EX x. P x)  Q)" 

1302 
"!!P Q. (EX x. P  Q x) = (P  (EX x. Q x))" 

1303 
"!!P Q. (EX x. P x > Q) = ((ALL x. P x) > Q)" 

1304 
"!!P Q. (EX x. P > Q x) = (P > (EX x. Q x))" 

1305 
 {* Miniscoping: pushing in existential quantifiers. *} 

1306 
by (iprover  blast)+ 

1307 

1308 
lemma all_simps: 

1309 
"!!P Q. (ALL x. P x & Q) = ((ALL x. P x) & Q)" 

1310 
"!!P Q. (ALL x. P & Q x) = (P & (ALL x. Q x))" 

1311 
"!!P Q. (ALL x. P x  Q) = ((ALL x. P x)  Q)" 

1312 
"!!P Q. (ALL x. P  Q x) = (P  (ALL x. Q x))" 

1313 
"!!P Q. (ALL x. P x > Q) = ((EX x. P x) > Q)" 

1314 
"!!P Q. (ALL x. P > Q x) = (P > (ALL x. Q x))" 

1315 
 {* Miniscoping: pushing in universal quantifiers. *} 

1316 
by (iprover  blast)+ 

15481  1317 

21671  1318 
lemmas [simp] = 
1319 
triv_forall_equality (*prunes params*) 

1320 
True_implies_equals (*prune asms `True'*) 

1321 
if_True 

1322 
if_False 

1323 
if_cancel 

1324 
if_eq_cancel 

1325 
imp_disjL 

20973  1326 
(*In general it seems wrong to add distributive laws by default: they 
1327 
might cause exponential blowup. But imp_disjL has been in for a while 

1328 
and cannot be removed without affecting existing proofs. Moreover, 

1329 
rewriting by "(PQ > R) = ((P>R)&(Q>R))" might be justified on the 

1330 
grounds that it allows simplification of R in the two cases.*) 

21671  1331 
conj_assoc 
1332 
disj_assoc 

1333 
de_Morgan_conj 

1334 
de_Morgan_disj 

1335 
imp_disj1 

1336 
imp_disj2 

1337 
not_imp 

1338 
disj_not1 

1339 
not_all 

1340 
not_ex 

1341 
cases_simp 

1342 
the_eq_trivial 

1343 
the_sym_eq_trivial 

1344 
ex_simps 

1345 
all_simps 

1346 
simp_thms 

1347 

1348 
lemmas [cong] = imp_cong simp_implies_cong 

1349 
lemmas [split] = split_if 

20973  1350 

22377  1351 
ML {* val HOL_ss = @{simpset} *} 
20973  1352 

20944  1353 
text {* Simplifies x assuming c and y assuming ~c *} 
1354 
lemma if_cong: 

1355 
assumes "b = c" 

1356 
and "c \<Longrightarrow> x = u" 

1357 
and "\<not> c \<Longrightarrow> y = v" 

1358 
shows "(if b then x else y) = (if c then u else v)" 

23553  1359 
unfolding if_def using assms by simp 
20944  1360 

1361 
text {* Prevents simplification of x and y: 

1362 
faster and allows the execution of functional programs. *} 

1363 
lemma if_weak_cong [cong]: 

1364 
assumes "b = c" 

1365 
shows "(if b then x else y) = (if c then x else y)" 

23553  1366 
using assms by (rule arg_cong) 
20944  1367 

1368 
text {* Prevents simplification of t: much faster *} 

1369 
lemma let_weak_cong: 
