added 'mlex_iff' lemma and simplified proof
authorblanchet
Mon Oct 30 21:52:31 2017 +0100 (19 months ago)
changeset 6695280985b62029d
parent 66951 dd4710b91277
child 66953 826a5fd4d36c
added 'mlex_iff' lemma and simplified proof
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/Wellfounded.thy	Mon Oct 30 20:27:25 2017 +0100
     1.2 +++ b/src/HOL/Wellfounded.thy	Mon Oct 30 21:52:31 2017 +0100
     1.3 @@ -199,7 +199,7 @@
     1.4  lemma wfP_empty [iff]: "wfP (\<lambda>x y. False)"
     1.5  proof -
     1.6    have "wfP bot"
     1.7 -    by (fact wf_empty [to_pred bot_empty_eq2])
     1.8 +    by (fact wf_empty[to_pred bot_empty_eq2])
     1.9    then show ?thesis
    1.10      by (simp add: bot_fun_def)
    1.11  qed
    1.12 @@ -753,13 +753,11 @@
    1.13  definition mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80)
    1.14    where "f <*mlex*> R = inv_image (less_than <*lex*> R) (\<lambda>x. (f x, x))"
    1.15  
    1.16 -lemma wf_mlex: "wf R \<Longrightarrow> wf (f <*mlex*> R)"
    1.17 -  by (auto simp: mlex_prod_def)
    1.18 -
    1.19 -lemma mlex_less: "f x < f y \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
    1.20 -  by (simp add: mlex_prod_def)
    1.21 -
    1.22 -lemma mlex_leq: "f x \<le> f y \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
    1.23 +lemma
    1.24 +  wf_mlex: "wf R \<Longrightarrow> wf (f <*mlex*> R)" and
    1.25 +  mlex_less: "f x < f y \<Longrightarrow> (x, y) \<in> f <*mlex*> R" and
    1.26 +  mlex_leq: "f x \<le> f y \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (x, y) \<in> f <*mlex*> R" and
    1.27 +  mlex_iff: "(x, y) \<in> f <*mlex*> R \<longleftrightarrow> f x < f y \<or> f x = f y \<and> (x, y) \<in> R"
    1.28    by (auto simp: mlex_prod_def)
    1.29  
    1.30  text \<open>Proper subset relation on finite sets.\<close>
    1.31 @@ -846,7 +844,6 @@
    1.32  lemma max_ext_additive: "(A, B) \<in> max_ext R \<Longrightarrow> (C, D) \<in> max_ext R \<Longrightarrow> (A \<union> C, B \<union> D) \<in> max_ext R"
    1.33    by (force elim!: max_ext.cases)
    1.34  
    1.35 -
    1.36  definition min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set"
    1.37    where "min_ext r = {(X, Y) | X Y. X \<noteq> {} \<and> (\<forall>y \<in> Y. (\<exists>x \<in> X. (x, y) \<in> r))}"
    1.38  
    1.39 @@ -854,7 +851,7 @@
    1.40    assumes "wf r"
    1.41    shows "wf (min_ext r)"
    1.42  proof (rule wfI_min)
    1.43 -  show "\<exists>m \<in> Q. (\<forall> n. (n, m) \<in> min_ext r \<longrightarrow> n \<notin> Q)" if nonempty: "x \<in> Q"
    1.44 +  show "\<exists>m \<in> Q. (\<forall>n. (n, m) \<in> min_ext r \<longrightarrow> n \<notin> Q)" if nonempty: "x \<in> Q"
    1.45      for Q :: "'a set set" and x
    1.46    proof (cases "Q = {{}}")
    1.47      case True
    1.48 @@ -900,20 +897,9 @@
    1.49  
    1.50  lemma finite_subset_wf:
    1.51    assumes "finite A"
    1.52 -  shows "wf {(X,Y). X \<subset> Y \<and> Y \<subseteq> A}"
    1.53 -proof (intro finite_acyclic_wf)
    1.54 -  have "{(X,Y). X \<subset> Y \<and> Y \<subseteq> A} \<subseteq> Pow A \<times> Pow A"
    1.55 -    by blast
    1.56 -  then show "finite {(X,Y). X \<subset> Y \<and> Y \<subseteq> A}"
    1.57 -    by (rule finite_subset) (auto simp: assms finite_cartesian_product)
    1.58 -next
    1.59 -  have "{(X, Y). X \<subset> Y \<and> Y \<subseteq> A}\<^sup>+ = {(X, Y). X \<subset> Y \<and> Y \<subseteq> A}"
    1.60 -    by (intro trancl_id transI) blast
    1.61 -  also have " \<forall>x. (x, x) \<notin> \<dots>"
    1.62 -    by blast
    1.63 -  finally show "acyclic {(X,Y). X \<subset> Y \<and> Y \<subseteq> A}"
    1.64 -    by (rule acyclicI)
    1.65 -qed
    1.66 +  shows "wf {(X, Y). X \<subset> Y \<and> Y \<subseteq> A}"
    1.67 +  by (rule wf_subset[OF wf_finite_psubset[unfolded finite_psubset_def]])
    1.68 +    (auto intro: finite_subset[OF _ assms])
    1.69  
    1.70  hide_const (open) acc accp
    1.71