simplified proofs for splitI and splitD, added splitD'
added split_conv_tac (also to claset()) as an optimization
made split_all_tac safe introducing safe_full_simp_tac,EXISTING PROOFS MAY FAIL
consts update :: ('a,'v)trie => 'a list => 'v => ('a,'v)trie
primrec
"update t [] v = Trie (Some v) (alist t)"
"update t (a#as) v = (let tt = (case assoc (alist t) a of
None => Trie None [] | Some at => at)
in Trie (value t) ((a,update tt as v)#alist t))"