author  hoelzl 
Thu, 30 Oct 2014 09:15:54 +0100  
changeset 58830  e05c620eceeb 
parent 58826  2ed2eaabe3df 
child 58839  ccda99401bc8 
permissions  rwrr 
923  1 
(* Title: HOL/HOL.thy 
11750  2 
Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson 
3 
*) 

923  4 

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

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

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

9 
keywords 
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 

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

277 
ML {* val cong_tac = Cong_Tac.cong_tac @{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 {*THE: definite description operator*} 
15411  554 

555 
lemma the_equality: 

556 
assumes prema: "P a" 

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

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

559 
apply (rule trans [OF _ the_eq_trivial]) 

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

561 
apply (rule ext) 

562 
apply (rule iffI) 

563 
apply (erule premx) 

564 
apply (erule ssubst, rule prema) 

565 
done 

566 

567 
lemma theI: 

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

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

23553  570 
by (iprover intro: assms the_equality [THEN ssubst]) 
15411  571 

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

573 
apply (erule ex1E) 

574 
apply (erule theI) 

575 
apply (erule allE) 

576 
apply (erule mp) 

577 
apply assumption 

578 
done 

579 

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

581 
lemma theI2: 

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

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

23553  584 
by (iprover intro: assms theI) 
15411  585 

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

588 
elim:allE impE) 

589 

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

593 
apply (erule ex1E) 

594 
apply (erule all_dupE) 

595 
apply (drule mp) 

596 
apply assumption 

597 
apply (erule ssubst) 

598 
apply (erule allE) 

599 
apply (erule mp) 

600 
apply assumption 

601 
done 

602 

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

604 
apply (rule the_equality) 

605 
apply (rule refl) 

606 
apply (erule sym) 

607 
done 

608 

609 

20944  610 
subsubsection {*Classical intro rules for disjunction and existential quantifiers*} 
15411  611 

612 
lemma disjCI: 

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

614 
apply (rule classical) 

23553  615 
apply (iprover intro: assms disjI1 disjI2 notI elim: notE) 
15411  616 
done 
617 

618 
lemma excluded_middle: "~P  P" 

17589  619 
by (iprover intro: disjCI) 
15411  620 

20944  621 
text {* 
622 
case distinction as a natural deduction rule. 

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

624 
*} 

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

625 
lemma case_split [case_names True False]: 
15411  626 
assumes prem1: "P ==> Q" 
627 
and prem2: "~P ==> Q" 

628 
shows "Q" 

629 
apply (rule excluded_middle [THEN disjE]) 

630 
apply (erule prem2) 

631 
apply (erule prem1) 

632 
done 

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

633 

15411  634 
(*Classical implies (>) elimination. *) 
635 
lemma impCE: 

636 
assumes major: "P>Q" 

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

638 
shows "R" 

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

17589  640 
apply (iprover intro: minor major [THEN mp])+ 
15411  641 
done 
642 

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

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

645 
default: would break old proofs.*) 

646 
lemma impCE': 

647 
assumes major: "P>Q" 

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

649 
shows "R" 

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

17589  651 
apply (iprover intro: minor major [THEN mp])+ 
15411  652 
done 
653 

654 
(*Classical <> elimination. *) 

655 
lemma iffCE: 

656 
assumes major: "P=Q" 

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

658 
shows "R" 

659 
apply (rule major [THEN iffE]) 

17589  660 
apply (iprover intro: minor elim: impCE notE) 
15411  661 
done 
662 

663 
lemma exCI: 

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

665 
shows "EX x. P(x)" 

666 
apply (rule ccontr) 

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

670 

12386  671 
subsubsection {* Intuitionistic Reasoning *} 
672 

673 
lemma impE': 

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

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

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

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

677 
shows R 
12386  678 
proof  
679 
from 3 and 1 have P . 

680 
with 1 have Q by (rule impE) 

681 
with 2 show R . 

682 
qed 

683 

684 
lemma allE': 

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

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

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

687 
shows Q 
12386  688 
proof  
689 
from 1 have "P x" by (rule spec) 

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

691 
qed 

692 

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

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

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

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

696 
shows R 
12386  697 
proof  
698 
from 2 and 1 have P . 

699 
with 1 show R by (rule notE) 

700 
qed 

701 

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

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

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

704 

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

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

708 
and [Pure.intro] = exI disjI2 disjI1 

12386  709 

710 
lemmas [trans] = trans 

711 
and [sym] = sym not_sym 

15801  712 
and [Pure.elim?] = iffD1 iffD2 impE 
11750  713 

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

714 

11750  715 
subsubsection {* Atomizing metalevel connectives *} 
716 

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

719 

11750  720 
lemma atomize_all [atomize]: "(!!x. P x) == Trueprop (ALL x. P x)" 
12003  721 
proof 
9488  722 
assume "!!x. P x" 
23389  723 
then show "ALL x. P x" .. 
9488  724 
next 
725 
assume "ALL x. P x" 

23553  726 
then show "!!x. P x" by (rule allE) 
9488  727 
qed 
728 

11750  729 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
12003  730 
proof 
9488  731 
assume r: "A ==> B" 
10383  732 
show "A > B" by (rule impI) (rule r) 
9488  733 
next 
734 
assume "A > B" and A 

23553  735 
then show B by (rule mp) 
9488  736 
qed 
737 

14749  738 
lemma atomize_not: "(A ==> False) == Trueprop (~A)" 
739 
proof 

740 
assume r: "A ==> False" 

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

742 
next 

743 
assume "~A" and A 

23553  744 
then show False by (rule notE) 
14749  745 
qed 
746 

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

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

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

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

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

755 

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

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

758 
assume conj: "A &&& B" 
19121  759 
show "A & B" 
760 
proof (rule conjI) 

761 
from conj show A by (rule conjunctionD1) 

762 
from conj show B by (rule conjunctionD2) 

763 
qed 

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

766 
show "A &&& B" 
19121  767 
proof  
768 
from conj show A .. 

769 
from conj show B .. 

11953  770 
qed 
771 
qed 

772 

12386  773 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
18832  774 
and [symmetric, defn] = atomize_all atomize_imp atomize_eq 
12386  775 

11750  776 

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

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

778 

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

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

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

781 

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

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

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

784 

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

785 
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

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

787 

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

788 
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

789 

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

790 

20944  791 
subsection {* Package setup *} 
792 

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

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

794 

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

795 

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

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

797 

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

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

799 
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

800 
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

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

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

803 

57963  804 
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

805 

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

806 

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

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

811 

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

813 
by (rule classical) iprover 

814 

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

817 

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

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

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

826 
val imp_intr = @{thm impI} 

827 
val rev_mp = @{thm rev_mp} 

828 
val subst = @{thm subst} 

829 
val sym = @{thm sym} 

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

42799  834 
structure Classical = Classical 
835 
( 

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

838 
val swap = @{thm swap} 

839 
val classical = @{thm classical} 

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

42799  842 
); 
21151  843 

58826  844 
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

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

846 
*} 
22129  847 

21009  848 
setup {* 
35389  849 
(*prevent substitution on bool*) 
58826  850 
let 
851 
fun non_bool_eq (@{const_name HOL.eq}, Type (_, [T, _])) = T <> @{typ bool} 

852 
 non_bool_eq _ = false; 

853 
fun hyp_subst_tac' ctxt = 

854 
SUBGOAL (fn (goal, i) => 

855 
if Term.exists_Const non_bool_eq goal 

856 
then Hypsubst.hyp_subst_tac ctxt i 

857 
else no_tac); 

858 
in 

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

860 
end 

21009  861 
*} 
862 

863 
declare iffI [intro!] 

864 
and notI [intro!] 

865 
and impI [intro!] 

866 
and disjCI [intro!] 

867 
and conjI [intro!] 

868 
and TrueI [intro!] 

869 
and refl [intro!] 

870 

871 
declare iffCE [elim!] 

872 
and FalseE [elim!] 

873 
and impCE [elim!] 

874 
and disjE [elim!] 

875 
and conjE [elim!] 

876 

877 
declare ex_ex1I [intro!] 

878 
and allI [intro!] 

879 
and the_equality [intro] 

880 
and exI [intro] 

881 

882 
declare exE [elim!] 

883 
allE [elim] 

884 

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

885 
ML {* val HOL_cs = claset_of @{context} *} 
19162  886 

20223  887 
lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P" 
888 
apply (erule swap) 

889 
apply (erule (1) meta_mp) 

890 
done 

10383  891 

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

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

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

894 

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

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

896 

12386  897 
lemmas [intro?] = ext 
898 
and [elim?] = ex1_implies_ex 

11977  899 

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

904 
shows R 

905 
apply (rule ex1E [OF major]) 

906 
apply (rule prem) 

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

909 
apply iprover 

910 
done 

20944  911 

21151  912 
ML {* 
42477  913 
structure Blast = Blast 
914 
( 

915 
structure Classical = Classical 

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

919 
val notE = @{thm notE} 

920 
val ccontr = @{thm ccontr} 

921 
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac 

922 
); 

923 
val blast_tac = Blast.blast_tac; 

20944  924 
*} 
925 

926 

927 
subsubsection {* Simplifier *} 

12281  928 

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

930 

931 
lemma simp_thms: 

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

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

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

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

936 
"(P  ~P) = True" "(~P  P) = True" 
12281  937 
"(x = x) = True" 
32068  938 
and not_True_eq_False [code]: "(\<not> True) = False" 
939 
and not_False_eq_True [code]: "(\<not> False) = True" 

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

941 
"(~P) ~= P" "P ~= (~P)" 
20944  942 
"(True=P) = P" 
943 
and eq_True: "(P = True) = P" 

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

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

946 
and 

12281  947 
"(True > P) = P" "(False > P) = True" 
948 
"(P > True) = True" "(P > P) = True" 

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

950 
"(P & True) = P" "(True & P) = P" 

951 
"(P & False) = False" "(False & P) = False" 

952 
"(P & P) = P" "(P & (P & Q)) = (P & Q)" 

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

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

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

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

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

958 
and 
12281  959 
"!!P. (EX x. x=t & P(x)) = P(t)" 
960 
"!!P. (EX x. t=x & P(x)) = P(t)" 

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

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

962 
"!!P. (ALL x. t=x > P(x)) = P(t)" 
17589  963 
by (blast, blast, blast, blast, blast, iprover+) 
13421  964 

14201  965 
lemma disj_absorb: "(A  A) = A" 
966 
by blast 

967 

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

969 
by blast 

970 

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

972 
by blast 

973 

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

975 
by blast 

976 

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

978 
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

979 
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

980 
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

981 
lemma neq_commute: "a \<noteq> b \<longleftrightarrow> b \<noteq> a" by iprover 
12281  982 

983 
lemma conj_comms: 

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

984 
shows conj_commute: "(P&Q) = (Q&P)" 
17589  985 
and conj_left_commute: "(P&(Q&R)) = (Q&(P&R))" by iprover+ 
986 
lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by iprover 

12281  987 

19174  988 
lemmas conj_ac = conj_commute conj_left_commute conj_assoc 
989 

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

991 
shows disj_commute: "(PQ) = (QP)" 
17589  992 
and disj_left_commute: "(P(QR)) = (Q(PR))" by iprover+ 
993 
lemma disj_assoc: "((PQ)R) = (P(QR))" by iprover 

12281  994 

19174  995 
lemmas disj_ac = disj_commute disj_left_commute disj_assoc 
996 

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

12281  999 

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

12281  1002 

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

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

12281  1006 

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

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

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

1010 

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

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

1013 

21151  1014 
lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P > Q) = (P' > Q'))" 
1015 
by iprover 

1016 

17589  1017 
lemma de_Morgan_disj: "(~(P  Q)) = (~P & ~Q)" by iprover 
12281  1018 
lemma de_Morgan_conj: "(~(P & Q)) = (~P  ~Q)" by blast 
1019 
lemma not_imp: "(~(P > Q)) = (P & ~Q)" by blast 

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

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

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

1023 
by blast 

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

1025 

17589  1026 
lemma iff_conv_conj_imp: "(P = Q) = ((P > Q) & (Q > P))" by iprover 
12281  1027 

1028 

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

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

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

1032 
by blast 

1033 

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

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

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

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

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

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

1041 

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

12281  1044 

1045 
text {* 

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

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

1048 

1049 
lemma conj_cong: 

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

17589  1051 
by iprover 
12281  1052 

1053 
lemma rev_conj_cong: 

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

17589  1055 
by iprover 
12281  1056 

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

1058 

1059 
lemma disj_cong: 

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

1061 
by blast 

1062 

1063 

1064 
text {* \medskip ifthenelse rules *} 

1065 

32068  1066 
lemma if_True [code]: "(if True then x else y) = x" 
38525  1067 
by (unfold If_def) blast 
12281  1068 

32068  1069 
lemma if_False [code]: "(if False then x else y) = y" 
38525  1070 
by (unfold If_def) blast 
12281  1071 

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

38525  1073 
by (unfold If_def) blast 
12281  1074 

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

38525  1076 
by (unfold If_def) blast 
12281  1077 

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

1079 
apply (rule case_split [of Q]) 

15481  1080 
apply (simplesubst if_P) 
1081 
prefer 3 apply (simplesubst if_not_P, blast+) 

12281  1082 
done 
1083 

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

15481  1085 
by (simplesubst split_if, blast) 
12281  1086 

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

1087 
lemmas if_splits [no_atp] = split_if split_if_asm 
12281  1088 

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

15481  1090 
by (simplesubst split_if, blast) 
12281  1091 

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

15481  1093 
by (simplesubst split_if, blast) 
12281  1094 

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

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

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

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

19796  1101 
 {* And this form is useful for expanding @{text "if"}s on the LEFT. *} 
15481  1102 
apply (simplesubst split_if, blast) 
12281  1103 
done 
1104 

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

12281  1107 

15423  1108 
text {* \medskip let rules for simproc *} 
1109 

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

1111 
by (unfold Let_def) 

1112 

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

1114 
by (unfold Let_def) 

1115 

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

1116 
text {* 
16999  1117 
The following copy of the implication operator is useful for 
1118 
finetuning congruence rules. It instructs the simplifier to simplify 

1119 
its premise. 

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

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

1121 

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

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

1124 

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

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

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

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

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

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

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

1132 

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

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

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

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

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

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

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

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

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

1142 

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

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

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

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

1146 
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

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

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

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

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

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

1153 
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

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

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

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

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

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

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

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

1162 

20944  1163 
lemma uncurry: 
1164 
assumes "P \<longrightarrow> Q \<longrightarrow> R" 

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

23553  1166 
using assms by blast 
20944  1167 

1168 
lemma iff_allI: 

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

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

23553  1171 
using assms by blast 
20944  1172 

1173 
lemma iff_exI: 

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

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

23553  1176 
using assms by blast 
20944  1177 

1178 
lemma all_comm: 

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

1180 
by blast 

1181 

1182 
lemma ex_comm: 

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

1184 
by blast 

1185 

48891  1186 
ML_file "Tools/simpdata.ML" 
21671  1187 
ML {* open Simpdata *} 
42455  1188 

58826  1189 
setup {* 
1190 
map_theory_simpset (put_simpset HOL_basic_ss) #> 

1191 
Simplifier.method_setup Splitter.split_modifiers 

1192 
*} 

42455  1193 

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

21671  1196 

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

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

1200 
let 

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

1202 
fun is_neq eq lhs rhs thm = 

1203 
(case Thm.prop_of thm of 

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

1205 
Not = HOLogic.Not andalso eq' = eq andalso 

1206 
r' aconv lhs andalso l' aconv rhs 

1207 
 _ => false); 

1208 
fun proc ss ct = 

1209 
(case Thm.term_of ct of 

1210 
eq $ lhs $ rhs => 

43597  1211 
(case find_first (is_neq eq lhs rhs) (Simplifier.prems_of ss) of 
24035  1212 
SOME thm => SOME (thm RS neq_to_EQ_False) 
1213 
 NONE => NONE) 

1214 
 _ => NONE); 

1215 
in proc end; 

1216 
*} 

1217 

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

1219 
let 

1220 
val (f_Let_unfold, x_Let_unfold) = 

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

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

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

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

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

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

1232 
 count_loose _ _ = 0; 

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

1234 
case t 

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

1236 
 _ => true; 

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

1237 
in fn _ => fn ctxt => fn ct => if is_trivial_let (Thm.term_of ct) 
31151  1238 
then SOME @{thm Let_def} (*no or one ocurrence of bound variable*) 
28741  1239 
else let (*Norbert Schirmer's case*) 
42361  1240 
val thy = Proof_Context.theory_of ctxt; 
28741  1241 
val t = Thm.term_of ct; 
1242 
val ([t'], ctxt') = Variable.import_terms false [t] ctxt; 

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

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

1245 
if is_Free x orelse is_Bound x orelse is_Const x 

1246 
then SOME @{thm Let_def} 

1247 
else 

1248 
let 

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

1250 
val cx = cterm_of thy x; 

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

1252 
val cf = cterm_of thy f; 

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

1253 
val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx); 
28741  1254 
val (_ $ _ $ g) = prop_of fx_g; 
1255 
val g' = abstract_over (x,g); 

51021
1cf4faed8b22
check alpha equality after applying beta and eta conversion in letsimproc, otherwise the simplifier may loop
hoelzl
parents:
50360
diff
changeset

1256 
val abs_g'= Abs (n,xT,g'); 
28741  1257 
in (if (g aconv g') 
1258 
then 

1259 
let 

1260 
val rl = 

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

1262 
in SOME (rl OF [fx_g]) end 

51021
1cf4faed8b22
check alpha equality after applying beta and eta conversion in letsimproc, otherwise the simplifier may loop
hoelzl
parents:
50360
diff
changeset

1263 
else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g') then NONE (*avoid identity conversion*) 
28741  1264 
else let 
1265 
val g'x = abs_g'$x; 

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

1269 
(g_Let_folded, cterm_of thy abs_g')] 

1270 
@{thm Let_folded}; 

36945  1271 
in SOME (rl OF [Thm.transitive fx_g g_g'x]) 
28741  1272 
end) 
1273 
end 

1274 
 _ => NONE) 

1275 
end 

1276 
end *} 

24035  1277 

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

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

21151  1282 
next 
1283 
assume "PROP P" 

23389  1284 
then show "PROP P" . 
21151  1285 
qed 
1286 

1287 
lemma ex_simps: 

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

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

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

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

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

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

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

1295 
by (iprover  blast)+ 

1296 

1297 
lemma all_simps: 

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

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

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

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

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

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

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

1305 
by (iprover  blast)+ 

15481  1306 

21671  1307 
lemmas [simp] = 
1308 
triv_forall_equality (*prunes params*) 

1309 
True_implies_equals (*prune asms `True'*) 

1310 
if_True 

1311 
if_False 

1312 
if_cancel 

1313 
if_eq_cancel 

1314 
imp_disjL 

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

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

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

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

21671  1320 
conj_assoc 
1321 
disj_assoc 

1322 
de_Morgan_conj 

1323 
de_Morgan_disj 

1324 
imp_disj1 

1325 
imp_disj2 

1326 
not_imp 

1327 
disj_not1 

1328 
not_all 

1329 
not_ex 

1330 
cases_simp 

1331 
the_eq_trivial 

1332 
the_sym_eq_trivial 

1333 
ex_simps 

1334 
all_simps 

1335 
simp_thms 

1336 

1337 
lemmas [cong] = imp_cong simp_implies_cong 

1338 
lemmas [split] = split_if 

20973  1339 

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

1340 
ML {* val HOL_ss = simpset_of @{context} *} 
20973  1341 

20944  1342 
text {* Simplifies x assuming c and y assuming ~c *} 
1343 
lemma if_cong: 

1344 
assumes "b = c" 

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

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

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

38525  1348 
using assms by simp 
20944  1349 

1350 
text {* Prevents simplification of x and y: 

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

1352 
lemma if_weak_cong [cong]: 

1353 
assumes "b = c" 

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

23553  1355 
using assms by (rule arg_cong) 
20944  1356 

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

1358 
lemma let_weak_cong: 