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