more de-applying
authorpaulson <lp15@cam.ac.uk>
Tue Jul 17 22:18:27 2018 +0100 (9 months ago)
changeset 686467dc9fe795dae
parent 68645 5e15795788d3
child 68647 f0d98441eff5
child 68662 227f85b1b98c
more de-applying
src/HOL/List.thy
src/HOL/MicroJava/DFA/Listn.thy
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/List.thy	Mon Jul 16 23:33:38 2018 +0100
     1.2 +++ b/src/HOL/List.thy	Tue Jul 17 22:18:27 2018 +0100
     1.3 @@ -5804,14 +5804,11 @@
     1.4  by (induct n arbitrary: xs ys) auto
     1.5  
     1.6  lemma wf_lex [intro!]: "wf r ==> wf (lex r)"
     1.7 -apply (unfold lex_def)
     1.8 -apply (rule wf_UN)
     1.9 -apply (blast intro: wf_lexn, clarify)
    1.10 -apply (rename_tac m n)
    1.11 -apply (subgoal_tac "m \<noteq> n")
    1.12 - prefer 2 apply blast
    1.13 -apply (blast dest: lexn_length not_sym)
    1.14 -done
    1.15 +  apply (unfold lex_def)
    1.16 +  apply (rule wf_UN)
    1.17 +   apply (simp add: wf_lexn)
    1.18 +  apply (metis DomainE Int_emptyI RangeE lexn_length)
    1.19 +  done
    1.20  
    1.21  lemma lexn_conv:
    1.22    "lexn r n =
     2.1 --- a/src/HOL/MicroJava/DFA/Listn.thy	Mon Jul 16 23:33:38 2018 +0100
     2.2 +++ b/src/HOL/MicroJava/DFA/Listn.thy	Tue Jul 17 22:18:27 2018 +0100
     2.3 @@ -323,12 +323,10 @@
     2.4   apply (blast intro: lesssub_list_impl_same_size)
     2.5  apply (rule wf_UN)
     2.6   prefer 2
     2.7 - apply clarify
     2.8   apply (rename_tac m n)
     2.9   apply (case_tac "m=n")
    2.10    apply simp
    2.11   apply (fast intro!: equals0I dest: not_sym)
    2.12 -apply clarify
    2.13  apply (rename_tac n)
    2.14  apply (induct_tac n)
    2.15   apply (simp add: lesssub_def cong: conj_cong)
    2.16 @@ -353,7 +351,7 @@
    2.17   apply blast
    2.18  apply clarify
    2.19  apply (thin_tac "m \<in> M")
    2.20 -apply (thin_tac "maxA#xs \<in> M")
    2.21 +  apply (thin_tac "maxA#xs \<in> M")
    2.22  apply (rule bexI)
    2.23   prefer 2
    2.24   apply assumption
     3.1 --- a/src/HOL/Wellfounded.thy	Mon Jul 16 23:33:38 2018 +0100
     3.2 +++ b/src/HOL/Wellfounded.thy	Tue Jul 17 22:18:27 2018 +0100
     3.3 @@ -132,13 +132,9 @@
     3.4  qed
     3.5  
     3.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))"
     3.7 -  apply auto
     3.8 -   apply (erule wfE_min)
     3.9 -    apply assumption
    3.10 -   apply blast
    3.11 -  apply (rule wfI_min)
    3.12 -  apply auto
    3.13 -  done
    3.14 +  apply (rule iffI)
    3.15 +   apply (blast intro:  elim!: wfE_min)
    3.16 +  by (rule wfI_min) auto
    3.17  
    3.18  lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]
    3.19  
    3.20 @@ -223,30 +219,45 @@
    3.21  qed
    3.22  
    3.23  text \<open>Well-foundedness of \<open>insert\<close>.\<close>
    3.24 -lemma wf_insert [iff]: "wf (insert (y, x) r) \<longleftrightarrow> wf r \<and> (x, y) \<notin> r\<^sup>*"
    3.25 -  apply (rule iffI)
    3.26 -   apply (blast elim: wf_trancl [THEN wf_irrefl]
    3.27 -      intro: rtrancl_into_trancl1 wf_subset rtrancl_mono [THEN [2] rev_subsetD])
    3.28 -  apply (simp add: wf_eq_minimal)
    3.29 -  apply safe
    3.30 -  apply (rule allE)
    3.31 -   apply assumption
    3.32 -  apply (erule impE)
    3.33 -   apply blast
    3.34 -  apply (erule bexE)
    3.35 -  apply (rename_tac a, case_tac "a = x")
    3.36 -   prefer 2
    3.37 -   apply blast
    3.38 -  apply (case_tac "y \<in> Q")
    3.39 -   prefer 2
    3.40 -   apply blast
    3.41 -  apply (rule_tac x = "{z. z \<in> Q \<and> (z,y) \<in> r\<^sup>*}" in allE)
    3.42 -   apply assumption
    3.43 -  apply (erule_tac V = "\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> P Q" for P in thin_rl)
    3.44 -  (*essential for speed*)
    3.45 -  (*blast with new substOccur fails*)
    3.46 -  apply (fast intro: converse_rtrancl_into_rtrancl)
    3.47 -  done
    3.48 +lemma wf_insert [iff]: "wf (insert (y,x) r) \<longleftrightarrow> wf r \<and> (x,y) \<notin> r\<^sup>*" (is "?lhs = ?rhs")
    3.49 +proof
    3.50 +  assume ?lhs then show ?rhs
    3.51 +    by (blast elim: wf_trancl [THEN wf_irrefl]
    3.52 +        intro: rtrancl_into_trancl1 wf_subset rtrancl_mono [THEN subsetD])
    3.53 +next
    3.54 +  assume R: ?rhs 
    3.55 +  then have R': "Q \<noteq> {} \<Longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q)" for Q
    3.56 +    by (auto simp: wf_eq_minimal)
    3.57 +  show ?lhs
    3.58 +    unfolding wf_eq_minimal
    3.59 +  proof clarify
    3.60 +    fix Q :: "'a set" and q
    3.61 +    assume "q \<in> Q"
    3.62 +    then obtain a where "a \<in> Q" and a: "\<And>y. (y, a) \<in> r \<Longrightarrow> y \<notin> Q"
    3.63 +      using R by (auto simp: wf_eq_minimal)
    3.64 +    show "\<exists>z\<in>Q. \<forall>y'. (y', z) \<in> insert (y, x) r \<longrightarrow> y' \<notin> Q"
    3.65 +    proof (cases "a=x")
    3.66 +      case True
    3.67 +      show ?thesis
    3.68 +      proof (cases "y \<in> Q")
    3.69 +        case True
    3.70 +        then obtain z where "z \<in> Q" "(z, y) \<in> r\<^sup>*"
    3.71 +                            "\<And>z'. (z', z) \<in> r \<longrightarrow> z' \<in> Q \<longrightarrow> (z', y) \<notin> r\<^sup>*"
    3.72 +          using R' [of "{z \<in> Q. (z,y) \<in> r\<^sup>*}"] by auto
    3.73 +        with R show ?thesis
    3.74 +          by (rule_tac x="z" in bexI) (blast intro: rtrancl_trans)
    3.75 +      next
    3.76 +        case False
    3.77 +        then show ?thesis
    3.78 +          using a \<open>a \<in> Q\<close> by blast
    3.79 +      qed
    3.80 +    next
    3.81 +      case False
    3.82 +      with a \<open>a \<in> Q\<close> show ?thesis
    3.83 +        by blast
    3.84 +    qed
    3.85 +  qed
    3.86 +qed
    3.87  
    3.88  
    3.89  subsubsection \<open>Well-foundedness of image\<close>
    3.90 @@ -307,20 +318,29 @@
    3.91  text \<open>Well-foundedness of indexed union with disjoint domains and ranges.\<close>
    3.92  
    3.93  lemma wf_UN:
    3.94 -  assumes "\<forall>i\<in>I. wf (r i)"
    3.95 -    and "\<forall>i\<in>I. \<forall>j\<in>I. r i \<noteq> r j \<longrightarrow> Domain (r i) \<inter> Range (r j) = {}"
    3.96 +  assumes r: "\<And>i. i \<in> I \<Longrightarrow> wf (r i)"
    3.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) = {}"
    3.98    shows "wf (\<Union>i\<in>I. r i)"
    3.99 -  using assms
   3.100 -  apply (simp only: wf_eq_minimal)
   3.101 -  apply clarify
   3.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")
   3.103 -   prefer 2
   3.104 -   apply force
   3.105 -  apply clarify
   3.106 -  apply (drule bspec, assumption)
   3.107 -  apply (erule_tac x="{a. a \<in> A \<and> (\<exists>b\<in>A. (b, a) \<in> r i) }" in allE)
   3.108 -  apply (blast elim!: allE)
   3.109 -  done
   3.110 +  unfolding wf_eq_minimal
   3.111 +proof clarify
   3.112 +  fix A and a :: "'b"
   3.113 +  assume "a \<in> A"
   3.114 +  show "\<exists>z\<in>A. \<forall>y. (y, z) \<in> UNION I r \<longrightarrow> y \<notin> A"
   3.115 +  proof (cases "\<exists>i\<in>I. \<exists>a\<in>A. \<exists>b\<in>A. (b, a) \<in> r i")
   3.116 +    case True
   3.117 +    then obtain i b c where ibc: "i \<in> I" "b \<in> A" "c \<in> A" "(c,b) \<in> r i"
   3.118 +      by blast
   3.119 +    have ri: "\<And>Q. Q \<noteq> {} \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> r i \<longrightarrow> y \<notin> Q"
   3.120 +      using r [OF \<open>i \<in> I\<close>] unfolding wf_eq_minimal by auto
   3.121 +    show ?thesis
   3.122 +      using ri [of "{a. a \<in> A \<and> (\<exists>b\<in>A. (b, a) \<in> r i) }"] ibc disj 
   3.123 +      by blast
   3.124 +  next
   3.125 +    case False
   3.126 +    with \<open>a \<in> A\<close> show ?thesis
   3.127 +      by blast
   3.128 +  qed
   3.129 +qed
   3.130  
   3.131  lemma wfP_SUP:
   3.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>
   3.133 @@ -482,11 +502,14 @@
   3.134  
   3.135  subsubsection \<open>Wellfoundedness of finite acyclic relations\<close>
   3.136  
   3.137 -lemma finite_acyclic_wf [rule_format]: "finite r \<Longrightarrow> acyclic r \<longrightarrow> wf r"
   3.138 -  apply (erule finite_induct)
   3.139 -   apply blast
   3.140 -  apply (simp add: split_tupled_all)
   3.141 -  done
   3.142 +lemma finite_acyclic_wf:
   3.143 +  assumes "finite r" "acyclic r" shows "wf r"
   3.144 +  using assms
   3.145 +proof (induction r rule: finite_induct)
   3.146 +  case (insert x r)
   3.147 +  then show ?case
   3.148 +    by (cases x) simp
   3.149 +qed simp
   3.150  
   3.151  lemma finite_acyclic_wf_converse: "finite r \<Longrightarrow> acyclic r \<Longrightarrow> wf (r\<inverse>)"
   3.152    apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf])
   3.153 @@ -595,8 +618,7 @@
   3.154    apply (rule major [THEN accp.induct])
   3.155    apply (rule hyp)
   3.156     apply (rule accp.accI)
   3.157 -   apply fast
   3.158 -  apply fast
   3.159 +   apply auto
   3.160    done
   3.161  
   3.162  lemmas accp_induct_rule = accp_induct [rule_format, induct set: accp]
   3.163 @@ -631,8 +653,7 @@
   3.164  theorem accp_wfPI: "\<forall>x. accp r x \<Longrightarrow> wfP r"
   3.165    apply (rule wfPUNIVI)
   3.166    apply (rule_tac P = P in accp_induct)
   3.167 -   apply blast
   3.168 -  apply blast
   3.169 +   apply blast+
   3.170    done
   3.171  
   3.172  theorem accp_wfPD: "wfP r \<Longrightarrow> accp r x"
   3.173 @@ -728,11 +749,8 @@
   3.174  
   3.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}"
   3.176    for f :: "'a \<Rightarrow> nat"
   3.177 -  apply (insert wf_measure[of f])
   3.178 -  apply (simp only: measure_def inv_image_def less_than_def less_eq)
   3.179 -  apply (erule wf_subset)
   3.180 -  apply auto
   3.181 -  done
   3.182 +  using wf_measure[of f] unfolding measure_def inv_image_def less_than_def less_eq
   3.183 +  by (rule wf_subset) auto
   3.184  
   3.185  
   3.186  subsubsection \<open>Lexicographic combinations\<close>
   3.187 @@ -742,7 +760,7 @@
   3.188    where "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}"
   3.189  
   3.190  lemma wf_lex_prod [intro!]: "wf ra \<Longrightarrow> wf rb \<Longrightarrow> wf (ra <*lex*> rb)"
   3.191 -  apply (unfold wf_def lex_prod_def)
   3.192 +  unfolding wf_def lex_prod_def
   3.193    apply (rule allI)
   3.194    apply (rule impI)
   3.195    apply (simp only: split_paired_All)