diff -r a5dc3558cdec -r 3b83960f9544 Nominal/NewFv.thy
--- a/Nominal/NewFv.thy	Wed May 19 12:44:03 2010 +0100
+++ b/Nominal/NewFv.thy	Thu May 20 21:23:53 2010 +0100
@@ -4,38 +4,42 @@
 begin
 
 ML {*
-(* binding modes *)
+(* binding modes  and binding clauses *)
 
-datatype bmodes =
-   BEmy of int
-|  BLst of ((term option * int) list) * (int list)
-|  BSet of ((term option * int) list) * (int list)
-|  BRes of ((term option * int) list) * (int list)
+datatype bmode = Lst | Res | Set
+
+datatype bclause =
+  BC of bmode * (term option * int) list * int list
 *}
 
 ML {*
-fun mk_singleton_atom x = HOLogic.mk_set @{typ atom} [mk_atom x];
-
-val noatoms = @{term "{} :: atom set"};
+fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"}
+  | mk_diff (t1, @{term "{}::atom set"}) = t1
+  | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2)
 
-fun mk_union sets =
-  fold (fn a => fn b =>
-  if a = noatoms then b else
-  if b = noatoms then a else
-  if a = b then a else
-  HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms;
+fun mk_union (@{term "{}::atom set"}, @{term "{}::atom set"}) = @{term "{}::atom set"}
+  | mk_union (t1 , @{term "{}::atom set"}) = t1
+  | mk_union (@{term "{}::atom set"}, t2) = t2
+  | mk_union (t1, t2) = HOLogic.mk_binop @{const_name sup} (t1, t2)  
+ 
+fun fold_union trms = fold (curry mk_union) trms @{term "{}::atom set"}
 *}
 
 ML {*
-fun is_atom thy ty =
-  Sign.of_sort thy (ty, @{sort at_base})
+fun is_atom ctxt ty =
+  Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})
 
-fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t
+fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t
   | is_atom_set _ _ = false;
 
-fun is_atom_fset thy (Type ("FSet.fset", [t])) = is_atom thy t
+fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t
   | is_atom_fset _ _ = false;
 
+fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t
+  | is_atom_list _ _ = false
+*}
+
+ML {*
 fun mk_atom_set t =
 let
   val ty = fastype_of t;
@@ -55,23 +59,6 @@
   fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)
 end;
 
-fun mk_diff a b =
-  if b = noatoms then a else
-  if b = a then noatoms else
-  HOLogic.mk_binop @{const_name minus} (a, b);
-*}
-
-ML {*
-fun is_atom_list (Type (@{type_name list}, [T])) = true
-  | is_atom_list _ = false
-*}
-
-ML {*
-fun dest_listT (Type (@{type_name list}, [T])) = T
-  | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], [])
-*}
-
-ML {*
 fun mk_atom_list t =
 let
   val ty = fastype_of t;
@@ -83,191 +70,170 @@
 *}
 
 ML {*
-fun setify thy t =
+fun setify ctxt t =
 let
   val ty = fastype_of t;
 in
-  if is_atom thy ty
-    then mk_singleton_atom t
-  else if is_atom_set thy ty
+  if is_atom ctxt ty
+    then  HOLogic.mk_set @{typ atom} [mk_atom t]
+  else if is_atom_set ctxt ty
     then mk_atom_set t
-  else if is_atom_fset thy ty
+  else if is_atom_fset ctxt ty
     then mk_atom_fset t
   else error ("setify" ^ (PolyML.makestring (t, ty)))
 end
 *}
 
 ML {*
-fun listify thy t =
+fun listify ctxt t =
 let
   val ty = fastype_of t;
 in
-  if is_atom thy ty
+  if is_atom ctxt ty
     then HOLogic.mk_list @{typ atom} [mk_atom t]
-  else if is_atom_list ty
+  else if is_atom_list ctxt ty
     then mk_atom_set t
   else error "listify"
 end
 *}
 
 ML {*
-fun set x =
+fun to_set x =
   if fastype_of x = @{typ "atom list"}
   then @{term "set::atom list \<Rightarrow> atom set"} $ x
   else x
 *}
 
 ML {*
-fun fv_body thy dts args fv_frees supp i =
+fun make_body fv_map args i = 
 let
-  val x = nth args i;
-  val dt = nth dts i;
+  val arg = nth args i
+  val ty = fastype_of arg
 in
-  if Datatype_Aux.is_rec_type dt
-  then nth fv_frees (Datatype_Aux.body_index dt) $ x
-  else (if supp then mk_supp x else setify thy x)
-end
+  case (AList.lookup (op=) fv_map ty) of
+    NONE => mk_supp arg
+  | SOME fv => fv $ arg
+end  
 *}
 
 ML {*
-fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys =
+fun make_binder lthy fv_bn_map args (bn_option, i) = 
 let
-  val fv_bodys = mk_union (map (fv_body thy dts args fv_frees true) bodys)
-  fun bound_var (SOME bn, i) = set (bn $ nth args i)
-    | bound_var (NONE, i) = fv_body thy dts args fv_frees false i
-  val bound_vars = mk_union (map bound_var binds);
-  fun non_rec_var (SOME bn, i) =
-      if member (op =) bodys i
-      then noatoms
-      else ((the (AList.lookup (op=) bn_fvbn bn)) $ nth args i)
-    | non_rec_var (NONE, _) = noatoms
+  val arg = nth args i
 in
-  mk_union ((mk_diff fv_bodys bound_vars) :: (map non_rec_var binds))
+  case bn_option of
+    NONE => (setify lthy arg, @{term "{}::atom set"})
+  | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg)
+end  
+*}
+
+ML {*
+fun make_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) =
+let
+  val t1 = map (make_body fv_map args) bodies
+  val (t2, t3) = split_list (map (make_binder lthy fv_bn_map args) binders)
+in 
+  fold_union (mk_diff (fold_union t1, fold_union t2)::t3)
 end
 *}
 
 ML {*
-fun fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn bm =
-case bm of
-  BEmy i =>
-    let
-      val x = nth args i;
-      val dt = nth dts i;
-    in
-      case AList.lookup (op=) args_in_bn i of
-        NONE => if Datatype_Aux.is_rec_type dt
-                then nth fv_frees (Datatype_Aux.body_index dt) $ x
-                else mk_supp x
-      | SOME (SOME (f : term)) => (the (AList.lookup (op=) bn_fvbn f)) $ x
-      | SOME NONE => noatoms
-    end
-| BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
-| BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
-| BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
-*}
-
-ML {*
-fun fv_bn thy dt_descr sorts fv_frees bn_fvbn bclausess (fvbn, (_, ith_dtyp, args_in_bns)) =
+fun make_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys) bclauses = 
 let
-  fun fv_bn_constr (cname, dts) (args_in_bn, bclauses) =
-  let
-    val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts;
-    val names = Datatype_Prop.make_tnames Ts;
-    val args = map Free (names ~~ Ts);
-    val c = Const (cname, Ts ---> (nth_dtyp dt_descr sorts ith_dtyp));
-    val fv_bn_bm = fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn
-  in
-    HOLogic.mk_Trueprop (HOLogic.mk_eq
-      (fvbn $ list_comb (c, args), mk_union (map fv_bn_bm bclauses)))
-  end;
-  val (_, (_, _, constrs)) = nth dt_descr ith_dtyp;
+  val arg_names = Datatype_Prop.make_tnames arg_tys
+  val args = map Free (arg_names ~~ arg_tys)
+  val fv = the (AList.lookup (op=) fv_map ty)
+  val lhs = fv $ list_comb (constr, args)
+  val rhs_trms = map (make_fv_rhs lthy fv_map fv_bn_map args) bclauses
+  val rhs = fold_union rhs_trms
 in
-  map2 fv_bn_constr constrs (args_in_bns ~~ bclausess)
+  HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
 end
 *}
 
 ML {*
-fun fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss =
+fun make_bn_body fv_map fv_bn_map bn_args args i = 
 let
-  fun mk_fvbn_free (bn, ith, _) =
-    let
-      val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn)));
-    in
-      (fvbn_name, Free (fvbn_name, fastype_of (nth fv_frees ith)))
-    end;
+  val arg = nth args i
+  val ty = fastype_of arg
+in
+  case AList.lookup (op=) bn_args i of
+    NONE => (case (AList.lookup (op=) fv_map ty) of
+              NONE => mk_supp arg
+            | SOME fv => fv $ arg)
+  | SOME (NONE) => @{term "{}::atom set"}
+  | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg
+end  
+*}
 
-  val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free bn_funs);
-  val bn_fvbn = (map (fn (bn, _, _) => bn) bn_funs) ~~ fvbn_frees
-  val bclausessl = map (fn (_, i, _) => nth bclausesss i) bn_funs;
-  val eqs = map2 (fv_bn thy dt_descr sorts fv_frees bn_fvbn) bclausessl (fvbn_frees ~~ bn_funs);
+ML {*
+fun make_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause =
+  case bclause of
+    BC (_, [], bodies) => fold_union (map (make_bn_body fv_map fv_bn_map bn_args args) bodies)
+  | BC (_, binders, bodies) => 
+      let
+        val t1 = map (make_body fv_map args) bodies
+        val (t2, t3) = split_list (map (make_binder lthy fv_bn_map args) binders)
+      in 
+        fold_union (mk_diff (fold_union t1, fold_union t2)::t3)
+      end
+*}
+
+ML {*
+fun make_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, ty, arg_tys)) bclauses =
+let
+  val arg_names = Datatype_Prop.make_tnames arg_tys
+  val args = map Free (arg_names ~~ arg_tys)
+  val fv_bn = the (AList.lookup (op=) fv_bn_map bn_trm)
+  val lhs = fv_bn $ list_comb (constr, args)
+  val rhs_trms = map (make_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses
+  val rhs = fold_union rhs_trms
 in
-  (bn_fvbn, fvbn_names, eqs)
+  HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
 end
 *}
 
 ML {*
-fun fv_bm thy dts args fv_frees bn_fvbn bm =
-case bm of
-  BEmy i =>
-    let
-      val x = nth args i;
-      val dt = nth dts i;
-    in
-      if Datatype_Aux.is_rec_type dt
-      then nth fv_frees (Datatype_Aux.body_index dt) $ x
-      else mk_supp x
-    end
-| BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
-| BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
-| BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
-*}
-
-ML {*
-fun fv thy dt_descr sorts fv_frees bn_fvbn bclausess (fv_free, ith_dtyp) =
+fun make_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = 
 let
-  fun fv_constr (cname, dts) bclauses =
-  let
-    val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts;
-    val names = Datatype_Prop.make_tnames Ts;
-    val args = map Free (names ~~ Ts);
-    val c = Const (cname, Ts ---> (nth_dtyp dt_descr sorts ith_dtyp));
-    val fv_bn_bm = fv_bm thy dts args fv_frees bn_fvbn
-  in
-    HOLogic.mk_Trueprop (HOLogic.mk_eq
-      (fv_free $ list_comb (c, args), mk_union (map fv_bn_bm bclauses)))
-  end;
-  val (_, (_, _, constrs)) = nth dt_descr ith_dtyp;
+  val nth_constrs_info = nth constrs_info bn_n
+  val nth_bclausess = nth bclausesss bn_n
 in
-  map2 fv_constr constrs bclausess
+  map2 (make_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
 end
 *}
 
 ML {*
-fun define_raw_fvs dt_descr sorts bn_funs bclausesss lthy =
+fun define_raw_fvs dt_descr sorts bn_funs bn_funs2 bclausesss lthy =
 let
-  val thy = ProofContext.theory_of lthy;
 
   val fv_names = prefix_dt_names dt_descr sorts "fv_"
-  val fv_types = map (fn (i, _) => nth_dtyp dt_descr sorts i --> @{typ "atom set"}) dt_descr;
-  val fv_frees = map Free (fv_names ~~ fv_types);
+  val fv_arg_tys = map (fn (i, _) => nth_dtyp dt_descr sorts i) dt_descr;
+  val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys;
+  val fv_frees = map Free (fv_names ~~ fv_tys);
+  val fv_map = fv_arg_tys ~~ fv_frees
 
-  (* free variables for the bn-functions *)
-  val (bn_fvbn_map, fv_bn_names, fv_bn_eqs) =
-    fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss;
+  val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_funs)
+  val (bns2, bn_tys2) = split_list (map (fn (bn, i, _) => (bn, i)) bn_funs2)
+  val bn_args2 = map (fn (_, _, arg) => arg) bn_funs2
+  val fv_bn_names2 = map (fn bn => "fv_" ^ (fst (dest_Free bn))) bns2
+  val fv_bn_arg_tys2 = map (fn i => nth_dtyp dt_descr sorts i) bn_tys2
+  val fv_bn_tys2 = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys2
+  val fv_bn_frees2 = map Free (fv_bn_names2 ~~ fv_bn_tys2)
+  val fv_bn_map2 = bns ~~ fv_bn_frees2
+  val fv_bn_map3 = bns2 ~~ fv_bn_frees2
+ 
+  val constrs_info = all_dtyp_constrs_types dt_descr sorts
 
-  val _ = tracing ("bn_fvbn_map" ^ commas (map @{make_string} bn_fvbn_map))
+  val fv_eqs2 = map2 (map2 (make_fv_eq lthy fv_map fv_bn_map2)) constrs_info bclausesss 
+  val fv_bn_eqs2 = map (make_fv_bn_eqs lthy fv_map fv_bn_map3 constrs_info bclausesss) bn_funs2
   
-  val fv_bns = map snd bn_fvbn_map;
-  val fv_nums = 0 upto (length fv_frees - 1)
-
-  val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn_map) bclausesss (fv_frees ~~ fv_nums);
+  val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names2)
+  val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs2 @ flat fv_bn_eqs2)
 
-  val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
-  val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)
-
-  fun pat_completeness_auto ctxt =
-    Pat_Completeness.pat_completeness_tac ctxt 1
-      THEN auto_tac (clasimpset_of ctxt)
+  fun pat_completeness_auto lthy =
+    Pat_Completeness.pat_completeness_tac lthy 1
+      THEN auto_tac (clasimpset_of lthy)
 
   fun prove_termination lthy =
     Function.prove_termination NONE
@@ -290,21 +256,8 @@
 end
 *}
 
-(**************************************************)
 
-datatype foo =
-  C1 nat
-| C2 foo int
 
-(*
-ML {* 
-fun mk_body descr sorts fv_ty_map dtyp =
-let
-  val nth_dtyp_constr_tys descr sorts
-in
-  true
-end
-*}
-*)
+
 
 end