src/ZF/QUniv.thy
author paulson
Wed Jan 13 11:57:09 1999 +0100 (1999-01-13)
changeset 6112 5e4871c5136b
parent 6093 87bf8c03b169
child 13220 62c899c77151
permissions -rw-r--r--
datatype package improvements
wenzelm@6093
     1
(*  Title:      ZF/QUniv.thy
clasohm@0
     2
    ID:         $Id$
clasohm@1478
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
wenzelm@6093
     6
A small universe for lazy recursive types.
clasohm@0
     7
*)
clasohm@0
     8
paulson@2469
     9
QUniv = Univ + QPair + mono + equalities +
wenzelm@3923
    10
paulson@6112
    11
(*Disjoint sums as a datatype*)
paulson@6112
    12
rep_datatype 
paulson@6112
    13
  elim		sumE
paulson@6112
    14
  induct	TrueI
paulson@6112
    15
  case_eqns	case_Inl, case_Inr
paulson@6112
    16
paulson@6112
    17
(*Variant disjoint sums as a datatype*)
paulson@6112
    18
rep_datatype 
paulson@6112
    19
  elim		qsumE
paulson@6112
    20
  induct	TrueI
paulson@6112
    21
  case_eqns	qcase_QInl, qcase_QInr
paulson@6112
    22
wenzelm@6093
    23
constdefs
wenzelm@6093
    24
  quniv :: i => i
paulson@6112
    25
   "quniv(A) == Pow(univ(eclose(A)))"
clasohm@0
    26
clasohm@0
    27
end