theory Detype_C

lemma map_of_le:
  "map_le (map_of xs) m \<Longrightarrow> distinct (map fst xs) \<Longrightarrow> \<forall>(x, v) \<in> set xs. m x = Some v" apply (induct xs) apply simp apply clarsimp apply (clarsimp simp: map_le_def dom_map_of_conv_image_fst) apply (drule(1) bspec, simp) apply (simp(no_asm_use) split: if_split_asm) apply (fastforce simp: image_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>map_of xs \<subseteq>\<^sub>m m; distinct (map fst xs)\<rbrakk> \<Longrightarrow> \<forall>(x, v)\<in>set xs. m x = Some v proof (prove)
goal (2 subgoals):
 1. \<lbrakk>map_of [] \<subseteq>\<^sub>m m; distinct (map fst [])\<rbrakk> \<Longrightarrow> \<forall>(x, v)\<in>set []. m x = Some v
 2. \<And>x1 xs. \<lbrakk>\<lbrakk>map_of xs \<subseteq>\<^sub>m m; distinct (map fst xs)\<rbrakk> \<Longrightarrow> \<forall>(x, v)\<in>set xs. m x = Some v; map_of (x1 # xs) \<subseteq>\<^sub>m m; distinct (map fst (x1 # xs))\<rbrakk> \<Longrightarrow> \<forall>(x, v)\<in>set (x1 # xs). m x = Some v proof (prove)
goal (1 subgoal):
 1. \<And>x1 xs. \<lbrakk>\<lbrakk>map_of xs \<subseteq>\<^sub>m m; distinct (map fst xs)\<rbrakk> \<Longrightarrow> \<forall>(x, v)\<in>set xs. m x = Some v; map_of (x1 # xs) \<subseteq>\<^sub>m m; distinct (map fst (x1 # xs))\<rbrakk> \<Longrightarrow> \<forall>(x, v)\<in>set (x1 # xs). m x = Some v proof (prove)
goal (1 subgoal):
 1. \<And>a b xs. \<lbrakk>map_of xs \<subseteq>\<^sub>m m \<Longrightarrow> \<forall>x\<in>set xs. case x of (x, v) \<Rightarrow> m x = Some v; (map_of xs)(a \<mapsto> b) \<subseteq>\<^sub>m m; a \<notin> fst ` set xs; distinct (map fst xs)\<rbrakk> \<Longrightarrow> m a = Some b \<and> (\<forall>x\<in>set xs. case x of (x, v) \<Rightarrow> m x = Some v) proof (prove)
goal (1 subgoal):
 1. \<And>a b xs aa ba. \<lbrakk>\<forall>a\<in>set xs. map_of xs (fst a) = m (fst a) \<Longrightarrow> \<forall>x\<in>set xs. case x of (x, v) \<Rightarrow> m x = Some v; a \<notin> fst ` set xs; distinct (map fst xs); (aa, ba) \<in> set xs; Some b = m a; \<forall>aa\<in>set xs. (if fst aa = a then Some b else map_of xs (fst aa)) = m (fst aa)\<rbrakk> \<Longrightarrow> m aa = Some ba proof (prove)
goal (1 subgoal):
 1. \<And>a b xs aa ba. \<lbrakk>\<forall>a\<in>set xs. map_of xs (fst a) = m (fst a) \<Longrightarrow> \<forall>x\<in>set xs. case x of (x, v) \<Rightarrow> m x = Some v; a \<notin> fst ` set xs; distinct (map fst xs); (aa, ba) \<in> set xs; Some b = m a; (if aa = a then Some b else map_of xs (fst (aa, ba))) = m aa\<rbrakk> \<Longrightarrow> m aa = Some ba proof (prove)
goal (2 subgoals):
 1. \<And>a b xs aa ba. \<lbrakk>\<forall>a\<in>set xs. map_of xs (fst a) = m (fst a) \<Longrightarrow> \<forall>x\<in>set xs. case x of (x, v) \<Rightarrow> m x = Some v; a \<notin> fst ` set xs; distinct (map fst xs); (aa, ba) \<in> set xs; Some b = m a; aa = a; Some b = m aa\<rbrakk> \<Longrightarrow> m aa = Some ba
 2. \<And>a b xs aa ba. \<lbrakk>\<forall>a\<in>set xs. map_of xs (fst a) = m (fst a) \<Longrightarrow> \<forall>x\<in>set xs. case x of (x, v) \<Rightarrow> m x = Some v; a \<notin> fst ` set xs; distinct (map fst xs); (aa, ba) \<in> set xs; Some b = m a; aa \<noteq> a; map_of xs aa = m aa\<rbrakk> \<Longrightarrow> m aa = Some ba proof (prove)
goal (1 subgoal):
 1. \<And>a b xs aa ba. \<lbrakk>\<forall>a\<in>set xs. map_of xs (fst a) = m (fst a) \<Longrightarrow> \<forall>x\<in>set xs. case x of (x, v) \<Rightarrow> m x = Some v; a \<notin> fst ` set xs; distinct (map fst xs); (aa, ba) \<in> set xs; Some b = m a; aa \<noteq> a; map_of xs aa = m aa\<rbrakk> \<Longrightarrow> m aa = Some ba proof (prove)
goal:
No subgoals!