src/ZF/constructor.ML
author clasohm
Fri Jul 01 11:03:42 1994 +0200 (1994-07-01 ago)
changeset 444 3ca9d49fd662
parent 231 cb6a24451544
child 448 d7ff85d292c7
permissions -rw-r--r--
replaced extend_theory by new add_* functions;
changed syntax of datatype declaration
     1 (*  Title: 	ZF/constructor.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Constructor function module -- for Datatype Definitions
     7 
     8 Defines constructors and a case-style eliminator (no primitive recursion)
     9 
    10 Features:
    11 * least or greatest fixedpoints
    12 * user-specified product and sum constructions
    13 * mutually recursive datatypes
    14 * recursion over arbitrary monotone operators
    15 * flexible: can derive any reasonable set of introduction rules
    16 * automatically constructs a case analysis operator (but no recursion op)
    17 * efficient treatment of large declarations (e.g. 60 constructors)
    18 *)
    19 
    20 (** STILL NEEDS: some treatment of recursion **)
    21 
    22 signature CONSTRUCTOR =
    23   sig
    24   val thy        : theory		(*parent theory*)
    25   val rec_specs  : (string * string * (string list * string * mixfix)list) list
    26                       (*recursion ops, types, domains, constructors*)
    27   val rec_styp	 : string		(*common type of all recursion ops*)
    28   val sintrs     : string list		(*desired introduction rules*)
    29   val monos      : thm list		(*monotonicity of each M operator*)
    30   val type_intrs : thm list		(*type-checking intro rules*)
    31   val type_elims : thm list		(*type-checking elim rules*)
    32   end;
    33 
    34 signature CONSTRUCTOR_RESULT =
    35   sig
    36   val con_thy	 : theory		(*theory defining the constructors*)
    37   val con_defs	 : thm list		(*definitions made in con_thy*)
    38   val case_eqns  : thm list		(*equations for case operator*)
    39   val free_iffs  : thm list		(*freeness rewrite rules*)
    40   val free_SEs   : thm list		(*freeness destruct rules*)
    41   val mk_free    : string -> thm	(*makes freeness theorems*)
    42   end;
    43 
    44 
    45 functor Constructor_Fun (structure Const: CONSTRUCTOR and
    46                       Pr : PR and Su : SU) : CONSTRUCTOR_RESULT =
    47 struct
    48 open Logic Const;
    49 
    50 val dummy = writeln"Defining the constructor functions...";
    51 
    52 val case_name = "f";		(*name for case variables*)
    53 
    54 (** Extract basic information from arguments **)
    55 
    56 val sign = sign_of thy;
    57 val rdty = typ_of o read_ctyp sign;
    58 
    59 val rec_names = map #1 rec_specs;
    60 
    61 val dummy = assert_all Syntax.is_identifier rec_names
    62    (fn a => "Name of recursive set not an identifier: " ^ a);
    63 
    64 (*Expands multiple constant declarations*)
    65 fun flatten_consts ((names, typ, mfix) :: cs) =
    66       let fun mk_const name = (name, typ, mfix)
    67       in (map mk_const names) @ (flatten_consts cs) end
    68   | flatten_consts [] = [];
    69 
    70 (*Constructors with types and arguments*)
    71 fun mk_con_ty_list cons_pairs = 
    72   let fun mk_con_ty (a, st, syn) =
    73 	  let val T = rdty st;
    74 	      val args = mk_frees "xa" (binder_types T);
    75               val name = const_name a syn; (* adds "op" to infix constructors*)
    76 	  in (name, T, args) end;
    77 
    78       fun pairtypes c = flatten_consts [c];
    79   in map mk_con_ty (flat (map pairtypes cons_pairs))  end;
    80 
    81 val con_ty_lists = map (mk_con_ty_list o #3) rec_specs;
    82 
    83 (** Define the constructors **)
    84 
    85 (*We identify 0 (the empty set) with the empty tuple*)
    86 fun mk_tuple [] = Const("0",iT)
    87   | mk_tuple args = foldr1 (app Pr.pair) args;
    88 
    89 fun mk_inject n k u = access_bal(ap Su.inl, ap Su.inr, u) n k;
    90 
    91 val npart = length rec_names;		(*number of mutually recursive parts*)
    92 
    93 (*Make constructor definition*)
    94 fun mk_con_defs (kpart, con_ty_list) = 
    95   let val ncon = length con_ty_list	   (*number of constructors*)
    96       fun mk_def ((a,T,args), kcon) = (*kcon = index of this constructor*)
    97 	  mk_defpair sign 
    98 	     (list_comb (Const(a,T), args),
    99 	      mk_inject npart kpart (mk_inject ncon kcon (mk_tuple args)))
   100   in  map mk_def (con_ty_list ~~ (1 upto ncon))  end;
   101 
   102 (** Define the case operator **)
   103 
   104 (*Combine split terms using case; yields the case operator for one part*)
   105 fun call_case case_list = 
   106   let fun call_f (free,args) = 
   107           ap_split Pr.split_const free (map (#2 o dest_Free) args)
   108   in  fold_bal (app Su.elim) (map call_f case_list)  end;
   109 
   110 (** Generating function variables for the case definition
   111     Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
   112 
   113 (*Treatment of a single constructor*)
   114 fun add_case ((a,T,args), (opno,cases)) =
   115     if Syntax.is_identifier a
   116     then (opno,   
   117 	  (Free(case_name ^ "_" ^ a, T), args) :: cases)
   118     else (opno+1, 
   119 	  (Free(case_name ^ "_op_" ^ string_of_int opno, T), args) :: cases);
   120 
   121 (*Treatment of a list of constructors, for one part*)
   122 fun add_case_list (con_ty_list, (opno,case_lists)) =
   123     let val (opno',case_list) = foldr add_case (con_ty_list, (opno,[]))
   124     in (opno', case_list :: case_lists) end;
   125 
   126 (*Treatment of all parts*)
   127 val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[]));
   128 
   129 val big_case_typ = flat (map (map #2) con_ty_lists) ---> (iT-->iT);
   130 
   131 val big_rec_name = space_implode "_" rec_names;
   132 
   133 val big_case_name = big_rec_name ^ "_case";
   134 
   135 (*The list of all the function variables*)
   136 val big_case_args = flat (map (map #1) case_lists);
   137 
   138 val big_case_tm = 
   139     list_comb (Const(big_case_name, big_case_typ), big_case_args); 
   140 
   141 val big_case_def = 
   142   mk_defpair sign 
   143     (big_case_tm, fold_bal (app Su.elim) (map call_case case_lists)); 
   144 
   145 (** Build the new theory **)
   146 
   147 val axpairs =
   148     big_case_def :: flat (map mk_con_defs ((1 upto npart) ~~ con_ty_lists));
   149 
   150 val const_decs = flatten_consts
   151 		   (([big_case_name], flatten_typ sign big_case_typ, NoSyn) ::
   152 		    (big_rec_name ins rec_names, rec_styp, NoSyn) ::
   153 		    flat (map #3 rec_specs));
   154 
   155 val con_thy = thy
   156               |> add_consts const_decs
   157               |> add_axioms axpairs
   158               |> add_thyname (big_rec_name ^ "_Constructors");
   159 
   160 (*1st element is the case definition; others are the constructors*)
   161 val con_defs = map (get_axiom con_thy o #1) axpairs;
   162 
   163 (** Prove the case theorem **)
   164 
   165 (*Each equation has the form 
   166   rec_case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *)
   167 fun mk_case_equation ((a,T,args), case_free) = 
   168   mk_tprop 
   169    (eq_const $ (big_case_tm $ (list_comb (Const(a,T), args)))
   170 	     $ (list_comb (case_free, args)));
   171 
   172 val case_trans = hd con_defs RS def_trans;
   173 
   174 (*proves a single case equation*)
   175 fun case_tacsf con_def _ = 
   176   [rewtac con_def,
   177    rtac case_trans 1,
   178    REPEAT (resolve_tac [refl, Pr.split_eq RS trans, 
   179 			Su.case_inl RS trans, 
   180 			Su.case_inr RS trans] 1)];
   181 
   182 fun prove_case_equation (arg,con_def) =
   183     prove_term (sign_of con_thy) [] 
   184         (mk_case_equation arg, case_tacsf con_def);
   185 
   186 val free_iffs = 
   187     map standard (con_defs RL [def_swap_iff]) @
   188     [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff];
   189 
   190 val free_SEs   = map (gen_make_elim [conjE,FalseE]) (free_iffs RL [iffD1]);
   191 
   192 val free_cs = ZF_cs addSEs free_SEs;
   193 
   194 (*Typical theorems have the form ~con1=con2, con1=con2==>False,
   195   con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc.  *)
   196 fun mk_free s =
   197     prove_goalw con_thy con_defs s
   198       (fn prems => [cut_facts_tac prems 1, fast_tac free_cs 1]);
   199 
   200 val case_eqns = map prove_case_equation 
   201 		    (flat con_ty_lists ~~ big_case_args ~~ tl con_defs);
   202 
   203 end;
   204 
   205