--- /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 \<in> A", "t1 \<in> bt(A)", "t2 \<in> bt(A)")
+
+declare bt.intros [simp]
+
+lemma Br_neq_left: "l \<in> bt(A) ==> (!!x r. Br(x, l, r) \<noteq> 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) \<in> 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 \<subseteq> B ==> bt(A) \<subseteq> 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)) \<subseteq> 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 \<subseteq> univ(B) ==> bt(A) \<subseteq> univ(B)"
+ apply (rule subset_trans)
+ apply (erule bt_mono)
+ apply (rule bt_univ)
+ done
+
+lemma bt_rec_type:
+ "[| t \<in> bt(A);
+ c \<in> C(Lf);
+ !!x y z r s. [| x \<in> A; y \<in> bt(A); z \<in> bt(A); r \<in> C(y); s \<in> C(z) |] ==>
+ h(x, y, z, r, s) \<in> C(Br(x, y, z))
+ |] ==> bt_rec(c, h, t) \<in> 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 \<in> bt(A) ==> n_nodes(t) \<in> 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 \<in> bt(A) ==> n_leaves(t) \<in> 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 \<in> bt(A) ==> bt_reflect(t) \<in> bt(A)"
+ by (induct_tac t) auto
+
+text {*
+ \medskip Theorems about @{term n_leaves}.
+*}
+
+lemma n_leaves_reflect: "t \<in> 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 \<in> 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 \<in> bt(A) ==> bt_reflect(bt_reflect(t)) = t"
+ by (induct_tac t) simp_all
+
+end
--- /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 \<in> A")
+ | Con2 ("a \<in> A", "b \<in> B")
+ | Con3 ("a \<in> A", "b \<in> B", "d \<in> data(A, B)")
+
+lemma data_unfold: "data(A, B) = ({0} + A) + (A \<times> B + A \<times> B \<times> 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 \<subseteq> C; B \<subseteq> D |] ==> data(A, B) \<subseteq> 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)) \<subseteq> 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 \<subseteq> univ(C); B \<subseteq> univ(C) |] ==> data(A, B) \<subseteq> 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
--- 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 \\<in> bt(A) ==> \\<forall>x r. Br(x,l,r) \\<noteq> 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) \\<in> bt(A)";
-
-(** Lemmas to justify using "bt" in other recursive type definitions **)
-
-Goalw bt.defs "A \\<subseteq> B ==> bt(A) \\<subseteq> 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)) \\<subseteq> 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 \\<in> bt(A); \
-\ c \\<in> C(Lf); \
-\ !!x y z r s. [| x \\<in> A; y \\<in> bt(A); z \\<in> bt(A); r \\<in> C(y); s \\<in> C(z) |] ==> \
-\ h(x,y,z,r,s): C(Br(x,y,z)) \
-\ |] ==> bt_rec(c,h,t) \\<in> C(t)";
- (*instead of induct_tac "t", since t \\<in> 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 \\<in> bt(A) ==> n_nodes(t) \\<in> nat";
-by (induct_tac "t" 1);
-by Auto_tac;
-qed "n_nodes_type";
-
-
-(** n_leaves **)
-
-Goal "t \\<in> bt(A) ==> n_leaves(t) \\<in> nat";
-by (induct_tac "t" 1);
-by Auto_tac;
-qed "n_leaves_type";
-
-(** bt_reflect **)
-
-Goal "t \\<in> bt(A) ==> bt_reflect(t) \\<in> 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 \\<in> 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 \\<in> 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 \\<in> bt(A) ==> bt_reflect(bt_reflect(t))=t";
-by (induct_tac "t" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "bt_reflect_bt_reflect_ident";
-
-
--- 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 \\<in> 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
--- 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 \\<subseteq> C; B \\<subseteq> D |] ==> data(A,B) \\<subseteq> 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)) \\<subseteq> 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));
-
-
--- 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 \\<in> A")
- | Con2 ("a \\<in> A", "b \\<in> B")
- | Con3 ("a \\<in> A", "b \\<in> B", "d \\<in> data(A,B)")
-
-end
--- 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 \\<noteq> C01";
-by (Simp_tac 1);
-result();
-
--- 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