# HG changeset patch # User haftmann # Date 1259307668 -3600 # Node ID abf9fa17452ac69ae1d3bcc7b6f90d2d81c74f10 # Parent 03f2ab6a4ea60ad9777229795d5ca8e2958977d6 modernized; dropped ancient constant Part diff -r 03f2ab6a4ea6 -r abf9fa17452a src/HOL/Sum_Type.thy --- a/src/HOL/Sum_Type.thy Wed Nov 25 11:16:58 2009 +0100 +++ b/src/HOL/Sum_Type.thy Fri Nov 27 08:41:08 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Sum_Type.thy - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge *) @@ -10,188 +9,83 @@ imports Typedef Inductive Fun begin -text{*The representations of the two injections*} +subsection {* Construction of the sum type and its basic abstract operations *} -constdefs - Inl_Rep :: "['a, 'a, 'b, bool] => bool" - "Inl_Rep == (%a. %x y p. x=a & p)" +definition Inl_Rep :: "'a \ 'a \ 'b \ bool \ bool" where + "Inl_Rep a x y p \ x = a \ p" - Inr_Rep :: "['b, 'a, 'b, bool] => bool" - "Inr_Rep == (%b. %x y p. y=b & ~p)" - +definition Inr_Rep :: "'b \ 'a \ 'b \ bool \ bool" where + "Inr_Rep b x y p \ y = b \ \ p" global -typedef (Sum) - ('a, 'b) "+" (infixr "+" 10) - = "{f. (? a. f = Inl_Rep(a::'a)) | (? b. f = Inr_Rep(b::'b))}" +typedef (Sum) ('a, 'b) "+" (infixr "+" 10) = "{f. (\a. f = Inl_Rep (a::'a)) \ (\b. f = Inr_Rep (b::'b))}" by auto local - -text{*abstract constants and syntax*} - -constdefs - Inl :: "'a => 'a + 'b" - "Inl == (%a. Abs_Sum(Inl_Rep(a)))" +lemma Inl_RepI: "Inl_Rep a \ Sum" + by (auto simp add: Sum_def) - Inr :: "'b => 'a + 'b" - "Inr == (%b. Abs_Sum(Inr_Rep(b)))" - - Plus :: "['a set, 'b set] => ('a + 'b) set" (infixr "<+>" 65) - "A <+> B == (Inl`A) Un (Inr`B)" - --{*disjoint sum for sets; the operator + is overloaded with wrong type!*} +lemma Inr_RepI: "Inr_Rep b \ Sum" + by (auto simp add: Sum_def) - Part :: "['a set, 'b => 'a] => 'a set" - "Part A h == A Int {x. ? z. x = h(z)}" - --{*for selecting out the components of a mutually recursive definition*} - - +lemma inj_on_Abs_Sum: "A \ Sum \ inj_on Abs_Sum A" + by (rule inj_on_inverseI, rule Abs_Sum_inverse) auto -(** Inl_Rep and Inr_Rep: Representations of the constructors **) - -(*This counts as a non-emptiness result for admitting 'a+'b as a type*) -lemma Inl_RepI: "Inl_Rep(a) : Sum" -by (auto simp add: Sum_def) - -lemma Inr_RepI: "Inr_Rep(b) : Sum" -by (auto simp add: Sum_def) +lemma Inl_Rep_inject: "inj_on Inl_Rep A" +proof (rule inj_onI) + show "\a c. Inl_Rep a = Inl_Rep c \ a = c" + by (auto simp add: Inl_Rep_def expand_fun_eq) +qed -lemma inj_on_Abs_Sum: "inj_on Abs_Sum Sum" -apply (rule inj_on_inverseI) -apply (erule Abs_Sum_inverse) -done - -subsection{*Freeness Properties for @{term Inl} and @{term Inr}*} - -text{*Distinctness*} - -lemma Inl_Rep_not_Inr_Rep: "Inl_Rep(a) ~= Inr_Rep(b)" -by (auto simp add: Inl_Rep_def Inr_Rep_def expand_fun_eq) +lemma Inr_Rep_inject: "inj_on Inr_Rep A" +proof (rule inj_onI) + show "\b d. Inr_Rep b = Inr_Rep d \ b = d" + by (auto simp add: Inr_Rep_def expand_fun_eq) +qed -lemma Inl_not_Inr [iff]: "Inl(a) ~= Inr(b)" -apply (simp add: Inl_def Inr_def) -apply (rule inj_on_Abs_Sum [THEN inj_on_contraD]) -apply (rule Inl_Rep_not_Inr_Rep) -apply (rule Inl_RepI) -apply (rule Inr_RepI) -done - -lemmas Inr_not_Inl = Inl_not_Inr [THEN not_sym, standard] -declare Inr_not_Inl [iff] +lemma Inl_Rep_not_Inr_Rep: "Inl_Rep a \ Inr_Rep b" + by (auto simp add: Inl_Rep_def Inr_Rep_def expand_fun_eq) -lemmas Inl_neq_Inr = Inl_not_Inr [THEN notE, standard] -lemmas Inr_neq_Inl = sym [THEN Inl_neq_Inr, standard] - - -text{*Injectiveness*} +definition Inl :: "'a \ 'a + 'b" where + "Inl = Abs_Sum \ Inl_Rep" -lemma Inl_Rep_inject: "Inl_Rep(a) = Inl_Rep(c) ==> a=c" -by (auto simp add: Inl_Rep_def expand_fun_eq) - -lemma Inr_Rep_inject: "Inr_Rep(b) = Inr_Rep(d) ==> b=d" -by (auto simp add: Inr_Rep_def expand_fun_eq) +definition Inr :: "'b \ 'a + 'b" where + "Inr = Abs_Sum \ Inr_Rep" lemma inj_Inl [simp]: "inj_on Inl A" -apply (simp add: Inl_def) -apply (rule inj_onI) -apply (erule inj_on_Abs_Sum [THEN inj_onD, THEN Inl_Rep_inject]) -apply (rule Inl_RepI) -apply (rule Inl_RepI) -done +by (auto simp add: Inl_def intro!: comp_inj_on Inl_Rep_inject inj_on_Abs_Sum Inl_RepI) -lemmas Inl_inject = inj_Inl [THEN injD, standard] +lemma Inl_inject: "Inl x = Inl y \ x = y" +using inj_Inl by (rule injD) lemma inj_Inr [simp]: "inj_on Inr A" -apply (simp add: Inr_def) -apply (rule inj_onI) -apply (erule inj_on_Abs_Sum [THEN inj_onD, THEN Inr_Rep_inject]) -apply (rule Inr_RepI) -apply (rule Inr_RepI) -done - -lemmas Inr_inject = inj_Inr [THEN injD, standard] +by (auto simp add: Inr_def intro!: comp_inj_on Inr_Rep_inject inj_on_Abs_Sum Inr_RepI) -lemma Inl_eq [iff]: "(Inl(x)=Inl(y)) = (x=y)" -by (blast dest!: Inl_inject) - -lemma Inr_eq [iff]: "(Inr(x)=Inr(y)) = (x=y)" -by (blast dest!: Inr_inject) - - -subsection{*The Disjoint Sum of Sets*} +lemma Inr_inject: "Inr x = Inr y \ x = y" +using inj_Inr by (rule injD) -(** Introduction rules for the injections **) - -lemma InlI [intro!]: "a : A ==> Inl(a) : A <+> B" -by (simp add: Plus_def) - -lemma InrI [intro!]: "b : B ==> Inr(b) : A <+> B" -by (simp add: Plus_def) - -(** Elimination rules **) +lemma Inl_not_Inr: "Inl a \ Inr b" +proof - + from Inl_RepI [of a] Inr_RepI [of b] have "{Inl_Rep a, Inr_Rep b} \ Sum" by auto + with inj_on_Abs_Sum have "inj_on Abs_Sum {Inl_Rep a, Inr_Rep b}" . + with Inl_Rep_not_Inr_Rep [of a b] inj_on_contraD have "Abs_Sum (Inl_Rep a) \ Abs_Sum (Inr_Rep b)" by auto + then show ?thesis by (simp add: Inl_def Inr_def) +qed -lemma PlusE [elim!]: - "[| u: A <+> B; - !!x. [| x:A; u=Inl(x) |] ==> P; - !!y. [| y:B; u=Inr(y) |] ==> P - |] ==> P" -by (auto simp add: Plus_def) +lemma Inr_not_Inl: "Inr b \ Inl a" + using Inl_not_Inr by (rule not_sym) - - -text{*Exhaustion rule for sums, a degenerate form of induction*} lemma sumE: - "[| !!x::'a. s = Inl(x) ==> P; !!y::'b. s = Inr(y) ==> P - |] ==> P" -apply (rule Abs_Sum_cases [of s]) -apply (auto simp add: Sum_def Inl_def Inr_def) -done - - -lemma UNIV_Plus_UNIV [simp]: "UNIV <+> UNIV = UNIV" -apply (rule set_ext) -apply(rename_tac s) -apply(rule_tac s=s in sumE) -apply auto -done - -lemma Plus_eq_empty_conv[simp]: "A <+> B = {} \ A = {} \ B = {}" -by(auto) - -subsection{*The @{term Part} Primitive*} - -lemma Part_eqI [intro]: "[| a : A; a=h(b) |] ==> a : Part A h" -by (auto simp add: Part_def) - -lemmas PartI = Part_eqI [OF _ refl, standard] - -lemma PartE [elim!]: "[| a : Part A h; !!z. [| a : A; a=h(z) |] ==> P |] ==> P" -by (auto simp add: Part_def) - - -lemma Part_subset: "Part A h <= A" -by (auto simp add: Part_def) - -lemma Part_mono: "A<=B ==> Part A h <= Part B h" -by blast - -lemmas basic_monos = basic_monos Part_mono - -lemma PartD1: "a : Part A h ==> a : A" -by (simp add: Part_def) - -lemma Part_id: "Part A (%x. x) = A" -by blast - -lemma Part_Int: "Part (A Int B) h = (Part A h) Int (Part B h)" -by blast - -lemma Part_Collect: "Part (A Int {x. P x}) h = (Part A h) Int {x. P x}" -by blast - -subsection {* Representing sums *} + assumes "\x::'a. s = Inl x \ P" + and "\y::'b. s = Inr y \ P" + shows P +proof (rule Abs_Sum_cases [of s]) + fix f + assume "s = Abs_Sum f" and "f \ Sum" + with assms show P by (auto simp add: Sum_def Inl_def Inr_def) +qed rep_datatype (sum) Inl Inr proof - @@ -199,100 +93,99 @@ fix s :: "'a + 'b" assume x: "\x\'a. P (Inl x)" and y: "\y\'b. P (Inr y)" then show "P s" by (auto intro: sumE [of s]) -qed simp_all +qed (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr) + -lemma sum_case_KK[simp]: "sum_case (%x. a) (%x. a) = (%x. a)" +subsection {* Projections *} + +lemma sum_case_KK [simp]: "sum_case (\x. a) (\x. a) = (\x. a)" by (rule ext) (simp split: sum.split) -lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)" - apply (rule_tac s = s in sumE) - apply (erule ssubst) - apply (rule sum.cases(1)) - apply (erule ssubst) - apply (rule sum.cases(2)) - done +lemma surjective_sum: "sum_case (\x::'a. f (Inl x)) (\y::'b. f (Inr y)) = f" +proof + fix s :: "'a + 'b" + show "(case s of Inl (x\'a) \ f (Inl x) | Inr (y\'b) \ f (Inr y)) = f s" + by (cases s) simp_all +qed -lemma sum_case_weak_cong: "s = t ==> sum_case f g s = sum_case f g t" +lemma sum_case_inject: + assumes a: "sum_case f1 f2 = sum_case g1 g2" + assumes r: "f1 = g1 \ f2 = g2 \ P" + shows P +proof (rule r) + show "f1 = g1" proof + fix x :: 'a + from a have "sum_case f1 f2 (Inl x) = sum_case g1 g2 (Inl x)" by simp + then show "f1 x = g1 x" by simp + qed + show "f2 = g2" proof + fix y :: 'b + from a have "sum_case f1 f2 (Inr y) = sum_case g1 g2 (Inr y)" by simp + then show "f2 y = g2 y" by simp + qed +qed + +lemma sum_case_weak_cong: + "s = t \ sum_case f g s = sum_case f g t" -- {* Prevents simplification of @{text f} and @{text g}: much faster. *} by simp -lemma sum_case_inject: - "sum_case f1 f2 = sum_case g1 g2 ==> (f1 = g1 ==> f2 = g2 ==> P) ==> P" -proof - - assume a: "sum_case f1 f2 = sum_case g1 g2" - assume r: "f1 = g1 ==> f2 = g2 ==> P" - show P - apply (rule r) - apply (rule ext) - apply (cut_tac x = "Inl x" in a [THEN fun_cong], simp) - apply (rule ext) - apply (cut_tac x = "Inr x" in a [THEN fun_cong], simp) - done +primrec Projl :: "'a + 'b \ 'a" where + Projl_Inl: "Projl (Inl x) = x" + +primrec Projr :: "'a + 'b \ 'b" where + Projr_Inr: "Projr (Inr x) = x" + +primrec Suml :: "('a \ 'c) \ 'a + 'b \ 'c" where + "Suml f (Inl x) = f x" + +primrec Sumr :: "('b \ 'c) \ 'a + 'b \ 'c" where + "Sumr f (Inr x) = f x" + +lemma Suml_inject: + assumes "Suml f = Suml g" shows "f = g" +proof + fix x :: 'a + let ?s = "Inl x \ 'a + 'b" + from assms have "Suml f ?s = Suml g ?s" by simp + then show "f x = g x" by simp qed -constdefs - Suml :: "('a => 'c) => 'a + 'b => 'c" - "Suml == (%f. sum_case f undefined)" +lemma Sumr_inject: + assumes "Sumr f = Sumr g" shows "f = g" +proof + fix x :: 'b + let ?s = "Inr x \ 'a + 'b" + from assms have "Sumr f ?s = Sumr g ?s" by simp + then show "f x = g x" by simp +qed - Sumr :: "('b => 'c) => 'a + 'b => 'c" - "Sumr == sum_case undefined" +subsection {* The Disjoint Sum of Sets *} -lemma [code]: - "Suml f (Inl x) = f x" - by (simp add: Suml_def) +definition Plus :: "'a set \ 'b set \ ('a + 'b) set" (infixr "<+>" 65) where + "A <+> B = Inl ` A \ Inr ` B" + +lemma InlI [intro!]: "a \ A \ Inl a \ A <+> B" +by (simp add: Plus_def) -lemma [code]: - "Sumr f (Inr x) = f x" - by (simp add: Sumr_def) +lemma InrI [intro!]: "b \ B \ Inr b \ A <+> B" +by (simp add: Plus_def) -lemma Suml_inject: "Suml f = Suml g ==> f = g" - by (unfold Suml_def) (erule sum_case_inject) +text {* Exhaustion rule for sums, a degenerate form of induction *} + +lemma PlusE [elim!]: + "u \ A <+> B \ (\x. x \ A \ u = Inl x \ P) \ (\y. y \ B \ u = Inr y \ P) \ P" +by (auto simp add: Plus_def) -lemma Sumr_inject: "Sumr f = Sumr g ==> f = g" - by (unfold Sumr_def) (erule sum_case_inject) +lemma Plus_eq_empty_conv [simp]: "A <+> B = {} \ A = {} \ B = {}" +by auto -primrec Projl :: "'a + 'b => 'a" -where Projl_Inl: "Projl (Inl x) = x" - -primrec Projr :: "'a + 'b => 'b" -where Projr_Inr: "Projr (Inr x) = x" +lemma UNIV_Plus_UNIV [simp]: "UNIV <+> UNIV = UNIV" +proof (rule set_ext) + fix u :: "'a + 'b" + show "u \ UNIV <+> UNIV \ u \ UNIV" by (cases u) auto +qed hide (open) const Suml Sumr Projl Projr - -ML -{* -val Inl_RepI = thm "Inl_RepI"; -val Inr_RepI = thm "Inr_RepI"; -val inj_on_Abs_Sum = thm "inj_on_Abs_Sum"; -val Inl_Rep_not_Inr_Rep = thm "Inl_Rep_not_Inr_Rep"; -val Inl_not_Inr = thm "Inl_not_Inr"; -val Inr_not_Inl = thm "Inr_not_Inl"; -val Inl_neq_Inr = thm "Inl_neq_Inr"; -val Inr_neq_Inl = thm "Inr_neq_Inl"; -val Inl_Rep_inject = thm "Inl_Rep_inject"; -val Inr_Rep_inject = thm "Inr_Rep_inject"; -val inj_Inl = thm "inj_Inl"; -val Inl_inject = thm "Inl_inject"; -val inj_Inr = thm "inj_Inr"; -val Inr_inject = thm "Inr_inject"; -val Inl_eq = thm "Inl_eq"; -val Inr_eq = thm "Inr_eq"; -val InlI = thm "InlI"; -val InrI = thm "InrI"; -val PlusE = thm "PlusE"; -val sumE = thm "sumE"; -val Part_eqI = thm "Part_eqI"; -val PartI = thm "PartI"; -val PartE = thm "PartE"; -val Part_subset = thm "Part_subset"; -val Part_mono = thm "Part_mono"; -val PartD1 = thm "PartD1"; -val Part_id = thm "Part_id"; -val Part_Int = thm "Part_Int"; -val Part_Collect = thm "Part_Collect"; - -val basic_monos = thms "basic_monos"; -*} - end