Quot/Nominal/Fv.thy
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Thu, 18 Feb 2010 13:36:38 +0100
changeset 1191 15362b433d64
parent 1185 7566b899ca6a
child 1192 6fd072d3acd2
permissions -rw-r--r--
Description of the fv procedure.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1168
5c1e16806901 Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     1
theory Fv
1178
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
     2
imports "Nominal2_Atoms"
1168
5c1e16806901 Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     3
begin
5c1e16806901 Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     4
1169
b9d02e0800e9 Description of intended bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1168
diff changeset
     5
(* Bindings are given as a list which has a length being equal
1172
9a609fefcf24 Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1169
diff changeset
     6
   to the length of the number of constructors.
9a609fefcf24 Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1169
diff changeset
     7
9a609fefcf24 Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1169
diff changeset
     8
   Each element is a list whose length is equal to the number
9a609fefcf24 Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1169
diff changeset
     9
   of arguents.
9a609fefcf24 Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1169
diff changeset
    10
9a609fefcf24 Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1169
diff changeset
    11
   Every element specifies bindings of this argument given as
9a609fefcf24 Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1169
diff changeset
    12
   a tuple: function, bound argument.
1169
b9d02e0800e9 Description of intended bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1168
diff changeset
    13
b9d02e0800e9 Description of intended bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1168
diff changeset
    14
  Eg:
b9d02e0800e9 Description of intended bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1168
diff changeset
    15
nominal_datatype
b9d02e0800e9 Description of intended bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1168
diff changeset
    16
b9d02e0800e9 Description of intended bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1168
diff changeset
    17
   C1
b9d02e0800e9 Description of intended bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1168
diff changeset
    18
 | C2 x y z bind x in z
1172
9a609fefcf24 Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1169
diff changeset
    19
 | C3 x y z bind f x in z bind g y in z
1169
b9d02e0800e9 Description of intended bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1168
diff changeset
    20
b9d02e0800e9 Description of intended bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1168
diff changeset
    21
yields:
1172
9a609fefcf24 Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1169
diff changeset
    22
[
9a609fefcf24 Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1169
diff changeset
    23
 [],
9a609fefcf24 Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1169
diff changeset
    24
 [[], [], [(NONE, 0)]],
1173
9cb99a28b40e Some optimizations and fixes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1172
diff changeset
    25
 [[], [], [(SOME (Const f), 0), (Some (Const g), 1)]]]
1185
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
    26
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
    27
A SOME binding has to have a function returning an atom set,
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
    28
and a NONE binding has to be on an argument that is an atom
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
    29
or an atom set.
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
    30
1191
15362b433d64 Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1185
diff changeset
    31
How the procedure works:
15362b433d64 Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1185
diff changeset
    32
  For each of the defined datatypes,
15362b433d64 Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1185
diff changeset
    33
  For each of the constructors,
15362b433d64 Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1185
diff changeset
    34
  It creates a union of free variables for each argument.
15362b433d64 Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1185
diff changeset
    35
15362b433d64 Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1185
diff changeset
    36
  For an argument the free variables are the variables minus
15362b433d64 Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1185
diff changeset
    37
  bound variables.
15362b433d64 Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1185
diff changeset
    38
15362b433d64 Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1185
diff changeset
    39
  The variables are:
15362b433d64 Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1185
diff changeset
    40
    For an atom, a singleton set with the atom itself.
15362b433d64 Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1185
diff changeset
    41
    For an atom set, the atom set itself.
15362b433d64 Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1185
diff changeset
    42
    For a recursive argument, the appropriate fv function applied to it.
15362b433d64 Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1185
diff changeset
    43
    (* TODO: This one is not implemented *)
15362b433d64 Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1185
diff changeset
    44
    For other arguments it should be an appropriate fv function stored
15362b433d64 Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1185
diff changeset
    45
      in the database.
15362b433d64 Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1185
diff changeset
    46
  The bound variables are a union of results of all bindings that
15362b433d64 Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1185
diff changeset
    47
  involve the given argument. For a paricular binding the result is:
15362b433d64 Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1185
diff changeset
    48
    For a function applied to an argument this function with the argument.
15362b433d64 Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1185
diff changeset
    49
    For an atom, a singleton set with the atom itself.
15362b433d64 Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1185
diff changeset
    50
    For an atom set, the atom set itself.
15362b433d64 Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1185
diff changeset
    51
    For a recursive argument, the appropriate fv function applied to it.
15362b433d64 Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1185
diff changeset
    52
    (* TODO: This one is not implemented *)
15362b433d64 Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1185
diff changeset
    53
    For other arguments it should be an appropriate fv function stored
15362b433d64 Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1185
diff changeset
    54
      in the database.
1169
b9d02e0800e9 Description of intended bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1168
diff changeset
    55
*)
b9d02e0800e9 Description of intended bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1168
diff changeset
    56
1168
5c1e16806901 Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    57
ML {*
1175
6a3be6ef348d Reorganization
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1174
diff changeset
    58
  open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *);
1178
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
    59
  (* TODO: It is the same as one in 'nominal_atoms' *)
1175
6a3be6ef348d Reorganization
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1174
diff changeset
    60
  fun mk_atom ty = Const (@{const_name atom}, ty --> @{typ atom});
6a3be6ef348d Reorganization
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1174
diff changeset
    61
  val noatoms = @{term "{} :: atom set"};
6a3be6ef348d Reorganization
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1174
diff changeset
    62
  fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x];
6a3be6ef348d Reorganization
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1174
diff changeset
    63
  fun mk_union sets =
6a3be6ef348d Reorganization
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1174
diff changeset
    64
    fold (fn a => fn b =>
6a3be6ef348d Reorganization
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1174
diff changeset
    65
      if a = noatoms then b else
6a3be6ef348d Reorganization
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1174
diff changeset
    66
      if b = noatoms then a else
6a3be6ef348d Reorganization
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1174
diff changeset
    67
      HOLogic.mk_binop @{const_name union} (a, b)) (rev sets) noatoms;
6a3be6ef348d Reorganization
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1174
diff changeset
    68
  fun mk_diff a b =
6a3be6ef348d Reorganization
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1174
diff changeset
    69
    if b = noatoms then a else
6a3be6ef348d Reorganization
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1174
diff changeset
    70
    if b = a then noatoms else
6a3be6ef348d Reorganization
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1174
diff changeset
    71
    HOLogic.mk_binop @{const_name minus} (a, b);
1185
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
    72
  fun mk_atoms t =
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
    73
    let
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
    74
      val ty = fastype_of t;
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
    75
      val atom_ty = HOLogic.dest_setT ty --> @{typ atom};
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
    76
      val img_ty = atom_ty --> ty --> @{typ "atom set"};
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
    77
    in
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
    78
      (Const (@{const_name image}, img_ty) $ Const (@{const_name atom}, atom_ty) $ t)
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
    79
    end;
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
    80
  (* Copy from Term *)
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
    81
  fun is_funtype (Type ("fun", [_, _])) = true
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
    82
    | is_funtype _ = false;
1175
6a3be6ef348d Reorganization
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1174
diff changeset
    83
*}
6a3be6ef348d Reorganization
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1174
diff changeset
    84
6a3be6ef348d Reorganization
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1174
diff changeset
    85
ML {*
1178
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
    86
(* Currently needs just one full_tname to access Datatype *)
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
    87
fun define_raw_fv full_tname bindsall lthy =
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
    88
let
1185
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
    89
  val thy = ProofContext.theory_of lthy;
1178
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
    90
  val {descr, ...} = Datatype.the_info thy full_tname;
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
    91
  val sorts = []; (* TODO *)
1168
5c1e16806901 Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    92
  fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
5c1e16806901 Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    93
  val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
5c1e16806901 Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    94
    "fv_" ^ name_of_typ (nth_dtyp i)) descr);
5c1e16806901 Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    95
  val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr;
5c1e16806901 Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    96
  val fv_frees = map Free (fv_names ~~ fv_types);
1173
9cb99a28b40e Some optimizations and fixes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1172
diff changeset
    97
  fun fv_eq_constr i (cname, dts) bindcs =
1168
5c1e16806901 Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    98
    let
5c1e16806901 Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    99
      val Ts = map (typ_of_dtyp descr sorts) dts;
5c1e16806901 Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   100
      val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
5c1e16806901 Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   101
      val args = map Free (names ~~ Ts);
5c1e16806901 Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   102
      val c = Const (cname, Ts ---> (nth_dtyp i));
5c1e16806901 Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   103
      val fv_c = Free (nth fv_names i, (nth_dtyp i) --> @{typ "atom set"});
1177
6f01720fe520 Add bindings of recursive types by free_variables.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1176
diff changeset
   104
      fun fv_bind (NONE, i) =
6f01720fe520 Add bindings of recursive types by free_variables.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1176
diff changeset
   105
            if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else
6f01720fe520 Add bindings of recursive types by free_variables.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1176
diff changeset
   106
            (* TODO we assume that all can be 'atomized' *)
1185
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
   107
            if (is_funtype o fastype_of) (nth args i) then mk_atoms (nth args i) else
1177
6f01720fe520 Add bindings of recursive types by free_variables.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1176
diff changeset
   108
            mk_single_atom (nth args i)
1174
f6e9ae54b855 Now should work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1173
diff changeset
   109
        | fv_bind (SOME f, i) = f $ (nth args i);
1173
9cb99a28b40e Some optimizations and fixes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1172
diff changeset
   110
      fun fv_arg ((dt, x), bindxs) =
1172
9a609fefcf24 Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1169
diff changeset
   111
        let
9a609fefcf24 Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1169
diff changeset
   112
          val arg =
1175
6a3be6ef348d Reorganization
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1174
diff changeset
   113
            if is_rec_type dt then nth fv_frees (body_index dt) $ x else
1174
f6e9ae54b855 Now should work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1173
diff changeset
   114
            (* TODO: we just assume everything can be 'atomized' *)
1185
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
   115
            if (is_funtype o fastype_of) x then mk_atoms x else
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
   116
            HOLogic.mk_set @{typ atom} [mk_atom (fastype_of x) $ x]
1173
9cb99a28b40e Some optimizations and fixes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1172
diff changeset
   117
          val sub = mk_union (map fv_bind bindxs)
1172
9a609fefcf24 Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1169
diff changeset
   118
        in
1173
9cb99a28b40e Some optimizations and fixes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1172
diff changeset
   119
          mk_diff arg sub
9cb99a28b40e Some optimizations and fixes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1172
diff changeset
   120
        end;
1176
29c4a0cf9237 Bindings adapted to multiple defined datatypes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1175
diff changeset
   121
        val _ = tracing ("d" ^ string_of_int (length dts));
29c4a0cf9237 Bindings adapted to multiple defined datatypes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1175
diff changeset
   122
        val _ = tracing (string_of_int (length args));
29c4a0cf9237 Bindings adapted to multiple defined datatypes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1175
diff changeset
   123
        val _ = tracing (string_of_int (length bindcs));
1173
9cb99a28b40e Some optimizations and fixes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1172
diff changeset
   124
    in
1168
5c1e16806901 Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   125
      (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
1173
9cb99a28b40e Some optimizations and fixes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1172
diff changeset
   126
        (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs)))))
1168
5c1e16806901 Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   127
    end;
1176
29c4a0cf9237 Bindings adapted to multiple defined datatypes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1175
diff changeset
   128
  fun fv_eq (i, (_, _, constrs)) binds = map2 (fv_eq_constr i) constrs binds;
29c4a0cf9237 Bindings adapted to multiple defined datatypes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1175
diff changeset
   129
  val fv_eqs = flat (map2 fv_eq descr bindsall)
1178
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   130
in
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   131
  snd (Primrec.add_primrec
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   132
    (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) fv_eqs lthy)
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   133
end
1168
5c1e16806901 Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   134
*}
5c1e16806901 Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   135
1185
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
   136
(* tests:
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
   137
1178
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   138
atom_decl name
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   139
1185
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
   140
datatype ty =
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
   141
  Var "name set"
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
   142
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
   143
ML {* Syntax.check_term @{context} (mk_atoms @{term "a :: name set"}) *}
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
   144
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
   145
local_setup {* define_raw_fv "Fv.ty" [[[[]]]] *}
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
   146
print_theorems
7566b899ca6a Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1180
diff changeset
   147
1178
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   148
datatype rtrm1 =
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   149
  rVr1 "name"
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   150
| rAp1 "rtrm1" "rtrm1"
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   151
| rLm1 "name" "rtrm1"        --"name is bound in trm1"
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   152
| rLt1 "bp" "rtrm1" "rtrm1"   --"all variables in bp are bound in the 2nd trm1"
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   153
and bp =
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   154
  BUnit
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   155
| BVr "name"
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   156
| BPr "bp" "bp"
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   157
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   158
(* to be given by the user *)
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   159
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   160
primrec 
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   161
  bv1
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   162
where
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   163
  "bv1 (BUnit) = {}"
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   164
| "bv1 (BVr x) = {atom x}"
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   165
| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   166
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   167
local_setup {* define_raw_fv "Fv.rtrm1"
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   168
  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]],
275a1cb3f2ba Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1177
diff changeset
   169
   [[], [[]], [[], []]]] *}
1168
5c1e16806901 Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   170
print_theorems
5c1e16806901 Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   171
1180
3f36936f1280 Testing Fv
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1178
diff changeset
   172
*)
3f36936f1280 Testing Fv
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1178
diff changeset
   173
1168
5c1e16806901 Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   174
end