author  wenzelm 
Wed, 26 Mar 2008 22:40:01 +0100  
changeset 26411  cd74690f3bfb 
parent 25966  74f6817870f9 
child 26496  49ae9456eba9 
permissions  rwrr 
923  1 
(* Title: HOL/HOL.thy 
2 
ID: $Id$ 

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

923  5 

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

15131  8 
theory HOL 
15140  9 
imports CPure 
23163  10 
uses 
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" 
24901
d3cbf79769b9
added first version of userspace type system for class target
haftmann
parents:
24844
diff
changeset

26 
"~~/src/Tools/induct.ML" 
24280  27 
"~~/src/Tools/code/code_name.ML" 
28 
"~~/src/Tools/code/code_funcgr.ML" 

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

30 
"~~/src/Tools/code/code_target.ML" 

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

24166  32 
"~~/src/Tools/nbe.ML" 
15131  33 
begin 
2260  34 

11750  35 
subsection {* Primitive logic *} 
36 

37 
subsubsection {* Core syntax *} 

2260  38 

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

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

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

42 

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

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

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

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

46 

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

47 
global 
923  48 

7357  49 
typedecl bool 
923  50 

11750  51 
judgment 
52 
Trueprop :: "bool => prop" ("(_)" 5) 

923  53 

11750  54 
consts 
7357  55 
Not :: "bool => bool" ("~ _" [40] 40) 
56 
True :: bool 

57 
False :: bool 

3947  58 
arbitrary :: 'a 
923  59 

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

60 
The :: "('a => bool) => 'a" 
7357  61 
All :: "('a => bool) => bool" (binder "ALL " 10) 
62 
Ex :: "('a => bool) => bool" (binder "EX " 10) 

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

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

923  65 

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

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

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

923  70 

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

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

72 

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

2260  75 

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

76 

11750  77 
subsubsection {* Additional concrete syntax *} 
2260  78 

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

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

81 

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

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

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

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

85 

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

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

88 

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

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

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

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

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

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

95 

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

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

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

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

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

101 

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

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

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

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

105 

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

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

108 

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

109 

4868  110 
nonterminals 
923  111 
letbinds letbind 
112 
case_syn cases_syn 

113 

114 
syntax 

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

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

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

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

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

923  121 

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

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

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

125 
"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/  _") 
923  126 

127 
translations 

13764  128 
"THE x. P" == "The (%x. P)" 
923  129 
"_Let (_binds b bs) e" == "_Let b (_Let bs e)" 
1114  130 
"let x = a in e" == "Let a (%x. e)" 
923  131 

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

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

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

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

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

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

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

138 

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

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

142 
notation (xsymbols) 

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

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

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

2372  146 

21524  147 
notation (HTML output) 
148 
All (binder "\<forall>" 10) and 

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

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

6340  151 

21524  152 
notation (HOL) 
153 
All (binder "! " 10) and 

154 
Ex (binder "? " 10) and 

155 
Ex1 (binder "?! " 10) 

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

156 

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

157 

11750  158 
subsubsection {* Axioms and basic definitions *} 
2260  159 

7357  160 
axioms 
15380  161 
eq_reflection: "(x=y) ==> (x==y)" 
923  162 

15380  163 
refl: "t = (t::'a)" 
6289  164 

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

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

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

6289  169 

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

170 
the_eq_trivial: "(THE x. x = a) = (a::'a)" 
923  171 

15380  172 
impI: "(P ==> Q) ==> P>Q" 
173 
mp: "[ P>Q; P ] ==> Q" 

174 

175 

923  176 
defs 
7357  177 
True_def: "True == ((%x::bool. x) = (%x. x))" 
178 
All_def: "All(P) == (P = (%x. True))" 

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

179 
Ex_def: "Ex(P) == !Q. (!x. P x > Q) > Q" 
7357  180 
False_def: "False == (!P. P)" 
181 
not_def: "~ P == P>False" 

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

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

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

923  185 

7357  186 
axioms 
187 
iff: "(P>Q) > (Q>P) > (P=Q)" 

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

923  189 

190 
defs 

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

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

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

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

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

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

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

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

199 

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

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

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

202 

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

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

204 
undefined_fun: "undefined x = undefined" 
3320  205 

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

206 

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

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

208 

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

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

210 
fixes default :: 'a 
4868  211 

22473  212 
class zero = type + 
25062  213 
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

214 

22473  215 
class one = type + 
25062  216 
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

217 

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

218 
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

219 

22473  220 
class plus = type + 
25062  221 
fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 65) 
11750  222 

22473  223 
class minus = type + 
25762  224 
fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "" 65) 
225 

226 
class uminus = type + 

25062  227 
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

228 

22473  229 
class times = type + 
25062  230 
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

231 

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

233 
fixes inverse :: "'a \<Rightarrow> 'a" 
25062  234 
and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "'/" 70) 
21524  235 

23878  236 
class abs = type + 
237 
fixes abs :: "'a \<Rightarrow> 'a" 

25388  238 
begin 
23878  239 

21524  240 
notation (xsymbols) 
241 
abs ("\<bar>_\<bar>") 

25388  242 

21524  243 
notation (HTML output) 
244 
abs ("\<bar>_\<bar>") 

11750  245 

25388  246 
end 
247 

25062  248 
class sgn = type + 
249 
fixes sgn :: "'a \<Rightarrow> 'a" 

250 

23878  251 
class ord = type + 
24748  252 
fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
253 
and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 

23878  254 
begin 
255 

256 
notation 

257 
less_eq ("op <=") and 

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

259 
less ("op <") and 

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

261 

262 
notation (xsymbols) 

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

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

265 

266 
notation (HTML output) 

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

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

269 

25388  270 
abbreviation (input) 
271 
greater_eq (infix ">=" 50) where 

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

273 

24842  274 
notation (input) 
23878  275 
greater_eq (infix "\<ge>" 50) 
276 

25388  277 
abbreviation (input) 
278 
greater (infix ">" 50) where 

279 
"x > y \<equiv> y < x" 

280 

281 
definition 

282 
Least :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "LEAST " 10) where 

283 
"Least P == (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> less_eq x y))" 

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 
*} 

15411  728 
lemma case_split_thm: 
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 

20944  736 
lemmas case_split = case_split_thm [case_names True False] 
15411  737 

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

739 
lemma impCE: 

740 
assumes major: "P>Q" 

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

742 
shows "R" 

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

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

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

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

749 
default: would break old proofs.*) 

750 
lemma impCE': 

751 
assumes major: "P>Q" 

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

753 
shows "R" 

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

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

758 
(*Classical <> elimination. *) 

759 
lemma iffCE: 

760 
assumes major: "P=Q" 

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

762 
shows "R" 

763 
apply (rule major [THEN iffE]) 

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

767 
lemma exCI: 

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

769 
shows "EX x. P(x)" 

770 
apply (rule ccontr) 

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

774 

12386  775 
subsubsection {* Intuitionistic Reasoning *} 
776 

777 
lemma impE': 

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

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

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

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

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

784 
with 1 have Q by (rule impE) 

785 
with 2 show R . 

786 
qed 

787 

788 
lemma allE': 

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

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

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

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

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

795 
qed 

796 

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

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

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

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

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

803 
with 1 show R by (rule notE) 

804 
qed 

805 

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

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

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

808 

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

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

812 
and [Pure.intro] = exI disjI2 disjI1 

12386  813 

814 
lemmas [trans] = trans 

815 
and [sym] = sym not_sym 

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

23553  818 
use "hologic.ML" 
819 

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

820 

11750  821 
subsubsection {* Atomizing metalevel connectives *} 
822 

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

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

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

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

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

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

843 
assume r: "A ==> False" 

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

845 
next 

846 
assume "~A" and A 

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

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

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

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

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

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

858 

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

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

865 
proof (rule conjI) 

866 
from conj show A by (rule conjunctionD1) 

867 
from conj show B by (rule conjunctionD2) 

868 
qed 

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

872 
proof  

873 
from conj show A .. 

874 
from conj show B .. 

11953  875 
qed 
876 
qed 

877 

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

11750  881 

20944  882 
subsection {* Package setup *} 
883 

11750  884 
subsubsection {* Classical Reasoner setup *} 
9529  885 

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

888 

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

890 
by (rule classical) iprover 

891 

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

894 

21151  895 
ML {* 
896 
structure Hypsubst = HypsubstFun( 

897 
struct 

898 
structure Simplifier = Simplifier 

21218  899 
val dest_eq = HOLogic.dest_eq 
21151  900 
val dest_Trueprop = HOLogic.dest_Trueprop 
901 
val dest_imp = HOLogic.dest_imp 

26411  902 
val eq_reflection = @{thm eq_reflection} 
903 
val rev_eq_reflection = @{thm meta_eq_to_obj_eq} 

904 
val imp_intr = @{thm impI} 

905 
val rev_mp = @{thm rev_mp} 

906 
val subst = @{thm subst} 

907 
val sym = @{thm sym} 

22129  908 
val thin_refl = @{thm thin_refl}; 
21151  909 
end); 
21671  910 
open Hypsubst; 
21151  911 

912 
structure Classical = ClassicalFun( 

913 
struct 

26411  914 
val imp_elim = @{thm imp_elim} 
915 
val not_elim = @{thm notE} 

916 
val swap = @{thm swap} 

917 
val classical = @{thm classical} 

21151  918 
val sizef = Drule.size_of_thm 
919 
val hyp_subst_tacs = [Hypsubst.hyp_subst_tac] 

920 
end); 

921 

922 
structure BasicClassical: BASIC_CLASSICAL = Classical; 

21671  923 
open BasicClassical; 
22129  924 

925 
ML_Context.value_antiq "claset" 

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

24035  927 

928 
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

929 

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

930 
structure ResBlacklist = NamedThmsFun(val name = "noatp" val description = "Theorems blacklisted for ATP"); 
21151  931 
*} 
932 

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

934 
These theorems typically produce clauses that are prolific (match too many equality or 
25388  935 
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

936 

21009  937 
setup {* 
938 
let 

939 
(*prevent substitution on bool*) 

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

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

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

943 
in 

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

946 
#> Classical.setup 

947 
#> ResAtpset.setup 

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

948 
#> ResBlacklist.setup 
21009  949 
end 
950 
*} 

951 

952 
declare iffI [intro!] 

953 
and notI [intro!] 

954 
and impI [intro!] 

955 
and disjCI [intro!] 

956 
and conjI [intro!] 

957 
and TrueI [intro!] 

958 
and refl [intro!] 

959 

960 
declare iffCE [elim!] 

961 
and FalseE [elim!] 

962 
and impCE [elim!] 

963 
and disjE [elim!] 

964 
and conjE [elim!] 

965 
and conjE [elim!] 

966 

967 
declare ex_ex1I [intro!] 

968 
and allI [intro!] 

969 
and the_equality [intro] 

970 
and exI [intro] 

971 

972 
declare exE [elim!] 

973 
allE [elim] 

974 

22377  975 
ML {* val HOL_cs = @{claset} *} 
19162  976 

20223  977 
lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P" 
978 
apply (erule swap) 

979 
apply (erule (1) meta_mp) 

980 
done 

10383  981 

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

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

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

984 

12386  985 
lemmas [intro?] = ext 
986 
and [elim?] = ex1_implies_ex 

11977  987 

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

992 
shows R 

993 
apply (rule ex1E [OF major]) 

994 
apply (rule prem) 

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

997 
apply iprover 

998 
done 

20944  999 

21151  1000 
ML {* 
25388  1001 
structure Blast = BlastFun 
1002 
( 

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

1004 
val equality_name = @{const_name "op ="} 
22993  1005 
val not_name = @{const_name Not} 
26411  1006 
val notE = @{thm notE} 
1007 
val ccontr = @{thm ccontr} 

21151  1008 
val contr_tac = Classical.contr_tac 
1009 
val dup_intr = Classical.dup_intr 

1010 
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac 

21671  1011 
val claset = Classical.claset 
21151  1012 
val rep_cs = Classical.rep_cs 
1013 
val cla_modifiers = Classical.cla_modifiers 

1014 
val cla_meth' = Classical.cla_meth' 

25388  1015 
); 
21671  1016 
val Blast_tac = Blast.Blast_tac; 
1017 
val blast_tac = Blast.blast_tac; 

20944  1018 
*} 
1019 

21151  1020 
setup Blast.setup 
1021 

20944  1022 

1023 
subsubsection {* Simplifier *} 

12281  1024 

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

1026 

1027 
lemma simp_thms: 

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

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

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

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

1032 
"(P  ~P) = True" "(~P  P) = True" 
12281  1033 
"(x = x) = True" 
20944  1034 
and not_True_eq_False: "(\<not> True) = False" 
1035 
and not_False_eq_True: "(\<not> False) = True" 

1036 
and 

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

1037 
"(~P) ~= P" "P ~= (~P)" 
20944  1038 
"(True=P) = P" 
1039 
and eq_True: "(P = True) = P" 

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

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

1042 
and 

12281  1043 
"(True > P) = P" "(False > P) = True" 
1044 
"(P > True) = True" "(P > P) = True" 

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

1046 
"(P & True) = P" "(True & P) = P" 

1047 
"(P & False) = False" "(False & P) = False" 

1048 
"(P & P) = P" "(P & (P & Q)) = (P & Q)" 

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

1050 
"(P  True) = True" "(True  P) = True" 

1051 
"(P  False) = P" "(False  P) = P" 

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

1052 
"(P  P) = P" "(P  (P  Q)) = (P  Q)" and 
12281  1053 
"(ALL x. P) = P" "(EX x. P) = P" "EX x. x=t" "EX x. t=x" 
1054 
 {* needed for the onepointrule quantifier simplification procs *} 

1055 
 {* essential for termination!! *} and 

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

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

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

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

1059 
"!!P. (ALL x. t=x > P(x)) = P(t)" 
17589  1060 
by (blast, blast, blast, blast, blast, iprover+) 
13421  1061 

14201  1062 
lemma disj_absorb: "(A  A) = A" 
1063 
by blast 

1064 

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

1066 
by blast 

1067 

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

1069 
by blast 

1070 

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

1072 
by blast 

1073 

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

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

1076 
and eq_left_commute: "(P=(Q=R)) = (Q=(P=R))" 
17589  1077 
and eq_assoc: "((P=Q)=R) = (P=(Q=R))" by (iprover, blast+) 
1078 
lemma neq_commute: "(a~=b) = (b~=a)" by iprover 

12281  1079 

1080 
lemma conj_comms: 

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

1081 
shows conj_commute: "(P&Q) = (Q&P)" 
17589  1082 
and conj_left_commute: "(P&(Q&R)) = (Q&(P&R))" by iprover+ 
1083 
lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by iprover 

12281  1084 

19174  1085 
lemmas conj_ac = conj_commute conj_left_commute conj_assoc 
1086 

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

1088 
shows disj_commute: "(PQ) = (QP)" 
17589  1089 
and disj_left_commute: "(P(QR)) = (Q(PR))" by iprover+ 
1090 
lemma disj_assoc: "((PQ)R) = (P(QR))" by iprover 

12281  1091 

19174  1092 
lemmas disj_ac = disj_commute disj_left_commute disj_assoc 
1093 

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

12281  1096 

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

12281  1099 

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

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

12281  1103 

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

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

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

1107 

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

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

1110 

21151  1111 
lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P > Q) = (P' > Q'))" 
1112 
by iprover 

1113 

17589  1114 
lemma de_Morgan_disj: "(~(P  Q)) = (~P & ~Q)" by iprover 
12281  1115 
lemma de_Morgan_conj: "(~(P & Q)) = (~P  ~Q)" by blast 
1116 
lemma not_imp: "(~(P > Q)) = (P & ~Q)" by blast 

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

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

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

1120 
by blast 

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

1122 

17589  1123 
lemma iff_conv_conj_imp: "(P = Q) = ((P > Q) & (Q > P))" by iprover 
12281  1124 

1125 

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

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

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

1129 
by blast 

1130 

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

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

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

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

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

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

1138 

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

12281  1141 

1142 
text {* 

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

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

1145 

1146 
lemma conj_cong: 

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

17589  1148 
by iprover 
12281  1149 

1150 
lemma rev_conj_cong: 

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

17589  1152 
by iprover 
12281  1153 

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

1155 

1156 
lemma disj_cong: 

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

1158 
by blast 

1159 

1160 

1161 
text {* \medskip ifthenelse rules *} 

1162 

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

1164 
by (unfold if_def) blast 

1165 

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

1167 
by (unfold if_def) blast 

1168 

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

1170 
by (unfold if_def) blast 

1171 

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

1173 
by (unfold if_def) blast 

1174 

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

1176 
apply (rule case_split [of Q]) 

15481  1177 
apply (simplesubst if_P) 
1178 
prefer 3 apply (simplesubst if_not_P, blast+) 

12281  1179 
done 
1180 

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

15481  1182 
by (simplesubst split_if, blast) 
12281  1183 

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

1184 
lemmas if_splits [noatp] = split_if split_if_asm 
12281  1185 

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

15481  1187 
by (simplesubst split_if, blast) 
12281  1188 

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

15481  1190 
by (simplesubst split_if, blast) 
12281  1191 

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

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

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

19796  1197 
 {* And this form is useful for expanding @{text "if"}s on the LEFT. *} 
15481  1198 
apply (simplesubst split_if, blast) 
12281  1199 
done 
1200 

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

12281  1203 

15423  1204 
text {* \medskip let rules for simproc *} 
1205 

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

1207 
by (unfold Let_def) 

1208 

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

1210 
by (unfold Let_def) 

1211 

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

1212 
text {* 
16999  1213 
The following copy of the implication operator is useful for 
1214 
finetuning congruence rules. It instructs the simplifier to simplify 

1215 
its premise. 

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

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

1217 

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

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

1221 

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

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

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

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

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

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

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

1229 

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

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

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

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

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

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

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

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

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

1239 

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

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

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

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

1243 
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

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

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

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

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

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

1250 
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

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

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

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

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

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

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

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

1259 

20944  1260 
lemma uncurry: 
1261 
assumes "P \<longrightarrow> Q \<longrightarrow> R" 

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

23553  1263 
using assms by blast 
20944  1264 

1265 
lemma iff_allI: 

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

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

23553  1268 
using assms by blast 
20944  1269 

1270 
lemma iff_exI: 

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

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

23553  1273 
using assms by blast 
20944  1274 

1275 
lemma all_comm: 

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

1277 
by blast 

1278 

1279 
lemma ex_comm: 

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

1281 
by blast 

1282 

9869  1283 
use "simpdata.ML" 
21671  1284 
ML {* open Simpdata *} 
1285 

21151  1286 
setup {* 
1287 
Simplifier.method_setup Splitter.split_modifiers 

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

1288 
#> (fn thy => (change_simpset_of thy (fn _ => Simpdata.simpset_simprocs); thy)) 
21151  1289 
#> Splitter.setup 
1290 
#> Clasimp.setup 

1291 
#> EqSubst.setup 

1292 
*} 

1293 

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

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

1297 
let 

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

1299 
fun is_neq eq lhs rhs thm = 

1300 
(case Thm.prop_of thm of 

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

1302 
Not = HOLogic.Not andalso eq' = eq andalso 

1303 
r' aconv lhs andalso l' aconv rhs 

1304 
 _ => false); 

1305 
fun proc ss ct = 

1306 
(case Thm.term_of ct of 

1307 
eq $ lhs $ rhs => 

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

1309 
SOME thm => SOME (thm RS neq_to_EQ_False) 

1310 
 NONE => NONE) 

1311 
 _ => NONE); 

1312 
in proc end; 

1313 
*} 

1314 

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

1316 
let 

1317 
val (f_Let_unfold, x_Let_unfold) = 

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

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

1320 
val (f_Let_folded, x_Let_folded) = 

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

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

1323 
val g_Let_folded = 

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

1325 

1326 
fun proc _ ss ct = 

1327 
let 

1328 
val ctxt = Simplifier.the_context ss; 

1329 
val thy = ProofContext.theory_of ctxt; 

1330 
val t = Thm.term_of ct; 

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

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

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

1334 
if is_Free x orelse is_Bound x orelse is_Const x 

1335 
then SOME @{thm Let_def} 

1336 
else 

1337 
let 

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

1339 
val cx = cterm_of thy x; 

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

1341 
val cf = cterm_of thy f; 

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

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

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

1345 
in (if (g aconv g') 

1346 
then 

1347 
let 

1348 
val rl = 

1349 
cterm_instantiate [(f_Let_unfold,cf),(x_Let_unfold,cx)] @{thm Let_unfold}; 

1350 
in SOME (rl OF [fx_g]) end 

1351 
else if Term.betapply (f,x) aconv g then NONE (*avoid identity conversion*) 

1352 
else let 

1353 
val abs_g'= Abs (n,xT,g'); 

1354 
val g'x = abs_g'$x; 

1355 
val g_g'x = symmetric (beta_conversion false (cterm_of thy g'x)); 

1356 
val rl = cterm_instantiate 

1357 
[(f_Let_folded,cterm_of thy f),(x_Let_folded,cx), 

1358 
(g_Let_folded,cterm_of thy abs_g')] 

1359 
@{thm Let_folded}; 

1360 
in SOME (rl OF [transitive fx_g g_g'x]) 

1361 
end) 

1362 
end 

1363 
 _ => NONE) 

1364 
end 

1365 
in proc end *} 

1366 

