Nominal/Perm.thy
changeset 1871 c704d129862b
parent 1774 c34347ec7ab3
child 1896 996d4411e95e
equal deleted inserted replaced
1870:55b2da92ff2f 1871:c704d129862b
     2 imports "../Nominal-General/Nominal2_Atoms"
     2 imports "../Nominal-General/Nominal2_Atoms"
     3 begin
     3 begin
     4 
     4 
     5 ML {*
     5 ML {*
     6   open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *)
     6   open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *)
     7   fun permute ty = Const (@{const_name permute}, @{typ perm} --> ty --> ty);
     7   open Nominal_Library; 
     8   val minus_perm = Const (@{const_name minus}, @{typ perm} --> @{typ perm});
       
     9 *}
     8 *}
    10 
     9 
    11 ML {*
    10 ML {*
    12 fun quotient_lift_consts_export qtys spec ctxt =
    11 fun quotient_lift_consts_export qtys spec ctxt =
    13 let
    12 let
    92           if is_rec_type dt then
    91           if is_rec_type dt then
    93             let val (Us, _) = strip_type T
    92             let val (Us, _) = strip_type T
    94             in list_abs (map (pair "x") Us,
    93             in list_abs (map (pair "x") Us,
    95               Free (nth perm_names_types' (body_index dt)) $ pi $
    94               Free (nth perm_names_types' (body_index dt)) $ pi $
    96                 list_comb (x, map (fn (i, U) =>
    95                 list_comb (x, map (fn (i, U) =>
    97                   (permute U) $ (minus_perm $ pi) $ Bound i)
    96                   (mk_perm_ty U (mk_minus pi) (Bound i)))
    98                   ((length Us - 1 downto 0) ~~ Us)))
    97                   ((length Us - 1 downto 0) ~~ Us)))
    99             end
    98             end
   100           else (permute T) $ pi $ x
    99           else (mk_perm_ty T pi x)
   101         end;
   100         end;
   102     in
   101     in
   103       (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
   102       (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
   104         (Free (nth perm_names_types' i) $
   103         (Free (nth perm_names_types' i) $
   105            Free ("pi", @{typ perm}) $ list_comb (c, args),
   104            Free ("pi", @{typ perm}) $ list_comb (c, args),
   123       (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs);
   122       (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs);
   124   in
   123   in
   125   lthy'
   124   lthy'
   126   |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms))
   125   |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms))
   127   |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms))
   126   |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms))
   128   |> Class_Target.prove_instantiation_exit_result morphism tac (perm_ldef, (perm_empty_thms @ perm_append_thms), perm_frees)
   127   |> Class_Target.prove_instantiation_exit_result morphism tac 
       
   128       (perm_ldef, (perm_empty_thms @ perm_append_thms), perm_frees)
   129   end
   129   end
   130 
   130 
   131 *}
   131 *}
   132 
   132 
   133 ML {*
   133 ML {*