15346

1 
(* ID: $Id$

10213

2 
Author: Konrad Slind


3 
Copyright 1995 TU Munich


4 
*)


5 

15346

6 
header {*Wellfounded Relations*}


7 


8 
theory Wellfounded_Relations


9 
imports Finite_Set


10 
begin


11 


12 
text{*Derived WF relations such as inverse image, lexicographic product and


13 
measure. The simple relational product, in which @{term "(x',y')"} precedes


14 
@{term "(x,y)"} if @{term "x'<x"} and @{term "y'<y"}, is a subset of the


15 
lexicographic product, and therefore does not need to be defined separately.*}

10213

16 


17 
constdefs


18 
less_than :: "(nat*nat)set"

15346

19 
"less_than == trancl pred_nat"

10213

20 


21 
measure :: "('a => nat) => ('a * 'a)set"

15346

22 
"measure == inv_image less_than"

10213

23 


24 
lex_prod :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"


25 
(infixr "<*lex*>" 80)

15346

26 
"ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra  a=a' & (b,b') : rb}"


27 


28 
finite_psubset :: "('a set * 'a set) set"


29 
{* finite proper subset*}


30 
"finite_psubset == {(A,B). A < B & finite B}"


31 


32 
same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"


33 
"same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"


34 
{*For @{text rec_def} declarations where the first n parameters


35 
stay unchanged in the recursive call.


36 
See @{text "Library/While_Combinator.thy"} for an application.*}


37 


38 


39 


40 


41 
subsection{*Measure Functions make Wellfounded Relations*}


42 


43 
subsubsection{*`Less than' on the natural numbers*}


44 


45 
lemma wf_less_than [iff]: "wf less_than"


46 
by (simp add: less_than_def wf_pred_nat [THEN wf_trancl])


47 


48 
lemma trans_less_than [iff]: "trans less_than"


49 
by (simp add: less_than_def trans_trancl)


50 


51 
lemma less_than_iff [iff]: "((x,y): less_than) = (x<y)"


52 
by (simp add: less_than_def less_def)


53 


54 
lemma full_nat_induct:


55 
assumes ih: "(!!n. (ALL m. Suc m <= n > P m) ==> P n)"


56 
shows "P n"


57 
apply (rule wf_less_than [THEN wf_induct])


58 
apply (rule ih, auto)


59 
done


60 


61 
subsubsection{*The Inverse Image into a Wellfounded Relation is Wellfounded.*}


62 


63 
lemma wf_inv_image [simp,intro!]: "wf(r) ==> wf(inv_image r (f::'a=>'b))"


64 
apply (simp (no_asm_use) add: inv_image_def wf_eq_minimal)


65 
apply clarify


66 
apply (subgoal_tac "EX (w::'b) . w : {w. EX (x::'a) . x: Q & (f x = w) }")


67 
prefer 2 apply (blast del: allE)


68 
apply (erule allE)


69 
apply (erule (1) notE impE)


70 
apply blast


71 
done

10213

72 

15346

73 


74 
subsubsection{*Finally, All Measures are Wellfounded.*}


75 


76 
lemma wf_measure [iff]: "wf (measure f)"


77 
apply (unfold measure_def)


78 
apply (rule wf_less_than [THEN wf_inv_image])


79 
done


80 


81 
lemmas measure_induct =


82 
wf_measure [THEN wf_induct, unfolded measure_def inv_image_def,


83 
simplified, standard]


84 


85 


86 
subsection{*Other Ways of Constructing Wellfounded Relations*}


87 


88 
text{*Wellfoundedness of lexicographic combinations*}


89 
lemma wf_lex_prod [intro!]: "[ wf(ra); wf(rb) ] ==> wf(ra <*lex*> rb)"


90 
apply (unfold wf_def lex_prod_def)


91 
apply (rule allI, rule impI)


92 
apply (simp (no_asm_use) only: split_paired_All)


93 
apply (drule spec, erule mp)


94 
apply (rule allI, rule impI)


95 
apply (drule spec, erule mp, blast)


96 
done


97 


98 


99 
text{*Transitivity of WF combinators.*}


100 
lemma trans_lex_prod [intro!]:


101 
"[ trans R1; trans R2 ] ==> trans (R1 <*lex*> R2)"


102 
by (unfold trans_def lex_prod_def, blast)


103 


104 


105 
subsubsection{*Wellfoundedness of proper subset on finite sets.*}


106 
lemma wf_finite_psubset: "wf(finite_psubset)"


107 
apply (unfold finite_psubset_def)


108 
apply (rule wf_measure [THEN wf_subset])


109 
apply (simp add: measure_def inv_image_def less_than_def less_def [symmetric])


110 
apply (fast elim!: psubset_card_mono)


111 
done


112 


113 
lemma trans_finite_psubset: "trans finite_psubset"


114 
by (simp add: finite_psubset_def psubset_def trans_def, blast)


115 


116 


117 
subsubsection{*Wellfoundedness of finite acyclic relations*}


118 


119 
text{*This proof belongs in this theory because it needs Finite.*}

10213

120 

15346

121 
lemma finite_acyclic_wf [rule_format]: "finite r ==> acyclic r > wf r"


122 
apply (erule finite_induct, blast)


123 
apply (simp (no_asm_simp) only: split_tupled_all)


124 
apply simp


125 
done


126 


127 
lemma finite_acyclic_wf_converse: "[finite r; acyclic r] ==> wf (r^1)"


128 
apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf])


129 
apply (erule acyclic_converse [THEN iffD2])


130 
done


131 


132 
lemma wf_iff_acyclic_if_finite: "finite r ==> wf r = acyclic r"


133 
by (blast intro: finite_acyclic_wf wf_acyclic)


134 


135 


136 
subsubsection{*Wellfoundedness of same_fst*}


137 


138 
lemma same_fstI [intro!]:


139 
"[ P x; (y',y) : R x ] ==> ((x,y'),(x,y)) : same_fst P R"


140 
by (simp add: same_fst_def)


141 


142 
lemma wf_same_fst:


143 
assumes prem: "(!!x. P x ==> wf(R x))"


144 
shows "wf(same_fst P R)"


145 
apply (simp cong del: imp_cong add: wf_def same_fst_def)


146 
apply (intro strip)


147 
apply (rename_tac a b)


148 
apply (case_tac "wf (R a)")


149 
apply (erule_tac a = b in wf_induct, blast)


150 
apply (blast intro: prem)


151 
done


152 


153 


154 
subsection{*Weakly decreasing sequences (w.r.t. some wellfounded order)


155 
stabilize.*}


156 


157 
text{*This material does not appear to be used any longer.*}


158 


159 
lemma lemma1: "[ ALL i. (f (Suc i), f i) : r^* ] ==> (f (i+k), f i) : r^*"


160 
apply (induct_tac "k", simp_all)


161 
apply (blast intro: rtrancl_trans)


162 
done


163 


164 
lemma lemma2: "[ ALL i. (f (Suc i), f i) : r^*; wf (r^+) ]


165 
==> ALL m. f m = x > (EX i. ALL k. f (m+i+k) = f (m+i))"


166 
apply (erule wf_induct, clarify)


167 
apply (case_tac "EX j. (f (m+j), f m) : r^+")


168 
apply clarify


169 
apply (subgoal_tac "EX i. ALL k. f ((m+j) +i+k) = f ( (m+j) +i) ")


170 
apply clarify


171 
apply (rule_tac x = "j+i" in exI)


172 
apply (simp add: add_ac, blast)


173 
apply (rule_tac x = 0 in exI, clarsimp)


174 
apply (drule_tac i = m and k = k in lemma1)


175 
apply (blast elim: rtranclE dest: rtrancl_into_trancl1)


176 
done


177 


178 
lemma wf_weak_decr_stable: "[ ALL i. (f (Suc i), f i) : r^*; wf (r^+) ]


179 
==> EX i. ALL k. f (i+k) = f i"


180 
apply (drule_tac x = 0 in lemma2 [THEN spec], auto)


181 
done


182 


183 
(* special case of the theorem above: <= *)


184 
lemma weak_decr_stable:


185 
"ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i"


186 
apply (rule_tac r = pred_nat in wf_weak_decr_stable)


187 
apply (simp add: pred_nat_trancl_eq_le)


188 
apply (intro wf_trancl wf_pred_nat)


189 
done


190 


191 


192 
ML


193 
{*


194 
val less_than_def = thm "less_than_def";


195 
val measure_def = thm "measure_def";


196 
val lex_prod_def = thm "lex_prod_def";


197 
val finite_psubset_def = thm "finite_psubset_def";


198 


199 
val wf_less_than = thm "wf_less_than";


200 
val trans_less_than = thm "trans_less_than";


201 
val less_than_iff = thm "less_than_iff";


202 
val full_nat_induct = thm "full_nat_induct";


203 
val wf_inv_image = thm "wf_inv_image";


204 
val wf_measure = thm "wf_measure";


205 
val measure_induct = thm "measure_induct";


206 
val wf_lex_prod = thm "wf_lex_prod";


207 
val trans_lex_prod = thm "trans_lex_prod";


208 
val wf_finite_psubset = thm "wf_finite_psubset";


209 
val trans_finite_psubset = thm "trans_finite_psubset";


210 
val finite_acyclic_wf = thm "finite_acyclic_wf";


211 
val finite_acyclic_wf_converse = thm "finite_acyclic_wf_converse";


212 
val wf_iff_acyclic_if_finite = thm "wf_iff_acyclic_if_finite";


213 
val wf_weak_decr_stable = thm "wf_weak_decr_stable";


214 
val weak_decr_stable = thm "weak_decr_stable";


215 
val same_fstI = thm "same_fstI";


216 
val wf_same_fst = thm "wf_same_fst";


217 
*}


218 

10213

219 


220 
end
