--- a/Nominal/NewAlpha.thy Sun May 23 02:15:24 2010 +0100
+++ b/Nominal/NewAlpha.thy Mon May 24 20:02:37 2010 +0100
@@ -1,236 +1,231 @@
theory NewAlpha
-imports "Abs" "Perm" "Nominal2_FSet"
-uses ("nominal_dt_rawperm.ML")
- ("nominal_dt_rawfuns.ML")
+imports "Abs" "Perm"
begin
-use "nominal_dt_rawperm.ML"
-use "nominal_dt_rawfuns.ML"
-
ML {*
-open Nominal_Dt_RawPerm
-open Nominal_Dt_RawFuns
-*}
-
-
-ML {*
-fun mk_binop2 ctxt s (l, r) =
- Syntax.check_term ctxt (Const (s, dummyT) $ l $ r)
+fun mk_prod_fv (t1, t2) =
+let
+ val ty1 = fastype_of t1
+ val ty2 = fastype_of t2
+ val resT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2) --> @{typ "atom set"}
+in
+ Const (@{const_name "prod_fv"}, [ty1, ty2] ---> resT) $ t1 $ t2
+end
*}
ML {*
-fun mk_compound_fv' ctxt = foldr1 (mk_binop2 ctxt @{const_name prod_fv})
-fun mk_compound_alpha' ctxt = foldr1 (mk_binop2 ctxt @{const_name prod_rel})
+fun mk_prod_alpha (t1, t2) =
+let
+ val ty1 = fastype_of t1
+ val ty2 = fastype_of t2
+ val prodT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2)
+ val resT = [prodT, prodT] ---> @{typ "bool"}
+in
+ Const (@{const_name "prod_alpha"}, [ty1, ty2] ---> resT) $ t1 $ t2
+end
*}
ML {*
-fun alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees fv_frees
- bn_alphabn alpha_const binds bodys =
+fun mk_binders lthy bmode args bodies =
+let
+ fun bind_set lthy args (NONE, i) = setify lthy (nth args i)
+ | bind_set _ args (SOME bn, i) = bn $ (nth args i)
+ fun bind_lst lthy args (NONE, i) = listify lthy (nth args i)
+ | bind_lst _ args (SOME bn, i) = bn $ (nth args i)
+
+ val (connect_fn, bind_fn) =
+ case bmode of
+ Lst => (mk_append, bind_lst)
+ | Set => (mk_union, bind_set)
+ | Res => (mk_union, bind_set)
+in
+ foldl1 connect_fn (map (bind_fn lthy args) bodies)
+end
+*}
+
+ML {*
+fun mk_alpha_prem bmode fv alpha args args' binders binders' =
let
- fun bind_set args (NONE, no) = setify lthy (nth args no)
- | bind_set args (SOME f, no) = f $ (nth args no)
- fun bind_lst args (NONE, no) = listify lthy (nth args no)
- | bind_lst args (SOME f, no) = f $ (nth args no)
- fun append (t1, t2) =
- Const(@{const_name append}, @{typ "atom list \<Rightarrow> atom list \<Rightarrow> atom list"}) $ t1 $ t2;
- fun binds_fn args nos =
- if alpha_const = @{const_name alpha_lst}
- then foldr1 append (map (bind_lst args) nos)
- else fold_union (map (bind_set args) nos);
- val lhs_binds = binds_fn args binds;
- val rhs_binds = binds_fn args2 binds;
- val lhs_bodys = foldr1 HOLogic.mk_prod (map (nth args) bodys);
- val rhs_bodys = foldr1 HOLogic.mk_prod (map (nth args2) bodys);
- val lhs = HOLogic.mk_prod (lhs_binds, lhs_bodys);
- val rhs = HOLogic.mk_prod (rhs_binds, rhs_bodys);
- val body_dts = map (nth dts) bodys;
- fun fv_for_dt dt =
- if Datatype_Aux.is_rec_type dt
- then nth fv_frees (Datatype_Aux.body_index dt)
- else Const (@{const_name supp},
- Datatype_Aux.typ_of_dtyp dt_descr sorts dt --> @{typ "atom set"})
- val fvs = map fv_for_dt body_dts;
- val fv = mk_compound_fv' lthy fvs;
- fun alpha_for_dt dt =
- if Datatype_Aux.is_rec_type dt
- then nth alpha_frees (Datatype_Aux.body_index dt)
- else Const (@{const_name "op ="},
- Datatype_Aux.typ_of_dtyp dt_descr sorts dt -->
- Datatype_Aux.typ_of_dtyp dt_descr sorts dt --> @{typ bool})
- val alphas = map alpha_for_dt body_dts;
- val alpha = mk_compound_alpha' lthy alphas;
- val alpha_gen_pre = Const (alpha_const, dummyT) $ lhs $ alpha $ fv $ (Bound 0) $ rhs
- val alpha_gen_ex = HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm}, alpha_gen_pre)
- val t = Syntax.check_term lthy alpha_gen_ex
- fun alpha_bn_bind (SOME bn, i) =
- if member (op =) bodys i then NONE
- else SOME ((the (AList.lookup (op=) bn_alphabn bn)) $ nth args i $ nth args2 i)
- | alpha_bn_bind (NONE, _) = NONE
+ val (alpha_name, binder_ty) =
+ case bmode of
+ Lst => (@{const_name "alpha_lst"}, @{typ "atom list"})
+ | Set => (@{const_name "alpha_gen"}, @{typ "atom set"})
+ | Res => (@{const_name "alpha_res"}, @{typ "atom set"})
+ val ty = fastype_of args
+ val pair_ty = HOLogic.mk_prodT (binder_ty, ty)
+ val alpha_ty = [ty, ty] ---> @{typ "bool"}
+ val fv_ty = ty --> @{typ "atom set"}
in
- t :: (map_filter alpha_bn_bind binds)
+ HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm},
+ Const (alpha_name, [pair_ty, alpha_ty, fv_ty, @{typ "perm"}, pair_ty] ---> @{typ bool})
+ $ HOLogic.mk_prod (binders, args) $ alpha $ fv $ (Bound 0) $ HOLogic.mk_prod (binders', args'))
end
*}
ML {*
-fun alpha_bn_bm lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn args_in_bn bm =
-case bm of
- BC (_, [], [i]) =>
- let
- val arg = nth args i;
- val arg2 = nth args2 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 alpha_frees (Datatype_Aux.body_index dt)) $ arg $ arg2]
- else [HOLogic.mk_eq (arg, arg2)]
- | SOME (SOME (f : term)) => [(the (AList.lookup (op=) bn_alphabn f)) $ arg $ arg2]
- | SOME NONE => []
- end
-| BC (Lst, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
- fv_frees bn_alphabn @{const_name alpha_lst} x y
-| BC (Set, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
- fv_frees bn_alphabn @{const_name alpha_gen} x y
-| BC (Res, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
- fv_frees bn_alphabn @{const_name alpha_res} x y
+fun mk_alpha_bn_prem alpha_bn_map args args' bodies binder =
+ case binder of
+ (NONE, i) => []
+ | (SOME bn, i) =>
+ if member (op=) bodies i
+ then []
+ else [the (AList.lookup (op=) alpha_bn_map bn) $ (nth args i) $ (nth args' i)]
*}
-
ML {*
-fun alpha_bn lthy dt_descr sorts alpha_frees fv_frees bn_alphabn bclausess
- (alphabn, (_, ith_dtyp, args_in_bns)) =
+fun mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause =
let
- fun alpha_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 names2 = Name.variant_list names (Datatype_Prop.make_tnames Ts);
- val args = map Free (names ~~ Ts);
- val args2 = map Free (names2 ~~ Ts);
- val c = Const (cname, Ts ---> (nth_dtyp dt_descr sorts ith_dtyp));
- val alpha_bn_bm = alpha_bn_bm lthy dt_descr sorts dts args args2 alpha_frees
- fv_frees bn_alphabn args_in_bn;
- val rhs = HOLogic.mk_Trueprop
- (alphabn $ (list_comb (c, args)) $ (list_comb (c, args2)));
- val lhss = map HOLogic.mk_Trueprop (flat (map alpha_bn_bm bclauses))
- in
- Library.foldr Logic.mk_implies (lhss, rhs)
- end;
- val (_, (_, _, constrs)) = nth dt_descr ith_dtyp;
+ fun mk_frees i =
+ let
+ val arg = nth args i
+ val arg' = nth args' i
+ val ty = fastype_of arg
+ in
+ if nth is_rec i
+ then fst (the (AList.lookup (op=) alpha_map ty)) $ arg $ arg'
+ else HOLogic.mk_eq (arg, arg')
+ end
+ fun mk_alpha_fv i =
+ let
+ val ty = fastype_of (nth args i)
+ in
+ case AList.lookup (op=) alpha_map ty of
+ NONE => (HOLogic.eq_const ty, supp_const ty)
+ | SOME (alpha, fv) => (alpha, fv)
+ end
+
in
- map2 alpha_bn_constr constrs (args_in_bns ~~ bclausess)
+ case bclause of
+ BC (_, [], bodies) => map (HOLogic.mk_Trueprop o mk_frees) bodies
+ | BC (bmode, binders, bodies) =>
+ let
+ val (alphas, fvs) = split_list (map mk_alpha_fv bodies)
+ val comp_fv = foldl1 mk_prod_fv fvs
+ val comp_alpha = foldl1 mk_prod_alpha alphas
+ val comp_args = foldl1 HOLogic.mk_prod (map (nth args) bodies)
+ val comp_args' = foldl1 HOLogic.mk_prod (map (nth args') bodies)
+ val comp_binders = mk_binders lthy bmode args binders
+ val comp_binders' = mk_binders lthy bmode args' binders
+ val alpha_prem =
+ mk_alpha_prem bmode comp_fv comp_alpha comp_args comp_args' comp_binders comp_binders'
+ val alpha_bn_prems = flat (map (mk_alpha_bn_prem alpha_bn_map args args' bodies) binders)
+ in
+ map HOLogic.mk_Trueprop (alpha_prem::alpha_bn_prems)
+ end
end
*}
ML {*
-fun alpha_bns lthy dt_descr sorts alpha_frees fv_frees bn_funs bclausesss =
+fun mk_alpha_intros lthy alpha_map alpha_bn_map (constr, ty, arg_tys, is_rec) bclauses =
let
- fun mk_alphabn_free (bn, ith, _) =
- let
- val alphabn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn)));
- val ty = nth_dtyp dt_descr sorts ith;
- val alphabn_type = ty --> ty --> @{typ bool};
- val alphabn_free = Free(alphabn_name, alphabn_type);
- in
- (alphabn_name, alphabn_free)
- end;
- val (alphabn_names, alphabn_frees) = split_list (map mk_alphabn_free bn_funs);
- val bn_alphabn = (map (fn (bn, _, _) => bn) bn_funs) ~~ alphabn_frees
- val bclausessl = map (fn (_, i, _) => nth bclausesss i) bn_funs;
- val eqs = map2 (alpha_bn lthy dt_descr sorts alpha_frees fv_frees bn_alphabn) bclausessl
- (alphabn_frees ~~ bn_funs);
+ val arg_names = Datatype_Prop.make_tnames arg_tys
+ val arg_names' = Name.variant_list arg_names arg_names
+ val args = map Free (arg_names ~~ arg_tys)
+ val args' = map Free (arg_names' ~~ arg_tys)
+ val alpha = fst (the (AList.lookup (op=) alpha_map ty))
+ val concl = HOLogic.mk_Trueprop (alpha $ list_comb (constr, args) $ list_comb (constr, args'))
+ val prems = map (mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args')) bclauses
in
- (bn_alphabn, alphabn_names, eqs)
+ Library.foldr Logic.mk_implies (flat prems, concl)
end
*}
ML {*
-fun alpha_bm lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn bm =
-case bm of
- BC (_, [], [i]) =>
- let
- val arg = nth args i;
- val arg2 = nth args2 i;
- val dt = nth dts i;
- in
- if Datatype_Aux.is_rec_type dt
- then [(nth alpha_frees (Datatype_Aux.body_index dt)) $ arg $ arg2]
- else [HOLogic.mk_eq (arg, arg2)]
- end
-| BC (Lst, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
- fv_frees bn_alphabn @{const_name alpha_lst} x y
-| BC (Set, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
- fv_frees bn_alphabn @{const_name alpha_gen} x y
-| BC (Res, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
- fv_frees bn_alphabn @{const_name alpha_res} x y
+fun mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args') bclause =
+let
+ fun mk_alpha_bn_prem alpha_map alpha_bn_map bn_args (args, args') i =
+ let
+ val arg = nth args i
+ val arg' = nth args' i
+ val ty = fastype_of arg
+ in
+ case AList.lookup (op=) bn_args i of
+ NONE => (case (AList.lookup (op=) alpha_map ty) of
+ NONE => [HOLogic.mk_eq (arg, arg')]
+ | SOME (alpha, _) => [alpha $ arg $ arg'])
+ | SOME (NONE) => []
+ | SOME (SOME bn) => [the (AList.lookup (op=) alpha_bn_map bn) $ arg $ arg']
+ end
+in
+ case bclause of
+ BC (_, [], bodies) =>
+ map HOLogic.mk_Trueprop
+ (flat (map (mk_alpha_bn_prem alpha_map alpha_bn_map bn_args (args, args')) bodies))
+ | _ => mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause
+end
*}
ML {*
-fun alpha lthy dt_descr sorts alpha_frees fv_frees bn_alphabn bclausess (alpha_free, ith_dtyp) =
+fun mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map (bn_args, (constr, _, arg_tys, is_rec)) bclauses =
let
- fun alpha_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 names2 = Name.variant_list names (Datatype_Prop.make_tnames Ts);
- val args = map Free (names ~~ Ts);
- val args2 = map Free (names2 ~~ Ts);
- val c = Const (cname, Ts ---> (nth_dtyp dt_descr sorts ith_dtyp));
- val alpha_bm = alpha_bm lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn
- val rhs = HOLogic.mk_Trueprop
- (alpha_free $ (list_comb (c, args)) $ (list_comb (c, args2)));
- val lhss = map HOLogic.mk_Trueprop (flat (map alpha_bm bclauses))
- in
- Library.foldr Logic.mk_implies (lhss, rhs)
- end;
- val (_, (_, _, constrs)) = nth dt_descr ith_dtyp;
+ val arg_names = Datatype_Prop.make_tnames arg_tys
+ val arg_names' = Name.variant_list arg_names arg_names
+ val args = map Free (arg_names ~~ arg_tys)
+ val args' = map Free (arg_names' ~~ arg_tys)
+ val alpha_bn = the (AList.lookup (op=) alpha_bn_map bn_trm)
+ val concl = HOLogic.mk_Trueprop (alpha_bn $ list_comb (constr, args) $ list_comb (constr, args'))
+ val prems = map (mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args')) bclauses
in
- map2 alpha_constr constrs bclausess
+ Library.foldr Logic.mk_implies (flat prems, concl)
end
*}
ML {*
-fun define_raw_alpha dt_descr sorts bn_funs bclausesss fv_frees lthy =
+fun mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) =
let
- val alpha_names = prefix_dt_names dt_descr sorts "alpha_";
- val alpha_types = map (fn (i, _) =>
- nth_dtyp dt_descr sorts i --> nth_dtyp dt_descr sorts i --> @{typ bool}) dt_descr;
- val alpha_frees = map Free (alpha_names ~~ alpha_types);
+ val nth_constrs_info = nth constrs_info bn_n
+ val nth_bclausess = nth bclausesss bn_n
+in
+ map2 (mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
+end
+*}
- val (bn_alphabn, alpha_bn_names, alpha_bn_eqs) =
- alpha_bns lthy dt_descr sorts alpha_frees fv_frees bn_funs bclausesss
+ML {*
+fun define_raw_alpha descr sorts bn_info bclausesss fvs fv_bns lthy =
+let
+ val alpha_names = prefix_dt_names descr sorts "alpha_"
+ val alpha_arg_tys = all_dtyps descr sorts
+ val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) alpha_arg_tys
+ val alpha_frees = map Free (alpha_names ~~ alpha_tys)
+ val alpha_map = alpha_arg_tys ~~ (alpha_frees ~~ fvs)
- val alpha_bns = map snd bn_alphabn;
- val alpha_bn_types = map fastype_of alpha_bns;
+ 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 alpha_bn_names = map (prefix "alpha_") bn_names
+ val alpha_bn_arg_tys = map (fn i => nth_dtyp descr sorts i) bn_tys
+ val alpha_bn_tys = map (fn ty => [ty, ty] ---> @{typ "bool"}) alpha_bn_arg_tys
+ val alpha_bn_frees = map Free (alpha_bn_names ~~ alpha_bn_tys)
+ val alpha_bn_map = bns ~~ alpha_bn_frees
- val alpha_nums = 0 upto (length alpha_frees - 1)
+ val constrs_info = all_dtyp_constrs_types descr sorts
- val alpha_eqs = map2 (alpha lthy dt_descr sorts alpha_frees fv_frees bn_alphabn) bclausesss
- (alpha_frees ~~ alpha_nums);
+ val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) constrs_info bclausesss
+ val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss) bn_info
val all_alpha_names = map2 (fn s => fn ty => ((Binding.name s, ty), NoSyn))
- (alpha_names @ alpha_bn_names) (alpha_types @ alpha_bn_types)
- val all_alpha_eqs = map (pair Attrib.empty_binding) (flat alpha_eqs @ flat alpha_bn_eqs)
-
+ (alpha_names @ alpha_bn_names) (alpha_tys @ alpha_bn_tys)
+ val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros)
+
val (alphas, lthy') = Inductive.add_inductive_i
{quiet_mode = true, verbose = false, alt_name = Binding.empty,
coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
- all_alpha_names [] all_alpha_eqs [] lthy
+ all_alpha_names [] all_alpha_intros [] lthy
- val alpha_ts_loc = #preds alphas;
+ val alpha_trms_loc = #preds alphas;
val alpha_induct_loc = #raw_induct alphas;
val alpha_intros_loc = #intrs alphas;
val alpha_cases_loc = #elims alphas;
- val morphism = ProofContext.export_morphism lthy' lthy;
+ val phi = ProofContext.export_morphism lthy' lthy;
- val alpha_ts = map (Morphism.term morphism) alpha_ts_loc;
- val alpha_induct = Morphism.thm morphism alpha_induct_loc;
- val alpha_intros = Morphism.fact morphism alpha_intros_loc
- val alpha_cases = Morphism.fact morphism alpha_cases_loc
+ val alpha_trms = map (Morphism.term phi) alpha_trms_loc;
+ val alpha_induct = Morphism.thm phi alpha_induct_loc;
+ val alpha_intros = map (Morphism.thm phi) alpha_intros_loc
+ val alpha_cases = map (Morphism.thm phi) alpha_cases_loc
in
- (alpha_ts, alpha_intros, alpha_cases, alpha_induct, lthy')
+ (alpha_trms, alpha_intros, alpha_cases, alpha_induct, lthy')
end
-handle UnequalLengths => error "Main"
*}
+ML {* ProofContext.export_morphism *}
+
end