18 val Not : term; |
18 val Not : term; |
19 val mkNot : term -> term; (* negates, no Trueprop *) |
19 val mkNot : term -> term; (* negates, no Trueprop *) |
20 val mkNotEqUU : term -> term; (* Trueprop(x ~= UU) *) |
20 val mkNotEqUU : term -> term; (* Trueprop(x ~= UU) *) |
21 val mkNotEqUU_in : term -> term -> term; (* "v~=UU ==> t" *) |
21 val mkNotEqUU_in : term -> term -> term; (* "v~=UU ==> t" *) |
22 val ==> : typ * typ -> typ; (* Infix operation typ constructor *) |
22 val ==> : typ * typ -> typ; (* Infix operation typ constructor *) |
|
23 val cfun_arrow : string (* internalized "->" *) |
23 val mkOpApp : term -> term -> term; (* Ops application (f ` x) *) |
24 val mkOpApp : term -> term -> term; (* Ops application (f ` x) *) |
24 val mkCPair : term -> term -> term; (* cpair constructor *) |
25 val mkCPair : term -> term -> term; (* cpair constructor *) |
25 end; |
26 end; |
26 |
27 |
27 structure HOLCFlogic : HOLCFLOGIC = |
28 structure HOLCFlogic : HOLCFLOGIC = |
42 |
43 |
43 (* mkNotEqUU_in v t = "v~=UU ==> t" *) |
44 (* mkNotEqUU_in v t = "v~=UU ==> t" *) |
44 fun mkNotEqUU_in vterm term = |
45 fun mkNotEqUU_in vterm term = |
45 mk_implies(mkNotEqUU vterm,term) |
46 mk_implies(mkNotEqUU vterm,term) |
46 |
47 |
|
48 val HOLCF_sg = sign_of HOLCF.thy; |
|
49 fun mk_typ t (S,T) = Sign.intern_typ HOLCF_sg (Type(t,[S,T])); |
|
50 fun rep_Type (Type x) = x| rep_Type _ = error "Internal error: rep_Type"; |
47 |
51 |
48 infixr 6 ==>; (* the analogon to --> for operations *) |
52 infixr 6 ==>; (* the analogon to --> for operations *) |
49 fun a ==> b = Type("->",[a,b]); |
53 val op ==> = mk_typ "->"; |
|
54 val cfun_arrow = fst (rep_Type (dummyT ==> dummyT)); |
50 |
55 |
51 (* Ops application (f ` x) *) |
56 (* Ops application (f ` x) *) |
52 fun mkOpApp (f as Const(_,ft as Type("->",[xt,rt]))) x = |
57 fun mkOpApp (f as Const(_,ft as Type(_(*"->"*),[xt,rt]))) x = |
53 Const("fapp",ft --> xt --> rt) $ f $ x |
58 Const("fapp",ft --> xt --> rt) $ f $ x |
54 | mkOpApp f x = (error("Internal error: mkOpApp: wrong args")); |
59 | mkOpApp f x = (error("Internal error: mkOpApp: wrong args")); |
55 |
60 |
56 (* cpair constructor *) |
61 (* cpair constructor *) |
57 fun mkCPair x y = let val tx = fastype_of x |
62 fun mkCPair x y = let val tx = fastype_of x |