equal
deleted
inserted
replaced
113 apply (subgoal_tac "\<exists>k' kr. ks = k' # kr") |
113 apply (subgoal_tac "\<exists>k' kr. ks = k' # kr") |
114 apply (clarify) |
114 apply (clarify) |
115 apply (drule_tac x=kr in spec) |
115 apply (drule_tac x=kr in spec) |
116 apply (simp only: rev.simps) |
116 apply (simp only: rev.simps) |
117 apply (subgoal_tac "(empty(rev kr @ [k'][\<mapsto>]rev xs @ [a])) = empty (rev kr[\<mapsto>]rev xs)([k'][\<mapsto>][a])") |
117 apply (subgoal_tac "(empty(rev kr @ [k'][\<mapsto>]rev xs @ [a])) = empty (rev kr[\<mapsto>]rev xs)([k'][\<mapsto>][a])") |
118 apply (simp split:split_if_asm) |
118 apply (simp split:if_split_asm) |
119 apply (simp add: map_upds_append [symmetric]) |
119 apply (simp add: map_upds_append [symmetric]) |
120 apply (case_tac ks) |
120 apply (case_tac ks) |
121 apply auto |
121 apply auto |
122 done |
122 done |
123 |
123 |