--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/NewAlpha.thy Thu Apr 29 17:52:19 2010 +0200
@@ -0,0 +1,249 @@
+theory NewAlpha
+imports "NewFv"
+begin
+
+(* Given [fv1, fv2, fv3]
+ produces %(x, y, z). fv1 x u fv2 y u fv3 z *)
+ML {*
+fun mk_compound_fv fvs =
+let
+ val nos = (length fvs - 1) downto 0;
+ val fvs_applied = map (fn (fv, no) => fv $ Bound no) (fvs ~~ nos);
+ val fvs_union = mk_union fvs_applied;
+ val (tyh :: tys) = rev (map (domain_type o fastype_of) fvs);
+ fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t))
+in
+ fold fold_fun tys (Abs ("", tyh, fvs_union))
+end;
+*}
+
+(* Given [R1, R2, R3]
+ produces %(x,x'). %(y,y'). %(z,z'). R x x' \<and> R y y' \<and> R z z' *)
+ML {*
+fun mk_compound_alpha Rs =
+let
+ val nos = (length Rs - 1) downto 0;
+ val nos2 = (2 * length Rs - 1) downto length Rs;
+ val Rs_applied = map (fn (R, (no2, no)) => R $ Bound no2 $ Bound no)
+ (Rs ~~ (nos2 ~~ nos));
+ val Rs_conj = foldr1 HOLogic.mk_conj Rs_applied;
+ val (tyh :: tys) = rev (map (domain_type o fastype_of) Rs);
+ fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t))
+ val abs_rhs = fold fold_fun tys (Abs ("", tyh, Rs_conj))
+in
+ fold fold_fun tys (Abs ("", tyh, abs_rhs))
+end;
+*}
+
+ML {*
+fun mk_pair (fst, snd) =
+let
+ val ty1 = fastype_of fst
+ val ty2 = fastype_of snd
+ val c = HOLogic.pair_const ty1 ty2
+in
+ c $ fst $ snd
+end;
+*}
+
+ML {*
+fun alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees fv_frees
+ bn_alphabn alpha_const binds bodys =
+let
+ val thy = ProofContext.theory_of lthy;
+ fun bind_set args (NONE, no) = setify thy (nth args no)
+ | bind_set args (SOME f, no) = f $ (nth args no)
+ fun bind_lst args (NONE, no) = listify thy (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 mk_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 = mk_pair (lhs_binds, lhs_bodys);
+ val rhs = mk_pair (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 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 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
+in
+ case binds of
+ [(SOME bn, i)] => if i mem bodys then [t]
+ else [t, ((the (AList.lookup (op=) bn_alphabn bn)) $ nth args i $ nth args2 i)]
+ | _ => [t]
+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
+ BEmy 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
+| BLst (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
+ fv_frees bn_alphabn @{const_name alpha_lst} x y
+| BSet (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
+ fv_frees bn_alphabn @{const_name alpha_gen} x y
+| BRes (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
+ fv_frees bn_alphabn @{const_name alpha_res} x y
+*}
+
+
+ML {*
+fun alpha_bn lthy dt_descr sorts alpha_frees fv_frees bn_alphabn bclausess
+ (alphabn, (_, ith_dtyp, args_in_bns)) =
+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;
+in
+ map2 alpha_bn_constr constrs (args_in_bns ~~ bclausess)
+end
+*}
+
+ML {*
+fun alpha_bns lthy dt_descr sorts alpha_frees fv_frees bn_funs bclausesss =
+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);
+in
+ (bn_alphabn, alphabn_names, eqs)
+end
+*}
+
+ML {*
+fun alpha_bm lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn bm =
+case bm of
+ BEmy 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
+| BLst (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
+ fv_frees bn_alphabn @{const_name alpha_lst} x y
+| BSet (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
+ fv_frees bn_alphabn @{const_name alpha_gen} x y
+| BRes (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
+ fv_frees bn_alphabn @{const_name alpha_res} x y
+*}
+
+ML {*
+fun alpha lthy dt_descr sorts alpha_frees fv_frees bn_alphabn bclausess (alpha_free, ith_dtyp) =
+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;
+in
+ map2 alpha_constr constrs bclausess
+end
+*}
+
+ML {*
+fun define_raw_alpha (dt_info : Datatype_Aux.info) bn_funs bclausesss fv_frees lthy =
+let
+ val {descr as dt_descr, sorts, ...} = dt_info;
+
+ 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 (bn_alphabn, alpha_bn_names, alpha_bn_eqs) =
+ alpha_bns lthy dt_descr sorts alpha_frees fv_frees bn_funs bclausesss
+
+ val alpha_bns = map snd bn_alphabn;
+ val alpha_bn_types = map fastype_of alpha_bns;
+
+ val alpha_nums = 0 upto (length alpha_frees - 1)
+
+ val alpha_eqs = map2 (alpha lthy dt_descr sorts alpha_frees fv_frees bn_alphabn) bclausesss
+ (alpha_frees ~~ alpha_nums);
+
+ 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)
+
+ 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
+in
+ (alphas, lthy')
+end
+*}
+
+end
--- a/Nominal/NewParser.thy Thu Apr 29 16:59:33 2010 +0200
+++ b/Nominal/NewParser.thy Thu Apr 29 17:52:19 2010 +0200
@@ -2,7 +2,7 @@
imports "../Nominal-General/Nominal2_Base"
"../Nominal-General/Nominal2_Eqvt"
"../Nominal-General/Nominal2_Supp"
- "Perm" "NewFv"
+ "Perm" "NewFv" "NewAlpha"
begin
section{* Interface for nominal_datatype *}
@@ -278,8 +278,9 @@
val lthy3 = Theory_Target.init NONE thy;
val ((fv, fvbn), info, lthy4) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3;
+ val (alpha, lthy5) = define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy4;
in
- ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy4)
+ ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy5)
end
*}
@@ -466,6 +467,7 @@
| "bn (P2 p1 p2) = bn p1 \<union> bn p2"
thm fv_lam_raw.simps fv_pt_raw.simps fv_bn_raw.simps
+thm alpha_lam_raw_alpha_pt_raw_alpha_bn_raw.intros
nominal_datatype exp =
EVar name
@@ -516,6 +518,7 @@
thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars]
thm permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[no_vars]
thm fv_exp_raw.simps fv_fnclause_raw.simps fv_fnclauses_raw.simps fv_lrb_raw.simps fv_lrbs_raw.simps fv_pat_raw.simps fv_b_lrbs_raw.simps fv_b_pat_raw.simps fv_b_fnclauses_raw.simps fv_b_lrb_raw.simps fv_b_fnclause_raw.simps
+thm alpha_exp_raw_alpha_fnclause_raw_alpha_fnclauses_raw_alpha_lrb_raw_alpha_lrbs_raw_alpha_pat_raw_alpha_b_lrbs_raw_alpha_b_pat_raw_alpha_b_fnclauses_raw_alpha_b_lrb_raw_alpha_b_fnclause_raw.intros
nominal_datatype ty =
Var "name"
@@ -524,6 +527,7 @@
nominal_datatype tys =
All xs::"name fset" ty::"ty_raw" bind_res xs in ty
thm fv_tys_raw.simps
+thm alpha_tys_raw.intros
(* some further tests *)