author  wenzelm 
Wed, 06 Dec 2006 01:12:42 +0100  
changeset 21671  f7d652ffef09 
parent 21547  9c9fdf4c2949 
child 22129  bb2203c93316 
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 
21151  10 
uses ("simpdata.ML") "Tools/res_atpset.ML" 
15131  11 
begin 
2260  12 

11750  13 
subsection {* Primitive logic *} 
14 

15 
subsubsection {* Core syntax *} 

2260  16 

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

18 
defaultsort type 
3947  19 

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

20 
global 
923  21 

7357  22 
typedecl bool 
923  23 

24 
arities 

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

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

26 
"fun" :: (type, type) type 
923  27 

11750  28 
judgment 
29 
Trueprop :: "bool => prop" ("(_)" 5) 

923  30 

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

34 
False :: bool 

3947  35 
arbitrary :: 'a 
20172  36 
undefined :: 'a 
923  37 

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

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

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

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

923  43 

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

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

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

923  48 

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

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

50 

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

2260  53 

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

54 

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

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

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

59 

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

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

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

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

63 

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

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

66 

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

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

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

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

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

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

73 

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

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

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

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

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

79 

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

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

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

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

83 

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

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

86 

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

87 

4868  88 
nonterminals 
923  89 
letbinds letbind 
90 
case_syn cases_syn 

91 

92 
syntax 

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

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

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

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

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

923  99 

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

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

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

103 
"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/  _") 
923  104 

105 
translations 

13764  106 
"THE x. P" == "The (%x. P)" 
923  107 
"_Let (_binds b bs) e" == "_Let b (_Let bs e)" 
1114  108 
"let x = a in e" == "Let a (%x. e)" 
923  109 

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

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

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

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

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

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

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

116 

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

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

120 
notation (xsymbols) 

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

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

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

2372  124 

21524  125 
notation (HTML output) 
126 
All (binder "\<forall>" 10) and 

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

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

6340  129 

21524  130 
notation (HOL) 
131 
All (binder "! " 10) and 

132 
Ex (binder "? " 10) and 

133 
Ex1 (binder "?! " 10) 

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

134 

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

135 

11750  136 
subsubsection {* Axioms and basic definitions *} 
2260  137 

7357  138 
axioms 
15380  139 
eq_reflection: "(x=y) ==> (x==y)" 
923  140 

15380  141 
refl: "t = (t::'a)" 
6289  142 

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

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

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

6289  147 

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

148 
the_eq_trivial: "(THE x. x = a) = (a::'a)" 
923  149 

15380  150 
impI: "(P ==> Q) ==> P>Q" 
151 
mp: "[ P>Q; P ] ==> Q" 

152 

153 

923  154 
defs 
7357  155 
True_def: "True == ((%x::bool. x) = (%x. x))" 
156 
All_def: "All(P) == (P = (%x. True))" 

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

157 
Ex_def: "Ex(P) == !Q. (!x. P x > Q) > Q" 
7357  158 
False_def: "False == (!P. P)" 
159 
not_def: "~ P == P>False" 

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

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

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

923  163 

7357  164 
axioms 
165 
iff: "(P>Q) > (Q>P) > (P=Q)" 

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

923  167 

168 
defs 

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

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

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

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

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

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

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

176 
arbitrary 
20172  177 
undefined 
3320  178 

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

179 

11750  180 
subsubsection {* Generic algebraic operations *} 
4868  181 

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

182 
class zero = 
21524  183 
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

184 

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

185 
class one = 
21524  186 
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

187 

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

188 
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

189 

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

190 
class plus = 
21524  191 
fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>+" 65) 
11750  192 

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

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

194 
fixes uminus :: "'a \<Rightarrow> 'a" 
21524  195 
and minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>" 65) 
196 
and abs :: "'a \<Rightarrow> 'a" 

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

197 

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

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

199 
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

200 

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

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

202 
fixes inverse :: "'a \<Rightarrow> 'a" 
21524  203 
and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>'/" 70) 
204 

205 
notation 

206 
uminus (" _" [81] 80) 

207 

208 
notation (xsymbols) 

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

210 
notation (HTML output) 

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

11750  212 

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

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

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

215 
translations 
14690  216 
(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

217 

11750  218 
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

219 
let 
21410  220 
val thy = the_context (); 
20713
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset

221 
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

222 
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

223 
else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T); 
21410  224 
in map (tr' o Sign.const_syntax_name thy) ["HOL.one", "HOL.zero"] end; 
11750  225 
*}  {* show types that are presumably too general *} 
226 

227 

20944  228 
subsection {* Fundamental rules *} 
229 

20973  230 
subsubsection {* Equality *} 
20944  231 

232 
text {* Thanks to Stephan Merz *} 

233 
lemma subst: 

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

235 
shows "P t" 

236 
proof  

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

238 
by (rule eq_reflection) 

239 
from p show ?thesis 

240 
by (unfold meta) 

241 
qed 

15411  242 

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

15411  245 

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

15411  248 

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

18457  250 
by (erule subst) 
15411  251 

20944  252 
lemma def_imp_eq: 
253 
assumes meq: "A == B" 

254 
shows "A = B" 

18457  255 
by (unfold meq) (rule refl) 
256 

20944  257 
(*a mere copy*) 
258 
lemma meta_eq_to_obj_eq: 

259 
assumes meq: "A == B" 

260 
shows "A = B" 

261 
by (unfold meq) (rule refl) 

15411  262 

21502  263 
text {* Useful with @{text erule} for proving equalities from known equalities. *} 
20944  264 
(* a = b 
15411  265 
  
266 
c = d *) 

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

268 
apply (rule trans) 

269 
apply (rule trans) 

270 
apply (rule sym) 

271 
apply assumption+ 

272 
done 

273 

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

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

275 

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

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

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

278 

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

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

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

281 

15411  282 

20944  283 
subsubsection {*Congruence rules for application*} 
15411  284 

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

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

287 
apply (erule subst) 

288 
apply (rule refl) 

289 
done 

290 

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

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

293 
apply (erule subst) 

294 
apply (rule refl) 

295 
done 

296 

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

299 
apply (rule refl) 

300 
done 

301 

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

304 
apply (rule refl) 

305 
done 

306 

307 

20944  308 
subsubsection {*Equality of booleans  iff*} 
15411  309 

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

15411  312 

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

18457  314 
by (erule ssubst) 
15411  315 

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

18457  317 
by (erule iffD2) 
15411  318 

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

321 

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

323 
by (drule sym) (rule rev_iffD2) 

15411  324 

325 
lemma iffE: 

326 
assumes major: "P=Q" 

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

15411  330 

331 

20944  332 
subsubsection {*True*} 
15411  333 

334 
lemma TrueI: "True" 

21504  335 
unfolding True_def by (rule refl) 
15411  336 

21504  337 
lemma eqTrueI: "P ==> P = True" 
18457  338 
by (iprover intro: iffI TrueI) 
15411  339 

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

15411  342 

343 

20944  344 
subsubsection {*Universal quantifier*} 
15411  345 

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

15411  348 

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

350 
apply (unfold All_def) 

351 
apply (rule eqTrueE) 

352 
apply (erule fun_cong) 

353 
done 

354 

355 
lemma allE: 

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

21504  357 
and minor: "P(x) ==> R" 
358 
shows R 

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

15411  360 

361 
lemma all_dupE: 

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

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

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

15411  366 

367 

21504  368 
subsubsection {* False *} 
369 

370 
text {* 

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

372 
logic before quantifiers! 

373 
*} 

15411  374 

375 
lemma FalseE: "False ==> P" 

21504  376 
apply (unfold False_def) 
377 
apply (erule spec) 

378 
done 

15411  379 

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

15411  382 

383 

21504  384 
subsubsection {* Negation *} 
15411  385 

386 
lemma notI: 

21504  387 
assumes "P ==> False" 
15411  388 
shows "~P" 
21504  389 
apply (unfold not_def) 
390 
apply (iprover intro: impI assms) 

391 
done 

15411  392 

393 
lemma False_not_True: "False ~= True" 

21504  394 
apply (rule notI) 
395 
apply (erule False_neq_True) 

396 
done 

15411  397 

398 
lemma True_not_False: "True ~= False" 

21504  399 
apply (rule notI) 
400 
apply (drule sym) 

401 
apply (erule False_neq_True) 

402 
done 

15411  403 

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

21504  405 
apply (unfold not_def) 
406 
apply (erule mp [THEN FalseE]) 

407 
apply assumption 

408 
done 

15411  409 

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

15411  412 

413 

20944  414 
subsubsection {*Implication*} 
15411  415 

416 
lemma impE: 

417 
assumes "P>Q" "P" "Q ==> R" 

418 
shows "R" 

17589  419 
by (iprover intro: prems mp) 
15411  420 

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

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

17589  423 
by (iprover intro: mp) 
15411  424 

425 
lemma contrapos_nn: 

426 
assumes major: "~Q" 

427 
and minor: "P==>Q" 

428 
shows "~P" 

17589  429 
by (iprover intro: notI minor major [THEN notE]) 
15411  430 

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

432 
lemma contrapos_pn: 

433 
assumes major: "Q" 

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

435 
shows "~P" 

17589  436 
by (iprover intro: notI minor major notE) 
15411  437 

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

21250  439 
by (erule contrapos_nn) (erule sym) 
440 

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

442 
by (erule subst, erule ssubst, assumption) 

15411  443 

444 
(*still used in HOLCF*) 

445 
lemma rev_contrapos: 

446 
assumes pq: "P ==> Q" 

447 
and nq: "~Q" 

448 
shows "~P" 

449 
apply (rule nq [THEN contrapos_nn]) 

450 
apply (erule pq) 

451 
done 

452 

20944  453 
subsubsection {*Existential quantifier*} 
15411  454 

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

456 
apply (unfold Ex_def) 

17589  457 
apply (iprover intro: allI allE impI mp) 
15411  458 
done 
459 

460 
lemma exE: 

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

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

463 
shows "Q" 

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

17589  465 
apply (iprover intro: impI [THEN allI] minor) 
15411  466 
done 
467 

468 

20944  469 
subsubsection {*Conjunction*} 
15411  470 

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

472 
apply (unfold and_def) 

17589  473 
apply (iprover intro: impI [THEN allI] mp) 
15411  474 
done 
475 

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

477 
apply (unfold and_def) 

17589  478 
apply (iprover intro: impI dest: spec mp) 
15411  479 
done 
480 

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

482 
apply (unfold and_def) 

17589  483 
apply (iprover intro: impI dest: spec mp) 
15411  484 
done 
485 

486 
lemma conjE: 

487 
assumes major: "P&Q" 

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

489 
shows "R" 

490 
apply (rule minor) 

491 
apply (rule major [THEN conjunct1]) 

492 
apply (rule major [THEN conjunct2]) 

493 
done 

494 

495 
lemma context_conjI: 

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

17589  497 
by (iprover intro: conjI prems) 
15411  498 

499 

20944  500 
subsubsection {*Disjunction*} 
15411  501 

502 
lemma disjI1: "P ==> PQ" 

503 
apply (unfold or_def) 

17589  504 
apply (iprover intro: allI impI mp) 
15411  505 
done 
506 

507 
lemma disjI2: "Q ==> PQ" 

508 
apply (unfold or_def) 

17589  509 
apply (iprover intro: allI impI mp) 
15411  510 
done 
511 

512 
lemma disjE: 

513 
assumes major: "PQ" 

514 
and minorP: "P ==> R" 

515 
and minorQ: "Q ==> R" 

516 
shows "R" 

17589  517 
by (iprover intro: minorP minorQ impI 
15411  518 
major [unfolded or_def, THEN spec, THEN mp, THEN mp]) 
519 

520 

20944  521 
subsubsection {*Classical logic*} 
15411  522 

523 
lemma classical: 

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

525 
shows "P" 

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

527 
apply assumption 

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

529 
apply (erule subst) 

530 
apply assumption 

531 
done 

532 

533 
lemmas ccontr = FalseE [THEN classical, standard] 

534 

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

536 
make elimination rules*) 

537 
lemma rev_notE: 

538 
assumes premp: "P" 

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

540 
shows "R" 

541 
apply (rule ccontr) 

542 
apply (erule notE [OF premnot premp]) 

543 
done 

544 

545 
(*Double negation law*) 

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

547 
apply (rule classical) 

548 
apply (erule notE) 

549 
apply assumption 

550 
done 

551 

552 
lemma contrapos_pp: 

553 
assumes p1: "Q" 

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

555 
shows "P" 

17589  556 
by (iprover intro: classical p1 p2 notE) 
15411  557 

558 

20944  559 
subsubsection {*Unique existence*} 
15411  560 

561 
lemma ex1I: 

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

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

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

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

567 
lemma ex_ex1I: 

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

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

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

17589  571 
by (iprover intro: ex_prem [THEN exE] ex1I eq) 
15411  572 

573 
lemma ex1E: 

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

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

576 
shows "R" 

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

578 
apply (erule conjE) 

17589  579 
apply (iprover intro: minor) 
15411  580 
done 
581 

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

583 
apply (erule ex1E) 

584 
apply (rule exI) 

585 
apply assumption 

586 
done 

587 

588 

20944  589 
subsubsection {*THE: definite description operator*} 
15411  590 

591 
lemma the_equality: 

592 
assumes prema: "P a" 

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

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

595 
apply (rule trans [OF _ the_eq_trivial]) 

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

597 
apply (rule ext) 

598 
apply (rule iffI) 

599 
apply (erule premx) 

600 
apply (erule ssubst, rule prema) 

601 
done 

602 

603 
lemma theI: 

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

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

17589  606 
by (iprover intro: prems the_equality [THEN ssubst]) 
15411  607 

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

609 
apply (erule ex1E) 

610 
apply (erule theI) 

611 
apply (erule allE) 

612 
apply (erule mp) 

613 
apply assumption 

614 
done 

615 

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

617 
lemma theI2: 

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

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

17589  620 
by (iprover intro: prems theI) 
15411  621 

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

625 
apply (erule ex1E) 

626 
apply (erule all_dupE) 

627 
apply (drule mp) 

628 
apply assumption 

629 
apply (erule ssubst) 

630 
apply (erule allE) 

631 
apply (erule mp) 

632 
apply assumption 

633 
done 

634 

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

636 
apply (rule the_equality) 

637 
apply (rule refl) 

638 
apply (erule sym) 

639 
done 

640 

641 

20944  642 
subsubsection {*Classical intro rules for disjunction and existential quantifiers*} 
15411  643 

644 
lemma disjCI: 

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

646 
apply (rule classical) 

17589  647 
apply (iprover intro: prems disjI1 disjI2 notI elim: notE) 
15411  648 
done 
649 

650 
lemma excluded_middle: "~P  P" 

17589  651 
by (iprover intro: disjCI) 
15411  652 

20944  653 
text {* 
654 
case distinction as a natural deduction rule. 

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

656 
*} 

15411  657 
lemma case_split_thm: 
658 
assumes prem1: "P ==> Q" 

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

660 
shows "Q" 

661 
apply (rule excluded_middle [THEN disjE]) 

662 
apply (erule prem2) 

663 
apply (erule prem1) 

664 
done 

20944  665 
lemmas case_split = case_split_thm [case_names True False] 
15411  666 

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

668 
lemma impCE: 

669 
assumes major: "P>Q" 

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

671 
shows "R" 

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

17589  673 
apply (iprover intro: minor major [THEN mp])+ 
15411  674 
done 
675 

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

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

678 
default: would break old proofs.*) 

679 
lemma impCE': 

680 
assumes major: "P>Q" 

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

682 
shows "R" 

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

17589  684 
apply (iprover intro: minor major [THEN mp])+ 
15411  685 
done 
686 

687 
(*Classical <> elimination. *) 

688 
lemma iffCE: 

689 
assumes major: "P=Q" 

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

691 
shows "R" 

692 
apply (rule major [THEN iffE]) 

17589  693 
apply (iprover intro: minor elim: impCE notE) 
15411  694 
done 
695 

696 
lemma exCI: 

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

698 
shows "EX x. P(x)" 

699 
apply (rule ccontr) 

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

703 

12386  704 
subsubsection {* Intuitionistic Reasoning *} 
705 

706 
lemma impE': 

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

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

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

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

710 
shows R 
12386  711 
proof  
712 
from 3 and 1 have P . 

713 
with 1 have Q by (rule impE) 

714 
with 2 show R . 

715 
qed 

716 

717 
lemma allE': 

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

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

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

720 
shows Q 
12386  721 
proof  
722 
from 1 have "P x" by (rule spec) 

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

724 
qed 

725 

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

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

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

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

729 
shows R 
12386  730 
proof  
731 
from 2 and 1 have P . 

732 
with 1 show R by (rule notE) 

733 
qed 

734 

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

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

738 
and [Pure.intro] = exI disjI2 disjI1 

12386  739 

740 
lemmas [trans] = trans 

741 
and [sym] = sym not_sym 

15801  742 
and [Pure.elim?] = iffD1 iffD2 impE 
11750  743 

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

744 

11750  745 
subsubsection {* Atomizing metalevel connectives *} 
746 

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

12003  748 
proof 
9488  749 
assume "!!x. P x" 
10383  750 
show "ALL x. P x" by (rule allI) 
9488  751 
next 
752 
assume "ALL x. P x" 

10383  753 
thus "!!x. P x" by (rule allE) 
9488  754 
qed 
755 

11750  756 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
12003  757 
proof 
9488  758 
assume r: "A ==> B" 
10383  759 
show "A > B" by (rule impI) (rule r) 
9488  760 
next 
761 
assume "A > B" and A 

10383  762 
thus B by (rule mp) 
9488  763 
qed 
764 

14749  765 
lemma atomize_not: "(A ==> False) == Trueprop (~A)" 
766 
proof 

767 
assume r: "A ==> False" 

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

769 
next 

770 
assume "~A" and A 

771 
thus False by (rule notE) 

772 
qed 

773 

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

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

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

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

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

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

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

782 

12023  783 
lemma atomize_conj [atomize]: 
19121  784 
includes meta_conjunction_syntax 
785 
shows "(A && B) == Trueprop (A & B)" 

12003  786 
proof 
19121  787 
assume conj: "A && B" 
788 
show "A & B" 

789 
proof (rule conjI) 

790 
from conj show A by (rule conjunctionD1) 

791 
from conj show B by (rule conjunctionD2) 

792 
qed 

11953  793 
next 
19121  794 
assume conj: "A & B" 
795 
show "A && B" 

796 
proof  

797 
from conj show A .. 

798 
from conj show B .. 

11953  799 
qed 
800 
qed 

801 

12386  802 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
18832  803 
and [symmetric, defn] = atomize_all atomize_imp atomize_eq 
12386  804 

11750  805 

20944  806 
subsection {* Package setup *} 
807 

11750  808 
subsubsection {* Classical Reasoner setup *} 
9529  809 

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

812 

21151  813 
ML {* 
814 
structure Hypsubst = HypsubstFun( 

815 
struct 

816 
structure Simplifier = Simplifier 

21218  817 
val dest_eq = HOLogic.dest_eq 
21151  818 
val dest_Trueprop = HOLogic.dest_Trueprop 
819 
val dest_imp = HOLogic.dest_imp 

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

820 
val eq_reflection = thm "HOL.eq_reflection" 
9c9fdf4c2949
moved order arities for fun and bool to Fun/Orderings
haftmann
parents:
21524
diff
changeset

821 
val rev_eq_reflection = thm "HOL.def_imp_eq" 
9c9fdf4c2949
moved order arities for fun and bool to Fun/Orderings
haftmann
parents:
21524
diff
changeset

822 
val imp_intr = thm "HOL.impI" 
9c9fdf4c2949
moved order arities for fun and bool to Fun/Orderings
haftmann
parents:
21524
diff
changeset

823 
val rev_mp = thm "HOL.rev_mp" 
9c9fdf4c2949
moved order arities for fun and bool to Fun/Orderings
haftmann
parents:
21524
diff
changeset

824 
val subst = thm "HOL.subst" 
9c9fdf4c2949
moved order arities for fun and bool to Fun/Orderings
haftmann
parents:
21524
diff
changeset

825 
val sym = thm "HOL.sym" 
21151  826 
val thin_refl = thm "thin_refl"; 
827 
end); 

21671  828 
open Hypsubst; 
21151  829 

830 
structure Classical = ClassicalFun( 

831 
struct 

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

832 
val mp = thm "HOL.mp" 
9c9fdf4c2949
moved order arities for fun and bool to Fun/Orderings
haftmann
parents:
21524
diff
changeset

833 
val not_elim = thm "HOL.notE" 
9c9fdf4c2949
moved order arities for fun and bool to Fun/Orderings
haftmann
parents:
21524
diff
changeset

834 
val classical = thm "HOL.classical" 
21151  835 
val sizef = Drule.size_of_thm 
836 
val hyp_subst_tacs = [Hypsubst.hyp_subst_tac] 

837 
end); 

838 

839 
structure BasicClassical: BASIC_CLASSICAL = Classical; 

21671  840 
open BasicClassical; 
21151  841 
*} 
842 

21009  843 
setup {* 
844 
let 

845 
(*prevent substitution on bool*) 

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

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

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

849 
in 

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

852 
#> Classical.setup 

853 
#> ResAtpset.setup 

21009  854 
end 
855 
*} 

856 

857 
declare iffI [intro!] 

858 
and notI [intro!] 

859 
and impI [intro!] 

860 
and disjCI [intro!] 

861 
and conjI [intro!] 

862 
and TrueI [intro!] 

863 
and refl [intro!] 

864 

865 
declare iffCE [elim!] 

866 
and FalseE [elim!] 

867 
and impCE [elim!] 

868 
and disjE [elim!] 

869 
and conjE [elim!] 

870 
and conjE [elim!] 

871 

872 
declare ex_ex1I [intro!] 

873 
and allI [intro!] 

874 
and the_equality [intro] 

875 
and exI [intro] 

876 

877 
declare exE [elim!] 

878 
allE [elim] 

879 

880 
ML {* 

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

881 
val HOL_cs = Classical.claset_of (the_context ()); 
21009  882 
*} 
19162  883 

20223  884 
lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P" 
885 
apply (erule swap) 

886 
apply (erule (1) meta_mp) 

887 
done 

10383  888 

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

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

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

891 

12386  892 
lemmas [intro?] = ext 
893 
and [elim?] = ex1_implies_ex 

11977  894 

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

899 
shows R 

900 
apply (rule ex1E [OF major]) 

901 
apply (rule prem) 

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

902 
apply (tactic {* ares_tac [thm "allI"] 1 *})+ 
9c9fdf4c2949
moved order arities for fun and bool to Fun/Orderings
haftmann
parents:
21524
diff
changeset

903 
apply (tactic {* etac (Classical.dup_elim (thm "allE")) 1 *}) 
20944  904 
by iprover 
905 

21151  906 
ML {* 
907 
structure Blast = BlastFun( 

908 
struct 

909 
type claset = Classical.claset 

910 
val equality_name = "op =" 

911 
val not_name = "Not" 

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

912 
val notE = thm "HOL.notE" 
9c9fdf4c2949
moved order arities for fun and bool to Fun/Orderings
haftmann
parents:
21524
diff
changeset

913 
val ccontr = thm "HOL.ccontr" 
21151  914 
val contr_tac = Classical.contr_tac 
915 
val dup_intr = Classical.dup_intr 

916 
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac 

21671  917 
val claset = Classical.claset 
21151  918 
val rep_cs = Classical.rep_cs 
919 
val cla_modifiers = Classical.cla_modifiers 

920 
val cla_meth' = Classical.cla_meth' 

921 
end); 

21671  922 
val Blast_tac = Blast.Blast_tac; 
923 
val blast_tac = Blast.blast_tac; 

20944  924 
*} 
925 

21151  926 
setup Blast.setup 
927 

20944  928 

929 
subsubsection {* Simplifier *} 

12281  930 

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

932 

933 
lemma simp_thms: 

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

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

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

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

938 
"(P  ~P) = True" "(~P  P) = True" 
12281  939 
"(x = x) = True" 
20944  940 
and not_True_eq_False: "(\<not> True) = False" 
941 
and not_False_eq_True: "(\<not> False) = True" 

942 
and 

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

943 
"(~P) ~= P" "P ~= (~P)" 
20944  944 
"(True=P) = P" 
945 
and eq_True: "(P = True) = P" 

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

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

948 
and 

12281  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 

14201  968 
lemma disj_absorb: "(A  A) = A" 
969 
by blast 

970 

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

972 
by blast 

973 

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

975 
by blast 

976 

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

978 
by blast 

979 

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

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

982 
and eq_left_commute: "(P=(Q=R)) = (Q=(P=R))" 
17589  983 
and eq_assoc: "((P=Q)=R) = (P=(Q=R))" by (iprover, blast+) 
984 
lemma neq_commute: "(a~=b) = (b~=a)" by iprover 

12281  985 

986 
lemma conj_comms: 

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

987 
shows conj_commute: "(P&Q) = (Q&P)" 
17589  988 
and conj_left_commute: "(P&(Q&R)) = (Q&(P&R))" by iprover+ 
989 
lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by iprover 

12281  990 

19174  991 
lemmas conj_ac = conj_commute conj_left_commute conj_assoc 
992 

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

994 
shows disj_commute: "(PQ) = (QP)" 
17589  995 
and disj_left_commute: "(P(QR)) = (Q(PR))" by iprover+ 
996 
lemma disj_assoc: "((PQ)R) = (P(QR))" by iprover 

12281  997 

19174  998 
lemmas disj_ac = disj_commute disj_left_commute disj_assoc 
999 

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

12281  1002 

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

12281  1005 

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

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

12281  1009 

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

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

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

1013 

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

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

1016 

21151  1017 
lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P > Q) = (P' > Q'))" 
1018 
by iprover 

1019 

17589  1020 
lemma de_Morgan_disj: "(~(P  Q)) = (~P & ~Q)" by iprover 
12281  1021 
lemma de_Morgan_conj: "(~(P & Q)) = (~P  ~Q)" by blast 
1022 
lemma not_imp: "(~(P > Q)) = (P & ~Q)" by blast 

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

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

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

1026 
by blast 

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

1028 

17589  1029 
lemma iff_conv_conj_imp: "(P = Q) = ((P > Q) & (Q > P))" by iprover 
12281  1030 

1031 

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

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

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

1035 
by blast 

1036 

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

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

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

12281  1041 

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

12281  1044 

1045 
text {* 

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

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

1048 

1049 
lemma conj_cong: 

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

17589  1051 
by iprover 
12281  1052 

1053 
lemma rev_conj_cong: 

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

17589  1055 
by iprover 
12281  1056 

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

1058 

1059 
lemma disj_cong: 

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

1061 
by blast 

1062 

1063 

1064 
text {* \medskip ifthenelse rules *} 

1065 

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

1067 
by (unfold if_def) blast 

1068 

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

1070 
by (unfold if_def) blast 

1071 

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

1073 
by (unfold if_def) blast 

1074 

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

1076 
by (unfold if_def) blast 

1077 

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

1079 
apply (rule case_split [of Q]) 

15481  1080 
apply (simplesubst if_P) 
1081 
prefer 3 apply (simplesubst if_not_P, blast+) 

12281  1082 
done 
1083 

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

15481  1085 
by (simplesubst split_if, blast) 
12281  1086 

1087 
lemmas if_splits = split_if split_if_asm 

1088 

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

15481  1090 
by (simplesubst split_if, blast) 
12281  1091 

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

15481  1093 
by (simplesubst split_if, blast) 
12281  1094 

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

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

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

19796  1100 
 {* And this form is useful for expanding @{text "if"}s on the LEFT. *} 
15481  1101 
apply (simplesubst split_if, blast) 
12281  1102 
done 
1103 

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

12281  1106 

15423  1107 
text {* \medskip let rules for simproc *} 
1108 

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

1110 
by (unfold Let_def) 

1111 

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

1113 
by (unfold Let_def) 

1114 

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

1115 
text {* 
16999  1116 
The following copy of the implication operator is useful for 
1117 
finetuning congruence rules. It instructs the simplifier to simplify 

1118 
its premise. 

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

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

1120 

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

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

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

1124 

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

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

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

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

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

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

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

1132 

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

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

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

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

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

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

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

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

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

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

1142 

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

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

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

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

1146 
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

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

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

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

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

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

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

1153 
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

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

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

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

1157 
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

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

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

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

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

1162 

20944  1163 
lemma uncurry: 
1164 
assumes "P \<longrightarrow> Q \<longrightarrow> R" 

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

1166 
using prems by blast 

1167 

1168 
lemma iff_allI: 

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

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

1171 
using prems by blast 

1172 

1173 
lemma iff_exI: 

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

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

1176 
using prems by blast 

1177 

1178 
lemma all_comm: 

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

1180 
by blast 

1181 

1182 
lemma ex_comm: 

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

1184 
by blast 

1185 

9869  1186 
use "simpdata.ML" 
21671  1187 
ML {* open Simpdata *} 
1188 

21151  1189 
setup {* 
1190 
Simplifier.method_setup Splitter.split_modifiers 

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

1191 
#> (fn thy => (change_simpset_of thy (fn _ => Simpdata.simpset_simprocs); thy)) 
21151  1192 
#> Splitter.setup 
1193 
#> Clasimp.setup 

1194 
#> EqSubst.setup 

1195 
*} 

1196 

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

1198 
proof 

1199 
assume prem: "True \<Longrightarrow> PROP P" 

1200 
from prem [OF TrueI] show "PROP P" . 

1201 
next 

1202 
assume "PROP P" 

1203 
show "PROP P" . 

1204 
qed 

1205 

1206 
lemma ex_simps: 

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

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

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

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

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

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

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

1214 
by (iprover  blast)+ 

1215 

1216 
lemma all_simps: 

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

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

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

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

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

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

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

1224 
by (iprover  blast)+ 

15481  1225 

21671  1226 
lemmas [simp] = 
1227 
triv_forall_equality (*prunes params*) 

1228 
True_implies_equals (*prune asms `True'*) 

1229 
if_True 

1230 
if_False 

1231 
if_cancel 

1232 
if_eq_cancel 

1233 
imp_disjL 

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

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

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

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

21671  1239 
conj_assoc 
1240 
disj_assoc 

1241 
de_Morgan_conj 

1242 
de_Morgan_disj 

1243 
imp_disj1 

1244 
imp_disj2 

1245 
not_imp 

1246 
disj_not1 

1247 
not_all 

1248 
not_ex 

1249 
cases_simp 

1250 
the_eq_trivial 

1251 
the_sym_eq_trivial 

1252 
ex_simps 

1253 
all_simps 

1254 
simp_thms 

1255 

1256 
lemmas [cong] = imp_cong simp_implies_cong 

1257 
lemmas [split] = split_if 

20973  1258 

1259 
ML {* 

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

1260 
val HOL_ss = Simplifier.simpset_of (the_context ()); 
20973  1261 
*} 
1262 

20944  1263 
text {* Simplifies x assuming c and y assuming ~c *} 
1264 
lemma if_cong: 

1265 
assumes "b = c" 

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

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

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

1269 
unfolding if_def using prems by simp 

1270 

1271 
text {* Prevents simplification of x and y: 

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

1273 
lemma if_weak_cong [cong]: 

1274 
assumes "b = c" 

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

1276 
using prems by (rule arg_cong) 

1277 

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

1279 
lemma let_weak_cong: 

1280 
assumes "a = b" 

1281 
shows "(let x = a in t x) = (let x = b in t x)" 

1282 
using prems by (rule arg_cong) 

1283 

1284 
text {* To tidy up the result of a simproc. Only the RHS will be simplified. *} 

1285 
lemma eq_cong2: 

1286 
assumes "u = u'" 

1287 
shows "(t \<equiv> u) \<equiv> (t \<equiv> u')" 

1288 
using prems by simp 

1289 

1290 
lemma if_distrib: 

1291 
"f (if c then x else y) = (if c then f x else f y)" 

1292 
by simp 

1293 

1294 
text {* This lemma restricts the effect of the rewrite rule u=v to the lefthand 

21502  1295 
side of an equality. Used in @{text "{Integ,Real}/simproc.ML"} *} 
20944  1296 
lemma restrict_to_left: 
1297 
assumes "x = y" 

1298 
shows "(x = z) = (y = z)" 

1299 
using prems by simp 

1300 

17459  1301 

20944  1302 
subsubsection {* Generic cases and induction *} 
17459  1303 

20944  1304 
text {* Rule projections: *} 
18887  1305 

20944  1306 
ML {* 
1307 
structure ProjectRule = ProjectRuleFun 

1308 
(struct 

1309 
val conjunct1 = thm "conjunct1"; 

1310 
val conjunct2 = thm "conjunct2"; 

1311 
val mp = thm "mp"; 

1312 
end) 

17459  1313 
*} 
1314 

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

1315 
constdefs 
18457  1316 
induct_forall where "induct_forall P == \<forall>x. P x" 
1317 
induct_implies where "induct_implies A B == A \<longrightarrow> B" 

1318 
induct_equal where "induct_equal x y == x = y" 

1319 
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

1320 

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

1323 

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

1326 

11989  1327 
lemma induct_equal_eq: "(x == y) == Trueprop (induct_equal x y)" 
18457  1328 
by (unfold atomize_eq induct_equal_def) 
1329 

1330 
lemma induct_conj_eq: 

1331 
includes meta_conjunction_syntax 

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

1333 
by (unfold atomize_conj induct_conj_def) 

1334 

1335 
lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq 

1336 
lemmas induct_rulify [symmetric, standard] = induct_atomize 

1337 
lemmas induct_rulify_fallback = 

1338 
induct_forall_def induct_implies_def induct_equal_def induct_conj_def 

1339 

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

1340 

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

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

1344 

11989  1345 
lemma induct_implies_conj: "induct_implies C (induct_conj A B) = 
1346 
induct_conj (induct_implies C A) (induct_implies C B)" 

17589  1347 
by (unfold induct_implies_def induct_conj_def) iprover 
11989  1348 

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

1349 
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

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

1351 
assume r: "induct_conj A B ==> PROP C" and A B 
18457  1352 
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

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

1354 
assume r: "A ==> B ==> PROP C" and "induct_conj A B" 
18457  1355 
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

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

1357 

11989  1358 
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

1359 

11989  1360 
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

1361 

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

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

1363 

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

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

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

1366 
(struct 
15411  1367 
val cases_default = thm "case_split" 
1368 
val atomize = thms "induct_atomize" 

18457  1369 