# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266837152 -3600
# Node ID fb33684e4ece17c1fdc31847b910e410db26f0f9
# Parent  9c968284553cda80cf563b8eae0c0df72b0c82b2
alpha reflexivity

diff -r 9c968284553c -r fb33684e4ece Quot/Nominal/Fv.thy
--- a/Quot/Nominal/Fv.thy	Mon Feb 22 10:57:39 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Mon Feb 22 12:12:32 2010 +0100
@@ -91,7 +91,6 @@
 *}
 
 (* TODO: Notice datatypes without bindings and replace alpha with equality *)
-
 ML {*
 (* Currently needs just one full_tname to access Datatype *)
 fun define_fv_alpha full_tname bindsall lthy =
@@ -253,4 +252,21 @@
 end
 *}
 
+ML {*
+fun build_alpha_refl_gl alphas =
+let
+  fun build_alpha alpha =
+    let
+      val ty = domain_type (fastype_of alpha);
+      val var = Free("x", ty);
+    in
+      alpha $ var $ var
+    end
+  val eqs = map build_alpha alphas
+in
+  @{term Trueprop} $ foldr1 HOLogic.mk_conj eqs
 end
+*}
+
+
+end
diff -r 9c968284553c -r fb33684e4ece Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Mon Feb 22 10:57:39 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Mon Feb 22 12:12:32 2010 +0100
@@ -116,9 +116,27 @@
   apply(simp add: permute_eqvt[symmetric])
   done
 
+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})
+ ) 1 *})
+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)