author  wenzelm 
Tue, 19 Apr 2011 23:57:28 +0200  
changeset 42411  ff997038e8eb 
parent 42361  23f352990944 
child 42422  6a2837ddde4b 
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") 
26580
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset

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

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

30 
("~~/src/Tools/induct_tacs.ML") 
29505  31 
("Tools/recfun_codegen.ML") 
39036
dff91b90d74c
use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
blanchet
parents:
39014
diff
changeset

32 
("Tools/cnf_funcs.ML") 
40939
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40858
diff
changeset

33 
"~~/src/Tools/subtyping.ML" 
41827  34 
"~~/src/Tools/case_product.ML" 
15131  35 
begin 
2260  36 

31299  37 
setup {* Intuitionistic.method_setup @{binding iprover} *} 
40939
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40858
diff
changeset

38 
setup Subtyping.setup 
41827  39 
setup Case_Product.setup 
33316  40 

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

41 

11750  42 
subsection {* Primitive logic *} 
43 

44 
subsubsection {* Core syntax *} 

2260  45 

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

49 

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

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

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

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

53 

7357  54 
typedecl bool 
923  55 

11750  56 
judgment 
57 
Trueprop :: "bool => prop" ("(_)" 5) 

923  58 

11750  59 
consts 
7357  60 
True :: bool 
61 
False :: bool 

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

63 

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

64 
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

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

66 
implies :: "[bool, bool] => bool" (infixr ">" 25) 
38555  67 

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

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

69 

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

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

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

923  74 

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

75 

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

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

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

80 

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

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

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

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

84 

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

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

87 

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

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

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

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

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

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

94 

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

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

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

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

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

100 

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

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

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

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

104 

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

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

107 

41229
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
41184
diff
changeset

108 
nonterminal letbinds and letbind 
42057
3eba96ff3d3e
more selective strip_positions in case patterns  reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
41865
diff
changeset

109 
nonterminal case_pat and case_syn and cases_syn 
923  110 

111 
syntax 

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

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

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

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

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

42057
3eba96ff3d3e
more selective strip_positions in case patterns  reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
41865
diff
changeset

119 
"_case_syntax" :: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10) 
3eba96ff3d3e
more selective strip_positions in case patterns  reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
41865
diff
changeset

120 
"_case1" :: "[case_pat, 'b] => case_syn" ("(2_ =>/ _)" 10) 
3eba96ff3d3e
more selective strip_positions in case patterns  reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
41865
diff
changeset

121 
"" :: "case_syn => cases_syn" ("_") 
3eba96ff3d3e
more selective strip_positions in case patterns  reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
41865
diff
changeset

122 
"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/  _") 
3eba96ff3d3e
more selective strip_positions in case patterns  reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
41865
diff
changeset

123 
"_strip_positions" :: "'a => case_pat" ("_") 
3eba96ff3d3e
more selective strip_positions in case patterns  reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
41865
diff
changeset

124 

3eba96ff3d3e
more selective strip_positions in case patterns  reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
41865
diff
changeset

125 
syntax (xsymbols) 
3eba96ff3d3e
more selective strip_positions in case patterns  reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
41865
diff
changeset

126 
"_case1" :: "[case_pat, 'b] => case_syn" ("(2_ \<Rightarrow>/ _)" 10) 
923  127 

128 
translations 

35115  129 
"THE x. P" == "CONST The (%x. P)" 
923  130 

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

131 
print_translation {* 
35115  132 
[(@{const_syntax The}, fn [Abs abs] => 
42284  133 
let val (x, t) = Syntax_Trans.atomic_abs_tr' abs 
35115  134 
in Syntax.const @{syntax_const "_The"} $ x $ t end)] 
135 
*}  {* To avoid etacontraction of body *} 

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

136 

21524  137 
notation (xsymbols) 
138 
All (binder "\<forall>" 10) and 

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

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

2372  141 

21524  142 
notation (HTML output) 
143 
All (binder "\<forall>" 10) and 

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

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

6340  146 

21524  147 
notation (HOL) 
148 
All (binder "! " 10) and 

149 
Ex (binder "? " 10) and 

150 
Ex1 (binder "?! " 10) 

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

151 

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

152 

11750  153 
subsubsection {* Axioms and basic definitions *} 
2260  154 

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

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

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

6289  162 

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

163 
the_eq_trivial: "(THE x. x = a) = (a::'a)" 
923  164 

15380  165 
impI: "(P ==> Q) ==> P>Q" 
166 
mp: "[ P>Q; P ] ==> Q" 

167 

168 

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

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

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

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

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

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

923  178 

7357  179 
axioms 
180 
iff: "(P>Q) > (Q>P) > (P=Q)" 

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

923  182 

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

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

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

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

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

187 

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

190 

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

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

193 

194 
translations 

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

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

197 

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

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

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

200 

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

202 
fixes default :: 'a 
4868  203 

11750  204 

20944  205 
subsection {* Fundamental rules *} 
206 

20973  207 
subsubsection {* Equality *} 
20944  208 

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

15411  211 

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

15411  214 

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

18457  216 
by (erule subst) 
15411  217 

40715
3ba17f07b23c
lemma trans_sym allows singlestep "normalization" in Isar, e.g. via moreover/ultimately;
wenzelm
parents:
40582
diff
changeset

218 
lemma trans_sym [Pure.elim?]: "r = s ==> t = s ==> r = t" 
3ba17f07b23c
lemma trans_sym allows singlestep "normalization" in Isar, e.g. via moreover/ultimately;
wenzelm
parents:
40582
diff
changeset

219 
by (rule trans [OF _ sym]) 
3ba17f07b23c
lemma trans_sym allows singlestep "normalization" in Isar, e.g. via moreover/ultimately;
wenzelm
parents:
40582
diff
changeset

220 

20944  221 
lemma meta_eq_to_obj_eq: 
222 
assumes meq: "A == B" 

223 
shows "A = B" 

224 
by (unfold meq) (rule refl) 

15411  225 

21502  226 
text {* Useful with @{text erule} for proving equalities from known equalities. *} 
20944  227 
(* a = b 
15411  228 
  
229 
c = d *) 

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

231 
apply (rule trans) 

232 
apply (rule trans) 

233 
apply (rule sym) 

234 
apply assumption+ 

235 
done 

236 

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

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

238 

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

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

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

241 

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

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

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

244 

15411  245 

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

246 
subsubsection {* Congruence rules for application *} 
15411  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_THM} in Gordon's HOL. *} 
15411  249 
lemma fun_cong: "(f::'a=>'b) = g ==> f(x)=g(x)" 
250 
apply (erule subst) 

251 
apply (rule refl) 

252 
done 

253 

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

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

257 
apply (rule refl) 

258 
done 

259 

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

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 
lemma cong: "[ f = g; (x::'a) = y ] ==> f x = g y" 
15411  266 
apply (erule subst)+ 
267 
apply (rule refl) 

268 
done 

269 

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

270 
ML {* val cong_tac = Cong_Tac.cong_tac @{thm cong} *} 
15411  271 

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

272 

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

273 
subsubsection {* Equality of booleans  iff *} 
15411  274 

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

15411  277 

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

18457  279 
by (erule ssubst) 
15411  280 

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

18457  282 
by (erule iffD2) 
15411  283 

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

286 

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

288 
by (drule sym) (rule rev_iffD2) 

15411  289 

290 
lemma iffE: 

291 
assumes major: "P=Q" 

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

15411  295 

296 

20944  297 
subsubsection {*True*} 
15411  298 

299 
lemma TrueI: "True" 

21504  300 
unfolding True_def by (rule refl) 
15411  301 

21504  302 
lemma eqTrueI: "P ==> P = True" 
18457  303 
by (iprover intro: iffI TrueI) 
15411  304 

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

15411  307 

308 

20944  309 
subsubsection {*Universal quantifier*} 
15411  310 

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

15411  313 

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

315 
apply (unfold All_def) 

316 
apply (rule eqTrueE) 

317 
apply (erule fun_cong) 

318 
done 

319 

320 
lemma allE: 

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

21504  322 
and minor: "P(x) ==> R" 
323 
shows R 

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

15411  325 

326 
lemma all_dupE: 

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

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

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

15411  331 

332 

21504  333 
subsubsection {* False *} 
334 

335 
text {* 

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

337 
logic before quantifiers! 

338 
*} 

15411  339 

340 
lemma FalseE: "False ==> P" 

21504  341 
apply (unfold False_def) 
342 
apply (erule spec) 

343 
done 

15411  344 

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

15411  347 

348 

21504  349 
subsubsection {* Negation *} 
15411  350 

351 
lemma notI: 

21504  352 
assumes "P ==> False" 
15411  353 
shows "~P" 
21504  354 
apply (unfold not_def) 
355 
apply (iprover intro: impI assms) 

356 
done 

15411  357 

358 
lemma False_not_True: "False ~= True" 

21504  359 
apply (rule notI) 
360 
apply (erule False_neq_True) 

361 
done 

15411  362 

363 
lemma True_not_False: "True ~= False" 

21504  364 
apply (rule notI) 
365 
apply (drule sym) 

366 
apply (erule False_neq_True) 

367 
done 

15411  368 

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

21504  370 
apply (unfold not_def) 
371 
apply (erule mp [THEN FalseE]) 

372 
apply assumption 

373 
done 

15411  374 

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

15411  377 

378 

20944  379 
subsubsection {*Implication*} 
15411  380 

381 
lemma impE: 

382 
assumes "P>Q" "P" "Q ==> R" 

383 
shows "R" 

23553  384 
by (iprover intro: assms mp) 
15411  385 

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

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

17589  388 
by (iprover intro: mp) 
15411  389 

390 
lemma contrapos_nn: 

391 
assumes major: "~Q" 

392 
and minor: "P==>Q" 

393 
shows "~P" 

17589  394 
by (iprover intro: notI minor major [THEN notE]) 
15411  395 

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

397 
lemma contrapos_pn: 

398 
assumes major: "Q" 

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

400 
shows "~P" 

17589  401 
by (iprover intro: notI minor major notE) 
15411  402 

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

21250  404 
by (erule contrapos_nn) (erule sym) 
405 

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

407 
by (erule subst, erule ssubst, assumption) 

15411  408 

409 
(*still used in HOLCF*) 

410 
lemma rev_contrapos: 

411 
assumes pq: "P ==> Q" 

412 
and nq: "~Q" 

413 
shows "~P" 

414 
apply (rule nq [THEN contrapos_nn]) 

415 
apply (erule pq) 

416 
done 

417 

20944  418 
subsubsection {*Existential quantifier*} 
15411  419 

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

421 
apply (unfold Ex_def) 

17589  422 
apply (iprover intro: allI allE impI mp) 
15411  423 
done 
424 

425 
lemma exE: 

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

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

428 
shows "Q" 

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

17589  430 
apply (iprover intro: impI [THEN allI] minor) 
15411  431 
done 
432 

433 

20944  434 
subsubsection {*Conjunction*} 
15411  435 

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

437 
apply (unfold and_def) 

17589  438 
apply (iprover intro: impI [THEN allI] mp) 
15411  439 
done 
440 

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

442 
apply (unfold and_def) 

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

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

447 
apply (unfold and_def) 

17589  448 
apply (iprover intro: impI dest: spec mp) 
15411  449 
done 
450 

451 
lemma conjE: 

452 
assumes major: "P&Q" 

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

454 
shows "R" 

455 
apply (rule minor) 

456 
apply (rule major [THEN conjunct1]) 

457 
apply (rule major [THEN conjunct2]) 

458 
done 

459 

460 
lemma context_conjI: 

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

15411  463 

464 

20944  465 
subsubsection {*Disjunction*} 
15411  466 

467 
lemma disjI1: "P ==> PQ" 

468 
apply (unfold or_def) 

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

472 
lemma disjI2: "Q ==> PQ" 

473 
apply (unfold or_def) 

17589  474 
apply (iprover intro: allI impI mp) 
15411  475 
done 
476 

477 
lemma disjE: 

478 
assumes major: "PQ" 

479 
and minorP: "P ==> R" 

480 
and minorQ: "Q ==> R" 

481 
shows "R" 

17589  482 
by (iprover intro: minorP minorQ impI 
15411  483 
major [unfolded or_def, THEN spec, THEN mp, THEN mp]) 
484 

485 

20944  486 
subsubsection {*Classical logic*} 
15411  487 

488 
lemma classical: 

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

490 
shows "P" 

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

492 
apply assumption 

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

494 
apply (erule subst) 

495 
apply assumption 

496 
done 

497 

498 
lemmas ccontr = FalseE [THEN classical, standard] 

499 

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

501 
make elimination rules*) 

502 
lemma rev_notE: 

503 
assumes premp: "P" 

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

505 
shows "R" 

506 
apply (rule ccontr) 

507 
apply (erule notE [OF premnot premp]) 

508 
done 

509 

510 
(*Double negation law*) 

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

512 
apply (rule classical) 

513 
apply (erule notE) 

514 
apply assumption 

515 
done 

516 

517 
lemma contrapos_pp: 

518 
assumes p1: "Q" 

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

520 
shows "P" 

17589  521 
by (iprover intro: classical p1 p2 notE) 
15411  522 

523 

20944  524 
subsubsection {*Unique existence*} 
15411  525 

526 
lemma ex1I: 

23553  527 
assumes "P a" "!!x. P(x) ==> x=a" 
15411  528 
shows "EX! x. P(x)" 
23553  529 
by (unfold Ex1_def, iprover intro: assms exI conjI allI impI) 
15411  530 

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

532 
lemma ex_ex1I: 

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

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

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

17589  536 
by (iprover intro: ex_prem [THEN exE] ex1I eq) 
15411  537 

538 
lemma ex1E: 

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

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

541 
shows "R" 

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

543 
apply (erule conjE) 

17589  544 
apply (iprover intro: minor) 
15411  545 
done 
546 

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

548 
apply (erule ex1E) 

549 
apply (rule exI) 

550 
apply assumption 

551 
done 

552 

553 

20944  554 
subsubsection {*THE: definite description operator*} 
15411  555 

556 
lemma the_equality: 

557 
assumes prema: "P a" 

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

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

560 
apply (rule trans [OF _ the_eq_trivial]) 

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

562 
apply (rule ext) 

563 
apply (rule iffI) 

564 
apply (erule premx) 

565 
apply (erule ssubst, rule prema) 

566 
done 

567 

568 
lemma theI: 

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

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

23553  571 
by (iprover intro: assms the_equality [THEN ssubst]) 
15411  572 

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

574 
apply (erule ex1E) 

575 
apply (erule theI) 

576 
apply (erule allE) 

577 
apply (erule mp) 

578 
apply assumption 

579 
done 

580 

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

582 
lemma theI2: 

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

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

23553  585 
by (iprover intro: assms theI) 
15411  586 

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

589 
elim:allE impE) 

590 

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

594 
apply (erule ex1E) 

595 
apply (erule all_dupE) 

596 
apply (drule mp) 

597 
apply assumption 

598 
apply (erule ssubst) 

599 
apply (erule allE) 

600 
apply (erule mp) 

601 
apply assumption 

602 
done 

603 

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

605 
apply (rule the_equality) 

606 
apply (rule refl) 

607 
apply (erule sym) 

608 
done 

609 

610 

20944  611 
subsubsection {*Classical intro rules for disjunction and existential quantifiers*} 
15411  612 

613 
lemma disjCI: 

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

615 
apply (rule classical) 

23553  616 
apply (iprover intro: assms disjI1 disjI2 notI elim: notE) 
15411  617 
done 
618 

619 
lemma excluded_middle: "~P  P" 

17589  620 
by (iprover intro: disjCI) 
15411  621 

20944  622 
text {* 
623 
case distinction as a natural deduction rule. 

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

625 
*} 

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

626 
lemma case_split [case_names True False]: 
15411  627 
assumes prem1: "P ==> Q" 
628 
and prem2: "~P ==> Q" 

629 
shows "Q" 

630 
apply (rule excluded_middle [THEN disjE]) 

631 
apply (erule prem2) 

632 
apply (erule prem1) 

633 
done 

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

634 

15411  635 
(*Classical implies (>) elimination. *) 
636 
lemma impCE: 

637 
assumes major: "P>Q" 

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

639 
shows "R" 

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

17589  641 
apply (iprover intro: minor major [THEN mp])+ 
15411  642 
done 
643 

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

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

646 
default: would break old proofs.*) 

647 
lemma impCE': 

648 
assumes major: "P>Q" 

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

650 
shows "R" 

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

17589  652 
apply (iprover intro: minor major [THEN mp])+ 
15411  653 
done 
654 

655 
(*Classical <> elimination. *) 

656 
lemma iffCE: 

657 
assumes major: "P=Q" 

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

659 
shows "R" 

660 
apply (rule major [THEN iffE]) 

17589  661 
apply (iprover intro: minor elim: impCE notE) 
15411  662 
done 
663 

664 
lemma exCI: 

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

666 
shows "EX x. P(x)" 

667 
apply (rule ccontr) 

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

671 

12386  672 
subsubsection {* Intuitionistic Reasoning *} 
673 

674 
lemma impE': 

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

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

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

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

678 
shows R 
12386  679 
proof  
680 
from 3 and 1 have P . 

681 
with 1 have Q by (rule impE) 

682 
with 2 show R . 

683 
qed 

684 

685 
lemma allE': 

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

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

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

688 
shows Q 
12386  689 
proof  
690 
from 1 have "P x" by (rule spec) 

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

692 
qed 

693 

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

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

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

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

697 
shows R 
12386  698 
proof  
699 
from 2 and 1 have P . 

700 
with 1 show R by (rule notE) 

701 
qed 

702 

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

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

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

705 

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

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

709 
and [Pure.intro] = exI disjI2 disjI1 

12386  710 

711 
lemmas [trans] = trans 

712 
and [sym] = sym not_sym 

15801  713 
and [Pure.elim?] = iffD1 iffD2 impE 
11750  714 

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

715 
use "Tools/hologic.ML" 
23553  716 

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

717 

11750  718 
subsubsection {* Atomizing metalevel connectives *} 
719 

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

722 

11750  723 
lemma atomize_all [atomize]: "(!!x. P x) == Trueprop (ALL x. P x)" 
12003  724 
proof 
9488  725 
assume "!!x. P x" 
23389  726 
then show "ALL x. P x" .. 
9488  727 
next 
728 
assume "ALL x. P x" 

23553  729 
then show "!!x. P x" by (rule allE) 
9488  730 
qed 
731 

11750  732 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
12003  733 
proof 
9488  734 
assume r: "A ==> B" 
10383  735 
show "A > B" by (rule impI) (rule r) 
9488  736 
next 
737 
assume "A > B" and A 

23553  738 
then show B by (rule mp) 
9488  739 
qed 
740 

14749  741 
lemma atomize_not: "(A ==> False) == Trueprop (~A)" 
742 
proof 

743 
assume r: "A ==> False" 

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

745 
next 

746 
assume "~A" and A 

23553  747 
then show False by (rule notE) 
14749  748 
qed 
749 

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

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

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

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

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

758 

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

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

761 
assume conj: "A &&& B" 
19121  762 
show "A & B" 
763 
proof (rule conjI) 

764 
from conj show A by (rule conjunctionD1) 

765 
from conj show B by (rule conjunctionD2) 

766 
qed 

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

769 
show "A &&& B" 
19121  770 
proof  
771 
from conj show A .. 

772 
from conj show B .. 

11953  773 
qed 
774 
qed 

775 

12386  776 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
18832  777 
and [symmetric, defn] = atomize_all atomize_imp atomize_eq 
12386  778 

11750  779 

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

780 
subsubsection {* Atomizing elimination rules *} 
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 
setup AtomizeElim.setup 
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_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

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_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

788 
by rule iprover+ 
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 
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

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

792 

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

793 
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

794 

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

795 

20944  796 
subsection {* Package setup *} 
797 

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

798 
subsubsection {* Sledgehammer setup *} 
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 
text {* 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset

801 
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

802 
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

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

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

805 

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

806 
ML {* 
36297
6b2b9516a3cd
removed obsolete Named_Thm_Set  Named_Thms provides efficient member operation;
wenzelm
parents:
36246
diff
changeset

807 
structure No_ATPs = Named_Thms 
35828
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 
val name = "no_atp" 
36060
4d27652ffb40
reintroduce efficient set structure to collect "no_atp" theorems
blanchet
parents:
35828
diff
changeset

810 
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

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

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

813 

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

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

815 

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

816 

11750  817 
subsubsection {* Classical Reasoner setup *} 
9529  818 

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

821 

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

823 
by (rule classical) iprover 

824 

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

827 

21151  828 
ML {* 
829 
structure Hypsubst = HypsubstFun( 

830 
struct 

831 
structure Simplifier = Simplifier 

21218  832 
val dest_eq = HOLogic.dest_eq 
21151  833 
val dest_Trueprop = HOLogic.dest_Trueprop 
834 
val dest_imp = HOLogic.dest_imp 

26411  835 
val eq_reflection = @{thm eq_reflection} 
836 
val rev_eq_reflection = @{thm meta_eq_to_obj_eq} 

837 
val imp_intr = @{thm impI} 

838 
val rev_mp = @{thm rev_mp} 

839 
val subst = @{thm subst} 

840 
val sym = @{thm sym} 

22129  841 
val thin_refl = @{thm thin_refl}; 
21151  842 
end); 
21671  843 
open Hypsubst; 
21151  844 

845 
structure Classical = ClassicalFun( 

846 
struct 

26411  847 
val imp_elim = @{thm imp_elim} 
848 
val not_elim = @{thm notE} 

849 
val swap = @{thm swap} 

850 
val classical = @{thm classical} 

21151  851 
val sizef = Drule.size_of_thm 
852 
val hyp_subst_tacs = [Hypsubst.hyp_subst_tac] 

853 
end); 

854 

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

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

856 
open Basic_Classical; 
22129  857 

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

859 
(Scan.succeed "Classical.claset_of (ML_Context.the_local_context ())"); 
21151  860 
*} 
861 

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

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

863 

21009  864 
setup {* 
865 
let 

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

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

869 
SUBGOAL (fn (goal, i) => 

870 
if Term.exists_Const non_bool_eq goal 

871 
then Hypsubst.hyp_subst_tac i 

872 
else no_tac); 

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

879 

880 
declare iffI [intro!] 

881 
and notI [intro!] 

882 
and impI [intro!] 

883 
and disjCI [intro!] 

884 
and conjI [intro!] 

885 
and TrueI [intro!] 

886 
and refl [intro!] 

887 

888 
declare iffCE [elim!] 

889 
and FalseE [elim!] 

890 
and impCE [elim!] 

891 
and disjE [elim!] 

892 
and conjE [elim!] 

893 

894 
declare ex_ex1I [intro!] 

895 
and allI [intro!] 

896 
and the_equality [intro] 

897 
and exI [intro] 

898 

899 
declare exE [elim!] 

900 
allE [elim] 

901 

22377  902 
ML {* val HOL_cs = @{claset} *} 
19162  903 

20223  904 
lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P" 
905 
apply (erule swap) 

906 
apply (erule (1) meta_mp) 

907 
done 

10383  908 

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

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

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

911 

41865
4e8483cc2cc5
declare ext [intro]: Extensionality now available by default
paulson
parents:
41827
diff
changeset

912 
declare ext [intro] 
4e8483cc2cc5
declare ext [intro]: Extensionality now available by default
paulson
parents:
41827
diff
changeset

913 

12386  914 
lemmas [intro?] = ext 
915 
and [elim?] = ex1_implies_ex 

11977  916 

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

921 
shows R 

922 
apply (rule ex1E [OF major]) 

923 
apply (rule prem) 

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

926 
apply iprover 

927 
done 

20944  928 

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

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

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

934 
val equality_name = @{const_name HOL.eq} 
22993  935 
val not_name = @{const_name Not} 
26411  936 
val notE = @{thm notE} 
937 
val ccontr = @{thm ccontr} 

21151  938 
val contr_tac = Classical.contr_tac 
939 
val dup_intr = Classical.dup_intr 

940 
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac 

941 
val rep_cs = Classical.rep_cs 

942 
val cla_modifiers = Classical.cla_modifiers 

943 
val cla_meth' = Classical.cla_meth' 

25388  944 
); 
21671  945 
val blast_tac = Blast.blast_tac; 
20944  946 
*} 
947 

21151  948 
setup Blast.setup 
949 

20944  950 

951 
subsubsection {* Simplifier *} 

12281  952 

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

954 

955 
lemma simp_thms: 

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

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

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

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

960 
"(P  ~P) = True" "(~P  P) = True" 
12281  961 
"(x = x) = True" 
32068  962 
and not_True_eq_False [code]: "(\<not> True) = False" 
963 
and not_False_eq_True [code]: "(\<not> False) = True" 

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

965 
"(~P) ~= P" "P ~= (~P)" 
20944  966 
"(True=P) = P" 
967 
and eq_True: "(P = True) = P" 

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

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

970 
and 

12281  971 
"(True > P) = P" "(False > P) = True" 
972 
"(P > True) = True" "(P > P) = True" 

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

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

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

976 
"(P & P) = P" "(P & (P & Q)) = (P & Q)" 

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

978 
"(P  True) = True" "(True  P) = True" 

979 
"(P  False) = P" "(False  P) = P" 

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

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

982 
and 
12281  983 
"!!P. (EX x. x=t & P(x)) = P(t)" 
984 
"!!P. (EX x. t=x & P(x)) = P(t)" 

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

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

986 
"!!P. (ALL x. t=x > P(x)) = P(t)" 
17589  987 
by (blast, blast, blast, blast, blast, iprover+) 
13421  988 

14201  989 
lemma disj_absorb: "(A  A) = A" 
990 
by blast 

991 

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

993 
by blast 

994 

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

996 
by blast 

997 

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

999 
by blast 

1000 

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

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

1003 
and eq_left_commute: "(P=(Q=R)) = (Q=(P=R))" 
17589  1004 
and eq_assoc: "((P=Q)=R) = (P=(Q=R))" by (iprover, blast+) 
1005 
lemma neq_commute: "(a~=b) = (b~=a)" by iprover 

12281  1006 

1007 
lemma conj_comms: 

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

1008 
shows conj_commute: "(P&Q) = (Q&P)" 
17589  1009 
and conj_left_commute: "(P&(Q&R)) = (Q&(P&R))" by iprover+ 
1010 
lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by iprover 

12281  1011 

19174  1012 
lemmas conj_ac = conj_commute conj_left_commute conj_assoc 
1013 

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

1015 
shows disj_commute: "(PQ) = (QP)" 
17589  1016 
and disj_left_commute: "(P(QR)) = (Q(PR))" by iprover+ 
1017 
lemma disj_assoc: "((PQ)R) = (P(QR))" by iprover 

12281  1018 

19174  1019 
lemmas disj_ac = disj_commute disj_left_commute disj_assoc 
1020 

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

12281  1023 

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

12281  1026 

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

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

12281  1030 

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

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

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

1034 

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

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

1037 

21151  1038 
lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P > Q) = (P' > Q'))" 
1039 
by iprover 

1040 

17589  1041 
lemma de_Morgan_disj: "(~(P  Q)) = (~P & ~Q)" by iprover 
12281  1042 
lemma de_Morgan_conj: "(~(P & Q)) = (~P  ~Q)" by blast 
1043 
lemma not_imp: "(~(P > Q)) = (P & ~Q)" by blast 

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

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

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

1047 
by blast 

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

1049 

17589  1050 
lemma iff_conv_conj_imp: "(P = Q) = ((P > Q) & (Q > P))" by iprover 
12281  1051 

1052 

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

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

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

1056 
by blast 

1057 

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

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

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

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

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

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

1065 

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

12281  1068 

1069 
text {* 

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

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

1072 

1073 
lemma conj_cong: 

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

17589  1075 
by iprover 
12281  1076 

1077 
lemma rev_conj_cong: 

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

17589  1079 
by iprover 
12281  1080 

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

1082 

1083 
lemma disj_cong: 

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

1085 
by blast 

1086 

1087 

1088 
text {* \medskip ifthenelse rules *} 

1089 

32068  1090 
lemma if_True [code]: "(if True then x else y) = x" 
38525  1091 
by (unfold If_def) blast 
12281  1092 

32068  1093 
lemma if_False [code]: "(if False then x else y) = y" 
38525  1094 
by (unfold If_def) blast 
12281  1095 

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

38525  1097 
by (unfold If_def) blast 
12281  1098 

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

38525  1100 
by (unfold If_def) blast 
12281  1101 

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

1103 
apply (rule case_split [of Q]) 

15481  1104 
apply (simplesubst if_P) 
1105 
prefer 3 apply (simplesubst if_not_P, blast+) 

12281  1106 
done 
1107 

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

15481  1109 
by (simplesubst split_if, blast) 
12281  1110 

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

1111 
lemmas if_splits [no_atp] = split_if split_if_asm 
12281  1112 

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

15481  1114 
by (simplesubst split_if, blast) 
12281  1115 

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

15481  1117 
by (simplesubst split_if, blast) 
12281  1118 

41792
ff3cb0c418b7
renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
blanchet
parents:
41636
diff
changeset

1119 
lemma if_bool_eq_conj: 
ff3cb0c418b7
renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
blanchet
parents:
41636
diff
changeset

1120 
"(if P then Q else R) = ((P>Q) & (~P>R))" 
19796  1121 
 {* This form is useful for expanding @{text "if"}s on the RIGHT of the @{text "==>"} symbol. *} 
12281  1122 
by (rule split_if) 
1123 

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

19796  1125 
 {* And this form is useful for expanding @{text "if"}s on the LEFT. *} 
15481  1126 
apply (simplesubst split_if, blast) 
12281  1127 
done 
1128 

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

12281  1131 

15423  1132 
text {* \medskip let rules for simproc *} 
1133 

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

1135 
by (unfold Let_def) 

1136 

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

1138 
by (unfold Let_def) 

1139 

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

1140 
text {* 
16999  1141 
The following copy of the implication operator is useful for 
1142 
finetuning congruence rules. It instructs the simplifier to simplify 

1143 
its premise. 

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

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

1145 

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

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

1148 

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

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

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

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

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

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

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

1156 

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

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

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

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

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

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

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

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

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

1166 

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

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

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

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

1170 
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

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

1172 
assume PQ: "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' [symmetric] and P' have "PROP P" 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

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

1177 
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

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

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

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

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

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

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

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

1186 

20944  1187 
lemma uncurry: 
1188 
assumes "P \<longrightarrow> Q \<longrightarrow> R" 

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

23553  1190 
using assms by blast 
20944  1191 

1192 
lemma iff_allI: 

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

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

23553  1195 
using assms by blast 
20944  1196 

1197 
lemma iff_exI: 

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

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

23553  1200 
using assms by blast 
20944  1201 

1202 
lemma all_comm: 

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

1204 
by blast 

1205 

1206 
lemma ex_comm: 

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

1208 
by blast 

1209 

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

1210 
use "Tools/simpdata.ML" 
21671  1211 
ML {* open Simpdata *} 
1212 

21151  1213 
setup {* 
1214 
Simplifier.method_setup Splitter.split_modifiers 

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

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

1217 
#> clasimp_setup 
21151  1218 
#> EqSubst.setup 
1219 
*} 

1220 

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

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

1224 
let 

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

1226 
fun is_neq eq lhs rhs thm = 

1227 
(case Thm.prop_of thm of 

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

1229 
Not = HOLogic.Not andalso eq' = eq andalso 

1230 
r' aconv lhs andalso l' aconv rhs 

1231 
 _ => false); 

1232 
fun proc ss ct = 

1233 
(case Thm.term_of ct of 

1234 
eq $ lhs $ rhs => 

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

1236 
SOME thm => SOME (thm RS neq_to_EQ_False) 

1237 
 NONE => NONE) 

1238 
 _ => NONE); 

1239 
in proc end; 

1240 
*} 

1241 

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

1243 
let 

1244 
val (f_Let_unfold, x_Let_unfold) = 

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

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

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

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

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

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

1256 
 count_loose _ _ = 0; 

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

1258 
case t 

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

1260 
 _ => true; 

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

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

42361  1265 
val thy = Proof_Context.theory_of ctxt; 
28741  1266 
val t = Thm.term_of ct; 
1267 
val ([t'], ctxt') = Variable.import_terms false [t] ctxt; 

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

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

1270 
if is_Free x orelse is_Bound x orelse is_Const x 

1271 
then SOME @{thm Let_def} 

1272 
else 

1273 
let 

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

1275 
val cx = cterm_of thy x; 

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

1277 
val cf = cterm_of thy f; 

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

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

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

1281 
in (if (g aconv g') 

1282 
then 

1283 
let 

1284 
val rl = 

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

1286 
in SOME (rl OF [fx_g]) end 

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

1288 
else let 

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

1290 
val g'x = abs_g'$x; 

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

1294 
(g_Let_folded, cterm_of thy abs_g')] 

1295 
@{thm Let_folded}; 

36945  1296 
in SOME (rl OF [Thm.transitive fx_g g_g'x]) 
28741  1297 
end) 
1298 
end 

1299 
 _ => NONE) 

1300 
end 

1301 
end *} 

24035  1302 

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

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

21151  1307 
next 
1308 
assume "PROP P" 

23389  1309 
then show "PROP P" . 
21151  1310 
qed 
1311 

1312 
lemma ex_simps: 

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

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

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

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

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

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

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

1320 
by (iprover  blast)+ 

1321 

1322 
lemma all_simps: 

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

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

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

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

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

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

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

1330 
by (iprover  blast)+ 

15481  1331 

21671  1332 
lemmas [simp] = 
1333 
triv_forall_equality (*prunes params*) 

1334 
True_implies_equals (*prune asms `True'*) 

1335 
if_True 

1336 
if_False 

1337 
if_cancel 

1338 
if_eq_cancel 

1339 
imp_disjL 

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

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

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

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

21671  1345 
conj_assoc 
1346 
disj_assoc 

1347 
de_Morgan_conj 

1348 
de_Morgan_disj 

1349 
imp_disj1 

1350 
imp_disj2 

1351 
not_imp 

1352 
disj_not1 

1353 
not_all 

1354 
not_ex 

1355 
cases_simp 

1356 
the_eq_trivial 

1357 
the_sym_eq_trivial 

f7d652ffef09
removed legacy ML bindings;
we&# 