src/HOL/Library/Multiset.thy
 changeset 63089 40134ddec3bf parent 63088 f2177f5d2aed child 63092 a949b2a5f51d
equal 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>`