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