src/ZF/QUniv.thy
author paulson
Tue Jun 18 18:45:07 2002 +0200 (2002-06-18)
changeset 13220 62c899c77151
parent 6112 5e4871c5136b
child 13285 28d1823ce0f2
permissions -rw-r--r--
tidying
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
paulson@13220
    24
  quniv :: "i => i"
paulson@6112
    25
   "quniv(A) == Pow(univ(eclose(A)))"
clasohm@0
    26
clasohm@0
    27
end