4 

     5 (* definitions of the permute function for raw nominal datatypes *)

     6 

     7 

     8 ML {*

     9 (* returns the type of the nth datatype *)

    10 fun nth_dtyp descr sorts n = 

    11   Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n);

    12 

    13 (* returns the constructors of the nth datatype *)

    14 fun nth_dtyp_constrs descr n = 

    15 let

    16   val (_, (_, _, constrs)) = nth descr n

    17 in

    18   constrs

    19 end

    20 

    21 (* returns the types of the constructors of the nth datatype *)

    22 fun nth_dtyp_constr_typs descr sorts n = 

    23   map (map (Datatype_Aux.typ_of_dtyp descr sorts) o snd) (nth_dtyp_constrs descr n)

    24 *}

    25 

    26 ML {*

    27 (* generates for every datatype a name str ^ dt_name 

    28    plus and index for multiple occurences of a string *)

    29 fun prefix_dt_names descr sorts str = 

    30 let

    31   fun get_nth_name (i, _) = 

    32     Datatype_Aux.name_of_typ (nth_dtyp descr sorts i) 

    33 in

    34   Datatype_Prop.indexify_names 

    35     (map (prefix str o get_nth_name) descr)

    36 end

    37 *}

    38 

    39 

    40 ML {*

    41 (* permutation function for one argument 

    42    

    43     - in case the argument is recursive it returns 

    44 

    45          permute_fn p arg

    46 

    47     - in case the argument is non-recursive it will return

    48 

    49          p o arg

    50 

    51 *)

    52 fun perm_arg permute_fn_frees p (arg_dty, arg) =

    53   if Datatype_Aux.is_rec_type arg_dty 

    54   then (nth permute_fn_frees (Datatype_Aux.body_index arg_dty)) $ p $ arg

    55   else mk_perm p arg

    56 *}

    57 

    58 ML {*

    59 (* generates the equation for the permutation function for one constructor;

    60    i is the index of the corresponding datatype *)

    61 fun perm_eq_constr dt_descr sorts permute_fn_frees i (cnstr_name, dts) =

    62 let

    63   val p = Free ("p", @{typ perm})

    64   val arg_tys = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts

    65   val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys)

    66   val args = map Free (arg_names ~~ arg_tys)

    67   val cnstr = Const (cnstr_name, arg_tys ---> (nth_dtyp dt_descr sorts i))

    68   val lhs = (nth permute_fn_frees i) $ p $ list_comb (cnstr, args)

    69   val rhs = list_comb (cnstr, map (perm_arg permute_fn_frees p) (dts ~~ args))

    70   val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))

    71 in

    72   (Attrib.empty_binding, eq)

    73 end

    74 *}

    75 

    76 ML {*

    77 (* proves the two pt-type class properties *)

    78 fun prove_permute_zero lthy induct perm_defs perm_fns =

    79 let

    80   val perm_types = map (body_type o fastype_of) perm_fns

    81   val perm_indnames = Datatype_Prop.make_tnames perm_types

    82   

    83   fun single_goal ((perm_fn, T), x) =

    84     HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T))

    85 

    86   val goals =

    87     HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj

    88       (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))

    89 

    90   val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs)

    91 

    92   val tac = (Datatype_Aux.indtac induct perm_indnames 

    93              THEN_ALL_NEW asm_simp_tac simps) 1

    94 in

    95   Goal.prove lthy perm_indnames [] goals (K tac)

    96   |> Datatype_Aux.split_conj_thm

    97 end

    98 *}

    99 

   100 ML {*

   101 fun prove_permute_plus lthy induct perm_defs perm_fns =

   102 let

   103   val p = Free ("p", @{typ perm})

   104   val q = Free ("q", @{typ perm})

   105   val perm_types = map (body_type o fastype_of) perm_fns

   106   val perm_indnames = Datatype_Prop.make_tnames perm_types

   107   

   108   fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq 

   109       (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T)))

   110 

   111   val goals =

   112     HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj

   113       (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))

   114 

   115   val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs)

   116 

   117   val tac = (Datatype_Aux.indtac induct perm_indnames

   118              THEN_ALL_NEW asm_simp_tac simps) 1

   119 in

   120   Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac)

   121   |> Datatype_Aux.split_conj_thm 

   122 end

   123 *}

   124 

   125 ML {*

   126 (* defines the permutation functions for raw datatypes and

   127    proves that they are instances of pt

   128 

   129    user_dt_nos refers to the number of "un-unfolded" datatypes

   130    given by the user

   131 *)

   132 fun define_raw_perms dt_descr sorts induct_thm user_dt_nos thy =

   133 let

   134   val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr;

   135   val user_full_tnames = List.take (all_full_tnames, user_dt_nos);

   136 

   137   val perm_fn_names = prefix_dt_names dt_descr sorts "permute_"

   138   val perm_fn_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr

   139   val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types)

   140 

   141   fun perm_eq (i, (_, _, constrs)) = 

   142     map (perm_eq_constr dt_descr sorts perm_fn_frees i) constrs;

   143 

   144   val perm_eqs = maps perm_eq dt_descr;

   145 

   146   val lthy =

   147     Theory_Target.instantiation (user_full_tnames, [], @{sort pt}) thy;

   148    

   149   val ((perm_funs, perm_eq_thms), lthy') =

   150     Primrec.add_primrec

   151       (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy;

   152     

   153   val perm_zero_thms = prove_permute_zero lthy' induct_thm perm_eq_thms perm_funs

   154   val perm_plus_thms = prove_permute_plus lthy' induct_thm perm_eq_thms perm_funs

   155   val perm_zero_thms' = List.take (perm_zero_thms, user_dt_nos);

   156   val perm_plus_thms' = List.take (perm_plus_thms, user_dt_nos)

   157   val perms_name = space_implode "_" perm_fn_names

   158   val perms_zero_bind = Binding.name (perms_name ^ "_zero")

   159   val perms_plus_bind = Binding.name (perms_name ^ "_plus")

   160   

   161   fun tac _ (_, _, simps) =

   162     Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps)

   163   

   164   fun morphism phi (fvs, dfs, simps) =

   165     (map (Morphism.term phi) fvs, map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps);

   166 in

   167   lthy'

   168   |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms'))

   169   |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms'))

   170   |> Class_Target.prove_instantiation_exit_result morphism tac 

   171        (perm_funs, perm_eq_thms, perm_zero_thms' @ perm_plus_thms')

   172 end

   173 *}

   174 

   175 

   176