# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266846653 -3600
# Node ID 7b1a3df239cd2772bc851c4cf14a8148c6d5397f
# Parent  cc86faf0d2a0065f423452efa760d6ffc15236b8
Some progress about transp

diff -r cc86faf0d2a0 -r 7b1a3df239cd Quot/Nominal/Fv.thy
--- a/Quot/Nominal/Fv.thy	Mon Feb 22 13:41:13 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Mon Feb 22 14:50:53 2010 +0100
@@ -260,14 +260,19 @@
       val ty = domain_type (fastype_of alpha);
       val var = Free("x", ty);
       val var2 = Free("y", ty);
+      val var3 = Free("z", ty);
+      val symp = HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var);
+      val transp = HOLogic.mk_imp (alpha $ var $ var2,
+        HOLogic.mk_all ("z", ty,
+          HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3)))
     in
-      ((alpha $ var $ var), (HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var)))
+      ((alpha $ var $ var), (symp, transp))
     end;
-  val (refl_eqs, sym_eqs) = split_list (map build_alpha alphas)
+  val (refl_eqs, eqs) = split_list (map build_alpha alphas)
+  val (sym_eqs, trans_eqs) = split_list eqs
+  fun conj l = @{term Trueprop} $ foldr1 HOLogic.mk_conj l
 in
-  Logic.mk_conjunction
-  (@{term Trueprop} $ foldr1 HOLogic.mk_conj refl_eqs,
-   @{term Trueprop} $ foldr1 HOLogic.mk_conj sym_eqs)
+  (conj refl_eqs, (conj sym_eqs, conj trans_eqs))
 end
 *}
 
diff -r cc86faf0d2a0 -r 7b1a3df239cd Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Mon Feb 22 13:41:13 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Mon Feb 22 14:50:53 2010 +0100
@@ -117,9 +117,10 @@
   done
 
 lemma alpha_gen_atom_sym:
-  assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "\<exists>pi. (aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s) \<Longrightarrow>
-        \<exists>pi. (ab, s) \<approx>gen R f pi (aa, t)"
+  assumes b: "\<exists>pi. (aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
+  and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
+  shows "\<exists>pi. (ab, s) \<approx>gen R f pi (aa, t)"
+  using b apply -
   apply(erule exE)
   apply(rule_tac x="- pi" in exI)
   apply(simp add: alpha_gen.simps)
@@ -132,38 +133,62 @@
   apply assumption
   done
 
+prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *}
+by (tactic {*
 
-prove alpha1_reflp_aux: {* (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *}
-apply (tactic {*
  (indtac @{thm rtrm1_bp.induct} ["x", "x"] THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj}) THEN_ALL_NEW
   TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW
-  rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})
+  (rtac @{thm exI[of _ "0 :: perm"]} THEN'
+  asm_full_simp_tac (HOL_ss addsimps @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv}))
  ) 1 *})
-apply (tactic {*
+
+prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *}
+by (tactic {*
  (rtac @{thm alpha_rtrm1_alpha_bp.induct} THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj}) THEN_ALL_NEW
   TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW
-  (rtac @{thm alpha_gen_atom_sym} THEN' RANGE [
-    (asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt})), atac
-  ])
- ) 1 *})
+ (etac @{thm alpha_gen_atom_sym} THEN'
+  asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt})
+ )) 1 *})
+
+prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *}
+apply (rule alpha_rtrm1_alpha_bp.induct)
+apply simp_all
+apply (rule_tac [!] allI)
+apply (rule_tac [!] impI)
+apply (rotate_tac 4)
+apply (erule alpha_rtrm1.cases)
+apply (simp_all add: alpha1_inj)
+apply (rotate_tac 2)
+apply (erule alpha_rtrm1.cases)
+apply (simp_all add: alpha1_inj)
+thm alpha_gen_atom_trans
+(*apply (tactic {*
+ (rtac @{thm alpha_rtrm1_alpha_bp.induct} THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj})) 1 *})*)
+sorry
+
+lemma helper: "(\<forall>x y z. R x y \<and> R y z \<longrightarrow> R x z) = (\<forall>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z))"
+by meson
+
+lemma alpha1_equivp:
+  "equivp alpha_rtrm1"
+  "equivp alpha_bp"
+unfolding equivp_reflp_symp_transp reflp_def
+apply (simp_all add: alpha1_reflp_aux)
+unfolding symp_def
+apply (simp_all add: alpha1_symp_aux)
+unfolding transp_def
+apply (simp_all only: helper)
+apply (rule allI)+
+apply (rule conjunct1[OF alpha1_transp_aux])
+apply (rule allI)+
+apply (rule conjunct2[OF alpha1_transp_aux])
 done
 
-lemma alpha1_reflp: 
-  "reflp alpha_rtrm1"
-  "reflp alpha_bp"
-unfolding reflp_def
-apply (simp_all add: alpha1_reflp_aux)
-done
-
-lemma alpha1_equivp: "equivp alpha_rtrm1" 
-  sorry
-
-
 quotient_type trm1 = rtrm1 / alpha_rtrm1
-  by (rule alpha1_equivp)
+  by (rule alpha1_equivp(1))
 
 local_setup {*
 (fn ctxt => ctxt
@@ -275,7 +300,7 @@
 apply(simp_all)
 done
 
-lemma helper: "{b. \<forall>pi. pi \<bullet> (a \<rightleftharpoons> b) \<bullet> bp \<noteq> bp} = {}"
+lemma helper2: "{b. \<forall>pi. pi \<bullet> (a \<rightleftharpoons> b) \<bullet> bp \<noteq> bp} = {}"
 apply auto
 apply (rule_tac x="(x \<rightleftharpoons> a)" in exI)
 apply auto
@@ -304,7 +329,7 @@
 apply(simp add: Abs_eq_iff)
 apply(simp add: alpha_gen)
 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv)
-apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper)
+apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper2)
 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)
 apply(simp (no_asm) add: supp_def eqvts)
 apply(fold supp_def)