diff -r baa67b07f436 -r 4eaae533efc3 Nominal/Fv.thy --- a/Nominal/Fv.thy Wed Mar 10 12:48:38 2010 +0100 +++ b/Nominal/Fv.thy Wed Mar 10 12:48:55 2010 +0100 @@ -193,6 +193,51 @@ end *} +ML {* +fun alpha_bn thy (dt_info : Datatype_Aux.info) alpha_frees ((bn, ith_dtyp, args_in_bns), is_rec) = +let + val {descr, sorts, ...} = dt_info; + fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); + val alpha_bn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn))); + val alpha_bn_type = @{typ perm} --> nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool} + val alpha_bn_free = Free(alpha_bn_name, alpha_bn_type); + fun alpha_bn_constr (cname, dts) args_in_bn = + let + val Ts = map (typ_of_dtyp descr sorts) dts; + val pi = Free("pi", @{typ perm}) + val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); + val names2 = Name.variant_list ("pi" :: 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 ith_dtyp)); + val rhs = HOLogic.mk_Trueprop + (alpha_bn_free $ pi $ (list_comb (c, args)) $ (list_comb (c, args2))); + fun lhs_arg ((dt, arg_no), (arg, arg2)) = + let + val argty = fastype_of arg; + val permute = Const (@{const_name permute}, @{typ perm} --> argty --> argty); + val permarg = if is_rec then permute $ pi $ arg else arg + in + if is_rec_type dt then + if arg_no mem args_in_bn then alpha_bn_free $ pi $ arg $ arg2 + else (nth alpha_frees (body_index dt)) $ permarg $ arg2 + else + if arg_no mem args_in_bn then @{term True} + else HOLogic.mk_eq (permarg, arg2) + end + val arg_nos = 0 upto (length dts - 1) + val lhss = mk_conjl (map lhs_arg (dts ~~ arg_nos ~~ (args ~~ args2))) + val eq = Logic.mk_implies (HOLogic.mk_Trueprop lhss, rhs) + in + eq + end + val (_, (_, _, constrs)) = nth descr ith_dtyp; + val eqs = map2i alpha_bn_constr constrs args_in_bns +in + ((bn, alpha_bn_free), (alpha_bn_name, eqs)) +end +*} + ML {* fn x => split_list(flat x) *} ML {* fn x => apsnd flat (split_list (map split_list x)) *} (* TODO: Notice datatypes without bindings and replace alpha with equality *) @@ -209,12 +254,17 @@ val nr_bns = non_rec_binds bindsall; val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns; val (bn_fv_bns, fv_bn_names_eqs) = split_list (map (fv_bn thy dt_info fv_frees) rel_bns); - val fv_bns = map snd bn_fv_bns; val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs; val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => "alpha_" ^ name_of_typ (nth_dtyp i)) descr); val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr; val alpha_frees = map Free (alpha_names ~~ alpha_types); + (* We assume that a bn is either recursive or not *) + val bns_rec = map (fn (bn, _, _) => not (bn mem nr_bns)) bns; + val (bn_alpha_bns, alpha_bn_names_eqs) = split_list (map (alpha_bn thy dt_info alpha_frees) (bns ~~ bns_rec)) + val (alpha_bn_names, alpha_bn_eqs) = split_list alpha_bn_names_eqs; + val alpha_bn_frees = map snd bn_alpha_bns; + val alpha_bn_types = map fastype_of alpha_bn_frees; fun fv_alpha_constr ith_dtyp (cname, dts) bindcs = let val Ts = map (typ_of_dtyp descr sorts) dts; @@ -269,14 +319,26 @@ HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2))); fun alpha_arg ((dt, arg_no), (arg, arg2)) = let - val relevant = filter (fn ((_, i, j), _) => i = arg_no orelse j = arg_no) bind_pis; + val rel_in_simp_binds = filter (fn ((NONE, i, _), _) => i = arg_no | _ => false) bind_pis; + val rel_in_comp_binds = filter (fn ((SOME _, i, _), _) => i = arg_no | _ => false) bind_pis; + val rel_has_binds = filter (fn ((SOME _, _, j), _) => j = arg_no | _ => false) bind_pis; in - if relevant = [] then ( - if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2) - else (HOLogic.mk_eq (arg, arg2))) - else - if is_rec_type dt then let - (* THE HARD CASE *) + case (rel_in_simp_binds, rel_in_comp_binds, rel_has_binds) of + ([], [], []) => + if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2) + else (HOLogic.mk_eq (arg, arg2)) + (* TODO: if more then check and accept *) + | (_, [], []) => @{term True} + | ([], [(((SOME (bn, _)), _, _), pi)], []) => + let + val alpha_bn = nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns) $ pi $ arg $ arg2 + val ty = fastype_of (bn $ arg) + val permute = Const(@{const_name permute}, @{typ perm} --> ty --> ty) + in + HOLogic.mk_conj (alpha_bn, HOLogic.mk_eq (permute $ pi $ (bn $ arg), (bn $ arg2))) + end + | ([], [], relevant) => + let val (rbinds, rpis) = split_list relevant val lhs_binds = fv_binds args rbinds val lhs = mk_pair (lhs_binds, arg); @@ -290,10 +352,10 @@ (* val pi_supps = map ((curry op $) @{term "supp :: perm \ atom set"}) rpis; val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"}) *) in - (*if length pi_supps > 1 then HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*) +(* if length pi_supps > 1 then HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*) alpha_gen - (* TODO Add some test that is makes sense *) - end else @{term "True"} + end + | _ => error "Fv.alpha: not supported binding structure" end val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2)) val alpha_lhss = mk_conjl alphas @@ -307,7 +369,7 @@ val fveqs_alphaeqs = map2i fv_alpha_eq descr (gather_binds bindsall) val (fv_eqs_perfv, alpha_eqs) = apsnd flat (split_list (map split_list fveqs_alphaeqs)) val rel_bns_nos = map (fn (_, i, _) => i) rel_bns; - fun filter_fun (a, b) = b mem rel_bns_nos; + fun filter_fun (_, b) = b mem rel_bns_nos; val all_fvs = (fv_names ~~ fv_eqs_perfv) ~~ (0 upto (length fv_names - 1)) val (fv_names_fst, fv_eqs_fst) = apsnd flat (split_list (map fst (filter_out filter_fun all_fvs))) val (fv_names_snd, fv_eqs_snd) = apsnd flat (split_list (map fst (filter filter_fun all_fvs))) @@ -325,38 +387,35 @@ 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} - (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) [] - (add_binds alpha_eqs) [] lthy'') + (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) (alpha_names @ alpha_bn_names) + (alpha_types @ alpha_bn_types)) [] + (add_binds (alpha_eqs @ flat alpha_bn_eqs)) [] lthy'') + val all_fvs = (fst fvs @ fst fvs2, snd fvs @ snd fvs2) in - ((fvs, alphas), lthy''') + ((all_fvs, alphas), lthy''') end *} (* atom_decl name - datatype lam = VAR "name" | APP "lam" "lam" | LET "bp" "lam" and bp = BP "name" "lam" - primrec bi::"bp \ atom set" where "bi (BP x t) = {atom x}" - setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.lam") 2 *} - - local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.lam") - [[[], [], [(SOME (@{term bi}, false), 0, 1)]], [[]]] [(@{term bi}, 1, [[0]])] *} + [[[], [], [(SOME (@{term bi}, true), 0, 1)]], [[]]] [(@{term bi}, 1, [[0]])] *} print_theorems *) -(* +(*atom_decl name datatype rtrm1 = rVr1 "name" | rAp1 "rtrm1" "rtrm1" @@ -366,24 +425,38 @@ BUnit | BVr "name" | BPr "bp" "bp" - -(* to be given by the user *) - primrec bv1 where "bv1 (BUnit) = {}" | "bv1 (BVr x) = {atom x}" | "bv1 (BPr bp1 bp2) = (bv1 bp1) \ (bv1 bp1)" - -setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Fv.rtrm1", "Fv.bp"] *} - -local_setup {* define_fv_alpha "Fv.rtrm1" - [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]], - [[], [[]], [[], []]]] *} +setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.rtrm1") 2 *} +local_setup {* + snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.rtrm1") + [[[], [], [(NONE, 0, 1)], [(SOME (@{term bv1}, false), 0, 2)]], + [[], [], []]] [(@{term bv1}, 1, [[], [0], [0, 1]])] *} print_theorems *) +(* +atom_decl name +datatype rtrm5 = + rVr5 "name" +| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)" +and rlts = + rLnil +| rLcons "name" "rtrm5" "rlts" +primrec + rbv5 +where + "rbv5 rLnil = {}" +| "rbv5 (rLcons n t ltl) = {atom n} \ (rbv5 ltl)" +setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.rtrm5") 2 *} +local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.rtrm5") + [[[], [(SOME (@{term rbv5}, false), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *} +print_theorems +*) ML {* fun alpha_inj_tac dist_inj intrs elims =