equal
deleted
inserted
replaced
59 apply (intro strip) |
59 apply (intro strip) |
60 apply (simp del: set_append map_append) |
60 apply (simp del: set_append map_append) |
61 apply (frule length_takeWhile) |
61 apply (frule length_takeWhile) |
62 apply (frule_tac f = "(the \<circ> loc)" in nth_map) |
62 apply (frule_tac f = "(the \<circ> loc)" in nth_map) |
63 apply simp |
63 apply simp |
|
64 done |
|
65 |
|
66 lemma lift_if: "(f (if b then t else e)) = (if b then (f t) else (f e))" |
|
67 apply auto |
64 done |
68 done |
65 |
69 |
66 lemma update_at_index: " |
70 lemma update_at_index: " |
67 \<lbrakk> distinct (gjmb_plns (gmb G C S)); |
71 \<lbrakk> distinct (gjmb_plns (gmb G C S)); |
68 x \<in> set (gjmb_plns (gmb G C S)); x \<noteq> This \<rbrakk> \<Longrightarrow> |
72 x \<in> set (gjmb_plns (gmb G C S)); x \<noteq> This \<rbrakk> \<Longrightarrow> |