[STATEMENT]
lemma invar_delete: "invar t \<Longrightarrow> invar (delete xs t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar t \<Longrightarrow> invar (Trie_Map.delete xs t)
[PROOF STEP]
apply(induction xs t rule: delete.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b m. invar (trie_map.Nd b m) \<Longrightarrow> invar (Trie_Map.delete [] (trie_map.Nd b m))
 2. \<And>x xs b m. \<lbrakk>\<And>x2. \<lbrakk>lookup m x = Some x2; invar x2\<rbrakk> \<Longrightarrow> invar (Trie_Map.delete xs x2); invar (trie_map.Nd b m)\<rbrakk> \<Longrightarrow> invar (Trie_Map.delete (x # xs) (trie_map.Nd b m))
[PROOF STEP]
apply(auto simp: M.map_specs split: option.split)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done