src/ZF/Sum.thy
 author wenzelm Sat Nov 04 19:17:19 2017 +0100 (21 months ago) changeset 67006 b1278ed3cd46 parent 60770 240563fbf41d child 69587 53982d5ec0bb permissions -rw-r--r--
prefer main entry points of HOL;
 wenzelm@41777 ` 1` ```(* Title: ZF/Sum.thy ``` clasohm@1478 ` 2` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` clasohm@0 ` 3` ``` Copyright 1993 University of Cambridge ``` clasohm@0 ` 4` ```*) ``` clasohm@0 ` 5` wenzelm@60770 ` 6` ```section\Disjoint Sums\ ``` paulson@13356 ` 7` haftmann@16417 ` 8` ```theory Sum imports Bool equalities begin ``` wenzelm@3923 ` 9` wenzelm@60770 ` 10` ```text\And the "Part" primitive for simultaneous recursive type definitions\ ``` paulson@13356 ` 11` haftmann@35416 ` 12` ```definition sum :: "[i,i]=>i" (infixr "+" 65) where ``` paulson@46820 ` 13` ``` "A+B == {0}*A \ {1}*B" ``` paulson@13240 ` 14` haftmann@35416 ` 15` ```definition Inl :: "i=>i" where ``` paulson@13240 ` 16` ``` "Inl(a) == <0,a>" ``` paulson@13240 ` 17` haftmann@35416 ` 18` ```definition Inr :: "i=>i" where ``` paulson@13240 ` 19` ``` "Inr(b) == <1,b>" ``` paulson@13240 ` 20` haftmann@35416 ` 21` ```definition "case" :: "[i=>i, i=>i, i]=>i" where ``` paulson@13240 ` 22` ``` "case(c,d) == (%. cond(y, d(z), c(z)))" ``` paulson@13240 ` 23` paulson@13240 ` 24` ``` (*operator for selecting out the various summands*) ``` haftmann@35416 ` 25` ```definition Part :: "[i,i=>i] => i" where ``` paulson@46953 ` 26` ``` "Part(A,h) == {x \ A. \z. x = h(z)}" ``` clasohm@0 ` 27` wenzelm@60770 ` 28` ```subsection\Rules for the @{term Part} Primitive\ ``` paulson@13240 ` 29` paulson@46953 ` 30` ```lemma Part_iff: ``` paulson@46953 ` 31` ``` "a \ Part(A,h) \ a \ A & (\y. a=h(y))" ``` paulson@13240 ` 32` ```apply (unfold Part_def) ``` paulson@13240 ` 33` ```apply (rule separation) ``` paulson@13240 ` 34` ```done ``` paulson@13240 ` 35` paulson@46953 ` 36` ```lemma Part_eqI [intro]: ``` paulson@46820 ` 37` ``` "[| a \ A; a=h(b) |] ==> a \ Part(A,h)" ``` paulson@13255 ` 38` ```by (unfold Part_def, blast) ``` paulson@13240 ` 39` paulson@13240 ` 40` ```lemmas PartI = refl [THEN [2] Part_eqI] ``` paulson@13240 ` 41` paulson@46953 ` 42` ```lemma PartE [elim!]: ``` paulson@46953 ` 43` ``` "[| a \ Part(A,h); !!z. [| a \ A; a=h(z) |] ==> P ``` paulson@13240 ` 44` ``` |] ==> P" ``` paulson@13255 ` 45` ```apply (unfold Part_def, blast) ``` paulson@13240 ` 46` ```done ``` paulson@13240 ` 47` paulson@46820 ` 48` ```lemma Part_subset: "Part(A,h) \ A" ``` paulson@13240 ` 49` ```apply (unfold Part_def) ``` paulson@13240 ` 50` ```apply (rule Collect_subset) ``` paulson@13240 ` 51` ```done ``` paulson@13240 ` 52` paulson@13240 ` 53` wenzelm@60770 ` 54` ```subsection\Rules for Disjoint Sums\ ``` paulson@13240 ` 55` paulson@13240 ` 56` ```lemmas sum_defs = sum_def Inl_def Inr_def case_def ``` paulson@13240 ` 57` paulson@13240 ` 58` ```lemma Sigma_bool: "Sigma(bool,C) = C(0) + C(1)" ``` paulson@13255 ` 59` ```by (unfold bool_def sum_def, blast) ``` paulson@13240 ` 60` paulson@13240 ` 61` ```(** Introduction rules for the injections **) ``` paulson@13240 ` 62` paulson@46820 ` 63` ```lemma InlI [intro!,simp,TC]: "a \ A ==> Inl(a) \ A+B" ``` paulson@13255 ` 64` ```by (unfold sum_defs, blast) ``` paulson@13240 ` 65` paulson@46820 ` 66` ```lemma InrI [intro!,simp,TC]: "b \ B ==> Inr(b) \ A+B" ``` paulson@13255 ` 67` ```by (unfold sum_defs, blast) ``` paulson@13240 ` 68` paulson@13240 ` 69` ```(** Elimination rules **) ``` paulson@13240 ` 70` paulson@13240 ` 71` ```lemma sumE [elim!]: ``` paulson@46953 ` 72` ``` "[| u \ A+B; ``` paulson@46953 ` 73` ``` !!x. [| x \ A; u=Inl(x) |] ==> P; ``` paulson@46953 ` 74` ``` !!y. [| y \ B; u=Inr(y) |] ==> P ``` paulson@13240 ` 75` ``` |] ==> P" ``` paulson@46953 ` 76` ```by (unfold sum_defs, blast) ``` paulson@13240 ` 77` paulson@13240 ` 78` ```(** Injection and freeness equivalences, for rewriting **) ``` paulson@13240 ` 79` paulson@46821 ` 80` ```lemma Inl_iff [iff]: "Inl(a)=Inl(b) \ a=b" ``` paulson@13255 ` 81` ```by (simp add: sum_defs) ``` paulson@13240 ` 82` paulson@46821 ` 83` ```lemma Inr_iff [iff]: "Inr(a)=Inr(b) \ a=b" ``` paulson@13255 ` 84` ```by (simp add: sum_defs) ``` paulson@13240 ` 85` paulson@46821 ` 86` ```lemma Inl_Inr_iff [simp]: "Inl(a)=Inr(b) \ False" ``` paulson@13255 ` 87` ```by (simp add: sum_defs) ``` paulson@13240 ` 88` paulson@46821 ` 89` ```lemma Inr_Inl_iff [simp]: "Inr(b)=Inl(a) \ False" ``` paulson@13255 ` 90` ```by (simp add: sum_defs) ``` paulson@13240 ` 91` paulson@13240 ` 92` ```lemma sum_empty [simp]: "0+0 = 0" ``` paulson@13255 ` 93` ```by (simp add: sum_defs) ``` paulson@13240 ` 94` paulson@13240 ` 95` ```(*Injection and freeness rules*) ``` paulson@13240 ` 96` wenzelm@45602 ` 97` ```lemmas Inl_inject = Inl_iff [THEN iffD1] ``` wenzelm@45602 ` 98` ```lemmas Inr_inject = Inr_iff [THEN iffD1] ``` paulson@13823 ` 99` ```lemmas Inl_neq_Inr = Inl_Inr_iff [THEN iffD1, THEN FalseE, elim!] ``` paulson@13823 ` 100` ```lemmas Inr_neq_Inl = Inr_Inl_iff [THEN iffD1, THEN FalseE, elim!] ``` paulson@13240 ` 101` paulson@13240 ` 102` paulson@46953 ` 103` ```lemma InlD: "Inl(a): A+B ==> a \ A" ``` paulson@13255 ` 104` ```by blast ``` paulson@13240 ` 105` paulson@46953 ` 106` ```lemma InrD: "Inr(b): A+B ==> b \ B" ``` paulson@13255 ` 107` ```by blast ``` paulson@13240 ` 108` paulson@46953 ` 109` ```lemma sum_iff: "u \ A+B \ (\x. x \ A & u=Inl(x)) | (\y. y \ B & u=Inr(y))" ``` paulson@13255 ` 110` ```by blast ``` paulson@13255 ` 111` wenzelm@58860 ` 112` ```lemma Inl_in_sum_iff [simp]: "(Inl(x) \ A+B) \ (x \ A)" ``` paulson@13255 ` 113` ```by auto ``` paulson@13255 ` 114` wenzelm@58860 ` 115` ```lemma Inr_in_sum_iff [simp]: "(Inr(y) \ A+B) \ (y \ B)" ``` paulson@13255 ` 116` ```by auto ``` paulson@13240 ` 117` paulson@46821 ` 118` ```lemma sum_subset_iff: "A+B \ C+D \ A<=C & B<=D" ``` paulson@13255 ` 119` ```by blast ``` paulson@13240 ` 120` paulson@46821 ` 121` ```lemma sum_equal_iff: "A+B = C+D \ A=C & B=D" ``` paulson@13255 ` 122` ```by (simp add: extension sum_subset_iff, blast) ``` paulson@13240 ` 123` paulson@13240 ` 124` ```lemma sum_eq_2_times: "A+A = 2*A" ``` paulson@13255 ` 125` ```by (simp add: sum_def, blast) ``` paulson@13240 ` 126` paulson@13240 ` 127` wenzelm@60770 ` 128` ```subsection\The Eliminator: @{term case}\ ``` clasohm@0 ` 129` paulson@13240 ` 130` ```lemma case_Inl [simp]: "case(c, d, Inl(a)) = c(a)" ``` paulson@13255 ` 131` ```by (simp add: sum_defs) ``` paulson@13240 ` 132` paulson@13240 ` 133` ```lemma case_Inr [simp]: "case(c, d, Inr(b)) = d(b)" ``` paulson@13255 ` 134` ```by (simp add: sum_defs) ``` paulson@13240 ` 135` paulson@13240 ` 136` ```lemma case_type [TC]: ``` paulson@46953 ` 137` ``` "[| u \ A+B; ``` paulson@46953 ` 138` ``` !!x. x \ A ==> c(x): C(Inl(x)); ``` paulson@46953 ` 139` ``` !!y. y \ B ==> d(y): C(Inr(y)) ``` paulson@46820 ` 140` ``` |] ==> case(c,d,u) \ C(u)" ``` paulson@13255 ` 141` ```by auto ``` paulson@13240 ` 142` paulson@46953 ` 143` ```lemma expand_case: "u \ A+B ==> ``` paulson@46953 ` 144` ``` R(case(c,d,u)) \ ``` paulson@46953 ` 145` ``` ((\x\A. u = Inl(x) \ R(c(x))) & ``` paulson@46820 ` 146` ``` (\y\B. u = Inr(y) \ R(d(y))))" ``` paulson@13240 ` 147` ```by auto ``` paulson@13240 ` 148` paulson@13240 ` 149` ```lemma case_cong: ``` paulson@46953 ` 150` ``` "[| z \ A+B; ``` paulson@46953 ` 151` ``` !!x. x \ A ==> c(x)=c'(x); ``` paulson@46953 ` 152` ``` !!y. y \ B ==> d(y)=d'(y) ``` paulson@13240 ` 153` ``` |] ==> case(c,d,z) = case(c',d',z)" ``` paulson@46953 ` 154` ```by auto ``` paulson@13240 ` 155` paulson@46953 ` 156` ```lemma case_case: "z \ A+B ==> ``` paulson@46953 ` 157` ``` case(c, d, case(%x. Inl(c'(x)), %y. Inr(d'(y)), z)) = ``` paulson@13240 ` 158` ``` case(%x. c(c'(x)), %y. d(d'(y)), z)" ``` paulson@13240 ` 159` ```by auto ``` paulson@13240 ` 160` paulson@13240 ` 161` wenzelm@60770 ` 162` ```subsection\More Rules for @{term "Part(A,h)"}\ ``` paulson@13240 ` 163` paulson@13240 ` 164` ```lemma Part_mono: "A<=B ==> Part(A,h)<=Part(B,h)" ``` paulson@13255 ` 165` ```by blast ``` paulson@13240 ` 166` paulson@13240 ` 167` ```lemma Part_Collect: "Part(Collect(A,P), h) = Collect(Part(A,h), P)" ``` paulson@13255 ` 168` ```by blast ``` paulson@13240 ` 169` paulson@13240 ` 170` ```lemmas Part_CollectE = ``` wenzelm@45602 ` 171` ``` Part_Collect [THEN equalityD1, THEN subsetD, THEN CollectE] ``` paulson@13240 ` 172` paulson@46953 ` 173` ```lemma Part_Inl: "Part(A+B,Inl) = {Inl(x). x \ A}" ``` paulson@13255 ` 174` ```by blast ``` paulson@13240 ` 175` paulson@46953 ` 176` ```lemma Part_Inr: "Part(A+B,Inr) = {Inr(y). y \ B}" ``` paulson@13255 ` 177` ```by blast ``` paulson@13240 ` 178` paulson@46820 ` 179` ```lemma PartD1: "a \ Part(A,h) ==> a \ A" ``` paulson@13255 ` 180` ```by (simp add: Part_def) ``` paulson@13240 ` 181` paulson@13240 ` 182` ```lemma Part_id: "Part(A,%x. x) = A" ``` paulson@13255 ` 183` ```by blast ``` paulson@13240 ` 184` paulson@46953 ` 185` ```lemma Part_Inr2: "Part(A+B, %x. Inr(h(x))) = {Inr(y). y \ Part(B,h)}" ``` paulson@13255 ` 186` ```by blast ``` paulson@13240 ` 187` paulson@46820 ` 188` ```lemma Part_sum_equality: "C \ A+B ==> Part(C,Inl) \ Part(C,Inr) = C" ``` paulson@13255 ` 189` ```by blast ``` paulson@13240 ` 190` clasohm@0 ` 191` ```end ```