# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266416422 -3600
# Node ID 29c4a0cf9237b3124c5a3adc1fb50d8cd53530d3
# Parent  6a3be6ef348d6e24410b27969f4a800a8fd41f9b
Bindings adapted to multiple defined datatypes.

diff -r 6a3be6ef348d -r 29c4a0cf9237 Quot/Nominal/Fv.thy
--- a/Quot/Nominal/Fv.thy	Wed Feb 17 15:00:04 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Wed Feb 17 15:20:22 2010 +0100
@@ -43,15 +43,33 @@
 
 atom_decl name
 
-datatype rlam =
-  rVar "name"
-| rApp "rlam" "rlam"
-| rLam "name" "rlam"
+datatype rtrm1 =
+  rVr1 "name"
+| rAp1 "rtrm1" "rtrm1"
+| rLm1 "name" "rtrm1"        --"name is bound in trm1"
+| rLt1 "bp" "rtrm1" "rtrm1"   --"all variables in bp are bound in the 2nd trm1"
+and bp =
+  BUnit
+| BVr "name"
+| BPr "bp" "bp"
+
+(* to be given by the user *)
 
+primrec 
+  bv1
+where
+  "bv1 (BUnit) = {}"
+| "bv1 (BVr x) = {atom x}"
+| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
+
+ML maps
 ML {*
-  val {descr, ...} = Datatype.the_info @{theory} "Fv.rlam";
+  val {descr, ...} = Datatype.the_info @{theory} "Fv.rtrm1";
   val sorts = [];
-  val binds = [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]];
+  val bindsall = [
+    [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [], [(SOME @{term bv1}, 0)]]],
+    [[], [[]], [[], []]]
+  ];
   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
   val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
     "fv_" ^ name_of_typ (nth_dtyp i)) descr);
@@ -77,12 +95,15 @@
         in
           mk_diff arg sub
         end;
+        val _ = tracing ("d" ^ string_of_int (length dts));
+        val _ = tracing (string_of_int (length args));
+        val _ = tracing (string_of_int (length bindcs));
     in
       (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
         (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs)))))
     end;
-  fun fv_eq (i, (_, _, constrs)) = map2 (fv_eq_constr i) constrs binds;
-  val fv_eqs = maps fv_eq descr
+  fun fv_eq (i, (_, _, constrs)) binds = map2 (fv_eq_constr i) constrs binds;
+  val fv_eqs = flat (map2 fv_eq descr bindsall)
 *}
 
 
@@ -92,11 +113,5 @@
 *}
 print_theorems
 
-fun
-  fv_rlam :: "rlam \<Rightarrow> atom set"
-where
-  "fv_rlam (rVar a) = {atom a}"
-| "fv_rlam (rApp t1 t2) = (fv_rlam t1) \<union> (fv_rlam t2)"
-| "fv_rlam (rLam a t) = (fv_rlam t) - {atom a}"
 
 end