28 _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) |
28 _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) |
29 | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec)) |
29 | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec)) |
30 | _ => [thm]; |
30 | _ => [thm]; |
31 in map zero_var_indexes (at thm) end; |
31 in map zero_var_indexes (at thm) end; |
32 |
32 |
|
33 (* infix syntax *) |
|
34 |
|
35 infixr 5 -->; |
|
36 infixr 6 ->>; |
|
37 infixr 0 ===>; |
|
38 infixr 0 ==>; |
|
39 infix 0 ==; |
|
40 infix 1 ===; |
|
41 infix 1 ~=; |
|
42 infix 1 <<; |
|
43 infix 1 ~<<; |
|
44 |
|
45 infix 9 ` ; |
|
46 infix 9 `% ; |
|
47 infix 9 `%%; |
|
48 |
|
49 |
33 (* ----- specific support for domain ---------------------------------------- *) |
50 (* ----- specific support for domain ---------------------------------------- *) |
34 |
51 |
35 structure Domain_Library = struct |
52 signature DOMAIN_LIBRARY = |
|
53 sig |
|
54 val Imposs : string -> 'a; |
|
55 val pcpo_type : theory -> typ -> bool; |
|
56 val string_of_typ : theory -> typ -> string; |
|
57 |
|
58 (* Creating HOLCF types *) |
|
59 val mk_cfunT : typ * typ -> typ; |
|
60 val ->> : typ * typ -> typ; |
|
61 val mk_ssumT : typ * typ -> typ; |
|
62 val mk_sprodT : typ * typ -> typ; |
|
63 val mk_uT : typ -> typ; |
|
64 val oneT : typ; |
|
65 val trT : typ; |
|
66 val mk_maybeT : typ -> typ; |
|
67 val mk_ctupleT : typ list -> typ; |
|
68 val mk_TFree : string -> typ; |
|
69 val pcpoS : sort; |
|
70 |
|
71 (* Creating HOLCF terms *) |
|
72 val %: : string -> term; |
|
73 val %%: : string -> term; |
|
74 val ` : term * term -> term; |
|
75 val `% : term * string -> term; |
|
76 val /\ : string -> term -> term; |
|
77 val UU : term; |
|
78 val TT : term; |
|
79 val FF : term; |
|
80 val mk_up : term -> term; |
|
81 val mk_sinl : term -> term; |
|
82 val mk_sinr : term -> term; |
|
83 val mk_stuple : term list -> term; |
|
84 val mk_ctuple : term list -> term; |
|
85 val mk_fix : term -> term; |
|
86 val mk_iterate : term * term * term -> term; |
|
87 val mk_fail : term; |
|
88 val mk_return : term -> term; |
|
89 val cproj : term -> 'a list -> int -> term; |
|
90 val list_ccomb : term * term list -> term; |
|
91 val con_app : string -> ('a * 'b * string) list -> term; |
|
92 val con_app2 : string -> ('a -> term) -> 'a list -> term; |
|
93 val proj : term -> 'a list -> int -> term; |
|
94 val prj : ('a -> 'b -> 'a) -> ('a -> 'b -> 'a) -> 'a -> 'b list -> int -> 'a; |
|
95 val mk_ctuple_pat : term list -> term; |
|
96 val mk_branch : term -> term; |
|
97 |
|
98 (* Creating propositions *) |
|
99 val mk_conj : term * term -> term; |
|
100 val mk_disj : term * term -> term; |
|
101 val mk_imp : term * term -> term; |
|
102 val mk_lam : string * term -> term; |
|
103 val mk_all : string * term -> term; |
|
104 val mk_ex : string * term -> term; |
|
105 val mk_constrain : typ * term -> term; |
|
106 val mk_constrainall : string * typ * term -> term; |
|
107 val === : term * term -> term; |
|
108 val << : term * term -> term; |
|
109 val ~<< : term * term -> term; |
|
110 val strict : term -> term; |
|
111 val defined : term -> term; |
|
112 val mk_adm : term -> term; |
|
113 val mk_compact : term -> term; |
|
114 val lift : ('a -> term) -> 'a list * term -> term; |
|
115 val lift_defined : ('a -> term) -> 'a list * term -> term; |
|
116 |
|
117 (* Creating meta-propositions *) |
|
118 val mk_trp : term -> term; (* HOLogic.mk_Trueprop *) |
|
119 val == : term * term -> term; |
|
120 val ===> : term * term -> term; |
|
121 val ==> : term * term -> term; |
|
122 val mk_All : string * term -> term; |
|
123 |
|
124 (* Domain specifications *) |
|
125 type arg = (bool * int * DatatypeAux.dtyp) * string option * string; |
|
126 type cons = string * arg list; |
|
127 type eq = (string * typ list) * cons list; |
|
128 val is_lazy : arg -> bool; |
|
129 val rec_of : arg -> int; |
|
130 val sel_of : arg -> string option; |
|
131 val vname : arg -> string; |
|
132 val upd_vname : (string -> string) -> arg -> arg; |
|
133 val is_rec : arg -> bool; |
|
134 val is_nonlazy_rec : arg -> bool; |
|
135 val nonlazy : arg list -> string list; |
|
136 val nonlazy_rec : arg list -> string list; |
|
137 val %# : arg -> term; |
|
138 val /\# : arg * term -> term; |
|
139 val when_body : cons list -> (int * int -> term) -> term; |
|
140 val when_funs : 'a list -> string list; |
|
141 val bound_arg : ''a list -> ''a -> term; (* ''a = arg or string *) |
|
142 val idx_name : 'a list -> string -> int -> string; |
|
143 val app_rec_arg : (int -> term) -> arg -> term; |
|
144 |
|
145 (* Name mangling *) |
|
146 val strip_esc : string -> string; |
|
147 val extern_name : string -> string; |
|
148 val dis_name : string -> string; |
|
149 val mat_name : string -> string; |
|
150 val pat_name : string -> string; |
|
151 val mk_var_names : string list -> string list; |
|
152 end; |
|
153 |
|
154 structure Domain_Library : DOMAIN_LIBRARY = |
|
155 struct |
36 |
156 |
37 exception Impossible of string; |
157 exception Impossible of string; |
38 fun Imposs msg = raise Impossible ("Domain:"^msg); |
158 fun Imposs msg = raise Impossible ("Domain:"^msg); |
39 |
159 |
40 (* ----- name handling ----- *) |
160 (* ----- name handling ----- *) |
73 fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort pcpo}); |
193 fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort pcpo}); |
74 fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg; |
194 fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg; |
75 |
195 |
76 (* ----- constructor list handling ----- *) |
196 (* ----- constructor list handling ----- *) |
77 |
197 |
78 type cons = (string * (* operator name of constr *) |
198 type arg = |
79 ((bool*int*DatatypeAux.dtyp)* (* (lazy,recursive element or ~1) *) |
199 (bool * int * DatatypeAux.dtyp) * (* (lazy,recursive element or ~1) *) |
80 string option* (* selector name *) |
200 string option * (* selector name *) |
81 string) (* argument name *) |
201 string; (* argument name *) |
82 list); (* argument list *) |
202 |
83 type eq = (string * (* name of abstracted type *) |
203 type cons = |
84 typ list) * (* arguments of abstracted type *) |
204 string * (* operator name of constr *) |
85 cons list; (* represented type, as a constructor list *) |
205 arg list; (* argument list *) |
|
206 |
|
207 type eq = |
|
208 (string * (* name of abstracted type *) |
|
209 typ list) * (* arguments of abstracted type *) |
|
210 cons list; (* represented type, as a constructor list *) |
86 |
211 |
87 fun rec_of arg = second (first arg); |
212 fun rec_of arg = second (first arg); |
88 fun is_lazy arg = first (first arg); |
213 fun is_lazy arg = first (first arg); |
89 val sel_of = second; |
214 val sel_of = second; |
90 val vname = third; |
215 val vname = third; |
94 fun nonlazy args = map vname (filter_out is_lazy args); |
219 fun nonlazy args = map vname (filter_out is_lazy args); |
95 fun nonlazy_rec args = map vname (List.filter is_nonlazy_rec args); |
220 fun nonlazy_rec args = map vname (List.filter is_nonlazy_rec args); |
96 |
221 |
97 (* ----- support for type and mixfix expressions ----- *) |
222 (* ----- support for type and mixfix expressions ----- *) |
98 |
223 |
99 infixr 5 -->; |
|
100 fun mk_uT T = Type(@{type_name "u"}, [T]); |
224 fun mk_uT T = Type(@{type_name "u"}, [T]); |
101 fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]); |
225 fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]); |
102 fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]); |
226 fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]); |
103 fun mk_ssumT (T, U) = Type(@{type_name "++"}, [T, U]); |
227 fun mk_ssumT (T, U) = Type(@{type_name "++"}, [T, U]); |
104 val oneT = @{typ one}; |
228 val oneT = @{typ one}; |
105 val trT = @{typ tr}; |
229 val trT = @{typ tr}; |
106 |
230 |
107 infixr 6 ->>; |
|
108 val op ->> = mk_cfunT; |
231 val op ->> = mk_cfunT; |
109 |
232 |
110 fun mk_TFree s = TFree ("'" ^ s, @{sort pcpo}); |
233 fun mk_TFree s = TFree ("'" ^ s, @{sort pcpo}); |
111 |
234 |
112 (* ----- support for term expressions ----- *) |
235 (* ----- support for term expressions ----- *) |