1 (*  Title:      nominal_dt_rawperm.ML

     2     Author:     Cezary Kaliszyk

     3     Author:     Christian Urban

     4 

     5   Definitions of the raw bn, fv and fv_bn

     6   functions

     7 *)

     8 

     9 signature NOMINAL_DT_RAWFUNS =

    10 sig

    11   (* binding modes and binding clauses *)

    12 

    13   datatype bmode = Lst | Res | Set

    14 

    15   datatype bclause = BC of bmode * (term option * int) list * int list

    16 

    17   val setify: Proof.context -> term -> term

    18   val listify: Proof.context -> term -> term

    19   val fold_union: term list -> term

    20 

    21   val define_raw_fvs: Datatype_Aux.descr -> (string * sort) list ->

    22     (term * 'a * 'b) list -> (term * int * (int * term option) list list) list ->

    23       bclause list list list -> Proof.context -> term list * term list * thm list * local_theory

    24 end

    25 

    26 

    27 structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS =

    28 struct

    29 

    30 datatype bmode = Lst | Res | Set

    31 datatype bclause = BC of bmode * (term option * int) list * int list

    32 

    33 (* functions that construct differences and unions

    34    but avoid producing empty atom sets *)

    35 

    36 fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"}

    37   | mk_diff (t1, @{term "{}::atom set"}) = t1

    38   | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2)

    39 

    40 fun mk_union (@{term "{}::atom set"}, @{term "{}::atom set"}) = @{term "{}::atom set"}

    41   | mk_union (t1 , @{term "{}::atom set"}) = t1

    42   | mk_union (@{term "{}::atom set"}, t2) = t2

    43   | mk_union (t1, t2) = HOLogic.mk_binop @{const_name sup} (t1, t2)  

    44  

    45 fun fold_union trms = fold (curry mk_union) trms @{term "{}::atom set"}

    46 

    47 

    48 (* atom types *)

    49 fun is_atom ctxt ty =

    50   Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})

    51 

    52 fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t

    53   | is_atom_set _ _ = false;

    54 

    55 fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t

    56   | is_atom_fset _ _ = false;

    57 

    58 fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t

    59   | is_atom_list _ _ = false

    60 

    61 

    62 (* functions for producing sets, fsets and lists *)

    63 fun mk_atom_set t =

    64 let

    65   val ty = fastype_of t;

    66   val atom_ty = HOLogic.dest_setT ty --> @{typ atom};

    67   val img_ty = atom_ty --> ty --> @{typ "atom set"};

    68 in

    69   (Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t)

    70 end;

    71 

    72 fun mk_atom_fset t =

    73 let

    74   val ty = fastype_of t;

    75   val atom_ty = dest_fsetT ty --> @{typ atom};

    76   val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};

    77   val fset_to_set = @{term "fset_to_set :: atom fset => atom set"}

    78 in

    79   fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)

    80 end;

    81 

    82 fun mk_atom_list t =

    83 let

    84   val ty = fastype_of t;

    85   val atom_ty = dest_listT ty --> @{typ atom};

    86   val map_ty = atom_ty --> ty --> @{typ "atom list"};

    87 in

    88   (Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t)

    89 end;

    90 

    91 

    92 (* functions that coerces atoms, sets and fsets into atom sets ? *)

    93 fun setify ctxt t =

    94 let

    95   val ty = fastype_of t;

    96 in

    97   if is_atom ctxt ty

    98     then  HOLogic.mk_set @{typ atom} [mk_atom t]

    99   else if is_atom_set ctxt ty

   100     then mk_atom_set t

   101   else if is_atom_fset ctxt ty

   102     then mk_atom_fset t

   103   else raise TERM ("setify", [t])

   104 end

   105 

   106 (* functions that coerces atoms and lists into atom lists ? *)

   107 fun listify ctxt t =

   108 let

   109   val ty = fastype_of t;

   110 in

   111   if is_atom ctxt ty

   112     then HOLogic.mk_list @{typ atom} [mk_atom t]

   113   else if is_atom_list ctxt ty

   114     then mk_atom_set t

   115   else raise TERM ("listify", [t])

   116 end

   117 

   118 (* coerces a list into a set *)

   119 fun to_set x =

   120   if fastype_of x = @{typ "atom list"}

   121   then @{term "set::atom list => atom set"} $ x

   122   else x

   123 

   124 

   125 

   126 fun make_body fv_map args i = 

   127 let

   128   val arg = nth args i

   129   val ty = fastype_of arg

   130 in

   131   case (AList.lookup (op=) fv_map ty) of

   132     NONE => mk_supp arg

   133   | SOME fv => fv $ arg

   134 end  

   135 

   136 fun make_binder lthy fv_bn_map args (bn_option, i) = 

   137 let

   138   val arg = nth args i

   139 in

   140   case bn_option of

   141     NONE => (setify lthy arg, @{term "{}::atom set"})

   142   | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg)

   143 end  

   144 

   145 fun make_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) =

   146 let

   147   val t1 = map (make_body fv_map args) bodies

   148   val (t2, t3) = split_list (map (make_binder lthy fv_bn_map args) binders)

   149 in 

   150   fold_union (mk_diff (fold_union t1, fold_union t2)::t3)

   151 end

   152 

   153 fun make_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys) bclauses = 

   154 let

   155   val arg_names = Datatype_Prop.make_tnames arg_tys

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

   157   val fv = the (AList.lookup (op=) fv_map ty)

   158   val lhs = fv $ list_comb (constr, args)

   159   val rhs_trms = map (make_fv_rhs lthy fv_map fv_bn_map args) bclauses

   160   val rhs = fold_union rhs_trms

   161 in

   162   HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))

   163 end

   164 

   165 

   166 fun make_bn_body fv_map fv_bn_map bn_args args i = 

   167 let

   168   val arg = nth args i

   169   val ty = fastype_of arg

   170 in

   171   case AList.lookup (op=) bn_args i of

   172     NONE => (case (AList.lookup (op=) fv_map ty) of

   173               NONE => mk_supp arg

   174             | SOME fv => fv $ arg)

   175   | SOME (NONE) => @{term "{}::atom set"}

   176   | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg

   177 end  

   178 

   179 fun make_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause =

   180   case bclause of

   181     BC (_, [], bodies) => fold_union (map (make_bn_body fv_map fv_bn_map bn_args args) bodies)

   182   | BC (_, binders, bodies) => 

   183       let

   184         val t1 = map (make_body fv_map args) bodies

   185         val (t2, t3) = split_list (map (make_binder lthy fv_bn_map args) binders)

   186       in 

   187         fold_union (mk_diff (fold_union t1, fold_union t2)::t3)

   188       end

   189 

   190 fun make_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, ty, arg_tys)) bclauses =

   191 let

   192   val arg_names = Datatype_Prop.make_tnames arg_tys

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

   194   val fv_bn = the (AList.lookup (op=) fv_bn_map bn_trm)

   195   val lhs = fv_bn $ list_comb (constr, args)

   196   val rhs_trms = map (make_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses

   197   val rhs = fold_union rhs_trms

   198 in

   199   HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))

   200 end

   201 

   202 fun make_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = 

   203 let

   204   val nth_constrs_info = nth constrs_info bn_n

   205   val nth_bclausess = nth bclausesss bn_n

   206 in

   207   map2 (make_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess

   208 end

   209 

   210 fun define_raw_fvs dt_descr sorts bn_funs bn_funs2 bclausesss lthy =

   211 let

   212 

   213   val fv_names = prefix_dt_names dt_descr sorts "fv_"

   214   val fv_arg_tys = map (fn (i, _) => nth_dtyp dt_descr sorts i) dt_descr;

   215   val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys;

   216   val fv_frees = map Free (fv_names ~~ fv_tys);

   217   val fv_map = fv_arg_tys ~~ fv_frees

   218 

   219   val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_funs)

   220   val (bns2, bn_tys2) = split_list (map (fn (bn, i, _) => (bn, i)) bn_funs2)

   221   val bn_args2 = map (fn (_, _, arg) => arg) bn_funs2

   222   val fv_bn_names2 = map (fn bn => "fv_" ^ (fst (dest_Free bn))) bns2

   223   val fv_bn_arg_tys2 = map (fn i => nth_dtyp dt_descr sorts i) bn_tys2

   224   val fv_bn_tys2 = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys2

   225   val fv_bn_frees2 = map Free (fv_bn_names2 ~~ fv_bn_tys2)

   226   val fv_bn_map2 = bns ~~ fv_bn_frees2

   227   val fv_bn_map3 = bns2 ~~ fv_bn_frees2

   228  

   229   val constrs_info = all_dtyp_constrs_types dt_descr sorts

   230 

   231   val fv_eqs2 = map2 (map2 (make_fv_eq lthy fv_map fv_bn_map2)) constrs_info bclausesss 

   232   val fv_bn_eqs2 = map (make_fv_bn_eqs lthy fv_map fv_bn_map3 constrs_info bclausesss) bn_funs2

   233   

   234   val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names2)

   235   val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs2 @ flat fv_bn_eqs2)

   236 

   237   fun pat_completeness_auto lthy =

   238     Pat_Completeness.pat_completeness_tac lthy 1

   239       THEN auto_tac (clasimpset_of lthy)

   240 

   241   fun prove_termination lthy =

   242     Function.prove_termination NONE

   243       (Lexicographic_Order.lexicographic_order_tac true lthy) lthy

   244 

   245   val (_, lthy') = Function.add_function all_fv_names all_fv_eqs

   246     Function_Common.default_config pat_completeness_auto lthy

   247 

   248   val (info, lthy'') = prove_termination (Local_Theory.restore lthy')

   249 

   250   val {fs, simps, ...} = info;

   251 

   252   val morphism = ProofContext.export_morphism lthy'' lthy

   253   val fs_exp = map (Morphism.term morphism) fs

   254 

   255   val (fv_frees_exp, fv_bns_exp) = chop (length fv_frees) fs_exp

   256   val simps_exp = Morphism.fact morphism (the simps)

   257 in

   258   (fv_frees_exp, fv_bns_exp, simps_exp, lthy'')

   259 end

   260 

   261 end (* structure *)

   262