theory FiniteMap = AuxBox:
text {* \clearpage *}
section {* Finite Maps *}

--{* This theory models finite maps as lists of pairs. If a pair (l,r1) appears before another pair (l,r2) in a list
the second maplet is void (regared as overwritten). *}

types ('a,'b) "~~>" = "('a \<times> 'b) list" (infixr 0)
translations (type) "a ~~> b " <= (type) "(a \<times> b) list"

consts 
lookup:: "('a ~~> 'b) \<Rightarrow> 'a \<Rightarrow> 'b option" ("_ ? _" [90, 91] 90)
id_lookup::"('a ~~> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ("_?\<^sub>=_" [90, 91] 90)
dom:: "('a ~~> 'b) \<Rightarrow> 'a list"
ran:: "('a ~~> 'b) \<Rightarrow> 'b list"
del:: "('a ~~> 'b) \<Rightarrow> 'a \<Rightarrow> ('a \<times> 'b) list"
nojunk::"('a ~~> 'b) \<Rightarrow> bool"
clearjunk::"('a ~~> 'b) \<Rightarrow> ('a ~~> 'b)"

primrec
"lookup [] a = None"
"lookup (m#ms) a = (case (fst m = a)
                  of True \<Rightarrow> Some (snd m)
                  | False \<Rightarrow> lookup ms a)"

defs 

id_lookup_def: "id_lookup m a \<equiv> (case (m ? a) 
                  of None \<Rightarrow> a
                  | Some a' \<Rightarrow> a')" 

dom_def: "dom m \<equiv> map fst m"

ran_def: "ran m \<equiv> map (\<lambda> a. the (m ? a)) (dom m)"

del_def: "del m x \<equiv> filter (\<lambda> (a,b). a\<noteq>x) m"


primrec
"nojunk [] = True"
"nojunk (m#ms) = (case (ms ? (fst m))
                  of None \<Rightarrow> nojunk ms
                  | Some b \<Rightarrow> False)"   


lemma del_length:
"length (del mp a) \<le> length mp"
(*<*)
apply (induct mp)
apply (simp add: del_def)
apply (simp add: del_def)
apply (rule impI)
apply (subgoal_tac "length [(aa, b)\<in>list . aa \<noteq> a] \<le> length list")
 prefer 2
 apply (rule length_filter)
apply (subgoal_tac "length list \<le>  Suc (length list)")
 prefer 2
 apply simp
apply (drule_tac y="length list" and z="Suc (length list)" in order_trans)
apply assumption
apply assumption
(*>*)
done

lemma del_length_hint:
"length (del mp a) < Suc (length mp)"
(*<*)
apply (simp only:  less_Suc_eq_le)
apply (rule del_length)
(*>*)
done

recdef clearjunk "measure (\<lambda> mp. length mp)"
"clearjunk [] = []"
"clearjunk (m#mp) = m#(clearjunk (del mp (fst m)))"
(hints simp: del_length_hint)


subsection {* Lookup *}

lemma lookup_red:
"a\<noteq>a' \<Longrightarrow>  ((a,b)#as) ? a' = as ? a'"
(*<*)
apply (simp add: lookup.simps)
(*>*)
done

lemma id_lookup_red:
"a'\<noteq>a \<Longrightarrow>  ((a,b)#as) ?\<^sub>= a' = as ?\<^sub>= a'"
(*<*)
apply (drule not_sym)
apply (simp add: id_lookup_def)
(*>*)
done

lemma some_lookup_pair:
"mp ? a = Some b \<Longrightarrow> (a,b) \<in> set mp"
(*<*)
apply (induct mp)
apply simp
apply simp
apply (case_tac "fst aa = a")
apply simp
apply (drule_tac t="b" in sym)
apply (drule_tac t="a" in sym)
apply simp
apply simp
(*>*)
done

lemma map_empty:
"(\<forall> x. mp ? x = None) = (mp =[])"
(*<*)
apply (induct mp)
apply simp
apply simp
apply (rule_tac x="fst a" in exI)
apply (rule_tac x="snd a" in exI)
apply simp
(*>*)
done

lemma map_lookup_some:
"\<And> a b. (a,b) \<in> set mp \<Longrightarrow> (\<exists> c. mp ? a = Some c)"
(*<*)
apply (erule rev_mp)
apply (simp only:atomize_all)
apply (induct mp)
apply simp
apply simp
apply (rule allI)+
apply (rule conjI)
apply (rule impI)
apply (rule_tac x="snd a" in exI)
apply (drule_tac t="a" in sym)
apply simp

apply (rule impI)
apply (erule_tac x="aa" in allE)
apply (subgoal_tac "\<exists> b. (aa,b) \<in> set list")
 prefer 2
 apply (rule_tac x="b" in exI)
 apply simp
apply (drule mp, assumption)
apply (case_tac "fst a = aa")
apply (rule_tac x="snd a" in exI)
apply simp

apply (erule exE)+
apply (rule_tac x="c" in exI)
apply simp
(*>*)
done

lemma lookup_append:
"mp1 ? x = None \<Longrightarrow> (mp1 @ mp2) ? x = mp2 ? x"
(*<*)
apply (induct mp1)
apply simp
apply simp
apply (case_tac "fst a = x")
apply simp
apply simp
(*>*)
done

lemma lookup_append2:
"mp1 ? x = Some y \<Longrightarrow> (mp1 @ mp2) ? x = Some y"
(*<*)
apply (induct mp1)
apply simp
apply simp
apply (case_tac "fst a = x")
apply simp
apply simp
(*>*)
done

lemma lookup_switch:
"a \<noteq> c \<Longrightarrow> (mp1 @ (a,b) # (c,d) #  mp2) ? x = (mp1 @ (c,d) # (a,b) # mp2) ? x"
(*<*)
apply (case_tac "mp1 ? x")
apply (case_tac "a = x")
apply (case_tac "c = x")
prefer 3
apply (case_tac "c = x")
apply (auto simp add: lookup_append lookup_append2)
(*>*)
done


lemma lookup_redundancy:
"\<And> x y y' z mp' mp''. (mp@ (x,y) # mp' @ (x,y') # mp'') ? z = (mp @ (x,y) # mp' @ mp'') ? z"
(*<*)
apply (induct mp)
apply simp
apply (case_tac "x = z")
apply simp
apply simp
apply (erule rev_mp)
apply (simp only: atomize_all)
apply (rule forall_switch4)
apply (rule allI)
apply (induct_tac mp')
apply simp
apply simp
apply (rule allI)+
apply (case_tac "fst a = z")
apply simp
apply simp

--{* induction case *}
apply simp
apply (case_tac "fst a = z")
apply simp
apply simp
(*>*)
done

lemma some_lookup_split:
"\<And> x y. mp ? x = Some y \<Longrightarrow> (\<exists> mp1 mp2. mp = mp1 @ (x,y)#mp2 \<and> x \<notin> set (dom mp1))"
(*<*)
apply (induct mp)
apply simp
apply simp
apply (case_tac "fst a = x")
apply simp
apply (rule_tac x="[]" in exI)
apply (drule_tac t="y" in sym)
apply (drule_tac t="x" in sym)
apply (simp add: dom_def)

apply simp
apply atomize
apply (erule_tac x="x" in allE)
apply (erule_tac x="y" in allE)
apply (drule mp, assumption)
apply (erule exE)
apply (erule conjE)
apply (erule exE)
apply (rule_tac x="a#mp1" in exI)
apply (rule conjI)
apply (rule_tac x="mp2" in  exI)
apply simp

apply (simp add: dom_def)
apply (rule not_sym)
apply assumption
(*>*)
done


lemma lookup_append_notin_dom:
"x \<noteq> z \<Longrightarrow> (mp1 @ (x,y) # mp2) ? z = (mp1 @ mp2) ? z"
(*<*)
apply (induct mp1)
apply simp

apply simp
apply (case_tac "fst a = z")
apply simp

apply simp
(*>*)
done

--{* Delete *}

lemma del_lookup:
"a \<noteq> b \<Longrightarrow> m ? a = (del m b) ? a"
(*<*)
apply (induct m)
apply (simp add: del_def)
apply (simp add: lookup.simps)
apply (case_tac "fst aa = a")
apply (simp add: del_def split_def)
apply (simp add: del_def split_def)
(*>*)
done

lemma del_id_lookup:
"a \<noteq> b \<Longrightarrow> m ?\<^sub>= a = (del m b) ?\<^sub>= a"
(*<*)
apply (simp only: id_lookup_def)
apply (drule_tac m="m" and a="a" and b="b" in del_lookup)
apply simp
(*>*)
done

lemma del_lookup_eq:
"(del mp x) ? x = None"
(*<*)
apply (induct mp)
apply (simp add: del_def)
apply (simp add: del_def split_def)
(*>*)
done

lemma del_lookup_neq:
"x \<noteq> y \<Longrightarrow> (del mp x) ? y = mp ? y"
(*<*)
apply (induct mp)
apply (simp add: del_def)
apply (simp add: del_def split_def)
apply (rule impI)
apply (case_tac "fst a = y")
apply simp
apply simp
(*>*)
done

lemma del_in_mp:
"\<And> m a. \<lbrakk> fst m \<noteq> a \<rbrakk> \<Longrightarrow> (m \<in> set (del mp a)) = (m \<in> set mp)"
(*<*)
apply (induct mp)
apply (simp add: del_def)
apply atomize
apply (simp add: set.simps del_def split_def)
apply (rule impI)
apply (drule sym)
apply simp
apply (subgoal_tac "m \<noteq> a")
 prefer 2
 apply (rule classical)
 apply simp
apply simp
(*>*)
done

lemma del_append:
"del (mp@mp') x = (del mp x) @ (del mp' x)"
(*<*)
apply (induct mp)
apply (simp add: del_def)
apply (simp add: del_def)
(*>*)
done


lemma del_simp1:
"fst m = x \<Longrightarrow> del (m#mp) x = del mp x"
(*<*)
apply (simp add: del_def split_def)
(*>*)
done

lemma del_simp2:
"fst m \<noteq> x \<Longrightarrow> del (m#mp) x = m#(del mp x)"
(*<*)
apply (simp add: del_def split_def)
(*>*)
done

lemma del_del:
"del (del mp x) x = del mp x"
(*<*)
apply (induct mp)
apply (simp add: del_def)
apply (simp add: del_def)
(*>*)
done

lemma del_switch:
"del (del mp x) y = del (del mp y) x"
(*<*)
apply (induct mp)
apply (simp add: del_def)
apply (case_tac "fst a = x")
apply (case_tac "fst a = y")
apply (simp add: del_simp1 del_simp2)+
apply (case_tac "fst a = y")
apply (simp add: del_simp1 del_simp2)+
(*>*)
done

subsection {* Domain *}

lemma some_lookup_dom:
"mp ? a = Some b \<Longrightarrow> a \<in> set (dom mp)"
(*<*)
apply (drule some_lookup_pair)
apply (simp add: dom_def)
apply (subgoal_tac "(a \<in> fst ` set mp) = ((fst (a,b)) \<in> fst ` set mp)")
 prefer 2
 apply simp
apply (simp only:)
apply (rule_tac f="\<lambda> x. fst x" and x="(a,b)" in imageI)
apply assumption
(*>*)
done

lemma dom_notin:
"mp ? x = None \<Longrightarrow> x \<notin> set (dom mp)"
(*<*)
 apply (induct mp)
 apply (simp add: dom_def)
 apply (case_tac "x= fst a")
 apply (simp add: dom_def)

 apply (simp add: dom_def split add: bool.split_asm)
(*>*)
done


lemma dom_rec:
"dom (m#mp) = fst m # (dom mp)"
(*<*)
apply (simp add: dom_def)
(*>*)
done


lemma none_lookup_dom:
"(mp ? x = None) = (x \<notin> set (dom mp))"
(*<*)
apply (induct mp)
apply (simp add: dom_def)

apply simp
apply (case_tac "fst a = x")
apply (simp add: dom_def)
apply (simp only: dom_rec)
apply (drule_tac t="fst a" in not_sym)
apply simp
(*>*)
done

lemma notin_dom:
"x \<notin> set (dom mp) \<Longrightarrow> mp ? x = None"
(*<*)
apply (induct mp)
apply simp
apply simp
apply (case_tac "fst a = x")
apply (simp add: dom_def)
apply (simp add: dom_rec)
(*>*)
done

lemma dom_switch:
"a \<noteq> c \<Longrightarrow> set (dom (mp1 @ (a,b) # (c,d) # mp2)) = set (dom (mp1 @ (c,d) # (a,b) # mp2))"
(*<*)
apply (auto simp add: lookup_switch dom_def)
(*>*)
done



lemma effectless_del:
"x \<notin> set (dom mp) \<Longrightarrow> del mp x = mp"
(*<*)
apply (induct mp)
apply (simp add: dom_def del_def)

apply (simp add: dom_rec)
apply (erule conjE)+
apply (drule_tac t="x" in not_sym)
apply (simp add: del_def split_def)
(*>*)
done

lemma dom_redundancy:
"\<And> x y z mp'. set (dom (mp @ (x,y) # (x,z) # mp')) = set (dom (mp @ (x,y) # mp'))"
(*<*)
apply (induct mp)
apply (simp add: dom_def)

apply (simp add: dom_def)
(*>*)
done



lemma dom_del_set:
"\<And> mp x. set (dom (del mp x)) = set (dom mp) - {x}"
(*<*)
apply (subgoal_tac "\<exists> k. k=length mp")
 prefer 2
 apply simp
apply (erule exE)
apply (erule rev_mp)+
apply (simp only: atomize_all)
apply (rule forall_switch3)
apply (rule allI)
apply (rule_tac n="k" in nat_less_induct)
apply (rule allI)+
apply (rule impI)
apply (case_tac mp)
apply (simp add: dom_def del_def)

apply (case_tac "fst a = x")
apply (simp only: del_simp1 dom_def map.simps set.simps)
apply (erule_tac x="length list" in allE)
apply simp

apply (frule_tac m="a" and x="x" and mp="list" in del_simp2)
apply (simp only:  dom_def map.simps set.simps)
apply (erule_tac x="length list" in allE)
apply (simp add: insert_Diff_if)
(*>*)
done



--{* Range *}

lemma some_lookup_range:
"mp ? a = Some b \<Longrightarrow> b \<in> set (ran mp)"
(*<*)
apply (induct mp)
apply simp
apply simp
apply (case_tac "fst aa = a")
apply (simp add: ran_def lookup.simps dom_def)
apply (simp add: ran_def dom_def)
apply (subgoal_tac "(a,b) \<in> set list")
 prefer 2
 apply (rule some_lookup_pair)
 apply assumption
apply (subgoal_tac "fst (a,b) \<in> fst ` set list")
 prefer 2
 apply (rule imageI)
 apply assumption
apply (drule_tac f="(\<lambda>a. the (case fst aa = a of True \<Rightarrow> Some (snd aa) | False \<Rightarrow> (list ? a)))" and x="fst (a,b)" and A="fst ` set list" in imageI)
apply simp
(*>*)
done

lemma ran_switch:
"a \<noteq> c \<Longrightarrow> set (ran (mp1 @ (a,b) # (c,d) # mp2)) = set (ran (mp1 @ (c,d) # (a,b) # mp2))"
(*<*)
apply (auto simp add: lookup_switch ran_def)
apply (subgoal_tac "(mp1 @ (a, b) # (c, d) # mp2) ? aa = (mp1 @ (c, d) # (a, b) # mp2) ? aa")
 prefer 2
 apply (rule lookup_switch)
 apply assumption
apply simp
apply (rule imageI)
apply (subgoal_tac "set (dom (mp1 @ (a, b) # (c, d) # mp2)) = set (dom (mp1 @ (c, d) # (a, b) # mp2))")
 prefer 2
 apply (rule dom_switch)
 apply assumption
apply simp
apply (subgoal_tac "(mp1 @ (c, d) # (a, b) # mp2) ? aa = (mp1 @ (a, b) # (c, d) # mp2) ? aa")
 prefer 2
 apply (rule lookup_switch)
 apply (rule not_sym)
 apply assumption
apply simp
apply (rule imageI)
apply (subgoal_tac "set (dom (mp1 @ (a, b) # (c, d) # mp2)) = set (dom (mp1 @ (c, d) # (a, b) # mp2))")
 prefer 2
 apply (rule dom_switch)
 apply assumption
apply (simp add: dom_switch)
(*>*)
done


lemma ran_redundancy:
" set (ran (mp @ (x,y) # (x,y) # mp')) = set (ran (mp @ (x,y) # mp'))"
(*<*)
apply (simp add: ran_def)
apply (subgoal_tac "(\<lambda>a. the ((mp @ (x, y) # (x, y) # mp') ? a)) =
                    (\<lambda>a. the ((mp @ (x, y) # mp') ? a))")
 prefer 2
 apply (rule ext)
 apply (subgoal_tac "(mp @ (x, y) # (x, y) # mp') ? a = (mp @ (x, y) # mp') ? a")
  prefer 2
  apply (subgoal_tac "(mp @ (x, y) # (x, y) # mp') = (mp @ (x, y) # [] @  (x, y) # mp')")
   prefer 2
   apply simp
  apply (subgoal_tac "(mp @ (x, y) # mp') = (mp @ (x, y) # [] @ mp')")
   prefer 2
   apply simp
  apply (simp only:)
  apply (rule lookup_redundancy)
 apply simp
apply (subgoal_tac "set (FiniteMap.dom (mp @ (x, y) # (x, y) # mp')) =
             set (FiniteMap.dom (mp @ (x, y) # mp'))")
 prefer 2
 apply (rule dom_redundancy)
apply simp
(*>*)
done

--{* Clearjunk and Nojunk *}

lemma set_lookup:
"\<lbrakk> nojunk mp; x \<in> (set mp) \<rbrakk> \<Longrightarrow> (mp ? (fst x)) = Some (snd x)"
(*<*)
apply (induct mp)
apply simp
apply atomize
apply (case_tac "x=a")
apply (simp add: lookup.simps)
apply (simp add: lookup.simps nojunk.simps)
apply (case_tac "list ? (fst a)")
apply simp
apply (case_tac "fst a = fst x")
apply simp
apply simp
apply simp
(*>*)
done

lemma clearjunk_length:
"\<And> mp. length (clearjunk mp) \<le> length mp"
(*<*)
apply (subgoal_tac "\<exists> k. k=length mp")
 prefer 2
 apply simp
apply (erule exE)
apply (erule rev_mp)
apply (simp only: atomize_all)
apply (rule forall_switch2)
apply (rule allI)
apply (rule_tac n="k" in nat_less_induct)
apply (rule allI)
apply (rule impI)
apply (case_tac mp)
apply simp

apply simp
apply (erule_tac x="length (del list (fst a))" in allE)
apply (subgoal_tac " length (del list (fst a)) < Suc (length list)")
 prefer 2
 apply (simp only: less_Suc_eq_le) 
 apply (rule del_length)
apply (drule mp, assumption)
apply (erule_tac x="del list (fst a)" in allE)
apply simp
(*>*)
done

lemma clearjunk_lookup:
"\<And> mp a. mp ? a = (clearjunk mp) ? a"
(*<*)
apply (subgoal_tac "\<exists> k. k=length mp")
 prefer 2
 apply simp
apply (erule exE)
apply (erule rev_mp)
apply (simp only: atomize_all)
apply (rule forall_switch3)
apply (rule allI)
apply (rule_tac n="k" in nat_less_induct)
apply (rule allI)+
apply (rule impI)
apply (case_tac "mp")
apply simp
apply simp
apply (case_tac "fst aa = a")
apply (simp add: clearjunk.simps)
apply simp
apply (drule not_sym)
apply (frule_tac a="a" and b="fst aa" and m="list" in del_lookup)
apply simp
apply (erule_tac x="length (del list (fst aa))" in allE)
apply (subgoal_tac "length (del list (fst aa)) < Suc (length list)")
 prefer 2
 apply (simp only: less_Suc_eq_le) 
 apply (rule del_length)
apply (drule mp, assumption)
apply (erule_tac x="del list (fst aa)" in allE)
apply simp  
(*>*)
done

lemma nojunk_clearjunk:
"\<And> mp. nojunk mp \<Longrightarrow> clearjunk mp = mp"
(*<*)
apply (subgoal_tac "\<exists> k. k=length mp")
 prefer 2
 apply simp
apply (erule exE)
apply (erule rev_mp)+
apply (simp only: atomize_all)
apply (rule forall_switch2)
apply (rule allI)
apply (rule_tac n="k" in nat_less_induct)
apply (rule allI)+
apply (rule impI)
apply (case_tac mp)
apply simp

apply (rule impI)
apply simp
apply (case_tac "list ? fst a")
apply simp
apply (drule dom_notin)
apply (drule_tac mp="list" in effectless_del)
apply (erule_tac x="length list" in allE)
apply simp
apply simp
(*>*)
done

lemma clearjunk_nojunk:
"\<And> mp. nojunk (clearjunk mp)"
(*<*)
apply (subgoal_tac "\<exists> k. k=length mp")
 prefer 2
 apply simp
apply (erule exE)
apply (erule rev_mp)
apply (simp only: atomize_all)
apply (rule forall_switch2)
apply (rule allI)
apply (rule_tac n="k" in nat_less_induct)
apply (rule allI)+
apply (rule impI)
apply (case_tac mp)
apply simp

apply (simp add: clearjunk_lookup[THEN sym] del_lookup_eq)
apply (erule_tac x="length (del list (fst a))" in allE)
apply (subgoal_tac "length (del list (fst a)) < Suc (length list)")
 prefer 2
 apply (simp only: less_Suc_eq_le) 
 apply (rule del_length)
apply (drule mp, assumption)
apply (erule_tac x="del list (fst a)" in allE)
apply simp
(*>*)
done

lemma clearjunk_clearjunk:
"clearjunk (clearjunk mp) = (clearjunk mp)"
(*<*)
apply (subgoal_tac "nojunk (clearjunk mp)")
 prefer 2
 apply (rule clearjunk_nojunk)
apply (simp only: nojunk_clearjunk)
(*>*)
done

lemma nojunk_range:
"nojunk mp \<Longrightarrow> ran mp = (case mp 
                         of [] \<Rightarrow> []
                         | m#mp' \<Rightarrow> (snd m)#(ran mp'))"
(*<*)
apply (erule rev_mp)
apply (case_tac "mp")
apply (simp add: ran_def dom_def)
apply (simp add: ran_def dom_def)
apply (case_tac "list ? (fst a)")
prefer 2
apply simp

apply (simp)
apply (rule impI)
apply (rule ballI)
apply (subgoal_tac "list ? (fst x) = Some (snd x)")
 prefer 2
 apply (drule set_lookup)
 apply assumption+
 apply (case_tac "fst a = fst x")
 apply simp
 apply simp
(*>*)
done


lemma clearjunk_dom:
"\<And> mp. set (dom mp) = (set (dom (clearjunk mp)))"
(*<*)
apply (subgoal_tac "\<exists> k. k=length mp")
 prefer 2
 apply simp
apply (erule exE)
apply (erule rev_mp)
apply (simp only: atomize_all)
apply (rule forall_switch2)
apply (rule allI)
apply (rule_tac n="k" in nat_less_induct)
apply (rule allI)+
apply (rule impI)
apply (case_tac "mp")
apply simp
apply (simp add: dom_def)
apply (rule set_ext)
apply simp
apply (case_tac "x = fst a")
apply simp
apply simp
apply (erule_tac x="length (del list (fst a))" in allE)
apply (subgoal_tac "length (del list (fst a)) < Suc (length list)")
 prefer 2
 apply (simp only: less_Suc_eq_le) 
 apply (rule del_length)
apply (drule mp, assumption)
apply (erule_tac x="del list (fst a)" in allE)
apply simp
apply (drule_tac s="fst ` set (del list (fst a))" in sym)
apply simp
apply (rule iffI)
apply (erule imageE)
apply simp
apply (rule imageI)
apply (drule_tac m="xa" and a="fst a" and mp="list" in del_in_mp)
apply simp

apply (erule imageE)
apply simp
apply (rule imageI)
apply (drule_tac m="xa" and a="fst a" and mp="list" in del_in_mp)
apply simp
(*>*)
done

lemma clearjunk_ran:
"set (ran mp) = set (ran (clearjunk mp))"
(*<*)
apply (simp add: ran_def)
apply (subgoal_tac "set (FiniteMap.dom (clearjunk mp)) = set (dom mp)")
 prefer 2
 apply (rule sym)
 apply (rule clearjunk_dom)
apply simp
apply (rule set_ext)
apply (rule iffI)
apply (erule imageE)
apply simp
apply (subgoal_tac "mp ? a = (clearjunk mp) ? a")
 prefer 2
 apply (rule clearjunk_lookup)
apply simp

apply (erule imageE)
apply simp
 apply (subgoal_tac "(clearjunk mp) ? a = mp ? a")
 prefer 2
 apply (rule sym)
 apply (rule clearjunk_lookup)
apply simp
(*>*)
done

lemma ran_src:
"\<And> mp b. b \<in> set (ran mp) \<Longrightarrow> (\<exists> a. mp ? a = Some b)"
(*<*)
apply (subgoal_tac "\<exists> k. k=length mp")
 prefer 2
 apply simp
apply (erule exE)
apply (erule rev_mp)+
apply (simp only: atomize_all)
apply (rule forall_switch3)
apply (rule allI)
apply (rule_tac n="k" in nat_less_induct)
apply (rule allI)+
apply (rule impI)+
apply (case_tac mp)
apply (simp add: ran_def dom_def)
apply simp
apply (subgoal_tac "set (ran (a # list)) = set (ran (clearjunk (a # list)))")
 prefer 2
 apply (rule clearjunk_ran)
apply (subgoal_tac "nojunk (clearjunk (a # list))")
 prefer 2
 apply (rule clearjunk_nojunk)
apply (simp only: nojunk_range)
apply simp
apply (case_tac "b = snd a")
apply (rule_tac x="fst a" in exI)
apply simp

apply simp
apply (case_tac "clearjunk (del list (fst a)) ? fst a")
prefer 2
apply simp

apply simp

apply (erule_tac x="length (clearjunk (del list (fst a)))" in allE)
apply (subgoal_tac "length (clearjunk (del list (fst a))) < Suc (length list)")
 prefer 2
 apply (simp only: less_Suc_eq_le)
 apply (subgoal_tac "length (clearjunk (del list (fst a))) \<le> length (del list (fst a))")
  prefer 2
  apply (rule clearjunk_length)
 apply (subgoal_tac "length (del list (fst a)) \<le> length list")
  prefer 2
  apply (rule del_length)
 apply (drule_tac y="length (del list (fst a))" and z="length list" in order_trans)
 apply assumption+
apply (drule mp, assumption)
apply (erule_tac x="clearjunk (del list (fst a))" in allE)
apply simp
apply (erule_tac x="b" in allE)
apply simp
apply (erule exE)
apply (subgoal_tac "clearjunk (del list (fst a)) ? aa = (del list (fst a)) ? aa")
 prefer 2
 apply  (rule clearjunk_lookup[THEN sym])
apply (rule_tac x="aa" in exI)
apply simp
apply (case_tac "fst a = aa")
apply simp

apply simp
apply (drule_tac x="fst a" and y="aa" and mp="list" in del_lookup_neq)
apply simp
(*>*)
done

lemma ran_src2:
"(\<exists> x. (mp ? x) = Some y) \<Longrightarrow> y \<in> (set (ran mp))"
(*<*)
apply (erule exE)
apply (rule_tac a="x" in some_lookup_range)
apply simp
(*>*)
done

lemma ran_del:
"\<And> m. set (ran (m#mp)) = {(snd m)} \<union>  (set (ran (del mp (fst m))))"
(*<*)
apply (rule set_ext)
apply (rule iffI)
apply (drule ran_src)
apply (erule exE)
apply simp
apply (case_tac "fst m = a")
apply simp
apply simp
apply (rule disjI2)
apply (drule not_sym)
apply (drule_tac m="mp" in del_lookup)
apply (simp only:)
apply (rule some_lookup_range)
apply simp

apply simp
apply (case_tac "x = snd m")
apply (rule ran_src2)
apply (rule_tac x="fst m" in exI)
apply simp

apply simp
apply (drule ran_src)
apply (erule exE)

apply (drule not_sym)
apply (case_tac "a = fst m")
apply (simp add: del_lookup_eq)

apply (frule_tac m="mp" in del_lookup)
apply (rule_tac a="a" in some_lookup_range)
apply (drule_tac t="a" in not_sym)
apply simp
(*>*)
done


lemma del_clearjunk:
"\<And> mp. del (clearjunk mp) x = clearjunk (del mp x)"
(*<*)
apply (subgoal_tac "\<exists> k. k=length mp")
 prefer 2
 apply simp
apply (erule exE)
apply (erule rev_mp)
apply (simp only: atomize_all)
apply (rule forall_switch2)
apply (rule allI)
apply (rule_tac n="k" in nat_less_induct)
apply (rule allI)
apply (rule impI)
apply (case_tac mp)
apply (simp add: del_def)

apply (simp only:)
apply (case_tac "fst a = x")
apply (simp only: del_simp1 clearjunk.simps)
apply (erule_tac x="length (del list x)" in allE)
apply (subgoal_tac "length (del list x) < length (a # list)")
 prefer 2
 apply simp
 apply (simp only: less_Suc_eq_le)
 apply (rule del_length)
apply (drule mp, assumption)
apply (erule_tac x="del list x" in allE)
apply (simp add: del_del)

apply (simp add: del_simp2 clearjunk.simps)
apply (subst del_switch)
apply (erule_tac x="length (del list (fst a))" in allE)
apply (subgoal_tac "length (del list (fst a)) < length (a # list)")
 prefer 2
 apply simp
 apply (simp only: less_Suc_eq_le)
 apply (rule del_length) 
apply simp
(*>*)
done

lemma clearjunk_m_clearjunk:
"\<And> m mp. clearjunk (m#clearjunk mp) = clearjunk (m#mp)"
(*<*)
apply (subgoal_tac "\<exists> k. k=length mp")
 prefer 2
 apply simp
apply (erule exE)
apply (erule rev_mp)
apply (simp only: atomize_all)
apply (rule forall_switch3)
apply (rule allI)
apply (rule_tac n="k" in nat_less_induct)
apply (rule allI)+
apply (rule impI)
apply (case_tac mp)
apply simp

apply simp
apply (case_tac "fst a = fst m")
apply (simp only: del_simp1)
apply (erule_tac x="length (del list (fst m))" in allE)
apply (subgoal_tac "length (del list (fst m)) < Suc (length list)")
 prefer 2
 apply (simp only: less_Suc_eq_le)
 apply (rule del_length)
apply (drule mp, assumption)
apply (erule_tac x="fst m" in allE)
apply (erule_tac x="del list (fst m)" in allE)
apply (simp add: del_del)
apply (subst del_simp2)
apply simp
apply (subst del_simp2)
apply simp
apply (simp add: clearjunk.simps)
apply (subst del_clearjunk)
apply (subst del_switch)
apply (erule_tac x="length (del list (fst a))" in allE)
apply (subgoal_tac "length (del list (fst a)) < Suc (length list)")
  prefer 2
 apply (simp only: less_Suc_eq_le)
 apply (rule del_length)
apply (drule mp, assumption)
apply (erule_tac x="fst m" in allE)
apply (erule_tac x="del list (fst a)" in allE)
apply simp
apply (subst del_switch)
apply (subst del_clearjunk)
apply (simp only: del_del)
apply (subgoal_tac " clearjunk (clearjunk (del (del list (fst m)) (fst a))) = clearjunk (del (clearjunk (del list (fst a))) (fst m))")
 prefer 2
 apply (subst del_switch)
 apply (subst del_clearjunk)
 apply simp
apply simp
apply (subst del_switch)
apply simp
(*>*)
done

lemma nojunk_mon:
"nojunk (m#mp) \<Longrightarrow> nojunk mp"
(*<*)
apply simp
apply (case_tac "mp ? fst m")
apply simp
apply simp
(*>*)
done

end