2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs"

     2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm"

    42 (* needs to be stated by the package *)

    42 setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *}

    43 instantiation 

    44   rtrm1 and bp :: pt

    45 begin

    46 

    47 primrec

    48   permute_rtrm1 and permute_bp

    49 where

    50   "permute_rtrm1 pi (rVr1 a) = rVr1 (pi \<bullet> a)"

    51 | "permute_rtrm1 pi (rAp1 t1 t2) = rAp1 (permute_rtrm1 pi t1) (permute_rtrm1 pi t2)"

    52 | "permute_rtrm1 pi (rLm1 a t) = rLm1 (pi \<bullet> a) (permute_rtrm1 pi t)"

    53 | "permute_rtrm1 pi (rLt1 bp t1 t2) = rLt1 (permute_bp pi bp) (permute_rtrm1 pi t1) (permute_rtrm1 pi t2)"

    54 | "permute_bp pi (BUnit) = BUnit"

    55 | "permute_bp pi (BVr a) = BVr (pi \<bullet> a)"

    56 | "permute_bp pi (BPr bp1 bp2) = BPr (permute_bp pi bp1) (permute_bp pi bp2)"

    57 

    58 lemma pt_rtrm1_bp_zero:

    59   fixes t::rtrm1

    60   and   b::bp

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

    62   and   "0 \<bullet> b = b"

    63 apply(induct t and b rule: rtrm1_bp.inducts)

    64 apply(simp_all)

    65 done

    66 

    67 lemma pt_rtrm1_bp_plus:

    68   fixes t::rtrm1

    69   and   b::bp

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

    71   and   "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)"

    72 apply(induct t and b rule: rtrm1_bp.inducts)

    73 apply(simp_all)

    74 done

    75 

    76 instance

    77 apply default

    78 apply(simp_all add: pt_rtrm1_bp_zero pt_rtrm1_bp_plus)

    79 done

    80 

    81 end

   343 (* needs to be stated by the package *)

   304 setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *}

   344 instantiation

   345   rtrm2 and rassign :: pt

   346 begin

   347 

   348 primrec

   349   permute_rtrm2 and permute_rassign

   350 where

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

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

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

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

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

   356 

   357 lemma pt_rtrm2_rassign_zero:

   358   fixes t::rtrm2

   359   and   b::rassign

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

   361   and   "0 \<bullet> b = b"

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

   363 apply(simp_all)

   364 done

   365 

   366 lemma pt_rtrm2_rassign_plus:

   367   fixes t::rtrm2

   368   and   b::rassign

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

   370   and   "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)"

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

   372 apply(simp_all)

   373 done

   374 

   375 instance

   376 apply default

   377 apply(simp_all add: pt_rtrm2_rassign_zero pt_rtrm2_rassign_plus)

   378 done

   379 

   380 

   381 end

   437 (* needs to be stated by the package *)

   360 setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.assigns"] *}

   438 instantiation

   439  trm3 and assigns :: pt

   440 begin

   441 

   442 primrec

   443   permute_trm3 and permute_assigns

   444 where

   445   "permute_trm3 pi (Vr3 a) = Vr3 (pi \<bullet> a)"

   446 | "permute_trm3 pi (Ap3 t1 t2) = Ap3 (permute_trm3 pi t1) (permute_trm3 pi t2)"

   447 | "permute_trm3 pi (Lm3 a t) = Lm3 (pi \<bullet> a) (permute_trm3 pi t)"

   448 | "permute_trm3 pi (Lt3 as t) = Lt3 (permute_assigns pi as) (permute_trm3 pi t)"

   449 | "permute_assigns pi (ANil) = ANil"

   450 | "permute_assigns pi (ACons a t as) = ACons (pi \<bullet> a) (permute_trm3 pi t) (permute_assigns pi as)"

   451 

   452 lemma pt_trm3_assigns_zero:

   453   fixes t::trm3

   454   and   b::assigns

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

   456   and   "0 \<bullet> b = b"

   457 apply(induct t and b rule: trm3_assigns.inducts)

   458 apply(simp_all)

   459 done

   460 

   461 lemma pt_trm3_assigns_plus:

   462   fixes t::trm3

   463   and   b::assigns

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

   465   and   "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)"

   466 apply(induct t and b rule: trm3_assigns.inducts)

   467 apply(simp_all)

   468 done

   469 

   470 instance

   471 apply default

   472 apply(simp_all add: pt_trm3_assigns_zero pt_trm3_assigns_plus)

   473 done

   474 

   475 

   476 end

   522 

   406 (* there cannot be a clause for lists, as *)

   523 (* needs to be stated by the package *)

   524 (* there cannot be a clause for lists, as *) 

   526 instantiation

   408 setup {* snd o define_raw_perms ["trm4"] ["Terms.trm4"] *}

   527   trm4 :: pt

   528 begin

   529 

   530 (* does not work yet *)

   531 primrec

   532   permute_trm4  and permute_trm4_list

   533 where

   534   "permute_trm4 pi (Vr4 a) = Vr4 (pi \<bullet> a)"

   535 | "permute_trm4 pi (Ap4 t ts) = Ap4 (permute_trm4 pi t) (permute_trm4_list pi ts)"

   536 | "permute_trm4 pi (Lm4 a t) = Lm4 (pi \<bullet> a) (permute_trm4 pi t)"

   537 | "permute_trm4_list pi ([]) = []"

   538 | "permute_trm4_list pi (t#ts) = (permute_trm4 pi t) # (permute_trm4_list pi ts)"

   539 

   540 lemma pt_trm4_list_zero:

   541   fixes t::trm4

   542   and   ts::"trm4 list"

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

   544   and   "permute_trm4_list 0 ts = ts"

   545 apply(induct t and ts rule: trm4.inducts)

   546 apply(simp_all)

   547 done

   548 

   549 lemma pt_trm4_list_plus:

   550   fixes t::trm4

   551   and   ts::"trm4 list"

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

   553   and   "(permute_trm4_list (p + q) ts) = permute_trm4_list p (permute_trm4_list q ts)"

   554 apply(induct t and ts rule: trm4.inducts)

   555 apply(simp_all)

   556 done

   557 

   558 

   559 instance

   560 apply(default)

   561 apply(simp_all add: pt_trm4_list_zero pt_trm4_list_plus)

   562 done

   563 

   564 end

   619 instantiation

   463 setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *}

   620   rtrm5 and rlts :: pt

   464 print_theorems

   621 begin

   622 

   623 primrec

   624   permute_rtrm5 and permute_rlts

   625 where

   626   "permute_rtrm5 pi (rVr5 a) = rVr5 (pi \<bullet> a)"

   627 | "permute_rtrm5 pi (rAp5 t1 t2) = rAp5 (permute_rtrm5 pi t1) (permute_rtrm5 pi t2)"

   628 | "permute_rtrm5 pi (rLt5 ls t) = rLt5 (permute_rlts pi ls) (permute_rtrm5 pi t)"

   629 | "permute_rlts pi (rLnil) = rLnil"

   630 | "permute_rlts pi (rLcons n t ls) = rLcons (pi \<bullet> n) (permute_rtrm5 pi t) (permute_rlts pi ls)"

   631 

   632 lemma pt_rtrm5_zero:

   633   fixes t::rtrm5

   634   and   l::rlts

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

   636   and   "0 \<bullet> l = l"

   637 apply(induct t and l rule: rtrm5_rlts.inducts)

   638 apply(simp_all)

   639 done

   640 

   641 lemma pt_rtrm5_plus:

   642   fixes t::rtrm5

   643   and   l::rlts

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

   645   and   "((p + q) \<bullet> l) = p \<bullet> (q \<bullet> l)"

   646 apply(induct t and l rule: rtrm5_rlts.inducts)

   647 apply(simp_all)

   648 done

   649 

   650 instance

   651 apply default

   652 apply(simp_all add: pt_rtrm5_zero pt_rtrm5_plus)

   653 done

   654 

   655 end

   949 instantiation

   758 setup {* snd o define_raw_perms ["rtrm6"] ["Terms.rtrm6"] *}

   950   rtrm6 :: pt

   759 print_theorems

   951 begin

   952 

   953 primrec

   954   permute_rtrm6

   955 where

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

   957 | "permute_rtrm6 pi (rLm6 n t) = rLm6 (pi \<bullet> n) (permute_rtrm6 pi t)"

   958 | "permute_rtrm6 pi (rLt6 l r) = rLt6 (permute_rtrm6 pi l) (permute_rtrm6 pi r)"

   959 

   960 lemma pt_rtrm6_zero:

   961   fixes t::rtrm6

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

   963 apply(induct t)

   964 apply(simp_all)

   965 done

   966 

   967 lemma pt_rtrm6_plus:

   968   fixes t::rtrm6

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

   970 apply(induct t)

   971 apply(simp_all)

   972 done

   973 

   974 instance

   975 apply default

   976 apply(simp_all add: pt_rtrm6_zero pt_rtrm6_plus)

   977 done

   978 

   979 end

  1137 instantiation

   917 setup {* snd o define_raw_perms ["rtrm7"] ["Terms.rtrm7"] *}

  1138   rtrm7 :: pt

   918 print_theorems

  1139 begin

  1140 

  1141 primrec

  1142   permute_rtrm7

  1143 where

  1144   "permute_rtrm7 pi (rVr7 a) = rVr7 (pi \<bullet> a)"

  1145 | "permute_rtrm7 pi (rLm7 a t) = rLm7 (pi \<bullet> a) (permute_rtrm7 pi t)"

  1146 | "permute_rtrm7 pi (rLt7 t1 t2) = rLt7 (permute_rtrm7 pi t1) (permute_rtrm7 pi t2)"

  1147 

  1148 lemma pt_rtrm7_zero:

  1149   fixes t::rtrm7

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

  1151 apply(induct t)

  1152 apply(simp_all)

  1153 done

  1154 

  1155 lemma pt_rtrm7_plus:

  1156   fixes t::rtrm7

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

  1158 apply(induct t)

  1159 apply(simp_all)

  1160 done

  1161 

  1162 instance

  1163 apply default

  1164 apply(simp_all add: pt_rtrm7_zero pt_rtrm7_plus)

  1165 done

  1166 

  1167 end

  1219 instantiation

   970 setup {* snd o define_raw_perms ["rfoo8", "rbar8"] ["Terms.rfoo8", "Terms.rbar8"] *}

  1220   rfoo8 and rbar8 :: pt

   971 print_theorems

  1221 begin

  1222 

  1223 primrec

  1224   permute_rfoo8 and permute_rbar8

  1225 where

  1226   "permute_rfoo8 pi (Foo0 a) = Foo0 (pi \<bullet> a)"

  1227 | "permute_rfoo8 pi (Foo1 b t) = Foo1 (permute_rbar8 pi b) (permute_rfoo8 pi t)"

  1228 | "permute_rbar8 pi (Bar0 a) = Bar0 (pi \<bullet> a)"

  1229 | "permute_rbar8 pi (Bar1 v x t) = Bar1 (pi \<bullet> v) (pi \<bullet> x) (permute_rbar8 pi t)"

  1230 

  1231 instance sorry

  1232 

  1233 end

  1289 instantiation

  1027 setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Terms.rlam9", "Terms.rbla9"] *}

  1290   rlam9 and rbla9 :: pt

  1028 print_theorems

  1291 begin

  1292 

  1293 primrec

  1294   permute_rlam9 and permute_rbla9

  1295 where

  1296   "permute_rlam9 pi (Var9 a) = Var9 (pi \<bullet> a)"

  1297 | "permute_rlam9 pi (Lam9 b t) = Lam9 (pi \<bullet> b) (permute_rlam9 pi t)"

  1298 | "permute_rbla9 pi (Bla9 l r) = Bla9 (permute_rlam9 pi l) (permute_rlam9 pi r)"

  1299 

  1300 instance sorry

  1301 

  1302 end

  1383 instantiation

  1109 setup {* snd o define_raw_perms ["ty"] ["Terms.ty"] *}

  1384   ty :: pt

  1110 print_theorems

  1385 begin

  1386 

  1387 primrec

  1388   permute_ty 

  1389 where

  1390   "permute_ty pi (Var a) = Var (pi \<bullet> a)"

  1391 | "permute_ty pi (Fun T1 T2) = Fun (permute_ty pi T1) (permute_ty pi T2)"

  1392 

  1393 lemma pt_ty_zero:

  1394   fixes T::ty

  1395   shows "0 \<bullet> T = T"

  1396 apply(induct T rule: ty.inducts)

  1397 apply(simp_all)

  1398 done

  1399 

  1400 lemma pt_ty_plus:

  1401   fixes T::ty

  1402   shows "((p + q) \<bullet> T) = p \<bullet> (q \<bullet> T)"

  1403 apply(induct T rule: ty.inducts)

  1404 apply(simp_all)

  1405 done

  1406 

  1407 instance

  1408 apply default

  1409 apply(simp_all add: pt_ty_zero pt_ty_plus)

  1410 done

  1411 

  1412 end

  1417 instantiation

  1115 setup {* snd o define_raw_perms ["tyS"] ["Terms.tyS"] *}

  1418   tyS :: pt

  1116 print_theorems

  1419 begin

  1420 

  1421 primrec

  1422   permute_tyS 

  1423 where

  1424   "permute_tyS pi (All xs T) = All (pi \<bullet> xs) (pi \<bullet> T)"

  1425 

  1426 lemma pt_tyS_zero:

  1427   fixes T::tyS

  1428   shows "0 \<bullet> T = T"

  1429 apply(induct T rule: tyS.inducts)

  1430 apply(simp_all)

  1431 done

  1432 

  1433 lemma pt_tyS_plus:

  1434   fixes T::tyS

  1435   shows "((p + q) \<bullet> T) = p \<bullet> (q \<bullet> T)"

  1436 apply(induct T rule: tyS.inducts)

  1437 apply(simp_all)

  1438 done

  1439 

  1440 instance

  1441 apply default

  1442 apply(simp_all add: pt_tyS_zero pt_tyS_plus)

  1443 done

  1444 

  1445 end

  1446