(* Title: ZF/Induct/Ntree.thy ID: $Id: Ntree.thy,v 1.5 2005/06/17 14:15:11 haftmann Exp $ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge *) header {* Datatype definition n-ary branching trees *} theory Ntree imports Main begin text {* Demonstrates a simple use of function space in a datatype definition. Based upon theory @{text Term}. *} consts ntree :: "i => i" maptree :: "i => i" maptree2 :: "[i, i] => i" datatype "ntree(A)" = Branch ("a ∈ A", "h ∈ (\<Union>n ∈ nat. n -> ntree(A))") monos UN_mono [OF subset_refl Pi_mono] -- {* MUST have this form *} type_intros nat_fun_univ [THEN subsetD] type_elims UN_E datatype "maptree(A)" = Sons ("a ∈ A", "h ∈ maptree(A) -||> maptree(A)") monos FiniteFun_mono1 -- {* Use monotonicity in BOTH args *} type_intros FiniteFun_univ1 [THEN subsetD] datatype "maptree2(A, B)" = Sons2 ("a ∈ A", "h ∈ B -||> maptree2(A, B)") monos FiniteFun_mono [OF subset_refl] type_intros FiniteFun_in_univ' constdefs ntree_rec :: "[[i, i, i] => i, i] => i" "ntree_rec(b) == Vrecursor(λpr. ntree_case(λx h. b(x, h, λi ∈ domain(h). pr`(h`i))))" constdefs ntree_copy :: "i => i" "ntree_copy(z) == ntree_rec(λx h r. Branch(x,r), z)" text {* \medskip @{text ntree} *} lemma ntree_unfold: "ntree(A) = A × (\<Union>n ∈ nat. n -> ntree(A))" by (blast intro: ntree.intros [unfolded ntree.con_defs] elim: ntree.cases [unfolded ntree.con_defs]) lemma ntree_induct [induct set: ntree]: "[| t ∈ ntree(A); !!x n h. [| x ∈ A; n ∈ nat; h ∈ n -> ntree(A); ∀i ∈ n. P(h`i) |] ==> P(Branch(x,h)) |] ==> P(t)" -- {* A nicer induction rule than the standard one. *} proof - case rule_context assume "t ∈ ntree(A)" thus ?thesis apply induct apply (erule UN_E) apply (assumption | rule rule_context)+ apply (fast elim: fun_weaken_type) apply (fast dest: apply_type) done qed lemma ntree_induct_eqn: "[| t ∈ ntree(A); f ∈ ntree(A)->B; g ∈ ntree(A)->B; !!x n h. [| x ∈ A; n ∈ nat; h ∈ n -> ntree(A); f O h = g O h |] ==> f ` Branch(x,h) = g ` Branch(x,h) |] ==> f`t=g`t" -- {* Induction on @{term "ntree(A)"} to prove an equation *} proof - case rule_context assume "t ∈ ntree(A)" thus ?thesis apply induct apply (assumption | rule rule_context)+ apply (insert rule_context) apply (rule fun_extension) apply (assumption | rule comp_fun)+ apply (simp add: comp_fun_apply) done qed text {* \medskip Lemmas to justify using @{text Ntree} in other recursive type definitions. *} lemma ntree_mono: "A ⊆ B ==> ntree(A) ⊆ ntree(B)" apply (unfold ntree.defs) apply (rule lfp_mono) apply (rule ntree.bnd_mono)+ apply (assumption | rule univ_mono basic_monos)+ done lemma ntree_univ: "ntree(univ(A)) ⊆ univ(A)" -- {* Easily provable by induction also *} apply (unfold ntree.defs ntree.con_defs) apply (rule lfp_lowerbound) apply (rule_tac [2] A_subset_univ [THEN univ_mono]) apply (blast intro: Pair_in_univ nat_fun_univ [THEN subsetD]) done lemma ntree_subset_univ: "A ⊆ univ(B) ==> ntree(A) ⊆ univ(B)" by (rule subset_trans [OF ntree_mono ntree_univ]) text {* \medskip @{text ntree} recursion. *} lemma ntree_rec_Branch: "function(h) ==> ntree_rec(b, Branch(x,h)) = b(x, h, λi ∈ domain(h). ntree_rec(b, h`i))" apply (rule ntree_rec_def [THEN def_Vrecursor, THEN trans]) apply (simp add: ntree.con_defs rank_pair2 [THEN [2] lt_trans] rank_apply) done lemma ntree_copy_Branch [simp]: "function(h) ==> ntree_copy (Branch(x, h)) = Branch(x, λi ∈ domain(h). ntree_copy (h`i))" by (simp add: ntree_copy_def ntree_rec_Branch) lemma ntree_copy_is_ident: "z ∈ ntree(A) ==> ntree_copy(z) = z" apply (induct_tac z) apply (auto simp add: domain_of_fun Pi_Collect_iff fun_is_function) done text {* \medskip @{text maptree} *} lemma maptree_unfold: "maptree(A) = A × (maptree(A) -||> maptree(A))" by (fast intro!: maptree.intros [unfolded maptree.con_defs] elim: maptree.cases [unfolded maptree.con_defs]) lemma maptree_induct [induct set: maptree]: "[| t ∈ maptree(A); !!x n h. [| x ∈ A; h ∈ maptree(A) -||> maptree(A); ∀y ∈ field(h). P(y) |] ==> P(Sons(x,h)) |] ==> P(t)" -- {* A nicer induction rule than the standard one. *} proof - case rule_context assume "t ∈ maptree(A)" thus ?thesis apply induct apply (assumption | rule rule_context)+ apply (erule Collect_subset [THEN FiniteFun_mono1, THEN subsetD]) apply (drule FiniteFun.dom_subset [THEN subsetD]) apply (drule Fin.dom_subset [THEN subsetD]) apply fast done qed text {* \medskip @{text maptree2} *} lemma maptree2_unfold: "maptree2(A, B) = A × (B -||> maptree2(A, B))" by (fast intro!: maptree2.intros [unfolded maptree2.con_defs] elim: maptree2.cases [unfolded maptree2.con_defs]) lemma maptree2_induct [induct set: maptree2]: "[| t ∈ maptree2(A, B); !!x n h. [| x ∈ A; h ∈ B -||> maptree2(A,B); ∀y ∈ range(h). P(y) |] ==> P(Sons2(x,h)) |] ==> P(t)" proof - case rule_context assume "t ∈ maptree2(A, B)" thus ?thesis apply induct apply (assumption | rule rule_context)+ apply (erule FiniteFun_mono [OF subset_refl Collect_subset, THEN subsetD]) apply (drule FiniteFun.dom_subset [THEN subsetD]) apply (drule Fin.dom_subset [THEN subsetD]) apply fast done qed end
lemma ntree_unfold:
ntree(A) = A × (\<Union>n∈nat. n -> ntree(A))
lemma ntree_induct:
[| t ∈ ntree(A); !!x n h. [| x ∈ A; n ∈ nat; h ∈ n -> ntree(A); ∀i∈n. P(h ` i) |] ==> P(Branch(x, h)) |] ==> P(t)
lemma ntree_induct_eqn:
[| t ∈ ntree(A); f ∈ ntree(A) -> B; g ∈ ntree(A) -> B; !!x n h. [| x ∈ A; n ∈ nat; h ∈ n -> ntree(A); f O h = g O h |] ==> f ` Branch(x, h) = g ` Branch(x, h) |] ==> f ` t = g ` t
lemma ntree_mono:
A ⊆ B ==> ntree(A) ⊆ ntree(B)
lemma ntree_univ:
ntree(univ(A)) ⊆ univ(A)
lemma ntree_subset_univ:
A ⊆ univ(B) ==> ntree(A) ⊆ univ(B)
lemma ntree_rec_Branch:
function(h) ==> ntree_rec(b, Branch(x, h)) = b(x, h, λi∈domain(h). ntree_rec(b, h ` i))
lemma ntree_copy_Branch:
function(h) ==> ntree_copy(Branch(x, h)) = Branch(x, λi∈domain(h). ntree_copy(h ` i))
lemma ntree_copy_is_ident:
z ∈ ntree(A) ==> ntree_copy(z) = z
lemma maptree_unfold:
maptree(A) = A × (maptree(A) -||> maptree(A))
lemma maptree_induct:
[| t ∈ maptree(A); !!x n h. [| x ∈ A; h ∈ maptree(A) -||> maptree(A); ∀y∈field(h). P(y) |] ==> P(Sons(x, h)) |] ==> P(t)
lemma maptree2_unfold:
maptree2(A, B) = A × (B -||> maptree2(A, B))
lemma maptree2_induct:
[| t ∈ maptree2(A, B); !!x n h. [| x ∈ A; h ∈ B -||> maptree2(A, B); ∀y∈range(h). P(y) |] ==> P(Sons2(x, h)) |] ==> P(t)