author  wenzelm 
Sun, 05 Nov 2006 21:44:32 +0100  
changeset 21179  99f546731724 
parent 21151  25bd46916c12 
child 21210  c17fd2df4e9e 
permissions  rwrr 
923  1 
(* Title: HOL/HOL.thy 
2 
ID: $Id$ 

11750  3 
Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson 
4 
*) 

923  5 

11750  6 
header {* The basis of HigherOrder Logic *} 
923  7 

15131  8 
theory HOL 
15140  9 
imports CPure 
21151  10 
uses ("simpdata.ML") "Tools/res_atpset.ML" 
15131  11 
begin 
2260  12 

11750  13 
subsection {* Primitive logic *} 
14 

15 
subsubsection {* Core syntax *} 

2260  16 

14854  17 
classes type 
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12281
diff
changeset

18 
defaultsort type 
3947  19 

12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12281
diff
changeset

20 
global 
923  21 

7357  22 
typedecl bool 
923  23 

24 
arities 

12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12281
diff
changeset

25 
bool :: type 
20590
bf92900995f8
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
haftmann
parents:
20453
diff
changeset

26 
"fun" :: (type, type) type 
923  27 

11750  28 
judgment 
29 
Trueprop :: "bool => prop" ("(_)" 5) 

923  30 

11750  31 
consts 
7357  32 
Not :: "bool => bool" ("~ _" [40] 40) 
33 
True :: bool 

34 
False :: bool 

3947  35 
arbitrary :: 'a 
20172  36 
undefined :: 'a 
923  37 

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

38 
The :: "('a => bool) => 'a" 
7357  39 
All :: "('a => bool) => bool" (binder "ALL " 10) 
40 
Ex :: "('a => bool) => bool" (binder "EX " 10) 

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

42 
Let :: "['a, 'a => 'b] => 'b" 

923  43 

7357  44 
"=" :: "['a, 'a] => bool" (infixl 50) 
45 
& :: "[bool, bool] => bool" (infixr 35) 

46 
"" :: "[bool, bool] => bool" (infixr 30) 

47 
> :: "[bool, bool] => bool" (infixr 25) 

923  48 

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

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

50 

16587  51 
consts 
52 
If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) 

2260  53 

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

54 

11750  55 
subsubsection {* Additional concrete syntax *} 
2260  56 

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

57 
const_syntax (output) 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

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

59 

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

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

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

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

63 

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

64 
const_syntax (output) 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

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

66 

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

67 
const_syntax (xsymbols) 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

68 
Not ("\<not> _" [40] 40) 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

69 
"op &" (infixr "\<and>" 35) 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

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

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

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

73 

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

74 
const_syntax (HTML output) 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

75 
Not ("\<not> _" [40] 40) 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

76 
"op &" (infixr "\<and>" 35) 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

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

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

79 

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

80 
abbreviation (iff) 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

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

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

83 

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

84 
const_syntax (xsymbols) 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19607
diff
changeset

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

86 

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

87 

4868  88 
nonterminals 
923  89 
letbinds letbind 
90 
case_syn cases_syn 

91 

92 
syntax 

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

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

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

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

98 
"_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) 

923  99 

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

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

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

103 
"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/  _") 
923  104 

105 
translations 

13764  106 
"THE x. P" == "The (%x. P)" 
923  107 
"_Let (_binds b bs) e" == "_Let b (_Let bs e)" 
1114  108 
"let x = a in e" == "Let a (%x. e)" 
923  109 

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

110 
print_translation {* 
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset

111 
(* To avoid etacontraction of body: *) 
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset

112 
[("The", fn [Abs abs] => 
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset

113 
let val (x,t) = atomic_abs_tr' abs 
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset

114 
in Syntax.const "_The" $ x $ t end)] 
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13723
diff
changeset

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

116 

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

117 
syntax (xsymbols) 
11687  118 
"ALL " :: "[idts, bool] => bool" ("(3\<forall>_./ _)" [0, 10] 10) 
119 
"EX " :: "[idts, bool] => bool" ("(3\<exists>_./ _)" [0, 10] 10) 

120 
"EX! " :: "[idts, bool] => bool" ("(3\<exists>!_./ _)" [0, 10] 10) 

121 
"_case1" :: "['a, 'b] => case_syn" ("(2_ \<Rightarrow>/ _)" 10) 

14361
ad2f5da643b4
* Support for raw latex output in control symbols: \<^raw...>
schirmer
parents:
14357
diff
changeset

122 
(*"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ \<orelse> _")*) 
2372  123 

6340  124 
syntax (HTML output) 
14565  125 
"ALL " :: "[idts, bool] => bool" ("(3\<forall>_./ _)" [0, 10] 10) 
126 
"EX " :: "[idts, bool] => bool" ("(3\<exists>_./ _)" [0, 10] 10) 

127 
"EX! " :: "[idts, bool] => bool" ("(3\<exists>!_./ _)" [0, 10] 10) 

6340  128 

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

129 
syntax (HOL) 
7357  130 
"ALL " :: "[idts, bool] => bool" ("(3! _./ _)" [0, 10] 10) 
131 
"EX " :: "[idts, bool] => bool" ("(3? _./ _)" [0, 10] 10) 

132 
"EX! " :: "[idts, bool] => bool" ("(3?! _./ _)" [0, 10] 10) 

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

133 

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

134 

11750  135 
subsubsection {* Axioms and basic definitions *} 
2260  136 

7357  137 
axioms 
15380  138 
eq_reflection: "(x=y) ==> (x==y)" 
923  139 

15380  140 
refl: "t = (t::'a)" 
6289  141 

15380  142 
ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)" 
143 
 {*Extensionality is built into the metalogic, and this rule expresses 

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

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

6289  146 

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

147 
the_eq_trivial: "(THE x. x = a) = (a::'a)" 
923  148 

15380  149 
impI: "(P ==> Q) ==> P>Q" 
150 
mp: "[ P>Q; P ] ==> Q" 

151 

152 

923  153 
defs 
7357  154 
True_def: "True == ((%x::bool. x) = (%x. x))" 
155 
All_def: "All(P) == (P = (%x. True))" 

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

156 
Ex_def: "Ex(P) == !Q. (!x. P x > Q) > Q" 
7357  157 
False_def: "False == (!P. P)" 
158 
not_def: "~ P == P>False" 

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

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

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

923  162 

7357  163 
axioms 
164 
iff: "(P>Q) > (Q>P) > (P=Q)" 

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

923  166 

167 
defs 

7357  168 
Let_def: "Let s f == f(s)" 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11438
diff
changeset

169 
if_def: "If P x y == THE z::'a. (P=True > z=x) & (P=False > z=y)" 
5069  170 

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

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

172 
"op =" 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14208
diff
changeset

173 
"op >" 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14208
diff
changeset

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

175 
arbitrary 
20172  176 
undefined 
3320  177 

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

178 

11750  179 
subsubsection {* Generic algebraic operations *} 
4868  180 

20713
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset

181 
class zero = 
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset

182 
fixes zero :: "'a" ("\<^loc>0") 
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset

183 

823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset

184 
class one = 
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset

185 
fixes one :: "'a" ("\<^loc>1") 
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset

186 

823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset

187 
hide (open) const zero one 
20590
bf92900995f8
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
haftmann
parents:
20453
diff
changeset

188 

bf92900995f8
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
haftmann
parents:
20453
diff
changeset

189 
class plus = 
20713
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset

190 
fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>+" 65) 
11750  191 

20590
bf92900995f8
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
haftmann
parents:
20453
diff
changeset

192 
class minus = 
bf92900995f8
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
haftmann
parents:
20453
diff
changeset

193 
fixes uminus :: "'a \<Rightarrow> 'a" 
bf92900995f8
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
haftmann
parents:
20453
diff
changeset

194 
fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>" 65) 
bf92900995f8
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
haftmann
parents:
20453
diff
changeset

195 
fixes abs :: "'a \<Rightarrow> 'a" 
bf92900995f8
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
haftmann
parents:
20453
diff
changeset

196 

bf92900995f8
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
haftmann
parents:
20453
diff
changeset

197 
class times = 
20713
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset

198 
fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>*" 70) 
20590
bf92900995f8
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
haftmann
parents:
20453
diff
changeset

199 

bf92900995f8
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
haftmann
parents:
20453
diff
changeset

200 
class inverse = 
bf92900995f8
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
haftmann
parents:
20453
diff
changeset

201 
fixes inverse :: "'a \<Rightarrow> 'a" 
20713
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset

202 
fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>'/" 70) 
11750  203 

13456
42601eb7553f
special syntax for index "1" (plain numeral hidden by "1" symbol in HOL);
wenzelm
parents:
13438
diff
changeset

204 
syntax 
42601eb7553f
special syntax for index "1" (plain numeral hidden by "1" symbol in HOL);
wenzelm
parents:
13438
diff
changeset

205 
"_index1" :: index ("\<^sub>1") 
42601eb7553f
special syntax for index "1" (plain numeral hidden by "1" symbol in HOL);
wenzelm
parents:
13438
diff
changeset

206 
translations 
14690  207 
(index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>" 
13456
42601eb7553f
special syntax for index "1" (plain numeral hidden by "1" symbol in HOL);
wenzelm
parents:
13438
diff
changeset

208 

11750  209 
typed_print_translation {* 
20713
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset

210 
let 
21179  211 
val syntax_name = Sign.const_syntax_name (the_context ()); 
20713
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset

212 
fun tr' c = (c, fn show_sorts => fn T => fn ts => 
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset

213 
if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match 
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20698
diff
changeset

214 
else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T); 
21179  215 
in map (tr' o Sign.const_syntax_name (the_context ())) ["HOL.one", "HOL.zero"] end; 
11750  216 
*}  {* show types that are presumably too general *} 
217 

20741  218 
const_syntax 
219 
uminus (" _" [81] 80) 

20590
bf92900995f8
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
haftmann
parents:
20453
diff
changeset

220 

20741  221 
const_syntax (xsymbols) 
222 
abs ("\<bar>_\<bar>") 

223 
const_syntax (HTML output) 

224 
abs ("\<bar>_\<bar>") 

11750  225 

226 

20944  227 
subsection {* Fundamental rules *} 
228 

20973  229 
subsubsection {* Equality *} 
20944  230 

231 
text {* Thanks to Stephan Merz *} 

232 
lemma subst: 

233 
assumes eq: "s = t" and p: "P s" 

234 
shows "P t" 

235 
proof  

236 
from eq have meta: "s \<equiv> t" 

237 
by (rule eq_reflection) 

238 
from p show ?thesis 

239 
by (unfold meta) 

240 
qed 

15411  241 

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

15411  244 

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

15411  247 

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

18457  249 
by (erule subst) 
15411  250 

20944  251 
lemma def_imp_eq: 
252 
assumes meq: "A == B" 

253 
shows "A = B" 

18457  254 
by (unfold meq) (rule refl) 
255 

20944  256 
(*a mere copy*) 
257 
lemma meta_eq_to_obj_eq: 

258 
assumes meq: "A == B" 

259 
shows "A = B" 

260 
by (unfold meq) (rule refl) 

15411  261 

20944  262 
text {* Useful with eresolve\_tac for proving equalties from known equalities. *} 
263 
(* a = b 

15411  264 
  
265 
c = d *) 

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

267 
apply (rule trans) 

268 
apply (rule trans) 

269 
apply (rule sym) 

270 
apply assumption+ 

271 
done 

272 

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

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

274 

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

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

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

277 

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

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

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

280 

15411  281 

20944  282 
subsubsection {*Congruence rules for application*} 
15411  283 

284 
(*similar to AP_THM in Gordon's HOL*) 

285 
lemma fun_cong: "(f::'a=>'b) = g ==> f(x)=g(x)" 

286 
apply (erule subst) 

287 
apply (rule refl) 

288 
done 

289 

290 
(*similar to AP_TERM in Gordon's HOL and FOL's subst_context*) 

291 
lemma arg_cong: "x=y ==> f(x)=f(y)" 

292 
apply (erule subst) 

293 
apply (rule refl) 

294 
done 

295 

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

298 
apply (rule refl) 

299 
done 

300 

15411  301 
lemma cong: "[ f = g; (x::'a) = y ] ==> f(x) = g(y)" 
302 
apply (erule subst)+ 

303 
apply (rule refl) 

304 
done 

305 

306 

20944  307 
subsubsection {*Equality of booleans  iff*} 
15411  308 

309 
lemma iffI: assumes prems: "P ==> Q" "Q ==> P" shows "P=Q" 

18457  310 
by (iprover intro: iff [THEN mp, THEN mp] impI prems) 
15411  311 

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

18457  313 
by (erule ssubst) 
15411  314 

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

18457  316 
by (erule iffD2) 
15411  317 

318 
lemmas iffD1 = sym [THEN iffD2, standard] 

319 
lemmas rev_iffD1 = sym [THEN [2] rev_iffD2, standard] 

320 

321 
lemma iffE: 

322 
assumes major: "P=Q" 

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

18457  324 
shows R 
325 
by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1]) 

15411  326 

327 

20944  328 
subsubsection {*True*} 
15411  329 

330 
lemma TrueI: "True" 

18457  331 
by (unfold True_def) (rule refl) 
15411  332 

333 
lemma eqTrueI: "P ==> P=True" 

18457  334 
by (iprover intro: iffI TrueI) 
15411  335 

336 
lemma eqTrueE: "P=True ==> P" 

337 
apply (erule iffD2) 

338 
apply (rule TrueI) 

339 
done 

340 

341 

20944  342 
subsubsection {*Universal quantifier*} 
15411  343 

344 
lemma allI: assumes p: "!!x::'a. P(x)" shows "ALL x. P(x)" 

345 
apply (unfold All_def) 

17589  346 
apply (iprover intro: ext eqTrueI p) 
15411  347 
done 
348 

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

350 
apply (unfold All_def) 

351 
apply (rule eqTrueE) 

352 
apply (erule fun_cong) 

353 
done 

354 

355 
lemma allE: 

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

357 
and minor: "P(x) ==> R" 

358 
shows "R" 

17589  359 
by (iprover intro: minor major [THEN spec]) 
15411  360 

361 
lemma all_dupE: 

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

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

364 
shows "R" 

17589  365 
by (iprover intro: minor major major [THEN spec]) 
15411  366 

367 

20944  368 
subsubsection {*False*} 
15411  369 
(*Depends upon spec; it is impossible to do propositional logic before quantifiers!*) 
370 

371 
lemma FalseE: "False ==> P" 

372 
apply (unfold False_def) 

373 
apply (erule spec) 

374 
done 

375 

376 
lemma False_neq_True: "False=True ==> P" 

377 
by (erule eqTrueE [THEN FalseE]) 

378 

379 

20944  380 
subsubsection {*Negation*} 
15411  381 

382 
lemma notI: 

383 
assumes p: "P ==> False" 

384 
shows "~P" 

385 
apply (unfold not_def) 

17589  386 
apply (iprover intro: impI p) 
15411  387 
done 
388 

389 
lemma False_not_True: "False ~= True" 

390 
apply (rule notI) 

391 
apply (erule False_neq_True) 

392 
done 

393 

394 
lemma True_not_False: "True ~= False" 

395 
apply (rule notI) 

396 
apply (drule sym) 

397 
apply (erule False_neq_True) 

398 
done 

399 

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

401 
apply (unfold not_def) 

402 
apply (erule mp [THEN FalseE]) 

403 
apply assumption 

404 
done 

405 

406 
(* Alternative ~ introduction rule: [ P ==> ~ Pa; P ==> Pa ] ==> ~ P *) 

407 
lemmas notI2 = notE [THEN notI, standard] 

408 

409 

20944  410 
subsubsection {*Implication*} 
15411  411 

412 
lemma impE: 

413 
assumes "P>Q" "P" "Q ==> R" 

414 
shows "R" 

17589  415 
by (iprover intro: prems mp) 
15411  416 

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

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

17589  419 
by (iprover intro: mp) 
15411  420 

421 
lemma contrapos_nn: 

422 
assumes major: "~Q" 

423 
and minor: "P==>Q" 

424 
shows "~P" 

17589  425 
by (iprover intro: notI minor major [THEN notE]) 
15411  426 

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

428 
lemma contrapos_pn: 

429 
assumes major: "Q" 

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

431 
shows "~P" 

17589  432 
by (iprover intro: notI minor major notE) 
15411  433 

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

435 
apply (erule contrapos_nn) 

436 
apply (erule sym) 

437 
done 

438 

439 
(*still used in HOLCF*) 

440 
lemma rev_contrapos: 

441 
assumes pq: "P ==> Q" 

442 
and nq: "~Q" 

443 
shows "~P" 

444 
apply (rule nq [THEN contrapos_nn]) 

445 
apply (erule pq) 

446 
done 

447 

20944  448 
subsubsection {*Existential quantifier*} 
15411  449 

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

451 
apply (unfold Ex_def) 

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

455 
lemma exE: 

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

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

458 
shows "Q" 

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

17589  460 
apply (iprover intro: impI [THEN allI] minor) 
15411  461 
done 
462 

463 

20944  464 
subsubsection {*Conjunction*} 
15411  465 

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

467 
apply (unfold and_def) 

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

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

472 
apply (unfold and_def) 

17589  473 
apply (iprover intro: impI dest: spec mp) 
15411  474 
done 
475 

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

477 
apply (unfold and_def) 

17589  478 
apply (iprover intro: impI dest: spec mp) 
15411  479 
done 
480 

481 
lemma conjE: 

482 
assumes major: "P&Q" 

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

484 
shows "R" 

485 
apply (rule minor) 

486 
apply (rule major [THEN conjunct1]) 

487 
apply (rule major [THEN conjunct2]) 

488 
done 

489 

490 
lemma context_conjI: 

491 
assumes prems: "P" "P ==> Q" shows "P & Q" 

17589  492 
by (iprover intro: conjI prems) 
15411  493 

494 

20944  495 
subsubsection {*Disjunction*} 
15411  496 

497 
lemma disjI1: "P ==> PQ" 

498 
apply (unfold or_def) 

17589  499 
apply (iprover intro: allI impI mp) 
15411  500 
done 
501 

502 
lemma disjI2: "Q ==> PQ" 

503 
apply (unfold or_def) 

17589  504 
apply (iprover intro: allI impI mp) 
15411  505 
done 
506 

507 
lemma disjE: 

508 
assumes major: "PQ" 

509 
and minorP: "P ==> R" 

510 
and minorQ: "Q ==> R" 

511 
shows "R" 

17589  512 
by (iprover intro: minorP minorQ impI 
15411  513 
major [unfolded or_def, THEN spec, THEN mp, THEN mp]) 
514 

515 

20944  516 
subsubsection {*Classical logic*} 
15411  517 

518 
lemma classical: 

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

520 
shows "P" 

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

522 
apply assumption 

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

524 
apply (erule subst) 

525 
apply assumption 

526 
done 

527 

528 
lemmas ccontr = FalseE [THEN classical, standard] 

529 

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

531 
make elimination rules*) 

532 
lemma rev_notE: 

533 
assumes premp: "P" 

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

535 
shows "R" 

536 
apply (rule ccontr) 

537 
apply (erule notE [OF premnot premp]) 

538 
done 

539 

540 
(*Double negation law*) 

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

542 
apply (rule classical) 

543 
apply (erule notE) 

544 
apply assumption 

545 
done 

546 

547 
lemma contrapos_pp: 

548 
assumes p1: "Q" 

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

550 
shows "P" 

17589  551 
by (iprover intro: classical p1 p2 notE) 
15411  552 

553 

20944  554 
subsubsection {*Unique existence*} 
15411  555 

556 
lemma ex1I: 

557 
assumes prems: "P a" "!!x. P(x) ==> x=a" 

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

17589  559 
by (unfold Ex1_def, iprover intro: prems exI conjI allI impI) 
15411  560 

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

562 
lemma ex_ex1I: 

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

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

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

17589  566 
by (iprover intro: ex_prem [THEN exE] ex1I eq) 
15411  567 

568 
lemma ex1E: 

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

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

571 
shows "R" 

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

573 
apply (erule conjE) 

17589  574 
apply (iprover intro: minor) 
15411  575 
done 
576 

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

578 
apply (erule ex1E) 

579 
apply (rule exI) 

580 
apply assumption 

581 
done 

582 

583 

20944  584 
subsubsection {*THE: definite description operator*} 
15411  585 

586 
lemma the_equality: 

587 
assumes prema: "P a" 

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

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

590 
apply (rule trans [OF _ the_eq_trivial]) 

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

592 
apply (rule ext) 

593 
apply (rule iffI) 

594 
apply (erule premx) 

595 
apply (erule ssubst, rule prema) 

596 
done 

597 

598 
lemma theI: 

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

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

17589  601 
by (iprover intro: prems the_equality [THEN ssubst]) 
15411  602 

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

604 
apply (erule ex1E) 

605 
apply (erule theI) 

606 
apply (erule allE) 

607 
apply (erule mp) 

608 
apply assumption 

609 
done 

610 

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

612 
lemma theI2: 

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

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

17589  615 
by (iprover intro: prems theI) 
15411  616 

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

620 
apply (erule ex1E) 

621 
apply (erule all_dupE) 

622 
apply (drule mp) 

623 
apply assumption 

624 
apply (erule ssubst) 

625 
apply (erule allE) 

626 
apply (erule mp) 

627 
apply assumption 

628 
done 

629 

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

631 
apply (rule the_equality) 

632 
apply (rule refl) 

633 
apply (erule sym) 

634 
done 

635 

636 

20944  637 
subsubsection {*Classical intro rules for disjunction and existential quantifiers*} 
15411  638 

639 
lemma disjCI: 

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

641 
apply (rule classical) 

17589  642 
apply (iprover intro: prems disjI1 disjI2 notI elim: notE) 
15411  643 
done 
644 

645 
lemma excluded_middle: "~P  P" 

17589  646 
by (iprover intro: disjCI) 
15411  647 

20944  648 
text {* 
649 
case distinction as a natural deduction rule. 

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

651 
*} 

15411  652 
lemma case_split_thm: 
653 
assumes prem1: "P ==> Q" 

654 
and prem2: "~P ==> Q" 

655 
shows "Q" 

656 
apply (rule excluded_middle [THEN disjE]) 

657 
apply (erule prem2) 

658 
apply (erule prem1) 

659 
done 

20944  660 
lemmas case_split = case_split_thm [case_names True False] 
15411  661 

662 
(*Classical implies (>) elimination. *) 

663 
lemma impCE: 

664 
assumes major: "P>Q" 

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

666 
shows "R" 

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

17589  668 
apply (iprover intro: minor major [THEN mp])+ 
15411  669 
done 
670 

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

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

673 
default: would break old proofs.*) 

674 
lemma impCE': 

675 
assumes major: "P>Q" 

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

677 
shows "R" 

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

17589  679 
apply (iprover intro: minor major [THEN mp])+ 
15411  680 
done 
681 

682 
(*Classical <> elimination. *) 

683 
lemma iffCE: 

684 
assumes major: "P=Q" 

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

686 
shows "R" 

687 
apply (rule major [THEN iffE]) 

17589  688 
apply (iprover intro: minor elim: impCE notE) 
15411  689 
done 
690 

691 
lemma exCI: 

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

693 
shows "EX x. P(x)" 

694 
apply (rule ccontr) 

17589  695 
apply (iprover intro: prems exI allI notI notE [of "\<exists>x. P x"]) 
15411  696 
done 
697 

698 

12386  699 
subsubsection {* Intuitionistic Reasoning *} 
700 

701 
lemma impE': 

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

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

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

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

705 
shows R 
12386  706 
proof  
707 
from 3 and 1 have P . 

708 
with 1 have Q by (rule impE) 

709 
with 2 show R . 

710 
qed 

711 

712 
lemma allE': 

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

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

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

715 
shows Q 
12386  716 
proof  
717 
from 1 have "P x" by (rule spec) 

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

719 
qed 

720 

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

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

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

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

724 
shows R 
12386  725 
proof  
726 
from 2 and 1 have P . 

727 
with 1 show R by (rule notE) 

728 
qed 

729 

15801  730 
lemmas [Pure.elim!] = disjE iffE FalseE conjE exE 
731 
and [Pure.intro!] = iffI conjI impI TrueI notI allI refl 

732 
and [Pure.elim 2] = allE notE' impE' 

733 
and [Pure.intro] = exI disjI2 disjI1 

12386  734 

735 
lemmas [trans] = trans 

736 
and [sym] = sym not_sym 

15801  737 
and [Pure.elim?] = iffD1 iffD2 impE 
11750  738 

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

739 

11750  740 
subsubsection {* Atomizing metalevel connectives *} 
741 

742 
lemma atomize_all [atomize]: "(!!x. P x) == Trueprop (ALL x. P x)" 

12003  743 
proof 
9488  744 
assume "!!x. P x" 
10383  745 
show "ALL x. P x" by (rule allI) 
9488  746 
next 
747 
assume "ALL x. P x" 

10383  748 
thus "!!x. P x" by (rule allE) 
9488  749 
qed 
750 

11750  751 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
12003  752 
proof 
9488  753 
assume r: "A ==> B" 
10383  754 
show "A > B" by (rule impI) (rule r) 
9488  755 
next 
756 
assume "A > B" and A 

10383  757 
thus B by (rule mp) 
9488  758 
qed 
759 

14749  760 
lemma atomize_not: "(A ==> False) == Trueprop (~A)" 
761 
proof 

762 
assume r: "A ==> False" 

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

764 
next 

765 
assume "~A" and A 

766 
thus False by (rule notE) 

767 
qed 

768 

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

771 
assume "x == y" 
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset

772 
show "x = y" by (unfold prems) (rule refl) 
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset

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

774 
assume "x = y" 
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset

775 
thus "x == y" by (rule eq_reflection) 
3dfbc913d184
added axclass inverse and consts inverse, divide (infix "/");
wenzelm
parents:
10383
diff
changeset

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

777 

12023  778 
lemma atomize_conj [atomize]: 
19121  779 
includes meta_conjunction_syntax 
780 
shows "(A && B) == Trueprop (A & B)" 

12003  781 
proof 
19121  782 
assume conj: "A && B" 
783 
show "A & B" 

784 
proof (rule conjI) 

785 
from conj show A by (rule conjunctionD1) 

786 
from conj show B by (rule conjunctionD2) 

787 
qed 

11953  788 
next 
19121  789 
assume conj: "A & B" 
790 
show "A && B" 

791 
proof  

792 
from conj show A .. 

793 
from conj show B .. 

11953  794 
qed 
795 
qed 

796 

12386  797 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
18832  798 
and [symmetric, defn] = atomize_all atomize_imp atomize_eq 
12386  799 

11750  800 

20944  801 
subsection {* Package setup *} 
802 

803 
subsubsection {* Fundamental ML bindings *} 

804 

805 
ML {* 

806 
structure HOL = 

807 
struct 

808 
(*FIXME reduce this to a minimum*) 

809 
val eq_reflection = thm "eq_reflection"; 

810 
val def_imp_eq = thm "def_imp_eq"; 

811 
val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq"; 

812 
val ccontr = thm "ccontr"; 

813 
val impI = thm "impI"; 

814 
val impCE = thm "impCE"; 

815 
val notI = thm "notI"; 

816 
val notE = thm "notE"; 

817 
val iffI = thm "iffI"; 

818 
val iffCE = thm "iffCE"; 

819 
val conjI = thm "conjI"; 

820 
val conjE = thm "conjE"; 

821 
val disjCI = thm "disjCI"; 

822 
val disjE = thm "disjE"; 

823 
val TrueI = thm "TrueI"; 

824 
val FalseE = thm "FalseE"; 

825 
val allI = thm "allI"; 

826 
val allE = thm "allE"; 

827 
val exI = thm "exI"; 

828 
val exE = thm "exE"; 

829 
val ex_ex1I = thm "ex_ex1I"; 

830 
val the_equality = thm "the_equality"; 

831 
val mp = thm "mp"; 

832 
val rev_mp = thm "rev_mp" 

833 
val classical = thm "classical"; 

834 
val subst = thm "subst"; 

835 
val refl = thm "refl"; 

836 
val sym = thm "sym"; 

837 
val trans = thm "trans"; 

838 
val arg_cong = thm "arg_cong"; 

839 
val iffD1 = thm "iffD1"; 

840 
val iffD2 = thm "iffD2"; 

841 
val disjE = thm "disjE"; 

842 
val conjE = thm "conjE"; 

843 
val exE = thm "exE"; 

844 
val contrapos_nn = thm "contrapos_nn"; 

845 
val contrapos_pp = thm "contrapos_pp"; 

846 
val notnotD = thm "notnotD"; 

847 
val conjunct1 = thm "conjunct1"; 

848 
val conjunct2 = thm "conjunct2"; 

849 
val spec = thm "spec"; 

850 
val imp_cong = thm "imp_cong"; 

851 
val the_sym_eq_trivial = thm "the_sym_eq_trivial"; 

852 
val triv_forall_equality = thm "triv_forall_equality"; 

853 
val case_split = thm "case_split_thm"; 

854 
end 

855 
*} 

856 

857 

11750  858 
subsubsection {* Classical Reasoner setup *} 
9529  859 

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

862 

21151  863 
ML {* 
864 
structure Hypsubst = HypsubstFun( 

865 
struct 

866 
structure Simplifier = Simplifier 

867 
val dest_eq = HOLogic.dest_eq_typ 

868 
val dest_Trueprop = HOLogic.dest_Trueprop 

869 
val dest_imp = HOLogic.dest_imp 

870 
val eq_reflection = HOL.eq_reflection 

871 
val rev_eq_reflection = HOL.def_imp_eq 

872 
val imp_intr = HOL.impI 

873 
val rev_mp = HOL.rev_mp 

874 
val subst = HOL.subst 

875 
val sym = HOL.sym 

876 
val thin_refl = thm "thin_refl"; 

877 
end); 

878 

879 
structure Classical = ClassicalFun( 

880 
struct 

881 
val mp = HOL.mp 

882 
val not_elim = HOL.notE 

883 
val classical = HOL.classical 

884 
val sizef = Drule.size_of_thm 

885 
val hyp_subst_tacs = [Hypsubst.hyp_subst_tac] 

886 
end); 

887 

888 
structure BasicClassical: BASIC_CLASSICAL = Classical; 

889 
*} 

890 

21009  891 
setup {* 
892 
let 

893 
(*prevent substitution on bool*) 

894 
fun hyp_subst_tac' i thm = if i <= Thm.nprems_of thm andalso 

895 
Term.exists_Const (fn ("op =", Type (_, [T, _])) => T <> Type ("bool", [])  _ => false) 

896 
(nth (Thm.prems_of thm) (i  1)) then Hypsubst.hyp_subst_tac i thm else no_tac thm; 

897 
in 

21151  898 
Hypsubst.hypsubst_setup 
899 
#> ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac) 

900 
#> Classical.setup 

901 
#> ResAtpset.setup 

21009  902 
end 
903 
*} 

904 

905 
declare iffI [intro!] 

906 
and notI [intro!] 

907 
and impI [intro!] 

908 
and disjCI [intro!] 

909 
and conjI [intro!] 

910 
and TrueI [intro!] 

911 
and refl [intro!] 

912 

913 
declare iffCE [elim!] 

914 
and FalseE [elim!] 

915 
and impCE [elim!] 

916 
and disjE [elim!] 

917 
and conjE [elim!] 

918 
and conjE [elim!] 

919 

920 
declare ex_ex1I [intro!] 

921 
and allI [intro!] 

922 
and the_equality [intro] 

923 
and exI [intro] 

924 

925 
declare exE [elim!] 

926 
allE [elim] 

927 

928 
ML {* 

929 
structure HOL = 

930 
struct 

931 

932 
open HOL; 

933 

934 
val claset = Classical.claset_of (the_context ()); 

935 

936 
end; 

937 
*} 

19162  938 

20223  939 
lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P" 
940 
apply (erule swap) 

941 
apply (erule (1) meta_mp) 

942 
done 

10383  943 

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

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

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

946 

12386  947 
lemmas [intro?] = ext 
948 
and [elim?] = ex1_implies_ex 

11977  949 

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

954 
shows R 

955 
apply (rule ex1E [OF major]) 

956 
apply (rule prem) 

957 
apply (tactic "ares_tac [HOL.allI] 1")+ 

958 
apply (tactic "etac (Classical.dup_elim HOL.allE) 1") 

959 
by iprover 

960 

21151  961 
ML {* 
962 
structure Blast = BlastFun( 

963 
struct 

964 
type claset = Classical.claset 

965 
val equality_name = "op =" 

966 
val not_name = "Not" 

967 
val notE = HOL.notE 

968 
val ccontr = HOL.ccontr 

969 
val contr_tac = Classical.contr_tac 

970 
val dup_intr = Classical.dup_intr 

971 
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac 

972 
val claset = Classical.claset 

973 
val rep_cs = Classical.rep_cs 

974 
val cla_modifiers = Classical.cla_modifiers 

975 
val cla_meth' = Classical.cla_meth' 

976 
end); 

4868  977 

20944  978 
structure HOL = 
979 
struct 

11750  980 

20944  981 
open HOL; 
11750  982 

21151  983 
val Blast_tac = Blast.Blast_tac; 
984 
val blast_tac = Blast.blast_tac; 

985 

20944  986 
fun case_tac a = res_inst_tac [("P", a)] case_split; 
987 

21046
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

988 
(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *) 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

989 
local 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

990 
fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

991 
 wrong_prem (Bound _) = true 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

992 
 wrong_prem _ = false; 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

993 
val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of); 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

994 
in 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

995 
fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]); 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

996 
fun smp_tac j = EVERY'[dresolve_tac (smp j), atac]; 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

997 
end; 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

998 

fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

999 
fun strip_tac i = REPEAT (resolve_tac [impI, allI] i); 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

1000 

fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

1001 
fun Trueprop_conv conv ct = (case term_of ct of 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

1002 
Const ("Trueprop", _) $ _ => 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

1003 
let val (ct1, ct2) = Thm.dest_comb ct 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

1004 
in Thm.combination (Thm.reflexive ct1) (conv ct2) end 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

1005 
 _ => raise TERM ("Trueprop_conv", [])); 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

1006 

21112  1007 
fun Equals_conv conv ct = (case term_of ct of 
1008 
Const ("op =", _) $ _ $ _ => 

1009 
let 

1010 
val ((ct1, ct2), ct3) = (apfst Thm.dest_comb o Thm.dest_comb) ct; 

1011 
in Thm.combination (Thm.combination (Thm.reflexive ct1) (conv ct2)) (conv ct3) end 

1012 
 _ => conv ct); 

1013 

21046
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

1014 
fun constrain_op_eq_thms thy thms = 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

1015 
let 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

1016 
fun add_eq (Const ("op =", ty)) = 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

1017 
fold (insert (eq_fst (op =))) 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

1018 
(Term.add_tvarsT ty []) 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

1019 
 add_eq _ = 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

1020 
I 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

1021 
val eqs = fold (fold_aterms add_eq o Thm.prop_of) thms []; 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

1022 
val instT = map (fn (v_i, sort) => 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

1023 
(Thm.ctyp_of thy (TVar (v_i, sort)), 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

1024 
Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy) (sort, [HOLogic.class_eq]))))) eqs; 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

1025 
in 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

1026 
thms 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

1027 
> map (Thm.instantiate (instT, [])) 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

1028 
end; 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

1029 

20944  1030 
end; 
1031 
*} 

1032 

21151  1033 
setup Blast.setup 
1034 

20944  1035 

1036 
subsubsection {* Simplifier *} 

12281  1037 

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

1039 

1040 
lemma simp_thms: 

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

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

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

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

1045 
"(P  ~P) = True" "(~P  P) = True" 
12281  1046 
"(x = x) = True" 
20944  1047 
and not_True_eq_False: "(\<not> True) = False" 
1048 
and not_False_eq_True: "(\<not> False) = True" 

1049 
and 

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

1050 
"(~P) ~= P" "P ~= (~P)" 
20944  1051 
"(True=P) = P" 
1052 
and eq_True: "(P = True) = P" 

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

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

1055 
and 

12281  1056 
"(True > P) = P" "(False > P) = True" 
1057 
"(P > True) = True" "(P > P) = True" 

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

1059 
"(P & True) = P" "(True & P) = P" 

1060 
"(P & False) = False" "(False & P) = False" 

1061 
"(P & P) = P" "(P & (P & Q)) = (P & Q)" 

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

1063 
"(P  True) = True" "(True  P) = True" 

1064 
"(P  False) = P" "(False  P) = P" 

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

1065 
"(P  P) = P" "(P  (P  Q)) = (P  Q)" and 
12281  1066 
"(ALL x. P) = P" "(EX x. P) = P" "EX x. x=t" "EX x. t=x" 
1067 
 {* needed for the onepointrule quantifier simplification procs *} 

1068 
 {* essential for termination!! *} and 

1069 
"!!P. (EX x. x=t & P(x)) = P(t)" 

1070 
"!!P. (EX x. t=x & P(x)) = P(t)" 

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

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

1072 
"!!P. (ALL x. t=x > P(x)) = P(t)" 
17589  1073 
by (blast, blast, blast, blast, blast, iprover+) 
13421  1074 

14201  1075 
lemma disj_absorb: "(A  A) = A" 
1076 
by blast 

1077 

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

1079 
by blast 

1080 

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

1082 
by blast 

1083 

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

1085 
by blast 

1086 

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

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

1089 
and eq_left_commute: "(P=(Q=R)) = (Q=(P=R))" 
17589  1090 
and eq_assoc: "((P=Q)=R) = (P=(Q=R))" by (iprover, blast+) 
1091 
lemma neq_commute: "(a~=b) = (b~=a)" by iprover 

12281  1092 

1093 
lemma conj_comms: 

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

1094 
shows conj_commute: "(P&Q) = (Q&P)" 
17589  1095 
and conj_left_commute: "(P&(Q&R)) = (Q&(P&R))" by iprover+ 
1096 
lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by iprover 

12281  1097 

19174  1098 
lemmas conj_ac = conj_commute conj_left_commute conj_assoc 
1099 

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

1101 
shows disj_commute: "(PQ) = (QP)" 
17589  1102 
and disj_left_commute: "(P(QR)) = (Q(PR))" by iprover+ 
1103 
lemma disj_assoc: "((PQ)R) = (P(QR))" by iprover 

12281  1104 

19174  1105 
lemmas disj_ac = disj_commute disj_left_commute disj_assoc 
1106 

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

12281  1109 

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

12281  1112 

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

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

12281  1116 

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

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

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

1120 

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

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

1123 

21151  1124 
lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P > Q) = (P' > Q'))" 
1125 
by iprover 

1126 

17589  1127 
lemma de_Morgan_disj: "(~(P  Q)) = (~P & ~Q)" by iprover 
12281  1128 
lemma de_Morgan_conj: "(~(P & Q)) = (~P  ~Q)" by blast 
1129 
lemma not_imp: "(~(P > Q)) = (P & ~Q)" by blast 

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

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

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

1133 
by blast 

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

1135 

17589  1136 
lemma iff_conv_conj_imp: "(P = Q) = ((P > Q) & (Q > P))" by iprover 
12281  1137 

1138 

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

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

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

1142 
by blast 

1143 

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

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

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

12281  1148 

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

12281  1151 

1152 
text {* 

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

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

1155 

1156 
lemma conj_cong: 

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

17589  1158 
by iprover 
12281  1159 

1160 
lemma rev_conj_cong: 

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

17589  1162 
by iprover 
12281  1163 

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

1165 

1166 
lemma disj_cong: 

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

1168 
by blast 

1169 

1170 

1171 
text {* \medskip ifthenelse rules *} 

1172 

1173 
lemma if_True: "(if True then x else y) = x" 

1174 
by (unfold if_def) blast 

1175 

1176 
lemma if_False: "(if False then x else y) = y" 

1177 
by (unfold if_def) blast 

1178 

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

1180 
by (unfold if_def) blast 

1181 

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

1183 
by (unfold if_def) blast 

1184 

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

1186 
apply (rule case_split [of Q]) 

15481  1187 
apply (simplesubst if_P) 
1188 
prefer 3 apply (simplesubst if_not_P, blast+) 

12281  1189 
done 
1190 

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

15481  1192 
by (simplesubst split_if, blast) 
12281  1193 

1194 
lemmas if_splits = split_if split_if_asm 

1195 

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

15481  1197 
by (simplesubst split_if, blast) 
12281  1198 

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

15481  1200 
by (simplesubst split_if, blast) 
12281  1201 

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

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

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

19796  1207 
 {* And this form is useful for expanding @{text "if"}s on the LEFT. *} 
15481  1208 
apply (simplesubst split_if, blast) 
12281  1209 
done 
1210 

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

12281  1213 

15423  1214 
text {* \medskip let rules for simproc *} 
1215 

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

1217 
by (unfold Let_def) 

1218 

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

1220 
by (unfold Let_def) 

1221 

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

1222 
text {* 
16999  1223 
The following copy of the implication operator is useful for 
1224 
finetuning congruence rules. It instructs the simplifier to simplify 

1225 
its premise. 

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

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

1227 

17197  1228 
constdefs 
1229 
simp_implies :: "[prop, prop] => prop" (infixr "=simp=>" 1) 

1230 
"simp_implies \<equiv> op ==>" 

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

1231 

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

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

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

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

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

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

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

1239 

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

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

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

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

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

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

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

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

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

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

1249 

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

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

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

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

1253 
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

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

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

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

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

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

1259 
hence "PROP Q" by (rule PQ) 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1260 
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

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

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

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

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

1265 
hence "PROP Q'" by (rule P'Q') 
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

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

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

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

1269 

20944  1270 
lemma uncurry: 
1271 
assumes "P \<longrightarrow> Q \<longrightarrow> R" 

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

1273 
using prems by blast 

1274 

1275 
lemma iff_allI: 

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

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

1278 
using prems by blast 

1279 

1280 
lemma iff_exI: 

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

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

1283 
using prems by blast 

1284 

1285 
lemma all_comm: 

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

1287 
by blast 

1288 

1289 
lemma ex_comm: 

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

1291 
by blast 

1292 

9869  1293 
use "simpdata.ML" 
21151  1294 
setup {* 
1295 
Simplifier.method_setup Splitter.split_modifiers 

1296 
#> (fn thy => (change_simpset_of thy (fn _ => HOL.simpset_simprocs); thy)) 

1297 
#> Splitter.setup 

1298 
#> Clasimp.setup 

1299 
#> EqSubst.setup 

1300 
*} 

1301 

1302 
lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P" 

1303 
proof 

1304 
assume prem: "True \<Longrightarrow> PROP P" 

1305 
from prem [OF TrueI] show "PROP P" . 

1306 
next 

1307 
assume "PROP P" 

1308 
show "PROP P" . 

1309 
qed 

1310 

1311 
lemma ex_simps: 

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

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

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

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

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

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

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

1319 
by (iprover  blast)+ 

1320 

1321 
lemma all_simps: 

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

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

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

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

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

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

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

1329 
by (iprover  blast)+ 

15481  1330 

20973  1331 
declare triv_forall_equality [simp] (*prunes params*) 
1332 
and True_implies_equals [simp] (*prune asms `True'*) 

1333 
and if_True [simp] 

1334 
and if_False [simp] 

1335 
and if_cancel [simp] 

1336 
and if_eq_cancel [simp] 

1337 
and imp_disjL [simp] 

1338 
(*In general it seems wrong to add distributive laws by default: they 

1339 
might cause exponential blowup. But imp_disjL has been in for a while 

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

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

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

1343 
and conj_assoc [simp] 

1344 
and disj_assoc [simp] 

1345 
and de_Morgan_conj [simp] 

1346 
and de_Morgan_disj [simp] 

1347 
and imp_disj1 [simp] 

1348 
and imp_disj2 [simp] 

1349 
and not_imp [simp] 

1350 
and disj_not1 [simp] 

1351 
and not_all [simp] 

1352 
and not_ex [simp] 

1353 
and cases_simp [simp] 

1354 
and the_eq_trivial [simp] 

1355 
and the_sym_eq_trivial [simp] 

1356 
and ex_simps [simp] 

1357 
and all_simps [simp] 

1358 
and simp_thms [simp] 

1359 
and imp_cong [cong] 

1360 
and simp_implies_cong [cong] 

1361 
and split_if [split] 

1362 

1363 
ML {* 

1364 
structure HOL = 

1365 
struct 

1366 

1367 
open HOL; 

1368 

1369 
val simpset = Simplifier.simpset_of (the_context ()); 

1370 

1371 
end; 

1372 
*} 

1373 

20944  1374 
text {* Simplifies x assuming c and y assuming ~c *} 
1375 
lemma if_cong: 

1376 
assumes "b = c" 

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

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