# HG changeset patch # User wenzelm # Date 1005776563 -3600 # Node ID 13909cb72129938f2333fc4f2575f0c0abec0e19 # Parent b269a927c1371f8c98389a522687907d4d3ef415 converted datatype examples moved from ZF/ex to ZF/Induct; diff -r b269a927c137 -r 13909cb72129 src/ZF/Induct/Binary_Trees.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Induct/Binary_Trees.thy Wed Nov 14 23:22:43 2001 +0100 @@ -0,0 +1,120 @@ +(* Title: ZF/Induct/Binary_Trees.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1992 University of Cambridge +*) + +header {* Binary trees *} + +theory Binary_Trees = Main: + +subsection {* Datatype definition *} + +consts + bt :: "i => i" + +datatype "bt(A)" = + Lf | Br ("a \ A", "t1 \ bt(A)", "t2 \ bt(A)") + +declare bt.intros [simp] + +lemma Br_neq_left: "l \ bt(A) ==> (!!x r. Br(x, l, r) \ l)" + by (induct set: bt) auto + +lemma Br_iff: "Br(a, l, r) = Br(a', l', r') <-> a = a' & l = l' & r = r'" + -- "Proving a freeness theorem." + by (fast elim!: bt.free_elims) + +inductive_cases BrE: "Br(a, l, r) \ bt(A)" + -- "An elimination rule, for type-checking." + +text {* + \medskip Lemmas to justify using @{term bt} in other recursive type + definitions. +*} + +lemma bt_mono: "A \ B ==> bt(A) \ bt(B)" + apply (unfold bt.defs) + apply (rule lfp_mono) + apply (rule bt.bnd_mono)+ + apply (rule univ_mono basic_monos | assumption)+ + done + +lemma bt_univ: "bt(univ(A)) \ univ(A)" + apply (unfold bt.defs bt.con_defs) + apply (rule lfp_lowerbound) + apply (rule_tac [2] A_subset_univ [THEN univ_mono]) + apply (fast intro!: zero_in_univ Inl_in_univ Inr_in_univ Pair_in_univ) + done + +lemma bt_subset_univ: "A \ univ(B) ==> bt(A) \ univ(B)" + apply (rule subset_trans) + apply (erule bt_mono) + apply (rule bt_univ) + done + +lemma bt_rec_type: + "[| t \ bt(A); + c \ C(Lf); + !!x y z r s. [| x \ A; y \ bt(A); z \ bt(A); r \ C(y); s \ C(z) |] ==> + h(x, y, z, r, s) \ C(Br(x, y, z)) + |] ==> bt_rec(c, h, t) \ C(t)" + -- {* Type checking for recursor -- example only; not really needed. *} + apply (induct_tac t) + apply simp_all + done + + +subsection {* Number of nodes *} + +consts + n_nodes :: "i => i" +primrec + "n_nodes(Lf) = 0" + "n_nodes(Br(a, l, r)) = succ(n_nodes(l) #+ n_nodes(r))" + +lemma n_nodes_type [simp]: "t \ bt(A) ==> n_nodes(t) \ nat" + by (induct_tac t) auto + + +subsection {* Number of leaves *} + +consts + n_leaves :: "i => i" +primrec + "n_leaves(Lf) = 1" + "n_leaves(Br(a, l, r)) = n_leaves(l) #+ n_leaves(r)" + +lemma n_leaves_type [simp]: "t \ bt(A) ==> n_leaves(t) \ nat" + by (induct_tac t) auto + + +subsection {* Reflecting trees *} + +consts + bt_reflect :: "i => i" +primrec + "bt_reflect(Lf) = Lf" + "bt_reflect(Br(a, l, r)) = Br(a, bt_reflect(r), bt_reflect(l))" + +lemma bt_reflect_type [simp]: "t \ bt(A) ==> bt_reflect(t) \ bt(A)" + by (induct_tac t) auto + +text {* + \medskip Theorems about @{term n_leaves}. +*} + +lemma n_leaves_reflect: "t \ bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)" + by (induct_tac t) (simp_all add: add_commute n_leaves_type) + +lemma n_leaves_nodes: "t \ bt(A) ==> n_leaves(t) = succ(n_nodes(t))" + by (induct_tac t) (simp_all add: add_succ_right) + +text {* + Theorems about @{term bt_reflect}. +*} + +lemma bt_reflect_bt_reflect_ident: "t \ bt(A) ==> bt_reflect(bt_reflect(t)) = t" + by (induct_tac t) simp_all + +end diff -r b269a927c137 -r 13909cb72129 src/ZF/Induct/Datatypes.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Induct/Datatypes.thy Wed Nov 14 23:22:43 2001 +0100 @@ -0,0 +1,73 @@ +(* Title: ZF/ex/Datatypes.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge +*) + +header {* Sample datatype definitions *} + +theory Datatypes = Main: + +subsection {* A type with four constructors *} + +text {* + It has four contructors, of arities 0--3, and two parameters @{text + A} and @{text B}. +*} + +consts + data :: "[i, i] => i" + +datatype "data(A, B)" = + Con0 + | Con1 ("a \ A") + | Con2 ("a \ A", "b \ B") + | Con3 ("a \ A", "b \ B", "d \ data(A, B)") + +lemma data_unfold: "data(A, B) = ({0} + A) + (A \ B + A \ B \ data(A, B))" + by (fast intro!: data.intros [unfolded data.con_defs] + elim: data.cases [unfolded data.con_defs]) + +text {* + \medskip Lemmas to justify using @{term data} in other recursive + type definitions. +*} + +lemma data_mono: "[| A \ C; B \ D |] ==> data(A, B) \ data(C, D)" + apply (unfold data.defs) + apply (rule lfp_mono) + apply (rule data.bnd_mono)+ + apply (rule univ_mono Un_mono basic_monos | assumption)+ + done + +lemma data_univ: "data(univ(A), univ(A)) \ univ(A)" + apply (unfold data.defs data.con_defs) + apply (rule lfp_lowerbound) + apply (rule_tac [2] subset_trans [OF A_subset_univ Un_upper1, THEN univ_mono]) + apply (fast intro!: zero_in_univ Inl_in_univ Inr_in_univ Pair_in_univ) + done + +lemma data_subset_univ: + "[| A \ univ(C); B \ univ(C) |] ==> data(A, B) \ univ(C)" + by (rule subset_trans [OF data_mono data_univ]) + + +subsection {* Example of a big enumeration type *} + +text {* + Can go up to at least 100 constructors, but it takes nearly 7 + minutes \dots\ (back in 1994 that is). +*} + +consts + enum :: i + +datatype enum = + C00 | C01 | C02 | C03 | C04 | C05 | C06 | C07 | C08 | C09 + | C10 | C11 | C12 | C13 | C14 | C15 | C16 | C17 | C18 | C19 + | C20 | C21 | C22 | C23 | C24 | C25 | C26 | C27 | C28 | C29 + | C30 | C31 | C32 | C33 | C34 | C35 | C36 | C37 | C38 | C39 + | C40 | C41 | C42 | C43 | C44 | C45 | C46 | C47 | C48 | C49 + | C50 | C51 | C52 | C53 | C54 | C55 | C56 | C57 | C58 | C59 + +end diff -r b269a927c137 -r 13909cb72129 src/ZF/ex/BT.ML --- a/src/ZF/ex/BT.ML Wed Nov 14 23:22:15 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,100 +0,0 @@ -(* Title: ZF/ex/BT.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1994 University of Cambridge - -Datatype definition of binary trees -*) - -Addsimps bt.intrs; - -Goal "l \\ bt(A) ==> \\x r. Br(x,l,r) \\ l"; -by (induct_tac "l" 1); -by Auto_tac; -qed_spec_mp "Br_neq_left"; - -(*Proving a freeness theorem*) -val Br_iff = bt.mk_free "Br(a,l,r) = Br(a',l',r') <-> a=a' & l=l' & r=r'"; - -(*An elimination rule, for type-checking*) -val BrE = bt.mk_cases "Br(a,l,r) \\ bt(A)"; - -(** Lemmas to justify using "bt" in other recursive type definitions **) - -Goalw bt.defs "A \\ B ==> bt(A) \\ bt(B)"; -by (rtac lfp_mono 1); -by (REPEAT (rtac bt.bnd_mono 1)); -by (REPEAT (ares_tac (univ_mono::basic_monos) 1)); -qed "bt_mono"; - -Goalw (bt.defs@bt.con_defs) "bt(univ(A)) \\ univ(A)"; -by (rtac lfp_lowerbound 1); -by (rtac (A_subset_univ RS univ_mono) 2); -by (fast_tac (claset() addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ, - Pair_in_univ]) 1); -qed "bt_univ"; - -bind_thm ("bt_subset_univ", [bt_mono, bt_univ] MRS subset_trans); - - -(*Type checking for recursor -- example only; not really needed*) -val major::prems = goal BT.thy - "[| t \\ bt(A); \ -\ c \\ C(Lf); \ -\ !!x y z r s. [| x \\ A; y \\ bt(A); z \\ bt(A); r \\ C(y); s \\ C(z) |] ==> \ -\ h(x,y,z,r,s): C(Br(x,y,z)) \ -\ |] ==> bt_rec(c,h,t) \\ C(t)"; - (*instead of induct_tac "t", since t \\ bt(A) isn't an assumption*) -by (rtac (major RS bt.induct) 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); -qed "bt_rec_type"; - -(** n_nodes **) - -Goal "t \\ bt(A) ==> n_nodes(t) \\ nat"; -by (induct_tac "t" 1); -by Auto_tac; -qed "n_nodes_type"; - - -(** n_leaves **) - -Goal "t \\ bt(A) ==> n_leaves(t) \\ nat"; -by (induct_tac "t" 1); -by Auto_tac; -qed "n_leaves_type"; - -(** bt_reflect **) - -Goal "t \\ bt(A) ==> bt_reflect(t) \\ bt(A)"; -by (induct_tac "t" 1); -by Auto_tac; -qed "bt_reflect_type"; - - -(** BT simplification **) - - -Addsimps [n_nodes_type, n_leaves_type, bt_reflect_type]; - - -(*** theorems about n_leaves ***) - -Goal "t \\ bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)"; -by (induct_tac "t" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_commute, n_leaves_type]))); -qed "n_leaves_reflect"; - -Goal "t \\ bt(A) ==> n_leaves(t) = succ(n_nodes(t))"; -by (induct_tac "t" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_succ_right]))); -qed "n_leaves_nodes"; - -(*** theorems about bt_reflect ***) - -Goal "t \\ bt(A) ==> bt_reflect(bt_reflect(t))=t"; -by (induct_tac "t" 1); -by (ALLGOALS Asm_simp_tac); -qed "bt_reflect_bt_reflect_ident"; - - diff -r b269a927c137 -r 13909cb72129 src/ZF/ex/BT.thy --- a/src/ZF/ex/BT.thy Wed Nov 14 23:22:15 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,33 +0,0 @@ -(* Title: ZF/ex/BT.thy - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1992 University of Cambridge - -Binary trees -*) - -BT = Main + -consts - bt :: i=>i - -datatype - "bt(A)" = Lf | Br ("a \\ A", "t1: bt(A)", "t2: bt(A)") - -consts - n_nodes :: i=>i - n_leaves :: i=>i - bt_reflect :: i=>i - -primrec - "n_nodes(Lf) = 0" - "n_nodes(Br(a,l,r)) = succ(n_nodes(l) #+ n_nodes(r))" - -primrec - "n_leaves(Lf) = 1" - "n_leaves(Br(a,l,r)) = n_leaves(l) #+ n_leaves(r)" - -primrec - "bt_reflect(Lf) = Lf" - "bt_reflect(Br(a,l,r)) = Br(a, bt_reflect(r), bt_reflect(l))" - -end diff -r b269a927c137 -r 13909cb72129 src/ZF/ex/Data.ML --- a/src/ZF/ex/Data.ML Wed Nov 14 23:22:15 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,35 +0,0 @@ -(* Title: ZF/ex/Data.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -Sample datatype definition. -It has four contructors, of arities 0-3, and two parameters A and B. -*) - -open Data; - -Goal "data(A,B) = ({0} + A) + (A*B + A*B*data(A,B))"; -let open data; val rew = rewrite_rule con_defs in -by (fast_tac (claset() addSIs (map rew intrs) addEs [rew elim]) 1) -end; -qed "data_unfold"; - -(** Lemmas to justify using "data" in other recursive type definitions **) - -Goalw data.defs "[| A \\ C; B \\ D |] ==> data(A,B) \\ data(C,D)"; -by (rtac lfp_mono 1); -by (REPEAT (rtac data.bnd_mono 1)); -by (REPEAT (ares_tac (univ_mono::Un_mono::basic_monos) 1)); -qed "data_mono"; - -Goalw (data.defs@data.con_defs) "data(univ(A),univ(A)) \\ univ(A)"; -by (rtac lfp_lowerbound 1); -by (rtac ([A_subset_univ, Un_upper1] MRS subset_trans RS univ_mono) 2); -by (fast_tac (claset() addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ, - Pair_in_univ]) 1); -qed "data_univ"; - -bind_thm ("data_subset_univ", ([data_mono, data_univ] MRS subset_trans)); - - diff -r b269a927c137 -r 13909cb72129 src/ZF/ex/Data.thy --- a/src/ZF/ex/Data.thy Wed Nov 14 23:22:15 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,21 +0,0 @@ -(* Title: ZF/ex/Data.thy - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1994 University of Cambridge - -Sample datatype definition. -It has four contructors, of arities 0-3, and two parameters A and B. -*) - -Data = Main + - -consts - data :: [i,i] => i - -datatype - "data(A,B)" = Con0 - | Con1 ("a \\ A") - | Con2 ("a \\ A", "b \\ B") - | Con3 ("a \\ A", "b \\ B", "d \\ data(A,B)") - -end diff -r b269a927c137 -r 13909cb72129 src/ZF/ex/Enum.ML --- a/src/ZF/ex/Enum.ML Wed Nov 14 23:22:15 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,14 +0,0 @@ -(* Title: ZF/ex/Enum - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -Example of a BIG enumeration type - -Can go up to at least 100 constructors, but it takes nearly 7 minutes... -*) - -Goal "C00 \\ C01"; -by (Simp_tac 1); -result(); - diff -r b269a927c137 -r 13909cb72129 src/ZF/ex/Enum.thy --- a/src/ZF/ex/Enum.thy Wed Nov 14 23:22:15 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,24 +0,0 @@ -(* Title: ZF/ex/Enum - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -Example of a BIG enumeration type - -Can go up to at least 100 constructors, but it takes nearly 7 minutes... -*) - -Enum = Main + - -consts - enum :: i - -datatype - "enum" = C00 | C01 | C02 | C03 | C04 | C05 | C06 | C07 | C08 | C09 - | C10 | C11 | C12 | C13 | C14 | C15 | C16 | C17 | C18 | C19 - | C20 | C21 | C22 | C23 | C24 | C25 | C26 | C27 | C28 | C29 - | C30 | C31 | C32 | C33 | C34 | C35 | C36 | C37 | C38 | C39 - | C40 | C41 | C42 | C43 | C44 | C45 | C46 | C47 | C48 | C49 - | C50 | C51 | C52 | C53 | C54 | C55 | C56 | C57 | C58 | C59 - -end