100 fun all_varsl L = Utils.mk_set aconv |
97 fun all_varsl L = Utils.mk_set aconv |
101 (Utils.rev_itlist (curry op @ o all_vars) L []); |
98 (Utils.rev_itlist (curry op @ o all_vars) L []); |
102 |
99 |
103 |
100 |
104 (* Prelogic *) |
101 (* Prelogic *) |
105 val subst = subst_free o map (fn (a |-> b) => (a,b)); |
102 fun dest_tybinding (v,ty) = (#1(dest_vtype v),ty) |
106 |
|
107 fun dest_tybinding (v |-> ty) = (#1(dest_vtype v),ty) |
|
108 fun inst theta = subst_vars (map dest_tybinding theta,[]) |
103 fun inst theta = subst_vars (map dest_tybinding theta,[]) |
109 |
104 |
110 fun beta_conv((t1 as Abs _ ) $ t2) = betapply(t1,t2) |
105 fun beta_conv((t1 as Abs _ ) $ t2) = betapply(t1,t2) |
111 | beta_conv _ = raise ERR{func = "beta_conv", mesg = "Not a beta-redex"}; |
106 | beta_conv _ = raise USYN_ERR{func = "beta_conv", mesg = "Not a beta-redex"}; |
112 |
107 |
113 |
108 |
114 (* Construction routines *) |
109 (* Construction routines *) |
115 fun mk_var{Name,Ty} = Free(Name,Ty); |
110 fun mk_var{Name,Ty} = Free(Name,Ty); |
116 val mk_prim_var = Var; |
111 val mk_prim_var = Var; |
117 |
112 |
118 val string_variant = variant; |
113 val string_variant = variant; |
119 |
114 |
120 local fun var_name(Var((Name,_),_)) = Name |
115 local fun var_name(Var((Name,_),_)) = Name |
121 | var_name(Free(s,_)) = s |
116 | var_name(Free(s,_)) = s |
122 | var_name _ = raise ERR{func = "variant", |
117 | var_name _ = raise USYN_ERR{func = "variant", |
123 mesg = "list elem. is not a variable"} |
118 mesg = "list elem. is not a variable"} |
124 in |
119 in |
125 fun variant [] v = v |
120 fun variant [] v = v |
126 | variant vlist (Var((Name,i),ty)) = |
121 | variant vlist (Var((Name,i),ty)) = |
127 Var((string_variant (map var_name vlist) Name,i),ty) |
122 Var((string_variant (map var_name vlist) Name,i),ty) |
128 | variant vlist (Free(Name,ty)) = |
123 | variant vlist (Free(Name,ty)) = |
129 Free(string_variant (map var_name vlist) Name,ty) |
124 Free(string_variant (map var_name vlist) Name,ty) |
130 | variant _ _ = raise ERR{func = "variant", |
125 | variant _ _ = raise USYN_ERR{func = "variant", |
131 mesg = "2nd arg. should be a variable"} |
126 mesg = "2nd arg. should be a variable"} |
132 end; |
127 end; |
133 |
128 |
134 fun mk_const{Name,Ty} = Const(Name,Ty) |
129 fun mk_const{Name,Ty} = Const(Name,Ty) |
135 fun mk_comb{Rator,Rand} = Rator $ Rand; |
130 fun mk_comb{Rator,Rand} = Rator $ Rand; |
136 |
131 |
137 fun mk_abs{Bvar as Var((s,_),ty),Body} = Abs(s,ty,abstract_over(Bvar,Body)) |
132 fun mk_abs{Bvar as Var((s,_),ty),Body} = Abs(s,ty,abstract_over(Bvar,Body)) |
138 | mk_abs{Bvar as Free(s,ty),Body} = Abs(s,ty,abstract_over(Bvar,Body)) |
133 | mk_abs{Bvar as Free(s,ty),Body} = Abs(s,ty,abstract_over(Bvar,Body)) |
139 | mk_abs _ = raise ERR{func = "mk_abs", mesg = "Bvar is not a variable"}; |
134 | mk_abs _ = raise USYN_ERR{func = "mk_abs", mesg = "Bvar is not a variable"}; |
140 |
135 |
141 |
136 |
142 fun mk_imp{ant,conseq} = |
137 fun mk_imp{ant,conseq} = |
143 let val c = mk_const{Name = "op -->", Ty = HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT} |
138 let val c = mk_const{Name = "op -->", Ty = HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT} |
144 in list_comb(c,[ant,conseq]) |
139 in list_comb(c,[ant,conseq]) |
208 | dest_term(Const(s,ty)) = CONST{Name = s, Ty = ty} |
203 | dest_term(Const(s,ty)) = CONST{Name = s, Ty = ty} |
209 | dest_term(M$N) = COMB{Rator=M,Rand=N} |
204 | dest_term(M$N) = COMB{Rator=M,Rand=N} |
210 | dest_term(Abs(s,ty,M)) = let val v = mk_var{Name = s, Ty = ty} |
205 | dest_term(Abs(s,ty,M)) = let val v = mk_var{Name = s, Ty = ty} |
211 in LAMB{Bvar = v, Body = betapply (M,v)} |
206 in LAMB{Bvar = v, Body = betapply (M,v)} |
212 end |
207 end |
213 | dest_term(Bound _) = raise ERR{func = "dest_term",mesg = "Bound"}; |
208 | dest_term(Bound _) = raise USYN_ERR{func = "dest_term",mesg = "Bound"}; |
214 |
209 |
215 fun dest_const(Const(s,ty)) = {Name = s, Ty = ty} |
210 fun dest_const(Const(s,ty)) = {Name = s, Ty = ty} |
216 | dest_const _ = raise ERR{func = "dest_const", mesg = "not a constant"}; |
211 | dest_const _ = raise USYN_ERR{func = "dest_const", mesg = "not a constant"}; |
217 |
212 |
218 fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2} |
213 fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2} |
219 | dest_comb _ = raise ERR{func = "dest_comb", mesg = "not a comb"}; |
214 | dest_comb _ = raise USYN_ERR{func = "dest_comb", mesg = "not a comb"}; |
220 |
215 |
221 fun dest_abs(a as Abs(s,ty,M)) = |
216 fun dest_abs(a as Abs(s,ty,M)) = |
222 let val v = mk_var{Name = s, Ty = ty} |
217 let val v = mk_var{Name = s, Ty = ty} |
223 in {Bvar = v, Body = betapply (a,v)} |
218 in {Bvar = v, Body = betapply (a,v)} |
224 end |
219 end |
225 | dest_abs _ = raise ERR{func = "dest_abs", mesg = "not an abstraction"}; |
220 | dest_abs _ = raise USYN_ERR{func = "dest_abs", mesg = "not an abstraction"}; |
226 |
221 |
227 fun dest_eq(Const("op =",_) $ M $ N) = {lhs=M, rhs=N} |
222 fun dest_eq(Const("op =",_) $ M $ N) = {lhs=M, rhs=N} |
228 | dest_eq _ = raise ERR{func = "dest_eq", mesg = "not an equality"}; |
223 | dest_eq _ = raise USYN_ERR{func = "dest_eq", mesg = "not an equality"}; |
229 |
224 |
230 fun dest_imp(Const("op -->",_) $ M $ N) = {ant=M, conseq=N} |
225 fun dest_imp(Const("op -->",_) $ M $ N) = {ant=M, conseq=N} |
231 | dest_imp _ = raise ERR{func = "dest_imp", mesg = "not an implication"}; |
226 | dest_imp _ = raise USYN_ERR{func = "dest_imp", mesg = "not an implication"}; |
232 |
227 |
233 fun dest_select(Const("Eps",_) $ (a as Abs _)) = dest_abs a |
228 fun dest_select(Const("Eps",_) $ (a as Abs _)) = dest_abs a |
234 | dest_select _ = raise ERR{func = "dest_select", mesg = "not a select"}; |
229 | dest_select _ = raise USYN_ERR{func = "dest_select", mesg = "not a select"}; |
235 |
230 |
236 fun dest_forall(Const("All",_) $ (a as Abs _)) = dest_abs a |
231 fun dest_forall(Const("All",_) $ (a as Abs _)) = dest_abs a |
237 | dest_forall _ = raise ERR{func = "dest_forall", mesg = "not a forall"}; |
232 | dest_forall _ = raise USYN_ERR{func = "dest_forall", mesg = "not a forall"}; |
238 |
233 |
239 fun dest_exists(Const("Ex",_) $ (a as Abs _)) = dest_abs a |
234 fun dest_exists(Const("Ex",_) $ (a as Abs _)) = dest_abs a |
240 | dest_exists _ = raise ERR{func = "dest_exists", mesg="not an existential"}; |
235 | dest_exists _ = raise USYN_ERR{func = "dest_exists", mesg="not an existential"}; |
241 |
236 |
242 fun dest_neg(Const("not",_) $ M) = M |
237 fun dest_neg(Const("not",_) $ M) = M |
243 | dest_neg _ = raise ERR{func = "dest_neg", mesg = "not a negation"}; |
238 | dest_neg _ = raise USYN_ERR{func = "dest_neg", mesg = "not a negation"}; |
244 |
239 |
245 fun dest_conj(Const("op &",_) $ M $ N) = {conj1=M, conj2=N} |
240 fun dest_conj(Const("op &",_) $ M $ N) = {conj1=M, conj2=N} |
246 | dest_conj _ = raise ERR{func = "dest_conj", mesg = "not a conjunction"}; |
241 | dest_conj _ = raise USYN_ERR{func = "dest_conj", mesg = "not a conjunction"}; |
247 |
242 |
248 fun dest_disj(Const("op |",_) $ M $ N) = {disj1=M, disj2=N} |
243 fun dest_disj(Const("op |",_) $ M $ N) = {disj1=M, disj2=N} |
249 | dest_disj _ = raise ERR{func = "dest_disj", mesg = "not a disjunction"}; |
244 | dest_disj _ = raise USYN_ERR{func = "dest_disj", mesg = "not a disjunction"}; |
250 |
245 |
251 fun mk_pair{fst,snd} = |
246 fun mk_pair{fst,snd} = |
252 let val ty1 = type_of fst |
247 let val ty1 = type_of fst |
253 val ty2 = type_of snd |
248 val ty2 = type_of snd |
254 val c = mk_const{Name = "Pair", Ty = ty1 --> ty2 --> prod_ty ty1 ty2} |
249 val c = mk_const{Name = "Pair", Ty = ty1 --> ty2 --> prod_ty ty1 ty2} |
255 in list_comb(c,[fst,snd]) |
250 in list_comb(c,[fst,snd]) |
256 end; |
251 end; |
257 |
252 |
258 fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N} |
253 fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N} |
259 | dest_pair _ = raise ERR{func = "dest_pair", mesg = "not a pair"}; |
254 | dest_pair _ = raise USYN_ERR{func = "dest_pair", mesg = "not a pair"}; |
260 |
255 |
261 |
256 |
262 local fun ucheck t = (if #Name(dest_const t) = "split" then t |
257 local fun ucheck t = (if #Name(dest_const t) = "split" then t |
263 else raise Match) |
258 else raise Match) |
264 in |
259 in |
429 |
424 |
430 fun dest_relation tm = |
425 fun dest_relation tm = |
431 if (type_of tm = HOLogic.boolT) |
426 if (type_of tm = HOLogic.boolT) |
432 then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm |
427 then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm |
433 in (R,y,x) |
428 in (R,y,x) |
434 end handle _ => raise ERR{func="dest_relation", |
429 end handle _ => raise USYN_ERR{func="dest_relation", |
435 mesg="unexpected term structure"} |
430 mesg="unexpected term structure"} |
436 else raise ERR{func="dest_relation",mesg="not a boolean term"}; |
431 else raise USYN_ERR{func="dest_relation",mesg="not a boolean term"}; |
437 |
432 |
438 fun is_WFR tm = (#Name(dest_const(rator tm)) = "wf") handle _ => false; |
433 fun is_WFR tm = (#Name(dest_const(rator tm)) = "wf") handle _ => false; |
439 |
434 |
440 fun ARB ty = mk_select{Bvar=mk_var{Name="v",Ty=ty}, |
435 fun ARB ty = mk_select{Bvar=mk_var{Name="v",Ty=ty}, |
441 Body=mk_const{Name="True",Ty=HOLogic.boolT}}; |
436 Body=mk_const{Name="True",Ty=HOLogic.boolT}}; |