src/ZF/OrderArith.thy
 author paulson Mon May 13 09:02:13 2002 +0200 (2002-05-13 ago) changeset 13140 6d97dbb189a9 parent 9883 c1c8647af477 child 13269 3ba9be497c33 permissions -rw-r--r--
converted Order.ML OrderType.ML OrderArith.ML to Isar format
 clasohm@1478 ` 1` ```(* Title: ZF/OrderArith.thy ``` lcp@437 ` 2` ``` ID: \$Id\$ ``` clasohm@1478 ` 3` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` lcp@437 ` 4` ``` Copyright 1994 University of Cambridge ``` lcp@437 ` 5` paulson@9883 ` 6` ```Towards ordinal arithmetic. Also useful with wfrec. ``` lcp@437 ` 7` ```*) ``` lcp@437 ` 8` paulson@13140 ` 9` ```theory OrderArith = Order + Sum + Ordinal: ``` paulson@13140 ` 10` ```constdefs ``` lcp@437 ` 11` lcp@437 ` 12` ``` (*disjoint sum of two relations; underlies ordinal addition*) ``` paulson@13140 ` 13` ``` radd :: "[i,i,i,i]=>i" ``` paulson@13140 ` 14` ``` "radd(A,r,B,s) == ``` clasohm@1155 ` 15` ``` {z: (A+B) * (A+B). ``` clasohm@1478 ` 16` ``` (EX x y. z = ) | ``` clasohm@1478 ` 17` ``` (EX x' x. z = & :r) | ``` clasohm@1155 ` 18` ``` (EX y' y. z = & :s)}" ``` lcp@437 ` 19` lcp@437 ` 20` ``` (*lexicographic product of two relations; underlies ordinal multiplication*) ``` paulson@13140 ` 21` ``` rmult :: "[i,i,i,i]=>i" ``` paulson@13140 ` 22` ``` "rmult(A,r,B,s) == ``` clasohm@1155 ` 23` ``` {z: (A*B) * (A*B). ``` clasohm@1478 ` 24` ``` EX x' y' x y. z = <, > & ``` clasohm@1155 ` 25` ``` (: r | (x'=x & : s))}" ``` lcp@437 ` 26` lcp@437 ` 27` ``` (*inverse image of a relation*) ``` paulson@13140 ` 28` ``` rvimage :: "[i,i,i]=>i" ``` paulson@13140 ` 29` ``` "rvimage(A,f,r) == {z: A*A. EX x y. z = & : r}" ``` paulson@13140 ` 30` paulson@13140 ` 31` ``` measure :: "[i, i\i] \ i" ``` paulson@13140 ` 32` ``` "measure(A,f) == {: A*A. f(x) < f(y)}" ``` paulson@13140 ` 33` paulson@13140 ` 34` paulson@13140 ` 35` ```(**** Addition of relations -- disjoint sum ****) ``` paulson@13140 ` 36` paulson@13140 ` 37` ```(** Rewrite rules. Can be used to obtain introduction rules **) ``` paulson@13140 ` 38` paulson@13140 ` 39` ```lemma radd_Inl_Inr_iff [iff]: ``` paulson@13140 ` 40` ``` " : radd(A,r,B,s) <-> a:A & b:B" ``` paulson@13140 ` 41` ```apply (unfold radd_def) ``` paulson@13140 ` 42` ```apply blast ``` paulson@13140 ` 43` ```done ``` paulson@13140 ` 44` paulson@13140 ` 45` ```lemma radd_Inl_iff [iff]: ``` paulson@13140 ` 46` ``` " : radd(A,r,B,s) <-> a':A & a:A & :r" ``` paulson@13140 ` 47` ```apply (unfold radd_def) ``` paulson@13140 ` 48` ```apply blast ``` paulson@13140 ` 49` ```done ``` paulson@13140 ` 50` paulson@13140 ` 51` ```lemma radd_Inr_iff [iff]: ``` paulson@13140 ` 52` ``` " : radd(A,r,B,s) <-> b':B & b:B & :s" ``` paulson@13140 ` 53` ```apply (unfold radd_def) ``` paulson@13140 ` 54` ```apply blast ``` paulson@13140 ` 55` ```done ``` paulson@13140 ` 56` paulson@13140 ` 57` ```lemma radd_Inr_Inl_iff [iff]: ``` paulson@13140 ` 58` ``` " : radd(A,r,B,s) <-> False" ``` paulson@13140 ` 59` ```apply (unfold radd_def) ``` paulson@13140 ` 60` ```apply blast ``` paulson@13140 ` 61` ```done ``` paulson@13140 ` 62` paulson@13140 ` 63` ```(** Elimination Rule **) ``` paulson@13140 ` 64` paulson@13140 ` 65` ```lemma raddE: ``` paulson@13140 ` 66` ``` "[| : radd(A,r,B,s); ``` paulson@13140 ` 67` ``` !!x y. [| p'=Inl(x); x:A; p=Inr(y); y:B |] ==> Q; ``` paulson@13140 ` 68` ``` !!x' x. [| p'=Inl(x'); p=Inl(x); : r; x':A; x:A |] ==> Q; ``` paulson@13140 ` 69` ``` !!y' y. [| p'=Inr(y'); p=Inr(y); : s; y':B; y:B |] ==> Q ``` paulson@13140 ` 70` ``` |] ==> Q" ``` paulson@13140 ` 71` ```apply (unfold radd_def) ``` paulson@13140 ` 72` ```apply (blast intro: elim:); ``` paulson@13140 ` 73` ```done ``` paulson@13140 ` 74` paulson@13140 ` 75` ```(** Type checking **) ``` paulson@13140 ` 76` paulson@13140 ` 77` ```lemma radd_type: "radd(A,r,B,s) <= (A+B) * (A+B)" ``` paulson@13140 ` 78` ```apply (unfold radd_def) ``` paulson@13140 ` 79` ```apply (rule Collect_subset) ``` paulson@13140 ` 80` ```done ``` paulson@13140 ` 81` paulson@13140 ` 82` ```lemmas field_radd = radd_type [THEN field_rel_subset] ``` paulson@13140 ` 83` paulson@13140 ` 84` ```(** Linearity **) ``` paulson@13140 ` 85` paulson@13140 ` 86` ```lemma linear_radd: ``` paulson@13140 ` 87` ``` "[| linear(A,r); linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))" ``` paulson@13140 ` 88` ```apply (unfold linear_def) ``` paulson@13140 ` 89` ```apply (blast intro: elim:); ``` paulson@13140 ` 90` ```done ``` paulson@13140 ` 91` paulson@13140 ` 92` paulson@13140 ` 93` ```(** Well-foundedness **) ``` paulson@13140 ` 94` paulson@13140 ` 95` ```lemma wf_on_radd: "[| wf[A](r); wf[B](s) |] ==> wf[A+B](radd(A,r,B,s))" ``` paulson@13140 ` 96` ```apply (rule wf_onI2) ``` paulson@13140 ` 97` ```apply (subgoal_tac "ALL x:A. Inl (x) : Ba") ``` paulson@13140 ` 98` ```(*Proving the lemma, which is needed twice!*) ``` paulson@13140 ` 99` ``` prefer 2 ``` paulson@13140 ` 100` ``` apply (erule_tac V = "y : A + B" in thin_rl) ``` paulson@13140 ` 101` ``` apply (rule_tac ballI) ``` paulson@13140 ` 102` ``` apply (erule_tac r = "r" and a = "x" in wf_on_induct, assumption) ``` paulson@13140 ` 103` ``` apply (blast intro: elim:); ``` paulson@13140 ` 104` ```(*Returning to main part of proof*) ``` paulson@13140 ` 105` ```apply safe ``` paulson@13140 ` 106` ```apply blast ``` paulson@13140 ` 107` ```apply (erule_tac r = "s" and a = "ya" in wf_on_induct , assumption) ``` paulson@13140 ` 108` ```apply (blast intro: elim:); ``` paulson@13140 ` 109` ```done ``` paulson@13140 ` 110` paulson@13140 ` 111` ```lemma wf_radd: "[| wf(r); wf(s) |] ==> wf(radd(field(r),r,field(s),s))" ``` paulson@13140 ` 112` ```apply (simp add: wf_iff_wf_on_field) ``` paulson@13140 ` 113` ```apply (rule wf_on_subset_A [OF _ field_radd]) ``` paulson@13140 ` 114` ```apply (blast intro: wf_on_radd) ``` paulson@13140 ` 115` ```done ``` paulson@13140 ` 116` paulson@13140 ` 117` ```lemma well_ord_radd: ``` paulson@13140 ` 118` ``` "[| well_ord(A,r); well_ord(B,s) |] ==> well_ord(A+B, radd(A,r,B,s))" ``` paulson@13140 ` 119` ```apply (rule well_ordI) ``` paulson@13140 ` 120` ```apply (simp add: well_ord_def wf_on_radd) ``` paulson@13140 ` 121` ```apply (simp add: well_ord_def tot_ord_def linear_radd) ``` paulson@13140 ` 122` ```done ``` paulson@13140 ` 123` paulson@13140 ` 124` ```(** An ord_iso congruence law **) ``` lcp@437 ` 125` paulson@13140 ` 126` ```lemma sum_bij: ``` paulson@13140 ` 127` ``` "[| f: bij(A,C); g: bij(B,D) |] ``` paulson@13140 ` 128` ``` ==> (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) : bij(A+B, C+D)" ``` paulson@13140 ` 129` ```apply (rule_tac d = "case (%x. Inl (converse (f) `x) , %y. Inr (converse (g) `y))" in lam_bijective) ``` paulson@13140 ` 130` ```apply (typecheck add: bij_is_inj inj_is_fun) ``` paulson@13140 ` 131` ```apply (auto simp add: left_inverse_bij right_inverse_bij) ``` paulson@13140 ` 132` ```done ``` paulson@13140 ` 133` paulson@13140 ` 134` ```lemma sum_ord_iso_cong: ``` paulson@13140 ` 135` ``` "[| f: ord_iso(A,r,A',r'); g: ord_iso(B,s,B',s') |] ==> ``` paulson@13140 ` 136` ``` (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) ``` paulson@13140 ` 137` ``` : ord_iso(A+B, radd(A,r,B,s), A'+B', radd(A',r',B',s'))" ``` paulson@13140 ` 138` ```apply (unfold ord_iso_def) ``` paulson@13140 ` 139` ```apply (safe intro!: sum_bij) ``` paulson@13140 ` 140` ```(*Do the beta-reductions now*) ``` paulson@13140 ` 141` ```apply (auto cong add: conj_cong simp add: bij_is_fun [THEN apply_type]) ``` paulson@13140 ` 142` ```done ``` paulson@13140 ` 143` paulson@13140 ` 144` ```(*Could we prove an ord_iso result? Perhaps ``` paulson@13140 ` 145` ``` ord_iso(A+B, radd(A,r,B,s), A Un B, r Un s) *) ``` paulson@13140 ` 146` ```lemma sum_disjoint_bij: "A Int B = 0 ==> ``` paulson@13140 ` 147` ``` (lam z:A+B. case(%x. x, %y. y, z)) : bij(A+B, A Un B)" ``` paulson@13140 ` 148` ```apply (rule_tac d = "%z. if z:A then Inl (z) else Inr (z) " in lam_bijective) ``` paulson@13140 ` 149` ```apply auto ``` paulson@13140 ` 150` ```done ``` paulson@13140 ` 151` paulson@13140 ` 152` ```(** Associativity **) ``` paulson@13140 ` 153` paulson@13140 ` 154` ```lemma sum_assoc_bij: ``` paulson@13140 ` 155` ``` "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) ``` paulson@13140 ` 156` ``` : bij((A+B)+C, A+(B+C))" ``` paulson@13140 ` 157` ```apply (rule_tac d = "case (%x. Inl (Inl (x)), case (%x. Inl (Inr (x)), Inr))" ``` paulson@13140 ` 158` ``` in lam_bijective) ``` paulson@13140 ` 159` ```apply auto ``` paulson@13140 ` 160` ```done ``` paulson@13140 ` 161` paulson@13140 ` 162` ```lemma sum_assoc_ord_iso: ``` paulson@13140 ` 163` ``` "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) ``` paulson@13140 ` 164` ``` : ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t), ``` paulson@13140 ` 165` ``` A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))" ``` paulson@13140 ` 166` ```apply (rule sum_assoc_bij [THEN ord_isoI]) ``` paulson@13140 ` 167` ```apply auto ``` paulson@13140 ` 168` ```done ``` paulson@13140 ` 169` paulson@13140 ` 170` paulson@13140 ` 171` ```(**** Multiplication of relations -- lexicographic product ****) ``` paulson@13140 ` 172` paulson@13140 ` 173` ```(** Rewrite rule. Can be used to obtain introduction rules **) ``` paulson@13140 ` 174` paulson@13140 ` 175` ```lemma rmult_iff [iff]: ``` paulson@13140 ` 176` ``` "<, > : rmult(A,r,B,s) <-> ``` paulson@13140 ` 177` ``` (: r & a':A & a:A & b': B & b: B) | ``` paulson@13140 ` 178` ``` (: s & a'=a & a:A & b': B & b: B)" ``` paulson@13140 ` 179` paulson@13140 ` 180` ```apply (unfold rmult_def) ``` paulson@13140 ` 181` ```apply blast ``` paulson@13140 ` 182` ```done ``` paulson@13140 ` 183` paulson@13140 ` 184` ```lemma rmultE: ``` paulson@13140 ` 185` ``` "[| <, > : rmult(A,r,B,s); ``` paulson@13140 ` 186` ``` [| : r; a':A; a:A; b':B; b:B |] ==> Q; ``` paulson@13140 ` 187` ``` [| : s; a:A; a'=a; b':B; b:B |] ==> Q ``` paulson@13140 ` 188` ``` |] ==> Q" ``` paulson@13140 ` 189` ```apply (blast intro: elim:); ``` paulson@13140 ` 190` ```done ``` paulson@13140 ` 191` paulson@13140 ` 192` ```(** Type checking **) ``` paulson@13140 ` 193` paulson@13140 ` 194` ```lemma rmult_type: "rmult(A,r,B,s) <= (A*B) * (A*B)" ``` paulson@13140 ` 195` ```apply (unfold rmult_def) ``` paulson@13140 ` 196` ```apply (rule Collect_subset) ``` paulson@13140 ` 197` ```done ``` paulson@13140 ` 198` paulson@13140 ` 199` ```lemmas field_rmult = rmult_type [THEN field_rel_subset] ``` paulson@13140 ` 200` paulson@13140 ` 201` ```(** Linearity **) ``` paulson@13140 ` 202` paulson@13140 ` 203` ```lemma linear_rmult: ``` paulson@13140 ` 204` ``` "[| linear(A,r); linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))" ``` paulson@13140 ` 205` ```apply (simp add: linear_def); ``` paulson@13140 ` 206` ```apply (blast intro: elim:); ``` paulson@13140 ` 207` ```done ``` paulson@13140 ` 208` paulson@13140 ` 209` ```(** Well-foundedness **) ``` paulson@13140 ` 210` paulson@13140 ` 211` ```lemma wf_on_rmult: "[| wf[A](r); wf[B](s) |] ==> wf[A*B](rmult(A,r,B,s))" ``` paulson@13140 ` 212` ```apply (rule wf_onI2) ``` paulson@13140 ` 213` ```apply (erule SigmaE) ``` paulson@13140 ` 214` ```apply (erule ssubst) ``` paulson@13140 ` 215` ```apply (subgoal_tac "ALL b:B. : Ba") ``` paulson@13140 ` 216` ```apply blast ``` paulson@13140 ` 217` ```apply (erule_tac a = "x" in wf_on_induct , assumption) ``` paulson@13140 ` 218` ```apply (rule ballI) ``` paulson@13140 ` 219` ```apply (erule_tac a = "b" in wf_on_induct , assumption) ``` paulson@13140 ` 220` ```apply (best elim!: rmultE bspec [THEN mp]) ``` paulson@13140 ` 221` ```done ``` paulson@13140 ` 222` paulson@13140 ` 223` paulson@13140 ` 224` ```lemma wf_rmult: "[| wf(r); wf(s) |] ==> wf(rmult(field(r),r,field(s),s))" ``` paulson@13140 ` 225` ```apply (simp add: wf_iff_wf_on_field) ``` paulson@13140 ` 226` ```apply (rule wf_on_subset_A [OF _ field_rmult]) ``` paulson@13140 ` 227` ```apply (blast intro: wf_on_rmult) ``` paulson@13140 ` 228` ```done ``` paulson@13140 ` 229` paulson@13140 ` 230` ```lemma well_ord_rmult: ``` paulson@13140 ` 231` ``` "[| well_ord(A,r); well_ord(B,s) |] ==> well_ord(A*B, rmult(A,r,B,s))" ``` paulson@13140 ` 232` ```apply (rule well_ordI) ``` paulson@13140 ` 233` ```apply (simp add: well_ord_def wf_on_rmult) ``` paulson@13140 ` 234` ```apply (simp add: well_ord_def tot_ord_def linear_rmult) ``` paulson@13140 ` 235` ```done ``` paulson@9883 ` 236` paulson@9883 ` 237` paulson@13140 ` 238` ```(** An ord_iso congruence law **) ``` paulson@13140 ` 239` paulson@13140 ` 240` ```lemma prod_bij: ``` paulson@13140 ` 241` ``` "[| f: bij(A,C); g: bij(B,D) |] ``` paulson@13140 ` 242` ``` ==> (lam :A*B. ) : bij(A*B, C*D)" ``` paulson@13140 ` 243` ```apply (rule_tac d = "%. " ``` paulson@13140 ` 244` ``` in lam_bijective) ``` paulson@13140 ` 245` ```apply (typecheck add: bij_is_inj inj_is_fun) ``` paulson@13140 ` 246` ```apply (auto simp add: left_inverse_bij right_inverse_bij) ``` paulson@13140 ` 247` ```done ``` paulson@13140 ` 248` paulson@13140 ` 249` ```lemma prod_ord_iso_cong: ``` paulson@13140 ` 250` ``` "[| f: ord_iso(A,r,A',r'); g: ord_iso(B,s,B',s') |] ``` paulson@13140 ` 251` ``` ==> (lam :A*B. ) ``` paulson@13140 ` 252` ``` : ord_iso(A*B, rmult(A,r,B,s), A'*B', rmult(A',r',B',s'))" ``` paulson@13140 ` 253` ```apply (unfold ord_iso_def) ``` paulson@13140 ` 254` ```apply (safe intro!: prod_bij) ``` paulson@13140 ` 255` ```apply (simp_all add: bij_is_fun [THEN apply_type]) ``` paulson@13140 ` 256` ```apply (blast intro: bij_is_inj [THEN inj_apply_equality]) ``` paulson@13140 ` 257` ```done ``` paulson@13140 ` 258` paulson@13140 ` 259` ```lemma singleton_prod_bij: "(lam z:A. ) : bij(A, {x}*A)" ``` paulson@13140 ` 260` ```apply (rule_tac d = "snd" in lam_bijective) ``` paulson@13140 ` 261` ```apply auto ``` paulson@13140 ` 262` ```done ``` paulson@13140 ` 263` paulson@13140 ` 264` ```(*Used??*) ``` paulson@13140 ` 265` ```lemma singleton_prod_ord_iso: ``` paulson@13140 ` 266` ``` "well_ord({x},xr) ==> ``` paulson@13140 ` 267` ``` (lam z:A. ) : ord_iso(A, r, {x}*A, rmult({x}, xr, A, r))" ``` paulson@13140 ` 268` ```apply (rule singleton_prod_bij [THEN ord_isoI]) ``` paulson@13140 ` 269` ```apply (simp (no_asm_simp)) ``` paulson@13140 ` 270` ```apply (blast dest: well_ord_is_wf [THEN wf_on_not_refl]) ``` paulson@13140 ` 271` ```done ``` paulson@13140 ` 272` paulson@13140 ` 273` ```(*Here we build a complicated function term, then simplify it using ``` paulson@13140 ` 274` ``` case_cong, id_conv, comp_lam, case_case.*) ``` paulson@13140 ` 275` ```lemma prod_sum_singleton_bij: ``` paulson@13140 ` 276` ``` "a~:C ==> ``` paulson@13140 ` 277` ``` (lam x:C*B + D. case(%x. x, %y., x)) ``` paulson@13140 ` 278` ``` : bij(C*B + D, C*B Un {a}*D)" ``` paulson@13140 ` 279` ```apply (rule subst_elem) ``` paulson@13140 ` 280` ```apply (rule id_bij [THEN sum_bij, THEN comp_bij]) ``` paulson@13140 ` 281` ```apply (rule singleton_prod_bij) ``` paulson@13140 ` 282` ```apply (rule sum_disjoint_bij) ``` paulson@13140 ` 283` ```apply blast ``` paulson@13140 ` 284` ```apply (simp (no_asm_simp) cong add: case_cong) ``` paulson@13140 ` 285` ```apply (rule comp_lam [THEN trans, symmetric]) ``` paulson@13140 ` 286` ```apply (fast elim!: case_type) ``` paulson@13140 ` 287` ```apply (simp (no_asm_simp) add: case_case) ``` paulson@13140 ` 288` ```done ``` paulson@13140 ` 289` paulson@13140 ` 290` ```lemma prod_sum_singleton_ord_iso: ``` paulson@13140 ` 291` ``` "[| a:A; well_ord(A,r) |] ==> ``` paulson@13140 ` 292` ``` (lam x:pred(A,a,r)*B + pred(B,b,s). case(%x. x, %y., x)) ``` paulson@13140 ` 293` ``` : ord_iso(pred(A,a,r)*B + pred(B,b,s), ``` paulson@13140 ` 294` ``` radd(A*B, rmult(A,r,B,s), B, s), ``` paulson@13140 ` 295` ``` pred(A,a,r)*B Un {a}*pred(B,b,s), rmult(A,r,B,s))" ``` paulson@13140 ` 296` ```apply (rule prod_sum_singleton_bij [THEN ord_isoI]) ``` paulson@13140 ` 297` ```apply (simp (no_asm_simp) add: pred_iff well_ord_is_wf [THEN wf_on_not_refl]) ``` paulson@13140 ` 298` ```apply (auto elim!: well_ord_is_wf [THEN wf_on_asym] predE) ``` paulson@13140 ` 299` ```done ``` paulson@13140 ` 300` paulson@13140 ` 301` ```(** Distributive law **) ``` paulson@13140 ` 302` paulson@13140 ` 303` ```lemma sum_prod_distrib_bij: ``` paulson@13140 ` 304` ``` "(lam :(A+B)*C. case(%y. Inl(), %y. Inr(), x)) ``` paulson@13140 ` 305` ``` : bij((A+B)*C, (A*C)+(B*C))" ``` paulson@13140 ` 306` ```apply (rule_tac d = "case (%., %.) " ``` paulson@13140 ` 307` ``` in lam_bijective) ``` paulson@13140 ` 308` ```apply auto ``` paulson@13140 ` 309` ```done ``` paulson@13140 ` 310` paulson@13140 ` 311` ```lemma sum_prod_distrib_ord_iso: ``` paulson@13140 ` 312` ``` "(lam :(A+B)*C. case(%y. Inl(), %y. Inr(), x)) ``` paulson@13140 ` 313` ``` : ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t), ``` paulson@13140 ` 314` ``` (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))" ``` paulson@13140 ` 315` ```apply (rule sum_prod_distrib_bij [THEN ord_isoI]) ``` paulson@13140 ` 316` ```apply auto ``` paulson@13140 ` 317` ```done ``` paulson@13140 ` 318` paulson@13140 ` 319` ```(** Associativity **) ``` paulson@13140 ` 320` paulson@13140 ` 321` ```lemma prod_assoc_bij: ``` paulson@13140 ` 322` ``` "(lam <, z>:(A*B)*C. >) : bij((A*B)*C, A*(B*C))" ``` paulson@13140 ` 323` ```apply (rule_tac d = "%>. <, z>" in lam_bijective) ``` paulson@13140 ` 324` ```apply auto ``` paulson@13140 ` 325` ```done ``` paulson@13140 ` 326` paulson@13140 ` 327` ```lemma prod_assoc_ord_iso: ``` paulson@13140 ` 328` ``` "(lam <, z>:(A*B)*C. >) ``` paulson@13140 ` 329` ``` : ord_iso((A*B)*C, rmult(A*B, rmult(A,r,B,s), C, t), ``` paulson@13140 ` 330` ``` A*(B*C), rmult(A, r, B*C, rmult(B,s,C,t)))" ``` paulson@13140 ` 331` ```apply (rule prod_assoc_bij [THEN ord_isoI]) ``` paulson@13140 ` 332` ```apply auto ``` paulson@13140 ` 333` ```done ``` paulson@13140 ` 334` paulson@13140 ` 335` ```(**** Inverse image of a relation ****) ``` paulson@13140 ` 336` paulson@13140 ` 337` ```(** Rewrite rule **) ``` paulson@13140 ` 338` paulson@13140 ` 339` ```lemma rvimage_iff: " : rvimage(A,f,r) <-> : r & a:A & b:A" ``` paulson@13140 ` 340` ```apply (unfold rvimage_def) ``` paulson@13140 ` 341` ```apply blast ``` paulson@13140 ` 342` ```done ``` paulson@13140 ` 343` paulson@13140 ` 344` ```(** Type checking **) ``` paulson@13140 ` 345` paulson@13140 ` 346` ```lemma rvimage_type: "rvimage(A,f,r) <= A*A" ``` paulson@13140 ` 347` ```apply (unfold rvimage_def) ``` paulson@13140 ` 348` ```apply (rule Collect_subset) ``` paulson@13140 ` 349` ```done ``` paulson@13140 ` 350` paulson@13140 ` 351` ```lemmas field_rvimage = rvimage_type [THEN field_rel_subset] ``` paulson@13140 ` 352` paulson@13140 ` 353` ```lemma rvimage_converse: "rvimage(A,f, converse(r)) = converse(rvimage(A,f,r))" ``` paulson@13140 ` 354` ```apply (unfold rvimage_def) ``` paulson@13140 ` 355` ```apply blast ``` paulson@13140 ` 356` ```done ``` paulson@13140 ` 357` paulson@13140 ` 358` paulson@13140 ` 359` ```(** Partial Ordering Properties **) ``` paulson@13140 ` 360` paulson@13140 ` 361` ```lemma irrefl_rvimage: ``` paulson@13140 ` 362` ``` "[| f: inj(A,B); irrefl(B,r) |] ==> irrefl(A, rvimage(A,f,r))" ``` paulson@13140 ` 363` ```apply (unfold irrefl_def rvimage_def) ``` paulson@13140 ` 364` ```apply (blast intro: inj_is_fun [THEN apply_type]) ``` paulson@13140 ` 365` ```done ``` paulson@13140 ` 366` paulson@13140 ` 367` ```lemma trans_on_rvimage: ``` paulson@13140 ` 368` ``` "[| f: inj(A,B); trans[B](r) |] ==> trans[A](rvimage(A,f,r))" ``` paulson@13140 ` 369` ```apply (unfold trans_on_def rvimage_def) ``` paulson@13140 ` 370` ```apply (blast intro: inj_is_fun [THEN apply_type]) ``` paulson@13140 ` 371` ```done ``` paulson@13140 ` 372` paulson@13140 ` 373` ```lemma part_ord_rvimage: ``` paulson@13140 ` 374` ``` "[| f: inj(A,B); part_ord(B,r) |] ==> part_ord(A, rvimage(A,f,r))" ``` paulson@13140 ` 375` ```apply (unfold part_ord_def) ``` paulson@13140 ` 376` ```apply (blast intro!: irrefl_rvimage trans_on_rvimage) ``` paulson@13140 ` 377` ```done ``` paulson@13140 ` 378` paulson@13140 ` 379` ```(** Linearity **) ``` paulson@13140 ` 380` paulson@13140 ` 381` ```lemma linear_rvimage: ``` paulson@13140 ` 382` ``` "[| f: inj(A,B); linear(B,r) |] ==> linear(A,rvimage(A,f,r))" ``` paulson@13140 ` 383` ```apply (simp add: inj_def linear_def rvimage_iff) ``` paulson@13140 ` 384` ```apply (blast intro: apply_funtype); ``` paulson@13140 ` 385` ```done ``` paulson@13140 ` 386` paulson@13140 ` 387` ```lemma tot_ord_rvimage: ``` paulson@13140 ` 388` ``` "[| f: inj(A,B); tot_ord(B,r) |] ==> tot_ord(A, rvimage(A,f,r))" ``` paulson@13140 ` 389` ```apply (unfold tot_ord_def) ``` paulson@13140 ` 390` ```apply (blast intro!: part_ord_rvimage linear_rvimage) ``` paulson@13140 ` 391` ```done ``` paulson@13140 ` 392` paulson@13140 ` 393` paulson@13140 ` 394` ```(** Well-foundedness **) ``` paulson@13140 ` 395` paulson@13140 ` 396` ```(*Not sure if wf_on_rvimage could be proved from this!*) ``` paulson@13140 ` 397` ```lemma wf_rvimage [intro!]: "wf(r) ==> wf(rvimage(A,f,r))" ``` paulson@13140 ` 398` ```apply (simp (no_asm_use) add: rvimage_def wf_eq_minimal) ``` paulson@13140 ` 399` ```apply clarify ``` paulson@13140 ` 400` ```apply (subgoal_tac "EX w. w : {w: {f`x. x:Q}. EX x. x: Q & (f`x = w) }") ``` paulson@13140 ` 401` ``` apply (erule allE) ``` paulson@13140 ` 402` ``` apply (erule impE) ``` paulson@13140 ` 403` ``` apply assumption; ``` paulson@13140 ` 404` ``` apply blast ``` paulson@13140 ` 405` ```apply (blast intro: elim:); ``` paulson@13140 ` 406` ```done ``` paulson@13140 ` 407` paulson@13140 ` 408` ```lemma wf_on_rvimage: "[| f: A->B; wf[B](r) |] ==> wf[A](rvimage(A,f,r))" ``` paulson@13140 ` 409` ```apply (rule wf_onI2) ``` paulson@13140 ` 410` ```apply (subgoal_tac "ALL z:A. f`z=f`y --> z: Ba") ``` paulson@13140 ` 411` ``` apply blast ``` paulson@13140 ` 412` ```apply (erule_tac a = "f`y" in wf_on_induct) ``` paulson@13140 ` 413` ``` apply (blast intro!: apply_funtype) ``` paulson@13140 ` 414` ```apply (blast intro!: apply_funtype dest!: rvimage_iff [THEN iffD1]) ``` paulson@13140 ` 415` ```done ``` paulson@13140 ` 416` paulson@13140 ` 417` ```(*Note that we need only wf[A](...) and linear(A,...) to get the result!*) ``` paulson@13140 ` 418` ```lemma well_ord_rvimage: ``` paulson@13140 ` 419` ``` "[| f: inj(A,B); well_ord(B,r) |] ==> well_ord(A, rvimage(A,f,r))" ``` paulson@13140 ` 420` ```apply (rule well_ordI) ``` paulson@13140 ` 421` ```apply (unfold well_ord_def tot_ord_def) ``` paulson@13140 ` 422` ```apply (blast intro!: wf_on_rvimage inj_is_fun) ``` paulson@13140 ` 423` ```apply (blast intro!: linear_rvimage) ``` paulson@13140 ` 424` ```done ``` paulson@13140 ` 425` paulson@13140 ` 426` ```lemma ord_iso_rvimage: ``` paulson@13140 ` 427` ``` "f: bij(A,B) ==> f: ord_iso(A, rvimage(A,f,s), B, s)" ``` paulson@13140 ` 428` ```apply (unfold ord_iso_def) ``` paulson@13140 ` 429` ```apply (simp add: rvimage_iff) ``` paulson@13140 ` 430` ```done ``` paulson@13140 ` 431` paulson@13140 ` 432` ```lemma ord_iso_rvimage_eq: ``` paulson@13140 ` 433` ``` "f: ord_iso(A,r, B,s) ==> rvimage(A,f,s) = r Int A*A" ``` paulson@13140 ` 434` ```apply (unfold ord_iso_def rvimage_def) ``` paulson@13140 ` 435` ```apply blast ``` paulson@13140 ` 436` ```done ``` paulson@13140 ` 437` paulson@13140 ` 438` paulson@13140 ` 439` ```(** The "measure" relation is useful with wfrec **) ``` paulson@13140 ` 440` paulson@13140 ` 441` ```lemma measure_eq_rvimage_Memrel: ``` paulson@13140 ` 442` ``` "measure(A,f) = rvimage(A,Lambda(A,f),Memrel(Collect(RepFun(A,f),Ord)))" ``` paulson@13140 ` 443` ```apply (simp (no_asm) add: measure_def rvimage_def Memrel_iff) ``` paulson@13140 ` 444` ```apply (rule equalityI) ``` paulson@13140 ` 445` ```apply auto ``` paulson@13140 ` 446` ```apply (auto intro: Ord_in_Ord simp add: lt_def) ``` paulson@13140 ` 447` ```done ``` paulson@13140 ` 448` paulson@13140 ` 449` ```lemma wf_measure [iff]: "wf(measure(A,f))" ``` paulson@13140 ` 450` ```apply (simp (no_asm) add: measure_eq_rvimage_Memrel wf_Memrel wf_rvimage) ``` paulson@13140 ` 451` ```done ``` paulson@13140 ` 452` paulson@13140 ` 453` ```lemma measure_iff [iff]: " : measure(A,f) <-> x:A & y:A & f(x)