TFL/usyntax.sml
author oheimb
Wed, 12 Nov 1997 12:34:43 +0100
changeset 4206 688050e83d89
parent 3713 8a1f7d5b1eff
child 6498 1ebbe18fe236
permissions -rw-r--r--
restored last version
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
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    53
(* Free variables, in order of occurrence, from left to right in the 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    54
 * syntax tree. *)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    55
fun free_vars_lr tm = 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    56
  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
    57
      fun add (t, frees) = case t of
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    58
            Free   _ => if (memb t frees) then frees else t::frees
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    59
          | Abs (_,_,body) => add(body,frees)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    60
          | f$t =>  add(t, add(f, frees))
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    61
          | _ => frees
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    62
  in rev(add(tm,[]))
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    63
  end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    64
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    65
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    66
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    67
val type_vars_in_term = map mk_prim_vartype o term_tvars;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    68
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    69
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    70
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    71
(* Prelogic *)
3353
9112a2efb9a3 Removal of module Mask and datatype binding with its constructor |->
paulson
parents: 3330
diff changeset
    72
fun dest_tybinding (v,ty) = (#1(dest_vtype v),ty)
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    73
fun inst theta = subst_vars (map dest_tybinding theta,[])
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    74
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    75
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    76
(* Construction routines *)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    77
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    78
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
    79
  | 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
    80
  | mk_abs _ = raise USYN_ERR{func = "mk_abs", mesg = "Bvar is not a variable"};
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    81
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    82
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    83
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
    84
   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
    85
   in list_comb(c,[ant,conseq])
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    86
   end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    87
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    88
fun mk_select (r as {Bvar,Body}) = 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    89
  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
    90
      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
    91
  in list_comb(c,[mk_abs r])
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    92
  end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    93
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    94
fun mk_forall (r as {Bvar,Body}) = 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    95
  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
    96
      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
    97
  in list_comb(c,[mk_abs r])
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    98
  end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    99
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   100
fun mk_exists (r as {Bvar,Body}) = 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   101
  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
   102
      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
   103
  in list_comb(c,[mk_abs r])
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   104
  end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   105
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   106
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   107
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
   108
   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
   109
   in list_comb(c,[conj1,conj2])
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   110
   end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   111
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   112
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
   113
   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
   114
   in list_comb(c,[disj1,disj2])
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   115
   end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   116
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   117
fun prod_ty ty1 ty2 = Type("*", [ty1,ty2]);
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   118
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   119
local
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   120
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
   121
    Const("split",(xt --> yt --> zt) --> prod_ty xt yt --> zt)
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   122
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
   123
  | dest_pair _ = raise USYN_ERR{func = "dest_pair", mesg = "not a pair"}
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   124
fun is_var(Var(_)) = true | is_var (Free _) = true | is_var _ = false
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   125
in
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   126
fun mk_pabs{varstruct,body} = 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   127
 let fun mpa(varstruct,body) =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   128
       if (is_var varstruct)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   129
       then mk_abs{Bvar = varstruct, Body = body}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   130
       else let val {fst,snd} = dest_pair varstruct
3405
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms
paulson
parents: 3391
diff changeset
   131
            in mk_uncurry(type_of fst,type_of snd,type_of body) $
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms
paulson
parents: 3391
diff changeset
   132
	       mpa(fst,mpa(snd,body))
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   133
            end
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   134
 in mpa(varstruct,body)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   135
 end
3353
9112a2efb9a3 Removal of module Mask and datatype binding with its constructor |->
paulson
parents: 3330
diff changeset
   136
 handle _ => raise USYN_ERR{func = "mk_pabs", mesg = ""};
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   137
end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   138
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   139
(* Destruction routines *)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   140
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   141
datatype lambda = VAR   of {Name : string, Ty : typ}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   142
                | CONST of {Name : string, Ty : typ}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   143
                | COMB  of {Rator: term, Rand : term}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   144
                | LAMB  of {Bvar : term, Body : term};
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   145
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   146
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   147
fun dest_term(Var((s,i),ty)) = VAR{Name = s, Ty = ty}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   148
  | dest_term(Free(s,ty))    = VAR{Name = s, Ty = ty}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   149
  | dest_term(Const(s,ty))   = CONST{Name = s, Ty = ty}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   150
  | 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
   151
  | dest_term(Abs(s,ty,M))   = let  val v = Free(s,ty)
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   152
                               in LAMB{Bvar = v, Body = betapply (M,v)}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   153
                               end
3353
9112a2efb9a3 Removal of module Mask and datatype binding with its constructor |->
paulson
parents: 3330
diff changeset
   154
  | dest_term(Bound _)       = raise USYN_ERR{func = "dest_term",mesg = "Bound"};
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   155
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   156
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
   157
  | dest_const _ = raise USYN_ERR{func = "dest_const", mesg = "not a constant"};
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   158
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   159
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
   160
  | dest_comb _ =  raise USYN_ERR{func = "dest_comb", mesg = "not a comb"};
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   161
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   162
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
   163
     let val v = Free(s,ty)
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   164
     in {Bvar = v, Body = betapply (a,v)}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   165
     end
3353
9112a2efb9a3 Removal of module Mask and datatype binding with its constructor |->
paulson
parents: 3330
diff changeset
   166
  | dest_abs _ =  raise USYN_ERR{func = "dest_abs", mesg = "not an abstraction"};
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   167
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   168
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
   169
  | dest_eq _ = raise USYN_ERR{func = "dest_eq", mesg = "not an equality"};
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   170
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   171
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
   172
  | dest_imp _ = raise USYN_ERR{func = "dest_imp", mesg = "not an implication"};
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   173
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   174
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
   175
  | dest_forall _ = raise USYN_ERR{func = "dest_forall", mesg = "not a forall"};
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   176
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   177
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
   178
  | dest_exists _ = raise USYN_ERR{func = "dest_exists", mesg="not an existential"};
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   179
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   180
fun dest_neg(Const("not",_) $ M) = M
3353
9112a2efb9a3 Removal of module Mask and datatype binding with its constructor |->
paulson
parents: 3330
diff changeset
   181
  | dest_neg _ = raise USYN_ERR{func = "dest_neg", mesg = "not a negation"};
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   182
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   183
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
   184
  | dest_conj _ = raise USYN_ERR{func = "dest_conj", mesg = "not a conjunction"};
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   185
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   186
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
   187
  | dest_disj _ = raise USYN_ERR{func = "dest_disj", mesg = "not a disjunction"};
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   188
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   189
fun mk_pair{fst,snd} = 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   190
   let val ty1 = type_of fst
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   191
       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
   192
       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
   193
   in list_comb(c,[fst,snd])
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   194
   end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   195
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   196
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
   197
  | dest_pair _ = raise USYN_ERR{func = "dest_pair", mesg = "not a pair"};
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   198
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   199
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   200
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
   201
                       else raise Match)
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   202
in
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   203
fun dest_pabs tm =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   204
   let val {Bvar,Body} = dest_abs tm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   205
   in {varstruct = Bvar, body = Body}
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   206
   end 
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   207
    handle 
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   208
     _ => let val {Rator,Rand} = dest_comb tm
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   209
              val _ = ucheck Rator
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   210
              val {varstruct = lv,body} = dest_pabs Rand
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   211
              val {varstruct = rv,body} = dest_pabs body
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   212
          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
   213
          end
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   214
end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   215
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   216
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   217
(* Garbage - ought to be dropped *)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   218
val lhs   = #lhs o dest_eq
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   219
val rhs   = #rhs o dest_eq
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   220
val rand  = #Rand o dest_comb
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   221
  
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   222
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   223
(* Query routines *)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   224
val is_imp    = can dest_imp
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   225
val is_forall = can dest_forall
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   226
val is_exists = can dest_exists
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   227
val is_neg    = can dest_neg
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   228
val is_conj   = can dest_conj
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   229
val is_disj   = can dest_disj
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   230
val is_pair   = can dest_pair
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   231
val is_pabs   = can dest_pabs
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   232
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   233
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   234
(* Construction of a cterm from a list of Terms *)
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   235
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   236
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
   237
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   238
(* These others are almost never used *)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   239
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
   240
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
   241
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
   242
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   243
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   244
(* Need to reverse? *)
3391
5e45dd3b64e9 More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents: 3353
diff changeset
   245
fun gen_all tm = list_mk_forall(term_frees tm, tm);
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   246
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   247
(* Destructing a cterm to a list of Terms *)
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   248
fun strip_comb tm = 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   249
   let fun dest(M$N, A) = dest(M, N::A)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   250
         | dest x = x
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   251
   in dest(tm,[])
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
fun strip_abs(tm as Abs _) =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   255
       let val {Bvar,Body} = dest_abs tm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   256
           val (bvs, core) = strip_abs Body
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   257
       in (Bvar::bvs, core)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   258
       end
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   259
  | strip_abs M = ([],M);
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   260
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   261
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   262
fun strip_imp fm =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   263
   if (is_imp fm)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   264
   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
   265
            val (was,wb) = strip_imp conseq
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   266
        in ((ant::was), wb)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   267
        end
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   268
   else ([],fm);
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   269
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   270
fun strip_forall fm =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   271
   if (is_forall fm)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   272
   then let val {Bvar,Body} = dest_forall fm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   273
            val (bvs,core) = strip_forall Body
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   274
        in ((Bvar::bvs), core)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   275
        end
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   276
   else ([],fm);
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   277
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   278
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   279
fun strip_exists fm =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   280
   if (is_exists fm)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   281
   then let val {Bvar, Body} = dest_exists fm 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   282
            val (bvs,core) = strip_exists Body
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   283
        in (Bvar::bvs, core)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   284
        end
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   285
   else ([],fm);
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   286
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   287
fun strip_disj w =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   288
   if (is_disj w)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   289
   then let val {disj1,disj2} = dest_disj w 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   290
        in (strip_disj disj1@strip_disj disj2)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   291
        end
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   292
   else [w];
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   293
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   294
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   295
(* Miscellaneous *)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   296
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   297
fun mk_vstruct ty V =
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   298
  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
   299
	      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
   300
		  val (rtm,vs2) = follow_prod_type ty2 vs1
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   301
	      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
   302
	| follow_prod_type _ (v::vs) = (v,vs)
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   303
  in #1 (follow_prod_type ty V)  end;
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   304
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   305
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   306
(* Search a term for a sub-term satisfying the predicate p. *)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   307
fun find_term p =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   308
   let fun find tm =
3405
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms
paulson
parents: 3391
diff changeset
   309
      if (p tm) then Some tm 
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms
paulson
parents: 3391
diff changeset
   310
      else case tm of
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms
paulson
parents: 3391
diff changeset
   311
	  Abs(_,_,body) => find body
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms
paulson
parents: 3391
diff changeset
   312
	| (t$u)         => (Some (the (find t)) handle _ => find u)
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms
paulson
parents: 3391
diff changeset
   313
	| _             => None
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   314
   in find
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   315
   end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   316
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   317
fun dest_relation tm =
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   318
   if (type_of tm = HOLogic.boolT)
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   319
   then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   320
        in (R,y,x)
3353
9112a2efb9a3 Removal of module Mask and datatype binding with its constructor |->
paulson
parents: 3330
diff changeset
   321
        end handle _ => raise USYN_ERR{func="dest_relation",
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   322
                                  mesg="unexpected term structure"}
3353
9112a2efb9a3 Removal of module Mask and datatype binding with its constructor |->
paulson
parents: 3330
diff changeset
   323
   else raise USYN_ERR{func="dest_relation",mesg="not a boolean term"};
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   324
3405
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms
paulson
parents: 3391
diff changeset
   325
fun is_WFR (Const("wf",_)$_) = true
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms
paulson
parents: 3391
diff changeset
   326
  | is_WFR _                 = false;
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   327
3391
5e45dd3b64e9 More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents: 3353
diff changeset
   328
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
   329
                       Body=Const("True",HOLogic.boolT)};
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   330
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   331
end; (* Syntax *)