theory FastMap

lemma lookup_tree_to_list_of_distinct:
  "\<lbrakk> fst (lookup_tree_valid key tree);
     lookup_tree_to_list tree = binds;
     lookup_tree key tree = map_of (map (apfst key) binds) o key
   \<rbrakk> \<Longrightarrow> distinct (map (key o fst) binds)" apply (drule sym[where t = binds]) apply clarsimp apply (thin_tac "binds = _") apply (induct tree) apply simp apply (fastforce simp: map_add_def lookup_tree_to_list_of
                   split: prod.splits option.splits if_splits
                   dest: lookup_tree_valid_empty lookup_tree_valid_range
                         lookup_tree_valid_in_range lookup_tree_to_list_range
                   elim: lookup_tree_valid_in_range_None) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (lookup_tree_valid key tree); lookup_tree_to_list tree = binds; lookup_tree key tree = map_of (map (apfst key) binds) \<circ> key\<rbrakk> \<Longrightarrow> distinct (map (key \<circ> fst) binds) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (lookup_tree_valid key tree); lookup_tree key tree = map_of (map (apfst key) binds) \<circ> key; binds = lookup_tree_to_list tree\<rbrakk> \<Longrightarrow> distinct (map (key \<circ> fst) binds) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (lookup_tree_valid key tree); lookup_tree key tree = map_of (map (apfst key) (lookup_tree_to_list tree)) \<circ> key; binds = lookup_tree_to_list tree\<rbrakk> \<Longrightarrow> distinct (map (key \<circ> fst) (lookup_tree_to_list tree)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (lookup_tree_valid key tree); lookup_tree key tree = map_of (map (apfst key) (lookup_tree_to_list tree)) \<circ> key\<rbrakk> \<Longrightarrow> distinct (map (key \<circ> fst) (lookup_tree_to_list tree)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>fst (lookup_tree_valid key Leaf); lookup_tree key Leaf = map_of (map (apfst key) (lookup_tree_to_list Leaf)) \<circ> key\<rbrakk> \<Longrightarrow> distinct (map (key \<circ> fst) (lookup_tree_to_list Leaf))
 2. \<And>x1 x2 tree1 tree2. \<lbrakk>\<lbrakk>fst (lookup_tree_valid key tree1); lookup_tree key tree1 = map_of (map (apfst key) (lookup_tree_to_list tree1)) \<circ> key\<rbrakk> \<Longrightarrow> distinct (map (key \<circ> fst) (lookup_tree_to_list tree1)); \<lbrakk>fst (lookup_tree_valid key tree2); lookup_tree key tree2 = map_of (map (apfst key) (lookup_tree_to_list tree2)) \<circ> key\<rbrakk> \<Longrightarrow> distinct (map (key \<circ> fst) (lookup_tree_to_list tree2)); fst (lookup_tree_valid key (Node x1 x2 tree1 tree2)); lookup_tree key (Node x1 x2 tree1 tree2) = map_of (map (apfst key) (lookup_tree_to_list (Node x1 x2 tree1 tree2))) \<circ> key\<rbrakk> \<Longrightarrow> distinct (map (key \<circ> fst) (lookup_tree_to_list (Node x1 x2 tree1 tree2))) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 tree1 tree2. \<lbrakk>\<lbrakk>fst (lookup_tree_valid key tree1); lookup_tree key tree1 = map_of (map (apfst key) (lookup_tree_to_list tree1)) \<circ> key\<rbrakk> \<Longrightarrow> distinct (map (key \<circ> fst) (lookup_tree_to_list tree1)); \<lbrakk>fst (lookup_tree_valid key tree2); lookup_tree key tree2 = map_of (map (apfst key) (lookup_tree_to_list tree2)) \<circ> key\<rbrakk> \<Longrightarrow> distinct (map (key \<circ> fst) (lookup_tree_to_list tree2)); fst (lookup_tree_valid key (Node x1 x2 tree1 tree2)); lookup_tree key (Node x1 x2 tree1 tree2) = map_of (map (apfst key) (lookup_tree_to_list (Node x1 x2 tree1 tree2))) \<circ> key\<rbrakk> \<Longrightarrow> distinct (map (key \<circ> fst) (lookup_tree_to_list (Node x1 x2 tree1 tree2))) proof (prove)
goal:
No subgoals!