author  webertj 
Fri, 19 Oct 2012 15:12:52 +0200  
changeset 49962  a8cc904a6820 
parent 49339  d1fcb4de8349 
child 50360  628b37b9e8a2 
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 
47657
1ba213363d0c
moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator
haftmann
parents:
46973
diff
changeset

10 
"try" "solve_direct" "quickcheck" 
1ba213363d0c
moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator
haftmann
parents:
46973
diff
changeset

11 
"print_coercions" "print_coercion_maps" "print_claset" "print_induct_rules" :: diag and 
1ba213363d0c
moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator
haftmann
parents:
46973
diff
changeset

12 
"quickcheck_params" :: thy_decl 
15131  13 
begin 
2260  14 

48891  15 
ML_file "~~/src/Tools/misc_legacy.ML" 
16 
ML_file "~~/src/Tools/try.ML" 

17 
ML_file "~~/src/Tools/quickcheck.ML" 

18 
ML_file "~~/src/Tools/solve_direct.ML" 

19 
ML_file "~~/src/Tools/IsaPlanner/zipper.ML" 

20 
ML_file "~~/src/Tools/IsaPlanner/isand.ML" 

21 
ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML" 

22 
ML_file "~~/src/Provers/hypsubst.ML" 

23 
ML_file "~~/src/Provers/splitter.ML" 

24 
ML_file "~~/src/Provers/classical.ML" 

25 
ML_file "~~/src/Provers/blast.ML" 

26 
ML_file "~~/src/Provers/clasimp.ML" 

27 
ML_file "~~/src/Tools/coherent.ML" 

28 
ML_file "~~/src/Tools/eqsubst.ML" 

29 
ML_file "~~/src/Provers/quantifier1.ML" 

30 
ML_file "~~/src/Tools/atomize_elim.ML" 

31 
ML_file "~~/src/Tools/induct.ML" 

32 
ML_file "~~/src/Tools/cong_tac.ML" 

33 
ML_file "~~/src/Tools/intuitionistic.ML" 

34 
ML_file "~~/src/Tools/project_rule.ML" 

35 
ML_file "~~/src/Tools/subtyping.ML" 

36 
ML_file "~~/src/Tools/case_product.ML" 

37 

47657
1ba213363d0c
moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator
haftmann
parents:
46973
diff
changeset

38 
setup {* 
1ba213363d0c
moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator
haftmann
parents:
46973
diff
changeset

39 
Intuitionistic.method_setup @{binding iprover} 
1ba213363d0c
moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator
haftmann
parents:
46973
diff
changeset

40 
#> Quickcheck.setup 
1ba213363d0c
moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator
haftmann
parents:
46973
diff
changeset

41 
#> Solve_Direct.setup 
1ba213363d0c
moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator
haftmann
parents:
46973
diff
changeset

42 
#> Subtyping.setup 
1ba213363d0c
moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator
haftmann
parents:
46973
diff
changeset

43 
#> Case_Product.setup 
1ba213363d0c
moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator
haftmann
parents:
46973
diff
changeset

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

45 

11750  46 
subsection {* Primitive logic *} 
47 

48 
subsubsection {* Core syntax *} 

2260  49 

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

53 

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

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

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

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

57 

7357  58 
typedecl bool 
923  59 

11750  60 
judgment 
61 
Trueprop :: "bool => prop" ("(_)" 5) 

923  62 

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

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

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

67 

11750  68 
consts 
7357  69 
True :: bool 
70 
False :: bool 

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

72 

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

73 
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

74 
disj :: "[bool, bool] => bool" (infixr "" 30) 
38555  75 

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

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

923  79 

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

80 

11750  81 
subsubsection {* Additional concrete syntax *} 
2260  82 

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

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

85 

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

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

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

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

89 

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

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

92 

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

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

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

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

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

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

99 

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

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

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

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

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

105 

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

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

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

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

109 

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

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

112 

46973  113 
syntax "_The" :: "[pttrn, bool] => 'a" ("(3THE _./ _)" [0, 10] 10) 
114 
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

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

116 
[(@{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

117 
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

118 
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

119 
*}  {* To avoid etacontraction of body *} 
923  120 

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

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

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

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

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

128 
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

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

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

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

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

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

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

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

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 

46973  155 
axiomatization where 
156 
refl: "t = (t::'a)" and 

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

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

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

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

46973  165 
axiomatization where 
166 
impI: "(P ==> Q) ==> P>Q" and 

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

15380  168 

46973  169 
iff: "(P>Q) > (Q>P) > (P=Q)" and 
170 
True_or_False: "(P=True)  (P=False)" 

15380  171 

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

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

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

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

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

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

923  181 

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

923  184 

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

38525  187 

188 
translations 

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

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

191 

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

193 

46973  194 
class default = fixes default :: 'a 
4868  195 

11750  196 

20944  197 
subsection {* Fundamental rules *} 
198 

20973  199 
subsubsection {* Equality *} 
20944  200 

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

15411  203 

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

15411  206 

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

18457  208 
by (erule subst) 
15411  209 

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

210 
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

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

212 

20944  213 
lemma meta_eq_to_obj_eq: 
214 
assumes meq: "A == B" 

215 
shows "A = B" 

216 
by (unfold meq) (rule refl) 

15411  217 

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

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

223 
apply (rule trans) 

224 
apply (rule trans) 

225 
apply (rule sym) 

226 
apply assumption+ 

227 
done 

228 

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

229 
text {* For calculational reasoning: *} 
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 forw_subst: "a = b ==> P b ==> P a" 
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset

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

233 

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

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

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

236 

15411  237 

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

238 
subsubsection {* Congruence rules for application *} 
15411  239 

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

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

243 
apply (rule refl) 

244 
done 

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 
text {* Similar to @{text AP_TERM} in Gordon's HOL and FOL's @{text subst_context}. *} 
15411  247 
lemma arg_cong: "x=y ==> f(x)=f(y)" 
248 
apply (erule subst) 

249 
apply (rule refl) 

250 
done 

251 

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

254 
apply (rule refl) 

255 
done 

256 

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

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

260 
done 

261 

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

262 
ML {* val cong_tac = Cong_Tac.cong_tac @{thm cong} *} 
15411  263 

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

264 

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

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

15411  269 

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

18457  271 
by (erule ssubst) 
15411  272 

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

18457  274 
by (erule iffD2) 
15411  275 

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

278 

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

280 
by (drule sym) (rule rev_iffD2) 

15411  281 

282 
lemma iffE: 

283 
assumes major: "P=Q" 

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

15411  287 

288 

20944  289 
subsubsection {*True*} 
15411  290 

291 
lemma TrueI: "True" 

21504  292 
unfolding True_def by (rule refl) 
15411  293 

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

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

15411  299 

300 

20944  301 
subsubsection {*Universal quantifier*} 
15411  302 

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

15411  305 

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

307 
apply (unfold All_def) 

308 
apply (rule eqTrueE) 

309 
apply (erule fun_cong) 

310 
done 

311 

312 
lemma allE: 

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

21504  314 
and minor: "P(x) ==> R" 
315 
shows R 

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

15411  317 

318 
lemma all_dupE: 

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

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

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

15411  323 

324 

21504  325 
subsubsection {* False *} 
326 

327 
text {* 

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

329 
logic before quantifiers! 

330 
*} 

15411  331 

332 
lemma FalseE: "False ==> P" 

21504  333 
apply (unfold False_def) 
334 
apply (erule spec) 

335 
done 

15411  336 

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

15411  339 

340 

21504  341 
subsubsection {* Negation *} 
15411  342 

343 
lemma notI: 

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

348 
done 

15411  349 

350 
lemma False_not_True: "False ~= True" 

21504  351 
apply (rule notI) 
352 
apply (erule False_neq_True) 

353 
done 

15411  354 

355 
lemma True_not_False: "True ~= False" 

21504  356 
apply (rule notI) 
357 
apply (drule sym) 

358 
apply (erule False_neq_True) 

359 
done 

15411  360 

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

21504  362 
apply (unfold not_def) 
363 
apply (erule mp [THEN FalseE]) 

364 
apply assumption 

365 
done 

15411  366 

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

15411  369 

370 

20944  371 
subsubsection {*Implication*} 
15411  372 

373 
lemma impE: 

374 
assumes "P>Q" "P" "Q ==> R" 

375 
shows "R" 

23553  376 
by (iprover intro: assms mp) 
15411  377 

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

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

17589  380 
by (iprover intro: mp) 
15411  381 

382 
lemma contrapos_nn: 

383 
assumes major: "~Q" 

384 
and minor: "P==>Q" 

385 
shows "~P" 

17589  386 
by (iprover intro: notI minor major [THEN notE]) 
15411  387 

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

389 
lemma contrapos_pn: 

390 
assumes major: "Q" 

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

392 
shows "~P" 

17589  393 
by (iprover intro: notI minor major notE) 
15411  394 

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

21250  396 
by (erule contrapos_nn) (erule sym) 
397 

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

399 
by (erule subst, erule ssubst, assumption) 

15411  400 

401 

20944  402 
subsubsection {*Existential quantifier*} 
15411  403 

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

405 
apply (unfold Ex_def) 

17589  406 
apply (iprover intro: allI allE impI mp) 
15411  407 
done 
408 

409 
lemma exE: 

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

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

412 
shows "Q" 

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

17589  414 
apply (iprover intro: impI [THEN allI] minor) 
15411  415 
done 
416 

417 

20944  418 
subsubsection {*Conjunction*} 
15411  419 

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

421 
apply (unfold and_def) 

17589  422 
apply (iprover intro: impI [THEN allI] mp) 
15411  423 
done 
424 

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

426 
apply (unfold and_def) 

17589  427 
apply (iprover intro: impI dest: spec mp) 
15411  428 
done 
429 

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

431 
apply (unfold and_def) 

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

435 
lemma conjE: 

436 
assumes major: "P&Q" 

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

438 
shows "R" 

439 
apply (rule minor) 

440 
apply (rule major [THEN conjunct1]) 

441 
apply (rule major [THEN conjunct2]) 

442 
done 

443 

444 
lemma context_conjI: 

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

15411  447 

448 

20944  449 
subsubsection {*Disjunction*} 
15411  450 

451 
lemma disjI1: "P ==> PQ" 

452 
apply (unfold or_def) 

17589  453 
apply (iprover intro: allI impI mp) 
15411  454 
done 
455 

456 
lemma disjI2: "Q ==> PQ" 

457 
apply (unfold or_def) 

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

461 
lemma disjE: 

462 
assumes major: "PQ" 

463 
and minorP: "P ==> R" 

464 
and minorQ: "Q ==> R" 

465 
shows "R" 

17589  466 
by (iprover intro: minorP minorQ impI 
15411  467 
major [unfolded or_def, THEN spec, THEN mp, THEN mp]) 
468 

469 

20944  470 
subsubsection {*Classical logic*} 
15411  471 

472 
lemma classical: 

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

474 
shows "P" 

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

476 
apply assumption 

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

478 
apply (erule subst) 

479 
apply assumption 

480 
done 

481 

45607  482 
lemmas ccontr = FalseE [THEN classical] 
15411  483 

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

485 
make elimination rules*) 

486 
lemma rev_notE: 

487 
assumes premp: "P" 

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

489 
shows "R" 

490 
apply (rule ccontr) 

491 
apply (erule notE [OF premnot premp]) 

492 
done 

493 

494 
(*Double negation law*) 

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

496 
apply (rule classical) 

497 
apply (erule notE) 

498 
apply assumption 

499 
done 

500 

501 
lemma contrapos_pp: 

502 
assumes p1: "Q" 

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

504 
shows "P" 

17589  505 
by (iprover intro: classical p1 p2 notE) 
15411  506 

507 

20944  508 
subsubsection {*Unique existence*} 
15411  509 

510 
lemma ex1I: 

23553  511 
assumes "P a" "!!x. P(x) ==> x=a" 
15411  512 
shows "EX! x. P(x)" 
23553  513 
by (unfold Ex1_def, iprover intro: assms exI conjI allI impI) 
15411  514 

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

516 
lemma ex_ex1I: 

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

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

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

17589  520 
by (iprover intro: ex_prem [THEN exE] ex1I eq) 
15411  521 

522 
lemma ex1E: 

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

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

525 
shows "R" 

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

527 
apply (erule conjE) 

17589  528 
apply (iprover intro: minor) 
15411  529 
done 
530 

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

532 
apply (erule ex1E) 

533 
apply (rule exI) 

534 
apply assumption 

535 
done 

536 

537 

20944  538 
subsubsection {*THE: definite description operator*} 
15411  539 

540 
lemma the_equality: 

541 
assumes prema: "P a" 

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

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

544 
apply (rule trans [OF _ the_eq_trivial]) 

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

546 
apply (rule ext) 

547 
apply (rule iffI) 

548 
apply (erule premx) 

549 
apply (erule ssubst, rule prema) 

550 
done 

551 

552 
lemma theI: 

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

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

23553  555 
by (iprover intro: assms the_equality [THEN ssubst]) 
15411  556 

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

558 
apply (erule ex1E) 

559 
apply (erule theI) 

560 
apply (erule allE) 

561 
apply (erule mp) 

562 
apply assumption 

563 
done 

564 

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

566 
lemma theI2: 

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

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

23553  569 
by (iprover intro: assms theI) 
15411  570 

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

573 
elim:allE impE) 

574 

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

578 
apply (erule ex1E) 

579 
apply (erule all_dupE) 

580 
apply (drule mp) 

581 
apply assumption 

582 
apply (erule ssubst) 

583 
apply (erule allE) 

584 
apply (erule mp) 

585 
apply assumption 

586 
done 

587 

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

589 
apply (rule the_equality) 

590 
apply (rule refl) 

591 
apply (erule sym) 

592 
done 

593 

594 

20944  595 
subsubsection {*Classical intro rules for disjunction and existential quantifiers*} 
15411  596 

597 
lemma disjCI: 

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

599 
apply (rule classical) 

23553  600 
apply (iprover intro: assms disjI1 disjI2 notI elim: notE) 
15411  601 
done 
602 

603 
lemma excluded_middle: "~P  P" 

17589  604 
by (iprover intro: disjCI) 
15411  605 

20944  606 
text {* 
607 
case distinction as a natural deduction rule. 

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

609 
*} 

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

610 
lemma case_split [case_names True False]: 
15411  611 
assumes prem1: "P ==> Q" 
612 
and prem2: "~P ==> Q" 

613 
shows "Q" 

614 
apply (rule excluded_middle [THEN disjE]) 

615 
apply (erule prem2) 

616 
apply (erule prem1) 

617 
done 

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

618 

15411  619 
(*Classical implies (>) elimination. *) 
620 
lemma impCE: 

621 
assumes major: "P>Q" 

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

623 
shows "R" 

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

17589  625 
apply (iprover intro: minor major [THEN mp])+ 
15411  626 
done 
627 

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

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

630 
default: would break old proofs.*) 

631 
lemma impCE': 

632 
assumes major: "P>Q" 

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

634 
shows "R" 

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

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

639 
(*Classical <> elimination. *) 

640 
lemma iffCE: 

641 
assumes major: "P=Q" 

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

643 
shows "R" 

644 
apply (rule major [THEN iffE]) 

17589  645 
apply (iprover intro: minor elim: impCE notE) 
15411  646 
done 
647 

648 
lemma exCI: 

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

650 
shows "EX x. P(x)" 

651 
apply (rule ccontr) 

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

655 

12386  656 
subsubsection {* Intuitionistic Reasoning *} 
657 

658 
lemma impE': 

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

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

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

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

662 
shows R 
12386  663 
proof  
664 
from 3 and 1 have P . 

665 
with 1 have Q by (rule impE) 

666 
with 2 show R . 

667 
qed 

668 

669 
lemma allE': 

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

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

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

672 
shows Q 
12386  673 
proof  
674 
from 1 have "P x" by (rule spec) 

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

676 
qed 

677 

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

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

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

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

681 
shows R 
12386  682 
proof  
683 
from 2 and 1 have P . 

684 
with 1 show R by (rule notE) 

685 
qed 

686 

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

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

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

689 

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

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

693 
and [Pure.intro] = exI disjI2 disjI1 

12386  694 

695 
lemmas [trans] = trans 

696 
and [sym] = sym not_sym 

15801  697 
and [Pure.elim?] = iffD1 iffD2 impE 
11750  698 

48891  699 
ML_file "Tools/hologic.ML" 
23553  700 

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

701 

11750  702 
subsubsection {* Atomizing metalevel connectives *} 
703 

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

706 

11750  707 
lemma atomize_all [atomize]: "(!!x. P x) == Trueprop (ALL x. P x)" 
12003  708 
proof 
9488  709 
assume "!!x. P x" 
23389  710 
then show "ALL x. P x" .. 
9488  711 
next 
712 
assume "ALL x. P x" 

23553  713 
then show "!!x. P x" by (rule allE) 
9488  714 
qed 
715 

11750  716 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
12003  717 
proof 
9488  718 
assume r: "A ==> B" 
10383  719 
show "A > B" by (rule impI) (rule r) 
9488  720 
next 
721 
assume "A > B" and A 

23553  722 
then show B by (rule mp) 
9488  723 
qed 
724 

14749  725 
lemma atomize_not: "(A ==> False) == Trueprop (~A)" 
726 
proof 

727 
assume r: "A ==> False" 

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

729 
next 

730 
assume "~A" and A 

23553  731 
then show False by (rule notE) 
14749  732 
qed 
733 

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

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

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

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

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

742 

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

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

745 
assume conj: "A &&& B" 
19121  746 
show "A & B" 
747 
proof (rule conjI) 

748 
from conj show A by (rule conjunctionD1) 

749 
from conj show B by (rule conjunctionD2) 

750 
qed 

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

753 
show "A &&& B" 
19121  754 
proof  
755 
from conj show A .. 

756 
from conj show B .. 

11953  757 
qed 
758 
qed 

759 

12386  760 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
18832  761 
and [symmetric, defn] = atomize_all atomize_imp atomize_eq 
12386  762 

11750  763 

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

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

765 

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

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

767 

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

768 
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

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

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

773 

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

774 
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

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

776 

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

777 
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

778 

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

779 

20944  780 
subsection {* Package setup *} 
781 

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

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

783 

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

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

785 
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

786 
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

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

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

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

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

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

794 
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

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

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

797 

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

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

11750  801 
subsubsection {* Classical Reasoner setup *} 
9529  802 

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

805 

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

807 
by (rule classical) iprover 

808 

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

811 

21151  812 
ML {* 
42799  813 
structure Hypsubst = Hypsubst 
814 
( 

21218  815 
val dest_eq = HOLogic.dest_eq 
21151  816 
val dest_Trueprop = HOLogic.dest_Trueprop 
817 
val dest_imp = HOLogic.dest_imp 

26411  818 
val eq_reflection = @{thm eq_reflection} 
819 
val rev_eq_reflection = @{thm meta_eq_to_obj_eq} 

820 
val imp_intr = @{thm impI} 

821 
val rev_mp = @{thm rev_mp} 

822 
val subst = @{thm subst} 

823 
val sym = @{thm sym} 

22129  824 
val thin_refl = @{thm thin_refl}; 
42799  825 
); 
21671  826 
open Hypsubst; 
21151  827 

42799  828 
structure Classical = Classical 
829 
( 

26411  830 
val imp_elim = @{thm imp_elim} 
831 
val not_elim = @{thm notE} 

832 
val swap = @{thm swap} 

833 
val classical = @{thm classical} 

21151  834 
val sizef = Drule.size_of_thm 
835 
val hyp_subst_tacs = [Hypsubst.hyp_subst_tac] 

42799  836 
); 
21151  837 

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

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

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

840 
*} 
22129  841 

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

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

843 
ML_Antiquote.value @{binding claset} 
48776
37cd53e69840
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents:
48195
diff
changeset

844 
(Scan.succeed "Classical.claset_of ML_context") 
21151  845 
*} 
846 

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

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

848 

21009  849 
setup {* 
850 
let 

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

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

854 
SUBGOAL (fn (goal, i) => 

855 
if Term.exists_Const non_bool_eq goal 

856 
then Hypsubst.hyp_subst_tac i 

857 
else no_tac); 

21009  858 
in 
21151  859 
Hypsubst.hypsubst_setup 
35389  860 
(*prevent substitution on bool*) 
33369  861 
#> Context_Rules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac) 
21009  862 
end 
863 
*} 

864 

865 
declare iffI [intro!] 

866 
and notI [intro!] 

867 
and impI [intro!] 

868 
and disjCI [intro!] 

869 
and conjI [intro!] 

870 
and TrueI [intro!] 

871 
and refl [intro!] 

872 

873 
declare iffCE [elim!] 

874 
and FalseE [elim!] 

875 
and impCE [elim!] 

876 
and disjE [elim!] 

877 
and conjE [elim!] 

878 

879 
declare ex_ex1I [intro!] 

880 
and allI [intro!] 

881 
and the_equality [intro] 

882 
and exI [intro] 

883 

884 
declare exE [elim!] 

885 
allE [elim] 

886 

22377  887 
ML {* val HOL_cs = @{claset} *} 
19162  888 

20223  889 
lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P" 
890 
apply (erule swap) 

891 
apply (erule (1) meta_mp) 

892 
done 

10383  893 

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

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

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

896 

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

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

898 

12386  899 
lemmas [intro?] = ext 
900 
and [elim?] = ex1_implies_ex 

11977  901 

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

906 
shows R 

907 
apply (rule ex1E [OF major]) 

908 
apply (rule prem) 

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

911 
apply iprover 

912 
done 

20944  913 

21151  914 
ML {* 
42477  915 
structure Blast = Blast 
916 
( 

917 
structure Classical = Classical 

42802  918 
val Trueprop_const = dest_Const @{const Trueprop} 
42477  919 
val equality_name = @{const_name HOL.eq} 
920 
val not_name = @{const_name Not} 

921 
val notE = @{thm notE} 

922 
val ccontr = @{thm ccontr} 

923 
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac 

924 
); 

925 
val blast_tac = Blast.blast_tac; 

20944  926 
*} 
927 

21151  928 
setup Blast.setup 
929 

20944  930 

931 
subsubsection {* Simplifier *} 

12281  932 

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

934 

935 
lemma simp_thms: 

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

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

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

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

940 
"(P  ~P) = True" "(~P  P) = True" 
12281  941 
"(x = x) = True" 
32068  942 
and not_True_eq_False [code]: "(\<not> True) = False" 
943 
and not_False_eq_True [code]: "(\<not> False) = True" 

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

945 
"(~P) ~= P" "P ~= (~P)" 
20944  946 
"(True=P) = P" 
947 
and eq_True: "(P = True) = P" 

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

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

950 
and 

12281  951 
"(True > P) = P" "(False > P) = True" 
952 
"(P > True) = True" "(P > P) = True" 

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

954 
"(P & True) = P" "(True & P) = P" 

955 
"(P & False) = False" "(False & P) = False" 

956 
"(P & P) = P" "(P & (P & Q)) = (P & Q)" 

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

958 
"(P  True) = True" "(True  P) = True" 

959 
"(P  False) = P" "(False  P) = P" 

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

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

962 
and 
12281  963 
"!!P. (EX x. x=t & P(x)) = P(t)" 
964 
"!!P. (EX x. t=x & P(x)) = P(t)" 

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

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

966 
"!!P. (ALL x. t=x > P(x)) = P(t)" 
17589  967 
by (blast, blast, blast, blast, blast, iprover+) 
13421  968 

14201  969 
lemma disj_absorb: "(A  A) = A" 
970 
by blast 

971 

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

973 
by blast 

974 

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

976 
by blast 

977 

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

979 
by blast 

980 

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

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

983 
and eq_left_commute: "(P=(Q=R)) = (Q=(P=R))" 
17589  984 
and eq_assoc: "((P=Q)=R) = (P=(Q=R))" by (iprover, blast+) 
985 
lemma neq_commute: "(a~=b) = (b~=a)" by iprover 

12281  986 

987 
lemma conj_comms: 

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

988 
shows conj_commute: "(P&Q) = (Q&P)" 
17589  989 
and conj_left_commute: "(P&(Q&R)) = (Q&(P&R))" by iprover+ 
990 
lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by iprover 

12281  991 

19174  992 
lemmas conj_ac = conj_commute conj_left_commute conj_assoc 
993 

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

995 
shows disj_commute: "(PQ) = (QP)" 
17589  996 
and disj_left_commute: "(P(QR)) = (Q(PR))" by iprover+ 
997 
lemma disj_assoc: "((PQ)R) = (P(QR))" by iprover 

12281  998 

19174  999 
lemmas disj_ac = disj_commute disj_left_commute disj_assoc 
1000 

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

12281  1003 

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

12281  1006 

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

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

12281  1010 

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

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

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

1014 

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

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

1017 

21151  1018 
lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P > Q) = (P' > Q'))" 
1019 
by iprover 

1020 

17589  1021 
lemma de_Morgan_disj: "(~(P  Q)) = (~P & ~Q)" by iprover 
12281  1022 
lemma de_Morgan_conj: "(~(P & Q)) = (~P  ~Q)" by blast 
1023 
lemma not_imp: "(~(P > Q)) = (P & ~Q)" by blast 

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

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

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

1027 
by blast 

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

1029 

17589  1030 
lemma iff_conv_conj_imp: "(P = Q) = ((P > Q) & (Q > P))" by iprover 
12281  1031 

1032 

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

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

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

1036 
by blast 

1037 

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

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

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

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

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

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

1045 

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

12281  1048 

1049 
text {* 

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

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

1052 

1053 
lemma conj_cong: 

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

17589  1055 
by iprover 
12281  1056 

1057 
lemma rev_conj_cong: 

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

17589  1059 
by iprover 
12281  1060 

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

1062 

1063 
lemma disj_cong: 

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

1065 
by blast 

1066 

1067 

1068 
text {* \medskip ifthenelse rules *} 

1069 

32068  1070 
lemma if_True [code]: "(if True then x else y) = x" 
38525  1071 
by (unfold If_def) blast 
12281  1072 

32068  1073 
lemma if_False [code]: "(if False then x else y) = y" 
38525  1074 
by (unfold If_def) blast 
12281  1075 

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

38525  1077 
by (unfold If_def) blast 
12281  1078 

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

38525  1080 
by (unfold If_def) blast 
12281  1081 

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

1083 
apply (rule case_split [of Q]) 

15481  1084 
apply (simplesubst if_P) 
1085 
prefer 3 apply (simplesubst if_not_P, blast+) 

12281  1086 
done 
1087 

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

15481  1089 
by (simplesubst split_if, blast) 
12281  1090 

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

1091 
lemmas if_splits [no_atp] = split_if split_if_asm 
12281  1092 

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

15481  1094 
by (simplesubst split_if, blast) 
12281  1095 

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

15481  1097 
by (simplesubst split_if, blast) 
12281  1098 

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

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

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

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

19796  1105 
 {* And this form is useful for expanding @{text "if"}s on the LEFT. *} 
15481  1106 
apply (simplesubst split_if, blast) 
12281  1107 
done 
1108 

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

12281  1111 

15423  1112 
text {* \medskip let rules for simproc *} 
1113 

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

1115 
by (unfold Let_def) 

1116 

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

1118 
by (unfold Let_def) 

1119 

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

1120 
text {* 
16999  1121 
The following copy of the implication operator is useful for 
1122 
finetuning congruence rules. It instructs the simplifier to simplify 

1123 
its premise. 

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

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

1125 

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

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

1128 

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

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

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

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

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

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

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

1136 

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

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

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

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

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

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

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

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

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

1146 

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

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

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

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

1150 
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

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

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

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

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

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

1157 
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

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

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

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

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

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

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

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

1166 

20944  1167 
lemma uncurry: 
1168 
assumes "P \<longrightarrow> Q \<longrightarrow> R" 

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

23553  1170 
using assms by blast 
20944  1171 

1172 
lemma iff_allI: 

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

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

23553  1175 
using assms by blast 
20944  1176 

1177 
lemma iff_exI: 

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

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

23553  1180 
using assms by blast 
20944  1181 

1182 
lemma all_comm: 

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

1184 
by blast 

1185 

1186 
lemma ex_comm: 

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

1188 
by blast 

1189 

48891  1190 
ML_file "Tools/simpdata.ML" 
21671  1191 
ML {* open Simpdata *} 
42455  1192 

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

1193 
setup {* Simplifier.map_simpset_global (K HOL_basic_ss) *} 
42455  1194 

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

21671  1197 

21151  1198 
setup {* 
1199 
Simplifier.method_setup Splitter.split_modifiers 

1200 
#> Splitter.setup 

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

1201 
#> clasimp_setup 
21151  1202 
#> EqSubst.setup 
1203 
*} 

1204 

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

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

1208 
let 

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

1210 
fun is_neq eq lhs rhs thm = 

1211 
(case Thm.prop_of thm of 

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

1213 
Not = HOLogic.Not andalso eq' = eq andalso 

1214 
r' aconv lhs andalso l' aconv rhs 

1215 
 _ => false); 

1216 
fun proc ss ct = 

1217 
(case Thm.term_of ct of 

1218 
eq $ lhs $ rhs => 

43597  1219 
(case find_first (is_neq eq lhs rhs) (Simplifier.prems_of ss) of 
24035  1220 
SOME thm => SOME (thm RS neq_to_EQ_False) 
1221 
 NONE => NONE) 

1222 
 _ => NONE); 

1223 
in proc end; 

1224 
*} 

1225 

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

1227 
let 

1228 
val (f_Let_unfold, x_Let_unfold) = 

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

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

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

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

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

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

1240 
 count_loose _ _ = 0; 

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

1242 
case t 

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

1244 
 _ => true; 

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

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

42361  1249 
val thy = Proof_Context.theory_of ctxt; 
28741  1250 
val t = Thm.term_of ct; 
1251 
val ([t'], ctxt') = Variable.import_terms false [t] ctxt; 

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

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

1254 
if is_Free x orelse is_Bound x orelse is_Const x 

1255 
then SOME @{thm Let_def} 

1256 
else 

1257 
let 

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

1259 
val cx = cterm_of thy x; 

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

1261 
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

1262 
val fx_g = Simplifier.rewrite ss (Thm.apply cf cx); 
28741  1263 
val (_ $ _ $ g) = prop_of fx_g; 
1264 
val g' = abstract_over (x,g); 

1265 
in (if (g aconv g') 

1266 
then 

1267 
let 

1268 
val rl = 

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

1270 
in SOME (rl OF [fx_g]) end 

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

1272 
else let 

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

1274 
val g'x = abs_g'$x; 

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

1278 
(g_Let_folded, cterm_of thy abs_g')] 

1279 
@{thm Let_folded}; 

36945  1280 
in SOME (rl OF [Thm.transitive fx_g g_g'x]) 
28741  1281 
end) 
1282 
end 

1283 
 _ => NONE) 

1284 
end 

1285 
end *} 

24035  1286 

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

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

21151  1291 
next 
1292 
assume "PROP P" 

23389  1293 
then show "PROP P" . 
21151  1294 
qed 
1295 

1296 
lemma ex_simps: 

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

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

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

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

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

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

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

1304 
by (iprover  blast)+ 

1305 

1306 
lemma all_simps: 

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

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

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

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

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

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

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

1314 
by (iprover  blast)+ 

15481  1315 

21671  1316 
lemmas [simp] = 
1317 
triv_forall_equality (*prunes params*) 

1318 
True_implies_equals (*prune asms `True'*) 

1319 
if_True 

1320 
if_False 

1321 
if_cancel 

1322 
if_eq_cancel 

1323 
imp_disjL 

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

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

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

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

21671  1329 
conj_assoc 
1330 
disj_assoc 

1331 
de_Morgan_conj 

1332 
de_Morgan_disj 

1333 
imp_disj1 

1334 
imp_disj2 

1335 
not_imp 

1336 
disj_not1 

1337 
not_all 

1338 
not_ex 

1339 
cases_simp 

1340 
the_eq_trivial 

1341 
the_sym_eq_trivial 

1342 
ex_simps 

1343 
all_simps 

1344 
simp_thms 

1345 

1346 
lemmas [cong] = imp_cong simp_implies_cong 

1347 
lemmas [split] = split_if 

20973  1348 

22377  1349 
ML {* val HOL_ss = @{simpset} *} 
20973  1350 

20944  1351 
text {* Simplifies x assuming c and y assuming ~c *} 
1352 
lemma if_cong: 

1353 
assumes "b = c" 

1354 
and "c \<Longrightarrow> x = u" 

1355 
and "\<not> c \<Longrightarrow> y = v" 

1356 
shows "(if b then x else y) = (if c then u else v)" 

38525  1357 
using assms by simp 
20944  1358 

1359 
text {* Prevents simplification of x and y: 
