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 |
|
|
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
|