author  wenzelm 
Thu, 22 Dec 2005 00:28:36 +0100  
changeset 18457  356a9f711899 
parent 17992  4379d46c8e13 
child 18511  beed2bc052a3 
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 
16417  10 
uses ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("eqrule_HOL_data.ML") 
15481  11 
("~~/src/Provers/eqsubst.ML") 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16633
diff
changeset

12 

15131  13 
begin 
2260  14 

11750  15 
subsection {* Primitive logic *} 
16 

17 
subsubsection {* Core syntax *} 

2260  18 

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

20 
defaultsort type 
3947  21 

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

22 
global 
923  23 

7357  24 
typedecl bool 
923  25 

26 
arities 

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

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

28 
fun :: (type, type) type 
923  29 

11750  30 
judgment 
31 
Trueprop :: "bool => prop" ("(_)" 5) 

923  32 

11750  33 
consts 
7357  34 
Not :: "bool => bool" ("~ _" [40] 40) 
35 
True :: bool 

36 
False :: bool 

3947  37 
arbitrary :: 'a 
923  38 

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

39 
The :: "('a => bool) => 'a" 
7357  40 
All :: "('a => bool) => bool" (binder "ALL " 10) 
41 
Ex :: "('a => bool) => bool" (binder "EX " 10) 

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

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

923  44 

7357  45 
"=" :: "['a, 'a] => bool" (infixl 50) 
46 
& :: "[bool, bool] => bool" (infixr 35) 

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

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

923  49 

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

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

51 

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

2260  54 

11750  55 
subsubsection {* Additional concrete syntax *} 
2260  56 

4868  57 
nonterminals 
923  58 
letbinds letbind 
59 
case_syn cases_syn 

60 

61 
syntax 

12650  62 
"_not_equal" :: "['a, 'a] => bool" (infixl "~=" 50) 
11432
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
10489
diff
changeset

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

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

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

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

923  69 

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

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

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

73 
"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/  _") 
923  74 

75 
translations 

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

76 
"x ~= y" == "~ (x = y)" 
13764  77 
"THE x. P" == "The (%x. P)" 
923  78 
"_Let (_binds b bs) e" == "_Let b (_Let bs e)" 
1114  79 
"let x = a in e" == "Let a (%x. e)" 
923  80 

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

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

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

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

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

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

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

87 

12633  88 
syntax (output) 
11687  89 
"=" :: "['a, 'a] => bool" (infix 50) 
12650  90 
"_not_equal" :: "['a, 'a] => bool" (infix "~=" 50) 
2260  91 

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

92 
syntax (xsymbols) 
11687  93 
Not :: "bool => bool" ("\<not> _" [40] 40) 
94 
"op &" :: "[bool, bool] => bool" (infixr "\<and>" 35) 

95 
"op " :: "[bool, bool] => bool" (infixr "\<or>" 30) 

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

96 
"op >" :: "[bool, bool] => bool" (infixr "\<longrightarrow>" 25) 
12650  97 
"_not_equal" :: "['a, 'a] => bool" (infix "\<noteq>" 50) 
11687  98 
"ALL " :: "[idts, bool] => bool" ("(3\<forall>_./ _)" [0, 10] 10) 
99 
"EX " :: "[idts, bool] => bool" ("(3\<exists>_./ _)" [0, 10] 10) 

100 
"EX! " :: "[idts, bool] => bool" ("(3\<exists>!_./ _)" [0, 10] 10) 

101 
"_case1" :: "['a, 'b] => case_syn" ("(2_ \<Rightarrow>/ _)" 10) 

14361
ad2f5da643b4
* Support for raw latex output in control symbols: \<^raw...>
schirmer
parents:
14357
diff
changeset

102 
(*"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ \<orelse> _")*) 
2372  103 

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

104 
syntax (xsymbols output) 
12650  105 
"_not_equal" :: "['a, 'a] => bool" (infix "\<noteq>" 50) 
3820  106 

6340  107 
syntax (HTML output) 
14565  108 
"_not_equal" :: "['a, 'a] => bool" (infix "\<noteq>" 50) 
11687  109 
Not :: "bool => bool" ("\<not> _" [40] 40) 
14565  110 
"op &" :: "[bool, bool] => bool" (infixr "\<and>" 35) 
111 
"op " :: "[bool, bool] => bool" (infixr "\<or>" 30) 

112 
"_not_equal" :: "['a, 'a] => bool" (infix "\<noteq>" 50) 

113 
"ALL " :: "[idts, bool] => bool" ("(3\<forall>_./ _)" [0, 10] 10) 

114 
"EX " :: "[idts, bool] => bool" ("(3\<exists>_./ _)" [0, 10] 10) 

115 
"EX! " :: "[idts, bool] => bool" ("(3\<exists>!_./ _)" [0, 10] 10) 

6340  116 

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

117 
syntax (HOL) 
7357  118 
"ALL " :: "[idts, bool] => bool" ("(3! _./ _)" [0, 10] 10) 
119 
"EX " :: "[idts, bool] => bool" ("(3? _./ _)" [0, 10] 10) 

120 
"EX! " :: "[idts, bool] => bool" ("(3?! _./ _)" [0, 10] 10) 

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

121 

17992
4379d46c8e13
alternative iff syntax for equality on booleans, with print_mode 'iff';
wenzelm
parents:
17639
diff
changeset

122 
syntax 
4379d46c8e13
alternative iff syntax for equality on booleans, with print_mode 'iff';
wenzelm
parents:
17639
diff
changeset

123 
"_iff" :: "bool => bool => bool" (infixr "<>" 25) 
4379d46c8e13
alternative iff syntax for equality on booleans, with print_mode 'iff';
wenzelm
parents:
17639
diff
changeset

124 
syntax (xsymbols) 
4379d46c8e13
alternative iff syntax for equality on booleans, with print_mode 'iff';
wenzelm
parents:
17639
diff
changeset

125 
"_iff" :: "bool => bool => bool" (infixr "\<longleftrightarrow>" 25) 
4379d46c8e13
alternative iff syntax for equality on booleans, with print_mode 'iff';
wenzelm
parents:
17639
diff
changeset

126 
translations 
4379d46c8e13
alternative iff syntax for equality on booleans, with print_mode 'iff';
wenzelm
parents:
17639
diff
changeset

127 
"op <>" => "op = :: bool => bool => bool" 
4379d46c8e13
alternative iff syntax for equality on booleans, with print_mode 'iff';
wenzelm
parents:
17639
diff
changeset

128 

4379d46c8e13
alternative iff syntax for equality on booleans, with print_mode 'iff';
wenzelm
parents:
17639
diff
changeset

129 
typed_print_translation {* 
4379d46c8e13
alternative iff syntax for equality on booleans, with print_mode 'iff';
wenzelm
parents:
17639
diff
changeset

130 
let 
4379d46c8e13
alternative iff syntax for equality on booleans, with print_mode 'iff';
wenzelm
parents:
17639
diff
changeset

131 
fun iff_tr' _ (Type ("fun", (Type ("bool", _) :: _))) ts = 
4379d46c8e13
alternative iff syntax for equality on booleans, with print_mode 'iff';
wenzelm
parents:
17639
diff
changeset

132 
if Output.has_mode "iff" then Term.list_comb (Syntax.const "_iff", ts) 
4379d46c8e13
alternative iff syntax for equality on booleans, with print_mode 'iff';
wenzelm
parents:
17639
diff
changeset

133 
else raise Match 
4379d46c8e13
alternative iff syntax for equality on booleans, with print_mode 'iff';
wenzelm
parents:
17639
diff
changeset

134 
 iff_tr' _ _ _ = raise Match; 
4379d46c8e13
alternative iff syntax for equality on booleans, with print_mode 'iff';
wenzelm
parents:
17639
diff
changeset

135 
in [("op =", iff_tr')] end 
4379d46c8e13
alternative iff syntax for equality on booleans, with print_mode 'iff';
wenzelm
parents:
17639
diff
changeset

136 
*} 
4379d46c8e13
alternative iff syntax for equality on booleans, with print_mode 'iff';
wenzelm
parents:
17639
diff
changeset

137 

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

138 

11750  139 
subsubsection {* Axioms and basic definitions *} 
2260  140 

7357  141 
axioms 
15380  142 
eq_reflection: "(x=y) ==> (x==y)" 
923  143 

15380  144 
refl: "t = (t::'a)" 
6289  145 

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

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

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

6289  150 

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

151 
the_eq_trivial: "(THE x. x = a) = (a::'a)" 
923  152 

15380  153 
impI: "(P ==> Q) ==> P>Q" 
154 
mp: "[ P>Q; P ] ==> Q" 

155 

156 

157 
text{*Thanks to Stephan Merz*} 

158 
theorem subst: 

159 
assumes eq: "s = t" and p: "P(s)" 

160 
shows "P(t::'a)" 

161 
proof  

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

163 
by (rule eq_reflection) 

164 
from p show ?thesis 

165 
by (unfold meta) 

166 
qed 

923  167 

168 
defs 

7357  169 
True_def: "True == ((%x::bool. x) = (%x. x))" 
170 
All_def: "All(P) == (P = (%x. True))" 

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

171 
Ex_def: "Ex(P) == !Q. (!x. P x > Q) > Q" 
7357  172 
False_def: "False == (!P. P)" 
173 
not_def: "~ P == P>False" 

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

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

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

923  177 

7357  178 
axioms 
179 
iff: "(P>Q) > (Q>P) > (P=Q)" 

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

923  181 

182 
defs 

7357  183 
Let_def: "Let s f == f(s)" 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11438
diff
changeset

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

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

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

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

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

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

190 
arbitrary 
3320  191 

11750  192 
subsubsection {* Generic algebraic operations *} 
4868  193 

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

194 
axclass zero < type 
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12281
diff
changeset

195 
axclass one < type 
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12281
diff
changeset

196 
axclass plus < type 
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12281
diff
changeset

197 
axclass minus < type 
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12281
diff
changeset

198 
axclass times < type 
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12281
diff
changeset

199 
axclass inverse < type 
11750  200 

201 
global 

202 

203 
consts 

204 
"0" :: "'a::zero" ("0") 

205 
"1" :: "'a::one" ("1") 

206 
"+" :: "['a::plus, 'a] => 'a" (infixl 65) 

207 
 :: "['a::minus, 'a] => 'a" (infixl 65) 

208 
uminus :: "['a::minus] => 'a" (" _" [81] 80) 

209 
* :: "['a::times, 'a] => 'a" (infixl 70) 

210 

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

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

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

213 
translations 
14690  214 
(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

215 

11750  216 
local 
217 

218 
typed_print_translation {* 

219 
let 

220 
fun tr' c = (c, fn show_sorts => fn T => fn ts => 

221 
if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match 

222 
else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T); 

223 
in [tr' "0", tr' "1"] end; 

224 
*}  {* show types that are presumably too general *} 

225 

226 

227 
consts 

228 
abs :: "'a::minus => 'a" 

229 
inverse :: "'a::inverse => 'a" 

230 
divide :: "['a::inverse, 'a] => 'a" (infixl "'/" 70) 

231 

232 
syntax (xsymbols) 

233 
abs :: "'a::minus => 'a" ("\<bar>_\<bar>") 

234 
syntax (HTML output) 

235 
abs :: "'a::minus => 'a" ("\<bar>_\<bar>") 

236 

237 

15411  238 
subsection {*Equality*} 
239 

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

15411  242 

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

15411  245 

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

18457  247 
by (erule subst) 
15411  248 

18457  249 
lemma def_imp_eq: assumes meq: "A == B" shows "A = B" 
250 
by (unfold meq) (rule refl) 

251 

15411  252 

253 
(*Useful with eresolve_tac for proving equalties from known equalities. 

254 
a = b 

255 
  

256 
c = d *) 

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

258 
apply (rule trans) 

259 
apply (rule trans) 

260 
apply (rule sym) 

261 
apply assumption+ 

262 
done 

263 

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

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

265 

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

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

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

268 

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

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

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

271 

15411  272 

273 
subsection {*Congruence rules for application*} 

274 

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

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

277 
apply (erule subst) 

278 
apply (rule refl) 

279 
done 

280 

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

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

283 
apply (erule subst) 

284 
apply (rule refl) 

285 
done 

286 

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

289 
apply (rule refl) 

290 
done 

291 

292 

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

295 
apply (rule refl) 

296 
done 

297 

298 

299 
subsection {*Equality of booleans  iff*} 

300 

301 
lemma iffI: assumes prems: "P ==> Q" "Q ==> P" shows "P=Q" 

18457  302 
by (iprover intro: iff [THEN mp, THEN mp] impI prems) 
15411  303 

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

18457  305 
by (erule ssubst) 
15411  306 

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

18457  308 
by (erule iffD2) 
15411  309 

310 
lemmas iffD1 = sym [THEN iffD2, standard] 

311 
lemmas rev_iffD1 = sym [THEN [2] rev_iffD2, standard] 

312 

313 
lemma iffE: 

314 
assumes major: "P=Q" 

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

18457  316 
shows R 
317 
by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1]) 

15411  318 

319 

320 
subsection {*True*} 

321 

322 
lemma TrueI: "True" 

18457  323 
by (unfold True_def) (rule refl) 
15411  324 

325 
lemma eqTrueI: "P ==> P=True" 

18457  326 
by (iprover intro: iffI TrueI) 
15411  327 

328 
lemma eqTrueE: "P=True ==> P" 

329 
apply (erule iffD2) 

330 
apply (rule TrueI) 

331 
done 

332 

333 

334 
subsection {*Universal quantifier*} 

335 

336 
lemma allI: assumes p: "!!x::'a. P(x)" shows "ALL x. P(x)" 

337 
apply (unfold All_def) 

17589  338 
apply (iprover intro: ext eqTrueI p) 
15411  339 
done 
340 

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

342 
apply (unfold All_def) 

343 
apply (rule eqTrueE) 

344 
apply (erule fun_cong) 

345 
done 

346 

347 
lemma allE: 

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

349 
and minor: "P(x) ==> R" 

350 
shows "R" 

17589  351 
by (iprover intro: minor major [THEN spec]) 
15411  352 

353 
lemma all_dupE: 

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

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

356 
shows "R" 

17589  357 
by (iprover intro: minor major major [THEN spec]) 
15411  358 

359 

360 
subsection {*False*} 

361 
(*Depends upon spec; it is impossible to do propositional logic before quantifiers!*) 

362 

363 
lemma FalseE: "False ==> P" 

364 
apply (unfold False_def) 

365 
apply (erule spec) 

366 
done 

367 

368 
lemma False_neq_True: "False=True ==> P" 

369 
by (erule eqTrueE [THEN FalseE]) 

370 

371 

372 
subsection {*Negation*} 

373 

374 
lemma notI: 

375 
assumes p: "P ==> False" 

376 
shows "~P" 

377 
apply (unfold not_def) 

17589  378 
apply (iprover intro: impI p) 
15411  379 
done 
380 

381 
lemma False_not_True: "False ~= True" 

382 
apply (rule notI) 

383 
apply (erule False_neq_True) 

384 
done 

385 

386 
lemma True_not_False: "True ~= False" 

387 
apply (rule notI) 

388 
apply (drule sym) 

389 
apply (erule False_neq_True) 

390 
done 

391 

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

393 
apply (unfold not_def) 

394 
apply (erule mp [THEN FalseE]) 

395 
apply assumption 

396 
done 

397 

398 
(* Alternative ~ introduction rule: [ P ==> ~ Pa; P ==> Pa ] ==> ~ P *) 

399 
lemmas notI2 = notE [THEN notI, standard] 

400 

401 

402 
subsection {*Implication*} 

403 

404 
lemma impE: 

405 
assumes "P>Q" "P" "Q ==> R" 

406 
shows "R" 

17589  407 
by (iprover intro: prems mp) 
15411  408 

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

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

17589  411 
by (iprover intro: mp) 
15411  412 

413 
lemma contrapos_nn: 

414 
assumes major: "~Q" 

415 
and minor: "P==>Q" 

416 
shows "~P" 

17589  417 
by (iprover intro: notI minor major [THEN notE]) 
15411  418 

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

420 
lemma contrapos_pn: 

421 
assumes major: "Q" 

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

423 
shows "~P" 

17589  424 
by (iprover intro: notI minor major notE) 
15411  425 

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

427 
apply (erule contrapos_nn) 

428 
apply (erule sym) 

429 
done 

430 

431 
(*still used in HOLCF*) 

432 
lemma rev_contrapos: 

433 
assumes pq: "P ==> Q" 

434 
and nq: "~Q" 

435 
shows "~P" 

436 
apply (rule nq [THEN contrapos_nn]) 

437 
apply (erule pq) 

438 
done 

439 

440 
subsection {*Existential quantifier*} 

441 

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

443 
apply (unfold Ex_def) 

17589  444 
apply (iprover intro: allI allE impI mp) 
15411  445 
done 
446 

447 
lemma exE: 

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

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

450 
shows "Q" 

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

17589  452 
apply (iprover intro: impI [THEN allI] minor) 
15411  453 
done 
454 

455 

456 
subsection {*Conjunction*} 

457 

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

459 
apply (unfold and_def) 

17589  460 
apply (iprover intro: impI [THEN allI] mp) 
15411  461 
done 
462 

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

464 
apply (unfold and_def) 

17589  465 
apply (iprover intro: impI dest: spec mp) 
15411  466 
done 
467 

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

469 
apply (unfold and_def) 

17589  470 
apply (iprover intro: impI dest: spec mp) 
15411  471 
done 
472 

473 
lemma conjE: 

474 
assumes major: "P&Q" 

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

476 
shows "R" 

477 
apply (rule minor) 

478 
apply (rule major [THEN conjunct1]) 

479 
apply (rule major [THEN conjunct2]) 

480 
done 

481 

482 
lemma context_conjI: 

483 
assumes prems: "P" "P ==> Q" shows "P & Q" 

17589  484 
by (iprover intro: conjI prems) 
15411  485 

486 

487 
subsection {*Disjunction*} 

488 

489 
lemma disjI1: "P ==> PQ" 

490 
apply (unfold or_def) 

17589  491 
apply (iprover intro: allI impI mp) 
15411  492 
done 
493 

494 
lemma disjI2: "Q ==> PQ" 

495 
apply (unfold or_def) 

17589  496 
apply (iprover intro: allI impI mp) 
15411  497 
done 
498 

499 
lemma disjE: 

500 
assumes major: "PQ" 

501 
and minorP: "P ==> R" 

502 
and minorQ: "Q ==> R" 

503 
shows "R" 

17589  504 
by (iprover intro: minorP minorQ impI 
15411  505 
major [unfolded or_def, THEN spec, THEN mp, THEN mp]) 
506 

507 

508 
subsection {*Classical logic*} 

509 

510 

511 
lemma classical: 

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

513 
shows "P" 

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

515 
apply assumption 

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

517 
apply (erule subst) 

518 
apply assumption 

519 
done 

520 

521 
lemmas ccontr = FalseE [THEN classical, standard] 

522 

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

524 
make elimination rules*) 

525 
lemma rev_notE: 

526 
assumes premp: "P" 

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

528 
shows "R" 

529 
apply (rule ccontr) 

530 
apply (erule notE [OF premnot premp]) 

531 
done 

532 

533 
(*Double negation law*) 

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

535 
apply (rule classical) 

536 
apply (erule notE) 

537 
apply assumption 

538 
done 

539 

540 
lemma contrapos_pp: 

541 
assumes p1: "Q" 

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

543 
shows "P" 

17589  544 
by (iprover intro: classical p1 p2 notE) 
15411  545 

546 

547 
subsection {*Unique existence*} 

548 

549 
lemma ex1I: 

550 
assumes prems: "P a" "!!x. P(x) ==> x=a" 

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

17589  552 
by (unfold Ex1_def, iprover intro: prems exI conjI allI impI) 
15411  553 

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

555 
lemma ex_ex1I: 

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

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

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

17589  559 
by (iprover intro: ex_prem [THEN exE] ex1I eq) 
15411  560 

561 
lemma ex1E: 

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

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

564 
shows "R" 

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

566 
apply (erule conjE) 

17589  567 
apply (iprover intro: minor) 
15411  568 
done 
569 

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

571 
apply (erule ex1E) 

572 
apply (rule exI) 

573 
apply assumption 

574 
done 

575 

576 

577 
subsection {*THE: definite description operator*} 

578 

579 
lemma the_equality: 

580 
assumes prema: "P a" 

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

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

583 
apply (rule trans [OF _ the_eq_trivial]) 

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

585 
apply (rule ext) 

586 
apply (rule iffI) 

587 
apply (erule premx) 

588 
apply (erule ssubst, rule prema) 

589 
done 

590 

591 
lemma theI: 

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

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

17589  594 
by (iprover intro: prems the_equality [THEN ssubst]) 
15411  595 

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

597 
apply (erule ex1E) 

598 
apply (erule theI) 

599 
apply (erule allE) 

600 
apply (erule mp) 

601 
apply assumption 

602 
done 

603 

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

605 
lemma theI2: 

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

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

17589  608 
by (iprover intro: prems theI) 
15411  609 

610 
lemma the1_equality: "[ EX!x. P x; P a ] ==> (THE x. P x) = a" 

611 
apply (rule the_equality) 

612 
apply assumption 

613 
apply (erule ex1E) 

614 
apply (erule all_dupE) 

615 
apply (drule mp) 

616 
apply assumption 

617 
apply (erule ssubst) 

618 
apply (erule allE) 

619 
apply (erule mp) 

620 
apply assumption 

621 
done 

622 

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

624 
apply (rule the_equality) 

625 
apply (rule refl) 

626 
apply (erule sym) 

627 
done 

628 

629 

630 
subsection {*Classical intro rules for disjunction and existential quantifiers*} 

631 

632 
lemma disjCI: 

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

634 
apply (rule classical) 

17589  635 
apply (iprover intro: prems disjI1 disjI2 notI elim: notE) 
15411  636 
done 
637 

638 
lemma excluded_middle: "~P  P" 

17589  639 
by (iprover intro: disjCI) 
15411  640 

641 
text{*case distinction as a natural deduction rule. Note that @{term "~P"} 

642 
is the second case, not the first.*} 

643 
lemma case_split_thm: 

644 
assumes prem1: "P ==> Q" 

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

646 
shows "Q" 

647 
apply (rule excluded_middle [THEN disjE]) 

648 
apply (erule prem2) 

649 
apply (erule prem1) 

650 
done 

651 

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

653 
lemma impCE: 

654 
assumes major: "P>Q" 

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

656 
shows "R" 

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

17589  658 
apply (iprover intro: minor major [THEN mp])+ 
15411  659 
done 
660 

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

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

663 
default: would break old proofs.*) 

664 
lemma impCE': 

665 
assumes major: "P>Q" 

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

667 
shows "R" 

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

17589  669 
apply (iprover intro: minor major [THEN mp])+ 
15411  670 
done 
671 

672 
(*Classical <> elimination. *) 

673 
lemma iffCE: 

674 
assumes major: "P=Q" 

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

676 
shows "R" 

677 
apply (rule major [THEN iffE]) 

17589  678 
apply (iprover intro: minor elim: impCE notE) 
15411  679 
done 
680 

681 
lemma exCI: 

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

683 
shows "EX x. P(x)" 

684 
apply (rule ccontr) 

17589  685 
apply (iprover intro: prems exI allI notI notE [of "\<exists>x. P x"]) 
15411  686 
done 
687 

688 

689 

11750  690 
subsection {* Theory and package setup *} 
691 

15411  692 
ML 
693 
{* 

694 
val eq_reflection = thm "eq_reflection" 

695 
val refl = thm "refl" 

696 
val subst = thm "subst" 

697 
val ext = thm "ext" 

698 
val impI = thm "impI" 

699 
val mp = thm "mp" 

700 
val True_def = thm "True_def" 

701 
val All_def = thm "All_def" 

702 
val Ex_def = thm "Ex_def" 

703 
val False_def = thm "False_def" 

704 
val not_def = thm "not_def" 

705 
val and_def = thm "and_def" 

706 
val or_def = thm "or_def" 

707 
val Ex1_def = thm "Ex1_def" 

708 
val iff = thm "iff" 

709 
val True_or_False = thm "True_or_False" 

710 
val Let_def = thm "Let_def" 

711 
val if_def = thm "if_def" 

712 
val sym = thm "sym" 

713 
val ssubst = thm "ssubst" 

714 
val trans = thm "trans" 

715 
val def_imp_eq = thm "def_imp_eq" 

716 
val box_equals = thm "box_equals" 

717 
val fun_cong = thm "fun_cong" 

718 
val arg_cong = thm "arg_cong" 

719 
val cong = thm "cong" 

720 
val iffI = thm "iffI" 

721 
val iffD2 = thm "iffD2" 

722 
val rev_iffD2 = thm "rev_iffD2" 

723 
val iffD1 = thm "iffD1" 

724 
val rev_iffD1 = thm "rev_iffD1" 

725 
val iffE = thm "iffE" 

726 
val TrueI = thm "TrueI" 

727 
val eqTrueI = thm "eqTrueI" 

728 
val eqTrueE = thm "eqTrueE" 

729 
val allI = thm "allI" 

730 
val spec = thm "spec" 

731 
val allE = thm "allE" 

732 
val all_dupE = thm "all_dupE" 

733 
val FalseE = thm "FalseE" 

734 
val False_neq_True = thm "False_neq_True" 

735 
val notI = thm "notI" 

736 
val False_not_True = thm "False_not_True" 

737 
val True_not_False = thm "True_not_False" 

738 
val notE = thm "notE" 

739 
val notI2 = thm "notI2" 

740 
val impE = thm "impE" 

741 
val rev_mp = thm "rev_mp" 

742 
val contrapos_nn = thm "contrapos_nn" 

743 
val contrapos_pn = thm "contrapos_pn" 

744 
val not_sym = thm "not_sym" 

745 
val rev_contrapos = thm "rev_contrapos" 

746 
val exI = thm "exI" 

747 
val exE = thm "exE" 

748 
val conjI = thm "conjI" 

749 
val conjunct1 = thm "conjunct1" 

750 
val conjunct2 = thm "conjunct2" 

751 
val conjE = thm "conjE" 

752 
val context_conjI = thm "context_conjI" 

753 
val disjI1 = thm "disjI1" 

754 
val disjI2 = thm "disjI2" 

755 
val disjE = thm "disjE" 

756 
val classical = thm "classical" 

757 
val ccontr = thm "ccontr" 

758 
val rev_notE = thm "rev_notE" 

759 
val notnotD = thm "notnotD" 

760 
val contrapos_pp = thm "contrapos_pp" 

761 
val ex1I = thm "ex1I" 

762 
val ex_ex1I = thm "ex_ex1I" 

763 
val ex1E = thm "ex1E" 

764 
val ex1_implies_ex = thm "ex1_implies_ex" 

765 
val the_equality = thm "the_equality" 

766 
val theI = thm "theI" 

767 
val theI' = thm "theI'" 

768 
val theI2 = thm "theI2" 

769 
val the1_equality = thm "the1_equality" 

770 
val the_sym_eq_trivial = thm "the_sym_eq_trivial" 

771 
val disjCI = thm "disjCI" 

772 
val excluded_middle = thm "excluded_middle" 

773 
val case_split_thm = thm "case_split_thm" 

774 
val impCE = thm "impCE" 

775 
val impCE = thm "impCE" 

776 
val iffCE = thm "iffCE" 

777 
val exCI = thm "exCI" 

4868  778 

15411  779 
(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *) 
780 
local 

781 
fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t 

782 
 wrong_prem (Bound _) = true 

783 
 wrong_prem _ = false 

15570  784 
val filter_right = List.filter (fn t => not (wrong_prem (HOLogic.dest_Trueprop (hd (Thm.prems_of t))))) 
15411  785 
in 
786 
fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]) 

787 
fun smp_tac j = EVERY'[dresolve_tac (smp j), atac] 

788 
end 

789 

790 

791 
fun strip_tac i = REPEAT(resolve_tac [impI,allI] i) 

792 

793 
(*Obsolete form of disjunctive case analysis*) 

794 
fun excluded_middle_tac sP = 

795 
res_inst_tac [("Q",sP)] (excluded_middle RS disjE) 

796 

797 
fun case_tac a = res_inst_tac [("P",a)] case_split_thm 

798 
*} 

799 

11687  800 
theorems case_split = case_split_thm [case_names True False] 
9869  801 

18457  802 
ML {* 
803 
structure ProjectRule = ProjectRuleFun 

804 
(struct 

805 
val conjunct1 = thm "conjunct1"; 

806 
val conjunct2 = thm "conjunct2"; 

807 
val mp = thm "mp"; 

808 
end) 

809 
*} 

810 

12386  811 

812 
subsubsection {* Intuitionistic Reasoning *} 

813 

814 
lemma impE': 

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

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

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

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

818 
shows R 
12386  819 
proof  
820 
from 3 and 1 have P . 

821 
with 1 have Q by (rule impE) 

822 
with 2 show R . 

823 
qed 

824 

825 
lemma allE': 

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

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

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

828 
shows Q 
12386  829 
proof  
830 
from 1 have "P x" by (rule spec) 

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

832 
qed 

833 

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

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

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

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

837 
shows R 
12386  838 
proof  
839 
from 2 and 1 have P . 

840 
with 1 show R by (rule notE) 

841 
qed 

842 

15801  843 
lemmas [Pure.elim!] = disjE iffE FalseE conjE exE 
844 
and [Pure.intro!] = iffI conjI impI TrueI notI allI refl 

845 
and [Pure.elim 2] = allE notE' impE' 

846 
and [Pure.intro] = exI disjI2 disjI1 

12386  847 

848 
lemmas [trans] = trans 

849 
and [sym] = sym not_sym 

15801  850 
and [Pure.elim?] = iffD1 iffD2 impE 
11750  851 

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

852 

11750  853 
subsubsection {* Atomizing metalevel connectives *} 
854 

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

12003  856 
proof 
9488  857 
assume "!!x. P x" 
10383  858 
show "ALL x. P x" by (rule allI) 
9488  859 
next 
860 
assume "ALL x. P x" 

10383  861 
thus "!!x. P x" by (rule allE) 
9488  862 
qed 
863 

11750  864 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
12003  865 
proof 
9488  866 
assume r: "A ==> B" 
10383  867 
show "A > B" by (rule impI) (rule r) 
9488  868 
next 
869 
assume "A > B" and A 

10383  870 
thus B by (rule mp) 
9488  871 
qed 
872 

14749  873 
lemma atomize_not: "(A ==> False) == Trueprop (~A)" 
874 
proof 

875 
assume r: "A ==> False" 

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

877 
next 

878 
assume "~A" and A 

879 
thus False by (rule notE) 

880 
qed 

881 

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

884 
assume "x == y" 
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset

885 
show "x = y" by (unfold prems) (rule refl) 
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset

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

887 
assume "x = y" 
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset

888 
thus "x == y" by (rule eq_reflection) 
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset

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

890 

12023  891 
lemma atomize_conj [atomize]: 
892 
"(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)" 

12003  893 
proof 
11953  894 
assume "!!C. (A ==> B ==> PROP C) ==> PROP C" 
895 
show "A & B" by (rule conjI) 

896 
next 

897 
fix C 

898 
assume "A & B" 

899 
assume "A ==> B ==> PROP C" 

900 
thus "PROP C" 

901 
proof this 

902 
show A by (rule conjunct1) 

903 
show B by (rule conjunct2) 

904 
qed 

905 
qed 

906 

12386  907 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
908 

11750  909 

910 
subsubsection {* Classical Reasoner setup *} 

9529  911 

10383  912 
use "cladata.ML" 
913 
setup hypsubst_setup 

11977  914 

16121  915 
setup {* 
916 
[ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)] 

12386  917 
*} 
11977  918 

10383  919 
setup Classical.setup 
920 
setup clasetup 

921 

12386  922 
lemmas [intro?] = ext 
923 
and [elim?] = ex1_implies_ex 

11977  924 

9869  925 
use "blastdata.ML" 
926 
setup Blast.setup 

4868  927 

11750  928 

17459  929 
subsubsection {* Simplifier setup *} 
11750  930 

12281  931 
lemma meta_eq_to_obj_eq: "x == y ==> x = y" 
932 
proof  

933 
assume r: "x == y" 

934 
show "x = y" by (unfold r) (rule refl) 

935 
qed 

936 

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

938 

939 
lemma simp_thms: 

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

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

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

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

944 
"(P  ~P) = True" "(~P  P) = True" 
12281  945 
"(x = x) = True" 
946 
"(~True) = False" "(~False) = True" 

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

947 
"(~P) ~= P" "P ~= (~P)" 
12281  948 
"(True=P) = P" "(P=True) = P" "(False=P) = (~P)" "(P=False) = (~P)" 
949 
"(True > P) = P" "(False > P) = True" 

950 
"(P > True) = True" "(P > P) = True" 

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

952 
"(P & True) = P" "(True & P) = P" 

953 
"(P & False) = False" "(False & P) = False" 

954 
"(P & P) = P" "(P & (P & Q)) = (P & Q)" 

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

956 
"(P  True) = True" "(True  P) = True" 

957 
"(P  False) = P" "(False  P) = P" 

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

958 
"(P  P) = P" "(P  (P  Q)) = (P  Q)" and 
12281  959 
"(ALL x. P) = P" "(EX x. P) = P" "EX x. x=t" "EX x. t=x" 
960 
 {* needed for the onepointrule quantifier simplification procs *} 

961 
 {* essential for termination!! *} and 

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

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

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

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

965 
"!!P. (ALL x. t=x > P(x)) = P(t)" 
17589  966 
by (blast, blast, blast, blast, blast, iprover+) 
13421  967 

12281  968 
lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P > Q) = (P' > Q'))" 
17589  969 
by iprover 
12281  970 

971 
lemma ex_simps: 

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

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

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

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

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

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

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

17589  979 
by (iprover  blast)+ 
12281  980 

981 
lemma all_simps: 

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

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

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

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

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

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

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

17589  989 
by (iprover  blast)+ 
12281  990 

14201  991 
lemma disj_absorb: "(A  A) = A" 
992 
by blast 

993 

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

995 
by blast 

996 

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

998 
by blast 

999 

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

1001 
by blast 

1002 

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

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

1005 
and eq_left_commute: "(P=(Q=R)) = (Q=(P=R))" 
17589  1006 
and eq_assoc: "((P=Q)=R) = (P=(Q=R))" by (iprover, blast+) 
1007 
lemma neq_commute: "(a~=b) = (b~=a)" by iprover 

12281  1008 

1009 
lemma conj_comms: 

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

1010 
shows conj_commute: "(P&Q) = (Q&P)" 
17589  1011 
and conj_left_commute: "(P&(Q&R)) = (Q&(P&R))" by iprover+ 
1012 
lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by iprover 

12281  1013 

1014 
lemma disj_comms: 

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

1015 
shows disj_commute: "(PQ) = (QP)" 
17589  1016 
and disj_left_commute: "(P(QR)) = (Q(PR))" by iprover+ 
1017 
lemma disj_assoc: "((PQ)R) = (P(QR))" by iprover 

12281  1018 

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

12281  1021 

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

12281  1024 

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

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

12281  1028 

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

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

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

1032 

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

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

1035 

17589  1036 
lemma de_Morgan_disj: "(~(P  Q)) = (~P & ~Q)" by iprover 
12281  1037 
lemma de_Morgan_conj: "(~(P & Q)) = (~P  ~Q)" by blast 
1038 
lemma not_imp: "(~(P > Q)) = (P & ~Q)" by blast 

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

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

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

1042 
by blast 

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

1044 

17589  1045 
lemma iff_conv_conj_imp: "(P = Q) = ((P > Q) & (Q > P))" by iprover 
12281  1046 

1047 

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

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

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

1051 
by blast 

1052 

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

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

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

12281  1057 

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

12281  1060 

1061 
text {* 

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

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

1064 

1065 
lemma conj_cong: 

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

17589  1067 
by iprover 
12281  1068 

1069 
lemma rev_conj_cong: 

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

17589  1071 
by iprover 
12281  1072 

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

1074 

1075 
lemma disj_cong: 

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

1077 
by blast 

1078 

1079 
lemma eq_sym_conv: "(x = y) = (y = x)" 

17589  1080 
by iprover 
12281  1081 

1082 

1083 
text {* \medskip ifthenelse rules *} 

1084 

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

1086 
by (unfold if_def) blast 

1087 

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

1089 
by (unfold if_def) blast 

1090 

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

1092 
by (unfold if_def) blast 

1093 

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

1095 
by (unfold if_def) blast 

1096 

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

1098 
apply (rule case_split [of Q]) 

15481  1099 
apply (simplesubst if_P) 
1100 
prefer 3 apply (simplesubst if_not_P, blast+) 

12281  1101 
done 
1102 

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

15481  1104 
by (simplesubst split_if, blast) 
12281  1105 

1106 
lemmas if_splits = split_if split_if_asm 

1107 

1108 
lemma if_def2: "(if Q then x else y) = ((Q > x) & (~ Q > y))" 

1109 
by (rule split_if) 

1110 

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

15481  1112 
by (simplesubst split_if, blast) 
12281  1113 

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

15481  1115 
by (simplesubst split_if, blast) 
12281  1116 

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

1118 
 {* This form is useful for expanding @{text if}s on the RIGHT of the @{text "==>"} symbol. *} 

1119 
by (rule split_if) 

1120 

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

1122 
 {* And this form is useful for expanding @{text if}s on the LEFT. *} 

15481  1123 
apply (simplesubst split_if, blast) 
12281  1124 
done 
1125 

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

12281  1128 

15423  1129 
text {* \medskip let rules for simproc *} 
1130 

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

1132 
by (unfold Let_def) 

1133 

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

1135 
by (unfold Let_def) 

1136 

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

1137 
text {* 
16999  1138 
The following copy of the implication operator is useful for 
1139 
finetuning congruence rules. It instructs the simplifier to simplify 

1140 
its premise. 

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

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

1142 

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

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

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

1146 

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

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

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

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

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

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

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

1154 

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

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

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

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

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

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

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

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

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

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

1164 

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

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

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

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

1168 
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

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

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

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

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

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

1174 
hence "PROP Q" by (rule PQ) 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1175 
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

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

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

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

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

1180 
hence "PROP Q'" by (rule P'Q') 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

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

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

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

1184 

17459  1185 

1186 
text {* \medskip Actual Installation of the Simplifier. *} 

14201  1187 

9869  1188 
use "simpdata.ML" 
1189 
setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup 

1190 
setup Splitter.setup setup Clasimp.setup 

1191 

15481  1192 

17459  1193 
text {* \medskip Lucas Dixon's eqstep tactic. *} 
15481  1194 

1195 
use "~~/src/Provers/eqsubst.ML"; 

1196 
use "eqrule_HOL_data.ML"; 

17459  1197 
setup EQSubstTac.setup 
15481  1198 

17459  1199 

1200 
subsubsection {* Code generator setup *} 

1201 

1202 
types_code 

1203 
"bool" ("bool") 

1204 
attach (term_of) {* 

1205 
fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const; 

1206 
*} 

1207 
attach (test) {* 

1208 
fun gen_bool i = one_of [false, true]; 

1209 
*} 

1210 

1211 
consts_code 

1212 
"True" ("true") 

1213 
"False" ("false") 

1214 
"Not" ("not") 

1215 
"op " ("(_ orelse/ _)") 

1216 
"op &" ("(_ andalso/ _)") 

1217 
"HOL.If" ("(if _/ then _/ else _)") 

1218 

1219 
ML {* 

1220 
local 

1221 

1222 
fun eq_codegen thy defs gr dep thyname b t = 

1223 
(case strip_comb t of 

1224 
(Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE 

1225 
 (Const ("op =", _), [t, u]) => 

1226 
let 

1227 
val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t); 

17639
50878db27b94
eq_codegen now ensures that code for bool type is generated.
berghofe
parents:
17589
diff
changeset

1228 
val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u); 
50878db27b94
eq_codegen now ensures that code for bool type is generated.
berghofe
parents:
17589
diff
changeset

1229 
val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT) 
17459  1230 
in 
17639
50878db27b94
eq_codegen now ensures that code for bool type is generated.
berghofe
parents:
17589
diff
changeset

1231 
SOME (gr''', Codegen.parens 
17459  1232 
(Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu])) 
1233 
end 

1234 
 (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen 

1235 
thy defs dep thyname b (gr, Codegen.eta_expand t ts 2)) 

1236 
 _ => NONE); 

1237 

1238 
in 

1239 

1240 
val eq_codegen_setup = [Codegen.add_codegen "eq_codegen" eq_codegen]; 

1241 

1242 
end; 

1243 
*} 

1244 

1245 
setup eq_codegen_setup 

15481  1246 

1247 

1248 
subsection {* Other simple lemmas *} 

1249 

15411  1250 
declare disj_absorb [simp] conj_absorb [simp] 
14201  1251 

13723  1252 
lemma ex1_eq[iff]: "EX! x. x = t" "EX! x. t = x" 
1253 
by blast+ 

1254 

15481  1255 

13638  1256 
theorem choice_eq: "(ALL x. EX! y. P x y) = (EX! f. ALL x. P x (f x))" 
1257 
apply (rule iffI) 

1258 
apply (rule_tac a = "%x. THE y. P x y" in ex1I) 

1259 
apply (fast dest!: theI') 

1260 
apply (fast intro: ext the1_equality [symmetric]) 

1261 
apply (erule ex1E) 

1262 
apply (rule allI) 

1263 
apply (rule ex1I) 

1264 
apply (erule spec) 

1265 
apply (erule_tac x = "%z. if z = x then y else f z" in allE) 

1266 
apply (erule impE) 

1267 
apply (rule allI) 

1268 
apply (rule_tac P = "xa = x" in case_split_thm) 

14208  1269 
apply (drule_tac [3] x = x in fun_cong, simp_all) 
13638  1270 
done 
1271 

13438
527811f00c56
added mk_left_commute to HOL.thy and used it "everywhere"
nipkow
parents:
13421
diff
changeset

1272 
text{*Needs only HOLlemmas:*} 
527811f00c56
added mk_left_commute to HOL.thy and used it "everywhere"
nipkow
parents:
13421
diff
changeset

1273 
lemma mk_left_commute: 
527811f00c56
added mk_left_commute to HOL.thy and used it "everywhere"
nipkow
parents:
13421
diff
changeset

1274 
assumes a: "\<And>x y z. f (f x y) z = f x (f y z)" and 
527811f00c56
added mk_left_commute to HOL.thy and used it "everywhere"
nipkow
parents:
13421
diff
changeset

1275 
c: "\<And>x y. f x y = f y x" 
527811f00c56
added mk_left_commute to HOL.thy and used it "everywhere"
nipkow
parents:
13421
diff
changeset

1276 
shows "f x (f y z) = f y (f x z)" 
527811f00c56
added mk_left_commute to HOL.thy and used it "everywhere"
nipkow
parents:
13421
diff
changeset

1277 
by(rule trans[OF trans[OF c a] arg_cong[OF c, of "f y"]]) 
527811f00c56
added mk_left_commute to HOL.thy and used it "everywhere"
nipkow
parents:
13421
diff
changeset

1278 

11750  1279 

15481  1280 
subsection {* Generic cases and induction *} 
11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1281 

f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1282 
constdefs 
18457  1283 
induct_forall where "induct_forall P == \<forall>x. P x" 
1284 
induct_implies where "induct_implies A B == A \<longrightarrow> B" 

1285 
induct_equal where "induct_equal x y == x = y" 

1286 
induct_conj where "induct_conj A B == A \<and> B" 

11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1287 

11989  1288 
lemma induct_forall_eq: "(!!x. P x) == Trueprop (induct_forall (\<lambda>x. P x))" 
18457  1289 
by (unfold atomize_all induct_forall_def) 
11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1290 

11989  1291 
lemma induct_implies_eq: "(A ==> B) == Trueprop (induct_implies A B)" 
18457  1292 
by (unfold atomize_imp induct_implies_def) 
11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1293 

11989  1294 
lemma induct_equal_eq: "(x == y) == Trueprop (induct_equal x y)" 
18457  1295 
by (unfold atomize_eq induct_equal_def) 
1296 

1297 
lemma induct_conj_eq: 

1298 
includes meta_conjunction_syntax 

1299 
shows "(A && B) == Trueprop (induct_conj A B)" 

1300 
by (unfold atomize_conj induct_conj_def) 

1301 

1302 
lemmas induct_atomize_old = induct_forall_eq induct_implies_eq induct_equal_eq atomize_conj 

1303 
lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq 

1304 
lemmas induct_rulify [symmetric, standard] = induct_atomize 

1305 
lemmas induct_rulify_fallback = 

1306 
induct_forall_def induct_implies_def induct_equal_def induct_conj_def 

1307 

11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1308 

11989  1309 
lemma induct_forall_conj: "induct_forall (\<lambda>x. induct_conj (A x) (B x)) = 
1310 
induct_conj (induct_forall A) (induct_forall B)" 

17589  1311 
by (unfold induct_forall_def induct_conj_def) iprover 
11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1312 

11989  1313 
lemma induct_implies_conj: "induct_implies C (induct_conj A B) = 
1314 
induct_conj (induct_implies C A) (induct_implies C B)" 

17589  1315 
by (unfold induct_implies_def induct_conj_def) iprover 
11989  1316 

13598
8bc77b17f59f
Fixed problem with induct_conj_curry: variable C should have type prop.
berghofe
parents:
13596
diff
changeset

1317 
lemma induct_conj_curry: "(induct_conj A B ==> PROP C) == (A ==> B ==> PROP C)" 
8bc77b17f59f
Fixed problem with induct_conj_curry: variable C should have type prop.
berghofe
parents:
13596
diff
changeset

1318 
proof 
8bc77b17f59f
Fixed problem with induct_conj_curry: variable C should have type prop.
berghofe
parents:
13596
diff
changeset

1319 
assume r: "induct_conj A B ==> PROP C" and A B 
18457  1320 
show "PROP C" by (rule r) (simp add: induct_conj_def `A` `B`) 
13598
8bc77b17f59f
Fixed problem with induct_conj_curry: variable C should have type prop.
berghofe
parents:
13596
diff
changeset

1321 
next 
8bc77b17f59f
Fixed problem with induct_conj_curry: variable C should have type prop.
berghofe
parents:
13596
diff
changeset

1322 
assume r: "A ==> B ==> PROP C" and "induct_conj A B" 
18457  1323 
show "PROP C" by (rule r) (simp_all add: `induct_conj A B` [unfolded induct_conj_def]) 
13598
8bc77b17f59f
Fixed problem with induct_conj_curry: variable C should have type prop.
berghofe
parents:
13596
diff
changeset

1324 
qed 
11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1325 

11989  1326 
lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry 
11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1327 

11989  1328 
hide const induct_forall induct_implies induct_equal induct_conj 
11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1329 

f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1330 

f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1331 
text {* Method setup. *} 
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1332 

f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1333 
ML {* 
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1334 
structure InductMethod = InductMethodFun 
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1335 
(struct 
15411  1336 
val cases_default = thm "case_split" 
18457  1337 
val atomize_old = thms "induct_atomize_old" 
15411  1338 
val atomize = thms "induct_atomize" 
18457  1339 
val rulify = thms "induct_rulify" 
1340 
val rulify_fallback = thms "induct_rulify_fallback" 

11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1341 
end); 
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1342 
*} 
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1343 

f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1344 
setup InductMethod.setup 
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1345 

18457  1346 

1347 
subsubsection {*Tags, for the ATP Linkup *} 

17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17274
diff
changeset

1348 

d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17274
diff
changeset

1349 
constdefs 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17274
diff
changeset

1350 
tag :: "bool => bool" 
18457  1351 
"tag P == P" 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17274
diff
changeset

1352 

d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17274
diff
changeset

1353 
text{*These label the distinguished literals of introduction and elimination 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17274
diff
changeset

1354 
rules.*} 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17274
diff
changeset

1355 

d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17274
diff
changeset

1356 
lemma tagI: "P ==> tag P" 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17274
diff
changeset

1357 
by (simp add: tag_def) 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17274
diff
changeset

1358 

d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17274
diff
changeset

1359 
lemma tagD: "tag P ==> P" 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17274
diff
changeset

1360 
by (simp add: tag_def) 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17274
diff
changeset

1361 

d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17274
diff
changeset

1362 
text{*Applications of "tag" to True and False must go!*} 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17274
diff
changeset

1363 

d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17274
diff
changeset

1364 
lemma tag_True: "tag True = True" 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17274
diff
changeset

1365 
by (simp add: tag_def) 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17274
diff
changeset

1366 

d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17274
diff
changeset

1367 
lemma tag_False: "tag False = False" 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17274
diff
changeset

1368 
by (simp add: tag_def) 
11824
f4c1882dde2c
setup generic cases and induction (from Inductive.thy);
wenzelm
parents:
11770
diff
changeset

1369 

14357  1370 
end 