--- 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 []