|
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 |
|
35 (*For every valuation, if all elements of H are true then so is p*) |
|
36 sat_def "H |= p == ALL t. (ALL q:H. is_true(q,t)) --> is_true(p,t)" |
|
37 |
|
38 (** A finite set of hypotheses from t and the Vars in p **) |
|
39 hyps_def |
|
40 "hyps(p,t) == prop_rec(p, 0, %v. {if(v:t, #v, #v=>Fls)}, \ |
|
41 \ %p q Hp Hq. Hp Un Hq)" |
|
42 |
|
43 end |