# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269278969 -3600
# Node ID 6b1eea8dcdc03c58691acab3a9fed6103777b05e
# Parent  7b8f570b24506c09bee91033189b79427ff51e24
equivp_cheat can be removed for all one-permutation examples.

diff -r 7b8f570b2450 -r 6b1eea8dcdc0 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Mon Mar 22 17:21:27 2010 +0100
+++ b/Nominal/Abs.thy	Mon Mar 22 18:29:29 2010 +0100
@@ -642,7 +642,7 @@
   and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
   shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)"
   using b c apply -
-  apply(simp add: alpha_gen.simps)
+  apply(simp add: alpha_gen)
   apply(erule conjE)+
   apply(simp add: fresh_star_plus)
   apply(drule_tac x="- pia \<bullet> sa" in spec)
@@ -655,6 +655,40 @@
   apply(simp)
   done
 
+lemma alpha_gen_compose_trans2:
+  fixes pi pia
+  assumes b: "(aa, (t1, t2)) \<approx>gen
+    (\<lambda>(b, a) (d, c). R1 b d \<and> (\<forall>z. R1 d z \<longrightarrow> R1 b z) \<and> R2 a c \<and> (\<forall>z. R2 c z \<longrightarrow> R2 a z))
+    (\<lambda>(b, a). fv_a b \<union> fv_b a) pi (ab, (ta1, ta2))"
+  and c: "(ab, (ta1, ta2)) \<approx>gen (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
+    pia (ac, (sa1, sa2))"
+  and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
+  and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
+  shows "(aa, (t1, t2)) \<approx>gen (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
+    (pia + pi) (ac, (sa1, sa2))"
+  using b c apply -
+  apply(simp add: alpha_gen2)
+  apply(simp add: alpha_gen)
+  apply(erule conjE)+
+  apply(simp add: fresh_star_plus)
+  apply(drule_tac x="- pia \<bullet> sa1" in spec)
+  apply(drule mp)
+  apply(rotate_tac 5)
+  apply(drule_tac pi="- pia" in r1)
+  apply(simp)
+  apply(rotate_tac -1)
+  apply(drule_tac pi="pia" in r1)
+  apply(simp)
+  apply(drule_tac x="- pia \<bullet> sa2" in spec)
+  apply(drule mp)
+  apply(rotate_tac 6)
+  apply(drule_tac pi="- pia" in r2)
+  apply(simp)
+  apply(rotate_tac -1)
+  apply(drule_tac pi="pia" in r2)
+  apply(simp)
+  done
+
 lemma alpha_gen_compose_eqvt:
   fixes  pia
   assumes b: "(g d, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia (g e, s)"
diff -r 7b8f570b2450 -r 6b1eea8dcdc0 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Mon Mar 22 17:21:27 2010 +0100
+++ b/Nominal/Fv.thy	Mon Mar 22 18:29:29 2010 +0100
@@ -679,19 +679,24 @@
 *}
 
 ML {*
-fun build_alpha_refl_gl fv_alphas_lst =
+fun build_alpha_refl_gl fv_alphas_lst alphas =
 let
-  val (fvs_alphas, ls) = split_list fv_alphas_lst;
+  val (fvs_alphas, _) = split_list fv_alphas_lst;
   val (_, alpha_ts) = split_list fvs_alphas;
   val tys = map (domain_type o fastype_of) alpha_ts;
   val names = Datatype_Prop.make_tnames tys;
   val args = map Free (names ~~ tys);
+  fun find_alphas ty x =
+    domain_type (fastype_of x) = ty;
   fun mk_alpha_refl arg (_, alpha) = alpha $ arg $ arg;
-  fun refl_eq_arg ((alpha, arg), l) =
-    foldr1 HOLogic.mk_conj
-      ((alpha $ arg $ arg) ::
-       (map (mk_alpha_refl arg) l))
-  val eqs = map refl_eq_arg ((alpha_ts ~~ args) ~~ ls)
+  fun refl_eq_arg (ty, arg) =
+    let
+      val rel_alphas = filter (find_alphas ty) alphas;
+    in
+      map (fn x => x $ arg $ arg) rel_alphas
+    end;
+  (* Flattening loses the induction structure *)
+  val eqs = map (foldr1 HOLogic.mk_conj) (map refl_eq_arg (tys ~~ args))
 in
   (names, HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj eqs))
 end
@@ -708,9 +713,9 @@
 *}
 
 ML {*
-fun build_alpha_refl fv_alphas_lst induct eq_iff ctxt =
+fun build_alpha_refl fv_alphas_lst alphas induct eq_iff ctxt =
 let
-  val (names, gl) = build_alpha_refl_gl fv_alphas_lst;
+  val (names, gl) = build_alpha_refl_gl fv_alphas_lst alphas;
   val refl_conj = Goal.prove ctxt names [] gl (fn _ => reflp_tac induct eq_iff ctxt 1);
 in
   HOLogic.conj_elims refl_conj
@@ -825,23 +830,25 @@
   split_conjs THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conjs
   THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct)))
   THEN_ALL_NEW split_conjs THEN_ALL_NEW
-  TRY o (etac @{thm alpha_gen_compose_trans} THEN' RANGE[atac]) THEN_ALL_NEW
+  TRY o (etac @{thm alpha_gen_compose_trans2} ORELSE' etac @{thm alpha_gen_compose_trans}) THEN_ALL_NEW
   (asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ eqvt @ term_inj @ distinct)))
 *}
 
-lemma transp_aux:
+lemma transpI:
   "(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> transp R"
   unfolding transp_def
   by blast
 
 ML {*
 fun equivp_tac reflps symps transps =
+  let val _ = tracing (PolyML.makestring (reflps, symps, transps)) in
   simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def})
   THEN' rtac conjI THEN' rtac allI THEN'
   resolve_tac reflps THEN'
   rtac conjI THEN' rtac allI THEN' rtac allI THEN'
   resolve_tac symps THEN'
-  rtac @{thm transp_aux} THEN' resolve_tac transps
+  rtac @{thm transpI} THEN' resolve_tac transps
+  end
 *}
 
 ML {*
diff -r 7b8f570b2450 -r 6b1eea8dcdc0 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Mon Mar 22 17:21:27 2010 +0100
+++ b/Nominal/Parser.thy	Mon Mar 22 18:29:29 2010 +0100
@@ -337,7 +337,7 @@
   val _ = tracing "Proving equivalence";
   val (rfv_ts_nobn, rfv_ts_bn) = chop (length perms) ordered_fv_ts;
   val fv_alpha_all = combine_fv_alpha_bns (rfv_ts_nobn, rfv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
-  val reflps = build_alpha_refl fv_alpha_all induct alpha_eq_iff lthy6a;
+  val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6a;
   val alpha_equivp =
     if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts_nobn
     else build_equivps alpha_ts reflps alpha_induct