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