# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265894606 -3600
# Node ID 95e58790772855dfa2531608b55f4934ba24429e
# Parent  fb5f5735a4268183caa109a35be9cfddf8ffe69e
Even when bv = fv it still doesn't lift.

diff -r fb5f5735a426 -r 95e587907728 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Thu Feb 11 14:02:34 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Thu Feb 11 14:23:26 2010 +0100
@@ -1114,6 +1114,7 @@
 
 
 (* example with a respectful bn function defined over the type itself *)
+
 datatype rtrm7 =
   rVr7 "name"
 | rLm7 "name" "rtrm7"
@@ -1129,13 +1130,65 @@
 primrec
   rfv_trm7
 where
-  "rfv_trm7 (rVr7 n) = {}"
-| "rfv_trm7 (rLm7 n t) = {atom n} \<union> (rfv_trm7 t)"
-| "rfv_trm7 (rLt7 l r) = (rfv_trm7 r) \<union> (rfv_trm7 l)"
+  "rfv_trm7 (rVr7 n) = {atom n}"
+| "rfv_trm7 (rLm7 n t) = (rfv_trm7 t) - {atom n}"
+| "rfv_trm7 (rLt7 l r) = (rfv_trm7 l) \<union> (rfv_trm7 r - rbv7 l)"
+
+instantiation
+  rtrm7 :: pt
+begin
+
+primrec
+  permute_rtrm7
+where
+  "permute_rtrm7 pi (rVr7 a) = rVr7 (pi \<bullet> a)"
+| "permute_rtrm7 pi (rLm7 a t) = rLm7 (pi \<bullet> a) (permute_rtrm7 pi t)"
+| "permute_rtrm7 pi (rLt7 t1 t2) = rLt7 (permute_rtrm7 pi t1) (permute_rtrm7 pi t2)"
+
+lemma pt_rtrm7_zero:
+  fixes t::rtrm7
+  shows "0 \<bullet> t = t"
+apply(induct t)
+apply(simp_all)
+done
+
+lemma pt_rtrm7_plus:
+  fixes t::rtrm7
+  shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
+apply(induct t)
+apply(simp_all)
+done
 
+instance
+apply default
+apply(simp_all add: pt_rtrm7_zero pt_rtrm7_plus)
+done
 
+end
+
+inductive
+  alpha7 :: "rtrm7 \<Rightarrow> rtrm7 \<Rightarrow> bool" ("_ \<approx>7 _" [100, 100] 100)
+where
+  a1: "a = b \<Longrightarrow> (rVr7 a) \<approx>7 (rVr7 b)"
+| a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha7 rfv_trm7 pi ({atom b}, s))) \<Longrightarrow> rLm7 a t \<approx>7 rLm7 b s"
+| a3: "(\<exists>pi. (((rbv7 t1), s1) \<approx>gen alpha7 rfv_trm7 pi ((rbv7 t2), s2))) \<Longrightarrow> rLt7 t1 s1 \<approx>7 rLt7 t2 s2"
 
+lemma bvfv7: "rbv7 x = rfv_trm7 x"
+  apply induct
+  apply simp_all
+done
 
+lemma "(x::name) \<noteq> y \<Longrightarrow> \<not> (alpha7 ===> op =) rbv7 rbv7"
+  apply simp
+  apply (rule_tac x="rLt7 (rVr7 x) (rVr7 x)" in exI)
+  apply (rule_tac x="rLt7 (rVr7 y) (rVr7 y)" in exI)
+  apply simp
+  apply (rule a3)
+  apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+  apply (simp_all add: alpha_gen fresh_star_def)
+  apply (rule a1)
+  apply (rule refl)
+done
 
 
 text {* type schemes *}