author  nipkow 
Tue, 31 Mar 2015 17:29:44 +0200  
changeset 59864  c777743294e1 
parent 59779  b6bda9140e39 
child 59929  a090551e5ec8 
permissions  rwrr 
923  1 
(* Title: HOL/HOL.thy 
11750  2 
Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson 
3 
*) 

923  4 

58889  5 
section {* The basis of HigherOrder Logic *} 
923  6 

15131  7 
theory HOL 
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
30927
diff
changeset

8 
imports Pure "~~/src/Tools/Code_Generator" 
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46497
diff
changeset

9 
keywords 
52432  10 
"try" "solve_direct" "quickcheck" "print_coercions" "print_claset" 
11 
"print_induct_rules" :: diag and 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

58826  31 
ML_file "~~/src/Tools/intuitionistic.ML" setup \<open>Intuitionistic.method_setup @{binding iprover}\<close> 
48891  32 
ML_file "~~/src/Tools/project_rule.ML" 
33 
ML_file "~~/src/Tools/subtyping.ML" 

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

35 

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

36 

58659
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
57964
diff
changeset

37 
ML \<open>Plugin_Name.declare_setup @{binding extraction}\<close> 
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
57964
diff
changeset

38 

6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
57964
diff
changeset

39 
ML \<open> 
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
57964
diff
changeset

40 
Plugin_Name.declare_setup @{binding quickcheck_random}; 
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
57964
diff
changeset

41 
Plugin_Name.declare_setup @{binding quickcheck_exhaustive}; 
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
57964
diff
changeset

42 
Plugin_Name.declare_setup @{binding quickcheck_bounded_forall}; 
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
57964
diff
changeset

43 
Plugin_Name.declare_setup @{binding quickcheck_full_exhaustive}; 
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
57964
diff
changeset

44 
Plugin_Name.declare_setup @{binding quickcheck_narrowing}; 
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
57964
diff
changeset

45 
\<close> 
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
57964
diff
changeset

46 
ML \<open> 
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
57964
diff
changeset

47 
Plugin_Name.define_setup @{binding quickcheck} 
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
57964
diff
changeset

48 
[@{plugin quickcheck_exhaustive}, 
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
57964
diff
changeset

49 
@{plugin quickcheck_random}, 
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
57964
diff
changeset

50 
@{plugin quickcheck_bounded_forall}, 
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
57964
diff
changeset

51 
@{plugin quickcheck_full_exhaustive}, 
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
57964
diff
changeset

52 
@{plugin quickcheck_narrowing}] 
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
57964
diff
changeset

53 
\<close> 
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
57964
diff
changeset

54 

6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
57964
diff
changeset

55 

11750  56 
subsection {* Primitive logic *} 
57 

58 
subsubsection {* Core syntax *} 

2260  59 

56941
952833323c99
tuned signature to make axiomatizations more easy to spot in the source, via "add_axioms" or "axiomatization";
wenzelm
parents:
56375
diff
changeset

60 
setup {* Axclass.class_axiomatization (@{binding type}, []) *} 
36452  61 
default_sort type 
35625  62 
setup {* Object_Logic.add_base_sort @{sort type} *} 
25460
b80087af2274
interpretation of typedecls: instantiation to class type
haftmann
parents:
25388
diff
changeset

63 

55383  64 
axiomatization where fun_arity: "OFCLASS('a \<Rightarrow> 'b, type_class)" 
65 
instance "fun" :: (type, type) type by (rule fun_arity) 

66 

67 
axiomatization where itself_arity: "OFCLASS('a itself, type_class)" 

68 
instance itself :: (type) type by (rule itself_arity) 

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

69 

7357  70 
typedecl bool 
923  71 

11750  72 
judgment 
73 
Trueprop :: "bool => prop" ("(_)" 5) 

923  74 

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

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

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

79 

11750  80 
consts 
7357  81 
True :: bool 
82 
False :: bool 

38547  83 
Not :: "bool => bool" ("~ _" [40] 40) 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

84 

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

85 
conj :: "[bool, bool] => bool" (infixr "&" 35) 
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

86 
disj :: "[bool, bool] => bool" (infixr "" 30) 
38555  87 

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

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

923  91 

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

92 

11750  93 
subsubsection {* Additional concrete syntax *} 
2260  94 

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

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

97 

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

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

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

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

101 

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

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

104 

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

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

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

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

109 
implies (infixr "\<longrightarrow>" 25) and 
50360
628b37b9e8a2
\<noteq> now has the same associativity as ~= and =
nipkow
parents:
49339
diff
changeset

110 
not_equal (infixl "\<noteq>" 50) 
628b37b9e8a2
\<noteq> now has the same associativity as ~= and =
nipkow
parents:
49339
diff
changeset

111 

628b37b9e8a2
\<noteq> now has the same associativity as ~= and =
nipkow
parents:
49339
diff
changeset

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

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

114 

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

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

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

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

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

120 

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

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

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

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

124 

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

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

127 

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

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

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

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

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

134 
*}  {* To avoid etacontraction of body *} 
923  135 

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

136 
nonterminal letbinds and letbind 
923  137 
syntax 
7357  138 
"_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) 
139 
"" :: "letbind => letbinds" ("_") 

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

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

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

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

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

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

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

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

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

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

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

151 

21524  152 
notation (xsymbols) 
153 
All (binder "\<forall>" 10) and 

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

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

2372  156 

21524  157 
notation (HTML output) 
158 
All (binder "\<forall>" 10) and 

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

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

6340  161 

21524  162 
notation (HOL) 
163 
All (binder "! " 10) and 

164 
Ex (binder "? " 10) and 

165 
Ex1 (binder "?! " 10) 

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

166 

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

167 

11750  168 
subsubsection {* Axioms and basic definitions *} 
2260  169 

46973  170 
axiomatization where 
171 
refl: "t = (t::'a)" and 

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

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

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

46973  176 
rule, and similar to the ABS rule of HOL*} and 
6289  177 

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

178 
the_eq_trivial: "(THE x. x = a) = (a::'a)" 
923  179 

46973  180 
axiomatization where 
181 
impI: "(P ==> Q) ==> P>Q" and 

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

15380  183 

46973  184 
iff: "(P>Q) > (Q>P) > (P=Q)" and 
185 
True_or_False: "(P=True)  (P=False)" 

15380  186 

923  187 
defs 
7357  188 
True_def: "True == ((%x::bool. x) = (%x. x))" 
189 
All_def: "All(P) == (P = (%x. True))" 

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

190 
Ex_def: "Ex(P) == !Q. (!x. P x > Q) > Q" 
7357  191 
False_def: "False == (!P. P)" 
192 
not_def: "~ P == P>False" 

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

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

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

923  196 

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

923  199 

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

38525  202 

203 
translations 

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

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

206 

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

208 

46973  209 
class default = fixes default :: 'a 
4868  210 

11750  211 

20944  212 
subsection {* Fundamental rules *} 
213 

20973  214 
subsubsection {* Equality *} 
20944  215 

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

15411  218 

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

15411  221 

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

18457  223 
by (erule subst) 
15411  224 

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

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

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

227 

58826  228 
lemma meta_eq_to_obj_eq: 
20944  229 
assumes meq: "A == B" 
230 
shows "A = B" 

231 
by (unfold meq) (rule refl) 

15411  232 

21502  233 
text {* Useful with @{text erule} for proving equalities from known equalities. *} 
20944  234 
(* a = b 
15411  235 
  
236 
c = d *) 

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

238 
apply (rule trans) 

239 
apply (rule trans) 

240 
apply (rule sym) 

241 
apply assumption+ 

242 
done 

243 

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

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

245 

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

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

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

248 

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

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

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

251 

15411  252 

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

253 
subsubsection {* Congruence rules for application *} 
15411  254 

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

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

258 
apply (rule refl) 

259 
done 

260 

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

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

264 
apply (rule refl) 

265 
done 

266 

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

269 
apply (rule refl) 

270 
done 

271 

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

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

275 
done 

276 

58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58889
diff
changeset

277 
ML {* fun cong_tac ctxt = Cong_Tac.cong_tac ctxt @{thm cong} *} 
15411  278 

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

279 

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

280 
subsubsection {* Equality of booleans  iff *} 
15411  281 

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

15411  284 

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

18457  286 
by (erule ssubst) 
15411  287 

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

18457  289 
by (erule iffD2) 
15411  290 

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

293 

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

295 
by (drule sym) (rule rev_iffD2) 

15411  296 

297 
lemma iffE: 

298 
assumes major: "P=Q" 

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

15411  302 

303 

20944  304 
subsubsection {*True*} 
15411  305 

306 
lemma TrueI: "True" 

21504  307 
unfolding True_def by (rule refl) 
15411  308 

21504  309 
lemma eqTrueI: "P ==> P = True" 
18457  310 
by (iprover intro: iffI TrueI) 
15411  311 

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

15411  314 

315 

20944  316 
subsubsection {*Universal quantifier*} 
15411  317 

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

15411  320 

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

322 
apply (unfold All_def) 

323 
apply (rule eqTrueE) 

324 
apply (erule fun_cong) 

325 
done 

326 

327 
lemma allE: 

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

21504  329 
and minor: "P(x) ==> R" 
330 
shows R 

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

15411  332 

333 
lemma all_dupE: 

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

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

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

15411  338 

339 

21504  340 
subsubsection {* False *} 
341 

342 
text {* 

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

344 
logic before quantifiers! 

345 
*} 

15411  346 

347 
lemma FalseE: "False ==> P" 

21504  348 
apply (unfold False_def) 
349 
apply (erule spec) 

350 
done 

15411  351 

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

15411  354 

355 

21504  356 
subsubsection {* Negation *} 
15411  357 

358 
lemma notI: 

21504  359 
assumes "P ==> False" 
15411  360 
shows "~P" 
21504  361 
apply (unfold not_def) 
362 
apply (iprover intro: impI assms) 

363 
done 

15411  364 

365 
lemma False_not_True: "False ~= True" 

21504  366 
apply (rule notI) 
367 
apply (erule False_neq_True) 

368 
done 

15411  369 

370 
lemma True_not_False: "True ~= False" 

21504  371 
apply (rule notI) 
372 
apply (drule sym) 

373 
apply (erule False_neq_True) 

374 
done 

15411  375 

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

21504  377 
apply (unfold not_def) 
378 
apply (erule mp [THEN FalseE]) 

379 
apply assumption 

380 
done 

15411  381 

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

15411  384 

385 

20944  386 
subsubsection {*Implication*} 
15411  387 

388 
lemma impE: 

389 
assumes "P>Q" "P" "Q ==> R" 

390 
shows "R" 

23553  391 
by (iprover intro: assms mp) 
15411  392 

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

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

17589  395 
by (iprover intro: mp) 
15411  396 

397 
lemma contrapos_nn: 

398 
assumes major: "~Q" 

399 
and minor: "P==>Q" 

400 
shows "~P" 

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

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

404 
lemma contrapos_pn: 

405 
assumes major: "Q" 

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

407 
shows "~P" 

17589  408 
by (iprover intro: notI minor major notE) 
15411  409 

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

21250  411 
by (erule contrapos_nn) (erule sym) 
412 

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

414 
by (erule subst, erule ssubst, assumption) 

15411  415 

416 

20944  417 
subsubsection {*Existential quantifier*} 
15411  418 

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

420 
apply (unfold Ex_def) 

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

424 
lemma exE: 

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

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

427 
shows "Q" 

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

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

432 

20944  433 
subsubsection {*Conjunction*} 
15411  434 

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

436 
apply (unfold and_def) 

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

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

441 
apply (unfold and_def) 

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

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

446 
apply (unfold and_def) 

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

450 
lemma conjE: 

451 
assumes major: "P&Q" 

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

453 
shows "R" 

454 
apply (rule minor) 

455 
apply (rule major [THEN conjunct1]) 

456 
apply (rule major [THEN conjunct2]) 

457 
done 

458 

459 
lemma context_conjI: 

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

15411  462 

463 

20944  464 
subsubsection {*Disjunction*} 
15411  465 

466 
lemma disjI1: "P ==> PQ" 

467 
apply (unfold or_def) 

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

471 
lemma disjI2: "Q ==> PQ" 

472 
apply (unfold or_def) 

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

476 
lemma disjE: 

477 
assumes major: "PQ" 

478 
and minorP: "P ==> R" 

479 
and minorQ: "Q ==> R" 

480 
shows "R" 

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

484 

20944  485 
subsubsection {*Classical logic*} 
15411  486 

487 
lemma classical: 

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

489 
shows "P" 

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

491 
apply assumption 

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

493 
apply (erule subst) 

494 
apply assumption 

495 
done 

496 

45607  497 
lemmas ccontr = FalseE [THEN classical] 
15411  498 

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

500 
make elimination rules*) 

501 
lemma rev_notE: 

502 
assumes premp: "P" 

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

504 
shows "R" 

505 
apply (rule ccontr) 

506 
apply (erule notE [OF premnot premp]) 

507 
done 

508 

509 
(*Double negation law*) 

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

511 
apply (rule classical) 

512 
apply (erule notE) 

513 
apply assumption 

514 
done 

515 

516 
lemma contrapos_pp: 

517 
assumes p1: "Q" 

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

519 
shows "P" 

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

522 

20944  523 
subsubsection {*Unique existence*} 
15411  524 

525 
lemma ex1I: 

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

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

531 
lemma ex_ex1I: 

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

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

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

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

537 
lemma ex1E: 

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

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

540 
shows "R" 

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

542 
apply (erule conjE) 

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

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

547 
apply (erule ex1E) 

548 
apply (rule exI) 

549 
apply assumption 

550 
done 

551 

552 

20944  553 
subsubsection {*Classical intro rules for disjunction and existential quantifiers*} 
15411  554 

555 
lemma disjCI: 

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

557 
apply (rule classical) 

23553  558 
apply (iprover intro: assms disjI1 disjI2 notI elim: notE) 
15411  559 
done 
560 

561 
lemma excluded_middle: "~P  P" 

17589  562 
by (iprover intro: disjCI) 
15411  563 

20944  564 
text {* 
565 
case distinction as a natural deduction rule. 

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

567 
*} 

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

568 
lemma case_split [case_names True False]: 
15411  569 
assumes prem1: "P ==> Q" 
570 
and prem2: "~P ==> Q" 

571 
shows "Q" 

572 
apply (rule excluded_middle [THEN disjE]) 

573 
apply (erule prem2) 

574 
apply (erule prem1) 

575 
done 

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

576 

15411  577 
(*Classical implies (>) elimination. *) 
578 
lemma impCE: 

579 
assumes major: "P>Q" 

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

581 
shows "R" 

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

17589  583 
apply (iprover intro: minor major [THEN mp])+ 
15411  584 
done 
585 

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

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

588 
default: would break old proofs.*) 

589 
lemma impCE': 

590 
assumes major: "P>Q" 

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

592 
shows "R" 

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

17589  594 
apply (iprover intro: minor major [THEN mp])+ 
15411  595 
done 
596 

597 
(*Classical <> elimination. *) 

598 
lemma iffCE: 

599 
assumes major: "P=Q" 

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

601 
shows "R" 

602 
apply (rule major [THEN iffE]) 

17589  603 
apply (iprover intro: minor elim: impCE notE) 
15411  604 
done 
605 

606 
lemma exCI: 

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

608 
shows "EX x. P(x)" 

609 
apply (rule ccontr) 

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

613 

12386  614 
subsubsection {* Intuitionistic Reasoning *} 
615 

616 
lemma impE': 

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

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

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

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

620 
shows R 
12386  621 
proof  
622 
from 3 and 1 have P . 

623 
with 1 have Q by (rule impE) 

624 
with 2 show R . 

625 
qed 

626 

627 
lemma allE': 

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

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

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

630 
shows Q 
12386  631 
proof  
632 
from 1 have "P x" by (rule spec) 

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

634 
qed 

635 

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

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

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

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

639 
shows R 
12386  640 
proof  
641 
from 2 and 1 have P . 

642 
with 1 show R by (rule notE) 

643 
qed 

644 

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

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

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

647 

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

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

651 
and [Pure.intro] = exI disjI2 disjI1 

12386  652 

653 
lemmas [trans] = trans 

654 
and [sym] = sym not_sym 

15801  655 
and [Pure.elim?] = iffD1 iffD2 impE 
11750  656 

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

657 

11750  658 
subsubsection {* Atomizing metalevel connectives *} 
659 

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

662 

11750  663 
lemma atomize_all [atomize]: "(!!x. P x) == Trueprop (ALL x. P x)" 
12003  664 
proof 
9488  665 
assume "!!x. P x" 
23389  666 
then show "ALL x. P x" .. 
9488  667 
next 
668 
assume "ALL x. P x" 

23553  669 
then show "!!x. P x" by (rule allE) 
9488  670 
qed 
671 

11750  672 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
12003  673 
proof 
9488  674 
assume r: "A ==> B" 
10383  675 
show "A > B" by (rule impI) (rule r) 
9488  676 
next 
677 
assume "A > B" and A 

23553  678 
then show B by (rule mp) 
9488  679 
qed 
680 

14749  681 
lemma atomize_not: "(A ==> False) == Trueprop (~A)" 
682 
proof 

683 
assume r: "A ==> False" 

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

685 
next 

686 
assume "~A" and A 

23553  687 
then show False by (rule notE) 
14749  688 
qed 
689 

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

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

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

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

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

698 

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

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

701 
assume conj: "A &&& B" 
19121  702 
show "A & B" 
703 
proof (rule conjI) 

704 
from conj show A by (rule conjunctionD1) 

705 
from conj show B by (rule conjunctionD2) 

706 
qed 

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

709 
show "A &&& B" 
19121  710 
proof  
711 
from conj show A .. 

712 
from conj show B .. 

11953  713 
qed 
714 
qed 

715 

12386  716 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
18832  717 
and [symmetric, defn] = atomize_all atomize_imp atomize_eq 
12386  718 

11750  719 

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

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

721 

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

722 
lemma atomize_exL[atomize_elim]: "(!!x. P x ==> Q) == ((EX x. P x) ==> Q)" 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset

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

724 

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

725 
lemma atomize_conjL[atomize_elim]: "(A ==> B ==> C) == (A & B ==> C)" 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset

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

727 

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

728 
lemma atomize_disjL[atomize_elim]: "((A ==> C) ==> (B ==> C) ==> C) == ((A  B ==> C) ==> C)" 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset

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

730 

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

731 
lemma atomize_elimL[atomize_elim]: "(!!B. (A ==> B) ==> B) == Trueprop A" .. 
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset

732 

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

733 

20944  734 
subsection {* Package setup *} 
735 

51314
eac4bb5adbf9
just one HOLogic.Trueprop_conv, with regular exception CTERM;
wenzelm
parents:
51304
diff
changeset

736 
ML_file "Tools/hologic.ML" 
eac4bb5adbf9
just one HOLogic.Trueprop_conv, with regular exception CTERM;
wenzelm
parents:
51304
diff
changeset

737 

eac4bb5adbf9
just one HOLogic.Trueprop_conv, with regular exception CTERM;
wenzelm
parents:
51304
diff
changeset

738 

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

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

740 

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

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

742 
Theorems blacklisted to Sledgehammer. These theorems typically produce clauses 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset

743 
that are prolific (match too many equality or membership literals) and relate to 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset

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

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

746 

57963  747 
named_theorems no_atp "theorems that should be filtered out by Sledgehammer" 
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset

748 

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

749 

11750  750 
subsubsection {* Classical Reasoner setup *} 
9529  751 

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

754 

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

756 
by (rule classical) iprover 

757 

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

760 

21151  761 
ML {* 
42799  762 
structure Hypsubst = Hypsubst 
763 
( 

21218  764 
val dest_eq = HOLogic.dest_eq 
21151  765 
val dest_Trueprop = HOLogic.dest_Trueprop 
766 
val dest_imp = HOLogic.dest_imp 

26411  767 
val eq_reflection = @{thm eq_reflection} 
768 
val rev_eq_reflection = @{thm meta_eq_to_obj_eq} 

769 
val imp_intr = @{thm impI} 

770 
val rev_mp = @{thm rev_mp} 

771 
val subst = @{thm subst} 

772 
val sym = @{thm sym} 

22129  773 
val thin_refl = @{thm thin_refl}; 
42799  774 
); 
21671  775 
open Hypsubst; 
21151  776 

42799  777 
structure Classical = Classical 
778 
( 

26411  779 
val imp_elim = @{thm imp_elim} 
780 
val not_elim = @{thm notE} 

781 
val swap = @{thm swap} 

782 
val classical = @{thm classical} 

21151  783 
val sizef = Drule.size_of_thm 
784 
val hyp_subst_tacs = [Hypsubst.hyp_subst_tac] 

42799  785 
); 
21151  786 

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

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

789 
*} 
22129  790 

21009  791 
setup {* 
35389  792 
(*prevent substitution on bool*) 
58826  793 
let 
794 
fun non_bool_eq (@{const_name HOL.eq}, Type (_, [T, _])) = T <> @{typ bool} 

795 
 non_bool_eq _ = false; 

796 
fun hyp_subst_tac' ctxt = 

797 
SUBGOAL (fn (goal, i) => 

798 
if Term.exists_Const non_bool_eq goal 

799 
then Hypsubst.hyp_subst_tac ctxt i 

800 
else no_tac); 

801 
in 

802 
Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac' ctxt ORELSE' tac) 

803 
end 

21009  804 
*} 
805 

806 
declare iffI [intro!] 

807 
and notI [intro!] 

808 
and impI [intro!] 

809 
and disjCI [intro!] 

810 
and conjI [intro!] 

811 
and TrueI [intro!] 

812 
and refl [intro!] 

813 

814 
declare iffCE [elim!] 

815 
and FalseE [elim!] 

816 
and impCE [elim!] 

817 
and disjE [elim!] 

818 
and conjE [elim!] 

819 

820 
declare ex_ex1I [intro!] 

821 
and allI [intro!] 

822 
and exI [intro] 

823 

824 
declare exE [elim!] 

825 
allE [elim] 

826 

51687
3d8720271ebf
discontinued obsolete ML antiquotation @{claset};
wenzelm
parents:
51314
diff
changeset

827 
ML {* val HOL_cs = claset_of @{context} *} 
19162  828 

20223  829 
lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P" 
830 
apply (erule swap) 

831 
apply (erule (1) meta_mp) 

832 
done 

10383  833 

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

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

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

836 

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

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

838 

12386  839 
lemmas [intro?] = ext 
840 
and [elim?] = ex1_implies_ex 

11977  841 

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

846 
shows R 

847 
apply (rule ex1E [OF major]) 

848 
apply (rule prem) 

59499  849 
apply assumption 
850 
apply (rule allI)+ 

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59028
diff
changeset

851 
apply (tactic {* eresolve_tac @{context} [Classical.dup_elim NONE @{thm allE}] 1 *}) 
22129  852 
apply iprover 
853 
done 

20944  854 

21151  855 
ML {* 
42477  856 
structure Blast = Blast 
857 
( 

858 
structure Classical = Classical 

42802  859 
val Trueprop_const = dest_Const @{const Trueprop} 
42477  860 
val equality_name = @{const_name HOL.eq} 
861 
val not_name = @{const_name Not} 

862 
val notE = @{thm notE} 

863 
val ccontr = @{thm ccontr} 

864 
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac 

865 
); 

866 
val blast_tac = Blast.blast_tac; 

20944  867 
*} 
868 

869 

59504
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

870 
subsubsection {*THE: definite description operator*} 
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

871 

8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

872 
lemma the_equality [intro]: 
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

873 
assumes "P a" 
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

874 
and "!!x. P x ==> x=a" 
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

875 
shows "(THE x. P x) = a" 
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

876 
by (blast intro: assms trans [OF arg_cong [where f=The] the_eq_trivial]) 
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

877 

8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

878 
lemma theI: 
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

879 
assumes "P a" and "!!x. P x ==> x=a" 
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

880 
shows "P (THE x. P x)" 
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

881 
by (iprover intro: assms the_equality [THEN ssubst]) 
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

882 

8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

883 
lemma theI': "EX! x. P x ==> P (THE x. P x)" 
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

884 
by (blast intro: theI) 
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

885 

8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

886 
(*Easier to apply than theI: only one occurrence of P*) 
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

887 
lemma theI2: 
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

888 
assumes "P a" "!!x. P x ==> x=a" "!!x. P x ==> Q x" 
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

889 
shows "Q (THE x. P x)" 
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

890 
by (iprover intro: assms theI) 
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

891 

8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

892 
lemma the1I2: assumes "EX! x. P x" "\<And>x. P x \<Longrightarrow> Q x" shows "Q (THE x. P x)" 
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

893 
by(iprover intro:assms(2) theI2[where P=P and Q=Q] ex1E[OF assms(1)] 
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

894 
elim:allE impE) 
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

895 

8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

896 
lemma the1_equality [elim?]: "[ EX!x. P x; P a ] ==> (THE x. P x) = a" 
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

897 
by blast 
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

898 

8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

899 
lemma the_sym_eq_trivial: "(THE y. x=y) = x" 
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

900 
by blast 
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

901 

8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

902 

20944  903 
subsubsection {* Simplifier *} 
12281  904 

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

906 

907 
lemma simp_thms: 

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

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

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

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

912 
"(P  ~P) = True" "(~P  P) = True" 
12281  913 
"(x = x) = True" 
32068  914 
and not_True_eq_False [code]: "(\<not> True) = False" 
915 
and not_False_eq_True [code]: "(\<not> False) = True" 

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

917 
"(~P) ~= P" "P ~= (~P)" 
20944  918 
"(True=P) = P" 
919 
and eq_True: "(P = True) = P" 

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

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

922 
and 

12281  923 
"(True > P) = P" "(False > P) = True" 
924 
"(P > True) = True" "(P > P) = True" 

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

926 
"(P & True) = P" "(True & P) = P" 

927 
"(P & False) = False" "(False & P) = False" 

928 
"(P & P) = P" "(P & (P & Q)) = (P & Q)" 

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

930 
"(P  True) = True" "(True  P) = True" 

931 
"(P  False) = P" "(False  P) = P" 

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

932 
"(P  P) = P" "(P  (P  Q)) = (P  Q)" and 
12281  933 
"(ALL x. P) = P" "(EX x. P) = P" "EX x. x=t" "EX x. t=x" 
31166
a90fe83f58ea
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents:
31156
diff
changeset

934 
and 
12281  935 
"!!P. (EX x. x=t & P(x)) = P(t)" 
936 
"!!P. (EX x. t=x & P(x)) = P(t)" 

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

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

938 
"!!P. (ALL x. t=x > P(x)) = P(t)" 
17589  939 
by (blast, blast, blast, blast, blast, iprover+) 
13421  940 

14201  941 
lemma disj_absorb: "(A  A) = A" 
942 
by blast 

943 

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

945 
by blast 

946 

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

948 
by blast 

949 

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

951 
by blast 

952 

12281  953 
lemma eq_ac: 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56941
diff
changeset

954 
shows eq_commute: "a = b \<longleftrightarrow> b = a" 
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56941
diff
changeset

955 
and iff_left_commute: "(P \<longleftrightarrow> (Q \<longleftrightarrow> R)) \<longleftrightarrow> (Q \<longleftrightarrow> (P \<longleftrightarrow> R))" 
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56941
diff
changeset

956 
and iff_assoc: "((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))" by (iprover, blast+) 
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56941
diff
changeset

957 
lemma neq_commute: "a \<noteq> b \<longleftrightarrow> b \<noteq> a" by iprover 
12281  958 

959 
lemma conj_comms: 

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

960 
shows conj_commute: "(P&Q) = (Q&P)" 
17589  961 
and conj_left_commute: "(P&(Q&R)) = (Q&(P&R))" by iprover+ 
962 
lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by iprover 

12281  963 

19174  964 
lemmas conj_ac = conj_commute conj_left_commute conj_assoc 
965 

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

967 
shows disj_commute: "(PQ) = (QP)" 
17589  968 
and disj_left_commute: "(P(QR)) = (Q(PR))" by iprover+ 
969 
lemma disj_assoc: "((PQ)R) = (P(QR))" by iprover 

12281  970 

19174  971 
lemmas disj_ac = disj_commute disj_left_commute disj_assoc 
972 

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

12281  975 

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

12281  978 

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

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

12281  982 

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

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

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

986 

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

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

989 

21151  990 
lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P > Q) = (P' > Q'))" 
991 
by iprover 

992 

17589  993 
lemma de_Morgan_disj: "(~(P  Q)) = (~P & ~Q)" by iprover 
12281  994 
lemma de_Morgan_conj: "(~(P & Q)) = (~P  ~Q)" by blast 
995 
lemma not_imp: "(~(P > Q)) = (P & ~Q)" by blast 

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

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

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

999 
by blast 

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

1001 

17589  1002 
lemma iff_conv_conj_imp: "(P = Q) = ((P > Q) & (Q > P))" by iprover 
12281  1003 

1004 

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

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

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

1008 
by blast 

1009 

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

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

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

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

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

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

1017 

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

12281  1020 

1021 
text {* 

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

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

1024 

1025 
lemma conj_cong: 

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

17589  1027 
by iprover 
12281  1028 

1029 
lemma rev_conj_cong: 

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

17589  1031 
by iprover 
12281  1032 

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

1034 

1035 
lemma disj_cong: 

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

1037 
by blast 

1038 

1039 

1040 
text {* \medskip ifthenelse rules *} 

1041 

32068  1042 
lemma if_True [code]: "(if True then x else y) = x" 
38525  1043 
by (unfold If_def) blast 
12281  1044 

32068  1045 
lemma if_False [code]: "(if False then x else y) = y" 
38525  1046 
by (unfold If_def) blast 
12281  1047 

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

38525  1049 
by (unfold If_def) blast 
12281  1050 

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

38525  1052 
by (unfold If_def) blast 
12281  1053 

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

1055 
apply (rule case_split [of Q]) 

15481  1056 
apply (simplesubst if_P) 
1057 
prefer 3 apply (simplesubst if_not_P, blast+) 

12281  1058 
done 
1059 

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

15481  1061 
by (simplesubst split_if, blast) 
12281  1062 

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

1063 
lemmas if_splits [no_atp] = split_if split_if_asm 
12281  1064 

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

15481  1066 
by (simplesubst split_if, blast) 
12281  1067 

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

15481  1069 
by (simplesubst split_if, blast) 
12281  1070 

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

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

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

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

19796  1077 
 {* And this form is useful for expanding @{text "if"}s on the LEFT. *} 
59504
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

1078 
by (simplesubst split_if) blast 
12281  1079 

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

12281  1082 

15423  1083 
text {* \medskip let rules for simproc *} 
1084 

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

1086 
by (unfold Let_def) 

1087 

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

1089 
by (unfold Let_def) 

1090 

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

1091 
text {* 
16999  1092 
The following copy of the implication operator is useful for 
1093 
finetuning congruence rules. It instructs the simplifier to simplify 

1094 
its premise. 

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

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

1096 

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

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

1099 

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

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

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

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

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

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

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

1107 

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

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

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

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

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

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

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

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

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

1117 

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

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

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

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

1121 
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

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

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

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

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

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

1128 
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

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

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

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

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

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

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

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

1137 

20944  1138 
lemma uncurry: 
1139 
assumes "P \<longrightarrow> Q \<longrightarrow> R" 

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

23553  1141 
using assms by blast 
20944  1142 

1143 
lemma iff_allI: 

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

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

23553  1146 
using assms by blast 
20944  1147 

1148 
lemma iff_exI: 

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

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

23553  1151 
using assms by blast 
20944  1152 

1153 
lemma all_comm: 

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

1155 
by blast 

1156 

1157 
lemma ex_comm: 

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

1159 
by blast 

1160 

48891  1161 
ML_file "Tools/simpdata.ML" 
21671  1162 
ML {* open Simpdata *} 
42455  1163 

58826  1164 
setup {* 
1165 
map_theory_simpset (put_simpset HOL_basic_ss) #> 

1166 
Simplifier.method_setup Splitter.split_modifiers 

1167 
*} 

42455  1168 

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

21671  1171 

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

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

1175 
let 

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

1177 
fun is_neq eq lhs rhs thm = 

1178 
(case Thm.prop_of thm of 

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

1180 
Not = HOLogic.Not andalso eq' = eq andalso 

1181 
r' aconv lhs andalso l' aconv rhs 

1182 
 _ => false); 

1183 
fun proc ss ct = 

1184 
(case Thm.term_of ct of 

1185 
eq $ lhs $ rhs => 

43597  1186 
(case find_first (is_neq eq lhs rhs) (Simplifier.prems_of ss) of 
24035  1187 
SOME thm => SOME (thm RS neq_to_EQ_False) 
1188 
 NONE => NONE) 

1189 
 _ => NONE); 

1190 
in proc end; 

1191 
*} 

1192 

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

1194 
let 

1195 
val (f_Let_unfold, x_Let_unfold) = 

59582  1196 
let val [(_ $ (f $ x) $ _)] = Thm.prems_of @{thm Let_unfold} 
59628  1197 
in apply2 (Thm.cterm_of @{context}) (f, x) end 
24035  1198 
val (f_Let_folded, x_Let_folded) = 
59582  1199 
let val [(_ $ (f $ x) $ _)] = Thm.prems_of @{thm Let_folded} 
59628  1200 
in apply2 (Thm.cterm_of @{context}) (f, x) end; 
24035  1201 
val g_Let_folded = 
59582  1202 
let val [(_ $ _ $ (g $ _))] = Thm.prems_of @{thm Let_folded} 
59628  1203 
in Thm.cterm_of @{context} g end; 
28741  1204 
fun count_loose (Bound i) k = if i >= k then 1 else 0 
1205 
 count_loose (s $ t) k = count_loose s k + count_loose t k 

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

1207 
 count_loose _ _ = 0; 

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

59628  1209 
(case t of 
1210 
Abs (_, _, t') => count_loose t' 0 <= 1 

1211 
 _ => true); 

1212 
in 

1213 
fn _ => fn ctxt => fn ct => 

1214 
if is_trivial_let (Thm.term_of ct) 

1215 
then SOME @{thm Let_def} (*no or one ocurrence of bound variable*) 

1216 
else 

1217 
let (*Norbert Schirmer's case*) 

1218 
val t = Thm.term_of ct; 

1219 
val ([t'], ctxt') = Variable.import_terms false [t] ctxt; 

1220 
in 

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

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

1223 
if is_Free x orelse is_Bound x orelse is_Const x 

1224 
then SOME @{thm Let_def} 

1225 
else 

1226 
let 

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

1228 
val cx = Thm.cterm_of ctxt x; 

1229 
val xT = Thm.typ_of_cterm cx; 

1230 
val cf = Thm.cterm_of ctxt f; 

1231 
val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx); 

1232 
val (_ $ _ $ g) = Thm.prop_of fx_g; 

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

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

1235 
in 

1236 
if g aconv g' then 

1237 
let 

1238 
val rl = 

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

1240 
in SOME (rl OF [fx_g]) end 

1241 
else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g') 

1242 
then NONE (*avoid identity conversion*) 

1243 
else 

1244 
let 

1245 
val g'x = abs_g' $ x; 

1246 
val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.cterm_of ctxt g'x)); 

1247 
val rl = 

1248 
@{thm Let_folded} > cterm_instantiate 

1249 
[(f_Let_folded, Thm.cterm_of ctxt f), 

1250 
(x_Let_folded, cx), 

1251 
(g_Let_folded, Thm.cterm_of ctxt abs_g')]; 

1252 
in SOME (rl OF [Thm.transitive fx_g g_g'x]) end 

1253 
end 

1254 
 _ => NONE) 

1255 
end 

28741  1256 
end *} 
24035  1257 

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

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

21151  1262 
next 
1263 
assume "PROP P" 

23389  1264 
then show "PROP P" . 
21151  1265 
qed 
1266 

59864  1267 
lemma implies_True_equals: "(PROP P \<Longrightarrow> True) \<equiv> Trueprop True" 
1268 
by default (intro TrueI) 

1269 

1270 
lemma False_implies_equals: "(False \<Longrightarrow> P) \<equiv> Trueprop True" 

1271 
by default simp_all 

1272 

21151  1273 
lemma ex_simps: 
1274 
"!!P Q. (EX x. P x & Q) = ((EX x. P x) & Q)" 

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

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

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

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

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

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

1281 
by (iprover  blast)+ 

1282 

1283 
lemma all_simps: 

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

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

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

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

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

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

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

1291 
by (iprover  blast)+ 

15481  1292 

21671  1293 
lemmas [simp] = 
1294 
triv_forall_equality (*prunes params*) 

1295 
True_implies_equals (*prune asms `True'*) 

1296 
if_True 

1297 
if_False 

1298 
if_cancel 

1299 
if_eq_cancel 

1300 
imp_disjL 

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

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

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

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

21671  1306 
conj_assoc 
1307 
disj_assoc 

1308 
de_Morgan_conj 

1309 
de_Morgan_disj 

1310 
imp_disj1 

1311 
imp_disj2 

1312 
not_imp 

1313 
disj_not1 

1314 
not_all 

1315 
not_ex 

1316 
cases_simp 

1317 
the_eq_trivial 

1318 
the_sym_eq_trivial 

1319 
ex_simps 

1320 
all_simps 

1321 
simp_thms 

1322 

1323 
lemmas [cong] = imp_cong simp_implies_cong 

1324 
lemmas [split] = split_if 

20973  1325 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51692
diff
changeset

1326 
ML {* val HOL_ss = simpset_of @{context} *} 
20973  1327 

20944  1328 
text {* Simplifies x assuming c and y assuming ~c *} 
1329 
lemma if_cong: 

1330 
assumes "b = c" 

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

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

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

38525  1334 
using assms by simp 
20944  1335 

1336 
text {* Prevents simplification of x and y: 

1337 
faster and allows the execution of functional programs. *} 

1338 
lemma if_weak_cong [cong]: 

1339 
assumes "b = c" 

1340 
shows "(if b then x else y) = (if c then x else y)" 

23553  1341 
using assms by (rule arg_cong) 
20944  1342 

1343 
text {* Prevents simplification of t: much faster *} 

1344 
lemma let_weak_cong: 

1345 
assumes "a = b" 

1346 
shows "(let x = a in t x) = (let x = b in t x)" 
