src/HOL/Library/Multiset.thy
changeset 63089 40134ddec3bf
parent 63088 f2177f5d2aed
child 63092 a949b2a5f51d
equal deleted inserted replaced
63088:f2177f5d2aed 63089:40134ddec3bf
  2064 lemma one_step_implies_mult:
  2064 lemma one_step_implies_mult:
  2065   "J \<noteq> {#} \<Longrightarrow> \<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r
  2065   "J \<noteq> {#} \<Longrightarrow> \<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r
  2066     \<Longrightarrow> (I + K, I + J) \<in> mult r"
  2066     \<Longrightarrow> (I + K, I + J) \<in> mult r"
  2067 using one_step_implies_mult_aux by blast
  2067 using one_step_implies_mult_aux by blast
  2068 
  2068 
  2069 subsection \<open>A quasi-recursive characterization\<close>
  2069 subsection \<open>A quasi-executable characterization\<close>
  2070 
  2070 
  2071 text \<open>
  2071 text \<open>
  2072   The decreasing parts \<open>A\<close> and \<open>B\<close> of multisets in a multiset-comparison
  2072   The decreasing parts \<open>A\<close> and \<open>B\<close> of multisets in a multiset-comparison
  2073   \<open>(I + B, I + A) \<in> mult r\<close>, can always be made disjoint.
  2073   \<open>(I + B, I + A) \<in> mult r\<close>, can always be made disjoint.
  2074 \<close>
  2074 \<close>