author | lcp |
Fri, 29 Jul 1994 16:07:22 +0200 | |
changeset 501 | 9c724f7085f9 |
parent 0 | a5a9c433f639 |
child 515 | abcc438e7c27 |
permissions | -rw-r--r-- |
0 | 1 |
(* Title: ZF/ex/prop-log.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow & Lawrence C Paulson |
|
4 |
Copyright 1993 University of Cambridge |
|
5 |
||
6 |
Inductive definition of propositional logic. |
|
7 |
*) |
|
8 |
||
9 |
PropLog = Prop + Fin + |
|
10 |
consts |
|
11 |
(*semantics*) |
|
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 |
||
17 |
(*proof theory*) |
|
18 |
thms :: "i => i" |
|
19 |
"|-" :: "[i,i] => o" (infixl 50) |
|
20 |
||
21 |
translations |
|
22 |
"H |- p" == "p : thms(H)" |
|
23 |
||
24 |
rules |
|
25 |
||
26 |
prop_rec_def |
|
27 |
"prop_rec(p,b,c,h) == \ |
|
28 |
\ Vrec(p, %p g.prop_case(b, c, %x y. h(x, y, g`x, g`y), p))" |
|
29 |
||
30 |
(** Semantics of propositional logic **) |
|
31 |
is_true_def |
|
32 |
"is_true(p,t) == prop_rec(p, 0, %v. if(v:t, 1, 0), \ |
|
33 |
\ %p q tp tq. if(tp=1,tq,1)) = 1" |
|
34 |
||
501
9c724f7085f9
ZF/ex/PropLog/sat_XXX: renamed logcon_XXX, since the relation is logical
lcp
parents:
0
diff
changeset
|
35 |
(*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
|
36 |
then so is p*) |
9c724f7085f9
ZF/ex/PropLog/sat_XXX: renamed logcon_XXX, since the relation is logical
lcp
parents:
0
diff
changeset
|
37 |
logcon_def "H |= p == ALL t. (ALL q:H. is_true(q,t)) --> is_true(p,t)" |
0 | 38 |
|
39 |
(** A finite set of hypotheses from t and the Vars in p **) |
|
40 |
hyps_def |
|
41 |
"hyps(p,t) == prop_rec(p, 0, %v. {if(v:t, #v, #v=>Fls)}, \ |
|
42 |
\ %p q Hp Hq. Hp Un Hq)" |
|
43 |
||
44 |
end |