928 

   929 

   930 

   931 

   932 

   933 

   934 datatype rtrm6 =

   935   rVr6 "name"

   936 | rAp6 "rtrm6" "rtrm6"

   937 | rFo6 "rtrm6" "rtrm6" --"bind (bv6 left) in (right)"

   938 

   939 primrec

   940   rbv6

   941 where

   942   "rbv6 (rVr6 x) = {atom x}"

   943 | "rbv6 (rAp6 l r) = rbv6 l \<union> rbv6 r"

   944 | "rbv6 (rFo6 l r) = rbv6 l - rbv6 r"

   945 

   946 primrec

   947   rfv_trm6

   948 where

   949   "rfv_trm6 (rVr6 n) = {atom n}"

   950 | "rfv_trm6 (rAp6 t s) = (rfv_trm6 t) \<union> (rfv_trm6 s)"

   951 | "rfv_trm6 (rFo6 l r) = (rfv_trm6 r - rbv6 l) \<union> (rfv_trm6 l)"

   952 

   953 instantiation

   954   rtrm6 :: pt

   955 begin

   956 

   957 primrec

   958   permute_rtrm6

   959 where

   960   "permute_rtrm6 pi (rVr6 a) = rVr6 (pi \<bullet> a)"

   961 | "permute_rtrm6 pi (rAp6 t1 t2) = rAp6 (permute_rtrm6 pi t1) (permute_rtrm6 pi t2)"

   962 | "permute_rtrm6 pi (rFo6 l r) = rFo6 (permute_rtrm6 pi l) (permute_rtrm6 pi r)"

   963 

   964 lemma pt_rtrm6_zero:

   965   fixes t::rtrm6

   966   shows "0 \<bullet> t = t"

   967 apply(induct t)

   968 apply(simp_all)

   969 done

   970 

   971 lemma pt_rtrm6_plus:

   972   fixes t::rtrm6

   973   shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"

   974 apply(induct t)

   975 apply(simp_all)

   976 done

   977 

   978 instance

   979 apply default

   980 apply(simp_all add: pt_rtrm6_zero pt_rtrm6_plus)

   981 done

   982 

   983 end

   984 

   985 inductive

   986   alpha6 :: "rtrm6 \<Rightarrow> rtrm6 \<Rightarrow> bool" ("_ \<approx>6 _" [100, 100] 100)

   987 where

   988   a1: "a = b \<Longrightarrow> (rVr6 a) \<approx>6 (rVr6 b)"

   989 | a2: "\<lbrakk>t1 \<approx>6 t2; s1 \<approx>6 s2\<rbrakk> \<Longrightarrow> rAp6 t1 s1 \<approx>6 rAp6 t2 s2"

   990 | a3: "\<lbrakk>\<exists>pi. ((rbv6 l1, r1) \<approx>gen alpha6 rfv_trm6 pi (rbv6 l2, r2))\<rbrakk>

   991         \<Longrightarrow> rFo6 l1 r1 \<approx>6 rFo6 l2 r2"

   992 

   993 lemma alpha6_equivps:

   994   shows "equivp alpha6"

   995 sorry

   996 

   997 quotient_type

   998   trm6 = rtrm6 / alpha6

   999   by (auto intro: alpha6_equivps)

  1000 

  1001 quotient_definition

  1002   "Vr6 :: name \<Rightarrow> trm6"

  1003 as

  1004   "rVr6"

  1005 

  1006 quotient_definition

  1007   "Ap6 :: trm6 \<Rightarrow> trm6 \<Rightarrow> trm6"

  1008 as

  1009   "rAp6"

  1010 

  1011 quotient_definition

  1012   "Fo6 :: trm6 \<Rightarrow> trm6 \<Rightarrow> trm6"

  1013 as

  1014   "rFo6"

  1015 

  1016 quotient_definition

  1017    "fv_trm6 :: trm6 \<Rightarrow> atom set"

  1018 as

  1019   "rfv_trm6"

  1020 

  1021 quotient_definition

  1022    "bv6 :: trm6 \<Rightarrow> atom set"

  1023 as

  1024   "rbv6"

  1025 

  1026 

  1027 

  1028 lemma [quot_respect]:

  1029  "(op = ===> alpha6) rVr6 rVr6"

  1030  "(alpha6 ===> alpha6 ===> alpha6) rAp6 rAp6"

  1031  "(alpha6 ===> alpha6 ===> alpha6) rFo6 rFo6"

  1032 apply (simp_all add: a1 a2)

  1033 apply clarify

  1034 apply (rule a3)

  1035 apply (rule_tac x="0::perm" in exI)

  1036 apply (simp add: alpha_gen)

  1037 (* needs rbv6_rsp *)

  1038 sorry

  1039 

  1040 instantiation trm6 :: pt begin

  1041 

  1042 instance

  1043 sorry

  1044 end

  1045 

  1046 lemma "\<lbrakk>\<exists>pi. ((bv6 l1, r1) \<approx>gen (op =) fv_trm6 pi (bv6 l2, r2))\<rbrakk>

  1047         \<Longrightarrow> Fo6 l1 r1 = Fo6 l2 r2"

  1048 apply (unfold alpha_gen)

  1049 apply (lifting a3[unfolded alpha_gen])

  1050 apply injection

  1051 

  1052 

  1053 

  1054 sorry

  1055 

  1056 

  1057 

  1058 

  1059