src/ZF/OrderArith.thy
 author wenzelm Sun Nov 02 16:39:54 2014 +0100 (2014-11-02) changeset 58871 c399ae4b836f parent 46953 2b6e55924af3 child 60770 240563fbf41d permissions -rw-r--r--
 clasohm@1478 ` 1` ```(* Title: ZF/OrderArith.thy ``` clasohm@1478 ` 2` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` lcp@437 ` 3` ``` Copyright 1994 University of Cambridge ``` lcp@437 ` 4` ```*) ``` lcp@437 ` 5` wenzelm@58871 ` 6` ```section{*Combining Orderings: Foundations of Ordinal Arithmetic*} ``` paulson@13356 ` 7` haftmann@16417 ` 8` ```theory OrderArith imports Order Sum Ordinal begin ``` lcp@437 ` 9` wenzelm@24893 ` 10` ```definition ``` lcp@437 ` 11` ``` (*disjoint sum of two relations; underlies ordinal addition*) ``` wenzelm@24893 ` 12` ``` radd :: "[i,i,i,i]=>i" where ``` paulson@46953 ` 13` ``` "radd(A,r,B,s) == ``` paulson@46953 ` 14` ``` {z: (A+B) * (A+B). ``` paulson@46953 ` 15` ``` (\x y. z = ) | ``` paulson@46953 ` 16` ``` (\x' x. z = & :r) | ``` paulson@46820 ` 17` ``` (\y' y. z = & :s)}" ``` lcp@437 ` 18` wenzelm@24893 ` 19` ```definition ``` lcp@437 ` 20` ``` (*lexicographic product of two relations; underlies ordinal multiplication*) ``` wenzelm@24893 ` 21` ``` rmult :: "[i,i,i,i]=>i" where ``` paulson@46953 ` 22` ``` "rmult(A,r,B,s) == ``` paulson@46953 ` 23` ``` {z: (A*B) * (A*B). ``` paulson@46953 ` 24` ``` \x' y' x y. z = <, > & ``` clasohm@1155 ` 25` ``` (: r | (x'=x & : s))}" ``` lcp@437 ` 26` wenzelm@24893 ` 27` ```definition ``` lcp@437 ` 28` ``` (*inverse image of a relation*) ``` wenzelm@24893 ` 29` ``` rvimage :: "[i,i,i]=>i" where ``` paulson@46953 ` 30` ``` "rvimage(A,f,r) == {z \ A*A. \x y. z = & : r}" ``` paulson@13140 ` 31` wenzelm@24893 ` 32` ```definition ``` wenzelm@24893 ` 33` ``` measure :: "[i, i\i] \ i" where ``` paulson@13140 ` 34` ``` "measure(A,f) == {: A*A. f(x) < f(y)}" ``` paulson@13140 ` 35` paulson@13140 ` 36` paulson@13356 ` 37` ```subsection{*Addition of Relations -- Disjoint Sum*} ``` paulson@13140 ` 38` paulson@13512 ` 39` ```subsubsection{*Rewrite rules. Can be used to obtain introduction rules*} ``` paulson@13140 ` 40` paulson@46953 ` 41` ```lemma radd_Inl_Inr_iff [iff]: ``` paulson@46953 ` 42` ``` " \ radd(A,r,B,s) \ a \ A & b \ B" ``` paulson@13356 ` 43` ```by (unfold radd_def, blast) ``` paulson@13140 ` 44` paulson@46953 ` 45` ```lemma radd_Inl_iff [iff]: ``` paulson@46953 ` 46` ``` " \ radd(A,r,B,s) \ a':A & a \ A & :r" ``` paulson@13356 ` 47` ```by (unfold radd_def, blast) ``` paulson@13140 ` 48` paulson@46953 ` 49` ```lemma radd_Inr_iff [iff]: ``` paulson@46953 ` 50` ``` " \ radd(A,r,B,s) \ b':B & b \ B & :s" ``` paulson@13356 ` 51` ```by (unfold radd_def, blast) ``` paulson@13140 ` 52` paulson@46953 ` 53` ```lemma radd_Inr_Inl_iff [simp]: ``` paulson@46821 ` 54` ``` " \ radd(A,r,B,s) \ False" ``` paulson@13356 ` 55` ```by (unfold radd_def, blast) ``` paulson@13140 ` 56` paulson@46953 ` 57` ```declare radd_Inr_Inl_iff [THEN iffD1, dest!] ``` paulson@13823 ` 58` paulson@13512 ` 59` ```subsubsection{*Elimination Rule*} ``` paulson@13140 ` 60` paulson@13140 ` 61` ```lemma raddE: ``` paulson@46953 ` 62` ``` "[| \ radd(A,r,B,s); ``` paulson@46953 ` 63` ``` !!x y. [| p'=Inl(x); x \ A; p=Inr(y); y \ B |] ==> Q; ``` paulson@46953 ` 64` ``` !!x' x. [| p'=Inl(x'); p=Inl(x); : r; x':A; x \ A |] ==> Q; ``` paulson@46953 ` 65` ``` !!y' y. [| p'=Inr(y'); p=Inr(y); : s; y':B; y \ B |] ==> Q ``` paulson@13140 ` 66` ``` |] ==> Q" ``` paulson@46953 ` 67` ```by (unfold radd_def, blast) ``` paulson@13140 ` 68` paulson@13512 ` 69` ```subsubsection{*Type checking*} ``` paulson@13140 ` 70` paulson@46820 ` 71` ```lemma radd_type: "radd(A,r,B,s) \ (A+B) * (A+B)" ``` paulson@13140 ` 72` ```apply (unfold radd_def) ``` paulson@13140 ` 73` ```apply (rule Collect_subset) ``` paulson@13140 ` 74` ```done ``` paulson@13140 ` 75` paulson@13140 ` 76` ```lemmas field_radd = radd_type [THEN field_rel_subset] ``` paulson@13140 ` 77` paulson@13512 ` 78` ```subsubsection{*Linearity*} ``` paulson@13140 ` 79` paulson@46953 ` 80` ```lemma linear_radd: ``` paulson@13140 ` 81` ``` "[| linear(A,r); linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))" ``` paulson@46953 ` 82` ```by (unfold linear_def, blast) ``` paulson@13140 ` 83` paulson@13140 ` 84` paulson@13512 ` 85` ```subsubsection{*Well-foundedness*} ``` paulson@13140 ` 86` paulson@13140 ` 87` ```lemma wf_on_radd: "[| wf[A](r); wf[B](s) |] ==> wf[A+B](radd(A,r,B,s))" ``` paulson@13140 ` 88` ```apply (rule wf_onI2) ``` paulson@46820 ` 89` ```apply (subgoal_tac "\x\A. Inl (x) \ Ba") ``` paulson@13512 ` 90` ``` --{*Proving the lemma, which is needed twice!*} ``` paulson@13140 ` 91` ``` prefer 2 ``` paulson@46820 ` 92` ``` apply (erule_tac V = "y \ A + B" in thin_rl) ``` paulson@13140 ` 93` ``` apply (rule_tac ballI) ``` paulson@13784 ` 94` ``` apply (erule_tac r = r and a = x in wf_on_induct, assumption) ``` paulson@46953 ` 95` ``` apply blast ``` paulson@13512 ` 96` ```txt{*Returning to main part of proof*} ``` paulson@13140 ` 97` ```apply safe ``` paulson@13140 ` 98` ```apply blast ``` paulson@46953 ` 99` ```apply (erule_tac r = s and a = ya in wf_on_induct, assumption, blast) ``` paulson@13140 ` 100` ```done ``` paulson@13140 ` 101` paulson@13140 ` 102` ```lemma wf_radd: "[| wf(r); wf(s) |] ==> wf(radd(field(r),r,field(s),s))" ``` paulson@13140 ` 103` ```apply (simp add: wf_iff_wf_on_field) ``` paulson@13140 ` 104` ```apply (rule wf_on_subset_A [OF _ field_radd]) ``` paulson@46953 ` 105` ```apply (blast intro: wf_on_radd) ``` paulson@13140 ` 106` ```done ``` paulson@13140 ` 107` paulson@13140 ` 108` ```lemma well_ord_radd: ``` paulson@13140 ` 109` ``` "[| well_ord(A,r); well_ord(B,s) |] ==> well_ord(A+B, radd(A,r,B,s))" ``` paulson@13140 ` 110` ```apply (rule well_ordI) ``` paulson@13140 ` 111` ```apply (simp add: well_ord_def wf_on_radd) ``` paulson@13140 ` 112` ```apply (simp add: well_ord_def tot_ord_def linear_radd) ``` paulson@13140 ` 113` ```done ``` paulson@13140 ` 114` paulson@13512 ` 115` ```subsubsection{*An @{term ord_iso} congruence law*} ``` lcp@437 ` 116` paulson@13140 ` 117` ```lemma sum_bij: ``` paulson@46953 ` 118` ``` "[| f \ bij(A,C); g \ bij(B,D) |] ``` paulson@46820 ` 119` ``` ==> (\z\A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) \ bij(A+B, C+D)" ``` paulson@46953 ` 120` ```apply (rule_tac d = "case (%x. Inl (converse(f)`x), %y. Inr(converse(g)`y))" ``` paulson@13356 ` 121` ``` in lam_bijective) ``` paulson@46953 ` 122` ```apply (typecheck add: bij_is_inj inj_is_fun) ``` paulson@46953 ` 123` ```apply (auto simp add: left_inverse_bij right_inverse_bij) ``` paulson@13140 ` 124` ```done ``` paulson@13140 ` 125` paulson@46953 ` 126` ```lemma sum_ord_iso_cong: ``` paulson@46953 ` 127` ``` "[| f \ ord_iso(A,r,A',r'); g \ ord_iso(B,s,B',s') |] ==> ``` paulson@46953 ` 128` ``` (\z\A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) ``` paulson@46820 ` 129` ``` \ ord_iso(A+B, radd(A,r,B,s), A'+B', radd(A',r',B',s'))" ``` paulson@13140 ` 130` ```apply (unfold ord_iso_def) ``` paulson@13140 ` 131` ```apply (safe intro!: sum_bij) ``` paulson@13140 ` 132` ```(*Do the beta-reductions now*) ``` paulson@13140 ` 133` ```apply (auto cong add: conj_cong simp add: bij_is_fun [THEN apply_type]) ``` paulson@13140 ` 134` ```done ``` paulson@13140 ` 135` paulson@46953 ` 136` ```(*Could we prove an ord_iso result? Perhaps ``` paulson@46820 ` 137` ``` ord_iso(A+B, radd(A,r,B,s), A \ B, r \ s) *) ``` paulson@46953 ` 138` ```lemma sum_disjoint_bij: "A \ B = 0 ==> ``` paulson@46820 ` 139` ``` (\z\A+B. case(%x. x, %y. y, z)) \ bij(A+B, A \ B)" ``` paulson@46953 ` 140` ```apply (rule_tac d = "%z. if z \ A then Inl (z) else Inr (z) " in lam_bijective) ``` paulson@13140 ` 141` ```apply auto ``` paulson@13140 ` 142` ```done ``` paulson@13140 ` 143` paulson@13512 ` 144` ```subsubsection{*Associativity*} ``` paulson@13140 ` 145` paulson@13140 ` 146` ```lemma sum_assoc_bij: ``` paulson@46953 ` 147` ``` "(\z\(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) ``` paulson@46820 ` 148` ``` \ bij((A+B)+C, A+(B+C))" ``` paulson@46953 ` 149` ```apply (rule_tac d = "case (%x. Inl (Inl (x)), case (%x. Inl (Inr (x)), Inr))" ``` paulson@13140 ` 150` ``` in lam_bijective) ``` paulson@13140 ` 151` ```apply auto ``` paulson@13140 ` 152` ```done ``` paulson@13140 ` 153` paulson@13140 ` 154` ```lemma sum_assoc_ord_iso: ``` paulson@46953 ` 155` ``` "(\z\(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) ``` paulson@46953 ` 156` ``` \ ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t), ``` paulson@13140 ` 157` ``` A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))" ``` paulson@13356 ` 158` ```by (rule sum_assoc_bij [THEN ord_isoI], auto) ``` paulson@13140 ` 159` paulson@13140 ` 160` paulson@13356 ` 161` ```subsection{*Multiplication of Relations -- Lexicographic Product*} ``` paulson@13140 ` 162` paulson@13512 ` 163` ```subsubsection{*Rewrite rule. Can be used to obtain introduction rules*} ``` paulson@13140 ` 164` paulson@46953 ` 165` ```lemma rmult_iff [iff]: ``` paulson@46953 ` 166` ``` "<, > \ rmult(A,r,B,s) \ ``` paulson@46953 ` 167` ``` (: r & a':A & a \ A & b': B & b \ B) | ``` paulson@46953 ` 168` ``` (: s & a'=a & a \ A & b': B & b \ B)" ``` paulson@13140 ` 169` paulson@13356 ` 170` ```by (unfold rmult_def, blast) ``` paulson@13140 ` 171` paulson@46953 ` 172` ```lemma rmultE: ``` paulson@46953 ` 173` ``` "[| <, > \ rmult(A,r,B,s); ``` paulson@46953 ` 174` ``` [| : r; a':A; a \ A; b':B; b \ B |] ==> Q; ``` paulson@46953 ` 175` ``` [| : s; a \ A; a'=a; b':B; b \ B |] ==> Q ``` paulson@13140 ` 176` ``` |] ==> Q" ``` paulson@46953 ` 177` ```by blast ``` paulson@13140 ` 178` paulson@13512 ` 179` ```subsubsection{*Type checking*} ``` paulson@13140 ` 180` paulson@46820 ` 181` ```lemma rmult_type: "rmult(A,r,B,s) \ (A*B) * (A*B)" ``` paulson@13356 ` 182` ```by (unfold rmult_def, rule Collect_subset) ``` paulson@13140 ` 183` paulson@13140 ` 184` ```lemmas field_rmult = rmult_type [THEN field_rel_subset] ``` paulson@13140 ` 185` paulson@13512 ` 186` ```subsubsection{*Linearity*} ``` paulson@13140 ` 187` paulson@13140 ` 188` ```lemma linear_rmult: ``` paulson@13140 ` 189` ``` "[| linear(A,r); linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))" ``` paulson@46953 ` 190` ```by (simp add: linear_def, blast) ``` paulson@13140 ` 191` paulson@13512 ` 192` ```subsubsection{*Well-foundedness*} ``` paulson@13140 ` 193` paulson@13140 ` 194` ```lemma wf_on_rmult: "[| wf[A](r); wf[B](s) |] ==> wf[A*B](rmult(A,r,B,s))" ``` paulson@13140 ` 195` ```apply (rule wf_onI2) ``` paulson@13140 ` 196` ```apply (erule SigmaE) ``` paulson@13140 ` 197` ```apply (erule ssubst) ``` paulson@46820 ` 198` ```apply (subgoal_tac "\b\B. : Ba", blast) ``` paulson@13784 ` 199` ```apply (erule_tac a = x in wf_on_induct, assumption) ``` paulson@13140 ` 200` ```apply (rule ballI) ``` paulson@13784 ` 201` ```apply (erule_tac a = b in wf_on_induct, assumption) ``` paulson@13140 ` 202` ```apply (best elim!: rmultE bspec [THEN mp]) ``` paulson@13140 ` 203` ```done ``` paulson@13140 ` 204` paulson@13140 ` 205` paulson@13140 ` 206` ```lemma wf_rmult: "[| wf(r); wf(s) |] ==> wf(rmult(field(r),r,field(s),s))" ``` paulson@13140 ` 207` ```apply (simp add: wf_iff_wf_on_field) ``` paulson@13140 ` 208` ```apply (rule wf_on_subset_A [OF _ field_rmult]) ``` paulson@46953 ` 209` ```apply (blast intro: wf_on_rmult) ``` paulson@13140 ` 210` ```done ``` paulson@13140 ` 211` paulson@13140 ` 212` ```lemma well_ord_rmult: ``` paulson@13140 ` 213` ``` "[| well_ord(A,r); well_ord(B,s) |] ==> well_ord(A*B, rmult(A,r,B,s))" ``` paulson@13140 ` 214` ```apply (rule well_ordI) ``` paulson@13140 ` 215` ```apply (simp add: well_ord_def wf_on_rmult) ``` paulson@13140 ` 216` ```apply (simp add: well_ord_def tot_ord_def linear_rmult) ``` paulson@13140 ` 217` ```done ``` paulson@9883 ` 218` paulson@9883 ` 219` paulson@13512 ` 220` ```subsubsection{*An @{term ord_iso} congruence law*} ``` paulson@13140 ` 221` paulson@13140 ` 222` ```lemma prod_bij: ``` paulson@46953 ` 223` ``` "[| f \ bij(A,C); g \ bij(B,D) |] ``` paulson@46820 ` 224` ``` ==> (lam :A*B. ) \ bij(A*B, C*D)" ``` paulson@46953 ` 225` ```apply (rule_tac d = "%. " ``` paulson@13140 ` 226` ``` in lam_bijective) ``` paulson@46953 ` 227` ```apply (typecheck add: bij_is_inj inj_is_fun) ``` paulson@46953 ` 228` ```apply (auto simp add: left_inverse_bij right_inverse_bij) ``` paulson@13140 ` 229` ```done ``` paulson@13140 ` 230` paulson@46953 ` 231` ```lemma prod_ord_iso_cong: ``` paulson@46953 ` 232` ``` "[| f \ ord_iso(A,r,A',r'); g \ ord_iso(B,s,B',s') |] ``` paulson@46953 ` 233` ``` ==> (lam :A*B. ) ``` paulson@46820 ` 234` ``` \ ord_iso(A*B, rmult(A,r,B,s), A'*B', rmult(A',r',B',s'))" ``` paulson@13140 ` 235` ```apply (unfold ord_iso_def) ``` paulson@13140 ` 236` ```apply (safe intro!: prod_bij) ``` paulson@13140 ` 237` ```apply (simp_all add: bij_is_fun [THEN apply_type]) ``` paulson@13140 ` 238` ```apply (blast intro: bij_is_inj [THEN inj_apply_equality]) ``` paulson@13140 ` 239` ```done ``` paulson@13140 ` 240` paulson@46820 ` 241` ```lemma singleton_prod_bij: "(\z\A. ) \ bij(A, {x}*A)" ``` paulson@13784 ` 242` ```by (rule_tac d = snd in lam_bijective, auto) ``` paulson@13140 ` 243` paulson@13140 ` 244` ```(*Used??*) ``` paulson@13140 ` 245` ```lemma singleton_prod_ord_iso: ``` paulson@46953 ` 246` ``` "well_ord({x},xr) ==> ``` paulson@46820 ` 247` ``` (\z\A. ) \ ord_iso(A, r, {x}*A, rmult({x}, xr, A, r))" ``` paulson@13140 ` 248` ```apply (rule singleton_prod_bij [THEN ord_isoI]) ``` paulson@13140 ` 249` ```apply (simp (no_asm_simp)) ``` paulson@13140 ` 250` ```apply (blast dest: well_ord_is_wf [THEN wf_on_not_refl]) ``` paulson@13140 ` 251` ```done ``` paulson@13140 ` 252` paulson@13140 ` 253` ```(*Here we build a complicated function term, then simplify it using ``` paulson@13140 ` 254` ``` case_cong, id_conv, comp_lam, case_case.*) ``` paulson@13140 ` 255` ```lemma prod_sum_singleton_bij: ``` paulson@46953 ` 256` ``` "a\C ==> ``` paulson@46953 ` 257` ``` (\x\C*B + D. case(%x. x, %y., x)) ``` paulson@46820 ` 258` ``` \ bij(C*B + D, C*B \ {a}*D)" ``` paulson@13140 ` 259` ```apply (rule subst_elem) ``` paulson@13140 ` 260` ```apply (rule id_bij [THEN sum_bij, THEN comp_bij]) ``` paulson@13140 ` 261` ```apply (rule singleton_prod_bij) ``` paulson@13269 ` 262` ```apply (rule sum_disjoint_bij, blast) ``` paulson@13140 ` 263` ```apply (simp (no_asm_simp) cong add: case_cong) ``` paulson@13140 ` 264` ```apply (rule comp_lam [THEN trans, symmetric]) ``` paulson@13140 ` 265` ```apply (fast elim!: case_type) ``` paulson@13140 ` 266` ```apply (simp (no_asm_simp) add: case_case) ``` paulson@13140 ` 267` ```done ``` paulson@13140 ` 268` paulson@13140 ` 269` ```lemma prod_sum_singleton_ord_iso: ``` paulson@46953 ` 270` ``` "[| a \ A; well_ord(A,r) |] ==> ``` paulson@46953 ` 271` ``` (\x\pred(A,a,r)*B + pred(B,b,s). case(%x. x, %y., x)) ``` paulson@46953 ` 272` ``` \ ord_iso(pred(A,a,r)*B + pred(B,b,s), ``` paulson@46953 ` 273` ``` radd(A*B, rmult(A,r,B,s), B, s), ``` paulson@46820 ` 274` ``` pred(A,a,r)*B \ {a}*pred(B,b,s), rmult(A,r,B,s))" ``` paulson@13140 ` 275` ```apply (rule prod_sum_singleton_bij [THEN ord_isoI]) ``` paulson@13140 ` 276` ```apply (simp (no_asm_simp) add: pred_iff well_ord_is_wf [THEN wf_on_not_refl]) ``` paulson@13140 ` 277` ```apply (auto elim!: well_ord_is_wf [THEN wf_on_asym] predE) ``` paulson@13140 ` 278` ```done ``` paulson@13140 ` 279` paulson@13512 ` 280` ```subsubsection{*Distributive law*} ``` paulson@13140 ` 281` paulson@13140 ` 282` ```lemma sum_prod_distrib_bij: ``` paulson@46953 ` 283` ``` "(lam :(A+B)*C. case(%y. Inl(), %y. Inr(), x)) ``` paulson@46820 ` 284` ``` \ bij((A+B)*C, (A*C)+(B*C))" ``` paulson@46953 ` 285` ```by (rule_tac d = "case (%., %.) " ``` paulson@13356 ` 286` ``` in lam_bijective, auto) ``` paulson@13140 ` 287` paulson@13140 ` 288` ```lemma sum_prod_distrib_ord_iso: ``` paulson@46953 ` 289` ``` "(lam :(A+B)*C. case(%y. Inl(), %y. Inr(), x)) ``` paulson@46953 ` 290` ``` \ ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t), ``` paulson@13140 ` 291` ``` (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))" ``` paulson@13356 ` 292` ```by (rule sum_prod_distrib_bij [THEN ord_isoI], auto) ``` paulson@13140 ` 293` paulson@13512 ` 294` ```subsubsection{*Associativity*} ``` paulson@13140 ` 295` paulson@13140 ` 296` ```lemma prod_assoc_bij: ``` paulson@46820 ` 297` ``` "(lam <, z>:(A*B)*C. >) \ bij((A*B)*C, A*(B*C))" ``` paulson@13356 ` 298` ```by (rule_tac d = "%>. <, z>" in lam_bijective, auto) ``` paulson@13140 ` 299` paulson@13140 ` 300` ```lemma prod_assoc_ord_iso: ``` paulson@46953 ` 301` ``` "(lam <, z>:(A*B)*C. >) ``` paulson@46953 ` 302` ``` \ ord_iso((A*B)*C, rmult(A*B, rmult(A,r,B,s), C, t), ``` paulson@13140 ` 303` ``` A*(B*C), rmult(A, r, B*C, rmult(B,s,C,t)))" ``` paulson@13356 ` 304` ```by (rule prod_assoc_bij [THEN ord_isoI], auto) ``` paulson@13140 ` 305` paulson@13356 ` 306` ```subsection{*Inverse Image of a Relation*} ``` paulson@13140 ` 307` paulson@13512 ` 308` ```subsubsection{*Rewrite rule*} ``` paulson@13140 ` 309` paulson@46953 ` 310` ```lemma rvimage_iff: " \ rvimage(A,f,r) \ : r & a \ A & b \ A" ``` paulson@13269 ` 311` ```by (unfold rvimage_def, blast) ``` paulson@13140 ` 312` paulson@13512 ` 313` ```subsubsection{*Type checking*} ``` paulson@13140 ` 314` paulson@46820 ` 315` ```lemma rvimage_type: "rvimage(A,f,r) \ A*A" ``` paulson@13784 ` 316` ```by (unfold rvimage_def, rule Collect_subset) ``` paulson@13140 ` 317` paulson@13140 ` 318` ```lemmas field_rvimage = rvimage_type [THEN field_rel_subset] ``` paulson@13140 ` 319` paulson@13140 ` 320` ```lemma rvimage_converse: "rvimage(A,f, converse(r)) = converse(rvimage(A,f,r))" ``` paulson@13269 ` 321` ```by (unfold rvimage_def, blast) ``` paulson@13140 ` 322` paulson@13140 ` 323` paulson@13512 ` 324` ```subsubsection{*Partial Ordering Properties*} ``` paulson@13140 ` 325` paulson@46953 ` 326` ```lemma irrefl_rvimage: ``` paulson@46953 ` 327` ``` "[| f \ inj(A,B); irrefl(B,r) |] ==> irrefl(A, rvimage(A,f,r))" ``` paulson@13140 ` 328` ```apply (unfold irrefl_def rvimage_def) ``` paulson@13140 ` 329` ```apply (blast intro: inj_is_fun [THEN apply_type]) ``` paulson@13140 ` 330` ```done ``` paulson@13140 ` 331` paulson@46953 ` 332` ```lemma trans_on_rvimage: ``` paulson@46953 ` 333` ``` "[| f \ inj(A,B); trans[B](r) |] ==> trans[A](rvimage(A,f,r))" ``` paulson@13140 ` 334` ```apply (unfold trans_on_def rvimage_def) ``` paulson@13140 ` 335` ```apply (blast intro: inj_is_fun [THEN apply_type]) ``` paulson@13140 ` 336` ```done ``` paulson@13140 ` 337` paulson@46953 ` 338` ```lemma part_ord_rvimage: ``` paulson@46953 ` 339` ``` "[| f \ inj(A,B); part_ord(B,r) |] ==> part_ord(A, rvimage(A,f,r))" ``` paulson@13140 ` 340` ```apply (unfold part_ord_def) ``` paulson@13140 ` 341` ```apply (blast intro!: irrefl_rvimage trans_on_rvimage) ``` paulson@13140 ` 342` ```done ``` paulson@13140 ` 343` paulson@13512 ` 344` ```subsubsection{*Linearity*} ``` paulson@13140 ` 345` paulson@13140 ` 346` ```lemma linear_rvimage: ``` paulson@46953 ` 347` ``` "[| f \ inj(A,B); linear(B,r) |] ==> linear(A,rvimage(A,f,r))" ``` paulson@46953 ` 348` ```apply (simp add: inj_def linear_def rvimage_iff) ``` paulson@46953 ` 349` ```apply (blast intro: apply_funtype) ``` paulson@13140 ` 350` ```done ``` paulson@13140 ` 351` paulson@46953 ` 352` ```lemma tot_ord_rvimage: ``` paulson@46953 ` 353` ``` "[| f \ inj(A,B); tot_ord(B,r) |] ==> tot_ord(A, rvimage(A,f,r))" ``` paulson@13140 ` 354` ```apply (unfold tot_ord_def) ``` paulson@13140 ` 355` ```apply (blast intro!: part_ord_rvimage linear_rvimage) ``` paulson@13140 ` 356` ```done ``` paulson@13140 ` 357` paulson@13140 ` 358` paulson@13512 ` 359` ```subsubsection{*Well-foundedness*} ``` paulson@13140 ` 360` paulson@13140 ` 361` ```lemma wf_rvimage [intro!]: "wf(r) ==> wf(rvimage(A,f,r))" ``` paulson@13140 ` 362` ```apply (simp (no_asm_use) add: rvimage_def wf_eq_minimal) ``` paulson@13140 ` 363` ```apply clarify ``` paulson@46953 ` 364` ```apply (subgoal_tac "\w. w \ {w: {f`x. x \ Q}. \x. x \ Q & (f`x = w) }") ``` paulson@13140 ` 365` ``` apply (erule allE) ``` paulson@13140 ` 366` ``` apply (erule impE) ``` paulson@13269 ` 367` ``` apply assumption ``` paulson@13140 ` 368` ``` apply blast ``` paulson@46953 ` 369` ```apply blast ``` paulson@13140 ` 370` ```done ``` paulson@13140 ` 371` paulson@13544 ` 372` ```text{*But note that the combination of @{text wf_imp_wf_on} and ``` wenzelm@22710 ` 373` ``` @{text wf_rvimage} gives @{prop "wf(r) ==> wf[C](rvimage(A,f,r))"}*} ``` paulson@46953 ` 374` ```lemma wf_on_rvimage: "[| f \ A->B; wf[B](r) |] ==> wf[A](rvimage(A,f,r))" ``` paulson@13140 ` 375` ```apply (rule wf_onI2) ``` paulson@46953 ` 376` ```apply (subgoal_tac "\z\A. f`z=f`y \ z \ Ba") ``` paulson@13140 ` 377` ``` apply blast ``` paulson@13140 ` 378` ```apply (erule_tac a = "f`y" in wf_on_induct) ``` paulson@13140 ` 379` ``` apply (blast intro!: apply_funtype) ``` paulson@13140 ` 380` ```apply (blast intro!: apply_funtype dest!: rvimage_iff [THEN iffD1]) ``` paulson@13140 ` 381` ```done ``` paulson@13140 ` 382` paulson@13140 ` 383` ```(*Note that we need only wf[A](...) and linear(A,...) to get the result!*) ``` paulson@13140 ` 384` ```lemma well_ord_rvimage: ``` paulson@46953 ` 385` ``` "[| f \ inj(A,B); well_ord(B,r) |] ==> well_ord(A, rvimage(A,f,r))" ``` paulson@13140 ` 386` ```apply (rule well_ordI) ``` paulson@13140 ` 387` ```apply (unfold well_ord_def tot_ord_def) ``` paulson@13140 ` 388` ```apply (blast intro!: wf_on_rvimage inj_is_fun) ``` paulson@13140 ` 389` ```apply (blast intro!: linear_rvimage) ``` paulson@13140 ` 390` ```done ``` paulson@13140 ` 391` paulson@46953 ` 392` ```lemma ord_iso_rvimage: ``` paulson@46953 ` 393` ``` "f \ bij(A,B) ==> f \ ord_iso(A, rvimage(A,f,s), B, s)" ``` paulson@13140 ` 394` ```apply (unfold ord_iso_def) ``` paulson@13140 ` 395` ```apply (simp add: rvimage_iff) ``` paulson@13140 ` 396` ```done ``` paulson@13140 ` 397` paulson@46953 ` 398` ```lemma ord_iso_rvimage_eq: ``` paulson@46953 ` 399` ``` "f \ ord_iso(A,r, B,s) ==> rvimage(A,f,s) = r \ A*A" ``` paulson@13356 ` 400` ```by (unfold ord_iso_def rvimage_def, blast) ``` paulson@13140 ` 401` paulson@13140 ` 402` paulson@13634 ` 403` ```subsection{*Every well-founded relation is a subset of some inverse image of ``` paulson@13634 ` 404` ``` an ordinal*} ``` paulson@13634 ` 405` paulson@13634 ` 406` ```lemma wf_rvimage_Ord: "Ord(i) \ wf(rvimage(A, f, Memrel(i)))" ``` paulson@13634 ` 407` ```by (blast intro: wf_rvimage wf_Memrel) ``` paulson@13634 ` 408` paulson@13634 ` 409` wenzelm@24893 ` 410` ```definition ``` wenzelm@24893 ` 411` ``` wfrank :: "[i,i]=>i" where ``` paulson@13634 ` 412` ``` "wfrank(r,a) == wfrec(r, a, %x f. \y \ r-``{x}. succ(f`y))" ``` paulson@13634 ` 413` wenzelm@24893 ` 414` ```definition ``` wenzelm@24893 ` 415` ``` wftype :: "i=>i" where ``` paulson@13634 ` 416` ``` "wftype(r) == \y \ range(r). succ(wfrank(r,y))" ``` paulson@13634 ` 417` paulson@13634 ` 418` ```lemma wfrank: "wf(r) ==> wfrank(r,a) = (\y \ r-``{a}. succ(wfrank(r,y)))" ``` paulson@13634 ` 419` ```by (subst wfrank_def [THEN def_wfrec], simp_all) ``` paulson@13634 ` 420` paulson@13634 ` 421` ```lemma Ord_wfrank: "wf(r) ==> Ord(wfrank(r,a))" ``` paulson@13634 ` 422` ```apply (rule_tac a=a in wf_induct, assumption) ``` paulson@13634 ` 423` ```apply (subst wfrank, assumption) ``` paulson@13634 ` 424` ```apply (rule Ord_succ [THEN Ord_UN], blast) ``` paulson@13634 ` 425` ```done ``` paulson@13634 ` 426` paulson@13634 ` 427` ```lemma wfrank_lt: "[|wf(r); \ r|] ==> wfrank(r,a) < wfrank(r,b)" ``` paulson@13634 ` 428` ```apply (rule_tac a1 = b in wfrank [THEN ssubst], assumption) ``` paulson@13634 ` 429` ```apply (rule UN_I [THEN ltI]) ``` paulson@13634 ` 430` ```apply (simp add: Ord_wfrank vimage_iff)+ ``` paulson@13634 ` 431` ```done ``` paulson@13634 ` 432` paulson@13634 ` 433` ```lemma Ord_wftype: "wf(r) ==> Ord(wftype(r))" ``` paulson@13634 ` 434` ```by (simp add: wftype_def Ord_wfrank) ``` paulson@13634 ` 435` paulson@13634 ` 436` ```lemma wftypeI: "\wf(r); x \ field(r)\ \ wfrank(r,x) \ wftype(r)" ``` paulson@13634 ` 437` ```apply (simp add: wftype_def) ``` paulson@13634 ` 438` ```apply (blast intro: wfrank_lt [THEN ltD]) ``` paulson@13634 ` 439` ```done ``` paulson@13634 ` 440` paulson@13634 ` 441` paulson@13634 ` 442` ```lemma wf_imp_subset_rvimage: ``` paulson@46820 ` 443` ``` "[|wf(r); r \ A*A|] ==> \i f. Ord(i) & r \ rvimage(A, f, Memrel(i))" ``` paulson@13634 ` 444` ```apply (rule_tac x="wftype(r)" in exI) ``` paulson@13634 ` 445` ```apply (rule_tac x="\x\A. wfrank(r,x)" in exI) ``` paulson@13634 ` 446` ```apply (simp add: Ord_wftype, clarify) ``` paulson@13634 ` 447` ```apply (frule subsetD, assumption, clarify) ``` paulson@13634 ` 448` ```apply (simp add: rvimage_iff wfrank_lt [THEN ltD]) ``` paulson@13634 ` 449` ```apply (blast intro: wftypeI) ``` paulson@13634 ` 450` ```done ``` paulson@13634 ` 451` paulson@13634 ` 452` ```theorem wf_iff_subset_rvimage: ``` paulson@46821 ` 453` ``` "relation(r) ==> wf(r) \ (\i f A. Ord(i) & r \ rvimage(A, f, Memrel(i)))" ``` paulson@13634 ` 454` ```by (blast dest!: relation_field_times_field wf_imp_subset_rvimage ``` paulson@13634 ` 455` ``` intro: wf_rvimage_Ord [THEN wf_subset]) ``` paulson@13634 ` 456` paulson@13634 ` 457` paulson@13544 ` 458` ```subsection{*Other Results*} ``` paulson@13544 ` 459` paulson@46820 ` 460` ```lemma wf_times: "A \ B = 0 ==> wf(A*B)" ``` paulson@13544 ` 461` ```by (simp add: wf_def, blast) ``` paulson@13544 ` 462` paulson@13544 ` 463` ```text{*Could also be used to prove @{text wf_radd}*} ``` paulson@13544 ` 464` ```lemma wf_Un: ``` paulson@46820 ` 465` ``` "[| range(r) \ domain(s) = 0; wf(r); wf(s) |] ==> wf(r \ s)" ``` paulson@46953 ` 466` ```apply (simp add: wf_def, clarify) ``` paulson@46953 ` 467` ```apply (rule equalityI) ``` paulson@46953 ` 468` ``` prefer 2 apply blast ``` paulson@46953 ` 469` ```apply clarify ``` paulson@13544 ` 470` ```apply (drule_tac x=Z in spec) ``` paulson@46820 ` 471` ```apply (drule_tac x="Z \ domain(s)" in spec) ``` paulson@46953 ` 472` ```apply simp ``` paulson@46953 ` 473` ```apply (blast intro: elim: equalityE) ``` paulson@13544 ` 474` ```done ``` paulson@13544 ` 475` paulson@13544 ` 476` ```subsubsection{*The Empty Relation*} ``` paulson@13544 ` 477` paulson@13544 ` 478` ```lemma wf0: "wf(0)" ``` paulson@13544 ` 479` ```by (simp add: wf_def, blast) ``` paulson@13544 ` 480` paulson@13544 ` 481` ```lemma linear0: "linear(0,0)" ``` paulson@13544 ` 482` ```by (simp add: linear_def) ``` paulson@13544 ` 483` paulson@13544 ` 484` ```lemma well_ord0: "well_ord(0,0)" ``` paulson@13544 ` 485` ```by (blast intro: wf_imp_wf_on well_ordI wf0 linear0) ``` paulson@13512 ` 486` paulson@13512 ` 487` ```subsubsection{*The "measure" relation is useful with wfrec*} ``` paulson@13140 ` 488` paulson@13140 ` 489` ```lemma measure_eq_rvimage_Memrel: ``` paulson@13140 ` 490` ``` "measure(A,f) = rvimage(A,Lambda(A,f),Memrel(Collect(RepFun(A,f),Ord)))" ``` paulson@13140 ` 491` ```apply (simp (no_asm) add: measure_def rvimage_def Memrel_iff) ``` paulson@13269 ` 492` ```apply (rule equalityI, auto) ``` paulson@13140 ` 493` ```apply (auto intro: Ord_in_Ord simp add: lt_def) ``` paulson@13140 ` 494` ```done ``` paulson@13140 ` 495` paulson@13140 ` 496` ```lemma wf_measure [iff]: "wf(measure(A,f))" ``` paulson@13356 ` 497` ```by (simp (no_asm) add: measure_eq_rvimage_Memrel wf_Memrel wf_rvimage) ``` paulson@13140 ` 498` paulson@46953 ` 499` ```lemma measure_iff [iff]: " \ measure(A,f) \ x \ A & y \ A & f(x) A ==> Ord(f(x))" ``` paulson@13544 ` 504` ``` and inj: "!!x y. [|x \ A; y \ A; f(x) = f(y) |] ==> x=y" ``` paulson@13544 ` 505` ``` shows "linear(A, measure(A,f))" ``` paulson@46953 ` 506` ```apply (auto simp add: linear_def) ``` paulson@46953 ` 507` ```apply (rule_tac i="f(x)" and j="f(y)" in Ord_linear_lt) ``` paulson@46953 ` 508` ``` apply (simp_all add: Ordf) ``` paulson@46953 ` 509` ```apply (blast intro: inj) ``` paulson@13544 ` 510` ```done ``` paulson@13544 ` 511` paulson@13544 ` 512` ```lemma wf_on_measure: "wf[B](measure(A,f))" ``` paulson@13544 ` 513` ```by (rule wf_imp_wf_on [OF wf_measure]) ``` paulson@13544 ` 514` paulson@46953 ` 515` ```lemma well_ord_measure: ``` paulson@13544 ` 516` ``` assumes Ordf: "!!x. x \ A ==> Ord(f(x))" ``` paulson@13544 ` 517` ``` and inj: "!!x y. [|x \ A; y \ A; f(x) = f(y) |] ==> x=y" ``` paulson@13544 ` 518` ``` shows "well_ord(A, measure(A,f))" ``` paulson@13544 ` 519` ```apply (rule well_ordI) ``` paulson@46953 ` 520` ```apply (rule wf_on_measure) ``` paulson@46953 ` 521` ```apply (blast intro: linear_measure Ordf inj) ``` paulson@13544 ` 522` ```done ``` paulson@13544 ` 523` paulson@46820 ` 524` ```lemma measure_type: "measure(A,f) \ A*A" ``` paulson@13544 ` 525` ```by (auto simp add: measure_def) ``` paulson@13544 ` 526` paulson@13512 ` 527` ```subsubsection{*Well-foundedness of Unions*} ``` paulson@13512 ` 528` paulson@13512 ` 529` ```lemma wf_on_Union: ``` paulson@13512 ` 530` ``` assumes wfA: "wf[A](r)" ``` paulson@13512 ` 531` ``` and wfB: "!!a. a\A ==> wf[B(a)](s)" ``` paulson@46953 ` 532` ``` and ok: "!!a u v. [| \ s; v \ B(a); a \ A|] ``` paulson@13512 ` 533` ``` ==> (\a'\A. \ r & u \ B(a')) | u \ B(a)" ``` paulson@13512 ` 534` ``` shows "wf[\a\A. B(a)](s)" ``` paulson@13512 ` 535` ```apply (rule wf_onI2) ``` paulson@13512 ` 536` ```apply (erule UN_E) ``` paulson@13512 ` 537` ```apply (subgoal_tac "\z \ B(a). z \ Ba", blast) ``` paulson@13512 ` 538` ```apply (rule_tac a = a in wf_on_induct [OF wfA], assumption) ``` paulson@13512 ` 539` ```apply (rule ballI) ``` paulson@13512 ` 540` ```apply (rule_tac a = z in wf_on_induct [OF wfB], assumption, assumption) ``` paulson@46953 ` 541` ```apply (rename_tac u) ``` paulson@46953 ` 542` ```apply (drule_tac x=u in bspec, blast) ``` paulson@13512 ` 543` ```apply (erule mp, clarify) ``` paulson@46953 ` 544` ```apply (frule ok, assumption+, blast) ``` paulson@13512 ` 545` ```done ``` paulson@13512 ` 546` paulson@14120 ` 547` ```subsubsection{*Bijections involving Powersets*} ``` paulson@14120 ` 548` paulson@14120 ` 549` ```lemma Pow_sum_bij: ``` paulson@46953 ` 550` ``` "(\Z \ Pow(A+B). <{x \ A. Inl(x) \ Z}, {y \ B. Inr(y) \ Z}>) ``` paulson@14120 ` 551` ``` \ bij(Pow(A+B), Pow(A)*Pow(B))" ``` paulson@46953 ` 552` ```apply (rule_tac d = "%. {Inl (x). x \ X} \ {Inr (y). y \ Y}" ``` paulson@14120 ` 553` ``` in lam_bijective) ``` paulson@14120 ` 554` ```apply force+ ``` paulson@14120 ` 555` ```done ``` paulson@14120 ` 556` paulson@14120 ` 557` ```text{*As a special case, we have @{term "bij(Pow(A*B), A -> Pow(B))"} *} ``` paulson@14120 ` 558` ```lemma Pow_Sigma_bij: ``` paulson@46953 ` 559` ``` "(\r \ Pow(Sigma(A,B)). \x \ A. r``{x}) ``` skalberg@14171 ` 560` ``` \ bij(Pow(Sigma(A,B)), \ x \ A. Pow(B(x)))" ``` paulson@14120 ` 561` ```apply (rule_tac d = "%f. \x \ A. \y \ f`x. {}" in lam_bijective) ``` paulson@14120 ` 562` ```apply (blast intro: lam_type) ``` paulson@14120 ` 563` ```apply (blast dest: apply_type, simp_all) ``` paulson@14120 ` 564` ```apply fast (*strange, but blast can't do it*) ``` paulson@14120 ` 565` ```apply (rule fun_extension, auto) ``` paulson@14120 ` 566` ```by blast ``` paulson@14120 ` 567` lcp@437 ` 568` ```end ```