319 datatype trm2 =

   319 datatype rtrm2 =

   320   Vr2 "name"

   320   rVr2 "name"

   321 | Ap2 "trm2" "trm2"

   321 | rAp2 "rtrm2" "rtrm2"

   322 | Lm2 "name" "trm2"

   322 | rLm2 "name" "rtrm2"

   323 | Lt2 "assign" "trm2"

   323 | rLt2 "rassign" "rtrm2"

   324 and assign =

   324 and rassign =

   325   As "name" "trm2"

   325   rAs "name" "rtrm2"

   329   bv2

   329   rbv2

   330 where

   330 where

   331   "bv2 (As x t) = {atom x}"

   331   "rbv2 (rAs x t) = {atom x}"

   335   fv_trm2 and fv_assign

   335   fv_rtrm2 and fv_rassign

   336 where

   336 where

   337   "fv_trm2 (Vr2 x) = {atom x}"

   337   "fv_rtrm2 (rVr2 x) = {atom x}"

   338 | "fv_trm2 (Ap2 t1 t2) = (fv_trm2 t1) \<union> (fv_trm2 t2)"

   338 | "fv_rtrm2 (rAp2 t1 t2) = (fv_rtrm2 t1) \<union> (fv_rtrm2 t2)"

   339 | "fv_trm2 (Lm2 x t) = (fv_trm2 t) - {atom x}"

   339 | "fv_rtrm2 (rLm2 x t) = (fv_rtrm2 t) - {atom x}"

   340 | "fv_trm2 (Lt2 as t) = (fv_trm2 t - bv2 as) \<union> (fv_assign as)"

   340 | "fv_rtrm2 (rLt2 as t) = (fv_rtrm2 t - rbv2 as) \<union> (fv_rassign as)"

   341 | "fv_assign (As x t) = (fv_trm2 t)"

   341 | "fv_rassign (rAs x t) = fv_rtrm2 t"

   344 instantiation 

   344 instantiation

   345   trm2 and assign :: pt

   345   rtrm2 and rassign :: pt

   349   permute_trm2 and permute_assign

   349   permute_rtrm2 and permute_rassign

   350 where

   350 where

   351   "permute_trm2 pi (Vr2 a) = Vr2 (pi \<bullet> a)"

   351   "permute_rtrm2 pi (rVr2 a) = rVr2 (pi \<bullet> a)"

   352 | "permute_trm2 pi (Ap2 t1 t2) = Ap2 (permute_trm2 pi t1) (permute_trm2 pi t2)"

   352 | "permute_rtrm2 pi (rAp2 t1 t2) = rAp2 (permute_rtrm2 pi t1) (permute_rtrm2 pi t2)"

   353 | "permute_trm2 pi (Lm2 a t) = Lm2 (pi \<bullet> a) (permute_trm2 pi t)"

   353 | "permute_rtrm2 pi (rLm2 a t) = rLm2 (pi \<bullet> a) (permute_rtrm2 pi t)"

   354 | "permute_trm2 pi (Lt2 as t) = Lt2 (permute_assign pi as) (permute_trm2 pi t)"

   354 | "permute_rtrm2 pi (rLt2 as t) = rLt2 (permute_rassign pi as) (permute_rtrm2 pi t)"

   355 | "permute_assign pi (As a t) = As (pi \<bullet> a) (permute_trm2 pi t)"

   355 | "permute_rassign pi (rAs a t) = rAs (pi \<bullet> a) (permute_rtrm2 pi t)"

   356 

   356 

   357 lemma pt_trm2_assign_zero:

   357 lemma pt_rtrm2_rassign_zero:

   358   fixes t::trm2

   358   fixes t::rtrm2

   359   and   b::assign

   359   and   b::rassign

   362 apply(induct t and b rule: trm2_assign.inducts)

   362 apply(induct t and b rule: rtrm2_rassign.inducts)

   363 apply(simp_all)

   363 apply(simp_all)

   364 done

   364 done

   365 

   365 

   366 lemma pt_trm2_assign_plus:

   366 lemma pt_rtrm2_rassign_plus:

   367   fixes t::trm2

   367   fixes t::rtrm2

   368   and   b::assign

   368   and   b::rassign

   371 apply(induct t and b rule: trm2_assign.inducts)

   371 apply(induct t and b rule: rtrm2_rassign.inducts)

   377 apply(simp_all add: pt_trm2_assign_zero pt_trm2_assign_plus)

   377 apply(simp_all add: pt_rtrm2_rassign_zero pt_rtrm2_rassign_plus)

   384   alpha2 :: "trm2 \<Rightarrow> trm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)

   384   alpha2 :: "rtrm2 \<Rightarrow> rtrm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)

   385 where

   385 and

   386   a1: "a = b \<Longrightarrow> (Vr2 a) \<approx>2 (Vr2 b)"

   386   alpha2a :: "rassign \<Rightarrow> rassign \<Rightarrow> bool" ("_ \<approx>2a _" [100, 100] 100)

   387 | a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> Ap2 t1 s1 \<approx>2 Ap2 t2 s2"

   387 where

   388 | a3: "\<exists>pi. (fv_trm2 t - {atom a} = fv_trm2 s - {atom b} \<and> 

   388   a1: "a = b \<Longrightarrow> (rVr2 a) \<approx>2 (rVr2 b)"

   389             (fv_trm2 t - {atom a})\<sharp>* pi \<and> 

   389 | a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rAp2 t1 s1 \<approx>2 rAp2 t2 s2"

   390             (pi \<bullet> t) \<approx>2 s \<and> 

   390 | a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha2 fv_rtrm2 pi ({atom b}, s))) \<Longrightarrow> rLm2 a t \<approx>2 rLm2 b s"

   391             (pi \<bullet> a) = b)

   391 | a4: "(\<exists>pi. (((bv2 bt), t) \<approx>gen alpha2 fv_rtrm2 pi ((bv2 bs), s))) \<Longrightarrow> rLt2 bt t \<approx>2 rLt2 bs s"

   392        \<Longrightarrow> Lm2 a t \<approx>2 Lm2 b s"

   392 | a5: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha2 fv_rtrm2 pi ({atom b}, s))) \<Longrightarrow> rAs a t \<approx>2a rAs b s"

   393 | a4: "\<exists>pi. (

   393 

   394          fv_trm2 t1 - fv_assign b1 = fv_trm2 t2 - fv_assign b2 \<and>

   394 lemma alpha2_equivp:

   395          (fv_trm2 t1 - fv_assign b1) \<sharp>* pi \<and>

   395   "equivp alpha2"

   396          pi \<bullet> t1 = t2       (* \<and> (pi \<bullet> b1 = b2) *)

   396   "equivp alpha2a"

   397        ) \<Longrightarrow> Lt2 b1 t1 \<approx>2 Lt2 b2 t2"

   398 

   399 lemma alpha2_equivp: "equivp alpha2" 

   402 quotient_type qtrm2 = trm2 / alpha2

   399 quotient_type

   403   by (rule alpha2_equivp)

   400   trm2 = rtrm2 / alpha2

   401 and

   402   assign = rassign / alpha2a

   403   by (auto intro: alpha2_equivp)

   404