author  haftmann 
Thu, 02 Sep 2010 09:13:28 +0200  
changeset 39016  caad9d509bc4 
parent 39014  e820beaf7d8c 
parent 39015  81a70e2835b6 
child 39033  e8b68ec3bb9c 
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" 
37781
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
37767
diff
changeset

18 
"~~/src/Tools/misc_legacy.ML" 
23263  19 
"~~/src/Provers/hypsubst.ML" 
20 
"~~/src/Provers/splitter.ML" 

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

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

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

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

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

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

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

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

31 
("~~/src/Tools/induct_tacs.ML") 
29505  32 
("Tools/recfun_codegen.ML") 
38990  33 
"Tools/async_manager.ML" 
38944  34 
"Tools/try.ML" 
15131  35 
begin 
2260  36 

31299  37 
setup {* Intuitionistic.method_setup @{binding iprover} *} 
33316  38 

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

39 

11750  40 
subsection {* Primitive logic *} 
41 

42 
subsubsection {* Core syntax *} 

2260  43 

14854  44 
classes type 
36452  45 
default_sort type 
35625  46 
setup {* Object_Logic.add_base_sort @{sort type} *} 
25460
b80087af2274
interpretation of typedecls: instantiation to class type
haftmann
parents:
25388
diff
changeset

47 

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

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

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

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

51 

7357  52 
typedecl bool 
923  53 

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

923  56 

11750  57 
consts 
7357  58 
True :: bool 
59 
False :: bool 

38547  60 
Not :: "bool => bool" ("~ _" [40] 40) 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

61 

848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

62 
conj :: "[bool, bool] => bool" (infixr "&" 35) 
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

63 
disj :: "[bool, bool] => bool" (infixr "" 30) 
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38773
diff
changeset

64 
implies :: "[bool, bool] => bool" (infixr ">" 25) 
38555  65 

38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38857
diff
changeset

66 
eq :: "['a, 'a] => bool" (infixl "=" 50) 
38708
8915e3ce8655
discontinued obsolete 'global' and 'local' commands;
wenzelm
parents:
38669
diff
changeset

67 

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

68 
The :: "('a => bool) => 'a" 
7357  69 
All :: "('a => bool) => bool" (binder "ALL " 10) 
70 
Ex :: "('a => bool) => bool" (binder "EX " 10) 

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

923  72 

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

73 

11750  74 
subsubsection {* Additional concrete syntax *} 
2260  75 

21210  76 
notation (output) 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38857
diff
changeset

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

78 

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

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

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

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

82 

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

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

85 

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

87 
Not ("\<not> _" [40] 40) and 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38857
diff
changeset

88 
conj (infixr "\<and>" 35) and 
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38857
diff
changeset

89 
disj (infixr "\<or>" 30) and 
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38857
diff
changeset

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

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

92 

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

94 
Not ("\<not> _" [40] 40) and 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38857
diff
changeset

95 
conj (infixr "\<and>" 35) and 
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38857
diff
changeset

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

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

98 

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

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

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

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

102 

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

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

105 

4868  106 
nonterminals 
923  107 
letbinds letbind 
108 
case_syn cases_syn 

109 

110 
syntax 

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

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

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

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

36363  116 
"_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" [0, 10] 10) 
923  117 

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

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

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

121 
"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/  _") 
923  122 

123 
translations 

35115  124 
"THE x. P" == "CONST The (%x. P)" 
923  125 

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

126 
print_translation {* 
35115  127 
[(@{const_syntax The}, fn [Abs abs] => 
128 
let val (x, t) = atomic_abs_tr' abs 

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

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

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

131 

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

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

135 
notation (xsymbols) 

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

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

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

2372  139 

21524  140 
notation (HTML output) 
141 
All (binder "\<forall>" 10) and 

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

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

6340  144 

21524  145 
notation (HOL) 
146 
All (binder "! " 10) and 

147 
Ex (binder "? " 10) and 

148 
Ex1 (binder "?! " 10) 

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

149 

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

150 

11750  151 
subsubsection {* Axioms and basic definitions *} 
2260  152 

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

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

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

6289  160 

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

161 
the_eq_trivial: "(THE x. x = a) = (a::'a)" 
923  162 

15380  163 
impI: "(P ==> Q) ==> P>Q" 
164 
mp: "[ P>Q; P ] ==> Q" 

165 

166 

923  167 
defs 
7357  168 
True_def: "True == ((%x::bool. x) = (%x. x))" 
169 
All_def: "All(P) == (P = (%x. True))" 

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

170 
Ex_def: "Ex(P) == !Q. (!x. P x > Q) > Q" 
7357  171 
False_def: "False == (!P. P)" 
172 
not_def: "~ P == P>False" 

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

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

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

923  176 

7357  177 
axioms 
178 
iff: "(P>Q) > (Q>P) > (P=Q)" 

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

923  180 

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

181 
finalconsts 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38857
diff
changeset

182 
eq 
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38857
diff
changeset

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

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

185 

38525  186 
definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10) where 
187 
"If P x y \<equiv> (THE z::'a. (P=True > z=x) & (P=False > z=y))" 

188 

189 
definition Let :: "'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b" where 

190 
"Let s f \<equiv> f s" 

191 

192 
translations 

193 
"_Let (_binds b bs) e" == "_Let b (_Let bs e)" 

194 
"let x = a in e" == "CONST Let a (%x. e)" 

195 

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

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

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

198 

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

200 
fixes default :: 'a 
4868  201 

11750  202 

20944  203 
subsection {* Fundamental rules *} 
204 

20973  205 
subsubsection {* Equality *} 
20944  206 

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

15411  209 

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

15411  212 

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

18457  214 
by (erule subst) 
15411  215 

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

218 
shows "A = B" 

219 
by (unfold meq) (rule refl) 

15411  220 

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

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

226 
apply (rule trans) 

227 
apply (rule trans) 

228 
apply (rule sym) 

229 
apply assumption+ 

230 
done 

231 

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

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

233 

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

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

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

236 

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

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

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

239 

15411  240 

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

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

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

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

246 
apply (rule refl) 

247 
done 

248 

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

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

252 
apply (rule refl) 

253 
done 

254 

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

257 
apply (rule refl) 

258 
done 

259 

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

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

263 
done 

264 

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

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

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

267 

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 
subsubsection {* Equality of booleans  iff *} 
15411  269 

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

15411  272 

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

18457  274 
by (erule ssubst) 
15411  275 

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

18457  277 
by (erule iffD2) 
15411  278 

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

281 

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

283 
by (drule sym) (rule rev_iffD2) 

15411  284 

285 
lemma iffE: 

286 
assumes major: "P=Q" 

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

15411  290 

291 

20944  292 
subsubsection {*True*} 
15411  293 

294 
lemma TrueI: "True" 

21504  295 
unfolding True_def by (rule refl) 
15411  296 

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

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

15411  302 

303 

20944  304 
subsubsection {*Universal quantifier*} 
15411  305 

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

15411  308 

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

310 
apply (unfold All_def) 

311 
apply (rule eqTrueE) 

312 
apply (erule fun_cong) 

313 
done 

314 

315 
lemma allE: 

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

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

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

15411  320 

321 
lemma all_dupE: 

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

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

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

15411  326 

327 

21504  328 
subsubsection {* False *} 
329 

330 
text {* 

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

332 
logic before quantifiers! 

333 
*} 

15411  334 

335 
lemma FalseE: "False ==> P" 

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

338 
done 

15411  339 

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

15411  342 

343 

21504  344 
subsubsection {* Negation *} 
15411  345 

346 
lemma notI: 

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

351 
done 

15411  352 

353 
lemma False_not_True: "False ~= True" 

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

356 
done 

15411  357 

358 
lemma True_not_False: "True ~= False" 

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

361 
apply (erule False_neq_True) 

362 
done 

15411  363 

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

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

367 
apply assumption 

368 
done 

15411  369 

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

15411  372 

373 

20944  374 
subsubsection {*Implication*} 
15411  375 

376 
lemma impE: 

377 
assumes "P>Q" "P" "Q ==> R" 

378 
shows "R" 

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

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

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

17589  383 
by (iprover intro: mp) 
15411  384 

385 
lemma contrapos_nn: 

386 
assumes major: "~Q" 

387 
and minor: "P==>Q" 

388 
shows "~P" 

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

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

392 
lemma contrapos_pn: 

393 
assumes major: "Q" 

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

395 
shows "~P" 

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

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

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

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

402 
by (erule subst, erule ssubst, assumption) 

15411  403 

404 
(*still used in HOLCF*) 

405 
lemma rev_contrapos: 

406 
assumes pq: "P ==> Q" 

407 
and nq: "~Q" 

408 
shows "~P" 

409 
apply (rule nq [THEN contrapos_nn]) 

410 
apply (erule pq) 

411 
done 

412 

20944  413 
subsubsection {*Existential quantifier*} 
15411  414 

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

416 
apply (unfold Ex_def) 

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

420 
lemma exE: 

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

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

423 
shows "Q" 

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

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

428 

20944  429 
subsubsection {*Conjunction*} 
15411  430 

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

432 
apply (unfold and_def) 

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

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

437 
apply (unfold and_def) 

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

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

442 
apply (unfold and_def) 

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

446 
lemma conjE: 

447 
assumes major: "P&Q" 

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

449 
shows "R" 

450 
apply (rule minor) 

451 
apply (rule major [THEN conjunct1]) 

452 
apply (rule major [THEN conjunct2]) 

453 
done 

454 

455 
lemma context_conjI: 

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

15411  458 

459 

20944  460 
subsubsection {*Disjunction*} 
15411  461 

462 
lemma disjI1: "P ==> PQ" 

463 
apply (unfold or_def) 

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

467 
lemma disjI2: "Q ==> PQ" 

468 
apply (unfold or_def) 

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

472 
lemma disjE: 

473 
assumes major: "PQ" 

474 
and minorP: "P ==> R" 

475 
and minorQ: "Q ==> R" 

476 
shows "R" 

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

480 

20944  481 
subsubsection {*Classical logic*} 
15411  482 

483 
lemma classical: 

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

485 
shows "P" 

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

487 
apply assumption 

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

489 
apply (erule subst) 

490 
apply assumption 

491 
done 

492 

493 
lemmas ccontr = FalseE [THEN classical, standard] 

494 

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

496 
make elimination rules*) 

497 
lemma rev_notE: 

498 
assumes premp: "P" 

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

500 
shows "R" 

501 
apply (rule ccontr) 

502 
apply (erule notE [OF premnot premp]) 

503 
done 

504 

505 
(*Double negation law*) 

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

507 
apply (rule classical) 

508 
apply (erule notE) 

509 
apply assumption 

510 
done 

511 

512 
lemma contrapos_pp: 

513 
assumes p1: "Q" 

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

515 
shows "P" 

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

518 

20944  519 
subsubsection {*Unique existence*} 
15411  520 

521 
lemma ex1I: 

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

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

527 
lemma ex_ex1I: 

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

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

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

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

533 
lemma ex1E: 

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

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

536 
shows "R" 

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

538 
apply (erule conjE) 

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

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

543 
apply (erule ex1E) 

544 
apply (rule exI) 

545 
apply assumption 

546 
done 

547 

548 

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

551 
lemma the_equality: 

552 
assumes prema: "P a" 

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

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

555 
apply (rule trans [OF _ the_eq_trivial]) 

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

557 
apply (rule ext) 

558 
apply (rule iffI) 

559 
apply (erule premx) 

560 
apply (erule ssubst, rule prema) 

561 
done 

562 

563 
lemma theI: 

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

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

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

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

569 
apply (erule ex1E) 

570 
apply (erule theI) 

571 
apply (erule allE) 

572 
apply (erule mp) 

573 
apply assumption 

574 
done 

575 

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

577 
lemma theI2: 

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

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

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

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

584 
elim:allE impE) 

585 

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

589 
apply (erule ex1E) 

590 
apply (erule all_dupE) 

591 
apply (drule mp) 

592 
apply assumption 

593 
apply (erule ssubst) 

594 
apply (erule allE) 

595 
apply (erule mp) 

596 
apply assumption 

597 
done 

598 

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

600 
apply (rule the_equality) 

601 
apply (rule refl) 

602 
apply (erule sym) 

603 
done 

604 

605 

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

608 
lemma disjCI: 

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

610 
apply (rule classical) 

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

614 
lemma excluded_middle: "~P  P" 

17589  615 
by (iprover intro: disjCI) 
15411  616 

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

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

620 
*} 

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

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

624 
shows "Q" 

625 
apply (rule excluded_middle [THEN disjE]) 

626 
apply (erule prem2) 

627 
apply (erule prem1) 

628 
done 

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

629 

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

632 
assumes major: "P>Q" 

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

634 
shows "R" 

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

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

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

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

641 
default: would break old proofs.*) 

642 
lemma impCE': 

643 
assumes major: "P>Q" 

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

645 
shows "R" 

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

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

650 
(*Classical <> elimination. *) 

651 
lemma iffCE: 

652 
assumes major: "P=Q" 

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

654 
shows "R" 

655 
apply (rule major [THEN iffE]) 

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

659 
lemma exCI: 

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

661 
shows "EX x. P(x)" 

662 
apply (rule ccontr) 

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

666 

12386  667 
subsubsection {* Intuitionistic Reasoning *} 
668 

669 
lemma impE': 

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

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

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

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

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

676 
with 1 have Q by (rule impE) 

677 
with 2 show R . 

678 
qed 

679 

680 
lemma allE': 

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

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

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

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

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

687 
qed 

688 

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

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

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

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

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

695 
with 1 show R by (rule notE) 

696 
qed 

697 

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

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

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

700 

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

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

704 
and [Pure.intro] = exI disjI2 disjI1 

12386  705 

706 
lemmas [trans] = trans 

707 
and [sym] = sym not_sym 

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

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

710 
use "Tools/hologic.ML" 
23553  711 

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

712 

11750  713 
subsubsection {* Atomizing metalevel connectives *} 
714 

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

717 

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

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

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

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

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

738 
assume r: "A ==> False" 

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

740 
next 

741 
assume "~A" and A 

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

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

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

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

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

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

753 

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

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

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

759 
from conj show A by (rule conjunctionD1) 

760 
from conj show B by (rule conjunctionD2) 

761 
qed 

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

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

767 
from conj show B .. 

11953  768 
qed 
769 
qed 

770 

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

11750  774 

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

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

776 

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

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

778 

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

779 
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

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

781 

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

782 
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

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

784 

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

785 
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

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

787 

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

788 
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

789 

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

790 

20944  791 
subsection {* Package setup *} 
792 

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

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

794 

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

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

796 
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

797 
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

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

799 
*} 
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 
ML {* 
36297
6b2b9516a3cd
removed obsolete Named_Thm_Set  Named_Thms provides efficient member operation;
wenzelm
parents:
36246
diff
changeset

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

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

804 
val name = "no_atp" 
36060
4d27652ffb40
reintroduce efficient set structure to collect "no_atp" theorems
blanchet
parents:
35828
diff
changeset

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

806 
) 
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 
setup {* No_ATPs.setup *} 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset

810 

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

811 

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

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

816 

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

818 
by (rule classical) iprover 

819 

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

822 

21151  823 
ML {* 
824 
structure Hypsubst = HypsubstFun( 

825 
struct 

826 
structure Simplifier = Simplifier 

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

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

832 
val imp_intr = @{thm impI} 

833 
val rev_mp = @{thm rev_mp} 

834 
val subst = @{thm subst} 

835 
val sym = @{thm sym} 

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

837 
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

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

842 
structure Classical = ClassicalFun( 

843 
struct 

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

846 
val swap = @{thm swap} 

847 
val classical = @{thm classical} 

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

850 
end); 

851 

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

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

853 
open Basic_Classical; 
22129  854 

27338  855 
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

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

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

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

860 

21009  861 
setup {* 
862 
let 

38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38857
diff
changeset

863 
fun non_bool_eq (@{const_name HOL.eq}, Type (_, [T, _])) = T <> @{typ bool} 
35389  864 
 non_bool_eq _ = false; 
865 
val hyp_subst_tac' = 

866 
SUBGOAL (fn (goal, i) => 

867 
if Term.exists_Const non_bool_eq goal 

868 
then Hypsubst.hyp_subst_tac i 

869 
else no_tac); 

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

876 

877 
declare iffI [intro!] 

878 
and notI [intro!] 

879 
and impI [intro!] 

880 
and disjCI [intro!] 

881 
and conjI [intro!] 

882 
and TrueI [intro!] 

883 
and refl [intro!] 

884 

885 
declare iffCE [elim!] 

886 
and FalseE [elim!] 

887 
and impCE [elim!] 

888 
and disjE [elim!] 

889 
and conjE [elim!] 

890 

891 
declare ex_ex1I [intro!] 

892 
and allI [intro!] 

893 
and the_equality [intro] 

894 
and exI [intro] 

895 

896 
declare exE [elim!] 

897 
allE [elim] 

898 

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

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

903 
apply (erule (1) meta_mp) 

904 
done 

10383  905 

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

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

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

908 

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

11977  911 

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

916 
shows R 

917 
apply (rule ex1E [OF major]) 

918 
apply (rule prem) 

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

921 
apply iprover 

922 
done 

20944  923 

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

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

927 
val thy = @{theory} 
21151  928 
type claset = Classical.claset 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38857
diff
changeset

929 
val equality_name = @{const_name HOL.eq} 
22993  930 
val not_name = @{const_name Not} 
26411  931 
val notE = @{thm notE} 
932 
val ccontr = @{thm ccontr} 

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

935 
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac 

936 
val rep_cs = Classical.rep_cs 

937 
val cla_modifiers = Classical.cla_modifiers 

938 
val cla_meth' = Classical.cla_meth' 

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

21151  943 
setup Blast.setup 
944 

20944  945 

946 
subsubsection {* Simplifier *} 

12281  947 

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

949 

950 
lemma simp_thms: 

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

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

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

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

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

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

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

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

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

965 
and 

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

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

969 
"(P & True) = P" "(True & P) = P" 

970 
"(P & False) = False" "(False & P) = False" 

971 
"(P & P) = P" "(P & (P & Q)) = (P & Q)" 

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

973 
"(P  True) = True" "(True  P) = True" 

974 
"(P  False) = P" "(False  P) = P" 

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

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

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

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

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

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

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

986 

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

988 
by blast 

989 

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

991 
by blast 

992 

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

994 
by blast 

995 

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

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

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

12281  1001 

1002 
lemma conj_comms: 

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

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

12281  1006 

19174  1007 
lemmas conj_ac = conj_commute conj_left_commute conj_assoc 
1008 

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

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

12281  1013 

19174  1014 
lemmas disj_ac = disj_commute disj_left_commute disj_assoc 
1015 

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

12281  1018 

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

12281  1021 

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

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

12281  1025 

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

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

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

1029 

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

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

1032 

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

1035 

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

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

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

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

1042 
by blast 

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

1044 

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

1047 

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

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

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

1051 
by blast 

1052 

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

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

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

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

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

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

1060 

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

12281  1063 

1064 
text {* 

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

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

1067 

1068 
lemma conj_cong: 

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

17589  1070 
by iprover 
12281  1071 

1072 
lemma rev_conj_cong: 

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

17589  1074 
by iprover 
12281  1075 

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

1077 

1078 
lemma disj_cong: 

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

1080 
by blast 

1081 

1082 

1083 
text {* \medskip ifthenelse rules *} 

1084 

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

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

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

38525  1092 
by (unfold If_def) blast 
12281  1093 

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

38525  1095 
by (unfold If_def) blast 
12281  1096 

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

1098 
apply (rule case_split [of Q]) 

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

12281  1101 
done 
1102 

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

15481  1104 
by (simplesubst split_if, blast) 
12281  1105 

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

1106 
lemmas if_splits [no_atp] = split_if split_if_asm 
12281  1107 

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

15481  1109 
by (simplesubst split_if, blast) 
12281  1110 

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

15481  1112 
by (simplesubst split_if, blast) 
12281  1113 

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

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

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

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

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

12281  1125 

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

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

1129 
by (unfold Let_def) 

1130 

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

1132 
by (unfold Let_def) 

1133 

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

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

1137 
its premise. 

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

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

1139 

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

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

1142 

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

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

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

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

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

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

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

1150 

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

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

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

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

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

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

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

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

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

1160 

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

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

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

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

1164 
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

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

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

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

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

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

1171 
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

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

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

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

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

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

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

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

1180 

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

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

23553  1184 
using assms by blast 
20944  1185 

1186 
lemma iff_allI: 

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

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

23553  1189 
using assms by blast 
20944  1190 

1191 
lemma iff_exI: 

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

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

23553  1194 
using assms by blast 
20944  1195 

1196 
lemma all_comm: 

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

1198 
by blast 

1199 

1200 
lemma ex_comm: 

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

1202 
by blast 

1203 

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

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

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

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

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

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

1214 

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

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

1218 
let 

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

1220 
fun is_neq eq lhs rhs thm = 

1221 
(case Thm.prop_of thm of 

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

1223 
Not = HOLogic.Not andalso eq' = eq andalso 

1224 
r' aconv lhs andalso l' aconv rhs 

1225 
 _ => false); 

1226 
fun proc ss ct = 

1227 
(case Thm.term_of ct of 

1228 
eq $ lhs $ rhs => 

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

1230 
SOME thm => SOME (thm RS neq_to_EQ_False) 

1231 
 NONE => NONE) 

1232 
 _ => NONE); 

1233 
in proc end; 

1234 
*} 

1235 

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

1237 
let 

1238 
val (f_Let_unfold, x_Let_unfold) = 

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

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

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

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

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

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

1250 
 count_loose _ _ = 0; 

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

1252 
case t 

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

1254 
 _ => true; 

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

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

1259 
val thy = ProofContext.theory_of ctxt; 

1260 
val t = Thm.term_of ct; 

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

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

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

1264 
if is_Free x orelse is_Bound x orelse is_Const x 

1265 
then SOME @{thm Let_def} 

1266 
else 

1267 
let 

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

1269 
val cx = cterm_of thy x; 

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

1271 
val cf = cterm_of thy f; 

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

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

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

1275 
in (if (g aconv g') 

1276 
then 

1277 
let 

1278 
val rl = 

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

1280 
in SOME (rl OF [fx_g]) end 

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

1282 
else let 

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

1284 
val g'x = abs_g'$x; 

36945  1285 
val g_g'x = Thm.symmetric (Thm.beta_conversion false (cterm_of thy g'x)); 
28741  1286 
val rl = cterm_instantiate 
1287 
[(f_Let_folded, cterm_of thy f), (x_Let_folded, cx), 

1288 
(g_Let_folded, cterm_of thy abs_g')] 

1289 
@{thm Let_folded}; 

36945  1290 
in SOME (rl OF [Thm.transitive fx_g g_g'x]) 
28741  1291 
end) 
1292 
end 

1293 
 _ => NONE) 

1294 
end 

1295 
end *} 

24035  1296 

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

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

21151  1301 
next 
1302 
assume "PROP P" 

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

1306 
lemma ex_simps: 

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

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

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

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

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

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

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

1314 
by (iprover  blast)+ 

1315 

1316 
lemma all_simps: 

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

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

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

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

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

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

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

1324 
by (iprover  blast)+ 

15481  1325 

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

1328 
True_implies_equals (*prune asms `True'*) 

1329 
if_True 

1330 
if_False 

1331 
if_cancel 

1332 
if_eq_cancel 

1333 
imp_disjL 

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

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

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

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

21671  1339 
conj_assoc 
1340 
disj_assoc 

1341 
de_Morgan_conj 

1342 
de_Morgan_disj 

1343 
imp_disj1 

1344 
imp_disj2 

1345 
not_imp 

1346 
disj_not1 

1347 
not_all 

1348 
not_ex 

1349 
cases_simp 

1350 
the_eq_trivial 

1351 
the_sym_eq_trivial 

1352 
ex_simps 

1353 
all_simps 

1354 
simp_thms 

1355 

1356 
lemmas [cong] = imp_cong simp_implies_cong 

1357 
lemmas [split] = split_if 

20973  1358 

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