1274
|
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);
|
2719
|
36 |
val Not = Const("Not",boolT --> boolT);
|
1274
|
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
|
1284
|
54 |
| mkOpApp f x = (error("Internal error: mkOpApp: wrong args"));
|
1274
|
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;
|