equal
deleted
inserted
replaced
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 |
|
18 eval :: ['a set, 'a pl] => bool ("_[[_]]" [100,0] 100) |
17 eval :: ['a set, 'a pl] => bool ("_[[_]]" [100,0] 100) |
19 hyps :: ['a pl, 'a set] => 'a pl set |
18 hyps :: ['a pl, 'a set] => 'a pl set |
20 |
19 |
21 translations |
20 translations |
22 "H |- p" == "p : thms(H)" |
21 "H |- p" == "p : thms(H)" |
29 DN "H |- ((p->false) -> false) -> p" |
28 DN "H |- ((p->false) -> false) -> p" |
30 MP "[| H |- p->q; H |- p |] ==> H |- q" |
29 MP "[| H |- p->q; H |- p |] ==> H |- q" |
31 |
30 |
32 defs |
31 defs |
33 sat_def "H |= p == (!tt. (!q:H. tt[[q]]) --> tt[[p]])" |
32 sat_def "H |= p == (!tt. (!q:H. tt[[q]]) --> tt[[p]])" |
34 eval_def "tt[[p]] == eval2 p tt" |
|
35 |
33 |
36 primrec |
34 primrec |
37 "eval2(false) = (%x. False)" |
35 "tt[[false]] = False" |
38 "eval2(#v) = (%tt. v:tt)" |
36 "tt[[#v]] = (v:tt)" |
39 "eval2(p->q) = (%tt. eval2 p tt-->eval2 q tt)" |
37 eval_imp "tt[[p->q]] = (tt[[p]] --> tt[[q]])" |
40 |
38 |
41 primrec |
39 primrec |
42 "hyps(false) = (%tt.{})" |
40 "hyps false tt = {}" |
43 "hyps(#v) = (%tt.{if v:tt then #v else #v->false})" |
41 "hyps (#v) tt = {if v:tt then #v else #v->false}" |
44 "hyps(p->q) = (%tt. hyps p tt Un hyps q tt)" |
42 "hyps (p->q) tt = hyps p tt Un hyps q tt" |
45 |
43 |
46 end |
44 end |
47 |
45 |