|
1 (* |
|
2 ID: $Id$ |
|
3 Author: Tobias Mayr |
|
4 |
|
5 Additional term and type constructors, extension of Pure/term.ML, logic.ML |
|
6 and HOL/hologic.ML |
|
7 |
|
8 TODO: |
|
9 |
|
10 *) |
|
11 |
|
12 signature HOLCFLOGIC = |
|
13 sig |
|
14 val True : term; |
|
15 val False : term; |
|
16 val Imp : term; |
|
17 val And : term; |
|
18 val Not : term; |
|
19 val mkNot : term -> term; (* negates, no Trueprop *) |
|
20 val mkNotEqUU : term -> term; (* Trueprop(x ~= UU) *) |
|
21 val mkNotEqUU_in : term -> term -> term; (* "v~=UU ==> t" *) |
|
22 val ==> : typ * typ -> typ; (* Infix operation typ constructor *) |
|
23 val mkOpApp : term -> term -> term; (* Ops application (f ` x) *) |
|
24 val mkCPair : term -> term -> term; (* cpair constructor *) |
|
25 end; |
|
26 |
|
27 structure HOLCFlogic : HOLCFLOGIC = |
|
28 struct |
|
29 open Logic |
|
30 open HOLogic |
|
31 |
|
32 val True = Const("True",boolT); |
|
33 val False = Const("False",boolT); |
|
34 val Imp = Const("op -->",boolT --> boolT --> boolT); |
|
35 val And = Const("op &",boolT --> boolT --> boolT); |
|
36 val Not = Const("not",boolT --> boolT); |
|
37 |
|
38 fun mkNot A = Not $ A; (* negates, no Trueprop *) |
|
39 |
|
40 (* Trueprop(x ~= UU) *) |
|
41 fun mkNotEqUU v = mk_Trueprop(mkNot(mk_eq(v,Const("UU",fastype_of v)))); |
|
42 |
|
43 (* mkNotEqUU_in v t = "v~=UU ==> t" *) |
|
44 fun mkNotEqUU_in vterm term = |
|
45 mk_implies(mkNotEqUU vterm,term) |
|
46 |
|
47 |
|
48 infixr 6 ==>; (* the analogon to --> for operations *) |
|
49 fun a ==> b = Type("->",[a,b]); |
|
50 |
|
51 (* Ops application (f ` x) *) |
|
52 fun mkOpApp (f as Const(_,ft as Type("->",[xt,rt]))) x = |
|
53 Const("fapp",ft --> xt --> rt) $ f $ x |
|
54 | mkOpApp f x = (print(f);error("Internal error: mkOpApp: wrong args")); |
|
55 |
|
56 (* cpair constructor *) |
|
57 fun mkCPair x y = let val tx = fastype_of x |
|
58 val ty = fastype_of y |
|
59 in |
|
60 Const("fapp",(ty==>Type("*",[tx,ty]))-->ty-->Type("*",[tx,ty])) $ |
|
61 (mkOpApp (Const("cpair",tx ==> ty ==> Type("*",[tx,ty]))) x) $ y |
|
62 end; |
|
63 |
|
64 end; |