equal
deleted
inserted
replaced
11 text {* |
11 text {* |
12 Lifting an order to lists of elements, relating exactly one |
12 Lifting an order to lists of elements, relating exactly one |
13 element. |
13 element. |
14 *} |
14 *} |
15 |
15 |
16 constdefs |
16 definition |
17 step1 :: "('a \<times> 'a) set => ('a list \<times> 'a list) set" |
17 step1 :: "('a \<times> 'a) set => ('a list \<times> 'a list) set" |
18 "step1 r == |
18 "step1 r = |
19 {(ys, xs). \<exists>us z z' vs. xs = us @ z # vs \<and> (z', z) \<in> r \<and> ys = |
19 {(ys, xs). \<exists>us z z' vs. xs = us @ z # vs \<and> (z', z) \<in> r \<and> ys = |
20 us @ z' # vs}" |
20 us @ z' # vs}" |
21 |
21 |
22 |
22 |
23 lemma step1_converse [simp]: "step1 (r^-1) = (step1 r)^-1" |
23 lemma step1_converse [simp]: "step1 (r^-1) = (step1 r)^-1" |