--- 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 \<Rightarrow> perm \<Rightarrow> 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;