add_ind_def.ML
author nipkow
Fri, 02 Dec 1994 11:43:20 +0100
changeset 194 b93cc55cb7ab
parent 187 fcf8024c920d
permissions -rw-r--r--
small updates because datatype list is now used. In particular Nil -> []
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
128
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
     1
(*  Title: 	HOL/add_ind_def.ML
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
     2
    ID:         $Id$
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
     5
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
     6
Fixedpoint definition module -- for Inductive/Coinductive Definitions
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
     7
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
     8
Features:
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
     9
* least or greatest fixedpoints
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    10
* user-specified product and sum constructions
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    11
* mutually recursive definitions
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    12
* definitions involving arbitrary monotone operators
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    13
* automatically proves introduction and elimination rules
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    14
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    15
The recursive sets must *already* be declared as constants in parent theory!
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    16
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    17
  Introduction rules have the form
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    18
  [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk |]
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    19
  where M is some monotone operator (usually the identity)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    20
  P(x) is any (non-conjunctive) side condition on the free variables
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    21
  ti, t are any terms
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    22
  Sj, Sk are two of the sets being defined in mutual recursion
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    23
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    24
Sums are used only for mutual recursion;
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    25
Products are used only to derive "streamlined" induction rules for relations
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    26
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    27
Nestings of disjoint sum types:
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    28
   (a+(b+c)) for 3,  ((a+b)+(c+d)) for 4,  ((a+b)+(c+(d+e))) for 5,
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    29
   ((a+(b+c))+(d+(e+f))) for 6
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    30
*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    31
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    32
signature FP =		(** Description of a fixed point operator **)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    33
  sig
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    34
  val oper	: string * typ * term -> term	(*fixed point operator*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    35
  val Tarski	: thm			(*Tarski's fixed point theorem*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    36
  val induct	: thm			(*induction/coinduction rule*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    37
  end;
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    38
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    39
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    40
signature ADD_INDUCTIVE_DEF =
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    41
  sig 
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    42
  val add_fp_def_i : term list * term list -> theory -> theory
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    43
  end;
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    44
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    45
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    46
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    47
(*Declares functions to add fixedpoint/constructor defs to a theory*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    48
functor Add_inductive_def_Fun (Fp: FP) : ADD_INDUCTIVE_DEF =
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    49
struct
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    50
open Logic Ind_Syntax;
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    51
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    52
(*internal version*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    53
fun add_fp_def_i (rec_tms, intr_tms) thy = 
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    54
  let
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    55
    val sign = sign_of thy;
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    56
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    57
    (*recT and rec_params should agree for all mutually recursive components*)
181
3f5136a61a72 checks that the recursive sets are Consts before taking
lcp
parents: 142
diff changeset
    58
    val rec_hds = map head_of rec_tms;
128
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    59
181
3f5136a61a72 checks that the recursive sets are Consts before taking
lcp
parents: 142
diff changeset
    60
    val _ = assert_all is_Const rec_hds
3f5136a61a72 checks that the recursive sets are Consts before taking
lcp
parents: 142
diff changeset
    61
	    (fn t => "Recursive set not previously declared as constant: " ^ 
3f5136a61a72 checks that the recursive sets are Consts before taking
lcp
parents: 142
diff changeset
    62
	             Sign.string_of_term sign t);
128
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    63
181
3f5136a61a72 checks that the recursive sets are Consts before taking
lcp
parents: 142
diff changeset
    64
    (*Now we know they are all Consts, so get their names, type and params*)
3f5136a61a72 checks that the recursive sets are Consts before taking
lcp
parents: 142
diff changeset
    65
    val rec_names = map (#1 o dest_Const) rec_hds
3f5136a61a72 checks that the recursive sets are Consts before taking
lcp
parents: 142
diff changeset
    66
    and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
128
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    67
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    68
    val _ = assert_all Syntax.is_identifier rec_names
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    69
       (fn a => "Name of recursive set not an identifier: " ^ a);
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    70
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    71
    local (*Checking the introduction rules*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    72
      val intr_sets = map (#2 o rule_concl_msg sign) intr_tms;
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    73
      fun intr_ok set =
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    74
	  case head_of set of Const(a,_) => a mem rec_names | _ => false;
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    75
    in
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    76
      val _ =  assert_all intr_ok intr_sets
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    77
	 (fn t => "Conclusion of rule does not name a recursive set: " ^ 
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    78
		  Sign.string_of_term sign t);
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    79
    end;
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    80
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    81
    val _ = assert_all is_Free rec_params
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    82
	(fn t => "Param in recursion term not a free variable: " ^
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    83
		 Sign.string_of_term sign t);
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    84
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    85
    (*** Construct the lfp definition ***)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    86
    val mk_variant = variant (foldr add_term_names (intr_tms,[]));
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    87
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    88
    val z = mk_variant"z" and X = mk_variant"X" and w = mk_variant"w";
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    89
181
3f5136a61a72 checks that the recursive sets are Consts before taking
lcp
parents: 142
diff changeset
    90
    (*Probably INCORRECT for mutual recursion!*)
187
fcf8024c920d minor changes according to new hologic;
wenzelm
parents: 181
diff changeset
    91
    val domTs = summands(dest_setT (body_type recT));
128
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    92
    val dom_sumT = fold_bal mk_sum domTs;
187
fcf8024c920d minor changes according to new hologic;
wenzelm
parents: 181
diff changeset
    93
    val dom_set   = mk_setT dom_sumT;
128
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    94
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    95
    val freez   = Free(z, dom_sumT)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    96
    and freeX   = Free(X, dom_set);
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    97
    (*type of w may be any of the domTs*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    98
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
    99
    fun dest_tprop (Const("Trueprop",_) $ P) = P
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   100
      | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^ 
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   101
			      Sign.string_of_term sign Q);
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   102
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   103
    (*Makes a disjunct from an introduction rule*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   104
    fun lfp_part intr = (*quantify over rule's free vars except parameters*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   105
      let val prems = map dest_tprop (strip_imp_prems intr)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   106
	  val _ = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   107
	  val exfrees = term_frees intr \\ rec_params
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   108
	  val zeq = eq_const dom_sumT $ freez $ (#1 (rule_concl intr))
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   109
      in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end;
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   110
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   111
    (*The Part(A,h) terms -- compose injections to make h*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   112
    fun mk_Part (Bound 0, _) = freeX	(*no mutual rec, no Part needed*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   113
      | mk_Part (h, domT)    = 
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   114
	  let val goodh = mend_sum_types (h, dom_sumT)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   115
              and Part_const = 
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   116
		  Const("Part", [dom_set, domT-->dom_sumT]---> dom_set)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   117
          in  Part_const $ freeX $ Abs(w,domT,goodh)  end;
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   118
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   119
    (*Access to balanced disjoint sums via injections*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   120
    val parts = map mk_Part
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   121
	        (accesses_bal (ap Inl, ap Inr, Bound 0) (length domTs) ~~
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   122
		 domTs);
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   123
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   124
    (*replace each set by the corresponding Part(A,h)*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   125
    val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms;
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   126
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   127
    val lfp_rhs = Fp.oper(X, dom_sumT, 
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   128
			  mk_Collect(z, dom_sumT, 
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   129
				     fold_bal (app disj) part_intrs))
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   130
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   131
    val _ = seq (fn rec_hd => deny (rec_hd occs lfp_rhs) 
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   132
			       "Illegal occurrence of recursion operator")
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   133
	     rec_hds;
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   134
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   135
    (*** Make the new theory ***)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   136
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   137
    (*A key definition:
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   138
      If no mutual recursion then it equals the one recursive set.
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   139
      If mutual recursion then it differs from all the recursive sets. *)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   140
    val big_rec_name = space_implode "_" rec_names;
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   141
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   142
    (*Big_rec... is the union of the mutually recursive sets*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   143
    val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   144
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   145
    (*The individual sets must already be declared*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   146
    val axpairs = map mk_defpair 
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   147
	  ((big_rec_tm, lfp_rhs) ::
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   148
	   (case parts of 
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   149
	       [_] => [] 			(*no mutual recursion*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   150
	     | _ => rec_tms ~~		(*define the sets as Parts*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   151
		    map (subst_atomic [(freeX, big_rec_tm)]) parts));
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   152
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   153
    val _ = seq (writeln o Sign.string_of_term sign o #2) axpairs
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   154
  
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   155
  in  thy |> add_defs_i axpairs  end
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   156
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   157
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   158
(****************************************************************OMITTED
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   159
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   160
(*Expects the recursive sets to have been defined already.
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   161
  con_ty_lists specifies the constructors in the form (name,prems,mixfix) *)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   162
fun add_constructs_def (rec_names, con_ty_lists) thy = 
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   163
* let
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   164
*   val _ = writeln"  Defining the constructor functions...";
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   165
*   val case_name = "f";		(*name for case variables*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   166
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   167
*   (** Define the constructors **)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   168
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   169
*   (*The empty tuple is 0*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   170
*   fun mk_tuple [] = Const("0",iT)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   171
*     | mk_tuple args = foldr1 mk_Pair args;
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   172
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   173
*   fun mk_inject n k u = access_bal(ap Inl, ap Inr, u) n k;
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   174
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   175
*   val npart = length rec_names;	(*total # of mutually recursive parts*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   176
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   177
*   (*Make constructor definition; kpart is # of this mutually recursive part*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   178
*   fun mk_con_defs (kpart, con_ty_list) = 
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   179
*     let val ncon = length con_ty_list	   (*number of constructors*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   180
	  fun mk_def (((id,T,syn), name, args, prems), kcon) =
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   181
		(*kcon is index of constructor*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   182
	      mk_defpair (list_comb (Const(name,T), args),
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   183
			  mk_inject npart kpart
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   184
			  (mk_inject ncon kcon (mk_tuple args)))
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   185
*     in  map mk_def (con_ty_list ~~ (1 upto ncon))  end;
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   186
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   187
*   (** Define the case operator **)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   188
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   189
*   (*Combine split terms using case; yields the case operator for one part*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   190
*   fun call_case case_list = 
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   191
*     let fun call_f (free,args) = 
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   192
	      ap_split T free (map (#2 o dest_Free) args)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   193
*     in  fold_bal (app sum_case) (map call_f case_list)  end;
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   194
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   195
*   (** Generating function variables for the case definition
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   196
	Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   197
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   198
*   (*Treatment of a single constructor*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   199
*   fun add_case (((id,T,syn), name, args, prems), (opno,cases)) =
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   200
	if Syntax.is_identifier id
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   201
	then (opno,   
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   202
	      (Free(case_name ^ "_" ^ id, T), args) :: cases)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   203
	else (opno+1, 
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   204
	      (Free(case_name ^ "_op_" ^ string_of_int opno, T), args) :: 
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   205
	      cases)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   206
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   207
*   (*Treatment of a list of constructors, for one part*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   208
*   fun add_case_list (con_ty_list, (opno,case_lists)) =
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   209
	let val (opno',case_list) = foldr add_case (con_ty_list, (opno,[]))
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   210
	in (opno', case_list :: case_lists) end;
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   211
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   212
*   (*Treatment of all parts*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   213
*   val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[]));
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   214
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   215
*   val big_case_typ = flat (map (map (#2 o #1)) con_ty_lists) ---> (iT-->iT);
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   216
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   217
*   val big_rec_name = space_implode "_" rec_names;
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   218
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   219
*   val big_case_name = big_rec_name ^ "_case";
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   220
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   221
*   (*The list of all the function variables*)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   222
*   val big_case_args = flat (map (map #1) case_lists);
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   223
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   224
*   val big_case_tm = 
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   225
	list_comb (Const(big_case_name, big_case_typ), big_case_args); 
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   226
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   227
*   val big_case_def = mk_defpair  
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   228
	(big_case_tm, fold_bal (app sum_case) (map call_case case_lists)); 
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   229
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   230
*   (** Build the new theory **)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   231
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   232
*   val const_decs =
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   233
	(big_case_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists);
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   234
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   235
*   val axpairs =
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   236
	big_case_def :: flat (map mk_con_defs ((1 upto npart) ~~ con_ty_lists))
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   237
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   238
*   in  thy |> add_consts_i const_decs |> add_defs_i axpairs  end;
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   239
****************************************************************)
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   240
end;
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   241
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   242
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   243
89669c58e506 INSTALLATION OF INDUCTIVE DEFINITIONS
lcp
parents:
diff changeset
   244