1 (* Title: HOL/ex/PropLog.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1994 TU Muenchen |
|
5 |
|
6 Inductive definition of propositional logic. |
|
7 *) |
|
8 |
|
9 PropLog = Finite + |
|
10 datatype |
|
11 'a pl = false | var ('a) ("#_" [1000]) | "->" ('a pl,'a pl) (infixr 90) |
|
12 consts |
|
13 thms :: "'a pl set => 'a pl set" |
|
14 "|-" :: "['a pl set, 'a pl] => bool" (infixl 50) |
|
15 "|=" :: "['a pl set, 'a pl] => bool" (infixl 50) |
|
16 eval2 :: "['a pl, 'a set] => bool" |
|
17 eval :: "['a set, 'a pl] => bool" ("_[_]" [100,0] 100) |
|
18 hyps :: "['a pl, 'a set] => 'a pl set" |
|
19 |
|
20 translations |
|
21 "H |- p" == "p : thms(H)" |
|
22 |
|
23 inductive "thms(H)" |
|
24 intrs |
|
25 H "p:H ==> H |- p" |
|
26 K "H |- p->q->p" |
|
27 S "H |- (p->q->r) -> (p->q) -> p->r" |
|
28 DN "H |- ((p->false) -> false) -> p" |
|
29 MP "[| H |- p->q; H |- p |] ==> H |- q" |
|
30 |
|
31 defs |
|
32 sat_def "H |= p == (!tt. (!q:H. tt[q]) --> tt[p])" |
|
33 eval_def "tt[p] == eval2(p,tt)" |
|
34 |
|
35 primrec eval2 pl |
|
36 eval2_false "eval2(false) = (%x.False)" |
|
37 eval2_var "eval2(#v) = (%tt.v:tt)" |
|
38 eval2_imp "eval2(p->q) = (%tt.eval2(p,tt)-->eval2(q,tt))" |
|
39 |
|
40 primrec hyps pl |
|
41 hyps_false "hyps(false) = (%tt.{})" |
|
42 hyps_var "hyps(#v) = (%tt.{if(v:tt, #v, #v->false)})" |
|
43 hyps_imp "hyps(p->q) = (%tt.hyps(p,tt) Un hyps(q,tt))" |
|
44 |
|
45 end |
|