1 theory TestMorePerm

     2 imports "Parser"

     3 begin

     4 

     5 (* Since there are more permutations, we do not know how to prove equivalence

     6    (it is probably not true with the way alpha is defined now) so *)

     7 ML {* val _ = cheat_equivp := true *}

     8 

     9 

    10 atom_decl name

    11 

    12 (* example from my PHD *)

    13 

    14 atom_decl coname

    15 

    16 nominal_datatype phd =

    17    Ax "name" "coname"

    18 |  Cut n::"coname" t1::"phd" c::"coname" t2::"phd"              bind n in t1, bind c in t2

    19 |  AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname"  bind c1 in t1, bind c2 in t2

    20 |  AndL1 n::"name" t::"phd" "name"                              bind n in t

    21 |  AndL2 n::"name" t::"phd" "name"                              bind n in t

    22 |  ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name"        bind c in t1, bind n in t2

    23 |  ImpR c::"coname" n::"name" t::"phd" "coname"                 bind n in t, bind c in t

    24 

    25 thm phd.fv

    26 thm phd.eq_iff

    27 thm phd.bn

    28 thm phd.perm

    29 thm phd.induct

    30 thm phd.distinct

    31 thm phd.fv[simplified phd.supp]

    32 

    33 text {* weirdo example from Peter Sewell's bestiary *}

    34 

    35 nominal_datatype weird =

    36   WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"

    37     bind x in p1, bind x in p2, bind y in p2, bind y in p3

    38 | WV "name"

    39 | WP "weird" "weird"

    40 

    41 thm permute_weird_raw.simps[no_vars]

    42 thm alpha_weird_raw.intros[no_vars]

    43 thm fv_weird_raw.simps[no_vars]

    44 

    45 

    46 end

    47 

    48 

    49