author  wenzelm 
Sat, 20 Oct 2001 20:18:45 +0200  
changeset 11848  6e3017adb8c0 
parent 11771  b7b100a2de1d 
child 11953  f98623fdf6ef 
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 

2257  50 
syntax (symbols) 
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 
"op >" :: "[o, o] => o" (infixr "\<midarrow>\<rightarrow>" 25) 

55 
"op <>" :: "[o, o] => o" (infixr "\<leftarrow>\<rightarrow>" 25) 

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

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

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

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

2205  60 

6027
9dd06eeda95c
added new print_mode "xsymbols" for extended symbol support
oheimb
parents:
4854
diff
changeset

61 
syntax (xsymbols) 
11677  62 
"op >" :: "[o, o] => o" (infixr "\<longrightarrow>" 25) 
63 
"op <>" :: "[o, o] => o" (infixr "\<longleftrightarrow>" 25) 

35  64 

6340  65 
syntax (HTML output) 
11677  66 
Not :: "o => o" ("\<not> _" [40] 40) 
6340  67 

68 

3932  69 
local 
3906  70 

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

71 
axioms 
0  72 

79  73 
(* Equality *) 
0  74 

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

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

76 
subst: "[ a=b; P(a) ] ==> P(b)" 
0  77 

79  78 
(* Propositional logic *) 
0  79 

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

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

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

82 
conjunct2: "P&Q ==> Q" 
0  83 

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

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

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

86 
disjE: "[ PQ; P ==> R; Q ==> R ] ==> R" 
0  87 

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

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

89 
mp: "[ P>Q; P ] ==> Q" 
0  90 

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

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

92 

0  93 

79  94 
(* Definitions *) 
0  95 

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

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

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

98 
iff_def: "P<>Q == (P>Q) & (Q>P)" 
79  99 

100 
(* Unique existence *) 

0  101 

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

102 
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

103 

0  104 

79  105 
(* Quantifiers *) 
0  106 

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

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

108 
spec: "(ALL x. P(x)) ==> P(x)" 
0  109 

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

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

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

113 
(* Reflection *) 

114 

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

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

116 
iff_reflection: "(P<>Q) ==> (P==Q)" 
0  117 

4092  118 

11677  119 
subsection {* Lemmas and proof tools *} 
120 

9886  121 
setup Simplifier.setup 
122 
use "IFOL_lemmas.ML" 

11734  123 

124 
declare impE [Pure.elim] iffD1 [Pure.elim] iffD2 [Pure.elim] 

125 

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

126 
use "fologic.ML" 
9886  127 
use "hypsubstdata.ML" 
128 
setup hypsubst_setup 

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

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

130 

4092  131 

11677  132 
subsection {* Atomizing metalevel rules *} 
133 

11747  134 
lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))" 
11677  135 
proof (rule equal_intr_rule) 
136 
assume "!!x. P(x)" 

137 
show "ALL x. P(x)" by (rule allI) 

138 
next 

139 
assume "ALL x. P(x)" 

140 
thus "!!x. P(x)" by (rule allE) 

141 
qed 

142 

11747  143 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
11677  144 
proof (rule equal_intr_rule) 
145 
assume r: "A ==> B" 

146 
show "A > B" by (rule impI) (rule r) 

147 
next 

148 
assume "A > B" and A 

149 
thus B by (rule mp) 

150 
qed 

151 

11747  152 
lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)" 
11677  153 
proof (rule equal_intr_rule) 
154 
assume "x == y" 

155 
show "x = y" by (unfold prems) (rule refl) 

156 
next 

157 
assume "x = y" 

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

159 
qed 

160 

11771  161 
declare atomize_all [symmetric, rulify] atomize_imp [symmetric, rulify] 
162 

11848  163 

164 
subsection {* Calculational rules *} 

165 

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

167 
by (rule ssubst) 

168 

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

170 
by (rule subst) 

171 

172 
text {* 

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

174 
*} 

175 

176 
lemmas trans_rules [trans] = 

177 
forw_subst 

178 
back_subst 

179 
rev_mp 

180 
mp 

181 
transitive 

182 
trans 

183 

184 
lemmas [Pure.elim] = sym 

185 

4854  186 
end 