62 ML {*

    62 

    63 fun define_raw_perms (dt_info : Datatype_Aux.info) number thy =

    63 (* definitions of the permute function for a raw nominal datatype *)

    64 let

    64 

    65   val {descr, induct, sorts, ...} = dt_info;

    65 ML {*

    66   val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;

    66 fun nth_dtyp dt_descr sorts i = 

    67   val full_tnames = List.take (all_full_tnames, number);

    67   Datatype_Aux.typ_of_dtyp dt_descr sorts (Datatype_Aux.DtRec i);

    68   fun nth_dtyp i = Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i);

    68 *}

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

    69 

    70     "permute_" ^ Datatype_Aux.name_of_typ (nth_dtyp i)) descr);

    70 ML {*

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

    71 (* permutation function for one argument *)

    72     let val T = nth_dtyp i

    72 fun perm_arg permute_fns pi (arg_dty, arg) =

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

    73 let 

    74   val perm_names_types' = perm_names' ~~ perm_types;

    74   val T = type_of arg

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

    75 in

    76   fun perm_eq_constr i (cname, dts) =

    76   if Datatype_Aux.is_rec_type arg_dty 

    77     let

    77   then 

    78       val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) dts;

    78     let 

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

    79       val (Us, _) = strip_type T

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

    80       val indxs_tys = (length Us - 1 downto 0) ~~ Us

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

    81     in 

    82       fun perm_arg (dt, x) =

    82       list_abs (map (pair "x") Us,

    83         let val T = type_of x

    83         Free (nth permute_fns (Datatype_Aux.body_index arg_dty)) $ pi $

    84         in

    84           list_comb (arg, map (fn (i, U) => (mk_perm_ty U (mk_minus pi) (Bound i))) indxs_tys))

    85           if Datatype_Aux.is_rec_type dt then

    85     end

    86             let val (Us, _) = strip_type T

    86   else mk_perm_ty T pi arg

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

    87 end

    88               Free (nth perm_names_types' (Datatype_Aux.body_index dt)) $ pi $

    88 *}

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

    89 

    90                   (mk_perm_ty U (mk_minus pi) (Bound i)))

    90 ML {*

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

    91 (* equation for permutation function for one constructor *)

    92             end

    92 fun perm_eq_constr thy dt_descr sorts permute_fns i (cnstr_name, dts) =

    93           else (mk_perm_ty T pi x)

    93 let

    94         end;

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

    95     in

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

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

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

    97         (Free (nth perm_names_types' i) $

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

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

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

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

    99   val lhs = Free (nth permute_fns i) $ pi $ list_comb (cnstr, args)

   100     end;

   100   val rhs = list_comb (cnstr, map (perm_arg permute_fns pi) (dts ~~ args))

   101     fun perm_eq (i, (_, _, constrs)) = map (perm_eq_constr i) constrs;

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

   102     val perm_eqs = maps perm_eq descr;

   102 in

   103     val lthy =

   103   (Attrib.empty_binding, eq)

   104       Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;

   104 end

   105     val ((perm_frees, perm_ldef), lthy') =

   105 *}

   106       Primrec.add_primrec

   106 

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

   107 ML {*

   108     val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, number);

   108 (* defines the permutation functions for raw datatypes and

   109     val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, number)

   109    proves that they are instances of pt

   110     val perms_name = space_implode "_" perm_names'

   110 *)

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

   111 fun define_raw_perms (dt_info : Datatype_Aux.info) dt_nos thy =

   112     val perms_append_bind = Binding.name (perms_name ^ "_append")

   112 let

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

   113   val {descr as dt_descr, induct, sorts, ...} = dt_info;

   114       (Class.intro_classes_tac []) THEN (ALLGOALS (resolve_tac simps));

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

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

   115   val full_tnames = List.take (all_full_tnames, dt_nos);

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

   116 

   117   in

   117   val perm_fn_names = Datatype_Prop.indexify_names (map (fn (i, _) =>

   118   lthy'

   118     "permute_" ^ Datatype_Aux.name_of_typ (nth_dtyp dt_descr sorts i)) dt_descr);

   119   |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms))

   119 

   120   |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms))

   120   val perm_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr

   121   |> Class_Target.prove_instantiation_exit_result morphism tac 

   121 

   122       (perm_ldef, (perm_empty_thms @ perm_append_thms), perm_frees)

   122   val permute_fns = perm_fn_names ~~ perm_types

   123   end

   123 

   124 

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

   125 *}

   125     map (perm_eq_constr thy dt_descr sorts permute_fns i) constrs;

   126 

   126 

   127 ML {*

   127   val perm_eqs = maps perm_eq dt_descr;

   128 fun define_lifted_perms qtys full_tnames name_term_pairs thms thy =

   128 

   129 let

   132   val (_, _, lthy') = quotient_lift_consts_export qtys name_term_pairs lthy;

   131    

   133   val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms;

   132   val ((perm_frees, perm_ldef), lthy') =

   134   fun tac _ =

   133     Primrec.add_primrec

   135     Class.intro_classes_tac [] THEN

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

   136     (ALLGOALS (resolve_tac lifted_thms))

   135     

   137   val lthy'' = Class.prove_instantiation_instance tac lthy'

   136   val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, dt_nos);

   138 in

   137   val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, dt_nos)

   139   Local_Theory.exit_global lthy''

   138   val perms_name = space_implode "_" perm_fn_names

   140 end

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

   141 *}

   140   val perms_append_bind = Binding.name (perms_name ^ "_append")

   142 

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

   143 ML {*

   142     (Class.intro_classes_tac []) THEN (ALLGOALS (resolve_tac simps));

   144 fun neq_to_rel r neq =

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

   145 let

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

   146   val neq = HOLogic.dest_Trueprop (prop_of neq)

   145   in

   147   val eq = HOLogic.dest_not neq

   146     lthy'

   148   val (lhs, rhs) = HOLogic.dest_eq eq

   147     |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms))

   149   val rel = r $ lhs $ rhs

   148     |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms))

   150   val nrel = HOLogic.mk_not rel

   149     |> Class_Target.prove_instantiation_exit_result morphism tac 

   151 in

   150          (perm_ldef, (perm_empty_thms @ perm_append_thms), perm_frees)

   152   HOLogic.mk_Trueprop nrel

   151   end

   153 end

   152 *}

   154 *}

   153 

   155 

   154 (* Test *)

   156 ML {*

   157 fun neq_to_rel_tac cases distinct =

   158   rtac notI THEN' eresolve_tac cases THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct)

   159 *}

   160 

   161 ML {*

   162 fun distinct_rel ctxt cases (dists, rel) =

   163 let

   164   val ((_, thms), ctxt') = Variable.import false dists ctxt

   165   val terms = map (neq_to_rel rel) thms

   166   val nrels = map (fn t => Goal.prove ctxt' [] [] t (fn _ => neq_to_rel_tac cases dists 1)) terms

   167 in

   168   Variable.export ctxt' ctxt nrels

   169 end

   170 *}

   171 

   172 

   173 

   174 (* Test

   187 

   167 setup {* fn thy =>

   188 setup {* snd o define_raw_perms ["trm", "bp"] ["Perm.trm", "Perm.bp"] *}

   168 let 

   169   val info = Datatype.the_info thy "Perm.trm"

   170 in

   171   define_raw_perms info 2 thy |> snd

   172 end

   173 *}

   174 

   192 end

   178 ML {*

   179 fun define_lifted_perms qtys full_tnames name_term_pairs thms thy =

   180 let

   181   val lthy =

   182     Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;

   183   val (_, _, lthy') = quotient_lift_consts_export qtys name_term_pairs lthy;

   184   val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms;

   185   fun tac _ =

   186     Class.intro_classes_tac [] THEN

   187     (ALLGOALS (resolve_tac lifted_thms))

   188   val lthy'' = Class.prove_instantiation_instance tac lthy'

   189 in

   190   Local_Theory.exit_global lthy''

   191 end

   192 *}

   193 

   194 ML {*

   195 fun neq_to_rel r neq =

   196 let

   197   val neq = HOLogic.dest_Trueprop (prop_of neq)

   198   val eq = HOLogic.dest_not neq

   199   val (lhs, rhs) = HOLogic.dest_eq eq

   200   val rel = r $ lhs $ rhs

   201   val nrel = HOLogic.mk_not rel

   202 in

   203   HOLogic.mk_Trueprop nrel

   204 end

   205 *}

   206 

   207 ML {*

   208 fun neq_to_rel_tac cases distinct =

   209   rtac notI THEN' eresolve_tac cases THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct)

   210 *}

   211 

   212 ML {*

   213 fun distinct_rel ctxt cases (dists, rel) =

   214 let

   215   val ((_, thms), ctxt') = Variable.import false dists ctxt

   216   val terms = map (neq_to_rel rel) thms

   217   val nrels = map (fn t => Goal.prove ctxt' [] [] t (fn _ => neq_to_rel_tac cases dists 1)) terms

   218 in

   219   Variable.export ctxt' ctxt nrels

   220 end

   221 *}

   222 

   223 

   224 

   225 (* Test *)

   226 (*atom_decl name

   227 

   228 datatype trm =

   229   Var "name"

   230 | App "trm" "trm list"

   231 | Lam "name" "trm"

   232 | Let "bp" "trm" "trm"

   233 and bp =

   234   BUnit

   235 | BVar "name"

   236 | BPair "bp" "bp"

   237 

   238 setup {* fn thy =>

   239 let 

   240   val inf = Datatype.the_info thy "Perm.trm"

   241 in

   242   define_raw_perms inf 2 thy |> snd

   243 end

   244 *}

   245 

   246 print_theorems

   247 *)

   248 

   249 end