nominal2: comparison Quot/Nominal/Terms.thy

equal deleted inserted replaced

-:1e5dee9e6ae2
+:ee276c9f12f0
 (* example with a bn function defined over the type itself *)
 datatype rtrm6 =
 rVr6 "name"
-| rAp6 "rtrm6" "rtrm6"
+| rLm6 "name" "rtrm6"
-| rFo6 "rtrm6" "rtrm6" --"bind (bv6 left) in (right)"
+| rLt6 "rtrm6" "rtrm6" --"bind (bv6 left) in (right)"
 primrec
 rbv6
 where
-"rbv6 (rVr6 x) = {atom x}"
+"rbv6 (rVr6 n) = {}"
-| "rbv6 (rAp6 l r) = rbv6 l \<union> rbv6 r"
+| "rbv6 (rLm6 n t) = {atom n}"
-| "rbv6 (rFo6 l r) = rbv6 r - rbv6 l"
+| "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 (rLm6 n t) = (rfv_trm6 t) - {atom n}"
-| "rfv_trm6 (rFo6 l r) = (rfv_trm6 r - rbv6 l) \<union> (rfv_trm6 l)"
+| "rfv_trm6 (rLt6 l r) = (rfv_trm6 r - rbv6 l) \<union> rfv_trm6 r"
 instantiation
 rtrm6 :: pt
 begin
 primrec
 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 (rLm6 n t) = rLm6 (pi \<bullet> n) (permute_rtrm6 pi t)"
-| "permute_rtrm6 pi (rFo6 l r) = rFo6 (permute_rtrm6 pi l) (permute_rtrm6 pi r)"
+| "permute_rtrm6 pi (rLt6 l r) = rLt6 (permute_rtrm6 pi l) (permute_rtrm6 pi r)"
 lemma pt_rtrm6_zero:
 fixes t::rtrm6
 shows "0 \<bullet> t = t"
 apply(induct t)
 inductive
 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"
+| 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: "\<lbrakk>\<exists>pi. ((rbv6 l1, r1) \<approx>gen alpha6 rfv_trm6 pi (rbv6 l2, r2))\<rbrakk>
+| a3: "(\<exists>pi. (((rbv6 t1), s1) \<approx>gen alpha6 rfv_trm6 pi ((rbv6 t2), s2))) \<Longrightarrow> rLt6 t1 s1 \<approx>6 rLt6 t2 s2"
-\<Longrightarrow> rFo6 l1 r1 \<approx>6 rFo6 l2 r2"
 lemma alpha6_equivps:
 shows "equivp alpha6"
 sorry
 "Vr6 :: name \<Rightarrow> trm6"
 as
 "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"
 as
 "rfv_trm6"
 "bv6 :: trm6 \<Rightarrow> atom set"
 as
 "rbv6"
 lemma [quot_respect]:
-"(op = ===> alpha1 ===> alpha1) permute permute"
+"(op = ===> alpha6 ===> alpha6) permute permute"
-apply auto (* eqvt *)
+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 (rule a2)
-apply (simp add: alpha_gen)
+apply (rule_tac x="(a \<leftrightarrow> b)" in  exI)
-oops
+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_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 ===> 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)
-apply (erule conjE)+
+(* needs rfv6_rsp *) defer
-oops
-lemma [quot_respect]:
-"(op = ===> alpha6) rVr6 rVr6"
-"(alpha6 ===> alpha6 ===> alpha6) rAp6 rAp6"
-"(alpha6 ===> alpha6 ===> alpha6) rFo6 rFo6"
-apply (simp_all add: a1 a2)
 apply clarify
 apply (rule a3)
 apply (rule_tac x="0::perm" in exI)
 apply (simp add: alpha_gen)
 (* needs rbv6_rsp *)
 instance
 apply default
 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>a t b s.
-\<And>l1 r1 l2 r2.
+\<exists>pi. fv_trm6 t - {atom a} = fv_trm6 s - {atom b} \<and>
-\<exists>pi. (bv6 l1, r1) \<approx>gen (\<lambda>x1 x2. x1 = x2 \<and> P x1 x2) fv_trm6 pi (bv6 l2, r2) \<Longrightarrow>
+(fv_trm6 t - {atom a}) \<sharp>* pi \<and> pi \<bullet> t = s \<and> P (pi \<bullet> t) s \<Longrightarrow>
-P (Fo6 l1 r1) (Fo6 l2 r2)\<rbrakk>
+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
-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])
 apply injection
-sorry
+(* notice unsolvable goals: (alpha6 ===> op =) rbv6 rbv6 *)
+oops
+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
+(* notice unsolvable goals: (alpha6 ===> op =) rbv6 rbv6 *)
+oops

changeset 1111	ee276c9f12f0
parent 1109	86093c201bac
child 1117	8948319b190e