author  haftmann 
Wed, 08 Nov 2006 19:48:35 +0100  
changeset 21250  a268f6288fb6 
parent 21218  38013c3a77a2 
child 21404  eb85850d3eb7 
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 

21210  57 
notation (output) 
19656
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 

21210  64 
notation (output) 
19656
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 

21210  67 
notation (xsymbols) 
19656
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 

21210  74 
notation (HTML output) 
19656
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 

21210  84 
notation (xsymbols) 
19656
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 

21210  218 
notation 
20741  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 

21210  221 
notation (xsymbols) 
20741  222 
abs ("\<bar>_\<bar>") 
21210  223 
notation (HTML output) 
20741  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" 

21250  435 
by (erule contrapos_nn) (erule sym) 
436 

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

438 
by (erule subst, erule ssubst, assumption) 

15411  439 

440 
(*still used in HOLCF*) 

441 
lemma rev_contrapos: 

442 
assumes pq: "P ==> Q" 

443 
and nq: "~Q" 

444 
shows "~P" 

445 
apply (rule nq [THEN contrapos_nn]) 

446 
apply (erule pq) 

447 
done 

448 

20944  449 
subsubsection {*Existential quantifier*} 
15411  450 

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

452 
apply (unfold Ex_def) 

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

456 
lemma exE: 

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

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

459 
shows "Q" 

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

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

464 

20944  465 
subsubsection {*Conjunction*} 
15411  466 

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

468 
apply (unfold and_def) 

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

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

473 
apply (unfold and_def) 

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

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

478 
apply (unfold and_def) 

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

482 
lemma conjE: 

483 
assumes major: "P&Q" 

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

485 
shows "R" 

486 
apply (rule minor) 

487 
apply (rule major [THEN conjunct1]) 

488 
apply (rule major [THEN conjunct2]) 

489 
done 

490 

491 
lemma context_conjI: 

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

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

495 

20944  496 
subsubsection {*Disjunction*} 
15411  497 

498 
lemma disjI1: "P ==> PQ" 

499 
apply (unfold or_def) 

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

503 
lemma disjI2: "Q ==> PQ" 

504 
apply (unfold or_def) 

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

508 
lemma disjE: 

509 
assumes major: "PQ" 

510 
and minorP: "P ==> R" 

511 
and minorQ: "Q ==> R" 

512 
shows "R" 

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

516 

20944  517 
subsubsection {*Classical logic*} 
15411  518 

519 
lemma classical: 

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

521 
shows "P" 

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

523 
apply assumption 

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

525 
apply (erule subst) 

526 
apply assumption 

527 
done 

528 

529 
lemmas ccontr = FalseE [THEN classical, standard] 

530 

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

532 
make elimination rules*) 

533 
lemma rev_notE: 

534 
assumes premp: "P" 

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

536 
shows "R" 

537 
apply (rule ccontr) 

538 
apply (erule notE [OF premnot premp]) 

539 
done 

540 

541 
(*Double negation law*) 

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

543 
apply (rule classical) 

544 
apply (erule notE) 

545 
apply assumption 

546 
done 

547 

548 
lemma contrapos_pp: 

549 
assumes p1: "Q" 

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

551 
shows "P" 

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

554 

20944  555 
subsubsection {*Unique existence*} 
15411  556 

557 
lemma ex1I: 

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

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

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

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

563 
lemma ex_ex1I: 

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

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

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

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

569 
lemma ex1E: 

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

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

572 
shows "R" 

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

574 
apply (erule conjE) 

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

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

579 
apply (erule ex1E) 

580 
apply (rule exI) 

581 
apply assumption 

582 
done 

583 

584 

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

587 
lemma the_equality: 

588 
assumes prema: "P a" 

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

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

591 
apply (rule trans [OF _ the_eq_trivial]) 

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

593 
apply (rule ext) 

594 
apply (rule iffI) 

595 
apply (erule premx) 

596 
apply (erule ssubst, rule prema) 

597 
done 

598 

599 
lemma theI: 

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

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

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

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

605 
apply (erule ex1E) 

606 
apply (erule theI) 

607 
apply (erule allE) 

608 
apply (erule mp) 

609 
apply assumption 

610 
done 

611 

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

613 
lemma theI2: 

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

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

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

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

621 
apply (erule ex1E) 

622 
apply (erule all_dupE) 

623 
apply (drule mp) 

624 
apply assumption 

625 
apply (erule ssubst) 

626 
apply (erule allE) 

627 
apply (erule mp) 

628 
apply assumption 

629 
done 

630 

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

632 
apply (rule the_equality) 

633 
apply (rule refl) 

634 
apply (erule sym) 

635 
done 

636 

637 

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

640 
lemma disjCI: 

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

642 
apply (rule classical) 

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

646 
lemma excluded_middle: "~P  P" 

17589  647 
by (iprover intro: disjCI) 
15411  648 

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

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

652 
*} 

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

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

656 
shows "Q" 

657 
apply (rule excluded_middle [THEN disjE]) 

658 
apply (erule prem2) 

659 
apply (erule prem1) 

660 
done 

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

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

664 
lemma impCE: 

665 
assumes major: "P>Q" 

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

667 
shows "R" 

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

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

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

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

674 
default: would break old proofs.*) 

675 
lemma impCE': 

676 
assumes major: "P>Q" 

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

678 
shows "R" 

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

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

683 
(*Classical <> elimination. *) 

684 
lemma iffCE: 

685 
assumes major: "P=Q" 

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

687 
shows "R" 

688 
apply (rule major [THEN iffE]) 

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

692 
lemma exCI: 

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

694 
shows "EX x. P(x)" 

695 
apply (rule ccontr) 

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

699 

12386  700 
subsubsection {* Intuitionistic Reasoning *} 
701 

702 
lemma impE': 

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

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

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

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

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

709 
with 1 have Q by (rule impE) 

710 
with 2 show R . 

711 
qed 

712 

713 
lemma allE': 

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

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

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

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

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

720 
qed 

721 

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

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

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

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

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

728 
with 1 show R by (rule notE) 

729 
qed 

730 

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

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

734 
and [Pure.intro] = exI disjI2 disjI1 

12386  735 

736 
lemmas [trans] = trans 

737 
and [sym] = sym not_sym 

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

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

740 

11750  741 
subsubsection {* Atomizing metalevel connectives *} 
742 

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

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

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

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

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

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

763 
assume r: "A ==> False" 

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

765 
next 

766 
assume "~A" and A 

767 
thus False by (rule notE) 

768 
qed 

769 

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

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

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

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

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

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

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

778 

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

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

785 
proof (rule conjI) 

786 
from conj show A by (rule conjunctionD1) 

787 
from conj show B by (rule conjunctionD2) 

788 
qed 

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

792 
proof  

793 
from conj show A .. 

794 
from conj show B .. 

11953  795 
qed 
796 
qed 

797 

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

11750  801 

20944  802 
subsection {* Package setup *} 
803 

804 
subsubsection {* Fundamental ML bindings *} 

805 

806 
ML {* 

807 
structure HOL = 

808 
struct 

809 
(*FIXME reduce this to a minimum*) 

810 
val eq_reflection = thm "eq_reflection"; 

811 
val def_imp_eq = thm "def_imp_eq"; 

812 
val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq"; 

813 
val ccontr = thm "ccontr"; 

814 
val impI = thm "impI"; 

815 
val impCE = thm "impCE"; 

816 
val notI = thm "notI"; 

817 
val notE = thm "notE"; 

818 
val iffI = thm "iffI"; 

819 
val iffCE = thm "iffCE"; 

820 
val conjI = thm "conjI"; 

821 
val conjE = thm "conjE"; 

822 
val disjCI = thm "disjCI"; 

823 
val disjE = thm "disjE"; 

824 
val TrueI = thm "TrueI"; 

825 
val FalseE = thm "FalseE"; 

826 
val allI = thm "allI"; 

827 
val allE = thm "allE"; 

828 
val exI = thm "exI"; 

829 
val exE = thm "exE"; 

830 
val ex_ex1I = thm "ex_ex1I"; 

831 
val the_equality = thm "the_equality"; 

832 
val mp = thm "mp"; 

833 
val rev_mp = thm "rev_mp" 

834 
val classical = thm "classical"; 

835 
val subst = thm "subst"; 

836 
val refl = thm "refl"; 

837 
val sym = thm "sym"; 

838 
val trans = thm "trans"; 

839 
val arg_cong = thm "arg_cong"; 

840 
val iffD1 = thm "iffD1"; 

841 
val iffD2 = thm "iffD2"; 

842 
val disjE = thm "disjE"; 

843 
val conjE = thm "conjE"; 

844 
val exE = thm "exE"; 

845 
val contrapos_nn = thm "contrapos_nn"; 

846 
val contrapos_pp = thm "contrapos_pp"; 

847 
val notnotD = thm "notnotD"; 

848 
val conjunct1 = thm "conjunct1"; 

849 
val conjunct2 = thm "conjunct2"; 

850 
val spec = thm "spec"; 

851 
val imp_cong = thm "imp_cong"; 

852 
val the_sym_eq_trivial = thm "the_sym_eq_trivial"; 

853 
val triv_forall_equality = thm "triv_forall_equality"; 

854 
val case_split = thm "case_split_thm"; 

855 
end 

856 
*} 

857 

858 

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

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

863 

21151  864 
ML {* 
865 
structure Hypsubst = HypsubstFun( 

866 
struct 

867 
structure Simplifier = Simplifier 

21218  868 
val dest_eq = HOLogic.dest_eq 
21151  869 
val dest_Trueprop = HOLogic.dest_Trueprop 
870 
val dest_imp = HOLogic.dest_imp 

871 
val eq_reflection = HOL.eq_reflection 

872 
val rev_eq_reflection = HOL.def_imp_eq 

873 
val imp_intr = HOL.impI 

874 
val rev_mp = HOL.rev_mp 

875 
val subst = HOL.subst 

876 
val sym = HOL.sym 

877 
val thin_refl = thm "thin_refl"; 

878 
end); 

879 

880 
structure Classical = ClassicalFun( 

881 
struct 

882 
val mp = HOL.mp 

883 
val not_elim = HOL.notE 

884 
val classical = HOL.classical 

885 
val sizef = Drule.size_of_thm 

886 
val hyp_subst_tacs = [Hypsubst.hyp_subst_tac] 

887 
end); 

888 

889 
structure BasicClassical: BASIC_CLASSICAL = Classical; 

890 
*} 

891 

21009  892 
setup {* 
893 
let 

894 
(*prevent substitution on bool*) 

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

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

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

898 
in 

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

901 
#> Classical.setup 

902 
#> ResAtpset.setup 

21009  903 
end 
904 
*} 

905 

906 
declare iffI [intro!] 

907 
and notI [intro!] 

908 
and impI [intro!] 

909 
and disjCI [intro!] 

910 
and conjI [intro!] 

911 
and TrueI [intro!] 

912 
and refl [intro!] 

913 

914 
declare iffCE [elim!] 

915 
and FalseE [elim!] 

916 
and impCE [elim!] 

917 
and disjE [elim!] 

918 
and conjE [elim!] 

919 
and conjE [elim!] 

920 

921 
declare ex_ex1I [intro!] 

922 
and allI [intro!] 

923 
and the_equality [intro] 

924 
and exI [intro] 

925 

926 
declare exE [elim!] 

927 
allE [elim] 

928 

929 
ML {* 

930 
structure HOL = 

931 
struct 

932 

933 
open HOL; 

934 

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

936 

937 
end; 

938 
*} 

19162  939 

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

942 
apply (erule (1) meta_mp) 

943 
done 

10383  944 

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

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

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

947 

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

11977  950 

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

955 
shows R 

956 
apply (rule ex1E [OF major]) 

957 
apply (rule prem) 

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

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

960 
by iprover 

961 

21151  962 
ML {* 
963 
structure Blast = BlastFun( 

964 
struct 

965 
type claset = Classical.claset 

966 
val equality_name = "op =" 

967 
val not_name = "Not" 

968 
val notE = HOL.notE 

969 
val ccontr = HOL.ccontr 

970 
val contr_tac = Classical.contr_tac 

971 
val dup_intr = Classical.dup_intr 

972 
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac 

973 
val claset = Classical.claset 

974 
val rep_cs = Classical.rep_cs 

975 
val cla_modifiers = Classical.cla_modifiers 

976 
val cla_meth' = Classical.cla_meth' 

977 
end); 

4868  978 

20944  979 
structure HOL = 
980 
struct 

11750  981 

20944  982 
open HOL; 
11750  983 

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

986 

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

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

989 
(* 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

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

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

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

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

994 
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

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

996 
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

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

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

999 

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

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

1001 

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

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

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

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

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

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

1007 

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

1010 
let 

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

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

1013 
 _ => conv ct); 

1014 

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

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

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

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

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

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

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

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

1022 
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

1023 
val instT = map (fn (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, sort)), 
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
21009
diff
changeset

1025 
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

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

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

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

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

1030 

20944  1031 
end; 
1032 
*} 

1033 

21151  1034 
setup Blast.setup 
1035 

20944  1036 

1037 
subsubsection {* Simplifier *} 

12281  1038 

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

1040 

1041 
lemma simp_thms: 

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

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

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

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

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

1050 
and 

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

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

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

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

1056 
and 

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

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

1060 
"(P & True) = P" "(True & P) = P" 

1061 
"(P & False) = False" "(False & P) = False" 

1062 
"(P & P) = P" "(P & (P & Q)) = (P & Q)" 

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

1064 
"(P  True) = True" "(True  P) = True" 

1065 
"(P  False) = P" "(False  P) = P" 

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

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

1069 
 {* essential for termination!! *} and 

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

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

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

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

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

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

1078 

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

1080 
by blast 

1081 

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

1083 
by blast 

1084 

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

1086 
by blast 

1087 

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

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

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

12281  1093 

1094 
lemma conj_comms: 

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

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

12281  1098 

19174  1099 
lemmas conj_ac = conj_commute conj_left_commute conj_assoc 
1100 

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

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

12281  1105 

19174  1106 
lemmas disj_ac = disj_commute disj_left_commute disj_assoc 
1107 

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

12281  1110 

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

12281  1113 

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

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

12281  1117 

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

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

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

1121 

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

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

1124 

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

1127 

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

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

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

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

1134 
by blast 

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

1136 

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

1139 

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

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

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

1143 
by blast 

1144 

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

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

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

12281  1149 

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

12281  1152 

1153 
text {* 

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

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

1156 

1157 
lemma conj_cong: 

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

17589  1159 
by iprover 
12281  1160 

1161 
lemma rev_conj_cong: 

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

17589  1163 
by iprover 
12281  1164 

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

1166 

1167 
lemma disj_cong: 

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

1169 
by blast 

1170 

1171 

1172 
text {* \medskip ifthenelse rules *} 

1173 

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

1175 
by (unfold if_def) blast 

1176 

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

1178 
by (unfold if_def) blast 

1179 

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

1181 
by (unfold if_def) blast 

1182 

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

1184 
by (unfold if_def) blast 

1185 

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

1187 
apply (rule case_split [of Q]) 

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

12281  1190 
done 
1191 

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

15481  1193 
by (simplesubst split_if, blast) 
12281  1194 

1195 
lemmas if_splits = split_if split_if_asm 

1196 

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

15481  1198 
by (simplesubst split_if, blast) 
12281  1199 

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

15481  1201 
by (simplesubst split_if, blast) 
12281  1202 

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

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

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

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

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

12281  1214 

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

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

1218 
by (unfold Let_def) 

1219 

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

1221 
by (unfold Let_def) 

1222 

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

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

1226 
its premise. 

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

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

1228 

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

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

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

1232 

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

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

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

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

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

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

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

1240 

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

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

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

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

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

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

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

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

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

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

1250 

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

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

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

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

1254 
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

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

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

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

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

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

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

1261 
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

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

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

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

1265 
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

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

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

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

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

1270 

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

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

1274 
using prems by blast 

1275 

1276 
lemma iff_allI: 

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

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

1279 
using prems by blast 

1280 

1281 
lemma iff_exI: 

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

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

1284 
using prems by blast 

1285 

1286 
lemma all_comm: 

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

1288 
by blast 

1289 

1290 
lemma ex_comm: 

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

1292 
by blast 

1293 

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

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

1298 
#> Splitter.setup 

1299 
#> Clasimp.setup 

1300 
#> EqSubst.setup 

1301 
*} 

1302 

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

1304 
proof 

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

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

1307 
next 

1308 
assume "PROP P" 

1309 
show "PROP P" . 

1310 
qed 

1311 

1312 
lemma ex_simps: 

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

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

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

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

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

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

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

1320 
by (iprover  blast)+ 

1321 

1322 
lemma all_simps: 

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

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

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

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

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

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

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

1330 
by (iprover  blast)+ 

15481  1331 

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

1334 
and if_True [simp] 

1335 
and if_False [simp] 

1336 
and if_cancel [simp] 

1337 
and if_eq_cancel [simp] 

1338 
and imp_disjL [simp] 

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

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

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

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

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

1344 
and conj_assoc [simp] 

1345 
and disj_assoc [simp] 

1346 
and de_Morgan_conj [simp] 

1347 
and de_Morgan_disj [simp] 

1348 
and imp_disj1 [simp] 

1349 
and imp_disj2 [simp] 

1350 
and not_imp [simp] 

1351 
and disj_not1 [simp] 

1352 
and not_all [simp] 

1353 
and not_ex [simp] 

1354 
and cases_simp [simp] 

1355 
and the_eq_trivial [simp] 

1356 
and the_sym_eq_trivial [simp] 

1357 
and ex_simps [simp] 

1358 
and all_simps [simp] 

1359 
and simp_thms [simp] 

1360 
and imp_cong [cong] 

1361 
and simp_implies_cong [cong] 

1362 
and split_if [split] 

1363 

1364 
ML {* 

1365 
structure HOL = 

1366 
struct 

1367 

1368 
open HOL; 

1369 

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

1371 

1372 
end; 

1373 
*} 

1374 

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

