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