src/HOL/Tools/datatype_prop.ML
changeset 8434 5e4bba59bfaa
parent 7704 9a6783fdb9a5
child 8601 8fb3a81b4ccf
equal deleted inserted replaced
8433:8ae16c770fc8 8434:5e4bba59bfaa
     7 *)
     7 *)
     8 
     8 
     9 signature DATATYPE_PROP =
     9 signature DATATYPE_PROP =
    10 sig
    10 sig
    11   val dtK : int ref
    11   val dtK : int ref
       
    12   val indexify_names: string list -> string list
    12   val make_injs : (int * (string * DatatypeAux.dtyp list *
    13   val make_injs : (int * (string * DatatypeAux.dtyp list *
    13     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    14     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    14       term list list
    15       term list list
    15   val make_ind : (int * (string * DatatypeAux.dtyp list *
    16   val make_ind : (int * (string * DatatypeAux.dtyp list *
    16     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list -> term
    17     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list -> term
    46 open DatatypeAux;
    47 open DatatypeAux;
    47 
    48 
    48 (*the kind of distinctiveness axioms depends on number of constructors*)
    49 (*the kind of distinctiveness axioms depends on number of constructors*)
    49 val dtK = ref 7;
    50 val dtK = ref 7;
    50 
    51 
       
    52 fun indexify_names names =
       
    53   let
       
    54     fun index (x :: xs) tab =
       
    55       (case assoc (tab, x) of
       
    56         None => if x mem xs then (x ^ "1") :: index xs ((x, 2) :: tab) else x :: index xs tab
       
    57       | Some i => (x ^ Library.string_of_int i) :: index xs ((x, i + 1) :: tab))
       
    58     | index [] _ = [];
       
    59   in index names [] end;
       
    60 
    51 fun make_tnames Ts =
    61 fun make_tnames Ts =
    52   let
    62   let
    53     fun type_name (TFree (name, _)) = implode (tl (explode name))
    63     fun type_name (TFree (name, _)) = implode (tl (explode name))
    54       | type_name (Type (name, _)) = 
    64       | type_name (Type (name, _)) = 
    55           let val name' = Sign.base_name name
    65           let val name' = Sign.base_name name
    56           in if Syntax.is_identifier name' then name' else "x"
    66           in if Syntax.is_identifier name' then name' else "x" end;
    57           end;
    67   in indexify_names (map type_name Ts) end;
    58 
    68 
    59     fun index_vnames (vn::vns) tab =
    69 
    60           (case assoc (tab, vn) of
       
    61              None => if vn mem vns
       
    62                      then (vn ^ "1") :: index_vnames vns ((vn, 2)::tab)
       
    63                      else vn :: index_vnames vns tab
       
    64            | Some i => (vn ^ (string_of_int i))::
       
    65                      index_vnames vns ((vn, i + 1)::tab))
       
    66       | index_vnames [] _ = []
       
    67 
       
    68   in index_vnames (map type_name Ts) []
       
    69   end;
       
    70 
       
    71 (** FIXME: move to hologic.ML ? **)
       
    72 val Not = Const ("Not", HOLogic.boolT --> HOLogic.boolT);
       
    73 
    70 
    74 (************************* injectivity of constructors ************************)
    71 (************************* injectivity of constructors ************************)
    75 
    72 
    76 fun make_injs descr sorts =
    73 fun make_injs descr sorts =
    77   let
    74   let
   301                     val Ts' = map (typ_of_dtyp descr' sorts) cargs';
   298                     val Ts' = map (typ_of_dtyp descr' sorts) cargs';
   302                     val frees' = map Free ((map ((op ^) o (rpair "'"))
   299                     val frees' = map Free ((map ((op ^) o (rpair "'"))
   303                       (make_tnames Ts')) ~~ Ts');
   300                       (make_tnames Ts')) ~~ Ts');
   304                     val t' = list_comb (Const (cname', Ts' ---> T), frees')
   301                     val t' = list_comb (Const (cname', Ts' ---> T), frees')
   305                   in
   302                   in
   306                     (HOLogic.mk_Trueprop (Not $ HOLogic.mk_eq (t, t')))::
   303                     (HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.mk_eq (t, t')))::
   307                     (HOLogic.mk_Trueprop (Not $ HOLogic.mk_eq (t', t)))::
   304                     (HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.mk_eq (t', t)))::
   308                       (make_distincts' constrs')
   305                       (make_distincts' constrs')
   309                   end
   306                   end
   310 
   307 
   311           in (make_distincts' constrs) @ (make_distincts_1 T constrs)
   308           in (make_distincts' constrs) @ (make_distincts_1 T constrs)
   312           end;
   309           end;
   341               list_comb (Const (cname, Ts ---> T), frees));
   338               list_comb (Const (cname, Ts ---> T), frees));
   342             val P' = P $ list_comb (f, frees)
   339             val P' = P $ list_comb (f, frees)
   343           in ((foldr (fn (Free (s, T), t) => HOLogic.mk_all (s, T, t))
   340           in ((foldr (fn (Free (s, T), t) => HOLogic.mk_all (s, T, t))
   344                 (frees, HOLogic.imp $ eqn $ P'))::t1s,
   341                 (frees, HOLogic.imp $ eqn $ P'))::t1s,
   345               (foldr (fn (Free (s, T), t) => HOLogic.mk_exists (s, T, t))
   342               (foldr (fn (Free (s, T), t) => HOLogic.mk_exists (s, T, t))
   346                 (frees, HOLogic.conj $ eqn $ (Not $ P')))::t2s)
   343                 (frees, HOLogic.conj $ eqn $ (HOLogic.Not $ P')))::t2s)
   347           end;
   344           end;
   348 
   345 
   349         val (t1s, t2s) = foldr process_constr (constrs ~~ fs, ([], []));
   346         val (t1s, t2s) = foldr process_constr (constrs ~~ fs, ([], []));
   350         val lhs = P $ (comb_t $ Free ("x", T))
   347         val lhs = P $ (comb_t $ Free ("x", T))
   351       in
   348       in
   352         (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, mk_conj t1s)),
   349         (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, mk_conj t1s)),
   353          HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, Not $ mk_disj t2s)))
   350          HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, HOLogic.Not $ mk_disj t2s)))
   354       end
   351       end
   355 
   352 
   356   in map make_split ((hd descr) ~~ newTs ~~
   353   in map make_split ((hd descr) ~~ newTs ~~
   357     (make_case_combs new_type_names descr sorts thy "f"))
   354     (make_case_combs new_type_names descr sorts thy "f"))
   358   end;
   355   end;