theory Lib

lemma dom_unpack2:
  "dom (fold (++) ms Map.empty) = \<Union>(set (map dom ms))" apply (induct ms; clarsimp simp:dom_def) apply (rule equalityI; clarsimp) apply (drule fold_to_disj) apply (erule disjE) apply clarsimp apply (rename_tac b) apply (erule_tac x=b in ballE; clarsimp) apply clarsimp apply (rule conjI) apply clarsimp apply (rule_tac x=y in exI) apply (erule fold_ignore1) apply clarsimp apply (rename_tac y) apply (erule_tac y=y in fold_ignore4; clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom (fold (++) ms (\<lambda>x. None)) = \<Union> (set (map dom ms)) proof (prove)
goal (1 subgoal):
 1. \<And>a ms. {a. \<exists>y. fold (++) ms (\<lambda>x. None) a = Some y} = (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}) \<Longrightarrow> {aa. \<exists>y. fold (++) ms a aa = Some y} = {aa. \<exists>y. a aa = Some y} \<union> (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}) proof (prove)
goal (2 subgoals):
 1. \<And>a ms x y. \<lbrakk>{a. \<exists>y. fold (++) ms (\<lambda>x. None) a = Some y} = (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}); \<forall>xa\<in>set ms. xa x = None; fold (++) ms a x = Some y\<rbrakk> \<Longrightarrow> \<exists>y. a x = Some y
 2. \<And>a ms. {a. \<exists>y. fold (++) ms (\<lambda>x. None) a = Some y} = (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}) \<Longrightarrow> {aa. \<exists>y. a aa = Some y} \<subseteq> {aa. \<exists>y. fold (++) ms a aa = Some y} \<and> (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}) \<subseteq> {aa. \<exists>y. fold (++) ms a aa = Some y} proof (prove)
goal (2 subgoals):
 1. \<And>a ms x y. \<lbrakk>{a. \<exists>y. fold (++) ms (\<lambda>x. None) a = Some y} = (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}); \<forall>xa\<in>set ms. xa x = None; (\<exists>b\<in>set ms. b x = Some y) \<or> a x = Some y\<rbrakk> \<Longrightarrow> \<exists>y. a x = Some y
 2. \<And>a ms. {a. \<exists>y. fold (++) ms (\<lambda>x. None) a = Some y} = (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}) \<Longrightarrow> {aa. \<exists>y. a aa = Some y} \<subseteq> {aa. \<exists>y. fold (++) ms a aa = Some y} \<and> (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}) \<subseteq> {aa. \<exists>y. fold (++) ms a aa = Some y} proof (prove)
goal (3 subgoals):
 1. \<And>a ms x y. \<lbrakk>{a. \<exists>y. fold (++) ms (\<lambda>x. None) a = Some y} = (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}); \<forall>xa\<in>set ms. xa x = None; \<exists>b\<in>set ms. b x = Some y\<rbrakk> \<Longrightarrow> \<exists>y. a x = Some y
 2. \<And>a ms x y. \<lbrakk>{a. \<exists>y. fold (++) ms (\<lambda>x. None) a = Some y} = (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}); \<forall>xa\<in>set ms. xa x = None; a x = Some y\<rbrakk> \<Longrightarrow> \<exists>y. a x = Some y
 3. \<And>a ms. {a. \<exists>y. fold (++) ms (\<lambda>x. None) a = Some y} = (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}) \<Longrightarrow> {aa. \<exists>y. a aa = Some y} \<subseteq> {aa. \<exists>y. fold (++) ms a aa = Some y} \<and> (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}) \<subseteq> {aa. \<exists>y. fold (++) ms a aa = Some y} proof (prove)
goal (3 subgoals):
 1. \<And>a ms x y b. \<lbrakk>{a. \<exists>y. fold (++) ms (\<lambda>x. None) a = Some y} = (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}); \<forall>xa\<in>set ms. xa x = None; b \<in> set ms; b x = Some y\<rbrakk> \<Longrightarrow> \<exists>y. a x = Some y
 2. \<And>a ms x y. \<lbrakk>{a. \<exists>y. fold (++) ms (\<lambda>x. None) a = Some y} = (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}); \<forall>xa\<in>set ms. xa x = None; a x = Some y\<rbrakk> \<Longrightarrow> \<exists>y. a x = Some y
 3. \<And>a ms. {a. \<exists>y. fold (++) ms (\<lambda>x. None) a = Some y} = (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}) \<Longrightarrow> {aa. \<exists>y. a aa = Some y} \<subseteq> {aa. \<exists>y. fold (++) ms a aa = Some y} \<and> (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}) \<subseteq> {aa. \<exists>y. fold (++) ms a aa = Some y} proof (prove)
goal (3 subgoals):
 1. \<And>a ms x y b. \<lbrakk>{a. \<exists>y. fold (++) ms (\<lambda>x. None) a = Some y} = (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}); \<forall>xa\<in>set ms. xa x = None; b \<in> set ms; b x = Some y\<rbrakk> \<Longrightarrow> \<exists>y. a x = Some y
 2. \<And>a ms x y. \<lbrakk>{a. \<exists>y. fold (++) ms (\<lambda>x. None) a = Some y} = (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}); \<forall>xa\<in>set ms. xa x = None; a x = Some y\<rbrakk> \<Longrightarrow> \<exists>y. a x = Some y
 3. \<And>a ms. {a. \<exists>y. fold (++) ms (\<lambda>x. None) a = Some y} = (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}) \<Longrightarrow> {aa. \<exists>y. a aa = Some y} \<subseteq> {aa. \<exists>y. fold (++) ms a aa = Some y} \<and> (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}) \<subseteq> {aa. \<exists>y. fold (++) ms a aa = Some y} proof (prove)
goal (2 subgoals):
 1. \<And>a ms x y. \<lbrakk>{a. \<exists>y. fold (++) ms (\<lambda>x. None) a = Some y} = (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}); \<forall>xa\<in>set ms. xa x = None; a x = Some y\<rbrakk> \<Longrightarrow> \<exists>y. a x = Some y
 2. \<And>a ms. {a. \<exists>y. fold (++) ms (\<lambda>x. None) a = Some y} = (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}) \<Longrightarrow> {aa. \<exists>y. a aa = Some y} \<subseteq> {aa. \<exists>y. fold (++) ms a aa = Some y} \<and> (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}) \<subseteq> {aa. \<exists>y. fold (++) ms a aa = Some y} proof (prove)
goal (1 subgoal):
 1. \<And>a ms. {a. \<exists>y. fold (++) ms (\<lambda>x. None) a = Some y} = (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}) \<Longrightarrow> {aa. \<exists>y. a aa = Some y} \<subseteq> {aa. \<exists>y. fold (++) ms a aa = Some y} \<and> (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}) \<subseteq> {aa. \<exists>y. fold (++) ms a aa = Some y} proof (prove)
goal (2 subgoals):
 1. \<And>a ms. {a. \<exists>y. fold (++) ms (\<lambda>x. None) a = Some y} = (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}) \<Longrightarrow> {aa. \<exists>y. a aa = Some y} \<subseteq> {aa. \<exists>y. fold (++) ms a aa = Some y}
 2. \<And>a ms. {a. \<exists>y. fold (++) ms (\<lambda>x. None) a = Some y} = (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}) \<Longrightarrow> (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}) \<subseteq> {aa. \<exists>y. fold (++) ms a aa = Some y} proof (prove)
goal (2 subgoals):
 1. \<And>a ms x y. \<lbrakk>{a. \<exists>y. fold (++) ms (\<lambda>x. None) a = Some y} = (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}); a x = Some y\<rbrakk> \<Longrightarrow> \<exists>y. fold (++) ms a x = Some y
 2. \<And>a ms. {a. \<exists>y. fold (++) ms (\<lambda>x. None) a = Some y} = (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}) \<Longrightarrow> (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}) \<subseteq> {aa. \<exists>y. fold (++) ms a aa = Some y} proof (prove)
goal (2 subgoals):
 1. \<And>a ms x y. \<lbrakk>{a. \<exists>y. fold (++) ms (\<lambda>x. None) a = Some y} = (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}); a x = Some y\<rbrakk> \<Longrightarrow> fold (++) ms a x = Some y
 2. \<And>a ms. {a. \<exists>y. fold (++) ms (\<lambda>x. None) a = Some y} = (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}) \<Longrightarrow> (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}) \<subseteq> {aa. \<exists>y. fold (++) ms a aa = Some y} proof (prove)
goal (1 subgoal):
 1. \<And>a ms. {a. \<exists>y. fold (++) ms (\<lambda>x. None) a = Some y} = (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}) \<Longrightarrow> (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}) \<subseteq> {aa. \<exists>y. fold (++) ms a aa = Some y} proof (prove)
goal (1 subgoal):
 1. \<And>a ms x xa y. \<lbrakk>{a. \<exists>y. fold (++) ms (\<lambda>x. None) a = Some y} = (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}); xa \<in> set ms; xa x = Some y\<rbrakk> \<Longrightarrow> \<exists>y. fold (++) ms a x = Some y proof (prove)
goal (1 subgoal):
 1. \<And>a ms x xa y. \<lbrakk>{a. \<exists>y. fold (++) ms (\<lambda>x. None) a = Some y} = (\<Union>a\<in>set ms. {aa. \<exists>y. a aa = Some y}); xa \<in> set ms; xa x = Some y\<rbrakk> \<Longrightarrow> \<exists>y. fold (++) ms a x = Some y proof (prove)
goal:
No subgoals!