author | wenzelm |
Tue, 01 Nov 2016 01:20:33 +0100 | |
changeset 64439 | 2bafda87b524 |
parent 63906 | fa799a8e4adc |
child 68816 | 5a53724fe247 |
permissions | -rw-r--r-- |
1268 | 1 |
(* Title: FOL/IFOL.thy |
11677 | 2 |
Author: Lawrence C Paulson and Markus Wenzel |
3 |
*) |
|
35 | 4 |
|
60770 | 5 |
section \<open>Intuitionistic first-order logic\<close> |
35 | 6 |
|
15481 | 7 |
theory IFOL |
8 |
imports Pure |
|
9 |
begin |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
10 |
|
48891 | 11 |
ML_file "~~/src/Tools/misc_legacy.ML" |
12 |
ML_file "~~/src/Provers/splitter.ML" |
|
13 |
ML_file "~~/src/Provers/hypsubst.ML" |
|
14 |
ML_file "~~/src/Tools/IsaPlanner/zipper.ML" |
|
15 |
ML_file "~~/src/Tools/IsaPlanner/isand.ML" |
|
16 |
ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML" |
|
17 |
ML_file "~~/src/Provers/quantifier1.ML" |
|
18 |
ML_file "~~/src/Tools/intuitionistic.ML" |
|
19 |
ML_file "~~/src/Tools/project_rule.ML" |
|
20 |
ML_file "~~/src/Tools/atomize_elim.ML" |
|
21 |
||
0 | 22 |
|
60770 | 23 |
subsection \<open>Syntax and axiomatic basis\<close> |
11677 | 24 |
|
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39159
diff
changeset
|
25 |
setup Pure_Thy.old_appl_syntax_setup |
26956
1309a6a0a29f
setup PureThy.old_appl_syntax_setup -- theory Pure provides regular application syntax by default;
wenzelm
parents:
26580
diff
changeset
|
26 |
|
55380
4de48353034e
prefer vacuous definitional type classes over axiomatic ones;
wenzelm
parents:
52241
diff
changeset
|
27 |
class "term" |
36452 | 28 |
default_sort "term" |
0 | 29 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
30 |
typedecl o |
79 | 31 |
|
11747 | 32 |
judgment |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
33 |
Trueprop :: "o \<Rightarrow> prop" ("(_)" 5) |
0 | 34 |
|
79 | 35 |
|
60770 | 36 |
subsubsection \<open>Equality\<close> |
35 | 37 |
|
46972 | 38 |
axiomatization |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
39 |
eq :: "['a, 'a] \<Rightarrow> o" (infixl "=" 50) |
46972 | 40 |
where |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
41 |
refl: "a = a" and |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
42 |
subst: "a = b \<Longrightarrow> P(a) \<Longrightarrow> P(b)" |
79 | 43 |
|
0 | 44 |
|
60770 | 45 |
subsubsection \<open>Propositional logic\<close> |
46972 | 46 |
|
47 |
axiomatization |
|
48 |
False :: o and |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
49 |
conj :: "[o, o] => o" (infixr "\<and>" 35) and |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
50 |
disj :: "[o, o] => o" (infixr "\<or>" 30) and |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
51 |
imp :: "[o, o] => o" (infixr "\<longrightarrow>" 25) |
46972 | 52 |
where |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
53 |
conjI: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q" and |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
54 |
conjunct1: "P \<and> Q \<Longrightarrow> P" and |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
55 |
conjunct2: "P \<and> Q \<Longrightarrow> Q" and |
46972 | 56 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
57 |
disjI1: "P \<Longrightarrow> P \<or> Q" and |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
58 |
disjI2: "Q \<Longrightarrow> P \<or> Q" and |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
59 |
disjE: "\<lbrakk>P \<or> Q; P \<Longrightarrow> R; Q \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" and |
46972 | 60 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
61 |
impI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<longrightarrow> Q" and |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
62 |
mp: "\<lbrakk>P \<longrightarrow> Q; P\<rbrakk> \<Longrightarrow> Q" and |
46972 | 63 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
64 |
FalseE: "False \<Longrightarrow> P" |
46972 | 65 |
|
66 |
||
60770 | 67 |
subsubsection \<open>Quantifiers\<close> |
46972 | 68 |
|
69 |
axiomatization |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
70 |
All :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<forall>" 10) and |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
71 |
Ex :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10) |
46972 | 72 |
where |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
73 |
allI: "(\<And>x. P(x)) \<Longrightarrow> (\<forall>x. P(x))" and |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
74 |
spec: "(\<forall>x. P(x)) \<Longrightarrow> P(x)" and |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
75 |
exI: "P(x) \<Longrightarrow> (\<exists>x. P(x))" and |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
76 |
exE: "\<lbrakk>\<exists>x. P(x); \<And>x. P(x) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" |
46972 | 77 |
|
78 |
||
60770 | 79 |
subsubsection \<open>Definitions\<close> |
46972 | 80 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
81 |
definition "True \<equiv> False \<longrightarrow> False" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
82 |
|
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
83 |
definition Not ("\<not> _" [40] 40) |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
84 |
where not_def: "\<not> P \<equiv> P \<longrightarrow> False" |
46972 | 85 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
86 |
definition iff (infixr "\<longleftrightarrow>" 25) |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
87 |
where "P \<longleftrightarrow> Q \<equiv> (P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
88 |
|
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
89 |
definition Ex1 :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>!" 10) |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
90 |
where ex1_def: "\<exists>!x. P(x) \<equiv> \<exists>x. P(x) \<and> (\<forall>y. P(y) \<longrightarrow> y = x)" |
46972 | 91 |
|
62020 | 92 |
axiomatization where \<comment> \<open>Reflection, admissible\<close> |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
93 |
eq_reflection: "(x = y) \<Longrightarrow> (x \<equiv> y)" and |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
94 |
iff_reflection: "(P \<longleftrightarrow> Q) \<Longrightarrow> (P \<equiv> Q)" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
95 |
|
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
96 |
abbreviation not_equal :: "['a, 'a] \<Rightarrow> o" (infixl "\<noteq>" 50) |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
97 |
where "x \<noteq> y \<equiv> \<not> (x = y)" |
46972 | 98 |
|
99 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
100 |
subsubsection \<open>Old-style ASCII syntax\<close> |
79 | 101 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
102 |
notation (ASCII) |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
103 |
not_equal (infixl "~=" 50) and |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
104 |
Not ("~ _" [40] 40) and |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
105 |
conj (infixr "&" 35) and |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
106 |
disj (infixr "|" 30) and |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
107 |
All (binder "ALL " 10) and |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
108 |
Ex (binder "EX " 10) and |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
109 |
Ex1 (binder "EX! " 10) and |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
110 |
imp (infixr "-->" 25) and |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
111 |
iff (infixr "<->" 25) |
35 | 112 |
|
13779 | 113 |
|
60770 | 114 |
subsection \<open>Lemmas and proof tools\<close> |
11677 | 115 |
|
46972 | 116 |
lemmas strip = impI allI |
117 |
||
21539 | 118 |
lemma TrueI: True |
119 |
unfolding True_def by (rule impI) |
|
120 |
||
121 |
||
62020 | 122 |
subsubsection \<open>Sequent-style elimination rules for \<open>\<and>\<close> \<open>\<longrightarrow>\<close> and \<open>\<forall>\<close>\<close> |
21539 | 123 |
|
124 |
lemma conjE: |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
125 |
assumes major: "P \<and> Q" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
126 |
and r: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R" |
21539 | 127 |
shows R |
128 |
apply (rule r) |
|
129 |
apply (rule major [THEN conjunct1]) |
|
130 |
apply (rule major [THEN conjunct2]) |
|
131 |
done |
|
132 |
||
133 |
lemma impE: |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
134 |
assumes major: "P \<longrightarrow> Q" |
21539 | 135 |
and P |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
136 |
and r: "Q \<Longrightarrow> R" |
21539 | 137 |
shows R |
138 |
apply (rule r) |
|
139 |
apply (rule major [THEN mp]) |
|
60770 | 140 |
apply (rule \<open>P\<close>) |
21539 | 141 |
done |
142 |
||
143 |
lemma allE: |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
144 |
assumes major: "\<forall>x. P(x)" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
145 |
and r: "P(x) \<Longrightarrow> R" |
21539 | 146 |
shows R |
147 |
apply (rule r) |
|
148 |
apply (rule major [THEN spec]) |
|
149 |
done |
|
150 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
151 |
text \<open>Duplicates the quantifier; for use with @{ML eresolve_tac}.\<close> |
21539 | 152 |
lemma all_dupE: |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
153 |
assumes major: "\<forall>x. P(x)" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
154 |
and r: "\<lbrakk>P(x); \<forall>x. P(x)\<rbrakk> \<Longrightarrow> R" |
21539 | 155 |
shows R |
156 |
apply (rule r) |
|
157 |
apply (rule major [THEN spec]) |
|
158 |
apply (rule major) |
|
159 |
done |
|
160 |
||
161 |
||
62020 | 162 |
subsubsection \<open>Negation rules, which translate between \<open>\<not> P\<close> and \<open>P \<longrightarrow> False\<close>\<close> |
21539 | 163 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
164 |
lemma notI: "(P \<Longrightarrow> False) \<Longrightarrow> \<not> P" |
21539 | 165 |
unfolding not_def by (erule impI) |
166 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
167 |
lemma notE: "\<lbrakk>\<not> P; P\<rbrakk> \<Longrightarrow> R" |
21539 | 168 |
unfolding not_def by (erule mp [THEN FalseE]) |
169 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
170 |
lemma rev_notE: "\<lbrakk>P; \<not> P\<rbrakk> \<Longrightarrow> R" |
21539 | 171 |
by (erule notE) |
172 |
||
62020 | 173 |
text \<open>This is useful with the special implication rules for each kind of \<open>P\<close>.\<close> |
21539 | 174 |
lemma not_to_imp: |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
175 |
assumes "\<not> P" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
176 |
and r: "P \<longrightarrow> False \<Longrightarrow> Q" |
21539 | 177 |
shows Q |
178 |
apply (rule r) |
|
179 |
apply (rule impI) |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
180 |
apply (erule notE [OF \<open>\<not> P\<close>]) |
21539 | 181 |
done |
182 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
183 |
text \<open> |
62020 | 184 |
For substitution into an assumption \<open>P\<close>, reduce \<open>Q\<close> to \<open>P \<longrightarrow> Q\<close>, substitute into this implication, then apply \<open>impI\<close> to |
185 |
move \<open>P\<close> back into the assumptions. |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
186 |
\<close> |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
187 |
lemma rev_mp: "\<lbrakk>P; P \<longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
21539 | 188 |
by (erule mp) |
189 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
190 |
text \<open>Contrapositive of an inference rule.\<close> |
21539 | 191 |
lemma contrapos: |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
192 |
assumes major: "\<not> Q" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
193 |
and minor: "P \<Longrightarrow> Q" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
194 |
shows "\<not> P" |
21539 | 195 |
apply (rule major [THEN notE, THEN notI]) |
196 |
apply (erule minor) |
|
197 |
done |
|
198 |
||
199 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
200 |
subsubsection \<open>Modus Ponens Tactics\<close> |
21539 | 201 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
202 |
text \<open> |
62020 | 203 |
Finds \<open>P \<longrightarrow> Q\<close> and P in the assumptions, replaces implication by |
204 |
\<open>Q\<close>. |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
205 |
\<close> |
60770 | 206 |
ML \<open> |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
207 |
fun mp_tac ctxt i = |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
208 |
eresolve_tac ctxt @{thms notE impE} i THEN assume_tac ctxt i; |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
209 |
fun eq_mp_tac ctxt i = |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
210 |
eresolve_tac ctxt @{thms notE impE} i THEN eq_assume_tac i; |
60770 | 211 |
\<close> |
21539 | 212 |
|
213 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
214 |
subsection \<open>If-and-only-if\<close> |
21539 | 215 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
216 |
lemma iffI: "\<lbrakk>P \<Longrightarrow> Q; Q \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P \<longleftrightarrow> Q" |
21539 | 217 |
apply (unfold iff_def) |
218 |
apply (rule conjI) |
|
219 |
apply (erule impI) |
|
220 |
apply (erule impI) |
|
221 |
done |
|
222 |
||
223 |
lemma iffE: |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
224 |
assumes major: "P \<longleftrightarrow> Q" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
225 |
and r: "P \<longrightarrow> Q \<Longrightarrow> Q \<longrightarrow> P \<Longrightarrow> R" |
21539 | 226 |
shows R |
227 |
apply (insert major, unfold iff_def) |
|
228 |
apply (erule conjE) |
|
229 |
apply (erule r) |
|
230 |
apply assumption |
|
231 |
done |
|
232 |
||
233 |
||
62020 | 234 |
subsubsection \<open>Destruct rules for \<open>\<longleftrightarrow>\<close> similar to Modus Ponens\<close> |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
235 |
|
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
236 |
lemma iffD1: "\<lbrakk>P \<longleftrightarrow> Q; P\<rbrakk> \<Longrightarrow> Q" |
21539 | 237 |
apply (unfold iff_def) |
238 |
apply (erule conjunct1 [THEN mp]) |
|
239 |
apply assumption |
|
240 |
done |
|
241 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
242 |
lemma iffD2: "\<lbrakk>P \<longleftrightarrow> Q; Q\<rbrakk> \<Longrightarrow> P" |
21539 | 243 |
apply (unfold iff_def) |
244 |
apply (erule conjunct2 [THEN mp]) |
|
245 |
apply assumption |
|
246 |
done |
|
247 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
248 |
lemma rev_iffD1: "\<lbrakk>P; P \<longleftrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
21539 | 249 |
apply (erule iffD1) |
250 |
apply assumption |
|
251 |
done |
|
252 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
253 |
lemma rev_iffD2: "\<lbrakk>Q; P \<longleftrightarrow> Q\<rbrakk> \<Longrightarrow> P" |
21539 | 254 |
apply (erule iffD2) |
255 |
apply assumption |
|
256 |
done |
|
257 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
258 |
lemma iff_refl: "P \<longleftrightarrow> P" |
21539 | 259 |
by (rule iffI) |
260 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
261 |
lemma iff_sym: "Q \<longleftrightarrow> P \<Longrightarrow> P \<longleftrightarrow> Q" |
21539 | 262 |
apply (erule iffE) |
263 |
apply (rule iffI) |
|
264 |
apply (assumption | erule mp)+ |
|
265 |
done |
|
266 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
267 |
lemma iff_trans: "\<lbrakk>P \<longleftrightarrow> Q; Q \<longleftrightarrow> R\<rbrakk> \<Longrightarrow> P \<longleftrightarrow> R" |
21539 | 268 |
apply (rule iffI) |
269 |
apply (assumption | erule iffE | erule (1) notE impE)+ |
|
270 |
done |
|
271 |
||
272 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
273 |
subsection \<open>Unique existence\<close> |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
274 |
|
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
275 |
text \<open> |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
276 |
NOTE THAT the following 2 quantifications: |
21539 | 277 |
|
63906
fa799a8e4adc
repair LaTeX dropout from f83ef97d8d7d
Lars Hupel <lars.hupel@mytum.de>
parents:
63901
diff
changeset
|
278 |
\<^item> \<open>\<exists>!x\<close> such that [\<open>\<exists>!y\<close> such that P(x,y)] (sequential) |
fa799a8e4adc
repair LaTeX dropout from f83ef97d8d7d
Lars Hupel <lars.hupel@mytum.de>
parents:
63901
diff
changeset
|
279 |
\<^item> \<open>\<exists>!x,y\<close> such that P(x,y) (simultaneous) |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
280 |
|
63906
fa799a8e4adc
repair LaTeX dropout from f83ef97d8d7d
Lars Hupel <lars.hupel@mytum.de>
parents:
63901
diff
changeset
|
281 |
do NOT mean the same thing. The parser treats \<open>\<exists>!x y.P(x,y)\<close> as sequential. |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
282 |
\<close> |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
283 |
|
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
284 |
lemma ex1I: "P(a) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> x = a) \<Longrightarrow> \<exists>!x. P(x)" |
21539 | 285 |
apply (unfold ex1_def) |
23393 | 286 |
apply (assumption | rule exI conjI allI impI)+ |
21539 | 287 |
done |
288 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
289 |
text \<open>Sometimes easier to use: the premises have no shared variables. Safe!\<close> |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
290 |
lemma ex_ex1I: "\<exists>x. P(x) \<Longrightarrow> (\<And>x y. \<lbrakk>P(x); P(y)\<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> \<exists>!x. P(x)" |
23393 | 291 |
apply (erule exE) |
292 |
apply (rule ex1I) |
|
293 |
apply assumption |
|
294 |
apply assumption |
|
21539 | 295 |
done |
296 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
297 |
lemma ex1E: "\<exists>! x. P(x) \<Longrightarrow> (\<And>x. \<lbrakk>P(x); \<forall>y. P(y) \<longrightarrow> y = x\<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R" |
23393 | 298 |
apply (unfold ex1_def) |
21539 | 299 |
apply (assumption | erule exE conjE)+ |
300 |
done |
|
301 |
||
302 |
||
62020 | 303 |
subsubsection \<open>\<open>\<longleftrightarrow>\<close> congruence rules for simplification\<close> |
21539 | 304 |
|
62020 | 305 |
text \<open>Use \<open>iffE\<close> on a premise. For \<open>conj_cong\<close>, \<open>imp_cong\<close>, \<open>all_cong\<close>, \<open>ex_cong\<close>.\<close> |
60770 | 306 |
ML \<open> |
59529 | 307 |
fun iff_tac ctxt prems i = |
308 |
resolve_tac ctxt (prems RL @{thms iffE}) i THEN |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
309 |
REPEAT1 (eresolve_tac ctxt @{thms asm_rl mp} i); |
60770 | 310 |
\<close> |
21539 | 311 |
|
59529 | 312 |
method_setup iff = |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
313 |
\<open>Attrib.thms >> |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
314 |
(fn prems => fn ctxt => SIMPLE_METHOD' (iff_tac ctxt prems))\<close> |
59529 | 315 |
|
21539 | 316 |
lemma conj_cong: |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
317 |
assumes "P \<longleftrightarrow> P'" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
318 |
and "P' \<Longrightarrow> Q \<longleftrightarrow> Q'" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
319 |
shows "(P \<and> Q) \<longleftrightarrow> (P' \<and> Q')" |
21539 | 320 |
apply (insert assms) |
59529 | 321 |
apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+ |
21539 | 322 |
done |
323 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
324 |
text \<open>Reversed congruence rule! Used in ZF/Order.\<close> |
21539 | 325 |
lemma conj_cong2: |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
326 |
assumes "P \<longleftrightarrow> P'" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
327 |
and "P' \<Longrightarrow> Q \<longleftrightarrow> Q'" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
328 |
shows "(Q \<and> P) \<longleftrightarrow> (Q' \<and> P')" |
21539 | 329 |
apply (insert assms) |
59529 | 330 |
apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+ |
21539 | 331 |
done |
332 |
||
333 |
lemma disj_cong: |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
334 |
assumes "P \<longleftrightarrow> P'" and "Q \<longleftrightarrow> Q'" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
335 |
shows "(P \<or> Q) \<longleftrightarrow> (P' \<or> Q')" |
21539 | 336 |
apply (insert assms) |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
337 |
apply (erule iffE disjE disjI1 disjI2 | |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
338 |
assumption | rule iffI | erule (1) notE impE)+ |
21539 | 339 |
done |
340 |
||
341 |
lemma imp_cong: |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
342 |
assumes "P \<longleftrightarrow> P'" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
343 |
and "P' \<Longrightarrow> Q \<longleftrightarrow> Q'" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
344 |
shows "(P \<longrightarrow> Q) \<longleftrightarrow> (P' \<longrightarrow> Q')" |
21539 | 345 |
apply (insert assms) |
59529 | 346 |
apply (assumption | rule iffI impI | erule iffE | erule (1) notE impE | iff assms)+ |
21539 | 347 |
done |
348 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
349 |
lemma iff_cong: "\<lbrakk>P \<longleftrightarrow> P'; Q \<longleftrightarrow> Q'\<rbrakk> \<Longrightarrow> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P' \<longleftrightarrow> Q')" |
21539 | 350 |
apply (erule iffE | assumption | rule iffI | erule (1) notE impE)+ |
351 |
done |
|
352 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
353 |
lemma not_cong: "P \<longleftrightarrow> P' \<Longrightarrow> \<not> P \<longleftrightarrow> \<not> P'" |
21539 | 354 |
apply (assumption | rule iffI notI | erule (1) notE impE | erule iffE notE)+ |
355 |
done |
|
356 |
||
357 |
lemma all_cong: |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
358 |
assumes "\<And>x. P(x) \<longleftrightarrow> Q(x)" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
359 |
shows "(\<forall>x. P(x)) \<longleftrightarrow> (\<forall>x. Q(x))" |
59529 | 360 |
apply (assumption | rule iffI allI | erule (1) notE impE | erule allE | iff assms)+ |
21539 | 361 |
done |
362 |
||
363 |
lemma ex_cong: |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
364 |
assumes "\<And>x. P(x) \<longleftrightarrow> Q(x)" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
365 |
shows "(\<exists>x. P(x)) \<longleftrightarrow> (\<exists>x. Q(x))" |
59529 | 366 |
apply (erule exE | assumption | rule iffI exI | erule (1) notE impE | iff assms)+ |
21539 | 367 |
done |
368 |
||
369 |
lemma ex1_cong: |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
370 |
assumes "\<And>x. P(x) \<longleftrightarrow> Q(x)" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
371 |
shows "(\<exists>!x. P(x)) \<longleftrightarrow> (\<exists>!x. Q(x))" |
59529 | 372 |
apply (erule ex1E spec [THEN mp] | assumption | rule iffI ex1I | erule (1) notE impE | iff assms)+ |
21539 | 373 |
done |
374 |
||
375 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
376 |
subsection \<open>Equality rules\<close> |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
377 |
|
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
378 |
lemma sym: "a = b \<Longrightarrow> b = a" |
21539 | 379 |
apply (erule subst) |
380 |
apply (rule refl) |
|
381 |
done |
|
382 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
383 |
lemma trans: "\<lbrakk>a = b; b = c\<rbrakk> \<Longrightarrow> a = c" |
21539 | 384 |
apply (erule subst, assumption) |
385 |
done |
|
386 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
387 |
lemma not_sym: "b \<noteq> a \<Longrightarrow> a \<noteq> b" |
21539 | 388 |
apply (erule contrapos) |
389 |
apply (erule sym) |
|
390 |
done |
|
391 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
392 |
text \<open> |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
393 |
Two theorems for rewriting only one instance of a definition: |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
394 |
the first for definitions of formulae and the second for terms. |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
395 |
\<close> |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
396 |
|
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
397 |
lemma def_imp_iff: "(A \<equiv> B) \<Longrightarrow> A \<longleftrightarrow> B" |
21539 | 398 |
apply unfold |
399 |
apply (rule iff_refl) |
|
400 |
done |
|
401 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
402 |
lemma meta_eq_to_obj_eq: "(A \<equiv> B) \<Longrightarrow> A = B" |
21539 | 403 |
apply unfold |
404 |
apply (rule refl) |
|
405 |
done |
|
406 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
407 |
lemma meta_eq_to_iff: "x \<equiv> y \<Longrightarrow> x \<longleftrightarrow> y" |
21539 | 408 |
by unfold (rule iff_refl) |
409 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
410 |
text \<open>Substitution.\<close> |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
411 |
lemma ssubst: "\<lbrakk>b = a; P(a)\<rbrakk> \<Longrightarrow> P(b)" |
21539 | 412 |
apply (drule sym) |
413 |
apply (erule (1) subst) |
|
414 |
done |
|
415 |
||
62020 | 416 |
text \<open>A special case of \<open>ex1E\<close> that would otherwise need quantifier |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
417 |
expansion.\<close> |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
418 |
lemma ex1_equalsE: "\<lbrakk>\<exists>!x. P(x); P(a); P(b)\<rbrakk> \<Longrightarrow> a = b" |
21539 | 419 |
apply (erule ex1E) |
420 |
apply (rule trans) |
|
421 |
apply (rule_tac [2] sym) |
|
422 |
apply (assumption | erule spec [THEN mp])+ |
|
423 |
done |
|
424 |
||
425 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
426 |
subsubsection \<open>Polymorphic congruence rules\<close> |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
427 |
|
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
428 |
lemma subst_context: "a = b \<Longrightarrow> t(a) = t(b)" |
21539 | 429 |
apply (erule ssubst) |
430 |
apply (rule refl) |
|
431 |
done |
|
432 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
433 |
lemma subst_context2: "\<lbrakk>a = b; c = d\<rbrakk> \<Longrightarrow> t(a,c) = t(b,d)" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
434 |
apply (erule ssubst)+ |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
435 |
apply (rule refl) |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
436 |
done |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
437 |
|
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
438 |
lemma subst_context3: "\<lbrakk>a = b; c = d; e = f\<rbrakk> \<Longrightarrow> t(a,c,e) = t(b,d,f)" |
21539 | 439 |
apply (erule ssubst)+ |
440 |
apply (rule refl) |
|
441 |
done |
|
442 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
443 |
text \<open> |
61490 | 444 |
Useful with @{ML eresolve_tac} for proving equalities from known |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
445 |
equalities. |
21539 | 446 |
|
447 |
a = b |
|
448 |
| | |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
449 |
c = d |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
450 |
\<close> |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
451 |
lemma box_equals: "\<lbrakk>a = b; a = c; b = d\<rbrakk> \<Longrightarrow> c = d" |
21539 | 452 |
apply (rule trans) |
453 |
apply (rule trans) |
|
454 |
apply (rule sym) |
|
455 |
apply assumption+ |
|
456 |
done |
|
457 |
||
62020 | 458 |
text \<open>Dual of \<open>box_equals\<close>: for proving equalities backwards.\<close> |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
459 |
lemma simp_equals: "\<lbrakk>a = c; b = d; c = d\<rbrakk> \<Longrightarrow> a = b" |
21539 | 460 |
apply (rule trans) |
461 |
apply (rule trans) |
|
462 |
apply assumption+ |
|
463 |
apply (erule sym) |
|
464 |
done |
|
465 |
||
466 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
467 |
subsubsection \<open>Congruence rules for predicate letters\<close> |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
468 |
|
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
469 |
lemma pred1_cong: "a = a' \<Longrightarrow> P(a) \<longleftrightarrow> P(a')" |
21539 | 470 |
apply (rule iffI) |
471 |
apply (erule (1) subst) |
|
472 |
apply (erule (1) ssubst) |
|
473 |
done |
|
474 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
475 |
lemma pred2_cong: "\<lbrakk>a = a'; b = b'\<rbrakk> \<Longrightarrow> P(a,b) \<longleftrightarrow> P(a',b')" |
21539 | 476 |
apply (rule iffI) |
477 |
apply (erule subst)+ |
|
478 |
apply assumption |
|
479 |
apply (erule ssubst)+ |
|
480 |
apply assumption |
|
481 |
done |
|
482 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
483 |
lemma pred3_cong: "\<lbrakk>a = a'; b = b'; c = c'\<rbrakk> \<Longrightarrow> P(a,b,c) \<longleftrightarrow> P(a',b',c')" |
21539 | 484 |
apply (rule iffI) |
485 |
apply (erule subst)+ |
|
486 |
apply assumption |
|
487 |
apply (erule ssubst)+ |
|
488 |
apply assumption |
|
489 |
done |
|
490 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
491 |
text \<open>Special case for the equality predicate!\<close> |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
492 |
lemma eq_cong: "\<lbrakk>a = a'; b = b'\<rbrakk> \<Longrightarrow> a = b \<longleftrightarrow> a' = b'" |
21539 | 493 |
apply (erule (1) pred2_cong) |
494 |
done |
|
495 |
||
496 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
497 |
subsection \<open>Simplifications of assumed implications\<close> |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
498 |
|
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
499 |
text \<open> |
62020 | 500 |
Roy Dyckhoff has proved that \<open>conj_impE\<close>, \<open>disj_impE\<close>, and |
501 |
\<open>imp_impE\<close> used with @{ML mp_tac} (restricted to atomic formulae) is |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
502 |
COMPLETE for intuitionistic propositional logic. |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
503 |
|
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
504 |
See R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
505 |
(preprint, University of St Andrews, 1991). |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
506 |
\<close> |
21539 | 507 |
|
508 |
lemma conj_impE: |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
509 |
assumes major: "(P \<and> Q) \<longrightarrow> S" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
510 |
and r: "P \<longrightarrow> (Q \<longrightarrow> S) \<Longrightarrow> R" |
21539 | 511 |
shows R |
512 |
by (assumption | rule conjI impI major [THEN mp] r)+ |
|
513 |
||
514 |
lemma disj_impE: |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
515 |
assumes major: "(P \<or> Q) \<longrightarrow> S" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
516 |
and r: "\<lbrakk>P \<longrightarrow> S; Q \<longrightarrow> S\<rbrakk> \<Longrightarrow> R" |
21539 | 517 |
shows R |
518 |
by (assumption | rule disjI1 disjI2 impI major [THEN mp] r)+ |
|
519 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
520 |
text \<open>Simplifies the implication. Classical version is stronger. |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
521 |
Still UNSAFE since Q must be provable -- backtracking needed.\<close> |
21539 | 522 |
lemma imp_impE: |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
523 |
assumes major: "(P \<longrightarrow> Q) \<longrightarrow> S" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
524 |
and r1: "\<lbrakk>P; Q \<longrightarrow> S\<rbrakk> \<Longrightarrow> Q" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
525 |
and r2: "S \<Longrightarrow> R" |
21539 | 526 |
shows R |
527 |
by (assumption | rule impI major [THEN mp] r1 r2)+ |
|
528 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
529 |
text \<open>Simplifies the implication. Classical version is stronger. |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
530 |
Still UNSAFE since ~P must be provable -- backtracking needed.\<close> |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
531 |
lemma not_impE: "\<not> P \<longrightarrow> S \<Longrightarrow> (P \<Longrightarrow> False) \<Longrightarrow> (S \<Longrightarrow> R) \<Longrightarrow> R" |
23393 | 532 |
apply (drule mp) |
533 |
apply (rule notI) |
|
534 |
apply assumption |
|
535 |
apply assumption |
|
21539 | 536 |
done |
537 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
538 |
text \<open>Simplifies the implication. UNSAFE.\<close> |
21539 | 539 |
lemma iff_impE: |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
540 |
assumes major: "(P \<longleftrightarrow> Q) \<longrightarrow> S" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
541 |
and r1: "\<lbrakk>P; Q \<longrightarrow> S\<rbrakk> \<Longrightarrow> Q" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
542 |
and r2: "\<lbrakk>Q; P \<longrightarrow> S\<rbrakk> \<Longrightarrow> P" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
543 |
and r3: "S \<Longrightarrow> R" |
21539 | 544 |
shows R |
545 |
apply (assumption | rule iffI impI major [THEN mp] r1 r2 r3)+ |
|
546 |
done |
|
547 |
||
62020 | 548 |
text \<open>What if \<open>(\<forall>x. \<not> \<not> P(x)) \<longrightarrow> \<not> \<not> (\<forall>x. P(x))\<close> is an assumption? |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
549 |
UNSAFE.\<close> |
21539 | 550 |
lemma all_impE: |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
551 |
assumes major: "(\<forall>x. P(x)) \<longrightarrow> S" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
552 |
and r1: "\<And>x. P(x)" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
553 |
and r2: "S \<Longrightarrow> R" |
21539 | 554 |
shows R |
23393 | 555 |
apply (rule allI impI major [THEN mp] r1 r2)+ |
21539 | 556 |
done |
557 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
558 |
text \<open> |
62020 | 559 |
Unsafe: \<open>\<exists>x. P(x)) \<longrightarrow> S\<close> is equivalent |
560 |
to \<open>\<forall>x. P(x) \<longrightarrow> S\<close>.\<close> |
|
21539 | 561 |
lemma ex_impE: |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
562 |
assumes major: "(\<exists>x. P(x)) \<longrightarrow> S" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
563 |
and r: "P(x) \<longrightarrow> S \<Longrightarrow> R" |
21539 | 564 |
shows R |
565 |
apply (assumption | rule exI impI major [THEN mp] r)+ |
|
566 |
done |
|
567 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
568 |
text \<open>Courtesy of Krzysztof Grabczewski.\<close> |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
569 |
lemma disj_imp_disj: "P \<or> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> S) \<Longrightarrow> R \<or> S" |
23393 | 570 |
apply (erule disjE) |
21539 | 571 |
apply (rule disjI1) apply assumption |
572 |
apply (rule disjI2) apply assumption |
|
573 |
done |
|
11734 | 574 |
|
60770 | 575 |
ML \<open> |
32172 | 576 |
structure Project_Rule = Project_Rule |
577 |
( |
|
22139 | 578 |
val conjunct1 = @{thm conjunct1} |
579 |
val conjunct2 = @{thm conjunct2} |
|
580 |
val mp = @{thm mp} |
|
32172 | 581 |
) |
60770 | 582 |
\<close> |
18481 | 583 |
|
48891 | 584 |
ML_file "fologic.ML" |
21539 | 585 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
586 |
lemma thin_refl: "\<lbrakk>x = x; PROP W\<rbrakk> \<Longrightarrow> PROP W" . |
21539 | 587 |
|
60770 | 588 |
ML \<open> |
42799 | 589 |
structure Hypsubst = Hypsubst |
590 |
( |
|
591 |
val dest_eq = FOLogic.dest_eq |
|
592 |
val dest_Trueprop = FOLogic.dest_Trueprop |
|
593 |
val dest_imp = FOLogic.dest_imp |
|
594 |
val eq_reflection = @{thm eq_reflection} |
|
595 |
val rev_eq_reflection = @{thm meta_eq_to_obj_eq} |
|
596 |
val imp_intr = @{thm impI} |
|
597 |
val rev_mp = @{thm rev_mp} |
|
598 |
val subst = @{thm subst} |
|
599 |
val sym = @{thm sym} |
|
600 |
val thin_refl = @{thm thin_refl} |
|
601 |
); |
|
602 |
open Hypsubst; |
|
60770 | 603 |
\<close> |
42799 | 604 |
|
48891 | 605 |
ML_file "intprover.ML" |
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
606 |
|
4092 | 607 |
|
60770 | 608 |
subsection \<open>Intuitionistic Reasoning\<close> |
12368 | 609 |
|
60770 | 610 |
setup \<open>Intuitionistic.method_setup @{binding iprover}\<close> |
30165
6ee87f67d9cd
moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
30160
diff
changeset
|
611 |
|
12349 | 612 |
lemma impE': |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
613 |
assumes 1: "P \<longrightarrow> Q" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
614 |
and 2: "Q \<Longrightarrow> R" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
615 |
and 3: "P \<longrightarrow> Q \<Longrightarrow> P" |
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset
|
616 |
shows R |
12349 | 617 |
proof - |
618 |
from 3 and 1 have P . |
|
12368 | 619 |
with 1 have Q by (rule impE) |
12349 | 620 |
with 2 show R . |
621 |
qed |
|
622 |
||
623 |
lemma allE': |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
624 |
assumes 1: "\<forall>x. P(x)" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
625 |
and 2: "P(x) \<Longrightarrow> \<forall>x. P(x) \<Longrightarrow> Q" |
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset
|
626 |
shows Q |
12349 | 627 |
proof - |
628 |
from 1 have "P(x)" by (rule spec) |
|
629 |
from this and 1 show Q by (rule 2) |
|
630 |
qed |
|
631 |
||
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset
|
632 |
lemma notE': |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
633 |
assumes 1: "\<not> P" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
634 |
and 2: "\<not> P \<Longrightarrow> P" |
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset
|
635 |
shows R |
12349 | 636 |
proof - |
637 |
from 2 and 1 have P . |
|
638 |
with 1 show R by (rule notE) |
|
639 |
qed |
|
640 |
||
641 |
lemmas [Pure.elim!] = disjE iffE FalseE conjE exE |
|
642 |
and [Pure.intro!] = iffI conjI impI TrueI notI allI refl |
|
643 |
and [Pure.elim 2] = allE notE' impE' |
|
644 |
and [Pure.intro] = exI disjI2 disjI1 |
|
645 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
646 |
setup \<open> |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
647 |
Context_Rules.addSWrapper |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
648 |
(fn ctxt => fn tac => hyp_subst_tac ctxt ORELSE' tac) |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
649 |
\<close> |
12349 | 650 |
|
651 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
652 |
lemma iff_not_sym: "\<not> (Q \<longleftrightarrow> P) \<Longrightarrow> \<not> (P \<longleftrightarrow> Q)" |
17591 | 653 |
by iprover |
12368 | 654 |
|
655 |
lemmas [sym] = sym iff_sym not_sym iff_not_sym |
|
656 |
and [Pure.elim?] = iffD1 iffD2 impE |
|
657 |
||
658 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
659 |
lemma eq_commute: "a = b \<longleftrightarrow> b = a" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
660 |
apply (rule iffI) |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
661 |
apply (erule sym)+ |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
662 |
done |
13435 | 663 |
|
664 |
||
60770 | 665 |
subsection \<open>Atomizing meta-level rules\<close> |
11677 | 666 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
667 |
lemma atomize_all [atomize]: "(\<And>x. P(x)) \<equiv> Trueprop (\<forall>x. P(x))" |
11976 | 668 |
proof |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
669 |
assume "\<And>x. P(x)" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
670 |
then show "\<forall>x. P(x)" .. |
11677 | 671 |
next |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
672 |
assume "\<forall>x. P(x)" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
673 |
then show "\<And>x. P(x)" .. |
11677 | 674 |
qed |
675 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
676 |
lemma atomize_imp [atomize]: "(A \<Longrightarrow> B) \<equiv> Trueprop (A \<longrightarrow> B)" |
11976 | 677 |
proof |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
678 |
assume "A \<Longrightarrow> B" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
679 |
then show "A \<longrightarrow> B" .. |
11677 | 680 |
next |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
681 |
assume "A \<longrightarrow> B" and A |
22931 | 682 |
then show B by (rule mp) |
11677 | 683 |
qed |
684 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
685 |
lemma atomize_eq [atomize]: "(x \<equiv> y) \<equiv> Trueprop (x = y)" |
11976 | 686 |
proof |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
687 |
assume "x \<equiv> y" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
688 |
show "x = y" unfolding \<open>x \<equiv> y\<close> by (rule refl) |
11677 | 689 |
next |
690 |
assume "x = y" |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
691 |
then show "x \<equiv> y" by (rule eq_reflection) |
11677 | 692 |
qed |
693 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
694 |
lemma atomize_iff [atomize]: "(A \<equiv> B) \<equiv> Trueprop (A \<longleftrightarrow> B)" |
18813 | 695 |
proof |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
696 |
assume "A \<equiv> B" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
697 |
show "A \<longleftrightarrow> B" unfolding \<open>A \<equiv> B\<close> by (rule iff_refl) |
18813 | 698 |
next |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
699 |
assume "A \<longleftrightarrow> B" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
700 |
then show "A \<equiv> B" by (rule iff_reflection) |
18813 | 701 |
qed |
702 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
703 |
lemma atomize_conj [atomize]: "(A &&& B) \<equiv> Trueprop (A \<and> B)" |
11976 | 704 |
proof |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
705 |
assume conj: "A &&& B" |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
706 |
show "A \<and> B" |
19120
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
707 |
proof (rule conjI) |
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
708 |
from conj show A by (rule conjunctionD1) |
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
709 |
from conj show B by (rule conjunctionD2) |
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
710 |
qed |
11953 | 711 |
next |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
712 |
assume conj: "A \<and> B" |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
713 |
show "A &&& B" |
19120
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
714 |
proof - |
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
715 |
from conj show A .. |
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
716 |
from conj show B .. |
11953 | 717 |
qed |
718 |
qed |
|
719 |
||
12368 | 720 |
lemmas [symmetric, rulify] = atomize_all atomize_imp |
18861 | 721 |
and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff |
11771 | 722 |
|
11848 | 723 |
|
60770 | 724 |
subsection \<open>Atomizing elimination rules\<close> |
26580
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset
|
725 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
726 |
lemma atomize_exL[atomize_elim]: "(\<And>x. P(x) \<Longrightarrow> Q) \<equiv> ((\<exists>x. P(x)) \<Longrightarrow> Q)" |
57948 | 727 |
by rule iprover+ |
26580
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset
|
728 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
729 |
lemma atomize_conjL[atomize_elim]: "(A \<Longrightarrow> B \<Longrightarrow> C) \<equiv> (A \<and> B \<Longrightarrow> C)" |
57948 | 730 |
by rule iprover+ |
26580
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset
|
731 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
732 |
lemma atomize_disjL[atomize_elim]: "((A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C) \<equiv> ((A \<or> B \<Longrightarrow> C) \<Longrightarrow> C)" |
57948 | 733 |
by rule iprover+ |
26580
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset
|
734 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
735 |
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:
26286
diff
changeset
|
736 |
|
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
26286
diff
changeset
|
737 |
|
60770 | 738 |
subsection \<open>Calculational rules\<close> |
11848 | 739 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
740 |
lemma forw_subst: "a = b \<Longrightarrow> P(b) \<Longrightarrow> P(a)" |
11848 | 741 |
by (rule ssubst) |
742 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
743 |
lemma back_subst: "P(a) \<Longrightarrow> a = b \<Longrightarrow> P(b)" |
11848 | 744 |
by (rule subst) |
745 |
||
60770 | 746 |
text \<open> |
11848 | 747 |
Note that this list of rules is in reverse order of priorities. |
60770 | 748 |
\<close> |
11848 | 749 |
|
12019 | 750 |
lemmas basic_trans_rules [trans] = |
11848 | 751 |
forw_subst |
752 |
back_subst |
|
753 |
rev_mp |
|
754 |
mp |
|
755 |
trans |
|
756 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
757 |
|
60770 | 758 |
subsection \<open>``Let'' declarations\<close> |
13779 | 759 |
|
41229
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
39557
diff
changeset
|
760 |
nonterminal letbinds and letbind |
13779 | 761 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
762 |
definition Let :: "['a::{}, 'a => 'b] \<Rightarrow> ('b::{})" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
763 |
where "Let(s, f) \<equiv> f(s)" |
13779 | 764 |
|
765 |
syntax |
|
766 |
"_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) |
|
767 |
"" :: "letbind => letbinds" ("_") |
|
768 |
"_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") |
|
769 |
"_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) |
|
770 |
||
771 |
translations |
|
772 |
"_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))" |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
773 |
"let x = a in e" == "CONST Let(a, \<lambda>x. e)" |
13779 | 774 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
775 |
lemma LetI: |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
776 |
assumes "\<And>x. x = t \<Longrightarrow> P(u(x))" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
777 |
shows "P(let x = t in u(x))" |
21539 | 778 |
apply (unfold Let_def) |
779 |
apply (rule refl [THEN assms]) |
|
780 |
done |
|
781 |
||
782 |
||
60770 | 783 |
subsection \<open>Intuitionistic simplification rules\<close> |
26286 | 784 |
|
785 |
lemma conj_simps: |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
786 |
"P \<and> True \<longleftrightarrow> P" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
787 |
"True \<and> P \<longleftrightarrow> P" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
788 |
"P \<and> False \<longleftrightarrow> False" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
789 |
"False \<and> P \<longleftrightarrow> False" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
790 |
"P \<and> P \<longleftrightarrow> P" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
791 |
"P \<and> P \<and> Q \<longleftrightarrow> P \<and> Q" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
792 |
"P \<and> \<not> P \<longleftrightarrow> False" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
793 |
"\<not> P \<and> P \<longleftrightarrow> False" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
794 |
"(P \<and> Q) \<and> R \<longleftrightarrow> P \<and> (Q \<and> R)" |
26286 | 795 |
by iprover+ |
796 |
||
797 |
lemma disj_simps: |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
798 |
"P \<or> True \<longleftrightarrow> True" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
799 |
"True \<or> P \<longleftrightarrow> True" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
800 |
"P \<or> False \<longleftrightarrow> P" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
801 |
"False \<or> P \<longleftrightarrow> P" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
802 |
"P \<or> P \<longleftrightarrow> P" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
803 |
"P \<or> P \<or> Q \<longleftrightarrow> P \<or> Q" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
804 |
"(P \<or> Q) \<or> R \<longleftrightarrow> P \<or> (Q \<or> R)" |
26286 | 805 |
by iprover+ |
806 |
||
807 |
lemma not_simps: |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
808 |
"\<not> (P \<or> Q) \<longleftrightarrow> \<not> P \<and> \<not> Q" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
809 |
"\<not> False \<longleftrightarrow> True" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
810 |
"\<not> True \<longleftrightarrow> False" |
26286 | 811 |
by iprover+ |
812 |
||
813 |
lemma imp_simps: |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
814 |
"(P \<longrightarrow> False) \<longleftrightarrow> \<not> P" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
815 |
"(P \<longrightarrow> True) \<longleftrightarrow> True" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
816 |
"(False \<longrightarrow> P) \<longleftrightarrow> True" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
817 |
"(True \<longrightarrow> P) \<longleftrightarrow> P" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
818 |
"(P \<longrightarrow> P) \<longleftrightarrow> True" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
819 |
"(P \<longrightarrow> \<not> P) \<longleftrightarrow> \<not> P" |
26286 | 820 |
by iprover+ |
821 |
||
822 |
lemma iff_simps: |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
823 |
"(True \<longleftrightarrow> P) \<longleftrightarrow> P" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
824 |
"(P \<longleftrightarrow> True) \<longleftrightarrow> P" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
825 |
"(P \<longleftrightarrow> P) \<longleftrightarrow> True" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
826 |
"(False \<longleftrightarrow> P) \<longleftrightarrow> \<not> P" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
827 |
"(P \<longleftrightarrow> False) \<longleftrightarrow> \<not> P" |
26286 | 828 |
by iprover+ |
829 |
||
62020 | 830 |
text \<open>The \<open>x = t\<close> versions are needed for the simplification |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
831 |
procedures.\<close> |
26286 | 832 |
lemma quant_simps: |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
833 |
"\<And>P. (\<forall>x. P) \<longleftrightarrow> P" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
834 |
"(\<forall>x. x = t \<longrightarrow> P(x)) \<longleftrightarrow> P(t)" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
835 |
"(\<forall>x. t = x \<longrightarrow> P(x)) \<longleftrightarrow> P(t)" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
836 |
"\<And>P. (\<exists>x. P) \<longleftrightarrow> P" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
837 |
"\<exists>x. x = t" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
838 |
"\<exists>x. t = x" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
839 |
"(\<exists>x. x = t \<and> P(x)) \<longleftrightarrow> P(t)" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
840 |
"(\<exists>x. t = x \<and> P(x)) \<longleftrightarrow> P(t)" |
26286 | 841 |
by iprover+ |
842 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
843 |
text \<open>These are NOT supplied by default!\<close> |
26286 | 844 |
lemma distrib_simps: |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
845 |
"P \<and> (Q \<or> R) \<longleftrightarrow> P \<and> Q \<or> P \<and> R" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
846 |
"(Q \<or> R) \<and> P \<longleftrightarrow> Q \<and> P \<or> R \<and> P" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
847 |
"(P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)" |
26286 | 848 |
by iprover+ |
849 |
||
850 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
851 |
subsubsection \<open>Conversion into rewrite rules\<close> |
26286 | 852 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
853 |
lemma P_iff_F: "\<not> P \<Longrightarrow> (P \<longleftrightarrow> False)" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
854 |
by iprover |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
855 |
lemma iff_reflection_F: "\<not> P \<Longrightarrow> (P \<equiv> False)" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
856 |
by (rule P_iff_F [THEN iff_reflection]) |
26286 | 857 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
858 |
lemma P_iff_T: "P \<Longrightarrow> (P \<longleftrightarrow> True)" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
859 |
by iprover |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
860 |
lemma iff_reflection_T: "P \<Longrightarrow> (P \<equiv> True)" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
861 |
by (rule P_iff_T [THEN iff_reflection]) |
26286 | 862 |
|
863 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
864 |
subsubsection \<open>More rewrite rules\<close> |
26286 | 865 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
866 |
lemma conj_commute: "P \<and> Q \<longleftrightarrow> Q \<and> P" by iprover |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
867 |
lemma conj_left_commute: "P \<and> (Q \<and> R) \<longleftrightarrow> Q \<and> (P \<and> R)" by iprover |
26286 | 868 |
lemmas conj_comms = conj_commute conj_left_commute |
869 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
870 |
lemma disj_commute: "P \<or> Q \<longleftrightarrow> Q \<or> P" by iprover |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
871 |
lemma disj_left_commute: "P \<or> (Q \<or> R) \<longleftrightarrow> Q \<or> (P \<or> R)" by iprover |
26286 | 872 |
lemmas disj_comms = disj_commute disj_left_commute |
873 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
874 |
lemma conj_disj_distribL: "P \<and> (Q \<or> R) \<longleftrightarrow> (P \<and> Q \<or> P \<and> R)" by iprover |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
875 |
lemma conj_disj_distribR: "(P \<or> Q) \<and> R \<longleftrightarrow> (P \<and> R \<or> Q \<and> R)" by iprover |
26286 | 876 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
877 |
lemma disj_conj_distribL: "P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)" by iprover |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
878 |
lemma disj_conj_distribR: "(P \<and> Q) \<or> R \<longleftrightarrow> (P \<or> R) \<and> (Q \<or> R)" by iprover |
26286 | 879 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
880 |
lemma imp_conj_distrib: "(P \<longrightarrow> (Q \<and> R)) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)" by iprover |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
881 |
lemma imp_conj: "((P \<and> Q) \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))" by iprover |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
882 |
lemma imp_disj: "(P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)" by iprover |
26286 | 883 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
884 |
lemma de_Morgan_disj: "(\<not> (P \<or> Q)) \<longleftrightarrow> (\<not> P \<and> \<not> Q)" by iprover |
26286 | 885 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
886 |
lemma not_ex: "(\<not> (\<exists>x. P(x))) \<longleftrightarrow> (\<forall>x. \<not> P(x))" by iprover |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
887 |
lemma imp_ex: "((\<exists>x. P(x)) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x) \<longrightarrow> Q)" by iprover |
26286 | 888 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
889 |
lemma ex_disj_distrib: "(\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> ((\<exists>x. P(x)) \<or> (\<exists>x. Q(x)))" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
890 |
by iprover |
26286 | 891 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
892 |
lemma all_conj_distrib: "(\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> ((\<forall>x. P(x)) \<and> (\<forall>x. Q(x)))" |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
61378
diff
changeset
|
893 |
by iprover |
26286 | 894 |
|
4854 | 895 |
end |