theory Lib

lemma foldr_upd_dom:
  "dom (foldr (\<lambda>p ps. ps (p \<mapsto> f p)) as g) = dom g \<union> set as" proof (induct as) case Nil thus ?case by simp next case (Cons a as) show ?case proof (cases "a \<in> set as \<or> a \<in> dom g") case True hence ain: "a \<in> dom g \<union> set as" by auto hence "dom g \<union> set (a # as) = dom g \<union> set as" by auto thus ?thesis using Cons by fastforce next case False hence "a \<notin> (dom g \<union> set as)" by simp hence "dom g \<union> set (a # as) = insert a (dom g \<union> set as)" by simp thus ?thesis using Cons by fastforce qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g) = dom g \<union> set as proof (state)
goal (2 subgoals):
 1. dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) [] g) = dom g \<union> set []
 2. \<And>a as. dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g) = dom g \<union> set as \<Longrightarrow> dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g) = dom g \<union> set (a # as) proof (state)
this:


goal (2 subgoals):
 1. dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) [] g) = dom g \<union> set []
 2. \<And>a as. dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g) = dom g \<union> set as \<Longrightarrow> dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g) = dom g \<union> set (a # as) proof (prove)
goal (1 subgoal):
 1. dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) [] g) = dom g \<union> set [] proof (state)
this:
dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) [] g) = dom g \<union> set []

goal (1 subgoal):
 1. \<And>a as. dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g) = dom g \<union> set as \<Longrightarrow> dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g) = dom g \<union> set (a # as) proof (state)
goal (1 subgoal):
 1. \<And>a as. dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g) = dom g \<union> set as \<Longrightarrow> dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g) = dom g \<union> set (a # as) proof (state)
this:
dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g) = dom g \<union> set as

goal (1 subgoal):
 1. \<And>a as. dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g) = dom g \<union> set as \<Longrightarrow> dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g) = dom g \<union> set (a # as) proof (prove)
goal (1 subgoal):
 1. dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g) = dom g \<union> set (a # as) proof (state)
goal (2 subgoals):
 1. a \<in> set as \<or> a \<in> dom g \<Longrightarrow> dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g) = dom g \<union> set (a # as)
 2. \<not> (a \<in> set as \<or> a \<in> dom g) \<Longrightarrow> dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g) = dom g \<union> set (a # as) proof (state)
this:
a \<in> set as \<or> a \<in> dom g

goal (2 subgoals):
 1. a \<in> set as \<or> a \<in> dom g \<Longrightarrow> dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g) = dom g \<union> set (a # as)
 2. \<not> (a \<in> set as \<or> a \<in> dom g) \<Longrightarrow> dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g) = dom g \<union> set (a # as) proof (prove)
using this:
a \<in> set as \<or> a \<in> dom g

goal (1 subgoal):
 1. a \<in> dom g \<union> set as proof (state)
this:
a \<in> dom g \<union> set as

goal (2 subgoals):
 1. a \<in> set as \<or> a \<in> dom g \<Longrightarrow> dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g) = dom g \<union> set (a # as)
 2. \<not> (a \<in> set as \<or> a \<in> dom g) \<Longrightarrow> dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g) = dom g \<union> set (a # as) proof (prove)
using this:
a \<in> dom g \<union> set as

goal (1 subgoal):
 1. dom g \<union> set (a # as) = dom g \<union> set as proof (state)
this:
dom g \<union> set (a # as) = dom g \<union> set as

goal (2 subgoals):
 1. a \<in> set as \<or> a \<in> dom g \<Longrightarrow> dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g) = dom g \<union> set (a # as)
 2. \<not> (a \<in> set as \<or> a \<in> dom g) \<Longrightarrow> dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g) = dom g \<union> set (a # as) proof (prove)
using this:
dom g \<union> set (a # as) = dom g \<union> set as

goal (1 subgoal):
 1. dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g) = dom g \<union> set (a # as) proof (prove)
using this:
dom g \<union> set (a # as) = dom g \<union> set as
dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g) = dom g \<union> set as

goal (1 subgoal):
 1. dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g) = dom g \<union> set (a # as) proof (state)
this:
dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g) = dom g \<union> set (a # as)

goal (1 subgoal):
 1. \<not> (a \<in> set as \<or> a \<in> dom g) \<Longrightarrow> dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g) = dom g \<union> set (a # as) proof (state)
goal (1 subgoal):
 1. \<not> (a \<in> set as \<or> a \<in> dom g) \<Longrightarrow> dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g) = dom g \<union> set (a # as) proof (state)
this:
\<not> (a \<in> set as \<or> a \<in> dom g)

goal (1 subgoal):
 1. \<not> (a \<in> set as \<or> a \<in> dom g) \<Longrightarrow> dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g) = dom g \<union> set (a # as) proof (prove)
using this:
\<not> (a \<in> set as \<or> a \<in> dom g)

goal (1 subgoal):
 1. a \<notin> dom g \<union> set as proof (state)
this:
a \<notin> dom g \<union> set as

goal (1 subgoal):
 1. \<not> (a \<in> set as \<or> a \<in> dom g) \<Longrightarrow> dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g) = dom g \<union> set (a # as) proof (prove)
using this:
a \<notin> dom g \<union> set as

goal (1 subgoal):
 1. dom g \<union> set (a # as) = insert a (dom g \<union> set as) proof (state)
this:
dom g \<union> set (a # as) = insert a (dom g \<union> set as)

goal (1 subgoal):
 1. \<not> (a \<in> set as \<or> a \<in> dom g) \<Longrightarrow> dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g) = dom g \<union> set (a # as) proof (prove)
using this:
dom g \<union> set (a # as) = insert a (dom g \<union> set as)

goal (1 subgoal):
 1. dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g) = dom g \<union> set (a # as) proof (prove)
using this:
dom g \<union> set (a # as) = insert a (dom g \<union> set as)
dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g) = dom g \<union> set as

goal (1 subgoal):
 1. dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g) = dom g \<union> set (a # as) proof (state)
this:
dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g) = dom g \<union> set (a # as)

goal:
No subgoals! proof (state)
this:
dom (foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g) = dom g \<union> set (a # as)

goal:
No subgoals!