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   fun perm_eq (i, (_, _, constrs)) =

    50     map (fn (cname, dts) =>

    51       let

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

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

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

    55         val c = Const (cname, Ts ---> (nth_dtyp i));

    56         fun perm_arg (dt, x) =

    57           let val T = type_of x

    58           in

    59             if is_rec_type dt then

    60               let val (Us, _) = strip_type T

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

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

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

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

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

    66               end

    67             else (permute T) $ pi $ x

    68           end;

    69       in

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

    71           (Free (nth perm_names_types' i) $

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

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

    74       end) constrs;

    75   val perm_eqs = maps perm_eq descr;

    76 *}

    77 

    78 local_setup {*

    79 snd o (Primrec.add_primrec

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

    81 *}

    82 

    83 print_theorems

    84 

    85 ML {*

    86    val perm_empty_thms =

    87      let

    88        val gl =

    89          HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj

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

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

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

    93                 Free (x, T)))

    94             (perm_names ~~

    95              map body_type perm_types ~~ perm_indnames)));

    96        fun tac _ =

    97          EVERY [indtac induct perm_indnames 1,

    98            ALLGOALS (asm_full_simp_tac @{simpset})];

    99      in

   100        map Drule.export_without_context (List.take (split_conj_thm

   101          (Goal.prove @{context} [] [] gl tac),

   102        length new_type_names))

   103      end

   104 *}

   105 

   106 ML {*

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

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

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

   110    val perm_append_thms =

   111       List.take (map Drule.export_without_context (split_conj_thm

   112         (Goal.prove @{context} [] []

   113            (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj

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

   115                   let

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

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

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

   119                   in HOLogic.mk_eq (lhs, rhs)

   120                   end)

   121                 (perm_names ~~

   122                  map body_type perm_types ~~ perm_indnames))))

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

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

   125          length new_type_names)

   126 *}

   127 

   128 instance

   129 apply(tactic {*

   130  (Class.intro_classes_tac []) THEN

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

   132 done

   133 end