src/HOL/Wellfounded_Relations.thy
 changeset 15346 ac272926fb77 parent 12398 9c27f28c8f5a child 15348 0a60f15c2d7a
```     1.1 --- a/src/HOL/Wellfounded_Relations.thy	Tue Nov 30 13:29:36 2004 +0100
1.2 +++ b/src/HOL/Wellfounded_Relations.thy	Tue Nov 30 16:27:44 2004 +0100
1.3 @@ -1,36 +1,220 @@
1.4 -(*  Title:      HOL/Wellfounded_Relations
1.5 -    ID:         \$Id\$
1.6 +(*  ID:   \$Id\$
1.9 -
1.10 -Derived WF relations: inverse image, lexicographic product, measure, ...
1.11 -
1.12 -The simple relational product, in which (x',y')<(x,y) iff x'<x and y'<y, is a
1.13 -subset of the lexicographic product, and therefore does not need to be defined
1.14 -separately.
1.15  *)
1.16
1.17 -Wellfounded_Relations = Finite_Set +
1.19 +
1.20 +theory Wellfounded_Relations
1.21 +imports Finite_Set
1.22 +begin
1.23 +
1.24 +text{*Derived WF relations such as inverse image, lexicographic product and
1.25 +measure. The simple relational product, in which @{term "(x',y')"} precedes
1.26 +@{term "(x,y)"} if @{term "x'<x"} and @{term "y'<y"}, is a subset of the
1.27 +lexicographic product, and therefore does not need to be defined separately.*}
1.28
1.29  constdefs
1.30   less_than :: "(nat*nat)set"
1.31 -"less_than == trancl pred_nat"
1.32 +    "less_than == trancl pred_nat"
1.33
1.34   measure   :: "('a => nat) => ('a * 'a)set"
1.35 -"measure == inv_image less_than"
1.36 +    "measure == inv_image less_than"
1.37
1.38   lex_prod  :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
1.39                 (infixr "<*lex*>" 80)
1.40 -"ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra | a=a' & (b,b') : rb}"
1.41 +    "ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra | a=a' & (b,b') : rb}"
1.42 +
1.43 + finite_psubset  :: "('a set * 'a set) set"
1.44 +   --{* finite proper subset*}
1.45 +    "finite_psubset == {(A,B). A < B & finite B}"
1.46 +
1.47 + same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
1.48 +    "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
1.49 +   --{*For @{text rec_def} declarations where the first n parameters
1.50 +       stay unchanged in the recursive call.
1.51 +       See @{text "Library/While_Combinator.thy"} for an application.*}
1.52 +
1.53 +
1.54 +
1.55 +
1.56 +subsection{*Measure Functions make Wellfounded Relations*}
1.57 +
1.58 +subsubsection{*`Less than' on the natural numbers*}
1.59 +
1.60 +lemma wf_less_than [iff]: "wf less_than"
1.61 +by (simp add: less_than_def wf_pred_nat [THEN wf_trancl])
1.62 +
1.63 +lemma trans_less_than [iff]: "trans less_than"
1.64 +by (simp add: less_than_def trans_trancl)
1.65 +
1.66 +lemma less_than_iff [iff]: "((x,y): less_than) = (x<y)"
1.67 +by (simp add: less_than_def less_def)
1.68 +
1.69 +lemma full_nat_induct:
1.70 +  assumes ih: "(!!n. (ALL m. Suc m <= n --> P m) ==> P n)"
1.71 +  shows "P n"
1.72 +apply (rule wf_less_than [THEN wf_induct])
1.73 +apply (rule ih, auto)
1.74 +done
1.75 +
1.76 +subsubsection{*The Inverse Image into a Wellfounded Relation is Wellfounded.*}
1.77 +
1.78 +lemma wf_inv_image [simp,intro!]: "wf(r) ==> wf(inv_image r (f::'a=>'b))"
1.79 +apply (simp (no_asm_use) add: inv_image_def wf_eq_minimal)
1.80 +apply clarify
1.81 +apply (subgoal_tac "EX (w::'b) . w : {w. EX (x::'a) . x: Q & (f x = w) }")
1.82 +prefer 2 apply (blast del: allE)
1.83 +apply (erule allE)
1.84 +apply (erule (1) notE impE)
1.85 +apply blast
1.86 +done
1.87
1.88 - (* finite proper subset*)
1.89 - finite_psubset  :: "('a set * 'a set) set"
1.90 -"finite_psubset == {(A,B). A < B & finite B}"
1.91 +
1.92 +subsubsection{*Finally, All Measures are Wellfounded.*}
1.93 +
1.94 +lemma wf_measure [iff]: "wf (measure f)"
1.95 +apply (unfold measure_def)
1.96 +apply (rule wf_less_than [THEN wf_inv_image])
1.97 +done
1.98 +
1.99 +lemmas measure_induct =
1.100 +    wf_measure [THEN wf_induct, unfolded measure_def inv_image_def,
1.101 +                simplified, standard]
1.102 +
1.103 +
1.104 +subsection{*Other Ways of Constructing Wellfounded Relations*}
1.105 +
1.106 +text{*Wellfoundedness of lexicographic combinations*}
1.107 +lemma wf_lex_prod [intro!]: "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)"
1.108 +apply (unfold wf_def lex_prod_def)
1.109 +apply (rule allI, rule impI)
1.110 +apply (simp (no_asm_use) only: split_paired_All)
1.111 +apply (drule spec, erule mp)
1.112 +apply (rule allI, rule impI)
1.113 +apply (drule spec, erule mp, blast)
1.114 +done
1.115 +
1.116 +
1.117 +text{*Transitivity of WF combinators.*}
1.118 +lemma trans_lex_prod [intro!]:
1.119 +    "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"
1.120 +by (unfold trans_def lex_prod_def, blast)
1.121 +
1.122 +
1.123 +subsubsection{*Wellfoundedness of proper subset on finite sets.*}
1.124 +lemma wf_finite_psubset: "wf(finite_psubset)"
1.125 +apply (unfold finite_psubset_def)
1.126 +apply (rule wf_measure [THEN wf_subset])
1.127 +apply (simp add: measure_def inv_image_def less_than_def less_def [symmetric])
1.128 +apply (fast elim!: psubset_card_mono)
1.129 +done
1.130 +
1.131 +lemma trans_finite_psubset: "trans finite_psubset"
1.132 +by (simp add: finite_psubset_def psubset_def trans_def, blast)
1.133 +
1.134 +
1.135 +subsubsection{*Wellfoundedness of finite acyclic relations*}
1.136 +
1.137 +text{*This proof belongs in this theory because it needs Finite.*}
1.138
1.139 -(* For rec_defs where the first n parameters stay unchanged in the recursive
1.140 -   call. See Library/While_Combinator.thy for an application.
1.141 -*)
1.142 - same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
1.143 -"same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
1.144 +lemma finite_acyclic_wf [rule_format]: "finite r ==> acyclic r --> wf r"
1.145 +apply (erule finite_induct, blast)
1.146 +apply (simp (no_asm_simp) only: split_tupled_all)
1.147 +apply simp
1.148 +done
1.149 +
1.150 +lemma finite_acyclic_wf_converse: "[|finite r; acyclic r|] ==> wf (r^-1)"
1.151 +apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf])
1.152 +apply (erule acyclic_converse [THEN iffD2])
1.153 +done
1.154 +
1.155 +lemma wf_iff_acyclic_if_finite: "finite r ==> wf r = acyclic r"
1.156 +by (blast intro: finite_acyclic_wf wf_acyclic)
1.157 +
1.158 +
1.159 +subsubsection{*Wellfoundedness of same_fst*}
1.160 +
1.161 +lemma same_fstI [intro!]:
1.162 +     "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
1.164 +
1.165 +lemma wf_same_fst:
1.166 +  assumes prem: "(!!x. P x ==> wf(R x))"
1.167 +  shows "wf(same_fst P R)"
1.168 +apply (simp cong del: imp_cong add: wf_def same_fst_def)
1.169 +apply (intro strip)
1.170 +apply (rename_tac a b)
1.171 +apply (case_tac "wf (R a)")
1.172 + apply (erule_tac a = b in wf_induct, blast)
1.173 +apply (blast intro: prem)
1.174 +done
1.175 +
1.176 +
1.177 +subsection{*Weakly decreasing sequences (w.r.t. some well-founded order)
1.178 +   stabilize.*}
1.179 +
1.180 +text{*This material does not appear to be used any longer.*}
1.181 +
1.182 +lemma lemma1: "[| ALL i. (f (Suc i), f i) : r^* |] ==> (f (i+k), f i) : r^*"
1.183 +apply (induct_tac "k", simp_all)
1.184 +apply (blast intro: rtrancl_trans)
1.185 +done
1.186 +
1.187 +lemma lemma2: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |]
1.188 +      ==> ALL m. f m = x --> (EX i. ALL k. f (m+i+k) = f (m+i))"
1.189 +apply (erule wf_induct, clarify)
1.190 +apply (case_tac "EX j. (f (m+j), f m) : r^+")
1.191 + apply clarify
1.192 + apply (subgoal_tac "EX i. ALL k. f ((m+j) +i+k) = f ( (m+j) +i) ")
1.193 +  apply clarify
1.194 +  apply (rule_tac x = "j+i" in exI)
1.196 +apply (rule_tac x = 0 in exI, clarsimp)
1.197 +apply (drule_tac i = m and k = k in lemma1)
1.198 +apply (blast elim: rtranclE dest: rtrancl_into_trancl1)
1.199 +done
1.200 +
1.201 +lemma wf_weak_decr_stable: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |]
1.202 +      ==> EX i. ALL k. f (i+k) = f i"
1.203 +apply (drule_tac x = 0 in lemma2 [THEN spec], auto)
1.204 +done
1.205 +
1.206 +(* special case of the theorem above: <= *)
1.207 +lemma weak_decr_stable:
1.208 +     "ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i"
1.209 +apply (rule_tac r = pred_nat in wf_weak_decr_stable)
1.211 +apply (intro wf_trancl wf_pred_nat)
1.212 +done
1.213 +
1.214 +
1.215 +ML
1.216 +{*
1.217 +val less_than_def = thm "less_than_def";
1.218 +val measure_def = thm "measure_def";
1.219 +val lex_prod_def = thm "lex_prod_def";
1.220 +val finite_psubset_def = thm "finite_psubset_def";
1.221 +
1.222 +val wf_less_than = thm "wf_less_than";
1.223 +val trans_less_than = thm "trans_less_than";
1.224 +val less_than_iff = thm "less_than_iff";
1.225 +val full_nat_induct = thm "full_nat_induct";
1.226 +val wf_inv_image = thm "wf_inv_image";
1.227 +val wf_measure = thm "wf_measure";
1.228 +val measure_induct = thm "measure_induct";
1.229 +val wf_lex_prod = thm "wf_lex_prod";
1.230 +val trans_lex_prod = thm "trans_lex_prod";
1.231 +val wf_finite_psubset = thm "wf_finite_psubset";
1.232 +val trans_finite_psubset = thm "trans_finite_psubset";
1.233 +val finite_acyclic_wf = thm "finite_acyclic_wf";
1.234 +val finite_acyclic_wf_converse = thm "finite_acyclic_wf_converse";
1.235 +val wf_iff_acyclic_if_finite = thm "wf_iff_acyclic_if_finite";
1.236 +val wf_weak_decr_stable = thm "wf_weak_decr_stable";
1.237 +val weak_decr_stable = thm "weak_decr_stable";
1.238 +val same_fstI = thm "same_fstI";
1.239 +val wf_same_fst = thm "wf_same_fst";
1.240 +*}
1.241 +
1.242
1.243  end
```