equal
deleted
inserted
replaced
4 Copyright 1994 TU Muenchen |
4 Copyright 1994 TU Muenchen |
5 |
5 |
6 Inductive definition of propositional logic. |
6 Inductive definition of propositional logic. |
7 *) |
7 *) |
8 |
8 |
9 PropLog = Finite + Datatype + |
9 PropLog = Main + |
10 |
10 |
11 datatype |
11 datatype |
12 'a pl = false | var 'a ("#_" [1000]) | "->" ('a pl) ('a pl) (infixr 90) |
12 'a pl = false | var 'a ("#_" [1000]) | "->" ('a pl) ('a pl) (infixr 90) |
13 consts |
13 consts |
14 thms :: 'a pl set => 'a pl set |
14 thms :: 'a pl set => 'a pl set |
15 "|-" :: ['a pl set, 'a pl] => bool (infixl 50) |
15 "|-" :: ['a pl set, 'a pl] => bool (infixl 50) |
16 "|=" :: ['a pl set, 'a pl] => bool (infixl 50) |
16 "|=" :: ['a pl set, 'a pl] => bool (infixl 50) |
17 eval2 :: ['a pl, 'a set] => bool |
17 eval2 :: ['a pl, 'a set] => bool |
18 eval :: ['a set, 'a pl] => bool ("_[_]" [100,0] 100) |
18 eval :: ['a set, 'a pl] => bool ("_[[_]]" [100,0] 100) |
19 hyps :: ['a pl, 'a set] => 'a pl set |
19 hyps :: ['a pl, 'a set] => 'a pl set |
20 |
20 |
21 translations |
21 translations |
22 "H |- p" == "p : thms(H)" |
22 "H |- p" == "p : thms(H)" |
23 |
23 |
28 S "H |- (p->q->r) -> (p->q) -> p->r" |
28 S "H |- (p->q->r) -> (p->q) -> p->r" |
29 DN "H |- ((p->false) -> false) -> p" |
29 DN "H |- ((p->false) -> false) -> p" |
30 MP "[| H |- p->q; H |- p |] ==> H |- q" |
30 MP "[| H |- p->q; H |- p |] ==> H |- q" |
31 |
31 |
32 defs |
32 defs |
33 sat_def "H |= p == (!tt. (!q:H. tt[q]) --> tt[p])" |
33 sat_def "H |= p == (!tt. (!q:H. tt[[q]]) --> tt[[p]])" |
34 eval_def "tt[p] == eval2 p tt" |
34 eval_def "tt[[p]] == eval2 p tt" |
35 |
35 |
36 primrec |
36 primrec |
37 "eval2(false) = (%x. False)" |
37 "eval2(false) = (%x. False)" |
38 "eval2(#v) = (%tt. v:tt)" |
38 "eval2(#v) = (%tt. v:tt)" |
39 "eval2(p->q) = (%tt. eval2 p tt-->eval2 q tt)" |
39 "eval2(p->q) = (%tt. eval2 p tt-->eval2 q tt)" |