equal
deleted
inserted
replaced
441 "mult1 r == |
441 "mult1 r == |
442 {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and> |
442 {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and> |
443 (\<forall>b. b :# K --> (b, a) \<in> r)}" |
443 (\<forall>b. b :# K --> (b, a) \<in> r)}" |
444 |
444 |
445 mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" |
445 mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" |
446 "mult r == (mult1 r)^+" |
446 "mult r == (mult1 r)\<^sup>+" |
447 |
447 |
448 lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r" |
448 lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r" |
449 by (simp add: mult1_def) |
449 by (simp add: mult1_def) |
450 |
450 |
451 lemma less_add: "(N, M0 + {#a#}) \<in> mult1 r ==> |
451 lemma less_add: "(N, M0 + {#a#}) \<in> mult1 r ==> |