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