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