1 (* Title: ZF/ex/PropLog.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow & Lawrence C Paulson |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Datatype definition of propositional logic formulae and inductive definition |
|
7 of the propositional tautologies. |
|
8 *) |
|
9 |
|
10 PropLog = Main + |
|
11 |
|
12 (** The datatype of propositions; note mixfix syntax **) |
|
13 consts |
|
14 prop :: i |
|
15 |
|
16 datatype |
|
17 "prop" = Fls |
|
18 | Var ("n \\<in> nat") ("#_" [100] 100) |
|
19 | "=>" ("p \\<in> prop", "q \\<in> prop") (infixr 90) |
|
20 |
|
21 (** The proof system **) |
|
22 consts |
|
23 thms :: i => i |
|
24 |
|
25 syntax |
|
26 "|-" :: [i,i] => o (infixl 50) |
|
27 |
|
28 translations |
|
29 "H |- p" == "p \\<in> thms(H)" |
|
30 |
|
31 inductive |
|
32 domains "thms(H)" <= "prop" |
|
33 intrs |
|
34 H "[| p \\<in> H; p \\<in> prop |] ==> H |- p" |
|
35 K "[| p \\<in> prop; q \\<in> prop |] ==> H |- p=>q=>p" |
|
36 S "[| p \\<in> prop; q \\<in> prop; r \\<in> prop |] ==> H |- (p=>q=>r) => (p=>q) => p=>r" |
|
37 DN "p \\<in> prop ==> H |- ((p=>Fls) => Fls) => p" |
|
38 MP "[| H |- p=>q; H |- p; p \\<in> prop; q \\<in> prop |] ==> H |- q" |
|
39 type_intrs "prop.intrs" |
|
40 |
|
41 |
|
42 (** The semantics **) |
|
43 consts |
|
44 "|=" :: [i,i] => o (infixl 50) |
|
45 hyps :: [i,i] => i |
|
46 is_true_fun :: [i,i] => i |
|
47 |
|
48 constdefs (*this definitionis necessary since predicates can't be recursive*) |
|
49 is_true :: [i,i] => o |
|
50 "is_true(p,t) == is_true_fun(p,t)=1" |
|
51 |
|
52 defs |
|
53 (*Logical consequence: for every valuation, if all elements of H are true |
|
54 then so is p*) |
|
55 logcon_def "H |= p == \\<forall>t. (\\<forall>q \\<in> H. is_true(q,t)) --> is_true(p,t)" |
|
56 |
|
57 primrec (** A finite set of hypotheses from t and the Vars in p **) |
|
58 "hyps(Fls, t) = 0" |
|
59 "hyps(Var(v), t) = (if v \\<in> t then {#v} else {#v=>Fls})" |
|
60 "hyps(p=>q, t) = hyps(p,t) Un hyps(q,t)" |
|
61 |
|
62 primrec (** Semantics of propositional logic **) |
|
63 "is_true_fun(Fls, t) = 0" |
|
64 "is_true_fun(Var(v), t) = (if v \\<in> t then 1 else 0)" |
|
65 "is_true_fun(p=>q, t) = (if is_true_fun(p,t)=1 then is_true_fun(q,t) |
|
66 else 1)" |
|
67 |
|
68 end |
|