equal
deleted
inserted
replaced
26 |
26 |
27 (*** Logical Connectives -- Type Formers ***) |
27 (*** Logical Connectives -- Type Formers ***) |
28 eq :: "['a,'a] => o" (infixl "=" 50) |
28 eq :: "['a,'a] => o" (infixl "=" 50) |
29 True :: "o" |
29 True :: "o" |
30 False :: "o" |
30 False :: "o" |
31 Not :: "o => o" ("~ _" [40] 40) |
|
32 conj :: "[o,o] => o" (infixr "&" 35) |
31 conj :: "[o,o] => o" (infixr "&" 35) |
33 disj :: "[o,o] => o" (infixr "|" 30) |
32 disj :: "[o,o] => o" (infixr "|" 30) |
34 imp :: "[o,o] => o" (infixr "-->" 25) |
33 imp :: "[o,o] => o" (infixr "-->" 25) |
35 iff :: "[o,o] => o" (infixr "<->" 25) |
|
36 (*Quantifiers*) |
34 (*Quantifiers*) |
37 All :: "('a => o) => o" (binder "ALL " 10) |
35 All :: "('a => o) => o" (binder "ALL " 10) |
38 Ex :: "('a => o) => o" (binder "EX " 10) |
36 Ex :: "('a => o) => o" (binder "EX " 10) |
39 Ex1 :: "('a => o) => o" (binder "EX! " 10) |
|
40 (*Rewriting gadgets*) |
37 (*Rewriting gadgets*) |
41 NORM :: "o => o" |
38 NORM :: "o => o" |
42 norm :: "'a => 'a" |
39 norm :: "'a => 'a" |
43 |
40 |
44 (*** Proof Term Formers: precedence must exceed 50 ***) |
41 (*** Proof Term Formers: precedence must exceed 50 ***) |
155 specB: "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)" |
152 specB: "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)" |
156 |
153 |
157 |
154 |
158 (**** Definitions ****) |
155 (**** Definitions ****) |
159 |
156 |
160 defs |
157 definition Not :: "o => o" ("~ _" [40] 40) |
161 not_def: "~P == P-->False" |
158 where not_def: "~P == P-->False" |
162 iff_def: "P<->Q == (P-->Q) & (Q-->P)" |
159 |
|
160 definition iff :: "[o,o] => o" (infixr "<->" 25) |
|
161 where "P<->Q == (P-->Q) & (Q-->P)" |
163 |
162 |
164 (*Unique existence*) |
163 (*Unique existence*) |
165 ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)" |
164 definition Ex1 :: "('a => o) => o" (binder "EX! " 10) |
|
165 where ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)" |
166 |
166 |
167 (*Rewriting -- special constants to flag normalized terms and formulae*) |
167 (*Rewriting -- special constants to flag normalized terms and formulae*) |
168 axiomatization where |
168 axiomatization where |
169 norm_eq: "nrm : norm(x) = x" and |
169 norm_eq: "nrm : norm(x) = x" and |
170 NORM_iff: "NRM : NORM(P) <-> P" |
170 NORM_iff: "NRM : NORM(P) <-> P" |