# HG changeset patch # User Cezary Kaliszyk # Date 1272556339 -7200 # Node ID e306247b5ce3c48f866dbceccf8576e6b105851b # Parent 45721f92e471fbc3b307889db2e620ba855e31cc New Alpha. diff -r 45721f92e471 -r e306247b5ce3 Nominal/NewAlpha.thy --- /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' \ R y y' \ 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 \ atom list \ 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 diff -r 45721f92e471 -r e306247b5ce3 Nominal/NewParser.thy --- 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 \ 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 *)