author | paulson |
Thu, 07 Jan 1999 10:56:05 +0100 | |
changeset 6068 | 2d8f3e1f1151 |
parent 6046 | 2c8a8be36c94 |
child 11316 | b4e71bd751e4 |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/ex/PropLog.thy |
0 | 2 |
ID: $Id$ |
1478 | 3 |
Author: Tobias Nipkow & Lawrence C Paulson |
0 | 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 |
1401 | 14 |
prop :: i |
0 | 15 |
|
515 | 16 |
datatype |
17 |
"prop" = Fls |
|
1478 | 18 |
| Var ("n: nat") ("#_" [100] 100) |
19 |
| "=>" ("p: prop", "q: prop") (infixr 90) |
|
515 | 20 |
|
21 |
(** The proof system **) |
|
22 |
consts |
|
1401 | 23 |
thms :: i => i |
6046 | 24 |
|
25 |
syntax |
|
1478 | 26 |
"|-" :: [i,i] => o (infixl 50) |
0 | 27 |
|
28 |
translations |
|
29 |
"H |- p" == "p : thms(H)" |
|
30 |
||
515 | 31 |
inductive |
32 |
domains "thms(H)" <= "prop" |
|
33 |
intrs |
|
34 |
H "[| p:H; p:prop |] ==> H |- p" |
|
35 |
K "[| p:prop; q:prop |] ==> H |- p=>q=>p" |
|
36 |
S "[| p:prop; q:prop; r:prop |] ==> H |- (p=>q=>r) => (p=>q) => p=>r" |
|
37 |
DN "p:prop ==> H |- ((p=>Fls) => Fls) => p" |
|
38 |
MP "[| H |- p=>q; H |- p; p:prop; q:prop |] ==> H |- q" |
|
39 |
type_intrs "prop.intrs" |
|
40 |
||
41 |
||
42 |
(** The semantics **) |
|
43 |
consts |
|
6046 | 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" |
|
515 | 51 |
|
753 | 52 |
defs |
501
9c724f7085f9
ZF/ex/PropLog/sat_XXX: renamed logcon_XXX, since the relation is logical
lcp
parents:
0
diff
changeset
|
53 |
(*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
|
54 |
then so is p*) |
9c724f7085f9
ZF/ex/PropLog/sat_XXX: renamed logcon_XXX, since the relation is logical
lcp
parents:
0
diff
changeset
|
55 |
logcon_def "H |= p == ALL t. (ALL q:H. is_true(q,t)) --> is_true(p,t)" |
0 | 56 |
|
6046 | 57 |
primrec (** A finite set of hypotheses from t and the Vars in p **) |
58 |
"hyps(Fls, t) = 0" |
|
6068 | 59 |
"hyps(Var(v), t) = (if v:t then {#v} else {#v=>Fls})" |
6046 | 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" |
|
6068 | 64 |
"is_true_fun(Var(v), t) = (if v: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)" |
|
0 | 67 |
|
68 |
end |