1(* Title: ZF/WF.thy 2 Author: Tobias Nipkow and Lawrence C Paulson 3 Copyright 1994 University of Cambridge 4 5Derived first for transitive relations, and finally for arbitrary WF relations 6via wf_trancl and trans_trancl. 7 8It is difficult to derive this general case directly, using r^+ instead of 9r. In is_recfun, the two occurrences of the relation must have the same 10form. Inserting r^+ in the_recfun or wftrec yields a recursion rule with 11r^+ -`` {a} instead of r-``{a}. This recursion rule is stronger in 12principle, but harder to use, especially to prove wfrec_eclose_eq in 13epsilon.ML. Expanding out the definition of wftrec in wfrec would yield 14a mess. 15*) 16 17section\<open>Well-Founded Recursion\<close> 18 19theory WF imports Trancl begin 20 21definition 22 wf :: "i=>o" where 23 (*r is a well-founded relation*) 24 "wf(r) == \<forall>Z. Z=0 | (\<exists>x\<in>Z. \<forall>y. <y,x>:r \<longrightarrow> ~ y \<in> Z)" 25 26definition 27 wf_on :: "[i,i]=>o" (\<open>wf[_]'(_')\<close>) where 28 (*r is well-founded on A*) 29 "wf_on(A,r) == wf(r \<inter> A*A)" 30 31definition 32 is_recfun :: "[i, i, [i,i]=>i, i] =>o" where 33 "is_recfun(r,a,H,f) == (f = (\<lambda>x\<in>r-``{a}. H(x, restrict(f, r-``{x}))))" 34 35definition 36 the_recfun :: "[i, i, [i,i]=>i] =>i" where 37 "the_recfun(r,a,H) == (THE f. is_recfun(r,a,H,f))" 38 39definition 40 wftrec :: "[i, i, [i,i]=>i] =>i" where 41 "wftrec(r,a,H) == H(a, the_recfun(r,a,H))" 42 43definition 44 wfrec :: "[i, i, [i,i]=>i] =>i" where 45 (*public version. Does not require r to be transitive*) 46 "wfrec(r,a,H) == wftrec(r^+, a, %x f. H(x, restrict(f,r-``{x})))" 47 48definition 49 wfrec_on :: "[i, i, i, [i,i]=>i] =>i" (\<open>wfrec[_]'(_,_,_')\<close>) where 50 "wfrec[A](r,a,H) == wfrec(r \<inter> A*A, a, H)" 51 52 53subsection\<open>Well-Founded Relations\<close> 54 55subsubsection\<open>Equivalences between \<^term>\<open>wf\<close> and \<^term>\<open>wf_on\<close>\<close> 56 57lemma wf_imp_wf_on: "wf(r) ==> wf[A](r)" 58by (unfold wf_def wf_on_def, force) 59 60lemma wf_on_imp_wf: "[|wf[A](r); r \<subseteq> A*A|] ==> wf(r)" 61by (simp add: wf_on_def subset_Int_iff) 62 63lemma wf_on_field_imp_wf: "wf[field(r)](r) ==> wf(r)" 64by (unfold wf_def wf_on_def, fast) 65 66lemma wf_iff_wf_on_field: "wf(r) \<longleftrightarrow> wf[field(r)](r)" 67by (blast intro: wf_imp_wf_on wf_on_field_imp_wf) 68 69lemma wf_on_subset_A: "[| wf[A](r); B<=A |] ==> wf[B](r)" 70by (unfold wf_on_def wf_def, fast) 71 72lemma wf_on_subset_r: "[| wf[A](r); s<=r |] ==> wf[A](s)" 73by (unfold wf_on_def wf_def, fast) 74 75lemma wf_subset: "[|wf(s); r<=s|] ==> wf(r)" 76by (simp add: wf_def, fast) 77 78subsubsection\<open>Introduction Rules for \<^term>\<open>wf_on\<close>\<close> 79 80text\<open>If every non-empty subset of \<^term>\<open>A\<close> has an \<^term>\<open>r\<close>-minimal element 81 then we have \<^term>\<open>wf[A](r)\<close>.\<close> 82lemma wf_onI: 83 assumes prem: "!!Z u. [| Z<=A; u \<in> Z; \<forall>x\<in>Z. \<exists>y\<in>Z. <y,x>:r |] ==> False" 84 shows "wf[A](r)" 85apply (unfold wf_on_def wf_def) 86apply (rule equals0I [THEN disjCI, THEN allI]) 87apply (rule_tac Z = Z in prem, blast+) 88done 89 90text\<open>If \<^term>\<open>r\<close> allows well-founded induction over \<^term>\<open>A\<close> 91 then we have \<^term>\<open>wf[A](r)\<close>. Premise is equivalent to 92 \<^prop>\<open>!!B. \<forall>x\<in>A. (\<forall>y. <y,x>: r \<longrightarrow> y \<in> B) \<longrightarrow> x \<in> B ==> A<=B\<close>\<close> 93lemma wf_onI2: 94 assumes prem: "!!y B. [| \<forall>x\<in>A. (\<forall>y\<in>A. <y,x>:r \<longrightarrow> y \<in> B) \<longrightarrow> x \<in> B; y \<in> A |] 95 ==> y \<in> B" 96 shows "wf[A](r)" 97apply (rule wf_onI) 98apply (rule_tac c=u in prem [THEN DiffE]) 99 prefer 3 apply blast 100 apply fast+ 101done 102 103 104subsubsection\<open>Well-founded Induction\<close> 105 106text\<open>Consider the least \<^term>\<open>z\<close> in \<^term>\<open>domain(r)\<close> such that 107 \<^term>\<open>P(z)\<close> does not hold...\<close> 108lemma wf_induct_raw: 109 "[| wf(r); 110 !!x.[| \<forall>y. <y,x>: r \<longrightarrow> P(y) |] ==> P(x) |] 111 ==> P(a)" 112apply (unfold wf_def) 113apply (erule_tac x = "{z \<in> domain(r). ~ P(z)}" in allE) 114apply blast 115done 116 117lemmas wf_induct = wf_induct_raw [rule_format, consumes 1, case_names step, induct set: wf] 118 119text\<open>The form of this rule is designed to match \<open>wfI\<close>\<close> 120lemma wf_induct2: 121 "[| wf(r); a \<in> A; field(r)<=A; 122 !!x.[| x \<in> A; \<forall>y. <y,x>: r \<longrightarrow> P(y) |] ==> P(x) |] 123 ==> P(a)" 124apply (erule_tac P="a \<in> A" in rev_mp) 125apply (erule_tac a=a in wf_induct, blast) 126done 127 128lemma field_Int_square: "field(r \<inter> A*A) \<subseteq> A" 129by blast 130 131lemma wf_on_induct_raw [consumes 2, induct set: wf_on]: 132 "[| wf[A](r); a \<in> A; 133 !!x.[| x \<in> A; \<forall>y\<in>A. <y,x>: r \<longrightarrow> P(y) |] ==> P(x) 134 |] ==> P(a)" 135apply (unfold wf_on_def) 136apply (erule wf_induct2, assumption) 137apply (rule field_Int_square, blast) 138done 139 140lemma wf_on_induct [consumes 2, case_names step, induct set: wf_on]: 141 "wf[A](r) \<Longrightarrow> a \<in> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> (\<And>y. y \<in> A \<Longrightarrow> \<langle>y, x\<rangle> \<in> r \<Longrightarrow> P(y)) \<Longrightarrow> P(x)) \<Longrightarrow> P(a)" 142 using wf_on_induct_raw [of A r a P] by simp 143 144text\<open>If \<^term>\<open>r\<close> allows well-founded induction 145 then we have \<^term>\<open>wf(r)\<close>.\<close> 146lemma wfI: 147 "[| field(r)<=A; 148 !!y B. [| \<forall>x\<in>A. (\<forall>y\<in>A. <y,x>:r \<longrightarrow> y \<in> B) \<longrightarrow> x \<in> B; y \<in> A|] 149 ==> y \<in> B |] 150 ==> wf(r)" 151apply (rule wf_on_subset_A [THEN wf_on_field_imp_wf]) 152apply (rule wf_onI2) 153 prefer 2 apply blast 154apply blast 155done 156 157 158subsection\<open>Basic Properties of Well-Founded Relations\<close> 159 160lemma wf_not_refl: "wf(r) ==> <a,a> \<notin> r" 161by (erule_tac a=a in wf_induct, blast) 162 163lemma wf_not_sym [rule_format]: "wf(r) ==> \<forall>x. <a,x>:r \<longrightarrow> <x,a> \<notin> r" 164by (erule_tac a=a in wf_induct, blast) 165 166(* @{term"[| wf(r); <a,x> \<in> r; ~P ==> <x,a> \<in> r |] ==> P"} *) 167lemmas wf_asym = wf_not_sym [THEN swap] 168 169lemma wf_on_not_refl: "[| wf[A](r); a \<in> A |] ==> <a,a> \<notin> r" 170by (erule_tac a=a in wf_on_induct, assumption, blast) 171 172lemma wf_on_not_sym: 173 "[| wf[A](r); a \<in> A |] ==> (\<And>b. b\<in>A \<Longrightarrow> <a,b>:r \<Longrightarrow> <b,a>\<notin>r)" 174apply (atomize (full), intro impI) 175apply (erule_tac a=a in wf_on_induct, assumption, blast) 176done 177 178lemma wf_on_asym: 179 "[| wf[A](r); ~Z ==> <a,b> \<in> r; 180 <b,a> \<notin> r ==> Z; ~Z ==> a \<in> A; ~Z ==> b \<in> A |] ==> Z" 181by (blast dest: wf_on_not_sym) 182 183 184(*Needed to prove well_ordI. Could also reason that wf[A](r) means 185 wf(r \<inter> A*A); thus wf( (r \<inter> A*A)^+ ) and use wf_not_refl *) 186lemma wf_on_chain3: 187 "[| wf[A](r); <a,b>:r; <b,c>:r; <c,a>:r; a \<in> A; b \<in> A; c \<in> A |] ==> P" 188apply (subgoal_tac "\<forall>y\<in>A. \<forall>z\<in>A. <a,y>:r \<longrightarrow> <y,z>:r \<longrightarrow> <z,a>:r \<longrightarrow> P", 189 blast) 190apply (erule_tac a=a in wf_on_induct, assumption, blast) 191done 192 193 194 195text\<open>transitive closure of a WF relation is WF provided 196 \<^term>\<open>A\<close> is downward closed\<close> 197lemma wf_on_trancl: 198 "[| wf[A](r); r-``A \<subseteq> A |] ==> wf[A](r^+)" 199apply (rule wf_onI2) 200apply (frule bspec [THEN mp], assumption+) 201apply (erule_tac a = y in wf_on_induct, assumption) 202apply (blast elim: tranclE, blast) 203done 204 205lemma wf_trancl: "wf(r) ==> wf(r^+)" 206apply (simp add: wf_iff_wf_on_field) 207apply (rule wf_on_subset_A) 208 apply (erule wf_on_trancl) 209 apply blast 210apply (rule trancl_type [THEN field_rel_subset]) 211done 212 213 214text\<open>\<^term>\<open>r-``{a}\<close> is the set of everything under \<^term>\<open>a\<close> in \<^term>\<open>r\<close>\<close> 215 216lemmas underI = vimage_singleton_iff [THEN iffD2] 217lemmas underD = vimage_singleton_iff [THEN iffD1] 218 219 220subsection\<open>The Predicate \<^term>\<open>is_recfun\<close>\<close> 221 222lemma is_recfun_type: "is_recfun(r,a,H,f) ==> f \<in> r-``{a} -> range(f)" 223apply (unfold is_recfun_def) 224apply (erule ssubst) 225apply (rule lamI [THEN rangeI, THEN lam_type], assumption) 226done 227 228lemmas is_recfun_imp_function = is_recfun_type [THEN fun_is_function] 229 230lemma apply_recfun: 231 "[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))" 232apply (unfold is_recfun_def) 233 txt\<open>replace f only on the left-hand side\<close> 234apply (erule_tac P = "%x. t(x) = u" for t u in ssubst) 235apply (simp add: underI) 236done 237 238lemma is_recfun_equal [rule_format]: 239 "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,b,H,g) |] 240 ==> <x,a>:r \<longrightarrow> <x,b>:r \<longrightarrow> f`x=g`x" 241apply (frule_tac f = f in is_recfun_type) 242apply (frule_tac f = g in is_recfun_type) 243apply (simp add: is_recfun_def) 244apply (erule_tac a=x in wf_induct) 245apply (intro impI) 246apply (elim ssubst) 247apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def) 248apply (rule_tac t = "%z. H (x, z)" for x in subst_context) 249apply (subgoal_tac "\<forall>y\<in>r-``{x}. \<forall>z. <y,z>:f \<longleftrightarrow> <y,z>:g") 250 apply (blast dest: transD) 251apply (simp add: apply_iff) 252apply (blast dest: transD intro: sym) 253done 254 255lemma is_recfun_cut: 256 "[| wf(r); trans(r); 257 is_recfun(r,a,H,f); is_recfun(r,b,H,g); <b,a>:r |] 258 ==> restrict(f, r-``{b}) = g" 259apply (frule_tac f = f in is_recfun_type) 260apply (rule fun_extension) 261 apply (blast dest: transD intro: restrict_type2) 262 apply (erule is_recfun_type, simp) 263apply (blast dest: transD intro: is_recfun_equal) 264done 265 266subsection\<open>Recursion: Main Existence Lemma\<close> 267 268lemma is_recfun_functional: 269 "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |] ==> f=g" 270by (blast intro: fun_extension is_recfun_type is_recfun_equal) 271 272lemma the_recfun_eq: 273 "[| is_recfun(r,a,H,f); wf(r); trans(r) |] ==> the_recfun(r,a,H) = f" 274apply (unfold the_recfun_def) 275apply (blast intro: is_recfun_functional) 276done 277 278(*If some f satisfies is_recfun(r,a,H,-) then so does the_recfun(r,a,H) *) 279lemma is_the_recfun: 280 "[| is_recfun(r,a,H,f); wf(r); trans(r) |] 281 ==> is_recfun(r, a, H, the_recfun(r,a,H))" 282by (simp add: the_recfun_eq) 283 284lemma unfold_the_recfun: 285 "[| wf(r); trans(r) |] ==> is_recfun(r, a, H, the_recfun(r,a,H))" 286apply (rule_tac a=a in wf_induct, assumption) 287apply (rename_tac a1) 288apply (rule_tac f = "\<lambda>y\<in>r-``{a1}. wftrec (r,y,H)" in is_the_recfun) 289 apply typecheck 290apply (unfold is_recfun_def wftrec_def) 291 \<comment> \<open>Applying the substitution: must keep the quantified assumption!\<close> 292apply (rule lam_cong [OF refl]) 293apply (drule underD) 294apply (fold is_recfun_def) 295apply (rule_tac t = "%z. H(x, z)" for x in subst_context) 296apply (rule fun_extension) 297 apply (blast intro: is_recfun_type) 298 apply (rule lam_type [THEN restrict_type2]) 299 apply blast 300 apply (blast dest: transD) 301apply atomize 302apply (frule spec [THEN mp], assumption) 303apply (subgoal_tac "<xa,a1> \<in> r") 304 apply (drule_tac x1 = xa in spec [THEN mp], assumption) 305apply (simp add: vimage_singleton_iff 306 apply_recfun is_recfun_cut) 307apply (blast dest: transD) 308done 309 310 311subsection\<open>Unfolding \<^term>\<open>wftrec(r,a,H)\<close>\<close> 312 313lemma the_recfun_cut: 314 "[| wf(r); trans(r); <b,a>:r |] 315 ==> restrict(the_recfun(r,a,H), r-``{b}) = the_recfun(r,b,H)" 316by (blast intro: is_recfun_cut unfold_the_recfun) 317 318(*NOT SUITABLE FOR REWRITING: it is recursive!*) 319lemma wftrec: 320 "[| wf(r); trans(r) |] ==> 321 wftrec(r,a,H) = H(a, \<lambda>x\<in>r-``{a}. wftrec(r,x,H))" 322apply (unfold wftrec_def) 323apply (subst unfold_the_recfun [unfolded is_recfun_def]) 324apply (simp_all add: vimage_singleton_iff [THEN iff_sym] the_recfun_cut) 325done 326 327 328subsubsection\<open>Removal of the Premise \<^term>\<open>trans(r)\<close>\<close> 329 330(*NOT SUITABLE FOR REWRITING: it is recursive!*) 331lemma wfrec: 332 "wf(r) ==> wfrec(r,a,H) = H(a, \<lambda>x\<in>r-``{a}. wfrec(r,x,H))" 333apply (unfold wfrec_def) 334apply (erule wf_trancl [THEN wftrec, THEN ssubst]) 335 apply (rule trans_trancl) 336apply (rule vimage_pair_mono [THEN restrict_lam_eq, THEN subst_context]) 337 apply (erule r_into_trancl) 338apply (rule subset_refl) 339done 340 341(*This form avoids giant explosions in proofs. NOTE USE OF == *) 342lemma def_wfrec: 343 "[| !!x. h(x)==wfrec(r,x,H); wf(r) |] ==> 344 h(a) = H(a, \<lambda>x\<in>r-``{a}. h(x))" 345apply simp 346apply (elim wfrec) 347done 348 349lemma wfrec_type: 350 "[| wf(r); a \<in> A; field(r)<=A; 351 !!x u. [| x \<in> A; u \<in> Pi(r-``{x}, B) |] ==> H(x,u) \<in> B(x) 352 |] ==> wfrec(r,a,H) \<in> B(a)" 353apply (rule_tac a = a in wf_induct2, assumption+) 354apply (subst wfrec, assumption) 355apply (simp add: lam_type underD) 356done 357 358 359lemma wfrec_on: 360 "[| wf[A](r); a \<in> A |] ==> 361 wfrec[A](r,a,H) = H(a, \<lambda>x\<in>(r-``{a}) \<inter> A. wfrec[A](r,x,H))" 362apply (unfold wf_on_def wfrec_on_def) 363apply (erule wfrec [THEN trans]) 364apply (simp add: vimage_Int_square cons_subset_iff) 365done 366 367text\<open>Minimal-element characterization of well-foundedness\<close> 368lemma wf_eq_minimal: 369 "wf(r) \<longleftrightarrow> (\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. <y,z>:r \<longrightarrow> y\<notin>Q))" 370by (unfold wf_def, blast) 371 372end 373