src/HOL/Wellfounded_Relations.thy
 author krauss Mon Jun 05 14:22:58 2006 +0200 (2006-06-05) changeset 19769 c40ce2de2020 parent 19623 12e6cc4382ae child 22261 9e185f78e7d4 permissions -rw-r--r--
Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure".
This simplifies some proofs.
 paulson@15346 ` 1` ```(* ID: \$Id\$ ``` nipkow@10213 ` 2` ``` Author: Konrad Slind ``` nipkow@10213 ` 3` ``` Copyright 1995 TU Munich ``` nipkow@10213 ` 4` ```*) ``` nipkow@10213 ` 5` paulson@15346 ` 6` ```header {*Well-founded Relations*} ``` paulson@15346 ` 7` paulson@15346 ` 8` ```theory Wellfounded_Relations ``` paulson@15346 ` 9` ```imports Finite_Set ``` paulson@15346 ` 10` ```begin ``` paulson@15346 ` 11` paulson@15346 ` 12` ```text{*Derived WF relations such as inverse image, lexicographic product and ``` paulson@15346 ` 13` ```measure. The simple relational product, in which @{term "(x',y')"} precedes ``` paulson@15346 ` 14` ```@{term "(x,y)"} if @{term "x' nat) => ('a * 'a)set" ``` paulson@15346 ` 22` ``` "measure == inv_image less_than" ``` nipkow@10213 ` 23` nipkow@10213 ` 24` ``` lex_prod :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" ``` nipkow@10213 ` 25` ``` (infixr "<*lex*>" 80) ``` paulson@15346 ` 26` ``` "ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra | a=a' & (b,b') : rb}" ``` paulson@15346 ` 27` paulson@15346 ` 28` ``` finite_psubset :: "('a set * 'a set) set" ``` paulson@15346 ` 29` ``` --{* finite proper subset*} ``` paulson@15346 ` 30` ``` "finite_psubset == {(A,B). A < B & finite B}" ``` paulson@15346 ` 31` paulson@15346 ` 32` ``` same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set" ``` paulson@15346 ` 33` ``` "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}" ``` paulson@15346 ` 34` ``` --{*For @{text rec_def} declarations where the first n parameters ``` paulson@15346 ` 35` ``` stay unchanged in the recursive call. ``` paulson@15346 ` 36` ``` See @{text "Library/While_Combinator.thy"} for an application.*} ``` paulson@15346 ` 37` paulson@15346 ` 38` paulson@15346 ` 39` paulson@15346 ` 40` paulson@15346 ` 41` ```subsection{*Measure Functions make Wellfounded Relations*} ``` paulson@15346 ` 42` paulson@15346 ` 43` ```subsubsection{*`Less than' on the natural numbers*} ``` paulson@15346 ` 44` paulson@15346 ` 45` ```lemma wf_less_than [iff]: "wf less_than" ``` paulson@15346 ` 46` ```by (simp add: less_than_def wf_pred_nat [THEN wf_trancl]) ``` paulson@15346 ` 47` paulson@15346 ` 48` ```lemma trans_less_than [iff]: "trans less_than" ``` paulson@15346 ` 49` ```by (simp add: less_than_def trans_trancl) ``` paulson@15346 ` 50` paulson@15346 ` 51` ```lemma less_than_iff [iff]: "((x,y): less_than) = (x P m) ==> P n)" ``` paulson@15346 ` 56` ``` shows "P n" ``` paulson@15346 ` 57` ```apply (rule wf_less_than [THEN wf_induct]) ``` paulson@15346 ` 58` ```apply (rule ih, auto) ``` paulson@15346 ` 59` ```done ``` paulson@15346 ` 60` paulson@15346 ` 61` ```subsubsection{*The Inverse Image into a Wellfounded Relation is Wellfounded.*} ``` paulson@15346 ` 62` paulson@15346 ` 63` ```lemma wf_inv_image [simp,intro!]: "wf(r) ==> wf(inv_image r (f::'a=>'b))" ``` paulson@15346 ` 64` ```apply (simp (no_asm_use) add: inv_image_def wf_eq_minimal) ``` paulson@15346 ` 65` ```apply clarify ``` paulson@15346 ` 66` ```apply (subgoal_tac "EX (w::'b) . w : {w. EX (x::'a) . x: Q & (f x = w) }") ``` paulson@15346 ` 67` ```prefer 2 apply (blast del: allE) ``` paulson@15346 ` 68` ```apply (erule allE) ``` paulson@15346 ` 69` ```apply (erule (1) notE impE) ``` paulson@15346 ` 70` ```apply blast ``` paulson@15346 ` 71` ```done ``` nipkow@10213 ` 72` krauss@19769 ` 73` ```lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)" ``` krauss@19769 ` 74` ``` by (auto simp:inv_image_def) ``` paulson@15346 ` 75` paulson@15346 ` 76` ```subsubsection{*Finally, All Measures are Wellfounded.*} ``` paulson@15346 ` 77` nipkow@19623 ` 78` ```lemma in_measure[simp]: "((x,y) : measure f) = (f x < f y)" ``` krauss@19769 ` 79` ``` by (simp add:measure_def) ``` nipkow@19623 ` 80` paulson@15346 ` 81` ```lemma wf_measure [iff]: "wf (measure f)" ``` paulson@15346 ` 82` ```apply (unfold measure_def) ``` paulson@15346 ` 83` ```apply (rule wf_less_than [THEN wf_inv_image]) ``` paulson@15346 ` 84` ```done ``` paulson@15346 ` 85` wenzelm@18277 ` 86` ```lemma measure_induct_rule [case_names less]: ``` wenzelm@18277 ` 87` ``` fixes f :: "'a \ nat" ``` wenzelm@18277 ` 88` ``` assumes step: "\x. (\y. f y < f x \ P y) \ P x" ``` wenzelm@18277 ` 89` ``` shows "P a" ``` wenzelm@18277 ` 90` ```proof - ``` wenzelm@18277 ` 91` ``` have "wf (measure f)" .. ``` wenzelm@18277 ` 92` ``` then show ?thesis ``` wenzelm@18277 ` 93` ``` proof induct ``` wenzelm@18277 ` 94` ``` case (less x) ``` wenzelm@18277 ` 95` ``` show ?case ``` wenzelm@18277 ` 96` ``` proof (rule step) ``` wenzelm@18277 ` 97` ``` fix y ``` wenzelm@18277 ` 98` ``` assume "f y < f x" ``` nipkow@19623 ` 99` ``` hence "(y, x) \ measure f" by simp ``` nipkow@19623 ` 100` ``` thus "P y" by (rule less) ``` wenzelm@18277 ` 101` ``` qed ``` wenzelm@18277 ` 102` ``` qed ``` wenzelm@18277 ` 103` ```qed ``` wenzelm@18277 ` 104` wenzelm@18277 ` 105` ```lemma measure_induct: ``` wenzelm@18277 ` 106` ``` fixes f :: "'a \ nat" ``` wenzelm@18277 ` 107` ``` shows "(\x. \y. f y < f x \ P y \ P x) \ P a" ``` wenzelm@18277 ` 108` ``` by (rule measure_induct_rule [of f P a]) iprover ``` paulson@15346 ` 109` paulson@15346 ` 110` paulson@15346 ` 111` ```subsection{*Other Ways of Constructing Wellfounded Relations*} ``` paulson@15346 ` 112` paulson@15346 ` 113` ```text{*Wellfoundedness of lexicographic combinations*} ``` paulson@15346 ` 114` ```lemma wf_lex_prod [intro!]: "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)" ``` paulson@15346 ` 115` ```apply (unfold wf_def lex_prod_def) ``` paulson@15346 ` 116` ```apply (rule allI, rule impI) ``` paulson@15346 ` 117` ```apply (simp (no_asm_use) only: split_paired_All) ``` paulson@15346 ` 118` ```apply (drule spec, erule mp) ``` paulson@15346 ` 119` ```apply (rule allI, rule impI) ``` paulson@15346 ` 120` ```apply (drule spec, erule mp, blast) ``` paulson@15346 ` 121` ```done ``` paulson@15346 ` 122` krauss@19769 ` 123` ```lemma in_lex_prod[simp]: ``` krauss@19769 ` 124` ``` "(((a,b),(a',b')): r <*lex*> s) = ((a,a'): r \ (a = a' \ (b, b') : s))" ``` krauss@19769 ` 125` ``` by (auto simp:lex_prod_def) ``` krauss@19769 ` 126` paulson@15346 ` 127` ```text{*Transitivity of WF combinators.*} ``` paulson@15346 ` 128` ```lemma trans_lex_prod [intro!]: ``` paulson@15346 ` 129` ``` "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)" ``` paulson@15346 ` 130` ```by (unfold trans_def lex_prod_def, blast) ``` paulson@15346 ` 131` paulson@15346 ` 132` ```subsubsection{*Wellfoundedness of proper subset on finite sets.*} ``` paulson@15346 ` 133` ```lemma wf_finite_psubset: "wf(finite_psubset)" ``` paulson@15346 ` 134` ```apply (unfold finite_psubset_def) ``` paulson@15346 ` 135` ```apply (rule wf_measure [THEN wf_subset]) ``` paulson@15346 ` 136` ```apply (simp add: measure_def inv_image_def less_than_def less_def [symmetric]) ``` paulson@15346 ` 137` ```apply (fast elim!: psubset_card_mono) ``` paulson@15346 ` 138` ```done ``` paulson@15346 ` 139` paulson@15346 ` 140` ```lemma trans_finite_psubset: "trans finite_psubset" ``` paulson@15346 ` 141` ```by (simp add: finite_psubset_def psubset_def trans_def, blast) ``` paulson@15346 ` 142` paulson@15346 ` 143` paulson@15346 ` 144` ```subsubsection{*Wellfoundedness of finite acyclic relations*} ``` paulson@15346 ` 145` paulson@15346 ` 146` ```text{*This proof belongs in this theory because it needs Finite.*} ``` nipkow@10213 ` 147` paulson@15346 ` 148` ```lemma finite_acyclic_wf [rule_format]: "finite r ==> acyclic r --> wf r" ``` paulson@15346 ` 149` ```apply (erule finite_induct, blast) ``` paulson@15346 ` 150` ```apply (simp (no_asm_simp) only: split_tupled_all) ``` paulson@15346 ` 151` ```apply simp ``` paulson@15346 ` 152` ```done ``` paulson@15346 ` 153` paulson@15346 ` 154` ```lemma finite_acyclic_wf_converse: "[|finite r; acyclic r|] ==> wf (r^-1)" ``` paulson@15346 ` 155` ```apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf]) ``` paulson@15346 ` 156` ```apply (erule acyclic_converse [THEN iffD2]) ``` paulson@15346 ` 157` ```done ``` paulson@15346 ` 158` paulson@15346 ` 159` ```lemma wf_iff_acyclic_if_finite: "finite r ==> wf r = acyclic r" ``` paulson@15346 ` 160` ```by (blast intro: finite_acyclic_wf wf_acyclic) ``` paulson@15346 ` 161` paulson@15346 ` 162` paulson@15352 ` 163` ```subsubsection{*Wellfoundedness of @{term same_fst}*} ``` paulson@15346 ` 164` paulson@15346 ` 165` ```lemma same_fstI [intro!]: ``` paulson@15346 ` 166` ``` "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R" ``` paulson@15346 ` 167` ```by (simp add: same_fst_def) ``` paulson@15346 ` 168` paulson@15346 ` 169` ```lemma wf_same_fst: ``` paulson@15346 ` 170` ``` assumes prem: "(!!x. P x ==> wf(R x))" ``` paulson@15346 ` 171` ``` shows "wf(same_fst P R)" ``` paulson@15346 ` 172` ```apply (simp cong del: imp_cong add: wf_def same_fst_def) ``` paulson@15346 ` 173` ```apply (intro strip) ``` paulson@15346 ` 174` ```apply (rename_tac a b) ``` paulson@15346 ` 175` ```apply (case_tac "wf (R a)") ``` paulson@15346 ` 176` ``` apply (erule_tac a = b in wf_induct, blast) ``` paulson@15346 ` 177` ```apply (blast intro: prem) ``` paulson@15346 ` 178` ```done ``` paulson@15346 ` 179` paulson@15346 ` 180` paulson@15346 ` 181` ```subsection{*Weakly decreasing sequences (w.r.t. some well-founded order) ``` paulson@15346 ` 182` ``` stabilize.*} ``` paulson@15346 ` 183` paulson@15346 ` 184` ```text{*This material does not appear to be used any longer.*} ``` paulson@15346 ` 185` paulson@15346 ` 186` ```lemma lemma1: "[| ALL i. (f (Suc i), f i) : r^* |] ==> (f (i+k), f i) : r^*" ``` paulson@15346 ` 187` ```apply (induct_tac "k", simp_all) ``` paulson@15346 ` 188` ```apply (blast intro: rtrancl_trans) ``` paulson@15346 ` 189` ```done ``` paulson@15346 ` 190` paulson@15346 ` 191` ```lemma lemma2: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |] ``` paulson@15346 ` 192` ``` ==> ALL m. f m = x --> (EX i. ALL k. f (m+i+k) = f (m+i))" ``` paulson@15346 ` 193` ```apply (erule wf_induct, clarify) ``` paulson@15346 ` 194` ```apply (case_tac "EX j. (f (m+j), f m) : r^+") ``` paulson@15346 ` 195` ``` apply clarify ``` paulson@15346 ` 196` ``` apply (subgoal_tac "EX i. ALL k. f ((m+j) +i+k) = f ( (m+j) +i) ") ``` paulson@15346 ` 197` ``` apply clarify ``` paulson@15346 ` 198` ``` apply (rule_tac x = "j+i" in exI) ``` paulson@15346 ` 199` ``` apply (simp add: add_ac, blast) ``` paulson@15346 ` 200` ```apply (rule_tac x = 0 in exI, clarsimp) ``` paulson@15346 ` 201` ```apply (drule_tac i = m and k = k in lemma1) ``` paulson@15346 ` 202` ```apply (blast elim: rtranclE dest: rtrancl_into_trancl1) ``` paulson@15346 ` 203` ```done ``` paulson@15346 ` 204` paulson@15346 ` 205` ```lemma wf_weak_decr_stable: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |] ``` paulson@15346 ` 206` ``` ==> EX i. ALL k. f (i+k) = f i" ``` paulson@15346 ` 207` ```apply (drule_tac x = 0 in lemma2 [THEN spec], auto) ``` paulson@15346 ` 208` ```done ``` paulson@15346 ` 209` paulson@15346 ` 210` ```(* special case of the theorem above: <= *) ``` paulson@15346 ` 211` ```lemma weak_decr_stable: ``` paulson@15346 ` 212` ``` "ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i" ``` paulson@15346 ` 213` ```apply (rule_tac r = pred_nat in wf_weak_decr_stable) ``` paulson@15346 ` 214` ```apply (simp add: pred_nat_trancl_eq_le) ``` paulson@15346 ` 215` ```apply (intro wf_trancl wf_pred_nat) ``` paulson@15346 ` 216` ```done ``` paulson@15346 ` 217` paulson@15346 ` 218` paulson@15346 ` 219` ```ML ``` paulson@15346 ` 220` ```{* ``` paulson@15346 ` 221` ```val less_than_def = thm "less_than_def"; ``` paulson@15346 ` 222` ```val measure_def = thm "measure_def"; ``` paulson@15346 ` 223` ```val lex_prod_def = thm "lex_prod_def"; ``` paulson@15346 ` 224` ```val finite_psubset_def = thm "finite_psubset_def"; ``` paulson@15346 ` 225` paulson@15346 ` 226` ```val wf_less_than = thm "wf_less_than"; ``` paulson@15346 ` 227` ```val trans_less_than = thm "trans_less_than"; ``` paulson@15346 ` 228` ```val less_than_iff = thm "less_than_iff"; ``` paulson@15346 ` 229` ```val full_nat_induct = thm "full_nat_induct"; ``` paulson@15346 ` 230` ```val wf_inv_image = thm "wf_inv_image"; ``` paulson@15346 ` 231` ```val wf_measure = thm "wf_measure"; ``` paulson@15346 ` 232` ```val measure_induct = thm "measure_induct"; ``` paulson@15346 ` 233` ```val wf_lex_prod = thm "wf_lex_prod"; ``` paulson@15346 ` 234` ```val trans_lex_prod = thm "trans_lex_prod"; ``` paulson@15346 ` 235` ```val wf_finite_psubset = thm "wf_finite_psubset"; ``` paulson@15346 ` 236` ```val trans_finite_psubset = thm "trans_finite_psubset"; ``` paulson@15346 ` 237` ```val finite_acyclic_wf = thm "finite_acyclic_wf"; ``` paulson@15346 ` 238` ```val finite_acyclic_wf_converse = thm "finite_acyclic_wf_converse"; ``` paulson@15346 ` 239` ```val wf_iff_acyclic_if_finite = thm "wf_iff_acyclic_if_finite"; ``` paulson@15346 ` 240` ```val wf_weak_decr_stable = thm "wf_weak_decr_stable"; ``` paulson@15346 ` 241` ```val weak_decr_stable = thm "weak_decr_stable"; ``` paulson@15346 ` 242` ```val same_fstI = thm "same_fstI"; ``` paulson@15346 ` 243` ```val wf_same_fst = thm "wf_same_fst"; ``` paulson@15346 ` 244` ```*} ``` paulson@15346 ` 245` nipkow@10213 ` 246` nipkow@10213 ` 247` ```end ```