author  wenzelm 
Sun, 19 Jul 2015 00:03:10 +0200  
changeset 60759  36d9f215c982 
parent 60758  d8d85a8172b5 
child 60761  a443b08281e2 
permissions  rwrr 
923  1 
(* Title: HOL/HOL.thy 
11750  2 
Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson 
3 
*) 

923  4 

60758  5 
section \<open>The basis of HigherOrder Logic\<close> 
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 

60758  56 
subsection \<open>Primitive logic\<close> 
11750  57 

60758  58 
subsubsection \<open>Core syntax\<close> 
2260  59 

60758  60 
setup \<open>Axclass.class_axiomatization (@{binding type}, [])\<close> 
36452  61 
default_sort type 
60758  62 
setup \<open>Object_Logic.add_base_sort @{sort type}\<close> 
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 
60759  73 
Trueprop :: "bool \<Rightarrow> prop" ("(_)" 5) 
923  74 

46973  75 
axiomatization 
60759  76 
implies :: "[bool, bool] \<Rightarrow> bool" (infixr ">" 25) and 
77 
eq :: "['a, 'a] \<Rightarrow> bool" (infixl "=" 50) and 

78 
The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" 

46973  79 

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

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

84 

60759  85 
conj :: "[bool, bool] \<Rightarrow> bool" (infixr "&" 35) 
86 
disj :: "[bool, bool] \<Rightarrow> bool" (infixr "" 30) 

38555  87 

60759  88 
All :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "ALL " 10) 
89 
Ex :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "EX " 10) 

90 
Ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "EX! " 10) 

923  91 

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

92 

60758  93 
subsubsection \<open>Additional concrete syntax\<close> 
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 
60759  99 
not_equal :: "['a, 'a] \<Rightarrow> bool" (infixl "~=" 50) where 
100 
"x ~= y \<equiv> ~ (x = y)" 

19656
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) 
60759  122 
iff :: "[bool, bool] \<Rightarrow> bool" (infixr "<>" 25) where 
123 
"A <> B \<equiv> A = B" 

19656
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 

60759  128 
syntax "_The" :: "[pttrn, bool] \<Rightarrow> 'a" ("(3THE _./ _)" [0, 10] 10) 
129 
translations "THE x. P" \<rightleftharpoons> "CONST The (\<lambda>x. P)" 

60758  130 
print_translation \<open> 
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)] 
60758  134 
\<close>  \<open>To avoid etacontraction of body\<close> 
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 
60759  138 
"_bind" :: "[pttrn, 'a] \<Rightarrow> letbind" ("(2_ =/ _)" 10) 
139 
"" :: "letbind \<Rightarrow> letbinds" ("_") 

140 
"_binds" :: "[letbind, letbinds] \<Rightarrow> letbinds" ("_;/ _") 

141 
"_Let" :: "[letbinds, 'a] \<Rightarrow> '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 
60759  145 
"_case_syntax" :: "['a, cases_syn] \<Rightarrow> 'b" ("(case _ of/ _)" 10) 
146 
"_case1" :: "['a, 'b] \<Rightarrow> case_syn" ("(2_ =>/ _)" 10) 

147 
"" :: "case_syn \<Rightarrow> cases_syn" ("_") 

148 
"_case2" :: "[case_syn, cases_syn] \<Rightarrow> 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) 
60759  150 
"_case1" :: "['a, 'b] \<Rightarrow> 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 

60758  168 
subsubsection \<open>Axioms and basic definitions\<close> 
2260  169 

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

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

60759  173 
ext: "(\<And>x::'a. (f x ::'b) = g x) \<Longrightarrow> (\<lambda>x. f x) = (\<lambda>x. g x)" 
60758  174 
 \<open>Extensionality is built into the metalogic, and this rule expresses 
15380  175 
a related property. It is an etaexpanded version of the traditional 
60758  176 
rule, and similar to the ABS rule of HOL\<close> 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 
60759  181 
impI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<longrightarrow> Q" and 
182 
mp: "\<lbrakk>P \<longrightarrow> Q; P\<rbrakk> \<Longrightarrow> Q" and 

15380  183 

60759  184 
iff: "(P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P) \<longrightarrow> (P = Q)" and 
185 
True_or_False: "(P = True) \<or> (P = False)" 

15380  186 

923  187 
defs 
60759  188 
True_def: "True \<equiv> ((\<lambda>x::bool. x) = (\<lambda>x. x))" 
189 
All_def: "All P \<equiv> (P = (\<lambda>x. True))" 

190 
Ex_def: "Ex P \<equiv> \<forall>Q. (\<forall>x. P x \<longrightarrow> Q) \<longrightarrow> Q" 

191 
False_def: "False \<equiv> (\<forall>P. P)" 

192 
not_def: "\<not> P \<equiv> P \<longrightarrow> False" 

193 
and_def: "P \<and> Q \<equiv> \<forall>R. (P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> R" 

194 
or_def: "P \<or> Q \<equiv> \<forall>R. (P \<longrightarrow> R) \<longrightarrow> (Q \<longrightarrow> R) \<longrightarrow> R" 

195 
Ex1_def: "Ex1 P \<equiv> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x)" 

923  196 

46973  197 
definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10) 
60759  198 
where "If P x y \<equiv> (THE z::'a. (P = True \<longrightarrow> z = x) \<and> (P = False \<longrightarrow> 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 

60759  204 
"_Let (_binds b bs) e" \<rightleftharpoons> "_Let b (_Let bs e)" 
205 
"let x = a in e" \<rightleftharpoons> "CONST Let a (\<lambda>x. e)" 

38525  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 

60758  212 
subsection \<open>Fundamental rules\<close> 
20944  213 

60758  214 
subsubsection \<open>Equality\<close> 
20944  215 

60759  216 
lemma sym: "s = t \<Longrightarrow> t = s" 
18457  217 
by (erule subst) (rule refl) 
15411  218 

60759  219 
lemma ssubst: "t = s \<Longrightarrow> P s \<Longrightarrow> P t" 
18457  220 
by (drule sym) (erule subst) 
15411  221 

60759  222 
lemma trans: "\<lbrakk>r = s; s = t\<rbrakk> \<Longrightarrow> r = t" 
18457  223 
by (erule subst) 
15411  224 

60759  225 
lemma trans_sym [Pure.elim?]: "r = s \<Longrightarrow> t = s \<Longrightarrow> r = t" 
40715
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: 
60759  229 
assumes meq: "A \<equiv> B" 
20944  230 
shows "A = B" 
231 
by (unfold meq) (rule refl) 

15411  232 

60758  233 
text \<open>Useful with @{text erule} for proving equalities from known equalities.\<close> 
20944  234 
(* a = b 
15411  235 
  
236 
c = d *) 

60759  237 
lemma box_equals: "\<lbrakk>a = b; a = c; b = d\<rbrakk> \<Longrightarrow> c = d" 
15411  238 
apply (rule trans) 
239 
apply (rule trans) 

240 
apply (rule sym) 

241 
apply assumption+ 

242 
done 

243 

60758  244 
text \<open>For calculational reasoning:\<close> 
15524
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15481
diff
changeset

245 

60759  246 
lemma forw_subst: "a = b \<Longrightarrow> P b \<Longrightarrow> P a" 
15524
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 

60759  249 
lemma back_subst: "P a \<Longrightarrow> a = b \<Longrightarrow> P b" 
15524
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 

60758  253 
subsubsection \<open>Congruence rules for application\<close> 
15411  254 

60758  255 
text \<open>Similar to @{text AP_THM} in Gordon's HOL.\<close> 
60759  256 
lemma fun_cong: "(f :: 'a \<Rightarrow> 'b) = g \<Longrightarrow> f x = g x" 
15411  257 
apply (erule subst) 
258 
apply (rule refl) 

259 
done 

260 

60758  261 
text \<open>Similar to @{text AP_TERM} in Gordon's HOL and FOL's @{text subst_context}.\<close> 
60759  262 
lemma arg_cong: "x = y \<Longrightarrow> f x = f y" 
15411  263 
apply (erule subst) 
264 
apply (rule refl) 

265 
done 

266 

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

270 
done 

271 

60759  272 
lemma cong: "\<lbrakk>f = g; (x::'a) = y\<rbrakk> \<Longrightarrow> f x = g y" 
15411  273 
apply (erule subst)+ 
274 
apply (rule refl) 

275 
done 

276 

60758  277 
ML \<open>fun cong_tac ctxt = Cong_Tac.cong_tac ctxt @{thm cong}\<close> 
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 

60758  280 
subsubsection \<open>Equality of booleans  iff\<close> 
15411  281 

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

60759  285 
lemma iffD2: "\<lbrakk>P = Q; Q\<rbrakk> \<Longrightarrow> P" 
18457  286 
by (erule ssubst) 
15411  287 

60759  288 
lemma rev_iffD2: "\<lbrakk>Q; P = Q\<rbrakk> \<Longrightarrow> 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: 

60759  298 
assumes major: "P = Q" 
299 
and minor: "\<lbrakk>P \<longrightarrow> Q; Q \<longrightarrow> P\<rbrakk> \<Longrightarrow> R" 

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

15411  302 

303 

60758  304 
subsubsection \<open>True\<close> 
15411  305 

306 
lemma TrueI: "True" 

21504  307 
unfolding True_def by (rule refl) 
15411  308 

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

60759  312 
lemma eqTrueE: "P = True \<Longrightarrow> P" 
21504  313 
by (erule iffD2) (rule TrueI) 
15411  314 

315 

60758  316 
subsubsection \<open>Universal quantifier\<close> 
15411  317 

60759  318 
lemma allI: assumes "\<And>x::'a. P x" shows "\<forall>x. P x" 
21504  319 
unfolding All_def by (iprover intro: ext eqTrueI assms) 
15411  320 

60759  321 
lemma spec: "\<forall>x::'a. P x \<Longrightarrow> P x" 
15411  322 
apply (unfold All_def) 
323 
apply (rule eqTrueE) 

324 
apply (erule fun_cong) 

325 
done 

326 

327 
lemma allE: 

60759  328 
assumes major: "\<forall>x. P x" 
329 
and minor: "P x \<Longrightarrow> R" 

21504  330 
shows R 
331 
by (iprover intro: minor major [THEN spec]) 

15411  332 

333 
lemma all_dupE: 

60759  334 
assumes major: "\<forall>x. P x" 
335 
and minor: "\<lbrakk>P x; \<forall>x. P x\<rbrakk> \<Longrightarrow> R" 

21504  336 
shows R 
337 
by (iprover intro: minor major major [THEN spec]) 

15411  338 

339 

60758  340 
subsubsection \<open>False\<close> 
21504  341 

60758  342 
text \<open> 
21504  343 
Depends upon @{text spec}; it is impossible to do propositional 
344 
logic before quantifiers! 

60758  345 
\<close> 
15411  346 

60759  347 
lemma FalseE: "False \<Longrightarrow> P" 
21504  348 
apply (unfold False_def) 
349 
apply (erule spec) 

350 
done 

15411  351 

60759  352 
lemma False_neq_True: "False = True \<Longrightarrow> P" 
21504  353 
by (erule eqTrueE [THEN FalseE]) 
15411  354 

355 

60758  356 
subsubsection \<open>Negation\<close> 
15411  357 

358 
lemma notI: 

60759  359 
assumes "P \<Longrightarrow> False" 
360 
shows "\<not> P" 

21504  361 
apply (unfold not_def) 
362 
apply (iprover intro: impI assms) 

363 
done 

15411  364 

60759  365 
lemma False_not_True: "False \<noteq> True" 
21504  366 
apply (rule notI) 
367 
apply (erule False_neq_True) 

368 
done 

15411  369 

60759  370 
lemma True_not_False: "True \<noteq> False" 
21504  371 
apply (rule notI) 
372 
apply (drule sym) 

373 
apply (erule False_neq_True) 

374 
done 

15411  375 

60759  376 
lemma notE: "\<lbrakk>\<not> P; P\<rbrakk> \<Longrightarrow> 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 

60758  386 
subsubsection \<open>Implication\<close> 
15411  387 

388 
lemma impE: 

60759  389 
assumes "P \<longrightarrow> Q" P "Q \<Longrightarrow> R" 
390 
shows R 

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

60759  393 
(* Reduces Q to P \<longrightarrow> Q, allowing substitution in P. *) 
394 
lemma rev_mp: "\<lbrakk>P; P \<longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" 

17589  395 
by (iprover intro: mp) 
15411  396 

397 
lemma contrapos_nn: 

60759  398 
assumes major: "\<not> Q" 
399 
and minor: "P \<Longrightarrow> Q" 

400 
shows "\<not> 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" 

60759  406 
and minor: "P \<Longrightarrow> \<not> Q" 
407 
shows "\<not> P" 

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

60759  410 
lemma not_sym: "t \<noteq> s \<Longrightarrow> s \<noteq> t" 
21250  411 
by (erule contrapos_nn) (erule sym) 
412 

60759  413 
lemma eq_neq_eq_imp_neq: "\<lbrakk>x = a; a \<noteq> b; b = y\<rbrakk> \<Longrightarrow> x \<noteq> y" 
21250  414 
by (erule subst, erule ssubst, assumption) 
15411  415 

416 

60758  417 
subsubsection \<open>Existential quantifier\<close> 
15411  418 

60759  419 
lemma exI: "P x \<Longrightarrow> \<exists>x::'a. P x" 
15411  420 
apply (unfold Ex_def) 
17589  421 
apply (iprover intro: allI allE impI mp) 
15411  422 
done 
423 

424 
lemma exE: 

60759  425 
assumes major: "\<exists>x::'a. P x" 
426 
and minor: "\<And>x. P x \<Longrightarrow> Q" 

15411  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 

60758  433 
subsubsection \<open>Conjunction\<close> 
15411  434 

60759  435 
lemma conjI: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q" 
15411  436 
apply (unfold and_def) 
17589  437 
apply (iprover intro: impI [THEN allI] mp) 
15411  438 
done 
439 

60759  440 
lemma conjunct1: "\<lbrakk>P \<and> Q\<rbrakk> \<Longrightarrow> P" 
15411  441 
apply (unfold and_def) 
17589  442 
apply (iprover intro: impI dest: spec mp) 
15411  443 
done 
444 

60759  445 
lemma conjunct2: "\<lbrakk>P \<and> Q\<rbrakk> \<Longrightarrow> Q" 
15411  446 
apply (unfold and_def) 
17589  447 
apply (iprover intro: impI dest: spec mp) 
15411  448 
done 
449 

450 
lemma conjE: 

60759  451 
assumes major: "P \<and> Q" 
452 
and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R" 

453 
shows R 

15411  454 
apply (rule minor) 
455 
apply (rule major [THEN conjunct1]) 

456 
apply (rule major [THEN conjunct2]) 

457 
done 

458 

459 
lemma context_conjI: 

60759  460 
assumes P "P \<Longrightarrow> Q" shows "P \<and> Q" 
23553  461 
by (iprover intro: conjI assms) 
15411  462 

463 

60758  464 
subsubsection \<open>Disjunction\<close> 
15411  465 

60759  466 
lemma disjI1: "P \<Longrightarrow> P \<or> Q" 
15411  467 
apply (unfold or_def) 
17589  468 
apply (iprover intro: allI impI mp) 
15411  469 
done 
470 

60759  471 
lemma disjI2: "Q \<Longrightarrow> P \<or> Q" 
15411  472 
apply (unfold or_def) 
17589  473 
apply (iprover intro: allI impI mp) 
15411  474 
done 
475 

476 
lemma disjE: 

60759  477 
assumes major: "P \<or> Q" 
478 
and minorP: "P \<Longrightarrow> R" 

479 
and minorQ: "Q \<Longrightarrow> 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 

60758  485 
subsubsection \<open>Classical logic\<close> 
15411  486 

487 
lemma classical: 

60759  488 
assumes prem: "\<not> P \<Longrightarrow> P" 
489 
shows P 

15411  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 

60759  499 
(*notE with premises exchanged; it discharges \<not> R so that it can be used to 
15411  500 
make elimination rules*) 
501 
lemma rev_notE: 

60759  502 
assumes premp: P 
503 
and premnot: "\<not> R \<Longrightarrow> \<not> P" 

504 
shows R 

15411  505 
apply (rule ccontr) 
506 
apply (erule notE [OF premnot premp]) 

507 
done 

508 

509 
(*Double negation law*) 

60759  510 
lemma notnotD: "\<not>\<not> P \<Longrightarrow> P" 
15411  511 
apply (rule classical) 
512 
apply (erule notE) 

513 
apply assumption 

514 
done 

515 

516 
lemma contrapos_pp: 

60759  517 
assumes p1: Q 
518 
and p2: "\<not> P \<Longrightarrow> \<not> Q" 

519 
shows P 

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

522 

60758  523 
subsubsection \<open>Unique existence\<close> 
15411  524 

525 
lemma ex1I: 

60759  526 
assumes "P a" "\<And>x. P x \<Longrightarrow> x = a" 
527 
shows "\<exists>!x. P x" 

23553  528 
by (unfold Ex1_def, iprover intro: assms exI conjI allI impI) 
15411  529 

60758  530 
text\<open>Sometimes easier to use: the premises have no shared variables. Safe!\<close> 
15411  531 
lemma ex_ex1I: 
60759  532 
assumes ex_prem: "\<exists>x. P x" 
533 
and eq: "\<And>x y. \<lbrakk>P x; P y\<rbrakk> \<Longrightarrow> x = y" 

534 
shows "\<exists>!x. P x" 

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

537 
lemma ex1E: 

60759  538 
assumes major: "\<exists>!x. P x" 
539 
and minor: "\<And>x. \<lbrakk>P x; \<forall>y. P y \<longrightarrow> y = x\<rbrakk> \<Longrightarrow> R" 

540 
shows R 

15411  541 
apply (rule major [unfolded Ex1_def, THEN exE]) 
542 
apply (erule conjE) 

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

60759  546 
lemma ex1_implies_ex: "\<exists>!x. P x \<Longrightarrow> \<exists>x. P x" 
15411  547 
apply (erule ex1E) 
548 
apply (rule exI) 

549 
apply assumption 

550 
done 

551 

552 

60758  553 
subsubsection \<open>Classical intro rules for disjunction and existential quantifiers\<close> 
15411  554 

555 
lemma disjCI: 

60759  556 
assumes "\<not> Q \<Longrightarrow> P" shows "P \<or> Q" 
15411  557 
apply (rule classical) 
23553  558 
apply (iprover intro: assms disjI1 disjI2 notI elim: notE) 
15411  559 
done 
560 

60759  561 
lemma excluded_middle: "\<not> P \<or> P" 
17589  562 
by (iprover intro: disjCI) 
15411  563 

60758  564 
text \<open> 
20944  565 
case distinction as a natural deduction rule. 
60759  566 
Note that @{term "\<not> P"} is the second case, not the first 
60758  567 
\<close> 
27126
3ede9103de8e
eliminated obsolete case_split_thm  use case_split;
wenzelm
parents:
27107
diff
changeset

568 
lemma case_split [case_names True False]: 
60759  569 
assumes prem1: "P \<Longrightarrow> Q" 
570 
and prem2: "\<not> P \<Longrightarrow> Q" 

571 
shows Q 

15411  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 

60759  577 
(*Classical implies (\<longrightarrow>) elimination. *) 
15411  578 
lemma impCE: 
60759  579 
assumes major: "P \<longrightarrow> Q" 
580 
and minor: "\<not> P \<Longrightarrow> R" "Q \<Longrightarrow> R" 

581 
shows R 

15411  582 
apply (rule excluded_middle [of P, THEN disjE]) 
17589  583 
apply (iprover intro: minor major [THEN mp])+ 
15411  584 
done 
585 

60759  586 
(*This version of \<longrightarrow> elimination works on Q before P. It works best for 
15411  587 
those cases in which P holds "almost everywhere". Can't install as 
588 
default: would break old proofs.*) 

589 
lemma impCE': 

60759  590 
assumes major: "P \<longrightarrow> Q" 
591 
and minor: "Q \<Longrightarrow> R" "\<not> P \<Longrightarrow> R" 

592 
shows R 

15411  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: 

60759  599 
assumes major: "P = Q" 
600 
and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R" "\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> R" 

601 
shows R 

15411  602 
apply (rule major [THEN iffE]) 
17589  603 
apply (iprover intro: minor elim: impCE notE) 
15411  604 
done 
605 

606 
lemma exCI: 

60759  607 
assumes "\<forall>x. \<not> P x \<Longrightarrow> P a" 
608 
shows "\<exists>x. P x" 

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

613 

60758  614 
subsubsection \<open>Intuitionistic Reasoning\<close> 
12386  615 

616 
lemma impE': 

60759  617 
assumes 1: "P \<longrightarrow> Q" 
618 
and 2: "Q \<Longrightarrow> R" 

619 
and 3: "P \<longrightarrow> Q \<Longrightarrow> P" 

12937
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': 

60759  628 
assumes 1: "\<forall>x. P x" 
629 
and 2: "P x \<Longrightarrow> \<forall>x. P x \<Longrightarrow> Q" 

12937
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': 
60759  637 
assumes 1: "\<not> P" 
638 
and 2: "\<not> P \<Longrightarrow> P" 

12937
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 

60759  645 
lemma TrueE: "True \<Longrightarrow> P \<Longrightarrow> P" . 
646 
lemma notFalseE: "\<not> False \<Longrightarrow> P \<Longrightarrow> P" . 

22444
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 

60758  658 
subsubsection \<open>Atomizing metalevel connectives\<close> 
11750  659 

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

662 

60759  663 
lemma atomize_all [atomize]: "(\<And>x. P x) \<equiv> Trueprop (\<forall>x. P x)" 
12003  664 
proof 
60759  665 
assume "\<And>x. P x" 
666 
then show "\<forall>x. P x" .. 

9488  667 
next 
60759  668 
assume "\<forall>x. P x" 
669 
then show "\<And>x. P x" by (rule allE) 

9488  670 
qed 
671 

60759  672 
lemma atomize_imp [atomize]: "(A \<Longrightarrow> B) \<equiv> Trueprop (A \<longrightarrow> B)" 
12003  673 
proof 
60759  674 
assume r: "A \<Longrightarrow> B" 
675 
show "A \<longrightarrow> B" by (rule impI) (rule r) 

9488  676 
next 
60759  677 
assume "A \<longrightarrow> B" and A 
23553  678 
then show B by (rule mp) 
9488  679 
qed 
680 

60759  681 
lemma atomize_not: "(A \<Longrightarrow> False) \<equiv> Trueprop (\<not> A)" 
14749  682 
proof 
60759  683 
assume r: "A \<Longrightarrow> False" 
684 
show "\<not> A" by (rule notI) (rule r) 

14749  685 
next 
60759  686 
assume "\<not> A" and A 
23553  687 
then show False by (rule notE) 
14749  688 
qed 
689 

60759  690 
lemma atomize_eq [atomize, code]: "(x \<equiv> y) \<equiv> Trueprop (x = y)" 
12003  691 
proof 
60759  692 
assume "x \<equiv> y" 
693 
show "x = y" by (unfold \<open>x \<equiv> y\<close>) (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" 
60759  696 
then show "x \<equiv> 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 

60759  699 
lemma atomize_conj [atomize]: "(A &&& B) \<equiv> Trueprop (A \<and> 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" 
60759  702 
show "A \<and> B" 
19121  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 
60759  708 
assume conj: "A \<and> 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 

60758  720 
subsubsection \<open>Atomizing elimination rules\<close> 
26580
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26555
diff
changeset

721 

60759  722 
lemma atomize_exL[atomize_elim]: "(\<And>x. P x \<Longrightarrow> Q) \<equiv> ((\<exists>x. P x) \<Longrightarrow> Q)" 
26580
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 

60759  725 
lemma atomize_conjL[atomize_elim]: "(A \<Longrightarrow> B \<Longrightarrow> C) \<equiv> (A \<and> B \<Longrightarrow> C)" 
26580
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 

60759  728 
lemma atomize_disjL[atomize_elim]: "((A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C) \<equiv> ((A \<or> B \<Longrightarrow> C) \<Longrightarrow> C)" 
26580
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 

60759  731 
lemma atomize_elimL[atomize_elim]: "(\<And>B. (A \<Longrightarrow> B) \<Longrightarrow> B) \<equiv> Trueprop A" .. 
26580
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 

60758  734 
subsection \<open>Package setup\<close> 
20944  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 

60758  739 
subsubsection \<open>Sledgehammer setup\<close> 
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35808
diff
changeset

740 

60758  741 
text \<open> 
35828
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. 
60758  745 
\<close> 
35828
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 

60758  750 
subsubsection \<open>Classical Reasoner setup\<close> 
9529  751 

60759  752 
lemma imp_elim: "P \<longrightarrow> Q \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R" 
26411  753 
by (rule classical) iprover 
754 

60759  755 
lemma swap: "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R" 
26411  756 
by (rule classical) iprover 
757 

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

60758  760 
ML \<open> 
42799  761 
structure Hypsubst = Hypsubst 
762 
( 

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

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

768 
val imp_intr = @{thm impI} 

769 
val rev_mp = @{thm rev_mp} 

770 
val subst = @{thm subst} 

771 
val sym = @{thm sym} 

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

42799  776 
structure Classical = Classical 
777 
( 

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

780 
val swap = @{thm swap} 

781 
val classical = @{thm classical} 

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

42799  784 
); 
21151  785 

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

787 
open Basic_Classical; 
60758  788 
\<close> 
22129  789 

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

794 
 non_bool_eq _ = false; 

795 
fun hyp_subst_tac' ctxt = 

796 
SUBGOAL (fn (goal, i) => 

797 
if Term.exists_Const non_bool_eq goal 

798 
then Hypsubst.hyp_subst_tac ctxt i 

799 
else no_tac); 

800 
in 

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

802 
end 

60758  803 
\<close> 
21009  804 

805 
declare iffI [intro!] 

806 
and notI [intro!] 

807 
and impI [intro!] 

808 
and disjCI [intro!] 

809 
and conjI [intro!] 

810 
and TrueI [intro!] 

811 
and refl [intro!] 

812 

813 
declare iffCE [elim!] 

814 
and FalseE [elim!] 

815 
and impCE [elim!] 

816 
and disjE [elim!] 

817 
and conjE [elim!] 

818 

819 
declare ex_ex1I [intro!] 

820 
and allI [intro!] 

821 
and exI [intro] 

822 

823 
declare exE [elim!] 

824 
allE [elim] 

825 

60758  826 
ML \<open>val HOL_cs = claset_of @{context}\<close> 
19162  827 

60759  828 
lemma contrapos_np: "\<not> Q \<Longrightarrow> (\<not> P \<Longrightarrow> Q) \<Longrightarrow> P" 
20223  829 
apply (erule swap) 
830 
apply (erule (1) meta_mp) 

831 
done 

10383  832 

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

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

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

835 

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

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

837 

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

11977  840 

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

845 
shows R 

846 
apply (rule ex1E [OF major]) 

847 
apply (rule prem) 

59499  848 
apply assumption 
849 
apply (rule allI)+ 

60758  850 
apply (tactic \<open>eresolve_tac @{context} [Classical.dup_elim @{context} @{thm allE}] 1\<close>) 
22129  851 
apply iprover 
852 
done 

20944  853 

60758  854 
ML \<open> 
42477  855 
structure Blast = Blast 
856 
( 

857 
structure Classical = Classical 

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

861 
val notE = @{thm notE} 

862 
val ccontr = @{thm ccontr} 

863 
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac 

864 
); 

865 
val blast_tac = Blast.blast_tac; 

60758  866 
\<close> 
20944  867 

868 

60758  869 
subsubsection \<open>THE: definite description operator\<close> 
59504
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

870 

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

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

872 
assumes "P a" 
60759  873 
and "\<And>x. P x \<Longrightarrow> x = a" 
59504
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

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

875 
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

876 

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

877 
lemma theI: 
60759  878 
assumes "P a" and "\<And>x. P x \<Longrightarrow> x = a" 
59504
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

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

880 
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

881 

60759  882 
lemma theI': "\<exists>!x. P x \<Longrightarrow> P (THE x. P x)" 
59504
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

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

884 

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

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

886 
lemma theI2: 
60759  887 
assumes "P a" "\<And>x. P x \<Longrightarrow> x = a" "\<And>x. P x \<Longrightarrow> Q x" 
59504
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

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

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

890 

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

892 
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

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

894 

60759  895 
lemma the1_equality [elim?]: "\<lbrakk>\<exists>!x. P x; P a\<rbrakk> \<Longrightarrow> (THE x. P x) = a" 
59504
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

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

897 

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

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

900 

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

901 

60758  902 
subsubsection \<open>Simplifier\<close> 
12281  903 

60759  904 
lemma eta_contract_eq: "(\<lambda>s. f s) = f" .. 
12281  905 

906 
lemma simp_thms: 

60759  907 
shows not_not: "(\<not> \<not> P) = P" 
908 
and Not_eq_iff: "((\<not> P) = (\<not> Q)) = (P = Q)" 

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

909 
and 
60759  910 
"(P \<noteq> Q) = (P = (\<not> Q))" 
911 
"(P \<or> \<not>P) = True" "(\<not> P \<or> P) = True" 

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

20944  915 
and 
60759  916 
"(\<not> P) \<noteq> P" "P \<noteq> (\<not> P)" 
917 
"(True = P) = P" 

20944  918 
and eq_True: "(P = True) = P" 
60759  919 
and "(False = P) = (\<not> P)" 
20944  920 
and eq_False: "(P = False) = (\<not> P)" 
921 
and 

60759  922 
"(True \<longrightarrow> P) = P" "(False \<longrightarrow> P) = True" 
923 
"(P \<longrightarrow> True) = True" "(P \<longrightarrow> P) = True" 

924 
"(P \<longrightarrow> False) = (\<not> P)" "(P \<longrightarrow> \<not> P) = (\<not> P)" 

925 
"(P \<and> True) = P" "(True \<and> P) = P" 

926 
"(P \<and> False) = False" "(False \<and> P) = False" 

927 
"(P \<and> P) = P" "(P \<and> (P \<and> Q)) = (P \<and> Q)" 

928 
"(P \<and> \<not> P) = False" "(\<not> P \<and> P) = False" 

929 
"(P \<or> True) = True" "(True \<or> P) = True" 

930 
"(P \<or> False) = P" "(False \<or> P) = P" 

931 
"(P \<or> P) = P" "(P \<or> (P \<or> Q)) = (P \<or> Q)" and 

932 
"(\<forall>x. P) = P" "(\<exists>x. P) = P" "\<exists>x. x = t" "\<exists>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

933 
and 
60759  934 
"\<And>P. (\<exists>x. x = t \<and> P x) = P t" 
935 
"\<And>P. (\<exists>x. t = x \<and> P x) = P t" 

936 
"\<And>P. (\<forall>x. x = t \<longrightarrow> P x) = P t" 

937 
"\<And>P. (\<forall>x. t = x \<longrightarrow> P x) = P t" 

17589  938 
by (blast, blast, blast, blast, blast, iprover+) 
13421  939 

60759  940 
lemma disj_absorb: "(A \<or> A) = A" 
14201  941 
by blast 
942 

60759  943 
lemma disj_left_absorb: "(A \<or> (A \<or> B)) = (A \<or> B)" 
14201  944 
by blast 
945 

60759  946 
lemma conj_absorb: "(A \<and> A) = A" 
14201  947 
by blast 
948 

60759  949 
lemma conj_left_absorb: "(A \<and> (A \<and> B)) = (A \<and> B)" 
14201  950 
by blast 
951 

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

953 
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

954 
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

955 
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

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

958 
lemma conj_comms: 

60759  959 
shows conj_commute: "(P \<and> Q) = (Q \<and> P)" 
960 
and conj_left_commute: "(P \<and> (Q \<and> R)) = (Q \<and> (P \<and> R))" by iprover+ 

961 
lemma conj_assoc: "((P \<and> Q) \<and> R) = (P \<and> (Q \<and> R))" by iprover 

12281  962 

19174  963 
lemmas conj_ac = conj_commute conj_left_commute conj_assoc 
964 

12281  965 
lemma disj_comms: 
60759  966 
shows disj_commute: "(P \<or> Q) = (Q \<or> P)" 
967 
and disj_left_commute: "(P \<or> (Q \<or> R)) = (Q \<or> (P \<or> R))" by iprover+ 

968 
lemma disj_assoc: "((P \<or> Q) \<or> R) = (P \<or> (Q \<or> R))" by iprover 

12281  969 

19174  970 
lemmas disj_ac = disj_commute disj_left_commute disj_assoc 
971 

60759  972 
lemma conj_disj_distribL: "(P \<and> (Q \<or> R)) = (P \<and> Q \<or> P \<and> R)" by iprover 
973 
lemma conj_disj_distribR: "((P \<or> Q) \<and> R) = (P \<and> R \<or> Q \<and> R)" by iprover 

12281  974 

60759  975 
lemma disj_conj_distribL: "(P \<or> (Q \<and> R)) = ((P \<or> Q) \<and> (P \<or> R))" by iprover 
976 
lemma disj_conj_distribR: "((P \<and> Q) \<or> R) = ((P \<or> R) \<and> (Q \<or> R))" by iprover 

12281  977 

60759  978 
lemma imp_conjR: "(P \<longrightarrow> (Q \<and> R)) = ((P \<longrightarrow> Q) \<and> (P \<longrightarrow> R))" by iprover 
979 
lemma imp_conjL: "((P \<and> Q) \<longrightarrow> R) = (P \<longrightarrow> (Q \<longrightarrow> R))" by iprover 

980 
lemma imp_disjL: "((P \<or> Q) \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))" by iprover 

12281  981 

60758  982 
text \<open>These two are specialized, but @{text imp_disj_not1} is useful in @{text "Auth/Yahalom"}.\<close> 
60759  983 
lemma imp_disj_not1: "(P \<longrightarrow> Q \<or> R) = (\<not> Q \<longrightarrow> P \<longrightarrow> R)" by blast 
984 
lemma imp_disj_not2: "(P \<longrightarrow> Q \<or> R) = (\<not> R \<longrightarrow> P \<longrightarrow> Q)" by blast 

12281  985 

60759  986 
lemma imp_disj1: "((P \<longrightarrow> Q) \<or> R) = (P \<longrightarrow> Q \<or> R)" by blast 
987 
lemma imp_disj2: "(Q \<or> (P \<longrightarrow> R)) = (P \<longrightarrow> Q \<or> R)" by blast 

12281  988 

60759  989 
lemma imp_cong: "(P = P') \<Longrightarrow> (P' \<Longrightarrow> (Q = Q')) \<Longrightarrow> ((P \<longrightarrow> Q) = (P' \<longrightarrow> Q'))" 
21151  990 
by iprover 
991 

60759  992 
lemma de_Morgan_disj: "(\<not> (P \<or> Q)) = (\<not> P \<and> \<not> Q)" by iprover 
993 
lemma de_Morgan_conj: "(\<not> (P \<and> Q)) = (\<not> P \<or> \<not> Q)" by blast 

994 
lemma not_imp: "(\<not> (P \<longrightarrow> Q)) = (P \<and> \<not> Q)" by blast 

995 
lemma not_iff: "(P \<noteq> Q) = (P = (\<not> Q))" by blast 

996 
lemma disj_not1: "(\<not> P \<or> Q) = (P \<longrightarrow> Q)" by blast 

997 
lemma disj_not2: "(P \<or> \<not> Q) = (Q \<longrightarrow> P)"  \<open>changes orientation :(\<close> 

12281  998 
by blast 
60759  999 
lemma imp_conv_disj: "(P \<longrightarrow> Q) = ((\<not> P) \<or> Q)" by blast 
12281  1000 

60759  1001 
lemma iff_conv_conj_imp: "(P = Q) = ((P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P))" by iprover 
12281  1002 

1003 

60759  1004 
lemma cases_simp: "((P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q)) = Q" 
60758  1005 
 \<open>Avoids duplication of subgoals after @{text split_if}, when the true and false\<close> 
1006 
 \<open>cases boil down to the same thing.\<close> 

12281  1007 
by blast 
1008 

60759  1009 
lemma not_all: "(\<not> (\<forall>x. P x)) = (\<exists>x. \<not> P x)" by blast 
1010 
lemma imp_all: "((\<forall>x. P x) \<longrightarrow> Q) = (\<exists>x. P x \<longrightarrow> Q)" by blast 

1011 
lemma not_ex: "(\<not> (\<exists>x. P x)) = (\<forall>x. \<not> P x)" by iprover 

1012 
lemma imp_ex: "((\<exists>x. P x) \<longrightarrow> Q) = (\<forall>x. P x \<longrightarrow> Q)" by iprover 

1013 
lemma all_not_ex: "(\<forall>x. P x) = (\<not> (\<exists>x. \<not> P x ))" by blast 

12281  1014 

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

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

1016 

60759  1017 
lemma ex_disj_distrib: "(\<exists>x. P x \<or> Q x) = ((\<exists>x. P x) \<or> (\<exists>x. Q x))" by iprover 
1018 
lemma all_conj_distrib: "(\<forall>x. P x \<and> Q x) = ((\<forall>x. P x) \<and> (\<forall>x. Q x))" by iprover 

12281  1019 

60758  1020 
text \<open> 
60759  1021 
\medskip The @{text "\<and>"} congruence rule: not included by default! 
60758  1022 
May slow rewrite proofs down by as much as 50\%\<close> 
12281  1023 

1024 
lemma conj_cong: 

60759  1025 
"(P = P') \<Longrightarrow> (P' \<Longrightarrow> (Q = Q')) \<Longrightarrow> ((P \<and> Q) = (P' \<and> Q'))" 
17589  1026 
by iprover 
12281  1027 

1028 
lemma rev_conj_cong: 

60759  1029 
"(Q = Q') \<Longrightarrow> (Q' \<Longrightarrow> (P = P')) \<Longrightarrow> ((P \<and> Q) = (P' \<and> Q'))" 
17589  1030 
by iprover 
12281  1031 

60758  1032 
text \<open>The @{text ""} congruence rule: not included by default!\<close> 
12281  1033 

1034 
lemma disj_cong: 

60759  1035 
"(P = P') \<Longrightarrow> (\<not> P' \<Longrightarrow> (Q = Q')) \<Longrightarrow> ((P \<or> Q) = (P' \<or> Q'))" 
12281  1036 
by blast 
1037 

1038 

60758  1039 
text \<open>\medskip ifthenelse rules\<close> 
12281  1040 

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

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

60759  1047 
lemma if_P: "P \<Longrightarrow> (if P then x else y) = x" 
38525  1048 
by (unfold If_def) blast 
12281  1049 

60759  1050 
lemma if_not_P: "\<not> P \<Longrightarrow> (if P then x else y) = y" 
38525  1051 
by (unfold If_def) blast 
12281  1052 

60759  1053 
lemma split_if: "P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))" 
12281  1054 
apply (rule case_split [of Q]) 
15481  1055 
apply (simplesubst if_P) 
1056 
prefer 3 apply (simplesubst if_not_P, blast+) 

12281  1057 
done 
1058 

60759  1059 
lemma split_if_asm: "P (if Q then x else y) = (\<not> ((Q \<and> \<not> P x) \<or> (\<not> Q \<and> \<not> P y)))" 
15481  1060 
by (simplesubst split_if, blast) 
12281  1061 

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

1062 
lemmas if_splits [no_atp] = split_if split_if_asm 
12281  1063 

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

15481  1065 
by (simplesubst split_if, blast) 
12281  1066 

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

15481  1068 
by (simplesubst split_if, blast) 
12281  1069 

60759  1070 
lemma if_bool_eq_conj: "(if P then Q else R) = ((P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R))" 
1071 
 \<open>This form is useful for expanding @{text "if"}s on the RIGHT of the @{text "\<Longrightarrow>"} symbol.\<close> 

12281  1072 
by (rule split_if) 
1073 

60759  1074 
lemma if_bool_eq_disj: "(if P then Q else R) = ((P \<and> Q) \<or> (\<not> P \<and> R))" 
60758  1075 
 \<open>And this form is useful for expanding @{text "if"}s on the LEFT.\<close> 
59504
8c6747dba731
New lemmas and a bit of tidying up.
paulson <lp15@cam.ac.uk>
parents:
59028
diff
changeset

1076 
by (simplesubst split_if) blast 
12281  1077 

60759  1078 
lemma Eq_TrueI: "P \<Longrightarrow> P \<equiv> True" by (unfold atomize_eq) iprover 
1079 
lemma Eq_FalseI: "\<not> P \<Longrightarrow> P \<equiv> False" by (unfold atomize_eq) iprover 

12281  1080 

60758  1081 
text \<open>\medskip let rules for simproc\<close> 
15423  1082 

60759  1083 
lemma Let_folded: "f x \<equiv> g x \<Longrightarrow> Let x f \<equiv> Let x g" 
15423  1084 
by (unfold Let_def) 
1085 

60759  1086 
lemma Let_unfold: "f x \<equiv> g \<Longrightarrow> Let x f \<equiv> g" 
15423  1087 
by (unfold Let_def) 
1088 

60758  1089 
text \<open> 
16999  1090 
The following copy of the implication operator is useful for 
1091 
finetuning congruence rules. It instructs the simplifier to simplify 

1092 
its premise. 

60758  1093 
\<close> 
16633
208ebc9311f2
Implemented trick (due to Tobias Nipkow) for finetuning simplification
berghofe
parents:
16587
diff
changeset

1094 

60759  1095 
definition simp_implies :: "[prop, prop] \<Rightarrow> prop" (infixr "=simp=>" 1) where 
1096 
"simp_implies \<equiv> op \<Longrightarrow>" 

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

1097 

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

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

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

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

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

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

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

1105 

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

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

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

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

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

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

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

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

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

1115 

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

1116 
lemma simp_implies_cong: 
60759  1117 
assumes PP' :"PROP P \<equiv> PROP P'" 
1118 
and P'QQ': "PROP P' \<Longrightarrow> (PROP Q \<equiv> PROP Q')" 

1119 
shows "(PROP P =simp=> PROP Q) \<equiv> (PROP P' =simp=> PROP Q')" 

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

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

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

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

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

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

1126 
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

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

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

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

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

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

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

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

1135 

20944  1136 
lemma uncurry: 
1137 
assumes "P \<longrightarrow> Q \<longrightarrow> R" 

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

23553  1139 
using assms by blast 
20944  1140 

1141 
lemma iff_allI: 

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

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

23553  1144 
using assms by blast 
20944  1145 

1146 
lemma iff_exI: 

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

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

23553  1149 
using assms by blast 
20944  1150 

1151 
lemma all_comm: 

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

1153 
by blast 

1154 

1155 
lemma ex_comm: 

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

1157 
by blast 

1158 

48891  1159 
ML_file "Tools/simpdata.ML" 
60758  1160 
ML \<open>open Simpdata\<close> 
42455  1161 

60758  1162 
setup \<open> 
58826  1163 
map_theory_simpset (put_simpset HOL_basic_ss) #> 
1164 
Simplifier.method_setup Splitter.split_modifiers 

60758  1165 
\<close> 
42455  1166 

60759  1167 
simproc_setup defined_Ex ("\<exists>x. P x") = \<open>fn _ => Quantifier1.rearrange_ex\<close> 
1168 
simproc_setup defined_All ("\<forall>x. P x") = \<open>fn _ => Quantifier1.rearrange_all\<close> 

21671  1169 

60759  1170 
text \<open>Simproc for proving @{text "(y = x) \<equiv> False"} from premise @{text "\<not> (x = y)"}:\<close> 
24035  1171 

60758  1172 
simproc_setup neq ("x = y") = \<open>fn _ => 
24035  1173 
let 
1174 
val neq_to_EQ_False = @{thm not_sym} RS @{thm Eq_FalseI}; 

1175 
fun is_neq eq lhs rhs thm = 

1176 
(case Thm.prop_of thm of 

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

1178 
Not = HOLogic.Not andalso eq' = eq andalso 

1179 
r' aconv lhs andalso l' aconv rhs 

1180 
 _ => false); 

1181 
fun proc ss ct = 

1182 
(case Thm.term_of ct of 

1183 
eq $ lhs $ rhs => 

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

1187 
 _ => NONE); 

1188 
in proc end; 

60758  1189 
\<close> 
24035  1190 

60758  1191 
simproc_setup let_simp ("Let x f") = \<open> 
24035  1192 
let 
1193 
val (f_Let_unfold, x_Let_unfold) = 

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

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

1205 
 count_loose _ _ = 0; 

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

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

1209 
 _ => true); 

1210 
in 

1211 
fn _ => fn ctxt => fn ct => 

1212 
if is_trivial_let (Thm.term_of ct) 

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

1214 
else 

1215 
let (*Norbert Schirmer's case*) 

1216 
val t = Thm.term_of ct; 

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

1218 
in 

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

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

1221 
if is_Free x orelse is_Bound x orelse is_Const x 

1222 
then SOME @{thm Let_def} 

1223 
else 

1224 
let 

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

1226 
val cx = Thm.cterm_of ctxt x; 

1227 
val xT = Thm.typ_of_cterm cx; 

1228 
val cf = Thm.cterm_of ctxt f; 

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

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

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

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

1233 
in 

1234 
if g aconv g' then 

1235 
let 

1236 
val rl = 

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

1238 
in SOME (rl OF [fx_g]) end 

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

1240 
then NONE (*avoid identity conversion*) 

1241 
else 

1242 
let 

1243 
val g'x = abs_g' $ x; 

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

1245 
val rl = 

1246 
@{thm Let_folded} > cterm_instantiate 

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

1248 
(x_Let_folded, cx), 

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

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

1251 
end 

1252 
 _ => NONE) 

1253 
end 

60758  1254 
end\<close> 
24035  1255 

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

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

21151  1260 
next 
1261 
assume "PROP P" 

23389  1262 
then show "PROP P" . 
21151  1263 
qed 
1264 

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

1267 

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

1269 
by default simp_all 

1270 

60183
4cd4c204578c
undid 6d7b7a037e8d because it does not help but slows simplification down by up to 5% (AODV)
nipkow
parents:
60169
diff
changeset

1271 
(* This is not made a simp rule because it does not improve any proofs 
4cd4c204578c
undid 6d7b7a037e8d because it does not help but slows simplification down by up to 5% (AODV)
nipkow
parents:
60169
diff
changeset

1272 
but slows some AFP entries down by 5% (cpu time). May 2015 *) 
60169
5ef8ed685965
swap False to the right in assumptions to be eliminated at the right end
nipkow
parents:
60151
diff
changeset

1273 
lemma implies_False_swap: "NO_MATCH (Trueprop False) P \<Longrightarrow> 
5ef8ed685965
swap False to the right in assumptions to be eliminated at the right end
nipkow
parents:
60151
diff
changeset

1274 
(False \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> False \<Longrightarrow> PROP Q)" 
5ef8ed685965
swap False to the right in assumptions to be eliminated at the right end
nipkow
parents:
60151
diff
changeset

1275 
by(rule swap_prems_eq) 
5ef8ed685965
swap False to the right in assumptions to be eliminated at the right end
nipkow
parents:
60151
diff
changeset

1276 

21151  1277 
lemma ex_simps: 
60759  1278 
"\<And>P Q. (\<exists>x. P x \<and> Q) = ((\<exists>x. P x) \<and> Q)" 
1279 
"\<And>P Q. (\<exists>x. P \<and> Q x) = (P \<and> (\<exists>x. Q x))" 

1280 
"\<And>P Q. (\<exists>x. P x \<or> Q) = ((\<exists>x. P x) \<or> Q)" 

1281 
"\<And>P Q. (\<exists>x. P \<or> Q x) = (P \<or> (\<exists>x. Q x))" 

1282 
"\<And>P Q. (\<exists>x. P x \<longrightarrow> Q) = ((\<forall>x. P x) \<longrightarrow> Q)" 

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

60758  1284 
 \<open>Miniscoping: pushing in existential quantifiers.\<close> 
21151  1285 
by (iprover  blast)+ 
1286 

1287 
lemma all_simps: 

60759  1288 
"\<And>P Q. (\<forall>x. P x \<and> Q) = ((\<forall>x. P x) \<and> Q)" 
1289 
"\<And>P Q. (\<forall>x. P \<and> Q x) = (P \<and> (\<forall>x. Q x))" 

1290 
"\<And>P Q. (\<forall>x. P x \<or> Q) = ((\<forall>x. P x) \<or> Q)" 

1291 
"\<And>P Q. (\<forall>x. P \<or> Q x) = (P \<or> (\<forall>x. Q x))" 

1292 
"\<And>P Q. (\<forall>x. P x \<longrightarrow> Q) = ((\<exists>x. P x) \<longrightarrow> Q)" 

1293 
"\<And>P Q. (\<forall>x. P \<longrightarrow> Q x) = (P \<longrightarrow> (\<forall>x. Q x))" 

60758  1294 
 \<open>Miniscoping: pushing in universal quantifiers.\<close> 
21151  1295 
by (iprover  blast)+ 
15481  1296 

21671  1297 
lemmas [simp] = 
1298 
triv_forall_equality (*prunes params*) 

60143  1299 
True_implies_equals implies_True_equals (*prune True in asms*) 
60183
4cd4c204578c
undid 6d7b7a037e8d because it does not help but slows simplification down by up to 5% (AODV)
nipkow
parents:
60169
diff
changeset

1300 
False_implies_equals (*prune False in asms*) 
21671  1301 
if_True 
1302 
if_False 

1303 
if_cancel 

1304 
if_eq_cancel 

1305 
imp_disjL 

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

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

60759  1309 
rewriting by "(P \<or> Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))" might be justified on the 
20973  1310 
grounds that it allows simplification of R in the two cases.*) 
21671  1311 
conj_assoc 
1312 
disj_assoc 

1313 
de_Morgan_conj 

1314 
de_Morgan_disj 

1315 
imp_disj1 

1316 
imp_disj2 

1317 
not_imp 

1318 
disj_not1 

1319 
not_all 

1320 
not_ex 

1321 
cases_simp 

1322 
the_eq_trivial 

1323 
the_sym_eq_trivial 

1324 
ex_simps 
