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