author  haftmann 
Thu, 02 Sep 2010 10:29:47 +0200  
changeset 39026  962d12bc546c 
parent 38972  cd747b068311 
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") 
38944  33 
"Tools/try.ML" 
15131  34 
begin 
2260  35 

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

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

38 

11750  39 
subsection {* Primitive logic *} 
40 

41 
subsubsection {* Core syntax *} 

2260  42 

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

46 

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

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

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

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

50 

7357  51 
typedecl bool 
923  52 

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

923  55 

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

38547  59 
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

60 

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

61 
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

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

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

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

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

66 

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

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

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

923  71 

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

72 

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

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

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

77 

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

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

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

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

81 

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

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

84 

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

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

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

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

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

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

91 

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

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

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

95 
disj (infixr "\<or>" 30) 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 

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

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

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

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

101 

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

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

104 

4868  105 
nonterminals 
923  106 
letbinds letbind 
107 
case_syn cases_syn 

108 

109 
syntax 

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

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

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

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

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

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

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

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

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

122 
translations 

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

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

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

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

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

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

130 

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

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

134 
notation (xsymbols) 

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

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

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

2372  138 

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

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

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

6340  143 

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

146 
Ex (binder "? " 10) and 

147 
Ex1 (binder "?! " 10) 

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

148 

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

149 

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

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

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

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

6289  159 

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

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

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

164 

165 

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

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

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

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

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

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

923  175 

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

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

923  179 

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

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

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

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

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

184 

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

187 

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

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

190 

191 
translations 

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

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

194 

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

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

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

197 

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

199 
fixes default :: 'a 
4868  200 

11750  201 

20944  202 
subsection {* Fundamental rules *} 
203 

20973  204 
subsubsection {* Equality *} 
20944  205 

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

15411  208 

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

15411  211 

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

18457  213 
by (erule subst) 
15411  214 

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

217 
shows "A = B" 

218 
by (unfold meq) (rule refl) 

15411  219 

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

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

225 
apply (rule trans) 

226 
apply (rule trans) 

227 
apply (rule sym) 

228 
apply assumption+ 

229 
done 

230 

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

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

232 

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

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

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

235 

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

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

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

238 

15411  239 

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

240 
subsubsection {* Congruence rules for application *} 
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 
text {* Similar to @{text AP_THM} in Gordon's HOL. *} 
15411  243 
lemma fun_cong: "(f::'a=>'b) = g ==> f(x)=g(x)" 
244 
apply (erule subst) 

245 
apply (rule refl) 

246 
done 

247 

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

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

251 
apply (rule refl) 

252 
done 

253 

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

256 
apply (rule refl) 

257 
done 

258 

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

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

262 
done 

263 

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

264 
ML {* val cong_tac = Cong_Tac.cong_tac @{thm cong} *} 
15411  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 

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

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

15411  271 

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

18457  273 
by (erule ssubst) 
15411  274 

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

18457  276 
by (erule iffD2) 
15411  277 

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

280 

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

282 
by (drule sym) (rule rev_iffD2) 

15411  283 

284 
lemma iffE: 

285 
assumes major: "P=Q" 

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

15411  289 

290 

20944  291 
subsubsection {*True*} 
15411  292 

293 
lemma TrueI: "True" 

21504  294 
unfolding True_def by (rule refl) 
15411  295 

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

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

15411  301 

302 

20944  303 
subsubsection {*Universal quantifier*} 
15411  304 

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

15411  307 

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

309 
apply (unfold All_def) 

310 
apply (rule eqTrueE) 

311 
apply (erule fun_cong) 

312 
done 

313 

314 
lemma allE: 

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

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

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

15411  319 

320 
lemma all_dupE: 

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

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

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

15411  325 

326 

21504  327 
subsubsection {* False *} 
328 

329 
text {* 

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

331 
logic before quantifiers! 

332 
*} 

15411  333 

334 
lemma FalseE: "False ==> P" 

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

337 
done 

15411  338 

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

15411  341 

342 

21504  343 
subsubsection {* Negation *} 
15411  344 

345 
lemma notI: 

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

350 
done 

15411  351 

352 
lemma False_not_True: "False ~= True" 

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

355 
done 

15411  356 

357 
lemma True_not_False: "True ~= False" 

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

360 
apply (erule False_neq_True) 

361 
done 

15411  362 

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

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

366 
apply assumption 

367 
done 

15411  368 

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

15411  371 

372 

20944  373 
subsubsection {*Implication*} 
15411  374 

375 
lemma impE: 

376 
assumes "P>Q" "P" "Q ==> R" 

377 
shows "R" 

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

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

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

17589  382 
by (iprover intro: mp) 
15411  383 

384 
lemma contrapos_nn: 

385 
assumes major: "~Q" 

386 
and minor: "P==>Q" 

387 
shows "~P" 

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

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

391 
lemma contrapos_pn: 

392 
assumes major: "Q" 

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

394 
shows "~P" 

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

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

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

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

401 
by (erule subst, erule ssubst, assumption) 

15411  402 

403 
(*still used in HOLCF*) 

404 
lemma rev_contrapos: 

405 
assumes pq: "P ==> Q" 

406 
and nq: "~Q" 

407 
shows "~P" 

408 
apply (rule nq [THEN contrapos_nn]) 

409 
apply (erule pq) 

410 
done 

411 

20944  412 
subsubsection {*Existential quantifier*} 
15411  413 

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

415 
apply (unfold Ex_def) 

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

419 
lemma exE: 

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

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

422 
shows "Q" 

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

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

427 

20944  428 
subsubsection {*Conjunction*} 
15411  429 

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

431 
apply (unfold and_def) 

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

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

436 
apply (unfold and_def) 

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

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

441 
apply (unfold and_def) 

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

445 
lemma conjE: 

446 
assumes major: "P&Q" 

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

448 
shows "R" 

449 
apply (rule minor) 

450 
apply (rule major [THEN conjunct1]) 

451 
apply (rule major [THEN conjunct2]) 

452 
done 

453 

454 
lemma context_conjI: 

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

15411  457 

458 

20944  459 
subsubsection {*Disjunction*} 
15411  460 

461 
lemma disjI1: "P ==> PQ" 

462 
apply (unfold or_def) 

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

466 
lemma disjI2: "Q ==> PQ" 

467 
apply (unfold or_def) 

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

471 
lemma disjE: 

472 
assumes major: "PQ" 

473 
and minorP: "P ==> R" 

474 
and minorQ: "Q ==> R" 

475 
shows "R" 

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

479 

20944  480 
subsubsection {*Classical logic*} 
15411  481 

482 
lemma classical: 

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

484 
shows "P" 

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

486 
apply assumption 

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

488 
apply (erule subst) 

489 
apply assumption 

490 
done 

491 

492 
lemmas ccontr = FalseE [THEN classical, standard] 

493 

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

495 
make elimination rules*) 

496 
lemma rev_notE: 

497 
assumes premp: "P" 

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

499 
shows "R" 

500 
apply (rule ccontr) 

501 
apply (erule notE [OF premnot premp]) 

502 
done 

503 

504 
(*Double negation law*) 

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

506 
apply (rule classical) 

507 
apply (erule notE) 

508 
apply assumption 

509 
done 

510 

511 
lemma contrapos_pp: 

512 
assumes p1: "Q" 

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

514 
shows "P" 

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

517 

20944  518 
subsubsection {*Unique existence*} 
15411  519 

520 
lemma ex1I: 

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

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

526 
lemma ex_ex1I: 

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

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

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

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

532 
lemma ex1E: 

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

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

535 
shows "R" 

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

537 
apply (erule conjE) 

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

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

542 
apply (erule ex1E) 

543 
apply (rule exI) 

544 
apply assumption 

545 
done 

546 

547 

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

550 
lemma the_equality: 

551 
assumes prema: "P a" 

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

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

554 
apply (rule trans [OF _ the_eq_trivial]) 

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

556 
apply (rule ext) 

557 
apply (rule iffI) 

558 
apply (erule premx) 

559 
apply (erule ssubst, rule prema) 

560 
done 

561 

562 
lemma theI: 

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

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

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

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

568 
apply (erule ex1E) 

569 
apply (erule theI) 

570 
apply (erule allE) 

571 
apply (erule mp) 

572 
apply assumption 

573 
done 

574 

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

576 
lemma theI2: 

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

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

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

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

583 
elim:allE impE) 

584 

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

588 
apply (erule ex1E) 

589 
apply (erule all_dupE) 

590 
apply (drule mp) 

591 
apply assumption 

592 
apply (erule ssubst) 

593 
apply (erule allE) 

594 
apply (erule mp) 

595 
apply assumption 

596 
done 

597 

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

599 
apply (rule the_equality) 

600 
apply (rule refl) 

601 
apply (erule sym) 

602 
done 

603 

604 

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

607 
lemma disjCI: 

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

609 
apply (rule classical) 

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

613 
lemma excluded_middle: "~P  P" 

17589  614 
by (iprover intro: disjCI) 
15411  615 

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

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

619 
*} 

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

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

623 
shows "Q" 

624 
apply (rule excluded_middle [THEN disjE]) 

625 
apply (erule prem2) 

626 
apply (erule prem1) 

627 
done 

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

628 

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

631 
assumes major: "P>Q" 

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

633 
shows "R" 

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

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

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

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

640 
default: would break old proofs.*) 

641 
lemma impCE': 

642 
assumes major: "P>Q" 

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

644 
shows "R" 

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

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

649 
(*Classical <> elimination. *) 

650 
lemma iffCE: 

651 
assumes major: "P=Q" 

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

653 
shows "R" 

654 
apply (rule major [THEN iffE]) 

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

658 
lemma exCI: 

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

660 
shows "EX x. P(x)" 

661 
apply (rule ccontr) 

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

665 

12386  666 
subsubsection {* Intuitionistic Reasoning *} 
667 

668 
lemma impE': 

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

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

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

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

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

675 
with 1 have Q by (rule impE) 

676 
with 2 show R . 

677 
qed 

678 

679 
lemma allE': 

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

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

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

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

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

686 
qed 

687 

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

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

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

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

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

694 
with 1 show R by (rule notE) 

695 
qed 

696 

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

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

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

699 

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

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

703 
and [Pure.intro] = exI disjI2 disjI1 

12386  704 

705 
lemmas [trans] = trans 

706 
and [sym] = sym not_sym 

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

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

709 
use "Tools/hologic.ML" 
23553  710 

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

711 

11750  712 
subsubsection {* Atomizing metalevel connectives *} 
713 

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

716 

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

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

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

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

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

737 
assume r: "A ==> False" 

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

739 
next 

740 
assume "~A" and A 

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

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

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

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

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

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

752 

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

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

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

758 
from conj show A by (rule conjunctionD1) 

759 
from conj show B by (rule conjunctionD2) 

760 
qed 

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

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

766 
from conj show B .. 

11953  767 
qed 
768 
qed 

769 

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

11750  773 

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

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

775 

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

776 
setup AtomizeElim.setup 
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 
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

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

780 

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

781 
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

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

783 

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

784 
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

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

786 

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

787 
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

788 

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

789 

20944  790 
subsection {* Package setup *} 
791 

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

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

793 

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

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

795 
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

796 
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

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

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

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

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

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

804 
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

805 
) 
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 
setup {* No_ATPs.setup *} 
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 

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

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

815 

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

817 
by (rule classical) iprover 

818 

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

821 

21151  822 
ML {* 
823 
structure Hypsubst = HypsubstFun( 

824 
struct 

825 
structure Simplifier = Simplifier 

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

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

831 
val imp_intr = @{thm impI} 

832 
val rev_mp = @{thm rev_mp} 

833 
val subst = @{thm subst} 

834 
val sym = @{thm sym} 

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

836 
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

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

841 
structure Classical = ClassicalFun( 

842 
struct 

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

845 
val swap = @{thm swap} 

846 
val classical = @{thm classical} 

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

849 
end); 

850 

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

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

852 
open Basic_Classical; 
22129  853 

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

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

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

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

859 

21009  860 
setup {* 
861 
let 

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

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

865 
SUBGOAL (fn (goal, i) => 

866 
if Term.exists_Const non_bool_eq goal 

867 
then Hypsubst.hyp_subst_tac i 

868 
else no_tac); 

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

875 

876 
declare iffI [intro!] 

877 
and notI [intro!] 

878 
and impI [intro!] 

879 
and disjCI [intro!] 

880 
and conjI [intro!] 

881 
and TrueI [intro!] 

882 
and refl [intro!] 

883 

884 
declare iffCE [elim!] 

885 
and FalseE [elim!] 

886 
and impCE [elim!] 

887 
and disjE [elim!] 

888 
and conjE [elim!] 

889 

890 
declare ex_ex1I [intro!] 

891 
and allI [intro!] 

892 
and the_equality [intro] 

893 
and exI [intro] 

894 

895 
declare exE [elim!] 

896 
allE [elim] 

897 

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

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

902 
apply (erule (1) meta_mp) 

903 
done 

10383  904 

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

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

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

907 

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

11977  910 

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

915 
shows R 

916 
apply (rule ex1E [OF major]) 

917 
apply (rule prem) 

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

920 
apply iprover 

921 
done 

20944  922 

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

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

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

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

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

934 
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac 

935 
val rep_cs = Classical.rep_cs 

936 
val cla_modifiers = Classical.cla_modifiers 

937 
val cla_meth' = Classical.cla_meth' 

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

21151  942 
setup Blast.setup 
943 

20944  944 

945 
subsubsection {* Simplifier *} 

12281  946 

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

948 

949 
lemma simp_thms: 

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

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

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

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

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

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

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

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

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

964 
and 

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

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

968 
"(P & True) = P" "(True & P) = P" 

969 
"(P & False) = False" "(False & P) = False" 

970 
"(P & P) = P" "(P & (P & Q)) = (P & Q)" 

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

972 
"(P  True) = True" "(True  P) = True" 

973 
"(P  False) = P" "(False  P) = P" 

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

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

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

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

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

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

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

985 

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

987 
by blast 

988 

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

990 
by blast 

991 

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

993 
by blast 

994 

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

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

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

12281  1000 

1001 
lemma conj_comms: 

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

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

12281  1005 

19174  1006 
lemmas conj_ac = conj_commute conj_left_commute conj_assoc 
1007 

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

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

12281  1012 

19174  1013 
lemmas disj_ac = disj_commute disj_left_commute disj_assoc 
1014 

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

12281  1017 

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

12281  1020 

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

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

12281  1024 

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

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

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

1028 

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

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

1031 

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

1034 

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

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

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

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

1041 
by blast 

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

1043 

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

1046 

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

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

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

1050 
by blast 

1051 

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

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

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

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

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

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

1059 

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

12281  1062 

1063 
text {* 

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

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

1066 

1067 
lemma conj_cong: 

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

17589  1069 
by iprover 
12281  1070 

1071 
lemma rev_conj_cong: 

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

17589  1073 
by iprover 
12281  1074 

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

1076 

1077 
lemma disj_cong: 

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

1079 
by blast 

1080 

1081 

1082 
text {* \medskip ifthenelse rules *} 

1083 

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

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

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

38525  1091 
by (unfold If_def) blast 
12281  1092 

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

38525  1094 
by (unfold If_def) blast 
12281  1095 

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

1097 
apply (rule case_split [of Q]) 

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

12281  1100 
done 
1101 

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

15481  1103 
by (simplesubst split_if, blast) 
12281  1104 

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

1105 
lemmas if_splits [no_atp] = split_if split_if_asm 
12281  1106 

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

15481  1108 
by (simplesubst split_if, blast) 
12281  1109 

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

15481  1111 
by (simplesubst split_if, blast) 
12281  1112 

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

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

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

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

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

12281  1124 

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

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

1128 
by (unfold Let_def) 

1129 

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

1131 
by (unfold Let_def) 

1132 

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

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

1136 
its premise. 

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

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

1138 

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

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

1141 

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

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

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

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

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

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

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

1149 

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

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

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

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

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

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

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

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

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

1159 

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

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

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

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

1163 
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

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

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

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

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

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

1170 
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

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

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

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

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

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

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

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

1179 

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

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

23553  1183 
using assms by blast 
20944  1184 

1185 
lemma iff_allI: 

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

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

23553  1188 
using assms by blast 
20944  1189 

1190 
lemma iff_exI: 

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

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

23553  1193 
using assms by blast 
20944  1194 

1195 
lemma all_comm: 

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

1197 
by blast 

1198 

1199 
lemma ex_comm: 

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

1201 
by blast 

1202 

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

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

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

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

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

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

1213 

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

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

1217 
let 

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

1219 
fun is_neq eq lhs rhs thm = 

1220 
(case Thm.prop_of thm of 

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

1222 
Not = HOLogic.Not andalso eq' = eq andalso 

1223 
r' aconv lhs andalso l' aconv rhs 

1224 
 _ => false); 

1225 
fun proc ss ct = 

1226 
(case Thm.term_of ct of 

1227 
eq $ lhs $ rhs => 

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

1229 
SOME thm => SOME (thm RS neq_to_EQ_False) 

1230 
 NONE => NONE) 

1231 
 _ => NONE); 

1232 
in proc end; 

1233 
*} 

1234 

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

1236 
let 

1237 
val (f_Let_unfold, x_Let_unfold) = 

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

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

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

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

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

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

1249 
 count_loose _ _ = 0; 

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

1251 
case t 

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

1253 
 _ => true; 

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

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

1258 
val thy = ProofContext.theory_of ctxt; 

1259 
val t = Thm.term_of ct; 

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

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

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

1263 
if is_Free x orelse is_Bound x orelse is_Const x 

1264 
then SOME @{thm Let_def} 

1265 
else 

1266 
let 

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

1268 
val cx = cterm_of thy x; 

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

1270 
val cf = cterm_of thy f; 

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

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

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

1274 
in (if (g aconv g') 

1275 
then 

1276 
let 

1277 
val rl = 

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

1279 
in SOME (rl OF [fx_g]) end 

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

1281 
else let 

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

1283 
val g'x = abs_g'$x; 

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

1287 
(g_Let_folded, cterm_of thy abs_g')] 

1288 
@{thm Let_folded}; 

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

1292 
 _ => NONE) 

1293 
end 

1294 
end *} 

24035  1295 

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

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

21151  1300 
next 
1301 
assume "PROP P" 

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

1305 
lemma ex_simps: 

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

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

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) = ((ALL x. P x) > Q)" 

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

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

1313 
by (iprover  blast)+ 

1314 

1315 
lemma all_simps: 

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

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

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) = ((EX x. P x) > Q)" 

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

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

1323 
by (iprover  blast)+ 

15481  1324 

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

1327 
True_implies_equals (*prune asms `True'*) 

1328 
if_True 

1329 
if_False 

1330 
if_cancel 

1331 
if_eq_cancel 

1332 
imp_disjL 

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

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

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

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

21671  1338 
conj_assoc 
1339 
disj_assoc 

1340 
de_Morgan_conj 

1341 
de_Morgan_disj 

1342 
imp_disj1 

1343 
imp_disj2 

1344 
not_imp 

1345 
disj_not1 

1346 
not_all 

1347 
not_ex 

1348 
cases_simp 

1349 
the_eq_trivial 

1350 
the_sym_eq_trivial 

1351 
ex_simps 

1352 
all_simps 

1353 
simp_thms 

1354 

1355 
lemmas [cong] = imp_cong simp_implies_cong 

1356 
lemmas [split] = split_if 

20973  1357 

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

20944  1360 
text {* Simplifies x assuming c and y assuming ~c *} 