author  wenzelm 
Fri, 16 Mar 2012 22:31:19 +0100  
changeset 46973  d68798000e46 
parent 46950  d0181abdbdac 
child 47657  1ba213363d0c 
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" 
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46497
diff
changeset

9 
keywords 
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46497
diff
changeset

10 
"print_coercions" "print_coercion_maps" "print_claset" "print_induct_rules" :: diag 
23163  11 
uses 
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28856
diff
changeset

12 
("Tools/hologic.ML") 
23171  13 
"~~/src/Tools/IsaPlanner/zipper.ML" 
14 
"~~/src/Tools/IsaPlanner/isand.ML" 

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

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

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

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

18 
"~~/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

19 
"~~/src/Tools/cong_tac.ML" 
23263  20 
"~~/src/Provers/hypsubst.ML" 
21 
"~~/src/Provers/splitter.ML" 

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

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

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

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

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

28 
("Tools/simpdata.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" 
45014
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
44921
diff
changeset

31 
("~~/src/Tools/induction.ML") 
27326
d3beec370964
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
27212
diff
changeset

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

33 
("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

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

31299  38 
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

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

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

42 

11750  43 
subsection {* Primitive logic *} 
44 

45 
subsubsection {* Core syntax *} 

2260  46 

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

50 

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

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

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

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

54 

7357  55 
typedecl bool 
923  56 

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

923  59 

46973  60 
axiomatization 
61 
implies :: "[bool, bool] => bool" (infixr ">" 25) and 

62 
eq :: "['a, 'a] => bool" (infixl "=" 50) and 

63 
The :: "('a => bool) => 'a" 

64 

11750  65 
consts 
7357  66 
True :: bool 
67 
False :: bool 

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

69 

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

70 
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

71 
disj :: "[bool, bool] => bool" (infixr "" 30) 
38555  72 

7357  73 
All :: "('a => bool) => bool" (binder "ALL " 10) 
74 
Ex :: "('a => bool) => bool" (binder "EX " 10) 

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

923  76 

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

77 

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

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

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

82 

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

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

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

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

86 

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

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

89 

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

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

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

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

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

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

96 

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

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

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

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

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

102 

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

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

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

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

106 

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

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

109 

46973  110 
syntax "_The" :: "[pttrn, bool] => 'a" ("(3THE _./ _)" [0, 10] 10) 
111 
translations "THE x. P" == "CONST The (%x. P)" 

46125
00cd193a48dc
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
45654
diff
changeset

112 
print_translation {* 
00cd193a48dc
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
45654
diff
changeset

113 
[(@{const_syntax The}, fn [Abs abs] => 
00cd193a48dc
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
45654
diff
changeset

114 
let val (x, t) = Syntax_Trans.atomic_abs_tr' abs 
00cd193a48dc
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
45654
diff
changeset

115 
in Syntax.const @{syntax_const "_The"} $ x $ t end)] 
00cd193a48dc
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
45654
diff
changeset

116 
*}  {* To avoid etacontraction of body *} 
923  117 

46125
00cd193a48dc
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
45654
diff
changeset

118 
nonterminal letbinds and letbind 
923  119 
syntax 
7357  120 
"_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) 
121 
"" :: "letbind => letbinds" ("_") 

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

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

46125
00cd193a48dc
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
45654
diff
changeset

125 
nonterminal case_syn and cases_syn 
00cd193a48dc
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
45654
diff
changeset

126 
syntax 
00cd193a48dc
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
45654
diff
changeset

127 
"_case_syntax" :: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10) 
00cd193a48dc
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
45654
diff
changeset

128 
"_case1" :: "['a, 'b] => case_syn" ("(2_ =>/ _)" 10) 
00cd193a48dc
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
45654
diff
changeset

129 
"" :: "case_syn => cases_syn" ("_") 
00cd193a48dc
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
45654
diff
changeset

130 
"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/  _") 
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

131 
syntax (xsymbols) 
46125
00cd193a48dc
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
45654
diff
changeset

132 
"_case1" :: "['a, 'b] => case_syn" ("(2_ \<Rightarrow>/ _)" 10) 
13763
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset

133 

21524  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 

46973  152 
axiomatization where 
153 
refl: "t = (t::'a)" and 

154 
subst: "s = t \<Longrightarrow> P s \<Longrightarrow> P t" and 

155 
ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)" 

15380  156 
 {*Extensionality is built into the metalogic, and this rule expresses 
157 
a related property. It is an etaexpanded version of the traditional 

46973  158 
rule, and similar to the ABS rule of HOL*} and 
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 

46973  162 
axiomatization where 
163 
impI: "(P ==> Q) ==> P>Q" and 

164 
mp: "[ P>Q; P ] ==> Q" and 

15380  165 

46973  166 
iff: "(P>Q) > (Q>P) > (P=Q)" and 
167 
True_or_False: "(P=True)  (P=False)" 

15380  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 

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

923  181 

46973  182 
definition Let :: "'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b" 
183 
where "Let s f \<equiv> f s" 

38525  184 

185 
translations 

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

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

188 

46973  189 
axiomatization undefined :: 'a 
22481
79c2724c36b5
added class "default" and expansion axioms for undefined
haftmann
parents:
22473
diff
changeset

190 

46973  191 
class default = fixes default :: 'a 
4868  192 

11750  193 

20944  194 
subsection {* Fundamental rules *} 
195 

20973  196 
subsubsection {* Equality *} 
20944  197 

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

15411  200 

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

15411  203 

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

18457  205 
by (erule subst) 
15411  206 

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

207 
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

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

209 

20944  210 
lemma meta_eq_to_obj_eq: 
211 
assumes meq: "A == B" 

212 
shows "A = B" 

213 
by (unfold meq) (rule refl) 

15411  214 

21502  215 
text {* Useful with @{text erule} for proving equalities from known equalities. *} 
20944  216 
(* a = b 
15411  217 
  
218 
c = d *) 

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

220 
apply (rule trans) 

221 
apply (rule trans) 

222 
apply (rule sym) 

223 
apply assumption+ 

224 
done 

225 

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

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

227 

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

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

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

230 

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

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

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

233 

15411  234 

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

235 
subsubsection {* Congruence rules for application *} 
15411  236 

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

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

240 
apply (rule refl) 

241 
done 

242 

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

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

246 
apply (rule refl) 

247 
done 

248 

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

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 
lemma cong: "[ f = g; (x::'a) = y ] ==> f x = g y" 
15411  255 
apply (erule subst)+ 
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 
ML {* val cong_tac = Cong_Tac.cong_tac @{thm cong} *} 
15411  260 

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

261 

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

262 
subsubsection {* Equality of booleans  iff *} 
15411  263 

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

15411  266 

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

18457  268 
by (erule ssubst) 
15411  269 

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

18457  271 
by (erule iffD2) 
15411  272 

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

275 

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

277 
by (drule sym) (rule rev_iffD2) 

15411  278 

279 
lemma iffE: 

280 
assumes major: "P=Q" 

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

15411  284 

285 

20944  286 
subsubsection {*True*} 
15411  287 

288 
lemma TrueI: "True" 

21504  289 
unfolding True_def by (rule refl) 
15411  290 

21504  291 
lemma eqTrueI: "P ==> P = True" 
18457  292 
by (iprover intro: iffI TrueI) 
15411  293 

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

15411  296 

297 

20944  298 
subsubsection {*Universal quantifier*} 
15411  299 

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

15411  302 

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

304 
apply (unfold All_def) 

305 
apply (rule eqTrueE) 

306 
apply (erule fun_cong) 

307 
done 

308 

309 
lemma allE: 

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

21504  311 
and minor: "P(x) ==> R" 
312 
shows R 

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

15411  314 

315 
lemma all_dupE: 

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

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

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

15411  320 

321 

21504  322 
subsubsection {* False *} 
323 

324 
text {* 

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

326 
logic before quantifiers! 

327 
*} 

15411  328 

329 
lemma FalseE: "False ==> P" 

21504  330 
apply (unfold False_def) 
331 
apply (erule spec) 

332 
done 

15411  333 

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

15411  336 

337 

21504  338 
subsubsection {* Negation *} 
15411  339 

340 
lemma notI: 

21504  341 
assumes "P ==> False" 
15411  342 
shows "~P" 
21504  343 
apply (unfold not_def) 
344 
apply (iprover intro: impI assms) 

345 
done 

15411  346 

347 
lemma False_not_True: "False ~= True" 

21504  348 
apply (rule notI) 
349 
apply (erule False_neq_True) 

350 
done 

15411  351 

352 
lemma True_not_False: "True ~= False" 

21504  353 
apply (rule notI) 
354 
apply (drule sym) 

355 
apply (erule False_neq_True) 

356 
done 

15411  357 

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

21504  359 
apply (unfold not_def) 
360 
apply (erule mp [THEN FalseE]) 

361 
apply assumption 

362 
done 

15411  363 

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

15411  366 

367 

20944  368 
subsubsection {*Implication*} 
15411  369 

370 
lemma impE: 

371 
assumes "P>Q" "P" "Q ==> R" 

372 
shows "R" 

23553  373 
by (iprover intro: assms mp) 
15411  374 

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

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

17589  377 
by (iprover intro: mp) 
15411  378 

379 
lemma contrapos_nn: 

380 
assumes major: "~Q" 

381 
and minor: "P==>Q" 

382 
shows "~P" 

17589  383 
by (iprover intro: notI minor major [THEN notE]) 
15411  384 

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

386 
lemma contrapos_pn: 

387 
assumes major: "Q" 

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

389 
shows "~P" 

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

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

21250  393 
by (erule contrapos_nn) (erule sym) 
394 

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

396 
by (erule subst, erule ssubst, assumption) 

15411  397 

398 
(*still used in HOLCF*) 

399 
lemma rev_contrapos: 

400 
assumes pq: "P ==> Q" 

401 
and nq: "~Q" 

402 
shows "~P" 

403 
apply (rule nq [THEN contrapos_nn]) 

404 
apply (erule pq) 

405 
done 

406 

20944  407 
subsubsection {*Existential quantifier*} 
15411  408 

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

410 
apply (unfold Ex_def) 

17589  411 
apply (iprover intro: allI allE impI mp) 
15411  412 
done 
413 

414 
lemma exE: 

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

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

417 
shows "Q" 

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

17589  419 
apply (iprover intro: impI [THEN allI] minor) 
15411  420 
done 
421 

422 

20944  423 
subsubsection {*Conjunction*} 
15411  424 

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

426 
apply (unfold and_def) 

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

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

431 
apply (unfold and_def) 

17589  432 
apply (iprover intro: impI dest: spec mp) 
15411  433 
done 
434 

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

436 
apply (unfold and_def) 

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

440 
lemma conjE: 

441 
assumes major: "P&Q" 

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

443 
shows "R" 

444 
apply (rule minor) 

445 
apply (rule major [THEN conjunct1]) 

446 
apply (rule major [THEN conjunct2]) 

447 
done 

448 

449 
lemma context_conjI: 

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

15411  452 

453 

20944  454 
subsubsection {*Disjunction*} 
15411  455 

456 
lemma disjI1: "P ==> PQ" 

457 
apply (unfold or_def) 

17589  458 
apply (iprover intro: allI impI mp) 
15411  459 
done 
460 

461 
lemma disjI2: "Q ==> PQ" 

462 
apply (unfold or_def) 

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

466 
lemma disjE: 

467 
assumes major: "PQ" 

468 
and minorP: "P ==> R" 

469 
and minorQ: "Q ==> R" 

470 
shows "R" 

17589  471 
by (iprover intro: minorP minorQ impI 
15411  472 
major [unfolded or_def, THEN spec, THEN mp, THEN mp]) 
473 

474 

20944  475 
subsubsection {*Classical logic*} 
15411  476 

477 
lemma classical: 

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

479 
shows "P" 

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

481 
apply assumption 

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

483 
apply (erule subst) 

484 
apply assumption 

485 
done 

486 

45607  487 
lemmas ccontr = FalseE [THEN classical] 
15411  488 

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

490 
make elimination rules*) 

491 
lemma rev_notE: 

492 
assumes premp: "P" 

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

494 
shows "R" 

495 
apply (rule ccontr) 

496 
apply (erule notE [OF premnot premp]) 

497 
done 

498 

499 
(*Double negation law*) 

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

501 
apply (rule classical) 

502 
apply (erule notE) 

503 
apply assumption 

504 
done 

505 

506 
lemma contrapos_pp: 

507 
assumes p1: "Q" 

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

509 
shows "P" 

17589  510 
by (iprover intro: classical p1 p2 notE) 
15411  511 

512 

20944  513 
subsubsection {*Unique existence*} 
15411  514 

515 
lemma ex1I: 

23553  516 
assumes "P a" "!!x. P(x) ==> x=a" 
15411  517 
shows "EX! x. P(x)" 
23553  518 
by (unfold Ex1_def, iprover intro: assms exI conjI allI impI) 
15411  519 

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

521 
lemma ex_ex1I: 

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

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

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

17589  525 
by (iprover intro: ex_prem [THEN exE] ex1I eq) 
15411  526 

527 
lemma ex1E: 

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

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

530 
shows "R" 

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

532 
apply (erule conjE) 

17589  533 
apply (iprover intro: minor) 
15411  534 
done 
535 

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

537 
apply (erule ex1E) 

538 
apply (rule exI) 

539 
apply assumption 

540 
done 

541 

542 

20944  543 
subsubsection {*THE: definite description operator*} 
15411  544 

545 
lemma the_equality: 

546 
assumes prema: "P a" 

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

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

549 
apply (rule trans [OF _ the_eq_trivial]) 

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

551 
apply (rule ext) 

552 
apply (rule iffI) 

553 
apply (erule premx) 

554 
apply (erule ssubst, rule prema) 

555 
done 

556 

557 
lemma theI: 

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

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

23553  560 
by (iprover intro: assms the_equality [THEN ssubst]) 
15411  561 

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

563 
apply (erule ex1E) 

564 
apply (erule theI) 

565 
apply (erule allE) 

566 
apply (erule mp) 

567 
apply assumption 

568 
done 

569 

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

571 
lemma theI2: 

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

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

23553  574 
by (iprover intro: assms theI) 
15411  575 

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

578 
elim:allE impE) 

579 

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

583 
apply (erule ex1E) 

584 
apply (erule all_dupE) 

585 
apply (drule mp) 

586 
apply assumption 

587 
apply (erule ssubst) 

588 
apply (erule allE) 

589 
apply (erule mp) 

590 
apply assumption 

591 
done 

592 

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

594 
apply (rule the_equality) 

595 
apply (rule refl) 

596 
apply (erule sym) 

597 
done 

598 

599 

20944  600 
subsubsection {*Classical intro rules for disjunction and existential quantifiers*} 
15411  601 

602 
lemma disjCI: 

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

604 
apply (rule classical) 

23553  605 
apply (iprover intro: assms disjI1 disjI2 notI elim: notE) 
15411  606 
done 
607 

608 
lemma excluded_middle: "~P  P" 

17589  609 
by (iprover intro: disjCI) 
15411  610 

20944  611 
text {* 
612 
case distinction as a natural deduction rule. 

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

614 
*} 

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

615 
lemma case_split [case_names True False]: 
15411  616 
assumes prem1: "P ==> Q" 
617 
and prem2: "~P ==> Q" 

618 
shows "Q" 

619 
apply (rule excluded_middle [THEN disjE]) 

620 
apply (erule prem2) 

621 
apply (erule prem1) 

622 
done 

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

623 

15411  624 
(*Classical implies (>) elimination. *) 
625 
lemma impCE: 

626 
assumes major: "P>Q" 

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

628 
shows "R" 

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

17589  630 
apply (iprover intro: minor major [THEN mp])+ 
15411  631 
done 
632 

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

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

635 
default: would break old proofs.*) 

636 
lemma impCE': 

637 
assumes major: "P>Q" 

638 
and minor: "Q ==> R" "~P ==> 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 
(*Classical <> elimination. *) 

645 
lemma iffCE: 

646 
assumes major: "P=Q" 

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

648 
shows "R" 

649 
apply (rule major [THEN iffE]) 

17589  650 
apply (iprover intro: minor elim: impCE notE) 
15411  651 
done 
652 

653 
lemma exCI: 

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

655 
shows "EX x. P(x)" 

656 
apply (rule ccontr) 

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

660 

12386  661 
subsubsection {* Intuitionistic Reasoning *} 
662 

663 
lemma impE': 

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

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

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

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

667 
shows R 
12386  668 
proof  
669 
from 3 and 1 have P . 

670 
with 1 have Q by (rule impE) 

671 
with 2 show R . 

672 
qed 

673 

674 
lemma allE': 

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

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

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

677 
shows Q 
12386  678 
proof  
679 
from 1 have "P x" by (rule spec) 

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

681 
qed 

682 

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

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

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

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

686 
shows R 
12386  687 
proof  
688 
from 2 and 1 have P . 

689 
with 1 show R by (rule notE) 

690 
qed 

691 

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

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

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

694 

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

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

698 
and [Pure.intro] = exI disjI2 disjI1 

12386  699 

700 
lemmas [trans] = trans 

701 
and [sym] = sym not_sym 

15801  702 
and [Pure.elim?] = iffD1 iffD2 impE 
11750  703 

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

704 
use "Tools/hologic.ML" 
23553  705 

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

706 

11750  707 
subsubsection {* Atomizing metalevel connectives *} 
708 

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

711 

11750  712 
lemma atomize_all [atomize]: "(!!x. P x) == Trueprop (ALL x. P x)" 
12003  713 
proof 
9488  714 
assume "!!x. P x" 
23389  715 
then show "ALL x. P x" .. 
9488  716 
next 
717 
assume "ALL x. P x" 

23553  718 
then show "!!x. P x" by (rule allE) 
9488  719 
qed 
720 

11750  721 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
12003  722 
proof 
9488  723 
assume r: "A ==> B" 
10383  724 
show "A > B" by (rule impI) (rule r) 
9488  725 
next 
726 
assume "A > B" and A 

23553  727 
then show B by (rule mp) 
9488  728 
qed 
729 

14749  730 
lemma atomize_not: "(A ==> False) == Trueprop (~A)" 
731 
proof 

732 
assume r: "A ==> False" 

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

734 
next 

735 
assume "~A" and A 

23553  736 
then show False by (rule notE) 
14749  737 
qed 
738 

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

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

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

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

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

747 

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

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

750 
assume conj: "A &&& B" 
19121  751 
show "A & B" 
752 
proof (rule conjI) 

753 
from conj show A by (rule conjunctionD1) 

754 
from conj show B by (rule conjunctionD2) 

755 
qed 

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

758 
show "A &&& B" 
19121  759 
proof  
760 
from conj show A .. 

761 
from conj show B .. 

11953  762 
qed 
763 
qed 

764 

12386  765 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
18832  766 
and [symmetric, defn] = atomize_all atomize_imp atomize_eq 
12386  767 

11750  768 

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

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

770 

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

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

772 

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

773 
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

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

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

778 

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

779 
lemma atomize_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

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

781 

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

782 
lemma atomize_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

783 

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

784 

20944  785 
subsection {* Package setup *} 
786 

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

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

788 

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

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

790 
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

791 
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

792 
seldomused facts. Some duplicate other rules. 
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 

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

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

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

797 
( 
45294  798 
val name = @{binding no_atp} 
36060
4d27652ffb40
reintroduce efficient set structure to collect "no_atp" theorems
blanchet
parents:
35828
diff
changeset

799 
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

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

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

802 

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

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

11750  806 
subsubsection {* Classical Reasoner setup *} 
9529  807 

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

810 

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

812 
by (rule classical) iprover 

813 

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

816 

21151  817 
ML {* 
42799  818 
structure Hypsubst = Hypsubst 
819 
( 

21218  820 
val dest_eq = HOLogic.dest_eq 
21151  821 
val dest_Trueprop = HOLogic.dest_Trueprop 
822 
val dest_imp = HOLogic.dest_imp 

26411  823 
val eq_reflection = @{thm eq_reflection} 
824 
val rev_eq_reflection = @{thm meta_eq_to_obj_eq} 

825 
val imp_intr = @{thm impI} 

826 
val rev_mp = @{thm rev_mp} 

827 
val subst = @{thm subst} 

828 
val sym = @{thm sym} 

22129  829 
val thin_refl = @{thm thin_refl}; 
42799  830 
); 
21671  831 
open Hypsubst; 
21151  832 

42799  833 
structure Classical = Classical 
834 
( 

26411  835 
val imp_elim = @{thm imp_elim} 
836 
val not_elim = @{thm notE} 

837 
val swap = @{thm swap} 

838 
val classical = @{thm classical} 

21151  839 
val sizef = Drule.size_of_thm 
840 
val hyp_subst_tacs = [Hypsubst.hyp_subst_tac] 

42799  841 
); 
21151  842 

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

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

844 
open Basic_Classical; 
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42802
diff
changeset

845 
*} 
22129  846 

43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42802
diff
changeset

847 
setup {* 
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42802
diff
changeset

848 
ML_Antiquote.value @{binding claset} 
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42802
diff
changeset

849 
(Scan.succeed "Classical.claset_of (ML_Context.the_local_context ())") 
21151  850 
*} 
851 

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

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

853 

21009  854 
setup {* 
855 
let 

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

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

859 
SUBGOAL (fn (goal, i) => 

860 
if Term.exists_Const non_bool_eq goal 

861 
then Hypsubst.hyp_subst_tac i 

862 
else no_tac); 

21009  863 
in 
21151  864 
Hypsubst.hypsubst_setup 
35389  865 
(*prevent substitution on bool*) 
33369  866 
#> Context_Rules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac) 
21009  867 
end 
868 
*} 

869 

870 
declare iffI [intro!] 

871 
and notI [intro!] 

872 
and impI [intro!] 

873 
and disjCI [intro!] 

874 
and conjI [intro!] 

875 
and TrueI [intro!] 

876 
and refl [intro!] 

877 

878 
declare iffCE [elim!] 

879 
and FalseE [elim!] 

880 
and impCE [elim!] 

881 
and disjE [elim!] 

882 
and conjE [elim!] 

883 

884 
declare ex_ex1I [intro!] 

885 
and allI [intro!] 

886 
and the_equality [intro] 

887 
and exI [intro] 

888 

889 
declare exE [elim!] 

890 
allE [elim] 

891 

22377  892 
ML {* val HOL_cs = @{claset} *} 
19162  893 

20223  894 
lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P" 
895 
apply (erule swap) 

896 
apply (erule (1) meta_mp) 

897 
done 

10383  898 

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

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

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

901 

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

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

903 

12386  904 
lemmas [intro?] = ext 
905 
and [elim?] = ex1_implies_ex 

11977  906 

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

911 
shows R 

912 
apply (rule ex1E [OF major]) 

913 
apply (rule prem) 

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

916 
apply iprover 

917 
done 

20944  918 

21151  919 
ML {* 
42477  920 
structure Blast = Blast 
921 
( 

922 
structure Classical = Classical 

42802  923 
val Trueprop_const = dest_Const @{const Trueprop} 
42477  924 
val equality_name = @{const_name HOL.eq} 
925 
val not_name = @{const_name Not} 

926 
val notE = @{thm notE} 

927 
val ccontr = @{thm ccontr} 

928 
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac 

929 
); 

930 
val blast_tac = Blast.blast_tac; 

20944  931 
*} 
932 

21151  933 
setup Blast.setup 
934 

20944  935 

936 
subsubsection {* Simplifier *} 

12281  937 

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

939 

940 
lemma simp_thms: 

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

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

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

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

945 
"(P  ~P) = True" "(~P  P) = True" 
12281  946 
"(x = x) = True" 
32068  947 
and not_True_eq_False [code]: "(\<not> True) = False" 
948 
and not_False_eq_True [code]: "(\<not> False) = True" 

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

950 
"(~P) ~= P" "P ~= (~P)" 
20944  951 
"(True=P) = P" 
952 
and eq_True: "(P = True) = P" 

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

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

955 
and 

12281  956 
"(True > P) = P" "(False > P) = True" 
957 
"(P > True) = True" "(P > P) = True" 

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

959 
"(P & True) = P" "(True & P) = P" 

960 
"(P & False) = False" "(False & P) = False" 

961 
"(P & P) = P" "(P & (P & Q)) = (P & Q)" 

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

963 
"(P  True) = True" "(True  P) = True" 

964 
"(P  False) = P" "(False  P) = P" 

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

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

967 
and 
12281  968 
"!!P. (EX x. x=t & P(x)) = P(t)" 
969 
"!!P. (EX x. t=x & P(x)) = P(t)" 

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

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

971 
"!!P. (ALL x. t=x > P(x)) = P(t)" 
17589  972 
by (blast, blast, blast, blast, blast, iprover+) 
13421  973 

14201  974 
lemma disj_absorb: "(A  A) = A" 
975 
by blast 

976 

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

978 
by blast 

979 

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

981 
by blast 

982 

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

984 
by blast 

985 

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

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

988 
and eq_left_commute: "(P=(Q=R)) = (Q=(P=R))" 
17589  989 
and eq_assoc: "((P=Q)=R) = (P=(Q=R))" by (iprover, blast+) 
990 
lemma neq_commute: "(a~=b) = (b~=a)" by iprover 

12281  991 

992 
lemma conj_comms: 

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

993 
shows conj_commute: "(P&Q) = (Q&P)" 
17589  994 
and conj_left_commute: "(P&(Q&R)) = (Q&(P&R))" by iprover+ 
995 
lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by iprover 

12281  996 

19174  997 
lemmas conj_ac = conj_commute conj_left_commute conj_assoc 
998 

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

1000 
shows disj_commute: "(PQ) = (QP)" 
17589  1001 
and disj_left_commute: "(P(QR)) = (Q(PR))" by iprover+ 
1002 
lemma disj_assoc: "((PQ)R) = (P(QR))" by iprover 

12281  1003 

19174  1004 
lemmas disj_ac = disj_commute disj_left_commute disj_assoc 
1005 

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

12281  1008 

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

12281  1011 

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

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

12281  1015 

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

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

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

1019 

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

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

1022 

21151  1023 
lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P > Q) = (P' > Q'))" 
1024 
by iprover 

1025 

17589  1026 
lemma de_Morgan_disj: "(~(P  Q)) = (~P & ~Q)" by iprover 
12281  1027 
lemma de_Morgan_conj: "(~(P & Q)) = (~P  ~Q)" by blast 
1028 
lemma not_imp: "(~(P > Q)) = (P & ~Q)" by blast 

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

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

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

1032 
by blast 

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

1034 

17589  1035 
lemma iff_conv_conj_imp: "(P = Q) = ((P > Q) & (Q > P))" by iprover 
12281  1036 

1037 

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

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

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

1041 
by blast 

1042 

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

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

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

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

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

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

1050 

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

12281  1053 

1054 
text {* 

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

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

1057 

1058 
lemma conj_cong: 

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

17589  1060 
by iprover 
12281  1061 

1062 
lemma rev_conj_cong: 

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

17589  1064 
by iprover 
12281  1065 

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

1067 

1068 
lemma disj_cong: 

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

1070 
by blast 

1071 

1072 

1073 
text {* \medskip ifthenelse rules *} 

1074 

32068  1075 
lemma if_True [code]: "(if True then x else y) = x" 
38525  1076 
by (unfold If_def) blast 
12281  1077 

32068  1078 
lemma if_False [code]: "(if False then x else y) = y" 
38525  1079 
by (unfold If_def) blast 
12281  1080 

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

38525  1082 
by (unfold If_def) blast 
12281  1083 

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

38525  1085 
by (unfold If_def) blast 
12281  1086 

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

1088 
apply (rule case_split [of Q]) 

15481  1089 
apply (simplesubst if_P) 
1090 
prefer 3 apply (simplesubst if_not_P, blast+) 

12281  1091 
done 
1092 

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

15481  1094 
by (simplesubst split_if, blast) 
12281  1095 

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

1096 
lemmas if_splits [no_atp] = split_if split_if_asm 
12281  1097 

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

15481  1099 
by (simplesubst split_if, blast) 
12281  1100 

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

15481  1102 
by (simplesubst split_if, blast) 
12281  1103 

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

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

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

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

19796  1110 
 {* And this form is useful for expanding @{text "if"}s on the LEFT. *} 
15481  1111 
apply (simplesubst split_if, blast) 
12281  1112 
done 
1113 

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

12281  1116 

15423  1117 
text {* \medskip let rules for simproc *} 
1118 

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

1120 
by (unfold Let_def) 

1121 

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

1123 
by (unfold Let_def) 

1124 

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

1125 
text {* 
16999  1126 
The following copy of the implication operator is useful for 
1127 
finetuning congruence rules. It instructs the simplifier to simplify 

1128 
its premise. 

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

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

1130 

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

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

1133 

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

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

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

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

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

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

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

1141 

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

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

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

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

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

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

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

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

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

1151 

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

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

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

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

1155 
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

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

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

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

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

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

1162 
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

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

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

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

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

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

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

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

1171 

20944  1172 
lemma uncurry: 
1173 
assumes "P \<longrightarrow> Q \<longrightarrow> R" 

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

23553  1175 
using assms by blast 
20944  1176 

1177 
lemma iff_allI: 

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

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

23553  1180 
using assms by blast 
20944  1181 

1182 
lemma iff_exI: 

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

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

23553  1185 
using assms by blast 
20944  1186 

1187 
lemma all_comm: 

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

1189 
by blast 

1190 

1191 
lemma ex_comm: 

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

1193 
by blast 

1194 

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

1195 
use "Tools/simpdata.ML" 
21671  1196 
ML {* open Simpdata *} 
42455  1197 

42795
66fcc9882784
clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents:
42477
diff
changeset

1198 
setup {* Simplifier.map_simpset_global (K HOL_basic_ss) *} 
42455  1199 

42459  1200 
simproc_setup defined_Ex ("EX x. P x") = {* fn _ => Quantifier1.rearrange_ex *} 
1201 
simproc_setup defined_All ("ALL x. P x") = {* fn _ => Quantifier1.rearrange_all *} 

21671  1202 

21151  1203 
setup {* 
1204 
Simplifier.method_setup Splitter.split_modifiers 

1205 
#> Splitter.setup 

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

1206 
#> clasimp_setup 
21151  1207 
#> EqSubst.setup 
1208 
*} 

1209 

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

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

1213 
let 

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

1215 
fun is_neq eq lhs rhs thm = 

1216 
(case Thm.prop_of thm of 

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

1218 
Not = HOLogic.Not andalso eq' = eq andalso 

1219 
r' aconv lhs andalso l' aconv rhs 

1220 
 _ => false); 

1221 
fun proc ss ct = 

1222 
(case Thm.term_of ct of 

1223 
eq $ lhs $ rhs => 

43597  1224 
(case find_first (is_neq eq lhs rhs) (Simplifier.prems_of ss) of 
24035  1225 
SOME thm => SOME (thm RS neq_to_EQ_False) 
1226 
 NONE => NONE) 

1227 
 _ => NONE); 

1228 
in proc end; 

1229 
*} 

1230 

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

1232 
let 

1233 
val (f_Let_unfold, x_Let_unfold) = 

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

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

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

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

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

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

1245 
 count_loose _ _ = 0; 

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

1247 
case t 

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

1249 
 _ => true; 

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

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

42361  1254 
val thy = Proof_Context.theory_of ctxt; 
28741  1255 
val t = Thm.term_of ct; 
1256 
val ([t'], ctxt') = Variable.import_terms false [t] ctxt; 

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

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

1259 
if is_Free x orelse is_Bound x orelse is_Const x 

1260 
then SOME @{thm Let_def} 

1261 
else 

1262 
let 

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

1264 
val cx = cterm_of thy x; 

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

1266 
val cf = cterm_of thy f; 

46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
46190
diff
changeset

1267 
val fx_g = Simplifier.rewrite ss (Thm.apply cf cx); 
28741  1268 
val (_ $ _ $ g) = prop_of fx_g; 
1269 
val g' = abstract_over (x,g); 

1270 
in (if (g aconv g') 

1271 
then 

1272 
let 

1273 
val rl = 

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

1275 
in SOME (rl OF [fx_g]) end 

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

1277 
else let 

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

1279 
val g'x = abs_g'$x; 

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

1283 
(g_Let_folded, cterm_of thy abs_g')] 

1284 
@{thm Let_folded}; 

36945  1285 
in SOME (rl OF [Thm.transitive fx_g g_g'x]) 
28741  1286 
end) 
1287 
end 

1288 
 _ => NONE) 

1289 
end 

1290 
end *} 

24035  1291 

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

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

21151  1296 
next 
1297 
assume "PROP P" 

23389  1298 
then show "PROP P" . 
21151  1299 
qed 
1300 

1301 
lemma ex_simps: 

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

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

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

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

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

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

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

1309 
by (iprover  blast)+ 

1310 

1311 
lemma all_simps: 

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

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

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

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

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

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

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

1319 
by (iprover  blast)+ 

15481  1320 

21671  1321 
lemmas [simp] = 
1322 
triv_forall_equality (*prunes params*) 

1323 
True_implies_equals (*prune asms `True'*) 

1324 
if_True 

1325 
if_False 

1326 
if_cancel 

1327 
if_eq_cancel 

1328 
imp_disjL 

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

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

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

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

21671  1334 
conj_assoc 
1335 
disj_assoc 

1336 
de_Morgan_conj 

1337 
de_Morgan_disj 

1338 
imp_disj1 

1339 
imp_disj2 

1340 
not_imp 

1341 
disj_not1 

1342 
not_all 

1343 
not_ex 

1344 
cases_simp 

1345 
the_eq_trivial 

1346 
the_sym_eq_trivial 

1347 
ex_simps 

1348 
all_simps 

1349 
simp_thms 

1350 

1351 
lemmas [cong] = imp_cong simp_implies_cong 

1352 
lemmas [split] = split_if 

20973  1353 

22377  1354 
ML {* val HOL_ss = @{simpset} *} 
20973  1355 

20944  1356 
text {* Simplifies x assuming c and y assuming ~c *} 
1357 
lemma if_cong: 

34b2c1bb7178
cleanup basic HOL bootstrap
haft&# 