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.7      Author:     Konrad Slind
     1.8      Copyright   1995 TU Munich
     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.18 +header {*Well-founded Relations*}
    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.163 +by (simp add: same_fst_def)
   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.195 +  apply (simp add: add_ac, blast)
   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.210 +apply (simp add: pred_nat_trancl_eq_le)
   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