author  wenzelm 
Sun, 15 Oct 2000 19:50:35 +0200  
changeset 10220  2a726de6e124 
parent 9886  897d6602cbfb 
child 11677  ee12f18599e5 
permissions  rwrr 
1268  1 
(* Title: FOL/IFOL.thy 
35  2 
ID: $Id$ 
79  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
35  4 
Copyright 1993 University of Cambridge 
5 

2205  6 
Intuitionistic firstorder logic. 
35  7 
*) 
8 

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

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

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

11 

0  12 

3906  13 
global 
14 

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

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

16 
defaultsort "term" 
0  17 

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

18 
typedecl o 
79  19 

20 
consts 

0  21 

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

22 
Trueprop :: "o => prop" ("(_)" 5) 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

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

24 
False :: o 
79  25 

26 
(* Connectives *) 

27 

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

28 
"=" :: "['a, 'a] => o" (infixl 50) 
35  29 

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

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

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

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

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

34 
<> :: "[o, o] => o" (infixr 25) 
79  35 

36 
(* Quantifiers *) 

37 

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

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

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

40 
Ex1 :: "('a => o) => o" (binder "EX! " 10) 
79  41 

0  42 

2257  43 

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

45 
"~=" :: "['a, 'a] => o" (infixl 50) 
928  46 

35  47 
translations 
79  48 
"x ~= y" == "~ (x = y)" 
49 

2257  50 
syntax (symbols) 
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

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

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

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

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

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

56 
"ALL " :: "[idts, o] => o" ("(3\\<forall>_./ _)" [0, 10] 10) 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

57 
"EX " :: "[idts, o] => o" ("(3\\<exists>_./ _)" [0, 10] 10) 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

58 
"EX! " :: "[idts, o] => o" ("(3\\<exists>!_./ _)" [0, 10] 10) 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

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) 
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

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

63 
"op <>" :: "[o, o] => o" (infixr "\\<longleftrightarrow>" 25) 
35  64 

6340  65 
syntax (HTML output) 
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

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 

9886  119 
setup Simplifier.setup 
120 
use "IFOL_lemmas.ML" 

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

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

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

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

125 

4092  126 

4854  127 
end 