# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265195483 -3600
# Node ID aaac8274f08c14e3afec651691b7832bcdfa7c3b
# Parent  3a60a028cfc5a519ea7ee4c6c8fb5f53af1eda8f
The alpha-equivalence relation for let-rec. Not sure if correct...

diff -r 3a60a028cfc5 -r aaac8274f08c Quot/Nominal/LFex.thy
--- a/Quot/Nominal/LFex.thy	Wed Feb 03 11:47:37 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Wed Feb 03 12:11:23 2010 +0100
@@ -640,9 +640,9 @@
 done
 
 lemma supp_fv:
- "fv_kind t1 = supp t1"
- "fv_ty t2 = supp t2"
- "fv_trm t3 = supp t3"
+ "supp t1 = fv_kind t1"
+ "supp t2 = fv_ty t2"
+ "supp t3 = fv_trm t3"
 apply(induct t1 and t2 and t3 rule: KIND_TY_TRM_inducts)
 apply (simp_all add: supp_kind_ty_trm_easy)
 apply (simp_all add: fv_kind_ty_trm)
@@ -650,39 +650,33 @@
 apply(simp add: supp_Abs Set.Un_commute)
 apply(simp (no_asm) add: supp_def)
 apply(simp add: KIND_TY_TRM_INJECT)
-apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] alpha_gen)
-apply(simp add: Abs_eq_iff alpha_gen)
+apply(simp add: Abs_eq_iff)
+apply(simp add: alpha_gen)
+apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] eqvts atom_eqvt)
+apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
+apply(subgoal_tac "supp (TPI ty1 name ty2) = supp ty1 \<union> supp (Abs {atom name} ty2)")
+apply(simp add: supp_Abs Set.Un_commute)
+apply(simp (no_asm) add: supp_def)
+apply(simp add: KIND_TY_TRM_INJECT)
+apply(simp add: Abs_eq_iff)
+apply(simp add: alpha_gen)
+apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] eqvts atom_eqvt)
 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
-apply (rule refl)
-sorry (* Stuck *)
+apply(subgoal_tac "supp (LAM ty name trm) = supp ty \<union> supp (Abs {atom name} trm)")
+apply(simp add: supp_Abs Set.Un_commute)
+apply(simp (no_asm) add: supp_def)
+apply(simp add: KIND_TY_TRM_INJECT)
+apply(simp add: Abs_eq_iff)
+apply(simp add: alpha_gen)
+apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] eqvts atom_eqvt)
+apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
+done
 
+(* Not needed anymore *)
 lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abs {atom x} K)) \<union> supp A"
-(*apply (subst supp_Pair[symmetric])*)
-unfolding supp_def
-apply (simp add: permute_set_eq)
-apply(subst Abs_eq_iff)
-apply(subst KIND_TY_TRM_INJECT)
-apply(simp only: alpha_gen supp_fv)
-apply simp
-apply (simp_all add: Collect_imp_eq Collect_neg_eq)
-apply(subst Set.Un_commute)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
-apply (rule refl)
-prefer 2
-apply (rule refl)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
-apply (rule refl)
-apply (simp_all)
-apply (simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric])
-sorry (* should be true... *)
-
-lemma supp_kpi: "supp (KPI A x K) = supp A \<union> (supp K - {atom x})"
-apply(subst supp_kpi_pre)
-apply(subst supp_Abs)
-apply (simp only: Set.Un_commute)
+apply (simp add: permute_set_eq supp_def Abs_eq_iff KIND_TY_TRM_INJECT)
+apply (simp add: alpha_gen supp_fv)
+apply (simp add: Collect_imp_eq Collect_neg_eq add: atom_eqvt Set.Un_commute)
 done
 
 lemma supp_kind_ty_trm:
@@ -696,9 +690,8 @@
  "supp (APP M N) = supp M \<union> supp N"
  "supp (LAM A x M) = supp A \<union> (supp M - {atom x})"
 apply (simp_all only: supp_kind_ty_trm_easy)
-apply (simp add: supp_kpi)
-sorry (* Other ones will follow similarily *)
-
+apply (simp_all only: supp_fv fv_kind_ty_trm)
+done
 
 end
 
diff -r 3a60a028cfc5 -r aaac8274f08c Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Wed Feb 03 11:47:37 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 03 12:11:23 2010 +0100
@@ -649,6 +649,12 @@
   by (simp_all add: alpha4_equivp alpha4list_equivp)
 
 
+
+
+
+
+
+
 datatype rtrm5 =
   rVr5 "name"
 | rAp5 "rtrm5" "rtrm5"
@@ -708,8 +714,21 @@
 apply(simp_all add: pt_rtrm5_zero pt_rtrm5_plus)
 done
 
-
 end
 
+inductive
+  alpha5 :: "rtrm5 \<Rightarrow> rtrm5 \<Rightarrow> bool" ("_ \<approx>5 _" [100, 100] 100)
+and
+  alphalts :: "rlts \<Rightarrow> rlts \<Rightarrow> bool" ("_ \<approx>l _" [100, 100] 100)
+where
+  a1: "a = b \<Longrightarrow> (rVr5 a) \<approx>5 (rVr5 b)"
+| a2: "\<lbrakk>t1 \<approx>5 t2; s1 \<approx>5 s2\<rbrakk> \<Longrightarrow> rAp5 t1 s1 \<approx>5 rAp5 t2 s2"
+| a3: "\<exists>pi. ((bv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (bv5 l2, t2) \<and>
+             (bv5 l1, l1) \<approx>gen alphalts rfv_lts pi (bv5 l2, l2) \<and>
+              (pi \<bullet> (bv5 l1) = bv5 l2))
+        \<Longrightarrow> rLt5 l1 t1 \<approx>5 rLt5 l2 t2"
+| a4: "rLnil \<approx>l rLnil"
+| a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2"
 
+thm a3[simplified alpha_gen]
 end