theory Lib

lemma fold_to_map_of:
  "fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) Map.empty = map_of (map (\<lambda>x. (f x, g x)) xs)" apply (rule ext) apply (rename_tac x) apply (case_tac "fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) Map.empty x") apply clarsimp apply (drule fold_ignore3) apply (clarsimp split:if_split_asm) apply (rule sym) apply (subst map_of_eq_None_iff) apply clarsimp apply (rename_tac xa) apply (erule_tac x=xa in ballE; clarsimp) apply clarsimp apply (frule fold_ignore5; clarsimp split:if_split_asm) apply (subst map_add_map_of_foldr[where m=Map.empty, simplified]) apply (induct xs arbitrary:f g; clarsimp split:if_split) apply (rule conjI; clarsimp) apply (drule fold_ignore9; clarsimp) apply (cut_tac ms="map (\<lambda>x. [f x \<mapsto> g x]) xs" and f="[f a \<mapsto> g a]" and x="f b" in fold_ignore6, clarsimp) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) = map_of (map (\<lambda>x. (f x, g x)) xs) proof (prove)
goal (1 subgoal):
 1. \<And>x. fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) x = map_of (map (\<lambda>x. (f x, g x)) xs) x proof (prove)
goal (1 subgoal):
 1. \<And>x. fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) x = map_of (map (\<lambda>x. (f x, g x)) xs) x proof (prove)
goal (2 subgoals):
 1. \<And>x. fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) x = None \<Longrightarrow> fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) x = map_of (map (\<lambda>x. (f x, g x)) xs) x
 2. \<And>x a. fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) x = Some a \<Longrightarrow> fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) x = map_of (map (\<lambda>x. (f x, g x)) xs) x proof (prove)
goal (2 subgoals):
 1. \<And>x. fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) x = None \<Longrightarrow> None = map_of (map (\<lambda>x. (f x, g x)) xs) x
 2. \<And>x a. fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) x = Some a \<Longrightarrow> fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) x = map_of (map (\<lambda>x. (f x, g x)) xs) x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<forall>b\<in>set (map (\<lambda>x. [f x \<mapsto> g x]) xs). b x = None \<Longrightarrow> None = map_of (map (\<lambda>x. (f x, g x)) xs) x
 2. \<And>x a. fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) x = Some a \<Longrightarrow> fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) x = map_of (map (\<lambda>x. (f x, g x)) xs) x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<forall>b\<in>set xs. x \<noteq> f b \<Longrightarrow> None = map_of (map (\<lambda>x. (f x, g x)) xs) x
 2. \<And>x a. fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) x = Some a \<Longrightarrow> fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) x = map_of (map (\<lambda>x. (f x, g x)) xs) x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<forall>b\<in>set xs. x \<noteq> f b \<Longrightarrow> map_of (map (\<lambda>x. (f x, g x)) xs) x = None
 2. \<And>x a. fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) x = Some a \<Longrightarrow> fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) x = map_of (map (\<lambda>x. (f x, g x)) xs) x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<forall>b\<in>set xs. x \<noteq> f b \<Longrightarrow> x \<notin> fst ` set (map (\<lambda>x. (f x, g x)) xs)
 2. \<And>x a. fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) x = Some a \<Longrightarrow> fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) x = map_of (map (\<lambda>x. (f x, g x)) xs) x proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>b\<in>set xs. f xa \<noteq> f b; xa \<in> set xs\<rbrakk> \<Longrightarrow> False
 2. \<And>x a. fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) x = Some a \<Longrightarrow> fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) x = map_of (map (\<lambda>x. (f x, g x)) xs) x proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>b\<in>set xs. f xa \<noteq> f b; xa \<in> set xs\<rbrakk> \<Longrightarrow> False
 2. \<And>x a. fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) x = Some a \<Longrightarrow> fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) x = map_of (map (\<lambda>x. (f x, g x)) xs) x proof (prove)
goal (1 subgoal):
 1. \<And>x a. fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) x = Some a \<Longrightarrow> fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) x = map_of (map (\<lambda>x. (f x, g x)) xs) x proof (prove)
goal (1 subgoal):
 1. \<And>x a. fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) x = Some a \<Longrightarrow> Some a = map_of (map (\<lambda>x. (f x, g x)) xs) x proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) (f b) = Some (g b); b \<in> set xs\<rbrakk> \<Longrightarrow> Some (g b) = map_of (map (\<lambda>x. (f x, g x)) xs) (f b) proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) (f b) = Some (g b); b \<in> set xs\<rbrakk> \<Longrightarrow> Some (g b) = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) (map (\<lambda>x. (f x, g x)) xs) (\<lambda>x. None) (f b) proof (prove)
goal (1 subgoal):
 1. \<And>a xs b f g. \<lbrakk>\<And>b f g. \<lbrakk>fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) (f b) = Some (g b); b \<in> set xs\<rbrakk> \<Longrightarrow> Some (g b) = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) (map (\<lambda>x. (f x, g x)) xs) (\<lambda>x. None) (f b); fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) [f a \<mapsto> g a] (f b) = Some (g b); b = a \<or> b \<in> set xs\<rbrakk> \<Longrightarrow> (f b = f a \<longrightarrow> g b = g a) \<and> (f b \<noteq> f a \<longrightarrow> Some (g b) = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) (map (\<lambda>x. (f x, g x)) xs) (\<lambda>x. None) (f b)) proof (prove)
goal (2 subgoals):
 1. \<And>a xs b f g. \<lbrakk>\<And>b f g. \<lbrakk>fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) (f b) = Some (g b); b \<in> set xs\<rbrakk> \<Longrightarrow> Some (g b) = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) (map (\<lambda>x. (f x, g x)) xs) (\<lambda>x. None) (f b); fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) [f a \<mapsto> g a] (f a) = Some (g b); b = a \<or> b \<in> set xs; f b = f a\<rbrakk> \<Longrightarrow> g b = g a
 2. \<And>a xs b f g. \<lbrakk>\<And>b f g. \<lbrakk>fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) (f b) = Some (g b); b \<in> set xs\<rbrakk> \<Longrightarrow> Some (g b) = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) (map (\<lambda>x. (f x, g x)) xs) (\<lambda>x. None) (f b); fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) [f a \<mapsto> g a] (f b) = Some (g b); b = a \<or> b \<in> set xs; f b \<noteq> f a\<rbrakk> \<Longrightarrow> Some (g b) = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) (map (\<lambda>x. (f x, g x)) xs) (\<lambda>x. None) (f b) proof (prove)
goal (1 subgoal):
 1. \<And>a xs b f g. \<lbrakk>\<And>b f g. \<lbrakk>fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) (f b) = Some (g b); b \<in> set xs\<rbrakk> \<Longrightarrow> Some (g b) = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) (map (\<lambda>x. (f x, g x)) xs) (\<lambda>x. None) (f b); fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) [f a \<mapsto> g a] (f b) = Some (g b); b = a \<or> b \<in> set xs; f b \<noteq> f a\<rbrakk> \<Longrightarrow> Some (g b) = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) (map (\<lambda>x. (f x, g x)) xs) (\<lambda>x. None) (f b) proof (prove)
goal (1 subgoal):
 1. \<And>a xs b f g. \<lbrakk>\<And>b f g. \<lbrakk>fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) (f b) = Some (g b); b \<in> set xs\<rbrakk> \<Longrightarrow> Some (g b) = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) (map (\<lambda>x. (f x, g x)) xs) (\<lambda>x. None) (f b); fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) [f a \<mapsto> g a] (f b) = Some (g b); b = a \<or> b \<in> set xs; f b \<noteq> f a; fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) [f a \<mapsto> g a] (f b) = fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) (\<lambda>x. None) (f b)\<rbrakk> \<Longrightarrow> Some (g b) = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) (map (\<lambda>x. (f x, g x)) xs) (\<lambda>x. None) (f b) proof (prove)
goal:
No subgoals!