# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265794607 -3600
# Node ID ee276c9f12f0c72cc73f374911b4d888c9d6b7c9
# Parent  1e5dee9e6ae2db2da5317a767f0d05a5d6f3f6f3
A concrete example, with a proof that rbv is not regular and
with proofs of induction and pseudo-injectivity that require this

diff -r 1e5dee9e6ae2 -r ee276c9f12f0 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Tue Feb 09 19:08:08 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 10 10:36:47 2010 +0100
@@ -929,22 +929,22 @@
 (* example with a bn function defined over the type itself *)
 datatype rtrm6 =
   rVr6 "name"
-| rAp6 "rtrm6" "rtrm6"
-| rFo6 "rtrm6" "rtrm6" --"bind (bv6 left) in (right)"
+| rLm6 "name" "rtrm6"
+| rLt6 "rtrm6" "rtrm6" --"bind (bv6 left) in (right)"
 
 primrec
   rbv6
 where
-  "rbv6 (rVr6 x) = {atom x}"
-| "rbv6 (rAp6 l r) = rbv6 l \<union> rbv6 r"
-| "rbv6 (rFo6 l r) = rbv6 r - rbv6 l"
+  "rbv6 (rVr6 n) = {}"
+| "rbv6 (rLm6 n t) = {atom n}"
+| "rbv6 (rLt6 l r) = rbv6 l \<union> rbv6 r"
 
 primrec
   rfv_trm6
 where
   "rfv_trm6 (rVr6 n) = {atom n}"
-| "rfv_trm6 (rAp6 t s) = (rfv_trm6 t) \<union> (rfv_trm6 s)"
-| "rfv_trm6 (rFo6 l r) = (rfv_trm6 r - rbv6 l) \<union> (rfv_trm6 l)"
+| "rfv_trm6 (rLm6 n t) = (rfv_trm6 t) - {atom n}"
+| "rfv_trm6 (rLt6 l r) = (rfv_trm6 r - rbv6 l) \<union> rfv_trm6 r"
 
 instantiation
   rtrm6 :: pt
@@ -954,8 +954,8 @@
   permute_rtrm6
 where
   "permute_rtrm6 pi (rVr6 a) = rVr6 (pi \<bullet> a)"
-| "permute_rtrm6 pi (rAp6 t1 t2) = rAp6 (permute_rtrm6 pi t1) (permute_rtrm6 pi t2)"
-| "permute_rtrm6 pi (rFo6 l r) = rFo6 (permute_rtrm6 pi l) (permute_rtrm6 pi r)"
+| "permute_rtrm6 pi (rLm6 n t) = rLm6 (pi \<bullet> n) (permute_rtrm6 pi t)"
+| "permute_rtrm6 pi (rLt6 l r) = rLt6 (permute_rtrm6 pi l) (permute_rtrm6 pi r)"
 
 lemma pt_rtrm6_zero:
   fixes t::rtrm6
@@ -982,9 +982,8 @@
   alpha6 :: "rtrm6 \<Rightarrow> rtrm6 \<Rightarrow> bool" ("_ \<approx>6 _" [100, 100] 100)
 where
   a1: "a = b \<Longrightarrow> (rVr6 a) \<approx>6 (rVr6 b)"
-| a2: "\<lbrakk>t1 \<approx>6 t2; s1 \<approx>6 s2\<rbrakk> \<Longrightarrow> rAp6 t1 s1 \<approx>6 rAp6 t2 s2"
-| a3: "\<lbrakk>\<exists>pi. ((rbv6 l1, r1) \<approx>gen alpha6 rfv_trm6 pi (rbv6 l2, r2))\<rbrakk>
-        \<Longrightarrow> rFo6 l1 r1 \<approx>6 rFo6 l2 r2"
+| a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha6 rfv_trm6 pi ({atom b}, s))) \<Longrightarrow> rLm6 a t \<approx>6 rLm6 b s"
+| a3: "(\<exists>pi. (((rbv6 t1), s1) \<approx>gen alpha6 rfv_trm6 pi ((rbv6 t2), s2))) \<Longrightarrow> rLt6 t1 s1 \<approx>6 rLt6 t2 s2"
 
 lemma alpha6_equivps:
   shows "equivp alpha6"
@@ -1000,14 +999,14 @@
   "rVr6"
 
 quotient_definition
-  "Ap6 :: trm6 \<Rightarrow> trm6 \<Rightarrow> trm6"
+  "Lm6 :: name \<Rightarrow> trm6 \<Rightarrow> trm6"
 as
-  "rAp6"
+  "rLm6"
 
 quotient_definition
-  "Fo6 :: trm6 \<Rightarrow> trm6 \<Rightarrow> trm6"
+  "Lt6 :: trm6 \<Rightarrow> trm6 \<Rightarrow> trm6"
 as
-  "rFo6"
+  "rLt6"
 
 quotient_definition
    "fv_trm6 :: trm6 \<Rightarrow> atom set"
@@ -1020,33 +1019,53 @@
   "rbv6"
 
 lemma [quot_respect]:
-  "(op = ===> alpha1 ===> alpha1) permute permute"
-apply auto (* eqvt *)
+  "(op = ===> alpha6 ===> alpha6) permute permute"
+apply auto (* will work with eqvt *)
 sorry
 
+(* Definitely not true , see lemma below *)
+
 lemma [quot_respect]:"(alpha6 ===> op =) rbv6 rbv6"
 apply simp apply clarify
 apply (erule alpha6.induct)
+oops
+
+lemma "(a :: name) \<noteq> b \<Longrightarrow> \<not> (alpha6 ===> op =) rbv6 rbv6"
 apply simp
+apply (rule_tac x="rLm6 (a::name) (rVr6 (a :: name))" in  exI)
+apply (rule_tac x="rLm6 (b::name) (rVr6 (b :: name))" in  exI)
 apply simp
-apply (erule exE)
-apply (simp add: alpha_gen)
-oops
+apply (rule a2)
+apply (rule_tac x="(a \<leftrightarrow> b)" in  exI)
+apply (simp add: alpha_gen fresh_star_def)
+apply (rule a1)
+apply (rule refl)
+done
 
 lemma [quot_respect]:"(alpha6 ===> op =) rfv_trm6 rfv_trm6"
 apply simp apply clarify
 apply (induct_tac x y rule: alpha6.induct)
 apply simp_all
 apply (erule exE)
-apply (simp add: alpha_gen)
+apply (simp_all add: alpha_gen)
+apply (erule conjE)+
+apply (erule exE)
 apply (erule conjE)+
+apply (simp)
 oops
 
+
+lemma [quot_respect]: "(op = ===> alpha6) rVr6 rVr6"
+by (simp_all add: a1)
+
 lemma [quot_respect]:
- "(op = ===> alpha6) rVr6 rVr6"
- "(alpha6 ===> alpha6 ===> alpha6) rAp6 rAp6"
- "(alpha6 ===> alpha6 ===> alpha6) rFo6 rFo6"
-apply (simp_all add: a1 a2)
+ "(op = ===> alpha6 ===> alpha6) rLm6 rLm6"
+ "(alpha6 ===> alpha6 ===> alpha6) rLt6 rLt6"
+apply simp_all apply (clarify)
+apply (rule a2)
+apply (rule_tac x="0::perm" in exI)
+apply (simp add: alpha_gen)
+(* needs rfv6_rsp *) defer
 apply clarify
 apply (rule a3)
 apply (rule_tac x="0::perm" in exI)
@@ -1066,24 +1085,31 @@
 sorry
 end
 
-lemma 
+lemma lifted_induct:
 "\<lbrakk>x1 = x2; \<And>a b. a = b \<Longrightarrow> P (Vr6 a) (Vr6 b);
-  \<And>t1 t2 s1 s2. \<lbrakk>t1 = t2; P t1 t2; s1 = s2; P s1 s2\<rbrakk> \<Longrightarrow> P (Ap6 t1 s1) (Ap6 t2 s2);
-  \<And>l1 r1 l2 r2.
-     \<exists>pi. (bv6 l1, r1) \<approx>gen (\<lambda>x1 x2. x1 = x2 \<and> P x1 x2) fv_trm6 pi (bv6 l2, r2) \<Longrightarrow>
-     P (Fo6 l1 r1) (Fo6 l2 r2)\<rbrakk>
+ \<And>a t b s.
+   \<exists>pi. fv_trm6 t - {atom a} = fv_trm6 s - {atom b} \<and>
+        (fv_trm6 t - {atom a}) \<sharp>* pi \<and> pi \<bullet> t = s \<and> P (pi \<bullet> t) s \<Longrightarrow>
+   P (Lm6 a t) (Lm6 b s);
+ \<And>t1 s1 t2 s2.
+   \<exists>pi. fv_trm6 s1 - bv6 t1 = fv_trm6 s2 - bv6 t2 \<and>
+        (fv_trm6 s1 - bv6 t1) \<sharp>* pi \<and> pi \<bullet> s1 = s2 \<and> P (pi \<bullet> s1) s2 \<Longrightarrow>
+   P (Lt6 t1 s1) (Lt6 t2 s2)\<rbrakk>
  \<Longrightarrow> P x1 x2"
 unfolding alpha_gen
 apply (lifting alpha6.induct[unfolded alpha_gen])
-apply(injection)
-sorry
+apply injection
+(* notice unsolvable goals: (alpha6 ===> op =) rbv6 rbv6 *)
+oops
 
-lemma "\<lbrakk>\<exists>pi. ((bv6 l1, r1) \<approx>gen (op =) fv_trm6 pi (bv6 l2, r2))\<rbrakk>
-        \<Longrightarrow> Fo6 l1 r1 = Fo6 l2 r2"
-apply (unfold alpha_gen)
-apply (lifting a3[unfolded alpha_gen])
+lemma lifted_inject_a3:
+ "\<exists>pi. fv_trm6 s1 - bv6 t1 = fv_trm6 s2 - bv6 t2 \<and>
+    (fv_trm6 s1 - bv6 t1) \<sharp>* pi \<and> pi \<bullet> s1 = s2 \<Longrightarrow> Lt6 t1 s1 = Lt6 t2 s2"
+apply(lifting a3[unfolded alpha_gen])
 apply injection
-sorry
+(* notice unsolvable goals: (alpha6 ===> op =) rbv6 rbv6 *)
+oops
+