src/ZF/Induct/Datatypes.thy
author paulson
Tue, 21 May 2002 13:06:36 +0200
changeset 13168 afcbca3498b0
parent 12610 8b9845807f77
child 16417 9bc16273c2d4
permissions -rw-r--r--
converted domrange to Isar and merged with equalities
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12194
diff changeset
     1
(*  Title:      ZF/Induct/Datatypes.thy
12194
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
     5
*)
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
     6
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
     7
header {* Sample datatype definitions *}
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
     8
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
     9
theory Datatypes = Main:
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    10
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    11
subsection {* A type with four constructors *}
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    12
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    13
text {*
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    14
  It has four contructors, of arities 0--3, and two parameters @{text
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    15
  A} and @{text B}.
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    16
*}
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    17
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    18
consts
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    19
  data :: "[i, i] => i"
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    20
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    21
datatype "data(A, B)" =
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    22
    Con0
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    23
  | Con1 ("a \<in> A")
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    24
  | Con2 ("a \<in> A", "b \<in> B")
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    25
  | Con3 ("a \<in> A", "b \<in> B", "d \<in> data(A, B)")
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    26
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    27
lemma data_unfold: "data(A, B) = ({0} + A) + (A \<times> B + A \<times> B \<times> data(A, B))"
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    28
  by (fast intro!: data.intros [unfolded data.con_defs]
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    29
    elim: data.cases [unfolded data.con_defs])
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    30
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    31
text {*
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    32
  \medskip Lemmas to justify using @{term data} in other recursive
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    33
  type definitions.
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    34
*}
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    35
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    36
lemma data_mono: "[| A \<subseteq> C; B \<subseteq> D |] ==> data(A, B) \<subseteq> data(C, D)"
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    37
  apply (unfold data.defs)
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    38
  apply (rule lfp_mono)
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    39
   apply (rule data.bnd_mono)+
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    40
  apply (rule univ_mono Un_mono basic_monos | assumption)+
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    41
  done
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    42
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    43
lemma data_univ: "data(univ(A), univ(A)) \<subseteq> univ(A)"
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    44
  apply (unfold data.defs data.con_defs)
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    45
  apply (rule lfp_lowerbound)
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    46
   apply (rule_tac [2] subset_trans [OF A_subset_univ Un_upper1, THEN univ_mono])
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    47
  apply (fast intro!: zero_in_univ Inl_in_univ Inr_in_univ Pair_in_univ)
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    48
  done
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    49
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    50
lemma data_subset_univ:
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    51
    "[| A \<subseteq> univ(C); B \<subseteq> univ(C) |] ==> data(A, B) \<subseteq> univ(C)"
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    52
  by (rule subset_trans [OF data_mono data_univ])
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    53
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    54
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    55
subsection {* Example of a big enumeration type *}
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    56
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    57
text {*
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    58
  Can go up to at least 100 constructors, but it takes nearly 7
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    59
  minutes \dots\ (back in 1994 that is).
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    60
*}
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    61
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    62
consts
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    63
  enum :: i
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    64
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    65
datatype enum =
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    66
    C00 | C01 | C02 | C03 | C04 | C05 | C06 | C07 | C08 | C09
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    67
  | C10 | C11 | C12 | C13 | C14 | C15 | C16 | C17 | C18 | C19
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    68
  | C20 | C21 | C22 | C23 | C24 | C25 | C26 | C27 | C28 | C29
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    69
  | C30 | C31 | C32 | C33 | C34 | C35 | C36 | C37 | C38 | C39
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    70
  | C40 | C41 | C42 | C43 | C44 | C45 | C46 | C47 | C48 | C49
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    71
  | C50 | C51 | C52 | C53 | C54 | C55 | C56 | C57 | C58 | C59
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    72
13909cb72129 converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff changeset
    73
end