# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265203193 -3600
# Node ID e8bb5f85e510328b4de724c7387e4e6c65ecea57
# Parent  0f101870e2ff4db55290fd2c6afd3fefab728377
Lets are ok.

diff -r 0f101870e2ff -r e8bb5f85e510 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Wed Feb 03 13:00:37 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 03 14:19:53 2010 +0100
@@ -38,6 +38,7 @@
 | "rfv_bp (BUnit) = {}"
 | "rfv_bp (BVr x) = {atom x}"
 | "rfv_bp (BPr b1 b2) = (rfv_bp b1) \<union> (rfv_bp b2)"
+print_theorems
 
 (* needs to be stated by the package *)
 instantiation 
@@ -655,17 +656,17 @@
 | rLcons "name" "rtrm5" "rlts"
 
 primrec
-  bv5
+  rbv5
 where
-  "bv5 rLnil = {}"
-| "bv5 (rLcons n t ltl) = {atom n} \<union> (bv5 ltl)"
+  "rbv5 rLnil = {}"
+| "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
 
 primrec
   rfv_trm5 and rfv_lts
 where
   "rfv_trm5 (rVr5 n) = {atom n}"
 | "rfv_trm5 (rAp5 t s) = (rfv_trm5 t) \<union> (rfv_trm5 s)"
-| "rfv_trm5 (rLt5 lts t) = (rfv_trm5 t - bv5 lts) \<union> (rfv_lts lts - bv5 lts)"
+| "rfv_trm5 (rLt5 lts t) = (rfv_trm5 t - rbv5 lts) \<union> (rfv_lts lts - rbv5 lts)"
 | "rfv_lts (rLnil) = {}"
 | "rfv_lts (rLcons n t ltl) = (rfv_trm5 t) \<union> (rfv_lts ltl)"
 
@@ -678,7 +679,7 @@
 where
   "permute_rtrm5 pi (rVr5 a) = rVr5 (pi \<bullet> a)"
 | "permute_rtrm5 pi (rAp5 t1 t2) = rAp5 (permute_rtrm5 pi t1) (permute_rtrm5 pi t2)"
-| "permute_rtrm5 pi (rLt5 as t) = rLt5 (permute_rlts pi as) (permute_rtrm5 pi t)"
+| "permute_rtrm5 pi (rLt5 ls t) = rLt5 (permute_rlts pi ls) (permute_rtrm5 pi t)"
 | "permute_rlts pi (rLnil) = rLnil"
 | "permute_rlts pi (rLcons n t ls) = rLcons (pi \<bullet> n) (permute_rtrm5 pi t) (permute_rlts pi ls)"
 
@@ -714,9 +715,9 @@
 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))
+| a3: "\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (rbv5 l2, t2) \<and>
+             (rbv5 l1, l1) \<approx>gen alphalts rfv_lts pi (rbv5 l2, l2) \<and>
+              (pi \<bullet> (rbv5 l1) = rbv5 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> n1 = n2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2"
@@ -726,9 +727,9 @@
 lemma alpha5_inj:
   "((rVr5 a) \<approx>5 (rVr5 b)) = (a = b)"
   "(rAp5 t1 s1 \<approx>5 rAp5 t2 s2) = (t1 \<approx>5 t2 \<and> s1 \<approx>5 s2)"
-  "(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = (\<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)))"
+  "(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = (\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (rbv5 l2, t2) \<and>
+         (rbv5 l1, l1) \<approx>gen alphalts rfv_lts pi (rbv5 l2, l2) \<and>
+         (pi \<bullet> (rbv5 l1) = rbv5 l2)))"
   "rLnil \<approx>l rLnil"
   "(rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2) = (ls1 \<approx>l ls2 \<and> t1 \<approx>5 t2 \<and> n1 = n2)"
 apply -
@@ -789,9 +790,110 @@
   "rfv_trm5"
 
 quotient_definition
-   "fv_ltr :: lts \<Rightarrow> atom set"
+   "fv_lts :: lts \<Rightarrow> atom set"
 as
   "rfv_lts"
 
+quotient_definition
+   "bv5 :: lts \<Rightarrow> atom set"
+as
+  "rbv5"
+
+lemma alpha5_rfv:
+  "(t \<approx>5 s \<Longrightarrow> rfv_trm5 t = rfv_trm5 s)"
+  "(l \<approx>l m \<Longrightarrow> rfv_lts l = rfv_lts m)"
+  apply(induct rule: alpha5_alphalts.inducts)
+  apply(simp_all add: alpha_gen)
+  apply(erule conjE)+
+  apply(erule exE)
+  apply(erule conjE)+
+  apply simp
+  done
+
+lemma [quot_respect]:
+"(op = ===> alpha5 ===> alpha5) permute permute"
+"(op = ===> alphalts ===> alphalts) permute permute"
+"(op = ===> alpha5) rVr5 rVr5"
+"(alpha5 ===> alpha5 ===> alpha5) rAp5 rAp5"
+"(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
+"(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
+"(op = ===> alpha5 ===> alphalts ===> alphalts) rLcons rLcons"
+"(alpha5 ===> op =) rfv_trm5 rfv_trm5"
+"(alphalts ===> op =) rfv_lts rfv_lts"
+"(alphalts ===> op =) rbv5 rbv5"
+sorry
+
+instantiation trm5 and lts :: pt
+begin
+
+quotient_definition
+  "permute_trm5 :: perm \<Rightarrow> trm5 \<Rightarrow> trm5"
+as
+  "permute :: perm \<Rightarrow> rtrm5 \<Rightarrow> rtrm5"
+
+quotient_definition
+  "permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts"
+as
+  "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts"
+
+lemma permute_trm5_lts:
+"pi \<bullet> (Vr5 a) = Vr5 (pi \<bullet> a)"
+"pi \<bullet> (Ap5 t1 t2) = Ap5 (pi \<bullet> t1) (pi \<bullet> t2)"
+"pi \<bullet> (Lt5 ls t) = Lt5 (pi \<bullet> ls) (pi \<bullet> t)"
+"pi \<bullet> Lnil = Lnil"
+"pi \<bullet> (Lcons n t ls) = Lcons (pi \<bullet> n) (pi \<bullet> t) (pi \<bullet> ls)"
+by (lifting permute_rtrm5_permute_rlts.simps)
+
+lemma trm5_lts_zero:
+  "0 \<bullet> (x\<Colon>trm5) = x"
+  "0 \<bullet> (y\<Colon>lts) = y"
+sorry
+
+lemma trm5_lts_plus:
+  "(p + q) \<bullet> (x\<Colon>trm5) = p \<bullet> q \<bullet> x"
+  "(p + q) \<bullet> (y\<Colon>lts) = p \<bullet> q \<bullet> y"
+sorry
+
+instance
+apply default
+apply (simp_all add: trm5_lts_zero trm5_lts_plus)
+done
 
 end
+
+lemma alpha5_INJ:
+  "((Vr5 a) = (Vr5 b)) = (a = b)"
+  "(Ap5 t1 s1 = Ap5 t2 s2) = (t1 = t2 \<and> s1 = s2)"
+  "(Lt5 l1 t1 = Lt5 l2 t2) =
+     (\<exists>pi. ((bv5 l1, t1) \<approx>gen (op =) fv_trm5 pi (bv5 l2, t2) \<and>
+            (bv5 l1, l1) \<approx>gen (op =) fv_lts pi (bv5 l2, l2) \<and>
+            (pi \<bullet> (bv5 l1) = bv5 l2)))"
+  "Lnil = Lnil"
+  "(Lcons n1 t1 ls1 = Lcons n2 t2 ls2) = (ls1 = ls2 \<and> t1 = t2 \<and> n1 = n2)"
+unfolding alpha_gen
+apply(lifting alpha5_inj[unfolded alpha_gen])
+done
+
+lemma bv5[simp]:
+  "bv5 Lnil = {}"
+  "bv5 (Lcons n t ltl) = {atom n} \<union> bv5 ltl"
+by (lifting rbv5.simps)
+
+lemma fv_trm5_lts[simp]:
+  "fv_trm5 (Vr5 n) = {atom n}"
+  "fv_trm5 (Ap5 t s) = fv_trm5 t \<union> fv_trm5 s"
+  "fv_trm5 (Lt5 lts t) = fv_trm5 t - bv5 lts \<union> (fv_lts lts - bv5 lts)"
+  "fv_lts Lnil = {}"
+  "fv_lts (Lcons n t ltl) = fv_trm5 t \<union> fv_lts ltl"
+by (lifting rfv_trm5_rfv_lts.simps)
+
+lemma lets_ok:
+  "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
+apply (subst alpha5_INJ)
+apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+apply (simp only: alpha_gen)
+apply (simp add: permute_trm5_lts)
+sorry
+
+
+end