author  blanchet 
Thu, 18 Mar 2010 12:58:52 +0100  
changeset 35828  46cfc4b8112e 
parent 35808  df56c1b1680f 
child 36060  4d27652ffb40 
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") 
23171  11 
"~~/src/Tools/IsaPlanner/zipper.ML" 
12 
"~~/src/Tools/IsaPlanner/isand.ML" 

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

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

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

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

16 
"~~/src/Tools/project_rule.ML" 
32733
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32668
diff
changeset

17 
"~~/src/Tools/cong_tac.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") 
32402  32 
"~~/src/Tools/more_conv.ML" 
15131  33 
begin 
2260  34 

31299  35 
setup {* Intuitionistic.method_setup @{binding iprover} *} 
33316  36 

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

37 

11750  38 
subsection {* Primitive logic *} 
39 

40 
subsubsection {* Core syntax *} 

2260  41 

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

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

45 

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

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

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

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

49 

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

50 
global 
923  51 

7357  52 
typedecl bool 
923  53 

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

923  56 

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

60 
False :: bool 

923  61 

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

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

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

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

923  67 

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

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

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

923  72 

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

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

74 

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

2260  77 

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

78 

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

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

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

83 

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

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

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

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

87 

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

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

90 

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

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

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

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

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

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

97 

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

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

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

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

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

103 

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

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

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

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

107 

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

109 
iff (infixr "\<longleftrightarrow>" 25) 
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 

35115  129 
"THE x. P" == "CONST The (%x. P)" 
923  130 
"_Let (_binds b bs) e" == "_Let b (_Let bs e)" 
35115  131 
"let x = a in e" == "CONST 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 {* 
35115  134 
[(@{const_syntax The}, fn [Abs abs] => 
135 
let val (x, t) = atomic_abs_tr' abs 

136 
in Syntax.const @{syntax_const "_The"} $ x $ t end)] 

137 
*}  {* To avoid etacontraction of body *} 

13763
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 
refl: "t = (t::'a)" 
28513  162 
subst: "s = t \<Longrightarrow> P s \<Longrightarrow> P t" 
15380  163 
ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)" 
164 
 {*Extensionality is built into the metalogic, and this rule expresses 

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

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

6289  167 

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

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

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

172 

173 

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

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

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

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

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

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

923  183 

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

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

923  187 

188 
defs 

32068  189 
Let_def [code]: "Let s f == f(s)" 
190 
if_def: "If P x y == THE z::'a. (P=True > z=x) & (P=False > z=y)" 

5069  191 

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

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

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

196 

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

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

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

199 

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

201 
fixes default :: 'a 
4868  202 

11750  203 

20944  204 
subsection {* Fundamental rules *} 
205 

20973  206 
subsubsection {* Equality *} 
20944  207 

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

15411  210 

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

15411  213 

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

18457  215 
by (erule subst) 
15411  216 

20944  217 
lemma meta_eq_to_obj_eq: 
218 
assumes meq: "A == B" 

219 
shows "A = B" 

220 
by (unfold meq) (rule refl) 

15411  221 

21502  222 
text {* Useful with @{text erule} for proving equalities from known equalities. *} 
20944  223 
(* a = b 
15411  224 
  
225 
c = d *) 

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

227 
apply (rule trans) 

228 
apply (rule trans) 

229 
apply (rule sym) 

230 
apply assumption+ 

231 
done 

232 

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

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

234 

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

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

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

237 

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

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

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

240 

15411  241 

32733
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32668
diff
changeset

242 
subsubsection {* Congruence rules for application *} 
15411  243 

32733
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32668
diff
changeset

244 
text {* Similar to @{text AP_THM} in Gordon's HOL. *} 
15411  245 
lemma fun_cong: "(f::'a=>'b) = g ==> f(x)=g(x)" 
246 
apply (erule subst) 

247 
apply (rule refl) 

248 
done 

249 

32733
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32668
diff
changeset

250 
text {* Similar to @{text AP_TERM} in Gordon's HOL and FOL's @{text subst_context}. *} 
15411  251 
lemma arg_cong: "x=y ==> f(x)=f(y)" 
252 
apply (erule subst) 

253 
apply (rule refl) 

254 
done 

255 

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

258 
apply (rule refl) 

259 
done 

260 

32733
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32668
diff
changeset

261 
lemma cong: "[ f = g; (x::'a) = y ] ==> f x = g y" 
15411  262 
apply (erule subst)+ 
263 
apply (rule refl) 

264 
done 

265 

32733
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32668
diff
changeset

266 
ML {* val cong_tac = Cong_Tac.cong_tac @{thm cong} *} 
15411  267 

32733
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32668
diff
changeset

268 

71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32668
diff
changeset

269 
subsubsection {* Equality of booleans  iff *} 
15411  270 

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

15411  273 

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

18457  275 
by (erule ssubst) 
15411  276 

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

18457  278 
by (erule iffD2) 
15411  279 

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

282 

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

284 
by (drule sym) (rule rev_iffD2) 

15411  285 

286 
lemma iffE: 

287 
assumes major: "P=Q" 

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

15411  291 

292 

20944  293 
subsubsection {*True*} 
15411  294 

295 
lemma TrueI: "True" 

21504  296 
unfolding True_def by (rule refl) 
15411  297 

21504  298 
lemma eqTrueI: "P ==> P = True" 
18457  299 
by (iprover intro: iffI TrueI) 
15411  300 

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

15411  303 

304 

20944  305 
subsubsection {*Universal quantifier*} 
15411  306 

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

15411  309 

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

311 
apply (unfold All_def) 

312 
apply (rule eqTrueE) 

313 
apply (erule fun_cong) 

314 
done 

315 

316 
lemma allE: 

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

21504  318 
and minor: "P(x) ==> R" 
319 
shows R 

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

15411  321 

322 
lemma all_dupE: 

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

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

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

15411  327 

328 

21504  329 
subsubsection {* False *} 
330 

331 
text {* 

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

333 
logic before quantifiers! 

334 
*} 

15411  335 

336 
lemma FalseE: "False ==> P" 

21504  337 
apply (unfold False_def) 
338 
apply (erule spec) 

339 
done 

15411  340 

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

15411  343 

344 

21504  345 
subsubsection {* Negation *} 
15411  346 

347 
lemma notI: 

21504  348 
assumes "P ==> False" 
15411  349 
shows "~P" 
21504  350 
apply (unfold not_def) 
351 
apply (iprover intro: impI assms) 

352 
done 

15411  353 

354 
lemma False_not_True: "False ~= True" 

21504  355 
apply (rule notI) 
356 
apply (erule False_neq_True) 

357 
done 

15411  358 

359 
lemma True_not_False: "True ~= False" 

21504  360 
apply (rule notI) 
361 
apply (drule sym) 

362 
apply (erule False_neq_True) 

363 
done 

15411  364 

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

21504  366 
apply (unfold not_def) 
367 
apply (erule mp [THEN FalseE]) 

368 
apply assumption 

369 
done 

15411  370 

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

15411  373 

374 

20944  375 
subsubsection {*Implication*} 
15411  376 

377 
lemma impE: 

378 
assumes "P>Q" "P" "Q ==> R" 

379 
shows "R" 

23553  380 
by (iprover intro: assms mp) 
15411  381 

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

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

17589  384 
by (iprover intro: mp) 
15411  385 

386 
lemma contrapos_nn: 

387 
assumes major: "~Q" 

388 
and minor: "P==>Q" 

389 
shows "~P" 

17589  390 
by (iprover intro: notI minor major [THEN notE]) 
15411  391 

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

393 
lemma contrapos_pn: 

394 
assumes major: "Q" 

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

396 
shows "~P" 

17589  397 
by (iprover intro: notI minor major notE) 
15411  398 

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

21250  400 
by (erule contrapos_nn) (erule sym) 
401 

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

403 
by (erule subst, erule ssubst, assumption) 

15411  404 

405 
(*still used in HOLCF*) 

406 
lemma rev_contrapos: 

407 
assumes pq: "P ==> Q" 

408 
and nq: "~Q" 

409 
shows "~P" 

410 
apply (rule nq [THEN contrapos_nn]) 

411 
apply (erule pq) 

412 
done 

413 

20944  414 
subsubsection {*Existential quantifier*} 
15411  415 

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

417 
apply (unfold Ex_def) 

17589  418 
apply (iprover intro: allI allE impI mp) 
15411  419 
done 
420 

421 
lemma exE: 

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

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

424 
shows "Q" 

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

17589  426 
apply (iprover intro: impI [THEN allI] minor) 
15411  427 
done 
428 

429 

20944  430 
subsubsection {*Conjunction*} 
15411  431 

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

433 
apply (unfold and_def) 

17589  434 
apply (iprover intro: impI [THEN allI] mp) 
15411  435 
done 
436 

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

438 
apply (unfold and_def) 

17589  439 
apply (iprover intro: impI dest: spec mp) 
15411  440 
done 
441 

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

443 
apply (unfold and_def) 

17589  444 
apply (iprover intro: impI dest: spec mp) 
15411  445 
done 
446 

447 
lemma conjE: 

448 
assumes major: "P&Q" 

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

450 
shows "R" 

451 
apply (rule minor) 

452 
apply (rule major [THEN conjunct1]) 

453 
apply (rule major [THEN conjunct2]) 

454 
done 

455 

456 
lemma context_conjI: 

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

15411  459 

460 

20944  461 
subsubsection {*Disjunction*} 
15411  462 

463 
lemma disjI1: "P ==> PQ" 

464 
apply (unfold or_def) 

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

468 
lemma disjI2: "Q ==> PQ" 

469 
apply (unfold or_def) 

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

473 
lemma disjE: 

474 
assumes major: "PQ" 

475 
and minorP: "P ==> R" 

476 
and minorQ: "Q ==> R" 

477 
shows "R" 

17589  478 
by (iprover intro: minorP minorQ impI 
15411  479 
major [unfolded or_def, THEN spec, THEN mp, THEN mp]) 
480 

481 

20944  482 
subsubsection {*Classical logic*} 
15411  483 

484 
lemma classical: 

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

486 
shows "P" 

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

488 
apply assumption 

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

490 
apply (erule subst) 

491 
apply assumption 

492 
done 

493 

494 
lemmas ccontr = FalseE [THEN classical, standard] 

495 

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

497 
make elimination rules*) 

498 
lemma rev_notE: 

499 
assumes premp: "P" 

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

501 
shows "R" 

502 
apply (rule ccontr) 

503 
apply (erule notE [OF premnot premp]) 

504 
done 

505 

506 
(*Double negation law*) 

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

508 
apply (rule classical) 

509 
apply (erule notE) 

510 
apply assumption 

511 
done 

512 

513 
lemma contrapos_pp: 

514 
assumes p1: "Q" 

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

516 
shows "P" 

17589  517 
by (iprover intro: classical p1 p2 notE) 
15411  518 

519 

20944  520 
subsubsection {*Unique existence*} 
15411  521 

522 
lemma ex1I: 

23553  523 
assumes "P a" "!!x. P(x) ==> x=a" 
15411  524 
shows "EX! x. P(x)" 
23553  525 
by (unfold Ex1_def, iprover intro: assms exI conjI allI impI) 
15411  526 

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

528 
lemma ex_ex1I: 

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

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

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

17589  532 
by (iprover intro: ex_prem [THEN exE] ex1I eq) 
15411  533 

534 
lemma ex1E: 

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

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

537 
shows "R" 

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

539 
apply (erule conjE) 

17589  540 
apply (iprover intro: minor) 
15411  541 
done 
542 

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

544 
apply (erule ex1E) 

545 
apply (rule exI) 

546 
apply assumption 

547 
done 

548 

549 

20944  550 
subsubsection {*THE: definite description operator*} 
15411  551 

552 
lemma the_equality: 

553 
assumes prema: "P a" 

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

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

556 
apply (rule trans [OF _ the_eq_trivial]) 

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

558 
apply (rule ext) 

559 
apply (rule iffI) 

560 
apply (erule premx) 

561 
apply (erule ssubst, rule prema) 

562 
done 

563 

564 
lemma theI: 

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

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

23553  567 
by (iprover intro: assms the_equality [THEN ssubst]) 
15411  568 

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

570 
apply (erule ex1E) 

571 
apply (erule theI) 

572 
apply (erule allE) 

573 
apply (erule mp) 

574 
apply assumption 

575 
done 

576 

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

578 
lemma theI2: 

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

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

23553  581 
by (iprover intro: assms theI) 
15411  582 

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

585 
elim:allE impE) 

586 

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

590 
apply (erule ex1E) 

591 
apply (erule all_dupE) 

592 
apply (drule mp) 

593 
apply assumption 

594 
apply (erule ssubst) 

595 
apply (erule allE) 

596 
apply (erule mp) 

597 
apply assumption 

598 
done 

599 

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

601 
apply (rule the_equality) 

602 
apply (rule refl) 

603 
apply (erule sym) 

604 
done 

605 

606 

20944  607 
subsubsection {*Classical intro rules for disjunction and existential quantifiers*} 
15411  608 

609 
lemma disjCI: 

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

611 
apply (rule classical) 

23553  612 
apply (iprover intro: assms disjI1 disjI2 notI elim: notE) 
15411  613 
done 
614 

615 
lemma excluded_middle: "~P  P" 

17589  616 
by (iprover intro: disjCI) 
15411  617 

20944  618 
text {* 
619 
case distinction as a natural deduction rule. 

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

621 
*} 

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

622 
lemma case_split [case_names True False]: 
15411  623 
assumes prem1: "P ==> Q" 
624 
and prem2: "~P ==> Q" 

625 
shows "Q" 

626 
apply (rule excluded_middle [THEN disjE]) 

627 
apply (erule prem2) 

628 
apply (erule prem1) 

629 
done 

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

630 

15411  631 
(*Classical implies (>) elimination. *) 
632 
lemma impCE: 

633 
assumes major: "P>Q" 

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

635 
shows "R" 

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

17589  637 
apply (iprover intro: minor major [THEN mp])+ 
15411  638 
done 
639 

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

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

642 
default: would break old proofs.*) 

643 
lemma impCE': 

644 
assumes major: "P>Q" 

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

646 
shows "R" 

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

17589  648 
apply (iprover intro: minor major [THEN mp])+ 
15411  649 
done 
650 

651 
(*Classical <> elimination. *) 

652 
lemma iffCE: 

653 
assumes major: "P=Q" 

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

655 
shows "R" 

656 
apply (rule major [THEN iffE]) 

17589  657 
apply (iprover intro: minor elim: impCE notE) 
15411  658 
done 
659 

660 
lemma exCI: 

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

662 
shows "EX x. P(x)" 

663 
apply (rule ccontr) 

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

667 

12386  668 
subsubsection {* Intuitionistic Reasoning *} 
669 

670 
lemma impE': 

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

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

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

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

674 
shows R 
12386  675 
proof  
676 
from 3 and 1 have P . 

677 
with 1 have Q by (rule impE) 

678 
with 2 show R . 

679 
qed 

680 

681 
lemma allE': 

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

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

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

684 
shows Q 
12386  685 
proof  
686 
from 1 have "P x" by (rule spec) 

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

688 
qed 

689 

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

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

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

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

693 
shows R 
12386  694 
proof  
695 
from 2 and 1 have P . 

696 
with 1 show R by (rule notE) 

697 
qed 

698 

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

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

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

701 

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

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

705 
and [Pure.intro] = exI disjI2 disjI1 

12386  706 

707 
lemmas [trans] = trans 

708 
and [sym] = sym not_sym 

15801  709 
and [Pure.elim?] = iffD1 iffD2 impE 
11750  710 

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

711 
use "Tools/hologic.ML" 
23553  712 

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

713 

11750  714 
subsubsection {* Atomizing metalevel connectives *} 
715 

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

718 

11750  719 
lemma atomize_all [atomize]: "(!!x. P x) == Trueprop (ALL x. P x)" 
12003  720 
proof 
9488  721 
assume "!!x. P x" 
23389  722 
then show "ALL x. P x" .. 
9488  723 
next 
724 
assume "ALL x. P x" 

23553  725 
then show "!!x. P x" by (rule allE) 
9488  726 
qed 
727 

11750  728 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
12003  729 
proof 
9488  730 
assume r: "A ==> B" 
10383  731 
show "A > B" by (rule impI) (rule r) 
9488  732 
next 
733 
assume "A > B" and A 

23553  734 
then show B by (rule mp) 
9488  735 
qed 
736 

14749  737 
lemma atomize_not: "(A ==> False) == Trueprop (~A)" 
738 
proof 

739 
assume r: "A ==> False" 

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

741 
next 

742 
assume "~A" and A 

23553  743 
then show False by (rule notE) 
14749  744 
qed 
745 

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

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

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

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

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

754 

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

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

757 
assume conj: "A &&& B" 
19121  758 
show "A & B" 
759 
proof (rule conjI) 

760 
from conj show A by (rule conjunctionD1) 

761 
from conj show B by (rule conjunctionD2) 

762 
qed 

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

765 
show "A &&& B" 
19121  766 
proof  
767 
from conj show A .. 

768 
from conj show B .. 

11953  769 
qed 
770 
qed 

771 

12386  772 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
18832  773 
and [symmetric, defn] = atomize_all atomize_imp atomize_eq 
12386  774 

11750  775 

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

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

777 

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

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

779 

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

780 
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

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

782 

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

783 
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

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

785 

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

786 
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

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

788 

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

789 
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

790 

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

791 

20944  792 
subsection {* Package setup *} 
793 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset

794 
subsubsection {* Sledgehammer setup *} 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset

795 

46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset

796 
text {* 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset

797 
Theorems blacklisted to Sledgehammer. These theorems typically produce clauses 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset

798 
that are prolific (match too many equality or membership literals) and relate to 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset

799 
seldomused facts. Some duplicate other rules. 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset

800 
*} 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset

801 

46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset

802 
ML {* 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset

803 
structure No_ATPs = Named_Thms 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset

804 
( 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset

805 
val name = "no_atp" 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset

806 
val description = "theorems that should be avoided by Sledgehammer" 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset

807 
) 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset

808 
*} 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset

809 

46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset

810 
setup {* No_ATPs.setup *} 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset

811 

46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset

812 

11750  813 
subsubsection {* Classical Reasoner setup *} 
9529  814 

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

817 

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

819 
by (rule classical) iprover 

820 

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

823 

21151  824 
ML {* 
825 
structure Hypsubst = HypsubstFun( 

826 
struct 

827 
structure Simplifier = Simplifier 

21218  828 
val dest_eq = HOLogic.dest_eq 
21151  829 
val dest_Trueprop = HOLogic.dest_Trueprop 
830 
val dest_imp = HOLogic.dest_imp 

26411  831 
val eq_reflection = @{thm eq_reflection} 
832 
val rev_eq_reflection = @{thm meta_eq_to_obj_eq} 

833 
val imp_intr = @{thm impI} 

834 
val rev_mp = @{thm rev_mp} 

835 
val subst = @{thm subst} 

836 
val sym = @{thm sym} 

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

838 
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

839 
by (unfold prop_def) (drule eq_reflection, unfold)} 
21151  840 
end); 
21671  841 
open Hypsubst; 
21151  842 

843 
structure Classical = ClassicalFun( 

844 
struct 

26411  845 
val imp_elim = @{thm imp_elim} 
846 
val not_elim = @{thm notE} 

847 
val swap = @{thm swap} 

848 
val classical = @{thm classical} 

21151  849 
val sizef = Drule.size_of_thm 
850 
val hyp_subst_tacs = [Hypsubst.hyp_subst_tac] 

851 
end); 

852 

33308
cf62d1690d04
separate ResBlacklist, based on scalable persistent data  avoids inefficient hashing later on;
wenzelm
parents:
33185
diff
changeset

853 
structure Basic_Classical: BASIC_CLASSICAL = Classical; 
cf62d1690d04
separate ResBlacklist, based on scalable persistent data  avoids inefficient hashing later on;
wenzelm
parents:
33185
diff
changeset

854 
open Basic_Classical; 
22129  855 

27338  856 
ML_Antiquote.value "claset" 
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
32119
diff
changeset

857 
(Scan.succeed "Classical.claset_of (ML_Context.the_local_context ())"); 
21151  858 
*} 
859 

33308
cf62d1690d04
separate ResBlacklist, based on scalable persistent data  avoids inefficient hashing later on;
wenzelm
parents:
33185
diff
changeset

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

861 

21009  862 
setup {* 
863 
let 

35389  864 
fun non_bool_eq (@{const_name "op ="}, Type (_, [T, _])) = T <> @{typ bool} 
865 
 non_bool_eq _ = false; 

866 
val hyp_subst_tac' = 

867 
SUBGOAL (fn (goal, i) => 

868 
if Term.exists_Const non_bool_eq goal 

869 
then Hypsubst.hyp_subst_tac i 

870 
else no_tac); 

21009  871 
in 
21151  872 
Hypsubst.hypsubst_setup 
35389  873 
(*prevent substitution on bool*) 
33369  874 
#> Context_Rules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac) 
21009  875 
end 
876 
*} 

877 

878 
declare iffI [intro!] 

879 
and notI [intro!] 

880 
and impI [intro!] 

881 
and disjCI [intro!] 

882 
and conjI [intro!] 

883 
and TrueI [intro!] 

884 
and refl [intro!] 

885 

886 
declare iffCE [elim!] 

887 
and FalseE [elim!] 

888 
and impCE [elim!] 

889 
and disjE [elim!] 

890 
and conjE [elim!] 

891 

892 
declare ex_ex1I [intro!] 

893 
and allI [intro!] 

894 
and the_equality [intro] 

895 
and exI [intro] 

896 

897 
declare exE [elim!] 

898 
allE [elim] 

899 

22377  900 
ML {* val HOL_cs = @{claset} *} 
19162  901 

20223  902 
lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P" 
903 
apply (erule swap) 

904 
apply (erule (1) meta_mp) 

905 
done 

10383  906 

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

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

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

909 

12386  910 
lemmas [intro?] = ext 
911 
and [elim?] = ex1_implies_ex 

11977  912 

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

917 
shows R 

918 
apply (rule ex1E [OF major]) 

919 
apply (rule prem) 

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

922 
apply iprover 

923 
done 

20944  924 

21151  925 
ML {* 
32176
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32172
diff
changeset

926 
structure Blast = Blast 
25388  927 
( 
32176
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32172
diff
changeset

928 
val thy = @{theory} 
21151  929 
type claset = Classical.claset 
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22481
diff
changeset

930 
val equality_name = @{const_name "op ="} 
22993  931 
val not_name = @{const_name Not} 
26411  932 
val notE = @{thm notE} 
933 
val ccontr = @{thm ccontr} 

21151  934 
val contr_tac = Classical.contr_tac 
935 
val dup_intr = Classical.dup_intr 

936 
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac 

937 
val rep_cs = Classical.rep_cs 

938 
val cla_modifiers = Classical.cla_modifiers 

939 
val cla_meth' = Classical.cla_meth' 

25388  940 
); 
21671  941 
val blast_tac = Blast.blast_tac; 
20944  942 
*} 
943 

21151  944 
setup Blast.setup 
945 

20944  946 

947 
subsubsection {* Simplifier *} 

12281  948 

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

950 

951 
lemma simp_thms: 

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

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

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

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

956 
"(P  ~P) = True" "(~P  P) = True" 
12281  957 
"(x = x) = True" 
32068  958 
and not_True_eq_False [code]: "(\<not> True) = False" 
959 
and not_False_eq_True [code]: "(\<not> False) = True" 

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

961 
"(~P) ~= P" "P ~= (~P)" 
20944  962 
"(True=P) = P" 
963 
and eq_True: "(P = True) = P" 

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

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

966 
and 

12281  967 
"(True > P) = P" "(False > P) = True" 
968 
"(P > True) = True" "(P > P) = True" 

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

970 
"(P & True) = P" "(True & P) = P" 

971 
"(P & False) = False" "(False & P) = False" 

972 
"(P & P) = P" "(P & (P & Q)) = (P & Q)" 

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

974 
"(P  True) = True" "(True  P) = True" 

975 
"(P  False) = P" "(False  P) = P" 

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

976 
"(P  P) = P" "(P  (P  Q)) = (P  Q)" and 
12281  977 
"(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

978 
and 
12281  979 
"!!P. (EX x. x=t & P(x)) = P(t)" 
980 
"!!P. (EX x. t=x & P(x)) = P(t)" 

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

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

982 
"!!P. (ALL x. t=x > P(x)) = P(t)" 
17589  983 
by (blast, blast, blast, blast, blast, iprover+) 
13421  984 

14201  985 
lemma disj_absorb: "(A  A) = A" 
986 
by blast 

987 

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

989 
by blast 

990 

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

992 
by blast 

993 

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

995 
by blast 

996 

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

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

999 
and eq_left_commute: "(P=(Q=R)) = (Q=(P=R))" 
17589  1000 
and eq_assoc: "((P=Q)=R) = (P=(Q=R))" by (iprover, blast+) 
1001 
lemma neq_commute: "(a~=b) = (b~=a)" by iprover 

12281  1002 

1003 
lemma conj_comms: 

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

1004 
shows conj_commute: "(P&Q) = (Q&P)" 
17589  1005 
and conj_left_commute: "(P&(Q&R)) = (Q&(P&R))" by iprover+ 
1006 
lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by iprover 

12281  1007 

19174  1008 
lemmas conj_ac = conj_commute conj_left_commute conj_assoc 
1009 

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

1011 
shows disj_commute: "(PQ) = (QP)" 
17589  1012 
and disj_left_commute: "(P(QR)) = (Q(PR))" by iprover+ 
1013 
lemma disj_assoc: "((PQ)R) = (P(QR))" by iprover 

12281  1014 

19174  1015 
lemmas disj_ac = disj_commute disj_left_commute disj_assoc 
1016 

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

12281  1019 

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

12281  1022 

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

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

12281  1026 

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

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

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

1030 

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

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

1033 

21151  1034 
lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P > Q) = (P' > Q'))" 
1035 
by iprover 

1036 

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

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

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

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

1043 
by blast 

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

1045 

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

1048 

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

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

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

1052 
by blast 

1053 

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

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

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

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

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset

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

1061 

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

12281  1064 

1065 
text {* 

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

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

1068 

1069 
lemma conj_cong: 

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

17589  1071 
by iprover 
12281  1072 

1073 
lemma rev_conj_cong: 

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

17589  1075 
by iprover 
12281  1076 

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

1078 

1079 
lemma disj_cong: 

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

1081 
by blast 

1082 

1083 

1084 
text {* \medskip ifthenelse rules *} 

1085 

32068  1086 
lemma if_True [code]: "(if True then x else y) = x" 
12281  1087 
by (unfold if_def) blast 
1088 

32068  1089 
lemma if_False [code]: "(if False then x else y) = y" 
12281  1090 
by (unfold if_def) blast 
1091 

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

1093 
by (unfold if_def) blast 

1094 

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

1096 
by (unfold if_def) blast 

1097 

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

1099 
apply (rule case_split [of Q]) 

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

12281  1102 
done 
1103 

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

15481  1105 
by (simplesubst split_if, blast) 
12281  1106 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset

1107 
lemmas if_splits [no_atp] = split_if split_if_asm 
12281  1108 

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

15481  1110 
by (simplesubst split_if, blast) 
12281  1111 

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

15481  1113 
by (simplesubst split_if, blast) 
12281  1114 

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

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

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

19796  1120 
 {* And this form is useful for expanding @{text "if"}s on the LEFT. *} 
15481  1121 
apply (simplesubst split_if, blast) 
12281  1122 
done 
1123 

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

12281  1126 

15423  1127 
text {* \medskip let rules for simproc *} 
1128 

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

1130 
by (unfold Let_def) 

1131 

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

1133 
by (unfold Let_def) 

1134 

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

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

1138 
its premise. 

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

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

1140 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35115
diff
changeset

1141 
definition simp_implies :: "[prop, prop] => prop" (infixr "=simp=>" 1) where 
28562  1142 
[code del]: "simp_implies \<equiv> op ==>" 
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1143 

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

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

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

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

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

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

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

1151 

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

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

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

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

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

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

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

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

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

1161 

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

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

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

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

1165 
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

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

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

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

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

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

1172 
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

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

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

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

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

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

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

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

1181 

20944  1182 
lemma uncurry: 
1183 
assumes "P \<longrightarrow> Q \<longrightarrow> R" 

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

23553  1185 
using assms by blast 
20944  1186 

1187 
lemma iff_allI: 

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

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

23553  1190 
using assms by blast 
20944  1191 

1192 
lemma iff_exI: 

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

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

23553  1195 
using assms by blast 
20944  1196 

1197 
lemma all_comm: 

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

1199 
by blast 

1200 

1201 
lemma ex_comm: 

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

1203 
by blast 

1204 

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

1205 
use "Tools/simpdata.ML" 
21671  1206 
ML {* open Simpdata *} 
1207 

21151  1208 
setup {* 
1209 
Simplifier.method_setup Splitter.split_modifiers 

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

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

1212 
#> clasimp_setup 
21151  1213 
#> EqSubst.setup 
1214 
*} 

1215 

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

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

1219 
let 

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

1221 
fun is_neq eq lhs rhs thm = 

1222 
(case Thm.prop_of thm of 

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

1224 
Not = HOLogic.Not andalso eq' = eq andalso 

1225 
r' aconv lhs andalso l' aconv rhs 

1226 
 _ => false); 

1227 
fun proc ss ct = 

1228 
(case Thm.term_of ct of 

1229 
eq $ lhs $ rhs => 

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

1231 
SOME thm => SOME (thm RS neq_to_EQ_False) 

1232 
 NONE => NONE) 

1233 
 _ => NONE); 

1234 
in proc end; 

1235 
*} 

1236 

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

1238 
let 

1239 
val (f_Let_unfold, x_Let_unfold) = 

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

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

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

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

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

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

1251 
 count_loose _ _ = 0; 

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

1253 
case t 

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

1255 
 _ => true; 

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

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

1260 
val thy = ProofContext.theory_of ctxt; 

1261 
val t = Thm.term_of ct; 

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

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

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

1265 
if is_Free x orelse is_Bound x orelse is_Const x 

1266 
then SOME @{thm Let_def} 

1267 
else 

1268 
let 

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

1270 
val cx = cterm_of thy x; 

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

1272 
val cf = cterm_of thy f; 

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

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

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

1276 
in (if (g aconv g') 

1277 
then 

1278 
let 

1279 
val rl = 

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

1281 
in SOME (rl OF [fx_g]) end 

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

1283 
else let 

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

1285 
val g'x = abs_g'$x; 

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

1287 
val rl = cterm_instantiate 

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

1289 
(g_Let_folded, cterm_of thy abs_g')] 

1290 
@{thm Let_folded}; 

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

1292 
end) 

1293 
end 

1294 
 _ => NONE) 

1295 
end 

1296 
end *} 

24035  1297 

21151  1298 
lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P" 
1299 
proof 

23389  1300 
assume "True \<Longrightarrow> PROP P" 
1301 
from this [OF TrueI] show "PROP P" . 

21151  1302 
next 
1303 
assume "PROP P" 

23389  1304 
then show "PROP P" . 
21151  1305 
qed 
1306 

1307 
lemma ex_simps: 

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

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

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

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

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

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

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

1315 
by (iprover  blast)+ 

1316 

1317 
lemma all_simps: 

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

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

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

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

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

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

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

1325 
by (iprover  blast)+ 

15481  1326 

21671  1327 
lemmas [simp] = 
1328 
triv_forall_equality (*prunes params*) 

1329 
True_implies_equals (*prune asms `True'*) 

1330 
if_True 

1331 
if_False 

1332 
if_cancel 

1333 
if_eq_cancel 

1334 
imp_disjL 

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

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

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

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

21671  1340 
conj_assoc 
1341 
disj_assoc 

1342 
de_Morgan_conj 

1343 
de_Morgan_disj 

1344 
imp_disj1 

1345 
imp_disj2 

1346 
not_imp 

1347 
disj_not1 

1348 
not_all 

1349 
not_ex 

1350 
cases_simp 

1351 
the_eq_trivial 

1352 
the_sym_eq_trivial 

1353 
ex_simps 

1354 
all_simps 

1355 
simp_thms 

1356 

1357 
lemmas [cong] = imp_cong simp_implies_cong 

1358 
lemmas [split] = split_if 

20973  1359 

22377  1360 
ML {* val HOL_ss = @{simpset} *} 
20973  1361 

20944  1362 
text {* Simplifies x assuming c and y assuming ~c *} 
34b2c1bb7178
cleanup basic HOL bootstrap
h 