author | lcp |
Tue, 07 Mar 1995 13:37:48 +0100 | |
changeset 935 | a94ef3eed456 |
parent 753 | ec86863e87c8 |
child 1155 | 928a16e02f9f |
permissions | -rw-r--r-- |
515 | 1 |
(* Title: ZF/ex/PropLog.thy |
0 | 2 |
ID: $Id$ |
3 |
Author: Tobias Nipkow & Lawrence C Paulson |
|
4 |
Copyright 1993 University of Cambridge |
|
5 |
||
515 | 6 |
Datatype definition of propositional logic formulae and inductive definition |
7 |
of the propositional tautologies. |
|
0 | 8 |
*) |
9 |
||
935 | 10 |
PropLog = Finite + Datatype + |
515 | 11 |
|
12 |
(** The datatype of propositions; note mixfix syntax **) |
|
0 | 13 |
consts |
515 | 14 |
prop :: "i" |
0 | 15 |
|
515 | 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 |
|
0 | 23 |
thms :: "i => i" |
24 |
"|-" :: "[i,i] => o" (infixl 50) |
|
25 |
||
26 |
translations |
|
27 |
"H |- p" == "p : thms(H)" |
|
28 |
||
515 | 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" |
|
46 |
||
753 | 47 |
defs |
0 | 48 |
|
49 |
prop_rec_def |
|
50 |
"prop_rec(p,b,c,h) == \ |
|
51 |
\ Vrec(p, %p g.prop_case(b, c, %x y. h(x, y, g`x, g`y), p))" |
|
52 |
||
53 |
(** Semantics of propositional logic **) |
|
54 |
is_true_def |
|
55 |
"is_true(p,t) == prop_rec(p, 0, %v. if(v:t, 1, 0), \ |
|
56 |
\ %p q tp tq. if(tp=1,tq,1)) = 1" |
|
57 |
||
501
9c724f7085f9
ZF/ex/PropLog/sat_XXX: renamed logcon_XXX, since the relation is logical
lcp
parents:
0
diff
changeset
|
58 |
(*Logical consequence: for every valuation, if all elements of H are true |
9c724f7085f9
ZF/ex/PropLog/sat_XXX: renamed logcon_XXX, since the relation is logical
lcp
parents:
0
diff
changeset
|
59 |
then so is p*) |
9c724f7085f9
ZF/ex/PropLog/sat_XXX: renamed logcon_XXX, since the relation is logical
lcp
parents:
0
diff
changeset
|
60 |
logcon_def "H |= p == ALL t. (ALL q:H. is_true(q,t)) --> is_true(p,t)" |
0 | 61 |
|
62 |
(** A finite set of hypotheses from t and the Vars in p **) |
|
63 |
hyps_def |
|
64 |
"hyps(p,t) == prop_rec(p, 0, %v. {if(v:t, #v, #v=>Fls)}, \ |
|
65 |
\ %p q Hp Hq. Hp Un Hq)" |
|
66 |
||
67 |
end |