diff -r 486d4647bb37 -r 8f8652a8107f Nominal/nominal_dt_rawfuns.ML
--- a/Nominal/nominal_dt_rawfuns.ML	Fri Sep 10 09:17:40 2010 +0800
+++ b/Nominal/nominal_dt_rawfuns.ML	Sat Sep 11 05:56:49 2010 +0800
@@ -82,64 +82,64 @@
 (* functions for producing sets, fsets and lists of general atom type
    out from concrete atom types *)
 fun mk_atom_set t =
-let
-  val ty = fastype_of t;
-  val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"};
-  val img_ty = atom_ty --> ty --> @{typ "atom set"};
-in
-  Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t
-end
+  let
+    val ty = fastype_of t;
+    val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"};
+    val img_ty = atom_ty --> ty --> @{typ "atom set"};
+  in
+    Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t
+  end
 
 
 fun dest_fsetT (Type (@{type_name fset}, [T])) = T
   | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
 
 fun mk_atom_fset t =
-let
-  val ty = fastype_of t;
-  val atom_ty = dest_fsetT ty --> @{typ "atom"};
-  val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};
-  val fset_to_set = @{term "fset_to_set :: atom fset => atom set"}
-in
-  fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)
-end
+  let
+    val ty = fastype_of t;
+    val atom_ty = dest_fsetT ty --> @{typ "atom"};
+    val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};
+    val fset_to_set = @{term "fset_to_set :: atom fset => atom set"}
+  in
+    fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)
+  end
 
-fun mk_atom_list t =
-let
-  val ty = fastype_of t;
-  val atom_ty = dest_listT ty --> @{typ atom};
-  val map_ty = atom_ty --> ty --> @{typ "atom list"};
-in
-  Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t
-end
+  fun mk_atom_list t =
+  let
+    val ty = fastype_of t;
+    val atom_ty = dest_listT ty --> @{typ atom};
+    val map_ty = atom_ty --> ty --> @{typ "atom list"};
+  in
+    Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t
+  end
 
 (* functions that coerces singletons, sets and fsets of concrete atoms
    into sets of general atoms *)
 fun setify ctxt t =
-let
-  val ty = fastype_of t;
-in
-  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 ctxt ty
-    then mk_atom_fset t
-  else raise TERM ("setify", [t])
-end
+  let
+    val ty = fastype_of t;
+  in
+    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 ctxt ty
+      then mk_atom_fset t
+    else raise TERM ("setify", [t])
+  end
 
 (* functions that coerces singletons and lists of concrete atoms
    into lists of general atoms  *)
 fun listify ctxt t =
-let
-  val ty = fastype_of t;
-in
-  if is_atom ctxt ty
-    then HOLogic.mk_list @{typ atom} [mk_atom t]
-  else if is_atom_list ctxt ty
-    then mk_atom_set t
-  else raise TERM ("listify", [t])
-end
+  let
+    val ty = fastype_of t;
+  in
+    if is_atom ctxt ty
+      then HOLogic.mk_list @{typ atom} [mk_atom t]
+    else if is_atom_list ctxt ty
+      then mk_atom_set t
+    else raise TERM ("listify", [t])
+  end
 
 (* coerces a list into a set *)
 fun to_set t =
@@ -152,136 +152,136 @@
 (** functions that construct the equations for fv and fv_bn **)
 
 fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (bmode, binders, bodies)) =
-let
-  fun mk_fv_body fv_map args i = 
   let
-    val arg = nth args i
-    val ty = fastype_of arg
-  in
-    case AList.lookup (op=) fv_map ty of
-      NONE => mk_supp arg
-    | SOME fv => fv $ arg
-  end  
+    fun mk_fv_body fv_map args i = 
+      let
+        val arg = nth args i
+        val ty = fastype_of arg
+      in
+        case AList.lookup (op=) fv_map ty of
+          NONE => mk_supp arg
+        | SOME fv => fv $ arg
+      end  
 
   fun mk_fv_binder lthy fv_bn_map args binders = 
-  let
-    fun bind_set lthy args (NONE, i) = (setify lthy (nth args i), @{term "{}::atom set"})
-      | bind_set _ args (SOME bn, i) = (bn $ (nth args i), 
-          if  member (op=) bodies i then @{term "{}::atom set"}  
-          else lookup fv_bn_map bn $ (nth args i))
-    fun bind_lst lthy args (NONE, i) = (listify lthy (nth args i), @{term "[]::atom list"})
-      | bind_lst _ args (SOME bn, i) = (bn $ (nth args i),
-          if  member (op=) bodies i then @{term "[]::atom list"}  
-          else lookup fv_bn_map bn $ (nth args i)) 
+    let
+      fun bind_set lthy args (NONE, i) = (setify lthy (nth args i), @{term "{}::atom set"})
+        | bind_set _ args (SOME bn, i) = (bn $ (nth args i), 
+            if  member (op=) bodies i then @{term "{}::atom set"}  
+            else lookup fv_bn_map bn $ (nth args i))
+      fun bind_lst lthy args (NONE, i) = (listify lthy (nth args i), @{term "[]::atom list"})
+        | bind_lst _ args (SOME bn, i) = (bn $ (nth args i),
+            if  member (op=) bodies i then @{term "[]::atom list"}  
+            else lookup fv_bn_map bn $ (nth args i)) 
   
-    val (combine_fn, bind_fn) =
-      case bmode of
-        Lst => (fold_append, bind_lst) 
-      | Set => (fold_union, bind_set)
-      | Res => (fold_union, bind_set)
-  in
-    binders
-    |> map (bind_fn lthy args)
-    |> split_list
-    |> pairself combine_fn
-  end  
+      val (combine_fn, bind_fn) =
+        case bmode of
+          Lst => (fold_append, bind_lst) 
+        | Set => (fold_union, bind_set)
+        | Res => (fold_union, bind_set)
+    in
+      binders
+      |> map (bind_fn lthy args)
+      |> split_list
+      |> pairself combine_fn
+    end  
 
-  val t1 = map (mk_fv_body fv_map args) bodies
-  val (t2, t3) = mk_fv_binder lthy fv_bn_map args binders
-in 
-  mk_union (mk_diff (fold_union t1, to_set t2), to_set t3)
-end
+    val t1 = map (mk_fv_body fv_map args) bodies
+    val (t2, t3) = mk_fv_binder lthy fv_bn_map args binders
+  in 
+    mk_union (mk_diff (fold_union t1, to_set t2), to_set t3)
+  end
 
 (* in case of fv_bn we have to treat the case special, where an
    "empty" binding clause is given *)
 fun mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause =
-let
-  fun mk_fv_bn_body fv_map fv_bn_map bn_args args i = 
   let
-    val arg = nth args i
-    val ty = fastype_of arg
+    fun mk_fv_bn_body i = 
+    let
+      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) => lookup fv_bn_map bn $ arg
+    end  
   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) => lookup fv_bn_map bn $ arg
-  end  
-in
-  case bclause of
-    BC (_, [], bodies) => fold_union (map (mk_fv_bn_body fv_map fv_bn_map bn_args args) bodies)
-  | _ => mk_fv_rhs lthy fv_map fv_bn_map args bclause
-end
+    case bclause of
+      BC (_, [], bodies) => fold_union (map mk_fv_bn_body bodies)
+    | _ => mk_fv_rhs lthy fv_map fv_bn_map args bclause
+  end
 
 fun mk_fv_eq lthy fv_map fv_bn_map (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 = lookup fv_map ty
-  val lhs = fv $ list_comb (constr, args)
-  val rhs_trms = map (mk_fv_rhs lthy fv_map fv_bn_map args) bclauses
-  val rhs = fold_union rhs_trms
-in
-  HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
-end
+  let
+    val arg_names = Datatype_Prop.make_tnames arg_tys
+    val args = map Free (arg_names ~~ arg_tys)
+    val fv = lookup fv_map ty
+    val lhs = fv $ list_comb (constr, args)
+    val rhs_trms = map (mk_fv_rhs lthy fv_map fv_bn_map args) bclauses
+    val rhs = fold_union rhs_trms
+  in
+    HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+  end
 
 fun mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys, _)) bclauses =
-let
-  val arg_names = Datatype_Prop.make_tnames arg_tys
-  val args = map Free (arg_names ~~ arg_tys)
-  val fv_bn = lookup fv_bn_map bn_trm
-  val lhs = fv_bn $ list_comb (constr, args)
-  val rhs_trms = map (mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses
-  val rhs = fold_union rhs_trms
-in
-  HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
-end
+  let
+    val arg_names = Datatype_Prop.make_tnames arg_tys
+    val args = map Free (arg_names ~~ arg_tys)
+    val fv_bn = lookup fv_bn_map bn_trm
+    val lhs = fv_bn $ list_comb (constr, args)
+    val rhs_trms = map (mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses
+    val rhs = fold_union rhs_trms
+  in
+    HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+  end
 
 fun mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = 
-let
-  val nth_constrs_info = nth constrs_info bn_n
-  val nth_bclausess = nth bclausesss bn_n
-in
-  map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
-end
+  let
+    val nth_constrs_info = nth constrs_info bn_n
+    val nth_bclausess = nth bclausesss bn_n
+  in
+    map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
+  end
 
 fun define_raw_fvs raw_full_ty_names raw_tys cns_info bn_info bclausesss constr_thms size_simps lthy =
-let
-  val fv_names = map (prefix "fv_" o Long_Name.base_name) raw_full_ty_names
-  val fv_tys = map (fn ty => ty --> @{typ "atom set"}) raw_tys
-  val fv_frees = map Free (fv_names ~~ fv_tys);
-  val fv_map = raw_tys ~~ fv_frees
+  let
+    val fv_names = map (prefix "fv_" o Long_Name.base_name) raw_full_ty_names
+    val fv_tys = map (fn ty => ty --> @{typ "atom set"}) raw_tys
+    val fv_frees = map Free (fv_names ~~ fv_tys);
+    val fv_map = raw_tys ~~ fv_frees
 
-  val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info)
-  val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns
-  val fv_bn_names = map (prefix "fv_") bn_names
-  val fv_bn_arg_tys = map (nth raw_tys) bn_tys
-  val fv_bn_tys = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys
-  val fv_bn_frees = map Free (fv_bn_names ~~ fv_bn_tys)
-  val fv_bn_map = bns ~~ fv_bn_frees
+    val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info)
+    val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns
+    val fv_bn_names = map (prefix "fv_") bn_names
+    val fv_bn_arg_tys = map (nth raw_tys) bn_tys
+    val fv_bn_tys = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys
+    val fv_bn_frees = map Free (fv_bn_names ~~ fv_bn_tys)
+    val fv_bn_map = bns ~~ fv_bn_frees
 
-  val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) cns_info bclausesss 
-  val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map cns_info bclausesss) bn_info
+    val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) cns_info bclausesss 
+    val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map cns_info bclausesss) bn_info
   
-  val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
-  val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)
+    val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
+    val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)
 
-  val (_, lthy') = Function.add_function all_fun_names all_fun_eqs
-    Function_Common.default_config (pat_completeness_simp constr_thms) lthy
+    val (_, lthy') = Function.add_function all_fun_names all_fun_eqs
+      Function_Common.default_config (pat_completeness_simp constr_thms) lthy
   
-  val (info, lthy'') = prove_termination size_simps (Local_Theory.restore lthy')
+    val (info, lthy'') = prove_termination size_simps (Local_Theory.restore lthy')
  
-  val {fs, simps, inducts, ...} = info;
+    val {fs, simps, inducts, ...} = info;
 
-  val morphism = ProofContext.export_morphism lthy'' lthy
-  val simps_exp = map (Morphism.thm morphism) (the simps)
-  val inducts_exp = map (Morphism.thm morphism) (the inducts)
+    val morphism = ProofContext.export_morphism lthy'' lthy
+    val simps_exp = map (Morphism.thm morphism) (the simps)
+    val inducts_exp = map (Morphism.thm morphism) (the inducts)
 
-  val (fvs', fv_bns') = chop (length fv_frees) fs
-in
-  (fvs', fv_bns', simps_exp, inducts_exp, lthy'')
-end
+    val (fvs', fv_bns') = chop (length fv_frees) fs
+  in
+    (fvs', fv_bns', simps_exp, inducts_exp, lthy'')
+  end
 
 
 (** equivarance proofs **)
@@ -302,12 +302,12 @@
      THEN_ALL_NEW  subproof_tac const_names simps ctxt)
 
 fun mk_eqvt_goal pi const arg =
-let
-  val lhs = mk_perm pi (const $ arg)
-  val rhs = const $ (mk_perm pi arg)  
-in
-  HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
-end
+  let
+    val lhs = mk_perm pi (const $ arg)
+    val rhs = const $ (mk_perm pi arg)  
+  in
+    HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+  end
 
 fun raw_prove_eqvt consts ind_thms simps ctxt =
   if null consts then []