# HG changeset patch # User Cezary Kaliszyk # Date 1268813907 -3600 # Node ID 0c5dfd2866bb955f6b09ddf8d0687a7159ddfecd # Parent d18defacda25f82455682903d28e426a3d5845a0# Parent 416c9c5a1126a594be91564fc8daa45ba1d5b374 merge diff -r d18defacda25 -r 0c5dfd2866bb Nominal/Abs.thy --- 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) \gen (\(x1, y1) (x2, y2). R1 x1 x2 \ R2 y1 y2) (\(a, b). f1 a \ f2 b) pi (cs, y1, y2) = + (f1 x1 \ f2 x2 - bs = f1 y1 \ f2 y2 - cs \ (f1 x1 \ f2 x2 - bs) \* pi \ R1 (pi \ x1) y1 \ R2 (pi \ x2) y2)" +by (simp add: alpha_gen) + end diff -r d18defacda25 -r 0c5dfd2866bb Nominal/Fv.thy --- 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 "\(x, y, z). \(x', y', z'). R x x' \ R2 y y' \ R3 z z'"} *} + +(* Given [R1, R2, R3] creates %(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 = 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 \ 'a \ bool"}, @{term "R2 :: 'b \ 'b \ bool"}, @{term "R3 :: 'b \ 'b \ bool"}]) *} + ML {* fun add_perm (p1, p2) = Const(@{const_name plus}, @{typ "perm \ perm \ 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 diff -r d18defacda25 -r 0c5dfd2866bb Nominal/Parser.thy --- 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)))))