author  wenzelm 
Sat, 30 May 2009 12:52:57 +0200  
changeset 31299  0c5baf034d0e 
parent 31173  bbe9e29b9672 
child 31804  627d142fce19 
permissions  rwrr 
923  1 
(* Title: HOL/HOL.thy 
11750  2 
Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson 
3 
*) 

923  4 

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

15131  7 
theory HOL 
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset

8 
imports Pure "~~/src/Tools/Code_Generator" 
23163  9 
uses 
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28856
diff
changeset

10 
("Tools/hologic.ML") 
30980  11 
"~~/src/Tools/auto_solve.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" 

30165
6ee87f67d9cd
moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
30160
diff
changeset

16 
"~~/src/Tools/intuitionistic.ML" 
30160
5f7b17941730
moved some generic tools to src/Tools/  src/Provers is essentially obsolete;
wenzelm
parents:
30063
diff
changeset

17 
"~~/src/Tools/project_rule.ML" 
23263  18 
"~~/src/Provers/hypsubst.ML" 
19 
"~~/src/Provers/splitter.ML" 

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

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

30160
5f7b17941730
moved some generic tools to src/Tools/  src/Provers is essentially obsolete;
wenzelm
parents:
30063
diff
changeset

23 
"~~/src/Tools/coherent.ML" 
5f7b17941730
moved some generic tools to src/Tools/  src/Provers is essentially obsolete;
wenzelm
parents:
30063
diff
changeset

24 
"~~/src/Tools/eqsubst.ML" 
23163  25 
"~~/src/Provers/quantifier1.ML" 
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28856
diff
changeset

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

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

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

30 
("~~/src/Tools/induct_tacs.ML") 
29505  31 
("Tools/recfun_codegen.ML") 
15131  32 
begin 
2260  33 

31299  34 
setup {* Intuitionistic.method_setup @{binding iprover} *} 
30165
6ee87f67d9cd
moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
30160
diff
changeset

35 

6ee87f67d9cd
moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
30160
diff
changeset

36 

11750  37 
subsection {* Primitive logic *} 
38 

39 
subsubsection {* Core syntax *} 

2260  40 

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

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

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

44 

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

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

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

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

48 

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

49 
global 
923  50 

7357  51 
typedecl bool 
923  52 

11750  53 
judgment 
54 
Trueprop :: "bool => prop" ("(_)" 5) 

923  55 

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

59 
False :: bool 

923  60 

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

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

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

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

923  66 

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

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

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

923  71 

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

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

73 

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

2260  76 

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

77 

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

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

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

82 

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

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

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

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

86 

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

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

89 

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

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

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

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

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

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

96 

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

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

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

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

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

102 

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

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

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

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

106 

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

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

109 

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

110 

4868  111 
nonterminals 
923  112 
letbinds letbind 
113 
case_syn cases_syn 

114 

115 
syntax 

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

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

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

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

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

923  122 

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

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

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

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

128 
translations 

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

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

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

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

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

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

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

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

139 

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

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

143 
notation (xsymbols) 

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

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

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

2372  147 

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

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

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

6340  152 

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

155 
Ex (binder "? " 10) and 

156 
Ex1 (binder "?! " 10) 

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

157 

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

158 

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

7357  161 
axioms 
15380  162 
refl: "t = (t::'a)" 
28513  163 
subst: "s = t \<Longrightarrow> P s \<Longrightarrow> P t" 
15380  164 
ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)" 
165 
 {*Extensionality is built into the metalogic, and this rule expresses 

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

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

6289  168 

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

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

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

173 

174 

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

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

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

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

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

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

923  184 

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

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

923  188 

189 
defs 

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

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

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

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

194 
"op =" 
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 
The 
22481
79c2724c36b5
added class "default" and expansion axioms for undefined
haftmann
parents:
22473
diff
changeset

197 

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

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

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

200 

28682  201 
abbreviation (input) 
202 
"arbitrary \<equiv> undefined" 

3320  203 

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

204 

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

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

206 

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

208 
fixes default :: 'a 
4868  209 

29608  210 
class zero = 
25062  211 
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

212 

29608  213 
class one = 
25062  214 
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

215 

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

216 
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

217 

29608  218 
class plus = 
25062  219 
fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 65) 
11750  220 

29608  221 
class minus = 
25762  222 
fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "" 65) 
223 

29608  224 
class uminus = 
25062  225 
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

226 

29608  227 
class times = 
25062  228 
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

229 

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

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

29608  234 
class abs = 
23878  235 
fixes abs :: "'a \<Rightarrow> 'a" 
25388  236 
begin 
23878  237 

21524  238 
notation (xsymbols) 
239 
abs ("\<bar>_\<bar>") 

25388  240 

21524  241 
notation (HTML output) 
242 
abs ("\<bar>_\<bar>") 

11750  243 

25388  244 
end 
245 

29608  246 
class sgn = 
25062  247 
fixes sgn :: "'a \<Rightarrow> 'a" 
248 

29608  249 
class ord = 
24748  250 
fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
251 
and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 

23878  252 
begin 
253 

254 
notation 

255 
less_eq ("op <=") and 

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

257 
less ("op <") and 

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

259 

260 
notation (xsymbols) 

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

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

263 

264 
notation (HTML output) 

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

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

267 

25388  268 
abbreviation (input) 
269 
greater_eq (infix ">=" 50) where 

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

271 

24842  272 
notation (input) 
23878  273 
greater_eq (infix "\<ge>" 50) 
274 

25388  275 
abbreviation (input) 
276 
greater (infix ">" 50) where 

277 
"x > y \<equiv> y < x" 

278 

279 
end 

280 

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

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

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

283 
translations 
14690  284 
(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

285 

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

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

288 
fun tr' c = (c, fn show_sorts => fn T => fn ts => 
29968  289 
if (not o null) ts orelse T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match 
20713
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset

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

294 

20944  295 
subsection {* Fundamental rules *} 
296 

20973  297 
subsubsection {* Equality *} 
20944  298 

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

15411  301 

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

15411  304 

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

18457  306 
by (erule subst) 
15411  307 

20944  308 
lemma meta_eq_to_obj_eq: 
309 
assumes meq: "A == B" 

310 
shows "A = B" 

311 
by (unfold meq) (rule refl) 

15411  312 

21502  313 
text {* Useful with @{text erule} for proving equalities from known equalities. *} 
20944  314 
(* a = b 
15411  315 
  
316 
c = d *) 

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

318 
apply (rule trans) 

319 
apply (rule trans) 

320 
apply (rule sym) 

321 
apply assumption+ 

322 
done 

323 

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

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

325 

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

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

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

328 

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

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

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

331 

15411  332 

20944  333 
subsubsection {*Congruence rules for application*} 
15411  334 

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

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

337 
apply (erule subst) 

338 
apply (rule refl) 

339 
done 

340 

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

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

343 
apply (erule subst) 

344 
apply (rule refl) 

345 
done 

346 

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

349 
apply (rule refl) 

350 
done 

351 

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

354 
apply (rule refl) 

355 
done 

356 

357 

20944  358 
subsubsection {*Equality of booleans  iff*} 
15411  359 

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

15411  362 

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

18457  364 
by (erule ssubst) 
15411  365 

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

18457  367 
by (erule iffD2) 
15411  368 

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

371 

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

373 
by (drule sym) (rule rev_iffD2) 

15411  374 

375 
lemma iffE: 

376 
assumes major: "P=Q" 

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

15411  380 

381 

20944  382 
subsubsection {*True*} 
15411  383 

384 
lemma TrueI: "True" 

21504  385 
unfolding True_def by (rule refl) 
15411  386 

21504  387 
lemma eqTrueI: "P ==> P = True" 
18457  388 
by (iprover intro: iffI TrueI) 
15411  389 

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

15411  392 

393 

20944  394 
subsubsection {*Universal quantifier*} 
15411  395 

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

15411  398 

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

400 
apply (unfold All_def) 

401 
apply (rule eqTrueE) 

402 
apply (erule fun_cong) 

403 
done 

404 

405 
lemma allE: 

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

21504  407 
and minor: "P(x) ==> R" 
408 
shows R 

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

15411  410 

411 
lemma all_dupE: 

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

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

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

15411  416 

417 

21504  418 
subsubsection {* False *} 
419 

420 
text {* 

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

422 
logic before quantifiers! 

423 
*} 

15411  424 

425 
lemma FalseE: "False ==> P" 

21504  426 
apply (unfold False_def) 
427 
apply (erule spec) 

428 
done 

15411  429 

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

15411  432 

433 

21504  434 
subsubsection {* Negation *} 
15411  435 

436 
lemma notI: 

21504  437 
assumes "P ==> False" 
15411  438 
shows "~P" 
21504  439 
apply (unfold not_def) 
440 
apply (iprover intro: impI assms) 

441 
done 

15411  442 

443 
lemma False_not_True: "False ~= True" 

21504  444 
apply (rule notI) 
445 
apply (erule False_neq_True) 

446 
done 

15411  447 

448 
lemma True_not_False: "True ~= False" 

21504  449 
apply (rule notI) 
450 
apply (drule sym) 

451 
apply (erule False_neq_True) 

452 
done 

15411  453 

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

21504  455 
apply (unfold not_def) 
456 
apply (erule mp [THEN FalseE]) 

457 
apply assumption 

458 
done 

15411  459 

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

15411  462 

463 

20944  464 
subsubsection {*Implication*} 
15411  465 

466 
lemma impE: 

467 
assumes "P>Q" "P" "Q ==> R" 

468 
shows "R" 

23553  469 
by (iprover intro: assms mp) 
15411  470 

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

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

17589  473 
by (iprover intro: mp) 
15411  474 

475 
lemma contrapos_nn: 

476 
assumes major: "~Q" 

477 
and minor: "P==>Q" 

478 
shows "~P" 

17589  479 
by (iprover intro: notI minor major [THEN notE]) 
15411  480 

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

482 
lemma contrapos_pn: 

483 
assumes major: "Q" 

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

485 
shows "~P" 

17589  486 
by (iprover intro: notI minor major notE) 
15411  487 

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

21250  489 
by (erule contrapos_nn) (erule sym) 
490 

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

492 
by (erule subst, erule ssubst, assumption) 

15411  493 

494 
(*still used in HOLCF*) 

495 
lemma rev_contrapos: 

496 
assumes pq: "P ==> Q" 

497 
and nq: "~Q" 

498 
shows "~P" 

499 
apply (rule nq [THEN contrapos_nn]) 

500 
apply (erule pq) 

501 
done 

502 

20944  503 
subsubsection {*Existential quantifier*} 
15411  504 

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

506 
apply (unfold Ex_def) 

17589  507 
apply (iprover intro: allI allE impI mp) 
15411  508 
done 
509 

510 
lemma exE: 

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

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

513 
shows "Q" 

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

17589  515 
apply (iprover intro: impI [THEN allI] minor) 
15411  516 
done 
517 

518 

20944  519 
subsubsection {*Conjunction*} 
15411  520 

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

522 
apply (unfold and_def) 

17589  523 
apply (iprover intro: impI [THEN allI] mp) 
15411  524 
done 
525 

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

527 
apply (unfold and_def) 

17589  528 
apply (iprover intro: impI dest: spec mp) 
15411  529 
done 
530 

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

532 
apply (unfold and_def) 

17589  533 
apply (iprover intro: impI dest: spec mp) 
15411  534 
done 
535 

536 
lemma conjE: 

537 
assumes major: "P&Q" 

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

539 
shows "R" 

540 
apply (rule minor) 

541 
apply (rule major [THEN conjunct1]) 

542 
apply (rule major [THEN conjunct2]) 

543 
done 

544 

545 
lemma context_conjI: 

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

15411  548 

549 

20944  550 
subsubsection {*Disjunction*} 
15411  551 

552 
lemma disjI1: "P ==> PQ" 

553 
apply (unfold or_def) 

17589  554 
apply (iprover intro: allI impI mp) 
15411  555 
done 
556 

557 
lemma disjI2: "Q ==> PQ" 

558 
apply (unfold or_def) 

17589  559 
apply (iprover intro: allI impI mp) 
15411  560 
done 
561 

562 
lemma disjE: 

563 
assumes major: "PQ" 

564 
and minorP: "P ==> R" 

565 
and minorQ: "Q ==> R" 

566 
shows "R" 

17589  567 
by (iprover intro: minorP minorQ impI 
15411  568 
major [unfolded or_def, THEN spec, THEN mp, THEN mp]) 
569 

570 

20944  571 
subsubsection {*Classical logic*} 
15411  572 

573 
lemma classical: 

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

575 
shows "P" 

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

577 
apply assumption 

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

579 
apply (erule subst) 

580 
apply assumption 

581 
done 

582 

583 
lemmas ccontr = FalseE [THEN classical, standard] 

584 

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

586 
make elimination rules*) 

587 
lemma rev_notE: 

588 
assumes premp: "P" 

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

590 
shows "R" 

591 
apply (rule ccontr) 

592 
apply (erule notE [OF premnot premp]) 

593 
done 

594 

595 
(*Double negation law*) 

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

597 
apply (rule classical) 

598 
apply (erule notE) 

599 
apply assumption 

600 
done 

601 

602 
lemma contrapos_pp: 

603 
assumes p1: "Q" 

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

605 
shows "P" 

17589  606 
by (iprover intro: classical p1 p2 notE) 
15411  607 

608 

20944  609 
subsubsection {*Unique existence*} 
15411  610 

611 
lemma ex1I: 

23553  612 
assumes "P a" "!!x. P(x) ==> x=a" 
15411  613 
shows "EX! x. P(x)" 
23553  614 
by (unfold Ex1_def, iprover intro: assms exI conjI allI impI) 
15411  615 

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

617 
lemma ex_ex1I: 

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

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

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

17589  621 
by (iprover intro: ex_prem [THEN exE] ex1I eq) 
15411  622 

623 
lemma ex1E: 

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

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

626 
shows "R" 

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

628 
apply (erule conjE) 

17589  629 
apply (iprover intro: minor) 
15411  630 
done 
631 

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

633 
apply (erule ex1E) 

634 
apply (rule exI) 

635 
apply assumption 

636 
done 

637 

638 

20944  639 
subsubsection {*THE: definite description operator*} 
15411  640 

641 
lemma the_equality: 

642 
assumes prema: "P a" 

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

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

645 
apply (rule trans [OF _ the_eq_trivial]) 

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

647 
apply (rule ext) 

648 
apply (rule iffI) 

649 
apply (erule premx) 

650 
apply (erule ssubst, rule prema) 

651 
done 

652 

653 
lemma theI: 

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

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

23553  656 
by (iprover intro: assms the_equality [THEN ssubst]) 
15411  657 

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

659 
apply (erule ex1E) 

660 
apply (erule theI) 

661 
apply (erule allE) 

662 
apply (erule mp) 

663 
apply assumption 

664 
done 

665 

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

667 
lemma theI2: 

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

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

23553  670 
by (iprover intro: assms theI) 
15411  671 

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

674 
elim:allE impE) 

675 

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

679 
apply (erule ex1E) 

680 
apply (erule all_dupE) 

681 
apply (drule mp) 

682 
apply assumption 

683 
apply (erule ssubst) 

684 
apply (erule allE) 

685 
apply (erule mp) 

686 
apply assumption 

687 
done 

688 

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

690 
apply (rule the_equality) 

691 
apply (rule refl) 

692 
apply (erule sym) 

693 
done 

694 

695 

20944  696 
subsubsection {*Classical intro rules for disjunction and existential quantifiers*} 
15411  697 

698 
lemma disjCI: 

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

700 
apply (rule classical) 

23553  701 
apply (iprover intro: assms disjI1 disjI2 notI elim: notE) 
15411  702 
done 
703 

704 
lemma excluded_middle: "~P  P" 

17589  705 
by (iprover intro: disjCI) 
15411  706 

20944  707 
text {* 
708 
case distinction as a natural deduction rule. 

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

710 
*} 

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

711 
lemma case_split [case_names True False]: 
15411  712 
assumes prem1: "P ==> Q" 
713 
and prem2: "~P ==> Q" 

714 
shows "Q" 

715 
apply (rule excluded_middle [THEN disjE]) 

716 
apply (erule prem2) 

717 
apply (erule prem1) 

718 
done 

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

719 

15411  720 
(*Classical implies (>) elimination. *) 
721 
lemma impCE: 

722 
assumes major: "P>Q" 

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

724 
shows "R" 

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

17589  726 
apply (iprover intro: minor major [THEN mp])+ 
15411  727 
done 
728 

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

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

731 
default: would break old proofs.*) 

732 
lemma impCE': 

733 
assumes major: "P>Q" 

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

735 
shows "R" 

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

17589  737 
apply (iprover intro: minor major [THEN mp])+ 
15411  738 
done 
739 

740 
(*Classical <> elimination. *) 

741 
lemma iffCE: 

742 
assumes major: "P=Q" 

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

744 
shows "R" 

745 
apply (rule major [THEN iffE]) 

17589  746 
apply (iprover intro: minor elim: impCE notE) 
15411  747 
done 
748 

749 
lemma exCI: 

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

751 
shows "EX x. P(x)" 

752 
apply (rule ccontr) 

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

756 

12386  757 
subsubsection {* Intuitionistic Reasoning *} 
758 

759 
lemma impE': 

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

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

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

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

763 
shows R 
12386  764 
proof  
765 
from 3 and 1 have P . 

766 
with 1 have Q by (rule impE) 

767 
with 2 show R . 

768 
qed 

769 

770 
lemma allE': 

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

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

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

773 
shows Q 
12386  774 
proof  
775 
from 1 have "P x" by (rule spec) 

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

777 
qed 

778 

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

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

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

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

782 
shows R 
12386  783 
proof  
784 
from 2 and 1 have P . 

785 
with 1 show R by (rule notE) 

786 
qed 

787 

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

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

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

790 

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

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

794 
and [Pure.intro] = exI disjI2 disjI1 

12386  795 

796 
lemmas [trans] = trans 

797 
and [sym] = sym not_sym 

15801  798 
and [Pure.elim?] = iffD1 iffD2 impE 
11750  799 

28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28856
diff
changeset

800 
use "Tools/hologic.ML" 
23553  801 

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

802 

11750  803 
subsubsection {* Atomizing metalevel connectives *} 
804 

28513  805 
axiomatization where 
806 
eq_reflection: "x = y \<Longrightarrow> x \<equiv> y" (*admissible axiom*) 

807 

11750  808 
lemma atomize_all [atomize]: "(!!x. P x) == Trueprop (ALL x. P x)" 
12003  809 
proof 
9488  810 
assume "!!x. P x" 
23389  811 
then show "ALL x. P x" .. 
9488  812 
next 
813 
assume "ALL x. P x" 

23553  814 
then show "!!x. P x" by (rule allE) 
9488  815 
qed 
816 

11750  817 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
12003  818 
proof 
9488  819 
assume r: "A ==> B" 
10383  820 
show "A > B" by (rule impI) (rule r) 
9488  821 
next 
822 
assume "A > B" and A 

23553  823 
then show B by (rule mp) 
9488  824 
qed 
825 

14749  826 
lemma atomize_not: "(A ==> False) == Trueprop (~A)" 
827 
proof 

828 
assume r: "A ==> False" 

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

830 
next 

831 
assume "~A" and A 

23553  832 
then show False by (rule notE) 
14749  833 
qed 
834 

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

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

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

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

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

843 

28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28741
diff
changeset

844 
lemma atomize_conj [atomize]: "(A &&& B) == Trueprop (A & B)" 
12003  845 
proof 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28741
diff
changeset

846 
assume conj: "A &&& B" 
19121  847 
show "A & B" 
848 
proof (rule conjI) 

849 
from conj show A by (rule conjunctionD1) 

850 
from conj show B by (rule conjunctionD2) 

851 
qed 

11953  852 
next 
19121  853 
assume conj: "A & B" 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28741
diff
changeset

854 
show "A &&& B" 
19121  855 
proof  
856 
from conj show A .. 

857 
from conj show B .. 

11953  858 
qed 
859 
qed 

860 

12386  861 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
18832  862 
and [symmetric, defn] = atomize_all atomize_imp atomize_eq 
12386  863 

11750  864 

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

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

866 

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

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

868 

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

869 
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

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

871 

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

872 
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

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

874 

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

875 
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

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

877 

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

878 
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

879 

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

880 

20944  881 
subsection {* Package setup *} 
882 

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

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

887 

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

889 
by (rule classical) iprover 

890 

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

893 

21151  894 
ML {* 
895 
structure Hypsubst = HypsubstFun( 

896 
struct 

897 
structure Simplifier = Simplifier 

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

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

903 
val imp_intr = @{thm impI} 

904 
val rev_mp = @{thm rev_mp} 

905 
val subst = @{thm subst} 

906 
val sym = @{thm sym} 

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

908 
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

909 
by (unfold prop_def) (drule eq_reflection, unfold)} 
21151  910 
end); 
21671  911 
open Hypsubst; 
21151  912 

913 
structure Classical = ClassicalFun( 

914 
struct 

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

917 
val swap = @{thm swap} 

918 
val classical = @{thm classical} 

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

921 
end); 

922 

923 
structure BasicClassical: BASIC_CLASSICAL = Classical; 

21671  924 
open BasicClassical; 
22129  925 

27338  926 
ML_Antiquote.value "claset" 
927 
(Scan.succeed "Classical.local_claset_of (ML_Context.the_local_context ())"); 

24035  928 

929 
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

930 

29869
a7a8b90cd882
Renamed descriptions of Nitpick (and ATP) attributes, so that they fit well with the rest of the sentence in ProofGeneral.
blanchet
parents:
29868
diff
changeset

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

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

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

937 

21009  938 
setup {* 
939 
let 

940 
(*prevent substitution on bool*) 

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

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

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

944 
in 

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

947 
#> Classical.setup 

948 
#> ResAtpset.setup 

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

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

952 

953 
declare iffI [intro!] 

954 
and notI [intro!] 

955 
and impI [intro!] 

956 
and disjCI [intro!] 

957 
and conjI [intro!] 

958 
and TrueI [intro!] 

959 
and refl [intro!] 

960 

961 
declare iffCE [elim!] 

962 
and FalseE [elim!] 

963 
and impCE [elim!] 

964 
and disjE [elim!] 

965 
and conjE [elim!] 

966 
and conjE [elim!] 

967 

968 
declare ex_ex1I [intro!] 

969 
and allI [intro!] 

970 
and the_equality [intro] 

971 
and exI [intro] 

972 

973 
declare exE [elim!] 

974 
allE [elim] 

975 

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

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

980 
apply (erule (1) meta_mp) 

981 
done 

10383  982 

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

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

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

985 

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

11977  988 

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

993 
shows R 

994 
apply (rule ex1E [OF major]) 

995 
apply (rule prem) 

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

998 
apply iprover 

999 
done 

20944  1000 

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

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

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

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

1011 
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac 

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; 
20944  1017 
*} 
1018 

21151  1019 
setup Blast.setup 
1020 

20944  1021 

1022 
subsubsection {* Simplifier *} 

12281  1023 

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

1025 

1026 
lemma simp_thms: 

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

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

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

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

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

1035 
and 

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

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

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

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

1041 
and 

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

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

1045 
"(P & True) = P" "(True & P) = P" 

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

1047 
"(P & P) = P" "(P & (P & Q)) = (P & Q)" 

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

1049 
"(P  True) = True" "(True  P) = True" 

1050 
"(P  False) = P" "(False  P) = P" 

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

1051 
"(P  P) = P" "(P  (P  Q)) = (P  Q)" and 
12281  1052 
"(ALL x. P) = P" "(EX x. P) = P" "EX x. x=t" "EX x. t=x" 
31166
a90fe83f58ea
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents:
31156
diff
changeset

1053 
and 
12281  1054 
"!!P. (EX x. x=t & P(x)) = P(t)" 
1055 
"!!P. (EX x. t=x & P(x)) = P(t)" 

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

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

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

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

1062 

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

1064 
by blast 

1065 

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

1067 
by blast 

1068 

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

1070 
by blast 

1071 

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

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

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

12281  1077 

1078 
lemma conj_comms: 

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

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

12281  1082 

19174  1083 
lemmas conj_ac = conj_commute conj_left_commute conj_assoc 
1084 

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

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

12281  1089 

19174  1090 
lemmas disj_ac = disj_commute disj_left_commute disj_assoc 
1091 

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

12281  1094 

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

12281  1097 

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

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

12281  1101 

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

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

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

1105 

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

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

1108 

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

1111 

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

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

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

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

1118 
by blast 

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

1120 

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

1123 

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

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

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

1127 
by blast 

1128 

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

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

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

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

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

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

1136 

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

12281  1139 

1140 
text {* 

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

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

1143 

1144 
lemma conj_cong: 

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

17589  1146 
by iprover 
12281  1147 

1148 
lemma rev_conj_cong: 

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

17589  1150 
by iprover 
12281  1151 

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

1153 

1154 
lemma disj_cong: 

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

1156 
by blast 

1157 

1158 

1159 
text {* \medskip ifthenelse rules *} 

1160 

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

1162 
by (unfold if_def) blast 

1163 

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

1165 
by (unfold if_def) blast 

1166 

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

1168 
by (unfold if_def) blast 

1169 

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

1171 
by (unfold if_def) blast 

1172 

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

1174 
apply (rule case_split [of Q]) 

15481  1175 
apply (simplesubst if_P) 
1176 
prefer 3 apply (simplesubst if_not_P, blast+) 

12281  1177 
done 
1178 

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

15481  1180 
by (simplesubst split_if, blast) 
12281  1181 

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

1182 
lemmas if_splits [noatp] = split_if split_if_asm 
12281  1183 

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

15481  1185 
by (simplesubst split_if, blast) 
12281  1186 

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

15481  1188 
by (simplesubst split_if, blast) 
12281  1189 

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

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

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

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

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

12281  1201 

15423  1202 
text {* \medskip let rules for simproc *} 
1203 

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

1205 
by (unfold Let_def) 

1206 

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

1208 
by (unfold Let_def) 

1209 

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

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

1213 
its premise. 

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

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

1215 

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

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

1219 

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

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

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

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

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

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

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

1227 

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

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

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

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

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

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

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

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

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

1237 

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

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

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

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

1241 
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

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

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

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

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

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

1248 
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

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

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

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

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

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

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

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

1257 

20944  1258 
lemma uncurry: 
1259 
assumes "P \<longrightarrow> Q \<longrightarrow> R" 

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

23553  1261 
using assms by blast 
20944  1262 

1263 
lemma iff_allI: 

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

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

23553  1266 
using assms by blast 
20944  1267 

1268 
lemma iff_exI: 

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

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

23553  1271 
using assms by blast 
20944  1272 

1273 
lemma all_comm: 

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

1275 
by blast 

1276 

1277 
lemma ex_comm: 

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

1279 
by blast 

1280 

28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28856
diff
changeset

1281 
use "Tools/simpdata.ML" 
21671  1282 
ML {* open Simpdata *} 
1283 

21151  1284 
setup {* 
1285 
Simplifier.method_setup Splitter.split_modifiers 

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

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

1288 
#> clasimp_setup 
21151  1289 
#> EqSubst.setup 
1290 
*} 

1291 

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

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

1295 
let 

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

1297 
fun is_neq eq lhs rhs thm = 

1298 
(case Thm.prop_of thm of 

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

1300 
Not = HOLogic.Not andalso eq' = eq andalso 

1301 
r' aconv lhs andalso l' aconv rhs 

1302 
 _ => false); 

1303 
fun proc ss ct = 

1304 
(case Thm.term_of ct of 

1305 
eq $ lhs $ rhs => 

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

1307 
SOME thm => SOME (thm RS neq_to_EQ_False) 

1308 
 NONE => NONE) 

1309 
 _ => NONE); 

1310 
in proc end; 

1311 
*} 

1312 

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

1314 
let 

1315 
val (f_Let_unfold, x_Let_unfold) = 

28741  1316 
let val [(_ $ (f $ x) $ _)] = prems_of @{thm Let_unfold} 
24035  1317 
in (cterm_of @{theory} f, cterm_of @{theory} x) end 
1318 
val (f_Let_folded, x_Let_folded) = 

28741  1319 
let val [(_ $ (f $ x) $ _)] = prems_of @{thm Let_folded} 
24035  1320 
in (cterm_of @{theory} f, cterm_of @{theory} x) end; 
1321 
val g_Let_folded = 

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

1324 
fun count_loose (Bound i) k = if i >= k then 1 else 0 

1325 
 count_loose (s $ t) k = count_loose s k + count_loose t k 

1326 
 count_loose (Abs (_, _, t)) k = count_loose t (k + 1) 

1327 
 count_loose _ _ = 0; 

1328 
fun is_trivial_let (Const (@{const_name Let}, _) $ x $ t) = 

1329 
case t 

1330 
of Abs (_, _, t') => count_loose t' 0 <= 1 

1331 
 _ => true; 

1332 
in fn _ => fn ss => fn ct => if is_trivial_let (Thm.term_of ct) 

31151  1333 
then SOME @{thm Let_def} (*no or one ocurrence of bound variable*) 
28741  1334 
else let (*Norbert Schirmer's case*) 
1335 
val ctxt = Simplifier.the_context ss; 

1336 
val thy = ProofContext.theory_of ctxt; 

1337 
val t = Thm.term_of ct; 

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

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

1340 
(case t' of Const (@{const_name Let},_) $ x $ f => (* x and f are already in normal form *) 

1341 
if is_Free x orelse is_Bound x orelse is_Const x 

1342 
then SOME @{thm Let_def} 

1343 
else 

1344 
let 

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

1346 
val cx = cterm_of thy x; 

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

1348 
val cf = cterm_of thy f; 

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

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

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

1352 
in (if (g aconv g') 

1353 
then 

1354 
let 

1355 
val rl = 

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

1357 
in SOME (rl OF [fx_g]) end 

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

1359 
else let 

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

1361 
val g'x = abs_g'$x; 

1362 
val g_g'x 