--- a/Nominal/Abs.thy Wed Mar 17 08:07:25 2010 +0100
+++ b/Nominal/Abs.thy Wed Mar 17 09:18:27 2010 +0100
@@ -748,6 +748,22 @@
apply (simp add: swap_fresh_fresh)
done
+(* TODO: The following lemmas can be moved somewhere... *)
+lemma split_rsp2[quot_respect]: "((R1 ===> R2 ===> prod_rel R1 R2 ===> op =) ===>
+ prod_rel R1 R2 ===> prod_rel R1 R2 ===> op =) split split"
+ by auto
+
+lemma split_prs2[quot_preserve]:
+ assumes q1: "Quotient R1 Abs1 Rep1"
+ and q2: "Quotient R2 Abs2 Rep2"
+ shows "((Abs1 ---> Abs2 ---> prod_fun Abs1 Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> prod_fun Rep1 Rep2 ---> id) split = split"
+ by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+
+lemma alpha_gen2:
+ "(bs, x1, x2) \<approx>gen (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (cs, y1, y2) =
+ (f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2)"
+by (simp add: alpha_gen)
+
end
--- a/Nominal/Fv.thy Wed Mar 17 08:07:25 2010 +0100
+++ b/Nominal/Fv.thy Wed Mar 17 09:18:27 2010 +0100
@@ -139,9 +139,42 @@
val c = HOLogic.pair_const ty1 ty2
in c $ fst $ snd
end;
+*}
+(* Given [fv1, fv2, fv3] creates %(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;
*}
+ML {* @{term "\<lambda>(x, y, z). \<lambda>(x', y', z'). R x x' \<and> R2 y y' \<and> R3 z z'"} *}
+
+(* Given [R1, R2, R3] creates %(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 = mk_conjl 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 {* cterm_of @{theory} (mk_compound_alpha [@{term "R :: 'a \<Rightarrow> 'a \<Rightarrow> bool"}, @{term "R2 :: 'b \<Rightarrow> 'b \<Rightarrow> bool"}, @{term "R3 :: 'b \<Rightarrow> 'b \<Rightarrow> bool"}]) *}
+
ML {* fun add_perm (p1, p2) = Const(@{const_name plus}, @{typ "perm \<Rightarrow> perm \<Rightarrow> perm"}) $ p1 $ p2 *}
ML {*
@@ -328,7 +361,9 @@
let
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 ((_, _, j), _) => j = arg_no | _ => false) bind_pis;
+ val rel_has_binds = filter (fn ((NONE, _, j), _) => j = arg_no
+ | ((SOME (_, false), _, j), _) => j = arg_no
+ | _ => false) bind_pis;
in
case (rel_in_simp_binds, rel_in_comp_binds, rel_has_binds) of
([], [], []) =>
@@ -340,14 +375,27 @@
if is_rec then
let
val (rbinds, rpis) = split_list rel_in_comp_binds
+ val bound_in_nos = map (fn (_, _, i) => i) rbinds
+ val bound_in_ty_nos = map (fn i => body_index (nth dts i)) bound_in_nos;
+ val bound_args = arg :: map (nth args) bound_in_nos;
+ val bound_args2 = arg2 :: map (nth args2) bound_in_nos;
+ fun bound_in args (_, _, i) = nth args i;
val lhs_binds = fv_binds args rbinds
- val lhs = mk_pair (lhs_binds, arg);
+ val lhs_arg = foldr1 HOLogic.mk_prod bound_args
+ val lhs = mk_pair (lhs_binds, lhs_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);
+ val rhs_arg = foldr1 HOLogic.mk_prod bound_args2;
+ val rhs = mk_pair (rhs_binds, rhs_arg);
+ val _ = tracing (PolyML.makestring bound_in_ty_nos);
+ val fvs = map (nth fv_frees) ((body_index dt) :: bound_in_ty_nos);
+ val _ = tracing (PolyML.makestring fvs);
+ val fv = mk_compound_fv fvs;
+ val alphas = map (nth alpha_frees) ((body_index dt) :: bound_in_ty_nos);
+ val _ = tracing (PolyML.makestring alphas);
+ val alpha = mk_compound_alpha alphas;
val pi = foldr1 add_perm (distinct (op =) rpis);
val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
+ val _ = tracing (PolyML.makestring alpha_gen_pre);
val alpha_gen = Syntax.check_term lthy alpha_gen_pre
in
alpha_gen
--- a/Nominal/Parser.thy Wed Mar 17 08:07:25 2010 +0100
+++ b/Nominal/Parser.thy Wed Mar 17 09:18:27 2010 +0100
@@ -416,9 +416,11 @@
val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15;
val q_bn = map (lift_thm lthy16) raw_bn_eqs;
val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16;
- val inj_unfolded = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) alpha_inj
- val q_inj_pre = map (lift_thm lthy17) inj_unfolded;
- val q_inj = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_inj_pre
+ val inj_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alpha_gen2}) alpha_inj
+ val inj_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) inj_unfolded1
+ val q_inj_pre1 = map (lift_thm lthy17) inj_unfolded2;
+ val q_inj_pre2 = map (Local_Defs.fold lthy17 @{thms alpha_gen2}) q_inj_pre1
+ val q_inj = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_inj_pre2
val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17;
val rel_dists = flat (map (distinct_rel lthy18 alpha_cases)
(rel_distinct ~~ (List.take (alpha_ts, (length dts)))))