|
1 (* Title: ZF/ex/prop.ML |
|
2 ID: $Id$ |
|
3 Author: 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 (*Example of a datatype with mixfix syntax for some constructors*) |
|
11 structure Prop = Datatype_Fun |
|
12 (val thy = Univ.thy; |
|
13 val rec_specs = |
|
14 [("prop", "univ(0)", |
|
15 [(["Fls"], "i"), |
|
16 (["Var"], "i=>i"), |
|
17 (["op =>"], "[i,i]=>i")])]; |
|
18 val rec_styp = "i"; |
|
19 val ext = Some (NewSext { |
|
20 mixfix = |
|
21 [Mixfix("#_", "i => i", "Var", [100], 100), |
|
22 Infixr("=>", "[i,i] => i", 90)], |
|
23 xrules = [], |
|
24 parse_ast_translation = [], |
|
25 parse_preproc = None, |
|
26 parse_postproc = None, |
|
27 parse_translation = [], |
|
28 print_translation = [], |
|
29 print_preproc = None, |
|
30 print_postproc = None, |
|
31 print_ast_translation = []}); |
|
32 val sintrs = |
|
33 ["Fls : prop", |
|
34 "n: nat ==> #n : prop", |
|
35 "[| p: prop; q: prop |] ==> p=>q : prop"]; |
|
36 val monos = []; |
|
37 val type_intrs = data_typechecks; |
|
38 val type_elims = []); |
|
39 |
|
40 val [FlsI,VarI,ImpI] = Prop.intrs; |
|
41 |
|
42 |
|
43 (** Type-checking rules **) |
|
44 |
|
45 val ImpE = Prop.mk_cases Prop.con_defs "p=>q : prop"; |
|
46 |
|
47 writeln"Reached end of file."; |