src/HOL/Wellfounded.thy
changeset 68646 7dc9fe795dae
parent 68262 d231238bd977
child 69275 9bbd5497befd
     1.1 --- a/src/HOL/Wellfounded.thy	Mon Jul 16 23:33:38 2018 +0100
     1.2 +++ b/src/HOL/Wellfounded.thy	Tue Jul 17 22:18:27 2018 +0100
     1.3 @@ -132,13 +132,9 @@
     1.4  qed
     1.5  
     1.6  lemma wf_eq_minimal: "wf r \<longleftrightarrow> (\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q))"
     1.7 -  apply auto
     1.8 -   apply (erule wfE_min)
     1.9 -    apply assumption
    1.10 -   apply blast
    1.11 -  apply (rule wfI_min)
    1.12 -  apply auto
    1.13 -  done
    1.14 +  apply (rule iffI)
    1.15 +   apply (blast intro:  elim!: wfE_min)
    1.16 +  by (rule wfI_min) auto
    1.17  
    1.18  lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]
    1.19  
    1.20 @@ -223,30 +219,45 @@
    1.21  qed
    1.22  
    1.23  text \<open>Well-foundedness of \<open>insert\<close>.\<close>
    1.24 -lemma wf_insert [iff]: "wf (insert (y, x) r) \<longleftrightarrow> wf r \<and> (x, y) \<notin> r\<^sup>*"
    1.25 -  apply (rule iffI)
    1.26 -   apply (blast elim: wf_trancl [THEN wf_irrefl]
    1.27 -      intro: rtrancl_into_trancl1 wf_subset rtrancl_mono [THEN [2] rev_subsetD])
    1.28 -  apply (simp add: wf_eq_minimal)
    1.29 -  apply safe
    1.30 -  apply (rule allE)
    1.31 -   apply assumption
    1.32 -  apply (erule impE)
    1.33 -   apply blast
    1.34 -  apply (erule bexE)
    1.35 -  apply (rename_tac a, case_tac "a = x")
    1.36 -   prefer 2
    1.37 -   apply blast
    1.38 -  apply (case_tac "y \<in> Q")
    1.39 -   prefer 2
    1.40 -   apply blast
    1.41 -  apply (rule_tac x = "{z. z \<in> Q \<and> (z,y) \<in> r\<^sup>*}" in allE)
    1.42 -   apply assumption
    1.43 -  apply (erule_tac V = "\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> P Q" for P in thin_rl)
    1.44 -  (*essential for speed*)
    1.45 -  (*blast with new substOccur fails*)
    1.46 -  apply (fast intro: converse_rtrancl_into_rtrancl)
    1.47 -  done
    1.48 +lemma wf_insert [iff]: "wf (insert (y,x) r) \<longleftrightarrow> wf r \<and> (x,y) \<notin> r\<^sup>*" (is "?lhs = ?rhs")
    1.49 +proof
    1.50 +  assume ?lhs then show ?rhs
    1.51 +    by (blast elim: wf_trancl [THEN wf_irrefl]
    1.52 +        intro: rtrancl_into_trancl1 wf_subset rtrancl_mono [THEN subsetD])
    1.53 +next
    1.54 +  assume R: ?rhs 
    1.55 +  then have R': "Q \<noteq> {} \<Longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q)" for Q
    1.56 +    by (auto simp: wf_eq_minimal)
    1.57 +  show ?lhs
    1.58 +    unfolding wf_eq_minimal
    1.59 +  proof clarify
    1.60 +    fix Q :: "'a set" and q
    1.61 +    assume "q \<in> Q"
    1.62 +    then obtain a where "a \<in> Q" and a: "\<And>y. (y, a) \<in> r \<Longrightarrow> y \<notin> Q"
    1.63 +      using R by (auto simp: wf_eq_minimal)
    1.64 +    show "\<exists>z\<in>Q. \<forall>y'. (y', z) \<in> insert (y, x) r \<longrightarrow> y' \<notin> Q"
    1.65 +    proof (cases "a=x")
    1.66 +      case True
    1.67 +      show ?thesis
    1.68 +      proof (cases "y \<in> Q")
    1.69 +        case True
    1.70 +        then obtain z where "z \<in> Q" "(z, y) \<in> r\<^sup>*"
    1.71 +                            "\<And>z'. (z', z) \<in> r \<longrightarrow> z' \<in> Q \<longrightarrow> (z', y) \<notin> r\<^sup>*"
    1.72 +          using R' [of "{z \<in> Q. (z,y) \<in> r\<^sup>*}"] by auto
    1.73 +        with R show ?thesis
    1.74 +          by (rule_tac x="z" in bexI) (blast intro: rtrancl_trans)
    1.75 +      next
    1.76 +        case False
    1.77 +        then show ?thesis
    1.78 +          using a \<open>a \<in> Q\<close> by blast
    1.79 +      qed
    1.80 +    next
    1.81 +      case False
    1.82 +      with a \<open>a \<in> Q\<close> show ?thesis
    1.83 +        by blast
    1.84 +    qed
    1.85 +  qed
    1.86 +qed
    1.87  
    1.88  
    1.89  subsubsection \<open>Well-foundedness of image\<close>
    1.90 @@ -307,20 +318,29 @@
    1.91  text \<open>Well-foundedness of indexed union with disjoint domains and ranges.\<close>
    1.92  
    1.93  lemma wf_UN:
    1.94 -  assumes "\<forall>i\<in>I. wf (r i)"
    1.95 -    and "\<forall>i\<in>I. \<forall>j\<in>I. r i \<noteq> r j \<longrightarrow> Domain (r i) \<inter> Range (r j) = {}"
    1.96 +  assumes r: "\<And>i. i \<in> I \<Longrightarrow> wf (r i)"
    1.97 +    and disj: "\<And>i j. \<lbrakk>i \<in> I; j \<in> I; r i \<noteq> r j\<rbrakk> \<Longrightarrow> Domain (r i) \<inter> Range (r j) = {}"
    1.98    shows "wf (\<Union>i\<in>I. r i)"
    1.99 -  using assms
   1.100 -  apply (simp only: wf_eq_minimal)
   1.101 -  apply clarify
   1.102 -  apply (rename_tac A a, case_tac "\<exists>i\<in>I. \<exists>a\<in>A. \<exists>b\<in>A. (b, a) \<in> r i")
   1.103 -   prefer 2
   1.104 -   apply force
   1.105 -  apply clarify
   1.106 -  apply (drule bspec, assumption)
   1.107 -  apply (erule_tac x="{a. a \<in> A \<and> (\<exists>b\<in>A. (b, a) \<in> r i) }" in allE)
   1.108 -  apply (blast elim!: allE)
   1.109 -  done
   1.110 +  unfolding wf_eq_minimal
   1.111 +proof clarify
   1.112 +  fix A and a :: "'b"
   1.113 +  assume "a \<in> A"
   1.114 +  show "\<exists>z\<in>A. \<forall>y. (y, z) \<in> UNION I r \<longrightarrow> y \<notin> A"
   1.115 +  proof (cases "\<exists>i\<in>I. \<exists>a\<in>A. \<exists>b\<in>A. (b, a) \<in> r i")
   1.116 +    case True
   1.117 +    then obtain i b c where ibc: "i \<in> I" "b \<in> A" "c \<in> A" "(c,b) \<in> r i"
   1.118 +      by blast
   1.119 +    have ri: "\<And>Q. Q \<noteq> {} \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> r i \<longrightarrow> y \<notin> Q"
   1.120 +      using r [OF \<open>i \<in> I\<close>] unfolding wf_eq_minimal by auto
   1.121 +    show ?thesis
   1.122 +      using ri [of "{a. a \<in> A \<and> (\<exists>b\<in>A. (b, a) \<in> r i) }"] ibc disj 
   1.123 +      by blast
   1.124 +  next
   1.125 +    case False
   1.126 +    with \<open>a \<in> A\<close> show ?thesis
   1.127 +      by blast
   1.128 +  qed
   1.129 +qed
   1.130  
   1.131  lemma wfP_SUP:
   1.132    "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (Domainp (r i)) (Rangep (r j)) = bot \<Longrightarrow>
   1.133 @@ -482,11 +502,14 @@
   1.134  
   1.135  subsubsection \<open>Wellfoundedness of finite acyclic relations\<close>
   1.136  
   1.137 -lemma finite_acyclic_wf [rule_format]: "finite r \<Longrightarrow> acyclic r \<longrightarrow> wf r"
   1.138 -  apply (erule finite_induct)
   1.139 -   apply blast
   1.140 -  apply (simp add: split_tupled_all)
   1.141 -  done
   1.142 +lemma finite_acyclic_wf:
   1.143 +  assumes "finite r" "acyclic r" shows "wf r"
   1.144 +  using assms
   1.145 +proof (induction r rule: finite_induct)
   1.146 +  case (insert x r)
   1.147 +  then show ?case
   1.148 +    by (cases x) simp
   1.149 +qed simp
   1.150  
   1.151  lemma finite_acyclic_wf_converse: "finite r \<Longrightarrow> acyclic r \<Longrightarrow> wf (r\<inverse>)"
   1.152    apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf])
   1.153 @@ -595,8 +618,7 @@
   1.154    apply (rule major [THEN accp.induct])
   1.155    apply (rule hyp)
   1.156     apply (rule accp.accI)
   1.157 -   apply fast
   1.158 -  apply fast
   1.159 +   apply auto
   1.160    done
   1.161  
   1.162  lemmas accp_induct_rule = accp_induct [rule_format, induct set: accp]
   1.163 @@ -631,8 +653,7 @@
   1.164  theorem accp_wfPI: "\<forall>x. accp r x \<Longrightarrow> wfP r"
   1.165    apply (rule wfPUNIVI)
   1.166    apply (rule_tac P = P in accp_induct)
   1.167 -   apply blast
   1.168 -  apply blast
   1.169 +   apply blast+
   1.170    done
   1.171  
   1.172  theorem accp_wfPD: "wfP r \<Longrightarrow> accp r x"
   1.173 @@ -728,11 +749,8 @@
   1.174  
   1.175  lemma wf_if_measure: "(\<And>x. P x \<Longrightarrow> f(g x) < f x) \<Longrightarrow> wf {(y,x). P x \<and> y = g x}"
   1.176    for f :: "'a \<Rightarrow> nat"
   1.177 -  apply (insert wf_measure[of f])
   1.178 -  apply (simp only: measure_def inv_image_def less_than_def less_eq)
   1.179 -  apply (erule wf_subset)
   1.180 -  apply auto
   1.181 -  done
   1.182 +  using wf_measure[of f] unfolding measure_def inv_image_def less_than_def less_eq
   1.183 +  by (rule wf_subset) auto
   1.184  
   1.185  
   1.186  subsubsection \<open>Lexicographic combinations\<close>
   1.187 @@ -742,7 +760,7 @@
   1.188    where "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}"
   1.189  
   1.190  lemma wf_lex_prod [intro!]: "wf ra \<Longrightarrow> wf rb \<Longrightarrow> wf (ra <*lex*> rb)"
   1.191 -  apply (unfold wf_def lex_prod_def)
   1.192 +  unfolding wf_def lex_prod_def
   1.193    apply (rule allI)
   1.194    apply (rule impI)
   1.195    apply (simp only: split_paired_All)