1 (* Title: ZF/ex/prop-log.thy |
1 (* Title: ZF/ex/PropLog.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow & Lawrence C Paulson |
3 Author: Tobias Nipkow & Lawrence C Paulson |
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 |
5 |
6 Inductive definition of propositional logic. |
6 Datatype definition of propositional logic formulae and inductive definition |
|
7 of the propositional tautologies. |
7 *) |
8 *) |
8 |
9 |
9 PropLog = Prop + Fin + |
10 PropLog = Finite + Univ + |
|
11 |
|
12 (** The datatype of propositions; note mixfix syntax **) |
10 consts |
13 consts |
11 (*semantics*) |
14 prop :: "i" |
12 prop_rec :: "[i, i, i=>i, [i,i,i,i]=>i] => i" |
|
13 is_true :: "[i,i] => o" |
|
14 "|=" :: "[i,i] => o" (infixl 50) |
|
15 hyps :: "[i,i] => i" |
|
16 |
15 |
17 (*proof theory*) |
16 datatype |
|
17 "prop" = Fls |
|
18 | Var ("n: nat") ("#_" [100] 100) |
|
19 | "=>" ("p: prop", "q: prop") (infixr 90) |
|
20 |
|
21 (** The proof system **) |
|
22 consts |
18 thms :: "i => i" |
23 thms :: "i => i" |
19 "|-" :: "[i,i] => o" (infixl 50) |
24 "|-" :: "[i,i] => o" (infixl 50) |
20 |
25 |
21 translations |
26 translations |
22 "H |- p" == "p : thms(H)" |
27 "H |- p" == "p : thms(H)" |
|
28 |
|
29 inductive |
|
30 domains "thms(H)" <= "prop" |
|
31 intrs |
|
32 H "[| p:H; p:prop |] ==> H |- p" |
|
33 K "[| p:prop; q:prop |] ==> H |- p=>q=>p" |
|
34 S "[| p:prop; q:prop; r:prop |] ==> H |- (p=>q=>r) => (p=>q) => p=>r" |
|
35 DN "p:prop ==> H |- ((p=>Fls) => Fls) => p" |
|
36 MP "[| H |- p=>q; H |- p; p:prop; q:prop |] ==> H |- q" |
|
37 type_intrs "prop.intrs" |
|
38 |
|
39 |
|
40 (** The semantics **) |
|
41 consts |
|
42 prop_rec :: "[i, i, i=>i, [i,i,i,i]=>i] => i" |
|
43 is_true :: "[i,i] => o" |
|
44 "|=" :: "[i,i] => o" (infixl 50) |
|
45 hyps :: "[i,i] => i" |
23 |
46 |
24 rules |
47 rules |
25 |
48 |
26 prop_rec_def |
49 prop_rec_def |
27 "prop_rec(p,b,c,h) == \ |
50 "prop_rec(p,b,c,h) == \ |