author  haftmann 
Tue, 16 Sep 2008 09:21:22 +0200  
changeset 28227  77221ee0f7b9 
parent 28054  2b84d34c5d02 
child 28325  0b6b83ec8458 
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 
26957  9 
imports Pure 
23163  10 
uses 
23553  11 
("hologic.ML") 
23171  12 
"~~/src/Tools/IsaPlanner/zipper.ML" 
13 
"~~/src/Tools/IsaPlanner/isand.ML" 

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

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

23263  16 
"~~/src/Provers/project_rule.ML" 
17 
"~~/src/Provers/hypsubst.ML" 

18 
"~~/src/Provers/splitter.ML" 

23163  19 
"~~/src/Provers/classical.ML" 
20 
"~~/src/Provers/blast.ML" 

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

23263  22 
"~~/src/Provers/eqsubst.ML" 
23163  23 
"~~/src/Provers/quantifier1.ML" 
24 
("simpdata.ML") 

25741  25 
"~~/src/Tools/random_word.ML" 
26580
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset

26 
"~~/src/Tools/atomize_elim.ML" 
24901
d3cbf79769b9
added first version of userspace type system for class target
haftmann
parents:
24844
diff
changeset

27 
"~~/src/Tools/induct.ML" 
27326
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
27212
diff
changeset

28 
("~~/src/Tools/induct_tacs.ML") 
24280  29 
"~~/src/Tools/code/code_name.ML" 
30 
"~~/src/Tools/code/code_funcgr.ML" 

31 
"~~/src/Tools/code/code_thingol.ML" 

28054  32 
"~~/src/Tools/code/code_printer.ML" 
24280  33 
"~~/src/Tools/code/code_target.ML" 
28054  34 
"~~/src/Tools/code/code_ml.ML" 
35 
"~~/src/Tools/code/code_haskell.ML" 

24166  36 
"~~/src/Tools/nbe.ML" 
15131  37 
begin 
2260  38 

11750  39 
subsection {* Primitive logic *} 
40 

41 
subsubsection {* Core syntax *} 

2260  42 

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

44 
defaultsort type 
25494
b2484a7912ac
replaced typedecl interpretation by ObjectLogic.typedecl (based on base_sort);
wenzelm
parents:
25460
diff
changeset

45 
setup {* ObjectLogic.add_base_sort @{sort type} *} 
25460
b80087af2274
interpretation of typedecls: instantiation to class type
haftmann
parents:
25388
diff
changeset

46 

b80087af2274
interpretation of typedecls: instantiation to class type
haftmann
parents:
25388
diff
changeset

47 
arities 
b80087af2274
interpretation of typedecls: instantiation to class type
haftmann
parents:
25388
diff
changeset

48 
"fun" :: (type, type) type 
b80087af2274
interpretation of typedecls: instantiation to class type
haftmann
parents:
25388
diff
changeset

49 
itself :: (type) type 
b80087af2274
interpretation of typedecls: instantiation to class type
haftmann
parents:
25388
diff
changeset

50 

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

51 
global 
923  52 

7357  53 
typedecl bool 
923  54 

11750  55 
judgment 
56 
Trueprop :: "bool => prop" ("(_)" 5) 

923  57 

11750  58 
consts 
7357  59 
Not :: "bool => bool" ("~ _" [40] 40) 
60 
True :: bool 

61 
False :: bool 

3947  62 
arbitrary :: 'a 
923  63 

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

64 
The :: "('a => bool) => 'a" 
7357  65 
All :: "('a => bool) => bool" (binder "ALL " 10) 
66 
Ex :: "('a => bool) => bool" (binder "EX " 10) 

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

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

923  69 

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

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

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

923  74 

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

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

76 

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

2260  79 

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

80 

11750  81 
subsubsection {* Additional concrete syntax *} 
2260  82 

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

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

85 

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

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

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

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

89 

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

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

92 

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

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

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

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

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

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

99 

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

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

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

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

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

105 

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

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

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

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

109 

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

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

112 

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

113 

4868  114 
nonterminals 
923  115 
letbinds letbind 
116 
case_syn cases_syn 

117 

118 
syntax 

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

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

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

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

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

923  125 

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

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

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

129 
"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/  _") 
923  130 

131 
translations 

13764  132 
"THE x. P" == "The (%x. P)" 
923  133 
"_Let (_binds b bs) e" == "_Let b (_Let bs e)" 
1114  134 
"let x = a in e" == "Let a (%x. e)" 
923  135 

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

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

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

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

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

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

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

142 

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

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

146 
notation (xsymbols) 

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

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

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

2372  150 

21524  151 
notation (HTML output) 
152 
All (binder "\<forall>" 10) and 

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

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

6340  155 

21524  156 
notation (HOL) 
157 
All (binder "! " 10) and 

158 
Ex (binder "? " 10) and 

159 
Ex1 (binder "?! " 10) 

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

160 

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

161 

11750  162 
subsubsection {* Axioms and basic definitions *} 
2260  163 

7357  164 
axioms 
15380  165 
eq_reflection: "(x=y) ==> (x==y)" 
923  166 

15380  167 
refl: "t = (t::'a)" 
6289  168 

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

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

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

6289  173 

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

174 
the_eq_trivial: "(THE x. x = a) = (a::'a)" 
923  175 

15380  176 
impI: "(P ==> Q) ==> P>Q" 
177 
mp: "[ P>Q; P ] ==> Q" 

178 

179 

923  180 
defs 
7357  181 
True_def: "True == ((%x::bool. x) = (%x. x))" 
182 
All_def: "All(P) == (P = (%x. True))" 

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

183 
Ex_def: "Ex(P) == !Q. (!x. P x > Q) > Q" 
7357  184 
False_def: "False == (!P. P)" 
185 
not_def: "~ P == P>False" 

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

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

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

923  189 

7357  190 
axioms 
191 
iff: "(P>Q) > (Q>P) > (P=Q)" 

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

923  193 

194 
defs 

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

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

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

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

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

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

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

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

203 

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

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

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

206 

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

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

208 
undefined_fun: "undefined x = undefined" 
3320  209 

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

210 

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

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

212 

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

213 
class default = type + 
24901
d3cbf79769b9
added first version of userspace type system for class target
haftmann
parents:
24844
diff
changeset

214 
fixes default :: 'a 
4868  215 

22473  216 
class zero = type + 
25062  217 
fixes zero :: 'a ("0") 
20713
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset

218 

22473  219 
class one = type + 
25062  220 
fixes one :: 'a ("1") 
20713
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset

221 

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

222 
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

223 

22473  224 
class plus = type + 
25062  225 
fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 65) 
11750  226 

22473  227 
class minus = type + 
25762  228 
fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "" 65) 
229 

230 
class uminus = type + 

25062  231 
fixes uminus :: "'a \<Rightarrow> 'a" (" _" [81] 80) 
20590
bf92900995f8
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
haftmann
parents:
20453
diff
changeset

232 

22473  233 
class times = type + 
25062  234 
fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70) 
20590
bf92900995f8
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
haftmann
parents:
20453
diff
changeset

235 

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

237 
fixes inverse :: "'a \<Rightarrow> 'a" 
25062  238 
and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "'/" 70) 
21524  239 

23878  240 
class abs = type + 
241 
fixes abs :: "'a \<Rightarrow> 'a" 

25388  242 
begin 
23878  243 

21524  244 
notation (xsymbols) 
245 
abs ("\<bar>_\<bar>") 

25388  246 

21524  247 
notation (HTML output) 
248 
abs ("\<bar>_\<bar>") 

11750  249 

25388  250 
end 
251 

25062  252 
class sgn = type + 
253 
fixes sgn :: "'a \<Rightarrow> 'a" 

254 

23878  255 
class ord = type + 
24748  256 
fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
257 
and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 

23878  258 
begin 
259 

260 
notation 

261 
less_eq ("op <=") and 

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

263 
less ("op <") and 

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

265 

266 
notation (xsymbols) 

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

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

269 

270 
notation (HTML output) 

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

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

273 

25388  274 
abbreviation (input) 
275 
greater_eq (infix ">=" 50) where 

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

277 

24842  278 
notation (input) 
23878  279 
greater_eq (infix "\<ge>" 50) 
280 

25388  281 
abbreviation (input) 
282 
greater (infix ">" 50) where 

283 
"x > y \<equiv> y < x" 

284 

285 
end 

286 

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

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

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

289 
translations 
14690  290 
(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

291 

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

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

294 
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

295 
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

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

300 

20944  301 
subsection {* Fundamental rules *} 
302 

20973  303 
subsubsection {* Equality *} 
20944  304 

305 
text {* Thanks to Stephan Merz *} 

306 
lemma subst: 

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

308 
shows "P t" 

309 
proof  

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

311 
by (rule eq_reflection) 

312 
from p show ?thesis 

313 
by (unfold meta) 

314 
qed 

15411  315 

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

15411  318 

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

15411  321 

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

18457  323 
by (erule subst) 
15411  324 

20944  325 
lemma meta_eq_to_obj_eq: 
326 
assumes meq: "A == B" 

327 
shows "A = B" 

328 
by (unfold meq) (rule refl) 

15411  329 

21502  330 
text {* Useful with @{text erule} for proving equalities from known equalities. *} 
20944  331 
(* a = b 
15411  332 
  
333 
c = d *) 

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

335 
apply (rule trans) 

336 
apply (rule trans) 

337 
apply (rule sym) 

338 
apply assumption+ 

339 
done 

340 

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

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

342 

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

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

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

345 

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

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

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

348 

15411  349 

20944  350 
subsubsection {*Congruence rules for application*} 
15411  351 

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

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

354 
apply (erule subst) 

355 
apply (rule refl) 

356 
done 

357 

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

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

360 
apply (erule subst) 

361 
apply (rule refl) 

362 
done 

363 

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

366 
apply (rule refl) 

367 
done 

368 

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

371 
apply (rule refl) 

372 
done 

373 

374 

20944  375 
subsubsection {*Equality of booleans  iff*} 
15411  376 

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

15411  379 

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

18457  381 
by (erule ssubst) 
15411  382 

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

18457  384 
by (erule iffD2) 
15411  385 

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

388 

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

390 
by (drule sym) (rule rev_iffD2) 

15411  391 

392 
lemma iffE: 

393 
assumes major: "P=Q" 

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

15411  397 

398 

20944  399 
subsubsection {*True*} 
15411  400 

401 
lemma TrueI: "True" 

21504  402 
unfolding True_def by (rule refl) 
15411  403 

21504  404 
lemma eqTrueI: "P ==> P = True" 
18457  405 
by (iprover intro: iffI TrueI) 
15411  406 

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

15411  409 

410 

20944  411 
subsubsection {*Universal quantifier*} 
15411  412 

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

15411  415 

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

417 
apply (unfold All_def) 

418 
apply (rule eqTrueE) 

419 
apply (erule fun_cong) 

420 
done 

421 

422 
lemma allE: 

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

21504  424 
and minor: "P(x) ==> R" 
425 
shows R 

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

15411  427 

428 
lemma all_dupE: 

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

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

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

15411  433 

434 

21504  435 
subsubsection {* False *} 
436 

437 
text {* 

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

439 
logic before quantifiers! 

440 
*} 

15411  441 

442 
lemma FalseE: "False ==> P" 

21504  443 
apply (unfold False_def) 
444 
apply (erule spec) 

445 
done 

15411  446 

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

15411  449 

450 

21504  451 
subsubsection {* Negation *} 
15411  452 

453 
lemma notI: 

21504  454 
assumes "P ==> False" 
15411  455 
shows "~P" 
21504  456 
apply (unfold not_def) 
457 
apply (iprover intro: impI assms) 

458 
done 

15411  459 

460 
lemma False_not_True: "False ~= True" 

21504  461 
apply (rule notI) 
462 
apply (erule False_neq_True) 

463 
done 

15411  464 

465 
lemma True_not_False: "True ~= False" 

21504  466 
apply (rule notI) 
467 
apply (drule sym) 

468 
apply (erule False_neq_True) 

469 
done 

15411  470 

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

21504  472 
apply (unfold not_def) 
473 
apply (erule mp [THEN FalseE]) 

474 
apply assumption 

475 
done 

15411  476 

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

15411  479 

480 

20944  481 
subsubsection {*Implication*} 
15411  482 

483 
lemma impE: 

484 
assumes "P>Q" "P" "Q ==> R" 

485 
shows "R" 

23553  486 
by (iprover intro: assms mp) 
15411  487 

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

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

17589  490 
by (iprover intro: mp) 
15411  491 

492 
lemma contrapos_nn: 

493 
assumes major: "~Q" 

494 
and minor: "P==>Q" 

495 
shows "~P" 

17589  496 
by (iprover intro: notI minor major [THEN notE]) 
15411  497 

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

499 
lemma contrapos_pn: 

500 
assumes major: "Q" 

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

502 
shows "~P" 

17589  503 
by (iprover intro: notI minor major notE) 
15411  504 

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

21250  506 
by (erule contrapos_nn) (erule sym) 
507 

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

509 
by (erule subst, erule ssubst, assumption) 

15411  510 

511 
(*still used in HOLCF*) 

512 
lemma rev_contrapos: 

513 
assumes pq: "P ==> Q" 

514 
and nq: "~Q" 

515 
shows "~P" 

516 
apply (rule nq [THEN contrapos_nn]) 

517 
apply (erule pq) 

518 
done 

519 

20944  520 
subsubsection {*Existential quantifier*} 
15411  521 

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

523 
apply (unfold Ex_def) 

17589  524 
apply (iprover intro: allI allE impI mp) 
15411  525 
done 
526 

527 
lemma exE: 

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

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

530 
shows "Q" 

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

17589  532 
apply (iprover intro: impI [THEN allI] minor) 
15411  533 
done 
534 

535 

20944  536 
subsubsection {*Conjunction*} 
15411  537 

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

539 
apply (unfold and_def) 

17589  540 
apply (iprover intro: impI [THEN allI] mp) 
15411  541 
done 
542 

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

544 
apply (unfold and_def) 

17589  545 
apply (iprover intro: impI dest: spec mp) 
15411  546 
done 
547 

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

549 
apply (unfold and_def) 

17589  550 
apply (iprover intro: impI dest: spec mp) 
15411  551 
done 
552 

553 
lemma conjE: 

554 
assumes major: "P&Q" 

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

556 
shows "R" 

557 
apply (rule minor) 

558 
apply (rule major [THEN conjunct1]) 

559 
apply (rule major [THEN conjunct2]) 

560 
done 

561 

562 
lemma context_conjI: 

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

15411  565 

566 

20944  567 
subsubsection {*Disjunction*} 
15411  568 

569 
lemma disjI1: "P ==> PQ" 

570 
apply (unfold or_def) 

17589  571 
apply (iprover intro: allI impI mp) 
15411  572 
done 
573 

574 
lemma disjI2: "Q ==> PQ" 

575 
apply (unfold or_def) 

17589  576 
apply (iprover intro: allI impI mp) 
15411  577 
done 
578 

579 
lemma disjE: 

580 
assumes major: "PQ" 

581 
and minorP: "P ==> R" 

582 
and minorQ: "Q ==> R" 

583 
shows "R" 

17589  584 
by (iprover intro: minorP minorQ impI 
15411  585 
major [unfolded or_def, THEN spec, THEN mp, THEN mp]) 
586 

587 

20944  588 
subsubsection {*Classical logic*} 
15411  589 

590 
lemma classical: 

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

592 
shows "P" 

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

594 
apply assumption 

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

596 
apply (erule subst) 

597 
apply assumption 

598 
done 

599 

600 
lemmas ccontr = FalseE [THEN classical, standard] 

601 

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

603 
make elimination rules*) 

604 
lemma rev_notE: 

605 
assumes premp: "P" 

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

607 
shows "R" 

608 
apply (rule ccontr) 

609 
apply (erule notE [OF premnot premp]) 

610 
done 

611 

612 
(*Double negation law*) 

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

614 
apply (rule classical) 

615 
apply (erule notE) 

616 
apply assumption 

617 
done 

618 

619 
lemma contrapos_pp: 

620 
assumes p1: "Q" 

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

622 
shows "P" 

17589  623 
by (iprover intro: classical p1 p2 notE) 
15411  624 

625 

20944  626 
subsubsection {*Unique existence*} 
15411  627 

628 
lemma ex1I: 

23553  629 
assumes "P a" "!!x. P(x) ==> x=a" 
15411  630 
shows "EX! x. P(x)" 
23553  631 
by (unfold Ex1_def, iprover intro: assms exI conjI allI impI) 
15411  632 

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

634 
lemma ex_ex1I: 

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

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

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

17589  638 
by (iprover intro: ex_prem [THEN exE] ex1I eq) 
15411  639 

640 
lemma ex1E: 

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

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

643 
shows "R" 

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

645 
apply (erule conjE) 

17589  646 
apply (iprover intro: minor) 
15411  647 
done 
648 

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

650 
apply (erule ex1E) 

651 
apply (rule exI) 

652 
apply assumption 

653 
done 

654 

655 

20944  656 
subsubsection {*THE: definite description operator*} 
15411  657 

658 
lemma the_equality: 

659 
assumes prema: "P a" 

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

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

662 
apply (rule trans [OF _ the_eq_trivial]) 

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

664 
apply (rule ext) 

665 
apply (rule iffI) 

666 
apply (erule premx) 

667 
apply (erule ssubst, rule prema) 

668 
done 

669 

670 
lemma theI: 

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

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

23553  673 
by (iprover intro: assms the_equality [THEN ssubst]) 
15411  674 

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

676 
apply (erule ex1E) 

677 
apply (erule theI) 

678 
apply (erule allE) 

679 
apply (erule mp) 

680 
apply assumption 

681 
done 

682 

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

684 
lemma theI2: 

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

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

23553  687 
by (iprover intro: assms theI) 
15411  688 

24553  689 
lemma the1I2: assumes "EX! x. P x" "\<And>x. P x \<Longrightarrow> Q x" shows "Q (THE x. P x)" 
690 
by(iprover intro:assms(2) theI2[where P=P and Q=Q] ex1E[OF assms(1)] 

691 
elim:allE impE) 

692 

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

696 
apply (erule ex1E) 

697 
apply (erule all_dupE) 

698 
apply (drule mp) 

699 
apply assumption 

700 
apply (erule ssubst) 

701 
apply (erule allE) 

702 
apply (erule mp) 

703 
apply assumption 

704 
done 

705 

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

707 
apply (rule the_equality) 

708 
apply (rule refl) 

709 
apply (erule sym) 

710 
done 

711 

712 

20944  713 
subsubsection {*Classical intro rules for disjunction and existential quantifiers*} 
15411  714 

715 
lemma disjCI: 

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

717 
apply (rule classical) 

23553  718 
apply (iprover intro: assms disjI1 disjI2 notI elim: notE) 
15411  719 
done 
720 

721 
lemma excluded_middle: "~P  P" 

17589  722 
by (iprover intro: disjCI) 
15411  723 

20944  724 
text {* 
725 
case distinction as a natural deduction rule. 

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

727 
*} 

27126
3ede9103de8e
eliminated obsolete case_split_thm  use case_split;
wenzelm
parents:
27107
diff
changeset

728 
lemma case_split [case_names True False]: 
15411  729 
assumes prem1: "P ==> Q" 
730 
and prem2: "~P ==> Q" 

731 
shows "Q" 

732 
apply (rule excluded_middle [THEN disjE]) 

733 
apply (erule prem2) 

734 
apply (erule prem1) 

735 
done 

27126
3ede9103de8e
eliminated obsolete case_split_thm  use case_split;
wenzelm
parents:
27107
diff
changeset

736 

15411  737 
(*Classical implies (>) elimination. *) 
738 
lemma impCE: 

739 
assumes major: "P>Q" 

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

741 
shows "R" 

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

17589  743 
apply (iprover intro: minor major [THEN mp])+ 
15411  744 
done 
745 

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

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

748 
default: would break old proofs.*) 

749 
lemma impCE': 

750 
assumes major: "P>Q" 

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

752 
shows "R" 

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

17589  754 
apply (iprover intro: minor major [THEN mp])+ 
15411  755 
done 
756 

757 
(*Classical <> elimination. *) 

758 
lemma iffCE: 

759 
assumes major: "P=Q" 

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

761 
shows "R" 

762 
apply (rule major [THEN iffE]) 

17589  763 
apply (iprover intro: minor elim: impCE notE) 
15411  764 
done 
765 

766 
lemma exCI: 

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

768 
shows "EX x. P(x)" 

769 
apply (rule ccontr) 

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

773 

12386  774 
subsubsection {* Intuitionistic Reasoning *} 
775 

776 
lemma impE': 

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

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

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

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

780 
shows R 
12386  781 
proof  
782 
from 3 and 1 have P . 

783 
with 1 have Q by (rule impE) 

784 
with 2 show R . 

785 
qed 

786 

787 
lemma allE': 

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

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

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

790 
shows Q 
12386  791 
proof  
792 
from 1 have "P x" by (rule spec) 

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

794 
qed 

795 

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

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

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

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

799 
shows R 
12386  800 
proof  
801 
from 2 and 1 have P . 

802 
with 1 show R by (rule notE) 

803 
qed 

804 

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

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

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

807 

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

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

811 
and [Pure.intro] = exI disjI2 disjI1 

12386  812 

813 
lemmas [trans] = trans 

814 
and [sym] = sym not_sym 

15801  815 
and [Pure.elim?] = iffD1 iffD2 impE 
11750  816 

23553  817 
use "hologic.ML" 
818 

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

819 

11750  820 
subsubsection {* Atomizing metalevel connectives *} 
821 

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

12003  823 
proof 
9488  824 
assume "!!x. P x" 
23389  825 
then show "ALL x. P x" .. 
9488  826 
next 
827 
assume "ALL x. P x" 

23553  828 
then show "!!x. P x" by (rule allE) 
9488  829 
qed 
830 

11750  831 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
12003  832 
proof 
9488  833 
assume r: "A ==> B" 
10383  834 
show "A > B" by (rule impI) (rule r) 
9488  835 
next 
836 
assume "A > B" and A 

23553  837 
then show B by (rule mp) 
9488  838 
qed 
839 

14749  840 
lemma atomize_not: "(A ==> False) == Trueprop (~A)" 
841 
proof 

842 
assume r: "A ==> False" 

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

844 
next 

845 
assume "~A" and A 

23553  846 
then show False by (rule notE) 
14749  847 
qed 
848 

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

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

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

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

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

857 

12023  858 
lemma atomize_conj [atomize]: 
19121  859 
includes meta_conjunction_syntax 
860 
shows "(A && B) == Trueprop (A & B)" 

12003  861 
proof 
19121  862 
assume conj: "A && B" 
863 
show "A & B" 

864 
proof (rule conjI) 

865 
from conj show A by (rule conjunctionD1) 

866 
from conj show B by (rule conjunctionD2) 

867 
qed 

11953  868 
next 
19121  869 
assume conj: "A & B" 
870 
show "A && B" 

871 
proof  

872 
from conj show A .. 

873 
from conj show B .. 

11953  874 
qed 
875 
qed 

876 

12386  877 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
18832  878 
and [symmetric, defn] = atomize_all atomize_imp atomize_eq 
12386  879 

11750  880 

26580
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset

881 
subsubsection {* Atomizing elimination rules *} 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset

882 

c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset

883 
setup AtomizeElim.setup 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset

884 

c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset

885 
lemma atomize_exL[atomize_elim]: "(!!x. P x ==> Q) == ((EX x. P x) ==> Q)" 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset

886 
by rule iprover+ 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset

887 

c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset

888 
lemma atomize_conjL[atomize_elim]: "(A ==> B ==> C) == (A & B ==> C)" 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset

889 
by rule iprover+ 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset

890 

c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset

891 
lemma atomize_disjL[atomize_elim]: "((A ==> C) ==> (B ==> C) ==> C) == ((A  B ==> C) ==> C)" 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset

892 
by rule iprover+ 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset

893 

c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset

894 
lemma atomize_elimL[atomize_elim]: "(!!B. (A ==> B) ==> B) == Trueprop A" .. 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset

895 

c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset

896 

20944  897 
subsection {* Package setup *} 
898 

11750  899 
subsubsection {* Classical Reasoner setup *} 
9529  900 

26411  901 
lemma imp_elim: "P > Q ==> (~ R ==> P) ==> (Q ==> R) ==> R" 
902 
by (rule classical) iprover 

903 

904 
lemma swap: "~ P ==> (~ R ==> P) ==> R" 

905 
by (rule classical) iprover 

906 

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

909 

21151  910 
ML {* 
911 
structure Hypsubst = HypsubstFun( 

912 
struct 

913 
structure Simplifier = Simplifier 

21218  914 
val dest_eq = HOLogic.dest_eq 
21151  915 
val dest_Trueprop = HOLogic.dest_Trueprop 
916 
val dest_imp = HOLogic.dest_imp 

26411  917 
val eq_reflection = @{thm eq_reflection} 
918 
val rev_eq_reflection = @{thm meta_eq_to_obj_eq} 

919 
val imp_intr = @{thm impI} 

920 
val rev_mp = @{thm rev_mp} 

921 
val subst = @{thm subst} 

922 
val sym = @{thm sym} 

22129  923 
val thin_refl = @{thm thin_refl}; 
27572
67cd6ed76446
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents:
27338
diff
changeset

924 
val prop_subst = @{lemma "PROP P t ==> PROP prop (x = t ==> PROP P x)" 
67cd6ed76446
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents:
27338
diff
changeset

925 
by (unfold prop_def) (drule eq_reflection, unfold)} 
21151  926 
end); 
21671  927 
open Hypsubst; 
21151  928 

929 
structure Classical = ClassicalFun( 

930 
struct 

26411  931 
val imp_elim = @{thm imp_elim} 
932 
val not_elim = @{thm notE} 

933 
val swap = @{thm swap} 

934 
val classical = @{thm classical} 

21151  935 
val sizef = Drule.size_of_thm 
936 
val hyp_subst_tacs = [Hypsubst.hyp_subst_tac] 

937 
end); 

938 

939 
structure BasicClassical: BASIC_CLASSICAL = Classical; 

21671  940 
open BasicClassical; 
22129  941 

27338  942 
ML_Antiquote.value "claset" 
943 
(Scan.succeed "Classical.local_claset_of (ML_Context.the_local_context ())"); 

24035  944 

945 
structure ResAtpset = NamedThmsFun(val name = "atp" val description = "ATP rules"); 

24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24280
diff
changeset

946 

7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24280
diff
changeset

947 
structure ResBlacklist = NamedThmsFun(val name = "noatp" val description = "Theorems blacklisted for ATP"); 
21151  948 
*} 
949 

25388  950 
text {*ResBlacklist holds theorems blacklisted to sledgehammer. 
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24280
diff
changeset

951 
These theorems typically produce clauses that are prolific (match too many equality or 
25388  952 
membership literals) and relate to seldomused facts. Some duplicate other rules.*} 
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24280
diff
changeset

953 

21009  954 
setup {* 
955 
let 

956 
(*prevent substitution on bool*) 

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

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

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

960 
in 

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

963 
#> Classical.setup 

964 
#> ResAtpset.setup 

24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24280
diff
changeset

965 
#> ResBlacklist.setup 
21009  966 
end 
967 
*} 

968 

969 
declare iffI [intro!] 

970 
and notI [intro!] 

971 
and impI [intro!] 

972 
and disjCI [intro!] 

973 
and conjI [intro!] 

974 
and TrueI [intro!] 

975 
and refl [intro!] 

976 

977 
declare iffCE [elim!] 

978 
and FalseE [elim!] 

979 
and impCE [elim!] 

980 
and disjE [elim!] 

981 
and conjE [elim!] 

982 
and conjE [elim!] 

983 

984 
declare ex_ex1I [intro!] 

985 
and allI [intro!] 

986 
and the_equality [intro] 

987 
and exI [intro] 

988 

989 
declare exE [elim!] 

990 
allE [elim] 

991 

22377  992 
ML {* val HOL_cs = @{claset} *} 
19162  993 

20223  994 
lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P" 
995 
apply (erule swap) 

996 
apply (erule (1) meta_mp) 

997 
done 

10383  998 

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

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

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

1001 

12386  1002 
lemmas [intro?] = ext 
1003 
and [elim?] = ex1_implies_ex 

11977  1004 

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

1009 
shows R 

1010 
apply (rule ex1E [OF major]) 

1011 
apply (rule prem) 

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

1014 
apply iprover 

1015 
done 

20944  1016 

21151  1017 
ML {* 
25388  1018 
structure Blast = BlastFun 
1019 
( 

21151  1020 
type claset = Classical.claset 
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22481
diff
changeset

1021 
val equality_name = @{const_name "op ="} 
22993  1022 
val not_name = @{const_name Not} 
26411  1023 
val notE = @{thm notE} 
1024 
val ccontr = @{thm ccontr} 

21151  1025 
val contr_tac = Classical.contr_tac 
1026 
val dup_intr = Classical.dup_intr 

1027 
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac 

21671  1028 
val claset = Classical.claset 
21151  1029 
val rep_cs = Classical.rep_cs 
1030 
val cla_modifiers = Classical.cla_modifiers 

1031 
val cla_meth' = Classical.cla_meth' 

25388  1032 
); 
21671  1033 
val Blast_tac = Blast.Blast_tac; 
1034 
val blast_tac = Blast.blast_tac; 

20944  1035 
*} 
1036 

21151  1037 
setup Blast.setup 
1038 

20944  1039 

1040 
subsubsection {* Simplifier *} 

12281  1041 

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

1043 

1044 
lemma simp_thms: 

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

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

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

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

1049 
"(P  ~P) = True" "(~P  P) = True" 
12281  1050 
"(x = x) = True" 
20944  1051 
and not_True_eq_False: "(\<not> True) = False" 
1052 
and not_False_eq_True: "(\<not> False) = True" 

1053 
and 

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

1054 
"(~P) ~= P" "P ~= (~P)" 
20944  1055 
"(True=P) = P" 
1056 
and eq_True: "(P = True) = P" 

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

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

1059 
and 

12281  1060 
"(True > P) = P" "(False > P) = True" 
1061 
"(P > True) = True" "(P > P) = True" 

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

1063 
"(P & True) = P" "(True & P) = P" 

1064 
"(P & False) = False" "(False & P) = False" 

1065 
"(P & P) = P" "(P & (P & Q)) = (P & Q)" 

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

1067 
"(P  True) = True" "(True  P) = True" 

1068 
"(P  False) = P" "(False  P) = P" 

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

1069 
"(P  P) = P" "(P  (P  Q)) = (P  Q)" and 
12281  1070 
"(ALL x. P) = P" "(EX x. P) = P" "EX x. x=t" "EX x. t=x" 
1071 
 {* needed for the onepointrule quantifier simplification procs *} 

1072 
 {* essential for termination!! *} and 

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

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

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

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

1076 
"!!P. (ALL x. t=x > P(x)) = P(t)" 
17589  1077 
by (blast, blast, blast, blast, blast, iprover+) 
13421  1078 

14201  1079 
lemma disj_absorb: "(A  A) = A" 
1080 
by blast 

1081 

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

1083 
by blast 

1084 

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

1086 
by blast 

1087 

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

1089 
by blast 

1090 

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

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

1093 
and eq_left_commute: "(P=(Q=R)) = (Q=(P=R))" 
17589  1094 
and eq_assoc: "((P=Q)=R) = (P=(Q=R))" by (iprover, blast+) 
1095 
lemma neq_commute: "(a~=b) = (b~=a)" by iprover 

12281  1096 

1097 
lemma conj_comms: 

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

1098 
shows conj_commute: "(P&Q) = (Q&P)" 
17589  1099 
and conj_left_commute: "(P&(Q&R)) = (Q&(P&R))" by iprover+ 
1100 
lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by iprover 

12281  1101 

19174  1102 
lemmas conj_ac = conj_commute conj_left_commute conj_assoc 
1103 

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

1105 
shows disj_commute: "(PQ) = (QP)" 
17589  1106 
and disj_left_commute: "(P(QR)) = (Q(PR))" by iprover+ 
1107 
lemma disj_assoc: "((PQ)R) = (P(QR))" by iprover 

12281  1108 

19174  1109 
lemmas disj_ac = disj_commute disj_left_commute disj_assoc 
1110 

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

12281  1113 

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

12281  1116 

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

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

12281  1120 

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

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

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

1124 

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

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

1127 

21151  1128 
lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P > Q) = (P' > Q'))" 
1129 
by iprover 

1130 

17589  1131 
lemma de_Morgan_disj: "(~(P  Q)) = (~P & ~Q)" by iprover 
12281  1132 
lemma de_Morgan_conj: "(~(P & Q)) = (~P  ~Q)" by blast 
1133 
lemma not_imp: "(~(P > Q)) = (P & ~Q)" by blast 

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

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

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

1137 
by blast 

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

1139 

17589  1140 
lemma iff_conv_conj_imp: "(P = Q) = ((P > Q) & (Q > P))" by iprover 
12281  1141 

1142 

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

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

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

1146 
by blast 

1147 

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

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

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

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

24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24280
diff
changeset

1154 
declare All_def [noatp] 
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24280
diff
changeset

1155 

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

12281  1158 

1159 
text {* 

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

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

1162 

1163 
lemma conj_cong: 

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

17589  1165 
by iprover 
12281  1166 

1167 
lemma rev_conj_cong: 

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

17589  1169 
by iprover 
12281  1170 

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

1172 

1173 
lemma disj_cong: 

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

1175 
by blast 

1176 

1177 

1178 
text {* \medskip ifthenelse rules *} 

1179 

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

1181 
by (unfold if_def) blast 

1182 

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

1184 
by (unfold if_def) blast 

1185 

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

1187 
by (unfold if_def) blast 

1188 

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

1190 
by (unfold if_def) blast 

1191 

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

1193 
apply (rule case_split [of Q]) 

15481  1194 
apply (simplesubst if_P) 
1195 
prefer 3 apply (simplesubst if_not_P, blast+) 

12281  1196 
done 
1197 

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

15481  1199 
by (simplesubst split_if, blast) 
12281  1200 

24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24280
diff
changeset

1201 
lemmas if_splits [noatp] = split_if split_if_asm 
12281  1202 

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

15481  1204 
by (simplesubst split_if, blast) 
12281  1205 

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

15481  1207 
by (simplesubst split_if, blast) 
12281  1208 

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

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

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

19796  1214 
 {* And this form is useful for expanding @{text "if"}s on the LEFT. *} 
15481  1215 
apply (simplesubst split_if, blast) 
12281  1216 
done 
1217 

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

12281  1220 

15423  1221 
text {* \medskip let rules for simproc *} 
1222 

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

1224 
by (unfold Let_def) 

1225 

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

1227 
by (unfold Let_def) 

1228 

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

1229 
text {* 
16999  1230 
The following copy of the implication operator is useful for 
1231 
finetuning congruence rules. It instructs the simplifier to simplify 

1232 
its premise. 

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

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

1234 

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

25966  1237 
[code func del]: "simp_implies \<equiv> op ==>" 
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1238 

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

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

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

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

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

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

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

1246 

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

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

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

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

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

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

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

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

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

1256 

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

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

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

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

1260 
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

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

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

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

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

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

1267 
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

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

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

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

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

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

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

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

1276 

20944  1277 
lemma uncurry: 
1278 
assumes "P \<longrightarrow> Q \<longrightarrow> R" 

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

23553  1280 
using assms by blast 
20944  1281 

1282 
lemma iff_allI: 

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

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

23553  1285 
using assms by blast 
20944  1286 

1287 
lemma iff_exI: 

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

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

23553  1290 
using assms by blast 
20944  1291 

1292 
lemma all_comm: 

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

1294 
by blast 

1295 

1296 
lemma ex_comm: 

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

1298 
by blast 

1299 

9869  1300 
use "simpdata.ML" 
21671  1301 
ML {* open Simpdata *} 
1302 

21151  1303 
setup {* 
1304 
Simplifier.method_setup Splitter.split_modifiers 

26496
49ae9456eba9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26411
diff
changeset

1305 
#> Simplifier.map_simpset (K Simpdata.simpset_simprocs) 
21151  1306 
#> Splitter.setup 
26496
49ae9456eba9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26411
diff
changeset

1307 
#> clasimp_setup 
21151  1308 
#> EqSubst.setup 
1309 
*} 

1310 

24035  1311 
text {* Simproc for proving @{text "(y = x) == False"} from premise @{text "~(x = y)"}: *} 
1312 

1313 
simproc_setup neq ("x = y") = {* fn _ => 

1314 
let 

1315 
val neq_to_EQ_False = @{thm not_sym} RS @{thm Eq_FalseI}; 

1316 
fun is_neq eq lhs rhs thm = 

1317 
(case Thm.prop_of thm of 

1318 
_ $ (Not $ (eq' $ l' $ r')) => 

1319 
Not = HOLogic.Not andalso eq' = eq andalso 

1320 
r' aconv lhs andalso l' aconv rhs 

1321 
 _ => false); 

1322 
fun proc ss ct = 

1323 
(case Thm.term_of ct of 

1324 
eq $ lhs $ rhs => 

1325 
(case find_first (is_neq eq lhs rhs) (Simplifier.prems_of_ss ss) of 

1326 
SOME thm => SOME (thm RS neq_to_EQ_False) 

1327 
 NONE => NONE) 

1328 
 _ => NONE); 

1329 
in proc end; 

1330 
*} 

1331 

1332 
simproc_setup let_simp ("Let x f") = {* 

1333 
let 

1334 
val (f_Let_unfold, x_Let_unfold) = 

1335 
let val [(_$(f$x)$_)] = prems_of @{thm Let_unfold} 

1336 
in (cterm_of @{theory} f, cterm_of @{theory} x) end 

1337 
val (f_Let_folded, x_Let_folded) = 

1338 
let val [(_$(f$x)$_)] = prems_of @{thm Let_folded} 

1339 
in (cterm_of @{theory} f, cterm_of @{theory} x) end; 

1340 
val g_Let_folded = 

1341 
let val [(_$_$(g$_))] = prems_of @{thm Let_folded} in cterm_of @{theory} g end; 

1342 

1343 
fun proc _ ss ct = 

1344 
let 

1345 
val ctxt = Simplifier.the_context ss; 

1346 
val thy = ProofContext.theory_of ctxt; 

1347 
val t = Thm.term_of ct; 

1348 
val ([t'], ctxt') = Variable.import_terms false [t] ctxt; 

1349 
in Option.map (hd o Variable.export ctxt' ctxt o single) 

1350 
(case t' of Const ("Let",_) $ x $ f => (* x and f are already in normal form *) 

1351 
if is_Free x orelse is_Bound x orelse is_Const x 

1352 
then SOME @{thm Let_def} 

1353 
else 

1354 
let 

1355 
val n = case f of (Abs (x,_,_)) => x  _ => "x"; 

1356 
val cx = cterm_of thy x; 

1357 
val {T=xT,...} = rep_cterm cx; 

1358 
val cf = cterm_of thy f; 

1359 
val fx_g = Simplifier.rewrite ss (Thm.capply cf cx); 

1360 
val (_$_$g) = prop_of fx_g; 

1361 
val g' = abstract_over (x,g); 

1362 
in (if (g aconv g') 

1363 
then 

1364 
let 
