diff -r 8557af71724e -r 0203cd5cfd6c Nominal/Fv.thy --- a/Nominal/Fv.thy Mon Mar 01 14:26:14 2010 +0100 +++ b/Nominal/Fv.thy Mon Mar 01 16:04:03 2010 +0100 @@ -1,5 +1,5 @@ theory Fv -imports "Nominal2_Atoms" "Abs" +imports "Nominal2_Atoms" "Abs" "Perm" (* For testing *) begin (* Bindings are given as a list which has a length being equal @@ -54,6 +54,7 @@ in the database. *) +(* TODO: should be const_name union *) ML {* open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *); (* TODO: It is the same as one in 'nominal_atoms' *) @@ -64,7 +65,12 @@ fold (fn a => fn b => if a = noatoms then b else if b = noatoms then a else - HOLogic.mk_binop @{const_name union} (a, b)) (rev sets) noatoms; + HOLogic.mk_binop "Set.union" (a, b)) (rev sets) noatoms; + fun mk_conjl props = + fold (fn a => fn b => + if a = @{term True} then b else + if b = @{term True} then a else + HOLogic.mk_conj (a, b)) props @{term True}; fun mk_diff a b = if b = noatoms then a else if b = a then noatoms else @@ -90,6 +96,8 @@ *} +ML {* fun add_perm (p1, p2) = Const(@{const_name plus}, @{typ "perm \ perm \ perm"}) $ p1 $ p2 *} + (* TODO: Notice datatypes without bindings and replace alpha with equality *) ML {* fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall lthy = @@ -105,58 +113,75 @@ "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); - fun fv_alpha_constr i (cname, dts) bindcs = + fun fv_alpha_constr ith_dtyp (cname, dts) bindcs = let val Ts = map (typ_of_dtyp descr sorts) dts; - val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); + val bindslen = length bindcs + val pi_strs = replicate bindslen "pi" + val pis = map (fn ps => Free (ps, @{typ perm})) pi_strs; + val bind_pis = bindcs ~~ pis; + val names = Name.variant_list pi_strs (Datatype_Prop.make_tnames Ts); val args = map Free (names ~~ Ts); - val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts); + val names2 = Name.variant_list (pi_strs @ names) (Datatype_Prop.make_tnames Ts); val args2 = map Free (names2 ~~ Ts); - val c = Const (cname, Ts ---> (nth_dtyp i)); - val fv_c = nth fv_frees i; - val alpha = nth alpha_frees i; - fun fv_bind args (NONE, i) = + val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); + val fv_c = nth fv_frees ith_dtyp; + val alpha = nth alpha_frees ith_dtyp; + val arg_nos = 0 upto (length dts - 1) + fun fv_bind args (NONE, i, _) = if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else (* TODO we assume that all can be 'atomized' *) if (is_funtype o fastype_of) (nth args i) then mk_atoms (nth args i) else mk_single_atom (nth args i) - | fv_bind args (SOME f, i) = f $ (nth args i); - fun fv_arg ((dt, x), bindxs) = + | fv_bind args (SOME f, i, _) = f $ (nth args i); + fun fv_binds args relevant = mk_union (map (fv_bind args) relevant) + fun fv_arg ((dt, x), arg_no) = let val arg = if is_rec_type dt then nth fv_frees (body_index dt) $ x else (* TODO: we just assume everything can be 'atomized' *) if (is_funtype o fastype_of) x then mk_atoms x else - HOLogic.mk_set @{typ atom} [mk_atom (fastype_of x) $ x] - val sub = mk_union (map (fv_bind args) bindxs) + HOLogic.mk_set @{typ atom} [mk_atom (fastype_of x) $ x]; + (* If i = j then we generate it only once *) + val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs; + val sub = fv_binds args relevant in mk_diff arg sub end; val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq - (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs)))) + (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos)))) val alpha_rhs = HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2))); - fun alpha_arg ((dt, bindxs), (arg, arg2)) = - if bindxs = [] 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 *) - val lhs_binds = mk_union (map (fv_bind args) bindxs); - val lhs = mk_pair (lhs_binds, arg); - val rhs_binds = mk_union (map (fv_bind args2) bindxs); - val rhs = mk_pair (rhs_binds, arg2); - val alpha = nth alpha_frees (body_index dt); - val fv = nth fv_frees (body_index dt); - val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ (Free ("pi", @{typ perm})) $ rhs; - val alpha_gen_t = Syntax.check_term lthy alpha_gen_pre - in - HOLogic.mk_exists ("pi", @{typ perm}, alpha_gen_t) - (* TODO Add some test that is makes sense *) - end else @{term "True"} - val alpha_lhss = map (HOLogic.mk_Trueprop o alpha_arg) (dts ~~ bindcs ~~ (args ~~ args2)) - val alpha_eq = Logic.list_implies (alpha_lhss, alpha_rhs) + fun alpha_arg ((dt, arg_no), (arg, arg2)) = + let + val relevant = filter (fn ((_, i, j), _) => i = arg_no orelse j = arg_no) 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 *) + val (rbinds, rpis) = split_list relevant + val lhs_binds = fv_binds args rbinds + val lhs = mk_pair (lhs_binds, arg); + val rhs_binds = fv_binds args2 rbinds; + val rhs = mk_pair (rhs_binds, arg2); + val alpha = nth alpha_frees (body_index dt); + val fv = nth fv_frees (body_index dt); + (* TODO: check that pis have empty intersection *) + val pi = foldr1 add_perm rpis; + val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; + in + Syntax.check_term lthy alpha_gen_pre + (* TODO Add some test that is makes sense *) + end else @{term "True"} + end + val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2)) + val alpha_lhss = mk_conjl alphas + val alpha_lhss_ex = + fold (fn pi_str => fn t => HOLogic.mk_exists (pi_str, @{typ perm}, t)) pi_strs alpha_lhss + val alpha_eq = Logic.mk_implies (HOLogic.mk_Trueprop alpha_lhss_ex, alpha_rhs) in (fv_eq, alpha_eq) end;