equal
deleted
inserted
replaced
348 apply (unfold prefix_def) |
348 apply (unfold prefix_def) |
349 apply (rule trans_gen_prefix) |
349 apply (rule trans_gen_prefix) |
350 apply (auto simp add: trans_def) |
350 apply (auto simp add: trans_def) |
351 done |
351 done |
352 |
352 |
353 lemmas prefix_trans = trans_prefix [THEN transD, standard] |
353 lemmas prefix_trans = trans_prefix [THEN transD] |
354 |
354 |
355 lemma trans_on_prefix: "trans[list(A)](prefix(A))" |
355 lemma trans_on_prefix: "trans[list(A)](prefix(A))" |
356 apply (unfold prefix_def) |
356 apply (unfold prefix_def) |
357 apply (rule trans_on_gen_prefix) |
357 apply (rule trans_on_gen_prefix) |
358 apply (auto simp add: trans_def) |
358 apply (auto simp add: trans_def) |
359 done |
359 done |
360 |
360 |
361 lemmas prefix_trans_on = trans_on_prefix [THEN trans_onD, standard] |
361 lemmas prefix_trans_on = trans_on_prefix [THEN trans_onD] |
362 |
362 |
363 (* Monotonicity of "set" operator WRT prefix *) |
363 (* Monotonicity of "set" operator WRT prefix *) |
364 |
364 |
365 lemma set_of_list_prefix_mono: |
365 lemma set_of_list_prefix_mono: |
366 "<xs,ys> \<in> prefix(A) ==> set_of_list(xs) <= set_of_list(ys)" |
366 "<xs,ys> \<in> prefix(A) ==> set_of_list(xs) <= set_of_list(ys)" |