12088
|
1 |
(* Title: ZF/ex/PropLog.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow & Lawrence C Paulson
|
|
4 |
Copyright 1993 University of Cambridge
|
|
5 |
|
|
6 |
Datatype definition of propositional logic formulae and inductive definition
|
|
7 |
of the propositional tautologies.
|
|
8 |
*)
|
|
9 |
|
|
10 |
PropLog = Main +
|
|
11 |
|
|
12 |
(** The datatype of propositions; note mixfix syntax **)
|
|
13 |
consts
|
|
14 |
prop :: i
|
|
15 |
|
|
16 |
datatype
|
|
17 |
"prop" = Fls
|
|
18 |
| Var ("n \\<in> nat") ("#_" [100] 100)
|
|
19 |
| "=>" ("p \\<in> prop", "q \\<in> prop") (infixr 90)
|
|
20 |
|
|
21 |
(** The proof system **)
|
|
22 |
consts
|
|
23 |
thms :: i => i
|
|
24 |
|
|
25 |
syntax
|
|
26 |
"|-" :: [i,i] => o (infixl 50)
|
|
27 |
|
|
28 |
translations
|
|
29 |
"H |- p" == "p \\<in> thms(H)"
|
|
30 |
|
|
31 |
inductive
|
|
32 |
domains "thms(H)" <= "prop"
|
|
33 |
intrs
|
|
34 |
H "[| p \\<in> H; p \\<in> prop |] ==> H |- p"
|
|
35 |
K "[| p \\<in> prop; q \\<in> prop |] ==> H |- p=>q=>p"
|
|
36 |
S "[| p \\<in> prop; q \\<in> prop; r \\<in> prop |] ==> H |- (p=>q=>r) => (p=>q) => p=>r"
|
|
37 |
DN "p \\<in> prop ==> H |- ((p=>Fls) => Fls) => p"
|
|
38 |
MP "[| H |- p=>q; H |- p; p \\<in> prop; q \\<in> prop |] ==> H |- q"
|
|
39 |
type_intrs "prop.intrs"
|
|
40 |
|
|
41 |
|
|
42 |
(** The semantics **)
|
|
43 |
consts
|
|
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"
|
|
51 |
|
|
52 |
defs
|
|
53 |
(*Logical consequence: for every valuation, if all elements of H are true
|
|
54 |
then so is p*)
|
|
55 |
logcon_def "H |= p == \\<forall>t. (\\<forall>q \\<in> H. is_true(q,t)) --> is_true(p,t)"
|
|
56 |
|
|
57 |
primrec (** A finite set of hypotheses from t and the Vars in p **)
|
|
58 |
"hyps(Fls, t) = 0"
|
|
59 |
"hyps(Var(v), t) = (if v \\<in> t then {#v} else {#v=>Fls})"
|
|
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"
|
|
64 |
"is_true_fun(Var(v), t) = (if v \\<in> 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)"
|
|
67 |
|
|
68 |
end
|