1 theory Perm

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

     3 begin

     4 

     5 atom_decl name

     6 

     7 datatype rtrm1 =

     8   rVr1 "name"

     9 | rAp1 "rtrm1" "rtrm1 list"

    10 | rLm1 "name" "rtrm1"

    11 | rLt1 "bp" "rtrm1" "rtrm1"

    12 and bp =

    13   BUnit

    14 | BVr "name"

    15 | BPr "bp" "bp"

    16 

    17 ML {*

    18   open Datatype_Aux (* typ_of_dtyp, DtRec, ... *)

    19 *}

    20 

    21 instantiation rtrm1 and bp :: pt

    22 begin

    23 

    24 

    25 ML {*

    26   val {descr, induct, ...} = Datatype.the_info @{theory} "Perm.rtrm1";

    27   val new_type_names = ["rtrm1", "bp"];

    28   (* TODO: [] should be the sorts that we'll take from the specification *)

    29   val sorts = [];

    30 

    31   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);

    32   val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) =>

    33     "permute_" ^ name_of_typ (nth_dtyp i)) descr);

    34   val perm_names = replicate (length new_type_names) @{const_name permute} @

    35     map (Sign.full_bname @{theory}) (List.drop (perm_names', length new_type_names));

    36   val perm_types = map (fn (i, _) =>

    37     let val T = nth_dtyp i

    38     in @{typ perm} --> T --> T end) descr;

    39   val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);

    40   (* TODO: Next line only needed after instantiation *)

    41   val perm_names_types = perm_names ~~ perm_types;

    42   val perm_names_types' = perm_names' ~~ perm_types;

    43 

    44   val pi = Free ("pi", @{typ perm});

    45   fun permute ty = Const (@{const_name permute}, @{typ perm} --> ty --> ty);

    46   val minus_perm = Const (@{const_name minus}, @{typ perm} --> @{typ perm});

    47 *}

    48 ML {*

    49   val perm_eqs = maps (fn (i, (_, _, constrs)) =>

    50     let val T = nth_dtyp i

    51     in map (fn (cname, dts) =>

    52       let

    53         val Ts = map (typ_of_dtyp descr sorts) dts;

    54         val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);

    55         val args = map Free (names ~~ Ts);

    56         val c = Const (cname, Ts ---> T);

    57         fun perm_arg (dt, x) =

    58           let val T = type_of x

    59           in

    60             if is_rec_type dt then

    61               let val (Us, _) = strip_type T

    62               in list_abs (map (pair "x") Us,

    63                 Free (nth perm_names_types' (body_index dt)) $ pi $

    64                   list_comb (x, map (fn (i, U) =>

    65                     (permute U) $ (minus_perm $ pi) $ Bound i)

    66                     ((length Us - 1 downto 0) ~~ Us)))

    67               end

    68             else (permute T) $ pi $ x

    69           end;

    70       in

    71         (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq

    72           (Free (nth perm_names_types' i) $

    73              Free ("pi", @{typ perm}) $ list_comb (c, args),

    74            list_comb (c, map perm_arg (dts ~~ args)))))

    75       end) constrs

    76     end) descr;

    77 *}

    78 

    79 local_setup {*

    80 snd o (Primrec.add_primrec

    81   (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs)

    82 *}

    83 

    84 print_theorems

    85 

    86 ML {*

    87    val perm_empty_thms =

    88      let

    89        val gl =

    90          HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj

    91            (map (fn ((s, T), x) => HOLogic.mk_eq

    92                (Const (s, @{typ perm} --> T --> T) $

    93                   @{term "0 :: perm"} $ Free (x, T),

    94                 Free (x, T)))

    95             (perm_names ~~

    96              map body_type perm_types ~~ perm_indnames)));

    97        fun tac _ =

    98          EVERY [indtac induct perm_indnames 1,

    99            ALLGOALS (asm_full_simp_tac @{simpset})];

   100      in

   101        map Drule.export_without_context (List.take (split_conj_thm

   102          (Goal.prove_global @{theory} [] [] gl tac),

   103        length new_type_names))

   104      end

   105 *}

   106 

   107 ML {*

   108    val add_perm = @{term "op + :: (perm \<Rightarrow> perm \<Rightarrow> perm)"}

   109    val pi1 = Free ("pi1", @{typ perm});

   110    val pi2 = Free ("pi2", @{typ perm});

   111    val perm_append_thms =

   112       List.take (map Drule.export_without_context (split_conj_thm

   113         (Goal.prove_global @{theory} [] []

   114            (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj

   115               (map (fn ((s, T), x) =>

   116                   let

   117                     val perm = Const (s, @{typ perm} --> T --> T);

   118                     val lhs = perm $ (add_perm $ pi1 $ pi2) $ Free (x, T)

   119                     val rhs = perm $ pi1 $ (perm $ pi2 $ Free (x, T))

   120                   in HOLogic.mk_eq (lhs, rhs)

   121                   end)

   122                 (perm_names ~~

   123                  map body_type perm_types ~~ perm_indnames))))

   124            (fn _ => EVERY [indtac induct perm_indnames 1,

   125               ALLGOALS (asm_full_simp_tac @{simpset})]))),

   126          length new_type_names)

   127 *}

   128 

   129 instance

   130 apply(tactic {*

   131  (Class.intro_classes_tac []) THEN

   132  (ALLGOALS (simp_tac (@{simpset} addsimps (perm_empty_thms @ perm_append_thms)))) *})

   133 done

   134 end