src/ZF/Tools/cartprod.ML
author haftmann
Tue Nov 24 17:28:25 2009 +0100 (2009-11-24)
changeset 33955 fff6f11b1f09
parent 26189 9808cca5c54d
child 33957 e9afca2118d4
permissions -rw-r--r--
curried take/drop
haftmann@24584
     1
(*  Title:      ZF/Tools/cartprod.ML
paulson@6049
     2
    ID:         $Id$
paulson@6049
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@6049
     4
    Copyright   1996  University of Cambridge
paulson@6049
     5
paulson@6049
     6
Signatures for inductive definitions
paulson@6049
     7
paulson@6049
     8
Syntactic operations for Cartesian Products
paulson@6049
     9
*)
paulson@6049
    10
paulson@6049
    11
signature FP =          (** Description of a fixed point operator **)
paulson@6049
    12
  sig
paulson@6049
    13
  val oper      : term                  (*fixed point operator*)
paulson@6049
    14
  val bnd_mono  : term                  (*monotonicity predicate*)
paulson@6049
    15
  val bnd_monoI : thm                   (*intro rule for bnd_mono*)
paulson@6049
    16
  val subs      : thm                   (*subset theorem for fp*)
paulson@6049
    17
  val Tarski    : thm                   (*Tarski's fixed point theorem*)
paulson@6049
    18
  val induct    : thm                   (*induction/coinduction rule*)
paulson@6049
    19
  end;
paulson@6049
    20
paulson@6049
    21
signature SU =                  (** Description of a disjoint sum **)
paulson@6049
    22
  sig
paulson@6049
    23
  val sum       : term                  (*disjoint sum operator*)
paulson@6049
    24
  val inl       : term                  (*left injection*)
paulson@6049
    25
  val inr       : term                  (*right injection*)
paulson@6049
    26
  val elim      : term                  (*case operator*)
paulson@6049
    27
  val case_inl  : thm                   (*inl equality rule for case*)
paulson@6049
    28
  val case_inr  : thm                   (*inr equality rule for case*)
paulson@6049
    29
  val inl_iff   : thm                   (*injectivity of inl, using <->*)
paulson@6049
    30
  val inr_iff   : thm                   (*injectivity of inr, using <->*)
paulson@6049
    31
  val distinct  : thm                   (*distinctness of inl, inr using <->*)
paulson@6049
    32
  val distinct' : thm                   (*distinctness of inr, inl using <->*)
paulson@6049
    33
  val free_SEs  : thm list              (*elim rules for SU, and pair_iff!*)
paulson@6049
    34
  end;
paulson@6049
    35
paulson@6049
    36
signature PR =                  (** Description of a Cartesian product **)
paulson@6049
    37
  sig
paulson@6049
    38
  val sigma     : term                  (*Cartesian product operator*)
paulson@6049
    39
  val pair      : term                  (*pairing operator*)
paulson@6049
    40
  val split_name : string               (*name of polymorphic split*)
paulson@6049
    41
  val pair_iff  : thm                   (*injectivity of pairing, using <->*)
paulson@6049
    42
  val split_eq  : thm                   (*equality rule for split*)
paulson@6049
    43
  val fsplitI   : thm                   (*intro rule for fsplit*)
paulson@6049
    44
  val fsplitD   : thm                   (*destruct rule for fsplit*)
paulson@6049
    45
  val fsplitE   : thm                   (*elim rule; apparently never used*)
paulson@6049
    46
  end;
paulson@6049
    47
paulson@6049
    48
signature CARTPROD =            (** Derived syntactic functions for produts **)
paulson@6049
    49
  sig
paulson@6049
    50
  val ap_split : typ -> typ -> term -> term
paulson@6049
    51
  val factors : typ -> typ list
paulson@6049
    52
  val mk_prod : typ * typ -> typ
paulson@6049
    53
  val mk_tuple : term -> typ -> term list -> term
paulson@6049
    54
  val pseudo_type : term -> typ
paulson@6049
    55
  val remove_split : thm -> thm
paulson@6049
    56
  val split_const : typ -> term
paulson@6049
    57
  val split_rule_var : term * typ * thm -> thm
paulson@6049
    58
  end;
paulson@6049
    59
paulson@6049
    60
paulson@6049
    61
functor CartProd_Fun (Pr: PR) : CARTPROD =
paulson@6049
    62
struct
paulson@6049
    63
wenzelm@15674
    64
(* Some of these functions expect "pseudo-types" containing products,
paulson@6049
    65
   as in HOL; the true ZF types would just be "i" *)
paulson@6049
    66
paulson@6049
    67
fun mk_prod (T1,T2) = Type("*", [T1,T2]);
paulson@6049
    68
paulson@6049
    69
(*Bogus product type underlying a (possibly nested) Sigma.  
paulson@6049
    70
  Lets us share HOL code*)
paulson@6049
    71
fun pseudo_type (t $ A $ Abs(_,_,B)) = 
wenzelm@26189
    72
      if t = Pr.sigma
wenzelm@26189
    73
      then mk_prod(pseudo_type A, pseudo_type B)
wenzelm@26189
    74
      else @{typ i}
wenzelm@26189
    75
  | pseudo_type _ = @{typ i};
paulson@6049
    76
paulson@6049
    77
(*Maps the type T1*...*Tn to [T1,...,Tn], however nested*)
wenzelm@26189
    78
fun factors (Type("*", [T1, T2])) = factors T1 @ factors T2
wenzelm@26189
    79
  | factors T                     = [T];
paulson@6049
    80
paulson@6049
    81
(*Make a well-typed instance of "split"*)
paulson@6049
    82
fun split_const T = Const(Pr.split_name, 
paulson@6049
    83
                          [[Ind_Syntax.iT, Ind_Syntax.iT]--->T, 
paulson@6049
    84
                           Ind_Syntax.iT] ---> T);
paulson@6049
    85
paulson@6049
    86
(*In ap_split S T u, term u expects separate arguments for the factors of S,
paulson@6049
    87
  with result type T.  The call creates a new term expecting one argument
paulson@6049
    88
  of type S.*)
paulson@6049
    89
fun ap_split (Type("*", [T1,T2])) T3 u   = 
paulson@6049
    90
       split_const T3 $ 
paulson@6049
    91
       Abs("v", Ind_Syntax.iT, (*Not T1, as it involves pseudo-product types*)
paulson@6049
    92
           ap_split T2 T3
paulson@6049
    93
           ((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $ 
paulson@6049
    94
            Bound 0))
paulson@6049
    95
  | ap_split T T3 u = u;
paulson@6049
    96
paulson@6049
    97
(*Makes a nested tuple from a list, following the product type structure*)
paulson@6049
    98
fun mk_tuple pair (Type("*", [T1,T2])) tms = 
paulson@6049
    99
        pair $ (mk_tuple pair T1 tms)
haftmann@33955
   100
             $ (mk_tuple pair T2 ((uncurry drop) (length (factors T1), tms)))
paulson@6049
   101
  | mk_tuple pair T (t::_) = t;
paulson@6049
   102
paulson@6049
   103
(*Attempts to remove occurrences of split, and pair-valued parameters*)
paulson@6049
   104
val remove_split = rewrite_rule [Pr.split_eq];
paulson@6049
   105
paulson@6049
   106
(*Uncurries any Var according to its "pseudo-product type" T1 in the rule*)
paulson@6049
   107
fun split_rule_var (Var(v,_), Type("fun",[T1,T2]), rl) =
paulson@6049
   108
      let val T' = factors T1 ---> T2
paulson@6049
   109
          val newt = ap_split T1 T2 (Var(v,T'))
wenzelm@22596
   110
          val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
paulson@6049
   111
      in
paulson@6049
   112
          remove_split (instantiate ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)), 
paulson@6049
   113
                                           cterm newt)]) rl)
paulson@6049
   114
      end
paulson@6049
   115
  | split_rule_var (t,T,rl) = rl;
paulson@6049
   116
paulson@6049
   117
end;
paulson@6049
   118