src/HOL/Wellfounded_Relations.thy
author wenzelm
Fri Mar 28 19:43:54 2008 +0100 (2008-03-28)
changeset 26462 dac4e2bce00d
parent 26072 f65a7fa2da6c
permissions -rw-r--r--
avoid rebinding of existing facts;
     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 FunDef
    10 uses
    11   ("Tools/function_package/lexicographic_order.ML")
    12   ("Tools/function_package/fundef_datatype.ML")
    13 begin
    14 
    15 text{*Derived WF relations such as inverse image, lexicographic product and
    16 measure. The simple relational product, in which @{term "(x',y')"} precedes
    17 @{term "(x,y)"} if @{term "x'<x"} and @{term "y'<y"}, is a subset of the
    18 lexicographic product, and therefore does not need to be defined separately.*}
    19 
    20 constdefs
    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 subsection{*Measure Functions make Wellfounded Relations*}
    40 
    41 subsubsection{*`Less than' on the natural numbers*}
    42 
    43 lemma full_nat_induct:
    44   assumes ih: "(!!n. (ALL m. Suc m <= n --> P m) ==> P n)"
    45   shows "P n"
    46 apply (rule wf_less_than [THEN wf_induct])
    47 apply (rule ih, auto)
    48 done
    49 
    50 subsubsection{*The Inverse Image into a Wellfounded Relation is Wellfounded.*}
    51 
    52 lemma wf_inv_image [simp,intro!]: "wf(r) ==> wf(inv_image r (f::'a=>'b))"
    53 apply (simp (no_asm_use) add: inv_image_def wf_eq_minimal)
    54 apply clarify
    55 apply (subgoal_tac "EX (w::'b) . w : {w. EX (x::'a) . x: Q & (f x = w) }")
    56 prefer 2 apply (blast del: allE)
    57 apply (erule allE)
    58 apply (erule (1) notE impE)
    59 apply blast
    60 done
    61 
    62 lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)"
    63   by (auto simp:inv_image_def)
    64 
    65 subsubsection{*Finally, All Measures are Wellfounded.*}
    66 
    67 lemma in_measure[simp]: "((x,y) : measure f) = (f x < f y)"
    68   by (simp add:measure_def)
    69 
    70 lemma wf_measure [iff]: "wf (measure f)"
    71 apply (unfold measure_def)
    72 apply (rule wf_less_than [THEN wf_inv_image])
    73 done
    74 
    75 lemma measure_induct_rule [case_names less]:
    76   fixes f :: "'a \<Rightarrow> nat"
    77   assumes step: "\<And>x. (\<And>y. f y < f x \<Longrightarrow> P y) \<Longrightarrow> P x"
    78   shows "P a"
    79 proof -
    80   have "wf (measure f)" ..
    81   then show ?thesis
    82   proof induct
    83     case (less x)
    84     show ?case
    85     proof (rule step)
    86       fix y
    87       assume "f y < f x"
    88       hence "(y, x) \<in> measure f" by simp
    89       thus "P y" by (rule less)
    90     qed
    91   qed
    92 qed
    93 
    94 lemma measure_induct:
    95   fixes f :: "'a \<Rightarrow> nat"
    96   shows "(\<And>x. \<forall>y. f y < f x \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a"
    97   by (rule measure_induct_rule [of f P a]) iprover
    98 
    99 (* Should go into Finite_Set, but needs measure.
   100    Maybe move Wf_Rel before Finite_Set and finite_psubset to Finite_set?
   101 *)
   102 lemma (in linorder)
   103   finite_linorder_induct[consumes 1, case_names empty insert]:
   104  "finite A \<Longrightarrow> P {} \<Longrightarrow>
   105   (!!A b. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))
   106   \<Longrightarrow> P A"
   107 proof (induct A rule: measure_induct[where f=card])
   108   fix A :: "'a set"
   109   assume IH: "ALL B. card B < card A \<longrightarrow> finite B \<longrightarrow> P {} \<longrightarrow>
   110                  (\<forall>A b. finite A \<longrightarrow> (\<forall>a\<in>A. a<b) \<longrightarrow> P A \<longrightarrow> P (insert b A))
   111                   \<longrightarrow> P B"
   112   and "finite A" and "P {}"
   113   and step: "!!A b. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
   114   show "P A"
   115   proof cases
   116     assume "A = {}" thus "P A" using `P {}` by simp
   117   next
   118     let ?B = "A - {Max A}" let ?A = "insert (Max A) ?B"
   119     assume "A \<noteq> {}"
   120     with `finite A` have "Max A : A" by auto
   121     hence A: "?A = A" using insert_Diff_single insert_absorb by auto
   122     note card_Diff1_less[OF `finite A` `Max A : A`]
   123     moreover have "finite ?B" using `finite A` by simp
   124     ultimately have "P ?B" using `P {}` step IH by blast
   125     moreover have "\<forall>a\<in>?B. a < Max A"
   126       using Max_ge[OF `finite A` `A \<noteq> {}`] by fastsimp
   127     ultimately show "P A"
   128       using A insert_Diff_single step[OF `finite ?B`] by fastsimp
   129   qed
   130 qed
   131 
   132 
   133 subsection{*Other Ways of Constructing Wellfounded Relations*}
   134 
   135 text{*Wellfoundedness of lexicographic combinations*}
   136 lemma wf_lex_prod [intro!]: "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)"
   137 apply (unfold wf_def lex_prod_def) 
   138 apply (rule allI, rule impI)
   139 apply (simp (no_asm_use) only: split_paired_All)
   140 apply (drule spec, erule mp) 
   141 apply (rule allI, rule impI)
   142 apply (drule spec, erule mp, blast) 
   143 done
   144 
   145 lemma in_lex_prod[simp]: 
   146   "(((a,b),(a',b')): r <*lex*> s) = ((a,a'): r \<or> (a = a' \<and> (b, b') : s))"
   147   by (auto simp:lex_prod_def)
   148 
   149 text {* lexicographic combinations with measure functions *}
   150 
   151 definition 
   152   mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80)
   153 where
   154   "f <*mlex*> R = inv_image (less_than <*lex*> R) (%x. (f x, x))"
   155 
   156 lemma wf_mlex: "wf R \<Longrightarrow> wf (f <*mlex*> R)"
   157 unfolding mlex_prod_def
   158 by auto
   159 
   160 lemma mlex_less: "f x < f y \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
   161 unfolding mlex_prod_def by simp
   162 
   163 lemma mlex_leq: "f x \<le> f y \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
   164 unfolding mlex_prod_def by auto
   165 
   166 
   167 text{*Transitivity of WF combinators.*}
   168 lemma trans_lex_prod [intro!]: 
   169     "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"
   170 by (unfold trans_def lex_prod_def, blast) 
   171 
   172 subsubsection{*Wellfoundedness of proper subset on finite sets.*}
   173 lemma wf_finite_psubset: "wf(finite_psubset)"
   174 apply (unfold finite_psubset_def)
   175 apply (rule wf_measure [THEN wf_subset])
   176 apply (simp add: measure_def inv_image_def less_than_def less_eq)
   177 apply (fast elim!: psubset_card_mono)
   178 done
   179 
   180 lemma trans_finite_psubset: "trans finite_psubset"
   181 by (simp add: finite_psubset_def psubset_def trans_def, blast)
   182 
   183 
   184 subsubsection{*Wellfoundedness of finite acyclic relations*}
   185 
   186 text{*This proof belongs in this theory because it needs Finite.*}
   187 
   188 lemma finite_acyclic_wf [rule_format]: "finite r ==> acyclic r --> wf r"
   189 apply (erule finite_induct, blast)
   190 apply (simp (no_asm_simp) only: split_tupled_all)
   191 apply simp
   192 done
   193 
   194 lemma finite_acyclic_wf_converse: "[|finite r; acyclic r|] ==> wf (r^-1)"
   195 apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf])
   196 apply (erule acyclic_converse [THEN iffD2])
   197 done
   198 
   199 lemma wf_iff_acyclic_if_finite: "finite r ==> wf r = acyclic r"
   200 by (blast intro: finite_acyclic_wf wf_acyclic)
   201 
   202 
   203 subsubsection{*Wellfoundedness of @{term same_fst}*}
   204 
   205 lemma same_fstI [intro!]:
   206      "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
   207 by (simp add: same_fst_def)
   208 
   209 lemma wf_same_fst:
   210   assumes prem: "(!!x. P x ==> wf(R x))"
   211   shows "wf(same_fst P R)"
   212 apply (simp cong del: imp_cong add: wf_def same_fst_def)
   213 apply (intro strip)
   214 apply (rename_tac a b)
   215 apply (case_tac "wf (R a)")
   216  apply (erule_tac a = b in wf_induct, blast)
   217 apply (blast intro: prem)
   218 done
   219 
   220 
   221 subsection{*Weakly decreasing sequences (w.r.t. some well-founded order) 
   222    stabilize.*}
   223 
   224 text{*This material does not appear to be used any longer.*}
   225 
   226 lemma lemma1: "[| ALL i. (f (Suc i), f i) : r^* |] ==> (f (i+k), f i) : r^*"
   227 apply (induct_tac "k", simp_all)
   228 apply (blast intro: rtrancl_trans)
   229 done
   230 
   231 lemma lemma2: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |]  
   232       ==> ALL m. f m = x --> (EX i. ALL k. f (m+i+k) = f (m+i))"
   233 apply (erule wf_induct, clarify)
   234 apply (case_tac "EX j. (f (m+j), f m) : r^+")
   235  apply clarify
   236  apply (subgoal_tac "EX i. ALL k. f ((m+j) +i+k) = f ( (m+j) +i) ")
   237   apply clarify
   238   apply (rule_tac x = "j+i" in exI)
   239   apply (simp add: add_ac, blast)
   240 apply (rule_tac x = 0 in exI, clarsimp)
   241 apply (drule_tac i = m and k = k in lemma1)
   242 apply (blast elim: rtranclE dest: rtrancl_into_trancl1)
   243 done
   244 
   245 lemma wf_weak_decr_stable: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |]  
   246       ==> EX i. ALL k. f (i+k) = f i"
   247 apply (drule_tac x = 0 in lemma2 [THEN spec], auto)
   248 done
   249 
   250 (* special case of the theorem above: <= *)
   251 lemma weak_decr_stable:
   252      "ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i"
   253 apply (rule_tac r = pred_nat in wf_weak_decr_stable)
   254 apply (simp add: pred_nat_trancl_eq_le)
   255 apply (intro wf_trancl wf_pred_nat)
   256 done
   257 
   258 
   259 text {*
   260   Setup of @{text lexicographic_order} method
   261   and @{text fun} command
   262 *}
   263 
   264 use "Tools/function_package/lexicographic_order.ML"
   265 use "Tools/function_package/fundef_datatype.ML"
   266 
   267 setup "LexicographicOrder.setup #> FundefDatatype.setup"
   268 
   269 end