author  wenzelm 
Mon, 25 Feb 2002 20:48:14 +0100  
changeset 12937  0c4fd7529467 
parent 12875  bda60442bf02 
child 13435  05631e8f0258 
permissions  rwrr 
1268  1 
(* Title: FOL/IFOL.thy 
35  2 
ID: $Id$ 
11677  3 
Author: Lawrence C Paulson and Markus Wenzel 
4 
*) 

35  5 

11677  6 
header {* Intuitionistic firstorder logic *} 
35  7 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

8 
theory IFOL = Pure 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

9 
files ("IFOL_lemmas.ML") ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML"): 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

10 

0  11 

11677  12 
subsection {* Syntax and axiomatic basis *} 
13 

3906  14 
global 
15 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

16 
classes "term" < logic 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

17 
defaultsort "term" 
0  18 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

19 
typedecl o 
79  20 

11747  21 
judgment 
22 
Trueprop :: "o => prop" ("(_)" 5) 

0  23 

11747  24 
consts 
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

25 
True :: o 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

26 
False :: o 
79  27 

28 
(* Connectives *) 

29 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

30 
"=" :: "['a, 'a] => o" (infixl 50) 
35  31 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

32 
Not :: "o => o" ("~ _" [40] 40) 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

33 
& :: "[o, o] => o" (infixr 35) 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

34 
"" :: "[o, o] => o" (infixr 30) 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

35 
> :: "[o, o] => o" (infixr 25) 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

36 
<> :: "[o, o] => o" (infixr 25) 
79  37 

38 
(* Quantifiers *) 

39 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

40 
All :: "('a => o) => o" (binder "ALL " 10) 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

41 
Ex :: "('a => o) => o" (binder "EX " 10) 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

42 
Ex1 :: "('a => o) => o" (binder "EX! " 10) 
79  43 

0  44 

928  45 
syntax 
12662  46 
"_not_equal" :: "['a, 'a] => o" (infixl "~=" 50) 
35  47 
translations 
79  48 
"x ~= y" == "~ (x = y)" 
49 

12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
12019
diff
changeset

50 
syntax (xsymbols) 
11677  51 
Not :: "o => o" ("\<not> _" [40] 40) 
52 
"op &" :: "[o, o] => o" (infixr "\<and>" 35) 

53 
"op " :: "[o, o] => o" (infixr "\<or>" 30) 

54 
"ALL " :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10) 

55 
"EX " :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10) 

56 
"EX! " :: "[idts, o] => o" ("(3\<exists>!_./ _)" [0, 10] 10) 

12662  57 
"_not_equal" :: "['a, 'a] => o" (infixl "\<noteq>" 50) 
11677  58 
"op >" :: "[o, o] => o" (infixr "\<longrightarrow>" 25) 
59 
"op <>" :: "[o, o] => o" (infixr "\<longleftrightarrow>" 25) 

35  60 

6340  61 
syntax (HTML output) 
11677  62 
Not :: "o => o" ("\<not> _" [40] 40) 
6340  63 

64 

3932  65 
local 
3906  66 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

67 
axioms 
0  68 

79  69 
(* Equality *) 
0  70 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

71 
refl: "a=a" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

72 
subst: "[ a=b; P(a) ] ==> P(b)" 
0  73 

79  74 
(* Propositional logic *) 
0  75 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

76 
conjI: "[ P; Q ] ==> P&Q" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

77 
conjunct1: "P&Q ==> P" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

78 
conjunct2: "P&Q ==> Q" 
0  79 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

80 
disjI1: "P ==> PQ" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

81 
disjI2: "Q ==> PQ" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

82 
disjE: "[ PQ; P ==> R; Q ==> R ] ==> R" 
0  83 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

84 
impI: "(P ==> Q) ==> P>Q" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

85 
mp: "[ P>Q; P ] ==> Q" 
0  86 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

87 
FalseE: "False ==> P" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

88 

0  89 

79  90 
(* Definitions *) 
0  91 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

92 
True_def: "True == False>False" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

93 
not_def: "~P == P>False" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

94 
iff_def: "P<>Q == (P>Q) & (Q>P)" 
79  95 

96 
(* Unique existence *) 

0  97 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

98 
ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) > y=x)" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

99 

0  100 

79  101 
(* Quantifiers *) 
0  102 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

103 
allI: "(!!x. P(x)) ==> (ALL x. P(x))" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

104 
spec: "(ALL x. P(x)) ==> P(x)" 
0  105 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

106 
exI: "P(x) ==> (EX x. P(x))" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

107 
exE: "[ EX x. P(x); !!x. P(x) ==> R ] ==> R" 
0  108 

109 
(* Reflection *) 

110 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

111 
eq_reflection: "(x=y) ==> (x==y)" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

112 
iff_reflection: "(P<>Q) ==> (P==Q)" 
0  113 

4092  114 

11677  115 
subsection {* Lemmas and proof tools *} 
116 

9886  117 
setup Simplifier.setup 
118 
use "IFOL_lemmas.ML" 

11734  119 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

120 
use "fologic.ML" 
9886  121 
use "hypsubstdata.ML" 
122 
setup hypsubst_setup 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

123 
use "intprover.ML" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

124 

4092  125 

12875  126 
subsection {* Intuitionistic Reasoning *} 
12368  127 

12349  128 
lemma impE': 
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

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

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

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

132 
shows R 
12349  133 
proof  
134 
from 3 and 1 have P . 

12368  135 
with 1 have Q by (rule impE) 
12349  136 
with 2 show R . 
137 
qed 

138 

139 
lemma allE': 

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

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

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

142 
shows Q 
12349  143 
proof  
144 
from 1 have "P(x)" by (rule spec) 

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

146 
qed 

147 

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

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

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

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

151 
shows R 
12349  152 
proof  
153 
from 2 and 1 have P . 

154 
with 1 show R by (rule notE) 

155 
qed 

156 

157 
lemmas [Pure.elim!] = disjE iffE FalseE conjE exE 

158 
and [Pure.intro!] = iffI conjI impI TrueI notI allI refl 

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

160 
and [Pure.intro] = exI disjI2 disjI1 

161 

162 
ML_setup {* 

12352  163 
Context.>> (ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac)); 
12349  164 
*} 
165 

166 

12368  167 
lemma iff_not_sym: "~ (Q <> P) ==> ~ (P <> Q)" 
168 
by rules 

169 

170 
lemmas [sym] = sym iff_sym not_sym iff_not_sym 

171 
and [Pure.elim?] = iffD1 iffD2 impE 

172 

173 

11677  174 
subsection {* Atomizing metalevel rules *} 
175 

11747  176 
lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))" 
11976  177 
proof 
11677  178 
assume "!!x. P(x)" 
12368  179 
show "ALL x. P(x)" .. 
11677  180 
next 
181 
assume "ALL x. P(x)" 

12368  182 
thus "!!x. P(x)" .. 
11677  183 
qed 
184 

11747  185 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
11976  186 
proof 
12368  187 
assume "A ==> B" 
188 
thus "A > B" .. 

11677  189 
next 
190 
assume "A > B" and A 

191 
thus B by (rule mp) 

192 
qed 

193 

11747  194 
lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)" 
11976  195 
proof 
11677  196 
assume "x == y" 
197 
show "x = y" by (unfold prems) (rule refl) 

198 
next 

199 
assume "x = y" 

200 
thus "x == y" by (rule eq_reflection) 

201 
qed 

202 

12875  203 
lemma atomize_conj [atomize]: 
204 
"(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)" 

11976  205 
proof 
11953  206 
assume "!!C. (A ==> B ==> PROP C) ==> PROP C" 
207 
show "A & B" by (rule conjI) 

208 
next 

209 
fix C 

210 
assume "A & B" 

211 
assume "A ==> B ==> PROP C" 

212 
thus "PROP C" 

213 
proof this 

214 
show A by (rule conjunct1) 

215 
show B by (rule conjunct2) 

216 
qed 

217 
qed 

218 

12368  219 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
11771  220 

11848  221 

222 
subsection {* Calculational rules *} 

223 

224 
lemma forw_subst: "a = b ==> P(b) ==> P(a)" 

225 
by (rule ssubst) 

226 

227 
lemma back_subst: "P(a) ==> a = b ==> P(b)" 

228 
by (rule subst) 

229 

230 
text {* 

231 
Note that this list of rules is in reverse order of priorities. 

232 
*} 

233 

12019  234 
lemmas basic_trans_rules [trans] = 
11848  235 
forw_subst 
236 
back_subst 

237 
rev_mp 

238 
mp 

239 
trans 

240 

4854  241 
end 