1 (* Title: HOL/ex/PropLog.thy |
1 (* Title: HOL/ex/PropLog.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
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 + |
9 PropLog = Finite + |
10 datatype |
10 datatype |
11 'a pl = false | var 'a ("#_" [1000]) | "->" ('a pl) ('a pl) (infixr 90) |
11 'a pl = false | var 'a ("#_" [1000]) | "->" ('a pl) ('a pl) (infixr 90) |
12 consts |
12 consts |
13 thms :: 'a pl set => 'a pl set |
13 thms :: 'a pl set => 'a pl set |
14 "|-" :: ['a pl set, 'a pl] => bool (infixl 50) |
14 "|-" :: ['a pl set, 'a pl] => bool (infixl 50) |
15 "|=" :: ['a pl set, 'a pl] => bool (infixl 50) |
15 "|=" :: ['a pl set, 'a pl] => bool (infixl 50) |
16 eval2 :: ['a pl, 'a set] => bool |
16 eval2 :: ['a pl, 'a set] => bool |
17 eval :: ['a set, 'a pl] => bool ("_[_]" [100,0] 100) |
17 eval :: ['a set, 'a pl] => bool ("_[_]" [100,0] 100) |
18 hyps :: ['a pl, 'a set] => 'a pl set |
18 hyps :: ['a pl, 'a set] => 'a pl set |
19 |
19 |
20 translations |
20 translations |
21 "H |- p" == "p : thms(H)" |
21 "H |- p" == "p : thms(H)" |
22 |
22 |
23 inductive "thms(H)" |
23 inductive "thms(H)" |