author | wenzelm |
Tue, 05 Sep 2000 18:53:42 +0200 | |
changeset 9867 | bf8300fa4238 |
parent 9373 | 78a11a353473 |
child 9876 | a069795f1060 |
permissions | -rw-r--r-- |
9867 | 1 |
(* Title: TFL/usyntax.sml |
3302 | 2 |
ID: $Id$ |
3 |
Author: Konrad Slind, Cambridge University Computer Laboratory |
|
4 |
Copyright 1997 University of Cambridge |
|
5 |
||
9867 | 6 |
Emulation of HOL's abstract syntax functions. |
3302 | 7 |
*) |
8 |
||
9867 | 9 |
signature USyntax_sig = |
10 |
sig |
|
11 |
structure Utils : Utils_sig |
|
12 |
||
13 |
datatype lambda = VAR of {Name : string, Ty : typ} |
|
14 |
| CONST of {Name : string, Ty : typ} |
|
15 |
| COMB of {Rator: term, Rand : term} |
|
16 |
| LAMB of {Bvar : term, Body : term} |
|
17 |
||
18 |
val alpha : typ |
|
19 |
||
20 |
(* Types *) |
|
21 |
val type_vars : typ -> typ list |
|
22 |
val type_varsl : typ list -> typ list |
|
23 |
val mk_vartype : string -> typ |
|
24 |
val is_vartype : typ -> bool |
|
25 |
val strip_prod_type : typ -> typ list |
|
26 |
||
27 |
(* Terms *) |
|
28 |
val free_vars_lr : term -> term list |
|
29 |
val type_vars_in_term : term -> typ list |
|
30 |
val dest_term : term -> lambda |
|
31 |
||
32 |
(* Prelogic *) |
|
33 |
val inst : (typ*typ) list -> term -> term |
|
34 |
||
35 |
(* Construction routines *) |
|
36 |
val mk_abs :{Bvar : term, Body : term} -> term |
|
37 |
||
38 |
val mk_imp :{ant : term, conseq : term} -> term |
|
39 |
val mk_select :{Bvar : term, Body : term} -> term |
|
40 |
val mk_forall :{Bvar : term, Body : term} -> term |
|
41 |
val mk_exists :{Bvar : term, Body : term} -> term |
|
42 |
val mk_conj :{conj1 : term, conj2 : term} -> term |
|
43 |
val mk_disj :{disj1 : term, disj2 : term} -> term |
|
44 |
val mk_pabs :{varstruct : term, body : term} -> term |
|
45 |
||
46 |
(* Destruction routines *) |
|
47 |
val dest_const: term -> {Name : string, Ty : typ} |
|
48 |
val dest_comb : term -> {Rator : term, Rand : term} |
|
49 |
val dest_abs : term -> {Bvar : term, Body : term} |
|
50 |
val dest_eq : term -> {lhs : term, rhs : term} |
|
51 |
val dest_imp : term -> {ant : term, conseq : term} |
|
52 |
val dest_forall : term -> {Bvar : term, Body : term} |
|
53 |
val dest_exists : term -> {Bvar : term, Body : term} |
|
54 |
val dest_neg : term -> term |
|
55 |
val dest_conj : term -> {conj1 : term, conj2 : term} |
|
56 |
val dest_disj : term -> {disj1 : term, disj2 : term} |
|
57 |
val dest_pair : term -> {fst : term, snd : term} |
|
58 |
val dest_pabs : term -> {varstruct : term, body : term} |
|
59 |
||
60 |
val lhs : term -> term |
|
61 |
val rhs : term -> term |
|
62 |
val rand : term -> term |
|
63 |
||
64 |
(* Query routines *) |
|
65 |
val is_imp : term -> bool |
|
66 |
val is_forall : term -> bool |
|
67 |
val is_exists : term -> bool |
|
68 |
val is_neg : term -> bool |
|
69 |
val is_conj : term -> bool |
|
70 |
val is_disj : term -> bool |
|
71 |
val is_pair : term -> bool |
|
72 |
val is_pabs : term -> bool |
|
73 |
||
74 |
(* Construction of a term from a list of Preterms *) |
|
75 |
val list_mk_abs : (term list * term) -> term |
|
76 |
val list_mk_imp : (term list * term) -> term |
|
77 |
val list_mk_forall : (term list * term) -> term |
|
78 |
val list_mk_conj : term list -> term |
|
79 |
||
80 |
(* Destructing a term to a list of Preterms *) |
|
81 |
val strip_comb : term -> (term * term list) |
|
82 |
val strip_abs : term -> (term list * term) |
|
83 |
val strip_imp : term -> (term list * term) |
|
84 |
val strip_forall : term -> (term list * term) |
|
85 |
val strip_exists : term -> (term list * term) |
|
86 |
val strip_disj : term -> term list |
|
87 |
||
88 |
(* Miscellaneous *) |
|
89 |
val mk_vstruct : typ -> term list -> term |
|
90 |
val gen_all : term -> term |
|
91 |
val find_term : (term -> bool) -> term -> term option |
|
92 |
val dest_relation : term -> term * term * term |
|
93 |
val is_WFR : term -> bool |
|
94 |
val ARB : typ -> term |
|
95 |
end; |
|
96 |
||
97 |
||
2112 | 98 |
structure USyntax : USyntax_sig = |
99 |
struct |
|
100 |
||
101 |
structure Utils = Utils; |
|
102 |
open Utils; |
|
103 |
||
104 |
infix 4 ##; |
|
105 |
||
3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor |->
paulson
parents:
3330
diff
changeset
|
106 |
fun USYN_ERR{func,mesg} = Utils.ERR{module = "USyntax", func = func, mesg = mesg}; |
2112 | 107 |
|
108 |
||
109 |
(*--------------------------------------------------------------------------- |
|
110 |
* |
|
111 |
* Types |
|
112 |
* |
|
113 |
*---------------------------------------------------------------------------*) |
|
114 |
val mk_prim_vartype = TVar; |
|
115 |
fun mk_vartype s = mk_prim_vartype((s,0),["term"]); |
|
116 |
||
117 |
(* But internally, it's useful *) |
|
118 |
fun dest_vtype (TVar x) = x |
|
3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor |->
paulson
parents:
3330
diff
changeset
|
119 |
| dest_vtype _ = raise USYN_ERR{func = "dest_vtype", |
2112 | 120 |
mesg = "not a flexible type variable"}; |
121 |
||
122 |
val is_vartype = Utils.can dest_vtype; |
|
123 |
||
124 |
val type_vars = map mk_prim_vartype o typ_tvars |
|
3391
5e45dd3b64e9
More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents:
3353
diff
changeset
|
125 |
fun type_varsl L = distinct (Utils.rev_itlist (curry op @ o type_vars) L []); |
2112 | 126 |
|
127 |
val alpha = mk_vartype "'a" |
|
128 |
val beta = mk_vartype "'b" |
|
129 |
||
9373 | 130 |
val strip_prod_type = HOLogic.prodT_factors; |
2112 | 131 |
|
132 |
||
133 |
||
134 |
(*--------------------------------------------------------------------------- |
|
135 |
* |
|
136 |
* Terms |
|
137 |
* |
|
138 |
*---------------------------------------------------------------------------*) |
|
139 |
||
140 |
(* Free variables, in order of occurrence, from left to right in the |
|
141 |
* syntax tree. *) |
|
142 |
fun free_vars_lr tm = |
|
143 |
let fun memb x = let fun m[] = false | m(y::rst) = (x=y)orelse m rst in m end |
|
144 |
fun add (t, frees) = case t of |
|
145 |
Free _ => if (memb t frees) then frees else t::frees |
|
146 |
| Abs (_,_,body) => add(body,frees) |
|
147 |
| f$t => add(t, add(f, frees)) |
|
148 |
| _ => frees |
|
149 |
in rev(add(tm,[])) |
|
150 |
end; |
|
151 |
||
152 |
||
153 |
||
154 |
val type_vars_in_term = map mk_prim_vartype o term_tvars; |
|
155 |
||
156 |
||
157 |
||
158 |
(* Prelogic *) |
|
3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor |->
paulson
parents:
3330
diff
changeset
|
159 |
fun dest_tybinding (v,ty) = (#1(dest_vtype v),ty) |
2112 | 160 |
fun inst theta = subst_vars (map dest_tybinding theta,[]) |
161 |
||
162 |
||
163 |
(* Construction routines *) |
|
164 |
||
165 |
fun mk_abs{Bvar as Var((s,_),ty),Body} = Abs(s,ty,abstract_over(Bvar,Body)) |
|
166 |
| mk_abs{Bvar as Free(s,ty),Body} = Abs(s,ty,abstract_over(Bvar,Body)) |
|
3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor |->
paulson
parents:
3330
diff
changeset
|
167 |
| mk_abs _ = raise USYN_ERR{func = "mk_abs", mesg = "Bvar is not a variable"}; |
2112 | 168 |
|
169 |
||
170 |
fun mk_imp{ant,conseq} = |
|
3391
5e45dd3b64e9
More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents:
3353
diff
changeset
|
171 |
let val c = Const("op -->",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT) |
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
172 |
in list_comb(c,[ant,conseq]) |
2112 | 173 |
end; |
174 |
||
175 |
fun mk_select (r as {Bvar,Body}) = |
|
176 |
let val ty = type_of Bvar |
|
3391
5e45dd3b64e9
More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents:
3353
diff
changeset
|
177 |
val c = Const("Eps",(ty --> HOLogic.boolT) --> ty) |
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
178 |
in list_comb(c,[mk_abs r]) |
2112 | 179 |
end; |
180 |
||
181 |
fun mk_forall (r as {Bvar,Body}) = |
|
182 |
let val ty = type_of Bvar |
|
3391
5e45dd3b64e9
More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents:
3353
diff
changeset
|
183 |
val c = Const("All",(ty --> HOLogic.boolT) --> HOLogic.boolT) |
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
184 |
in list_comb(c,[mk_abs r]) |
2112 | 185 |
end; |
186 |
||
187 |
fun mk_exists (r as {Bvar,Body}) = |
|
188 |
let val ty = type_of Bvar |
|
3391
5e45dd3b64e9
More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents:
3353
diff
changeset
|
189 |
val c = Const("Ex",(ty --> HOLogic.boolT) --> HOLogic.boolT) |
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
190 |
in list_comb(c,[mk_abs r]) |
2112 | 191 |
end; |
192 |
||
193 |
||
194 |
fun mk_conj{conj1,conj2} = |
|
3391
5e45dd3b64e9
More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents:
3353
diff
changeset
|
195 |
let val c = Const("op &",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT) |
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
196 |
in list_comb(c,[conj1,conj2]) |
2112 | 197 |
end; |
198 |
||
199 |
fun mk_disj{disj1,disj2} = |
|
3391
5e45dd3b64e9
More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents:
3353
diff
changeset
|
200 |
let val c = Const("op |",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT) |
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
201 |
in list_comb(c,[disj1,disj2]) |
2112 | 202 |
end; |
203 |
||
9373 | 204 |
fun prod_ty ty1 ty2 = HOLogic.mk_prodT (ty1,ty2); |
2112 | 205 |
|
206 |
local |
|
207 |
fun mk_uncurry(xt,yt,zt) = |
|
3391
5e45dd3b64e9
More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents:
3353
diff
changeset
|
208 |
Const("split",(xt --> yt --> zt) --> prod_ty xt yt --> zt) |
2112 | 209 |
fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N} |
3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor |->
paulson
parents:
3330
diff
changeset
|
210 |
| dest_pair _ = raise USYN_ERR{func = "dest_pair", mesg = "not a pair"} |
2112 | 211 |
fun is_var(Var(_)) = true | is_var (Free _) = true | is_var _ = false |
212 |
in |
|
213 |
fun mk_pabs{varstruct,body} = |
|
214 |
let fun mpa(varstruct,body) = |
|
215 |
if (is_var varstruct) |
|
216 |
then mk_abs{Bvar = varstruct, Body = body} |
|
217 |
else let val {fst,snd} = dest_pair varstruct |
|
3405 | 218 |
in mk_uncurry(type_of fst,type_of snd,type_of body) $ |
219 |
mpa(fst,mpa(snd,body)) |
|
2112 | 220 |
end |
221 |
in mpa(varstruct,body) |
|
222 |
end |
|
3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor |->
paulson
parents:
3330
diff
changeset
|
223 |
handle _ => raise USYN_ERR{func = "mk_pabs", mesg = ""}; |
2112 | 224 |
end; |
225 |
||
226 |
(* Destruction routines *) |
|
227 |
||
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
228 |
datatype lambda = VAR of {Name : string, Ty : typ} |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
229 |
| CONST of {Name : string, Ty : typ} |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
230 |
| COMB of {Rator: term, Rand : term} |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
231 |
| LAMB of {Bvar : term, Body : term}; |
2112 | 232 |
|
233 |
||
234 |
fun dest_term(Var((s,i),ty)) = VAR{Name = s, Ty = ty} |
|
235 |
| dest_term(Free(s,ty)) = VAR{Name = s, Ty = ty} |
|
236 |
| dest_term(Const(s,ty)) = CONST{Name = s, Ty = ty} |
|
237 |
| dest_term(M$N) = COMB{Rator=M,Rand=N} |
|
3391
5e45dd3b64e9
More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents:
3353
diff
changeset
|
238 |
| dest_term(Abs(s,ty,M)) = let val v = Free(s,ty) |
2112 | 239 |
in LAMB{Bvar = v, Body = betapply (M,v)} |
240 |
end |
|
3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor |->
paulson
parents:
3330
diff
changeset
|
241 |
| dest_term(Bound _) = raise USYN_ERR{func = "dest_term",mesg = "Bound"}; |
2112 | 242 |
|
243 |
fun dest_const(Const(s,ty)) = {Name = s, Ty = ty} |
|
3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor |->
paulson
parents:
3330
diff
changeset
|
244 |
| dest_const _ = raise USYN_ERR{func = "dest_const", mesg = "not a constant"}; |
2112 | 245 |
|
246 |
fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2} |
|
3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor |->
paulson
parents:
3330
diff
changeset
|
247 |
| dest_comb _ = raise USYN_ERR{func = "dest_comb", mesg = "not a comb"}; |
2112 | 248 |
|
249 |
fun dest_abs(a as Abs(s,ty,M)) = |
|
3391
5e45dd3b64e9
More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents:
3353
diff
changeset
|
250 |
let val v = Free(s,ty) |
2112 | 251 |
in {Bvar = v, Body = betapply (a,v)} |
252 |
end |
|
3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor |->
paulson
parents:
3330
diff
changeset
|
253 |
| dest_abs _ = raise USYN_ERR{func = "dest_abs", mesg = "not an abstraction"}; |
2112 | 254 |
|
255 |
fun dest_eq(Const("op =",_) $ M $ N) = {lhs=M, rhs=N} |
|
3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor |->
paulson
parents:
3330
diff
changeset
|
256 |
| dest_eq _ = raise USYN_ERR{func = "dest_eq", mesg = "not an equality"}; |
2112 | 257 |
|
258 |
fun dest_imp(Const("op -->",_) $ M $ N) = {ant=M, conseq=N} |
|
3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor |->
paulson
parents:
3330
diff
changeset
|
259 |
| dest_imp _ = raise USYN_ERR{func = "dest_imp", mesg = "not an implication"}; |
2112 | 260 |
|
261 |
fun dest_forall(Const("All",_) $ (a as Abs _)) = dest_abs a |
|
3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor |->
paulson
parents:
3330
diff
changeset
|
262 |
| dest_forall _ = raise USYN_ERR{func = "dest_forall", mesg = "not a forall"}; |
2112 | 263 |
|
264 |
fun dest_exists(Const("Ex",_) $ (a as Abs _)) = dest_abs a |
|
3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor |->
paulson
parents:
3330
diff
changeset
|
265 |
| dest_exists _ = raise USYN_ERR{func = "dest_exists", mesg="not an existential"}; |
2112 | 266 |
|
267 |
fun dest_neg(Const("not",_) $ M) = M |
|
3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor |->
paulson
parents:
3330
diff
changeset
|
268 |
| dest_neg _ = raise USYN_ERR{func = "dest_neg", mesg = "not a negation"}; |
2112 | 269 |
|
270 |
fun dest_conj(Const("op &",_) $ M $ N) = {conj1=M, conj2=N} |
|
3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor |->
paulson
parents:
3330
diff
changeset
|
271 |
| dest_conj _ = raise USYN_ERR{func = "dest_conj", mesg = "not a conjunction"}; |
2112 | 272 |
|
273 |
fun dest_disj(Const("op |",_) $ M $ N) = {disj1=M, disj2=N} |
|
3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor |->
paulson
parents:
3330
diff
changeset
|
274 |
| dest_disj _ = raise USYN_ERR{func = "dest_disj", mesg = "not a disjunction"}; |
2112 | 275 |
|
276 |
fun mk_pair{fst,snd} = |
|
277 |
let val ty1 = type_of fst |
|
278 |
val ty2 = type_of snd |
|
3391
5e45dd3b64e9
More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents:
3353
diff
changeset
|
279 |
val c = Const("Pair",ty1 --> ty2 --> prod_ty ty1 ty2) |
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
280 |
in list_comb(c,[fst,snd]) |
2112 | 281 |
end; |
282 |
||
283 |
fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N} |
|
3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor |->
paulson
parents:
3330
diff
changeset
|
284 |
| dest_pair _ = raise USYN_ERR{func = "dest_pair", mesg = "not a pair"}; |
2112 | 285 |
|
286 |
||
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
287 |
local fun ucheck t = (if #Name(dest_const t) = "split" then t |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
288 |
else raise Match) |
2112 | 289 |
in |
290 |
fun dest_pabs tm = |
|
291 |
let val {Bvar,Body} = dest_abs tm |
|
292 |
in {varstruct = Bvar, body = Body} |
|
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
293 |
end |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
294 |
handle |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
295 |
_ => let val {Rator,Rand} = dest_comb tm |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
296 |
val _ = ucheck Rator |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
297 |
val {varstruct = lv,body} = dest_pabs Rand |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
298 |
val {varstruct = rv,body} = dest_pabs body |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
299 |
in {varstruct = mk_pair{fst = lv, snd = rv}, body = body} |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
300 |
end |
2112 | 301 |
end; |
302 |
||
303 |
||
304 |
val lhs = #lhs o dest_eq |
|
305 |
val rhs = #rhs o dest_eq |
|
306 |
val rand = #Rand o dest_comb |
|
307 |
||
308 |
||
309 |
(* Query routines *) |
|
310 |
val is_imp = can dest_imp |
|
311 |
val is_forall = can dest_forall |
|
312 |
val is_exists = can dest_exists |
|
313 |
val is_neg = can dest_neg |
|
314 |
val is_conj = can dest_conj |
|
315 |
val is_disj = can dest_disj |
|
316 |
val is_pair = can dest_pair |
|
317 |
val is_pabs = can dest_pabs |
|
318 |
||
319 |
||
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
320 |
(* Construction of a cterm from a list of Terms *) |
2112 | 321 |
|
322 |
fun list_mk_abs(L,tm) = itlist (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm; |
|
323 |
||
324 |
(* These others are almost never used *) |
|
325 |
fun list_mk_imp(A,c) = itlist(fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c; |
|
326 |
fun list_mk_forall(V,t) = itlist(fn v => fn b => mk_forall{Bvar=v, Body=b})V t; |
|
327 |
val list_mk_conj = end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm}) |
|
328 |
||
329 |
||
330 |
(* Need to reverse? *) |
|
3391
5e45dd3b64e9
More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents:
3353
diff
changeset
|
331 |
fun gen_all tm = list_mk_forall(term_frees tm, tm); |
2112 | 332 |
|
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
333 |
(* Destructing a cterm to a list of Terms *) |
2112 | 334 |
fun strip_comb tm = |
335 |
let fun dest(M$N, A) = dest(M, N::A) |
|
336 |
| dest x = x |
|
337 |
in dest(tm,[]) |
|
338 |
end; |
|
339 |
||
340 |
fun strip_abs(tm as Abs _) = |
|
341 |
let val {Bvar,Body} = dest_abs tm |
|
342 |
val (bvs, core) = strip_abs Body |
|
343 |
in (Bvar::bvs, core) |
|
344 |
end |
|
345 |
| strip_abs M = ([],M); |
|
346 |
||
347 |
||
348 |
fun strip_imp fm = |
|
349 |
if (is_imp fm) |
|
350 |
then let val {ant,conseq} = dest_imp fm |
|
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
351 |
val (was,wb) = strip_imp conseq |
2112 | 352 |
in ((ant::was), wb) |
353 |
end |
|
354 |
else ([],fm); |
|
355 |
||
356 |
fun strip_forall fm = |
|
357 |
if (is_forall fm) |
|
358 |
then let val {Bvar,Body} = dest_forall fm |
|
359 |
val (bvs,core) = strip_forall Body |
|
360 |
in ((Bvar::bvs), core) |
|
361 |
end |
|
362 |
else ([],fm); |
|
363 |
||
364 |
||
365 |
fun strip_exists fm = |
|
366 |
if (is_exists fm) |
|
367 |
then let val {Bvar, Body} = dest_exists fm |
|
368 |
val (bvs,core) = strip_exists Body |
|
369 |
in (Bvar::bvs, core) |
|
370 |
end |
|
371 |
else ([],fm); |
|
372 |
||
373 |
fun strip_disj w = |
|
374 |
if (is_disj w) |
|
375 |
then let val {disj1,disj2} = dest_disj w |
|
376 |
in (strip_disj disj1@strip_disj disj2) |
|
377 |
end |
|
378 |
else [w]; |
|
379 |
||
380 |
||
381 |
(* Miscellaneous *) |
|
382 |
||
383 |
fun mk_vstruct ty V = |
|
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
384 |
let fun follow_prod_type (Type("*",[ty1,ty2])) vs = |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
385 |
let val (ltm,vs1) = follow_prod_type ty1 vs |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
386 |
val (rtm,vs2) = follow_prod_type ty2 vs1 |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
387 |
in (mk_pair{fst=ltm, snd=rtm}, vs2) end |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
388 |
| follow_prod_type _ (v::vs) = (v,vs) |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
389 |
in #1 (follow_prod_type ty V) end; |
2112 | 390 |
|
391 |
||
392 |
(* Search a term for a sub-term satisfying the predicate p. *) |
|
393 |
fun find_term p = |
|
394 |
let fun find tm = |
|
3405 | 395 |
if (p tm) then Some tm |
396 |
else case tm of |
|
397 |
Abs(_,_,body) => find body |
|
398 |
| (t$u) => (Some (the (find t)) handle _ => find u) |
|
399 |
| _ => None |
|
2112 | 400 |
in find |
401 |
end; |
|
402 |
||
403 |
fun dest_relation tm = |
|
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
404 |
if (type_of tm = HOLogic.boolT) |
2112 | 405 |
then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm |
406 |
in (R,y,x) |
|
3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor |->
paulson
parents:
3330
diff
changeset
|
407 |
end handle _ => raise USYN_ERR{func="dest_relation", |
2112 | 408 |
mesg="unexpected term structure"} |
3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor |->
paulson
parents:
3330
diff
changeset
|
409 |
else raise USYN_ERR{func="dest_relation",mesg="not a boolean term"}; |
2112 | 410 |
|
8882 | 411 |
fun is_WFR (Const("WF.wf",_)$_) = true |
3405 | 412 |
| is_WFR _ = false; |
2112 | 413 |
|
3391
5e45dd3b64e9
More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents:
3353
diff
changeset
|
414 |
fun ARB ty = mk_select{Bvar=Free("v",ty), |
5e45dd3b64e9
More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents:
3353
diff
changeset
|
415 |
Body=Const("True",HOLogic.boolT)}; |
2112 | 416 |
|
417 |
end; (* Syntax *) |