src/HOL/Wellfounded_Relations.thy
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 15352 cba05842bd7a
child 18277 6c2b039b4847
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
     1 (*  ID:   $Id$
     2     Author:     Konrad Slind
     3     Copyright   1995 TU Munich
     4 *)
     5 
     6 header {*Well-founded 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.*}
    16 
    17 constdefs
    18  less_than :: "(nat*nat)set"
    19     "less_than == trancl pred_nat"
    20 
    21  measure   :: "('a => nat) => ('a * 'a)set"
    22     "measure == inv_image less_than"
    23 
    24  lex_prod  :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
    25                (infixr "<*lex*>" 80)
    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
    72 
    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.*}
   120 
   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 @{term 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 well-founded 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 
   219 
   220 end