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