author  wenzelm 
Wed, 05 Dec 2001 03:00:39 +0100  
changeset 12368  2af9ad81ea56 
parent 12352  92c48cc45e78 
child 12662  a9bbba3473f3 
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 
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

46 
"~=" :: "['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) 

57 
"op ~=" :: "['a, 'a] => o" (infixl "\<noteq>" 50) 

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 

12368  126 
subsubsection {* Intuitionistic Reasoning *} 
127 

12349  128 
lemma impE': 
129 
(assumes 1: "P > Q" and 2: "Q ==> R" and 3: "P > Q ==> P") R 

130 
proof  

131 
from 3 and 1 have P . 

12368  132 
with 1 have Q by (rule impE) 
12349  133 
with 2 show R . 
134 
qed 

135 

136 
lemma allE': 

137 
(assumes 1: "ALL x. P(x)" and 2: "P(x) ==> ALL x. P(x) ==> Q") Q 

138 
proof  

139 
from 1 have "P(x)" by (rule spec) 

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

141 
qed 

142 

143 
lemma notE': (assumes 1: "~ P" and 2: "~ P ==> P") R 

144 
proof  

145 
from 2 and 1 have P . 

146 
with 1 show R by (rule notE) 

147 
qed 

148 

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

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

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

152 
and [Pure.intro] = exI disjI2 disjI1 

153 

154 
ML_setup {* 

12352  155 
Context.>> (ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac)); 
12349  156 
*} 
157 

158 

12368  159 
lemma iff_not_sym: "~ (Q <> P) ==> ~ (P <> Q)" 
160 
by rules 

161 

162 
lemmas [sym] = sym iff_sym not_sym iff_not_sym 

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

164 

165 

11677  166 
subsection {* Atomizing metalevel rules *} 
167 

11747  168 
lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))" 
11976  169 
proof 
11677  170 
assume "!!x. P(x)" 
12368  171 
show "ALL x. P(x)" .. 
11677  172 
next 
173 
assume "ALL x. P(x)" 

12368  174 
thus "!!x. P(x)" .. 
11677  175 
qed 
176 

11747  177 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
11976  178 
proof 
12368  179 
assume "A ==> B" 
180 
thus "A > B" .. 

11677  181 
next 
182 
assume "A > B" and A 

183 
thus B by (rule mp) 

184 
qed 

185 

11747  186 
lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)" 
11976  187 
proof 
11677  188 
assume "x == y" 
189 
show "x = y" by (unfold prems) (rule refl) 

190 
next 

191 
assume "x = y" 

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

193 
qed 

194 

11953  195 
lemma atomize_conj [atomize]: "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)" 
11976  196 
proof 
11953  197 
assume "!!C. (A ==> B ==> PROP C) ==> PROP C" 
198 
show "A & B" by (rule conjI) 

199 
next 

200 
fix C 

201 
assume "A & B" 

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

203 
thus "PROP C" 

204 
proof this 

205 
show A by (rule conjunct1) 

206 
show B by (rule conjunct2) 

207 
qed 

208 
qed 

209 

12368  210 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
11771  211 

11848  212 

213 
subsection {* Calculational rules *} 

214 

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

216 
by (rule ssubst) 

217 

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

219 
by (rule subst) 

220 

221 
text {* 

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

223 
*} 

224 

12019  225 
lemmas basic_trans_rules [trans] = 
11848  226 
forw_subst 
227 
back_subst 

228 
rev_mp 

229 
mp 

230 
trans 

231 

4854  232 
end 