# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1282039255 -28800
# Node ID f1980f89c405c037266789111f3272e66137bb07
# Parent  49ab06c0ca6487df18c00dd122e0813603d366c9
deleted unused code

diff -r 49ab06c0ca64 -r f1980f89c405 Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Tue Aug 17 17:52:25 2010 +0800
+++ b/Nominal-General/nominal_library.ML	Tue Aug 17 18:00:55 2010 +0800
@@ -50,7 +50,6 @@
   val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list
 
   (* tactics for function package *)
-  val pat_completeness_auto: Proof.context -> tactic
   val pat_completeness_simp: thm list -> Proof.context -> tactic
   val prove_termination: Proof.context -> Function.info * local_theory
 
@@ -180,10 +179,6 @@
 
 (** function package tactics **)
 
-fun pat_completeness_auto lthy =
-  Pat_Completeness.pat_completeness_tac lthy 1
-    THEN auto_tac (clasimpset_of lthy)
-
 fun pat_completeness_simp simps lthy =
 let
   val simp_set = HOL_basic_ss addsimps (@{thms sum.inject sum.distinct} @ simps)
diff -r 49ab06c0ca64 -r f1980f89c405 Nominal/NewFv.thy
--- a/Nominal/NewFv.thy	Tue Aug 17 17:52:25 2010 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,263 +0,0 @@
-theory NewFv
-imports "../Nominal-General/Nominal2_Atoms"
-        "Abs" "Perm" "Nominal2_FSet"
-begin
-
-ML {*
-(* binding modes  and binding clauses *)
-
-datatype bmode = Lst | Res | Set
-
-datatype bclause =
-  BC of bmode * (term option * int) list * int list
-*}
-
-ML {*
-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 (@{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 ctxt ty =
-  Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})
-
-fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t
-  | is_atom_set _ _ = false;
-
-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;
-  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 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 \<Rightarrow> 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;
-*}
-
-ML {*
-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 error ("setify" ^ (PolyML.makestring (t, ty)))
-end
-*}
-
-ML {*
-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 error "listify"
-end
-*}
-
-ML {*
-fun to_set x =
-  if fastype_of x = @{typ "atom list"}
-  then @{term "set::atom list \<Rightarrow> atom set"} $ x
-  else x
-*}
-
-ML {*
-fun make_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  
-*}
-
-ML {*
-fun make_binder lthy fv_bn_map args (bn_option, i) = 
-let
-  val arg = nth args i
-in
-  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 make_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 = 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
-  HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
-end
-*}
-
-ML {*
-fun make_bn_body fv_map fv_bn_map bn_args args 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) => the (AList.lookup (op=) fv_bn_map bn) $ arg
-end  
-*}
-
-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
-  HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
-end
-*}
-
-ML {*
-fun make_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 (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 bn_funs2 bclausesss lthy =
-let
-
-  val fv_names = prefix_dt_names dt_descr sorts "fv_"
-  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
-
-  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 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 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)
-
-  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
-      (Lexicographic_Order.lexicographic_order_tac true lthy) lthy
-
-  val (_, lthy') = Function.add_function all_fv_names all_fv_eqs
-    Function_Common.default_config pat_completeness_auto lthy
-
-  val (info, lthy'') = prove_termination (Local_Theory.restore lthy')
-
-  val {fs, simps, ...} = info;
-
-  val morphism = ProofContext.export_morphism lthy'' lthy
-  val fs_exp = map (Morphism.term morphism) fs
-
-  val (fv_frees_exp, fv_bns_exp) = chop (length fv_frees) fs_exp
-  val simps_exp = Morphism.fact morphism (the simps)
-in
-  (fv_frees_exp, fv_bns_exp, simps_exp, lthy'')
-end
-*}
-
-
-
-
-
-end