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