kings-crown/FVELER_Isabelle huggingface dataset:
theory Lib

lemma Ball_conj_increase:
  "xs \<noteq> {} \<Longrightarrow> (( \<forall>x \<in> xs. P x) \<and> Q) = (\<forall>x \<in> xs. P x \<and> Q)"
  "xs \<noteq> {} \<Longrightarrow> (R \<and> (\<forall>x \<in> xs. S x)) = (\<forall>x \<in> xs. R \<and> S x)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (xs \<noteq> {} \<Longrightarrow> ((\<forall>x\<in>xs. P x) \<and> Q) = (\<forall>x\<in>xs. P x \<and> Q)) &&& (xs \<noteq> {} \<Longrightarrow> (R \<and> (\<forall>x\<in>xs. S x)) = (\<forall>x\<in>xs. R \<and> S x))
theory Lib

lemma disjoint_subset:
  assumes "A' \<subseteq> A" and "A \<inter> B = {}"
  shows   "A' \<inter> B = {}" using assms by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A' \<inter> B = {} proof (prove)
using this:
A' \<subseteq> A
A \<inter> B = {}

goal (1 subgoal):
 1. A' \<inter> B = {}
theory Lib

lemma disjoint_subset2:
  assumes "B' \<subseteq> B" and "A \<inter> B = {}"
  shows   "A \<inter> B' = {}" using assms by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A \<inter> B' = {} proof (prove)
using this:
B' \<subseteq> B
A \<inter> B = {}

goal (1 subgoal):
 1. A \<inter> B' = {}
theory Lib

lemma UN_nth_mem:
  "i < length xs \<Longrightarrow> f (xs ! i) \<subseteq> (\<Union>x\<in>set xs. f x)" by (metis UN_upper nth_mem)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i < length xs \<Longrightarrow> f (xs ! i) \<subseteq> \<Union> (f ` set xs)
theory Lib

lemma Union_equal:
  "f ` A = f ` B \<Longrightarrow> (\<Union>x \<in> A. f x) = (\<Union>x \<in> B. f x)" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f ` A = f ` B \<Longrightarrow> \<Union> (f ` A) = \<Union> (f ` B)
theory Lib

lemma UN_Diff_disjoint:
  "i < length xs \<Longrightarrow> (A - (\<Union>x\<in>set xs. f x)) \<inter> f (xs ! i) = {}" by (metis Diff_disjoint Int_commute UN_nth_mem disjoint_subset)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i < length xs \<Longrightarrow> (A - \<Union> (f ` set xs)) \<inter> f (xs ! i) = {}
theory Lib

lemma image_list_update:
  "f a = f (xs ! i)
  \<Longrightarrow> f ` set (xs [i := a]) = f ` set xs" by (metis list_update_id map_update set_map)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f a = f (xs ! i) \<Longrightarrow> f ` set (xs[i := a]) = f ` set xs
theory Lib

lemma Union_list_update_id:
  "f a = f (xs ! i) \<Longrightarrow> (\<Union>x\<in>set (xs [i := a]). f x) = (\<Union>x\<in>set xs. f x)" by (rule Union_equal) (erule image_list_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f a = f (xs ! i) \<Longrightarrow> \<Union> (f ` set (xs[i := a])) = \<Union> (f ` set xs)
theory Lib

lemma Union_list_update_id':
  "\<lbrakk>i < length xs; \<And>x. g (f x) = g x\<rbrakk>
  \<Longrightarrow> (\<Union>x\<in>set (xs [i := f (xs ! i)]). g x) = (\<Union>x\<in>set xs. g x)" by (metis Union_list_update_id)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < length xs; \<And>x. g (f x) = g x\<rbrakk> \<Longrightarrow> \<Union> (g ` set (xs[i := f (xs ! i)])) = \<Union> (g ` set xs)
theory Lib

lemma Union_subset:
  "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> (f x) \<subseteq> (g x)\<rbrakk> \<Longrightarrow> (\<Union>x \<in> A. f x) \<subseteq> (\<Union>x \<in> A. g x)" by (metis UN_mono order_refl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> \<Union> (f ` A) \<subseteq> \<Union> (g ` A)
theory Lib

lemma bij_betw_fun_updI:
  "\<lbrakk>x \<notin> A; y \<notin> B; bij_betw f A B\<rbrakk> \<Longrightarrow> bij_betw (f(x := y)) (insert x A) (insert y B)" by (clarsimp simp: bij_betw_def fun_upd_image inj_on_fun_updI split: if_split_asm; blast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<notin> A; y \<notin> B; bij_betw f A B\<rbrakk> \<Longrightarrow> bij_betw (f(x := y)) (insert x A) (insert y B)
theory Lib

lemma bij_betw_map_fun_updI:
  "\<lbrakk>x \<notin> A; y \<notin> B; bij_betw_map f A B\<rbrakk>
  \<Longrightarrow> bij_betw_map (f(x \<mapsto> y)) (insert x A) (insert y B)" unfolding bij_betw_map_def by clarsimp (erule bij_betw_fun_updI; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<notin> A; y \<notin> B; bij_betw_map f A B\<rbrakk> \<Longrightarrow> bij_betw_map (f(x \<mapsto> y)) (insert x A) (insert y B) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<notin> A; y \<notin> B; bij_betw f A (Some ` B)\<rbrakk> \<Longrightarrow> bij_betw (f(x \<mapsto> y)) (insert x A) (Some ` insert y B)
theory Lib

lemma bij_betw_map_imp_inj_on:
  "bij_betw_map f A B \<Longrightarrow> inj_on f A" by (simp add: bij_betw_map_def bij_betw_imp_inj_on)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bij_betw_map f A B \<Longrightarrow> inj_on f A
theory Lib

lemma bij_betw_empty_dom_exists:
  "r = {} \<Longrightarrow> \<exists>t. bij_betw t {} r" by (clarsimp simp: bij_betw_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. r = {} \<Longrightarrow> \<exists>t. bij_betw t {} r
theory Lib

lemma bij_betw_map_empty_dom_exists:
  "r = {} \<Longrightarrow> \<exists>t. bij_betw_map t {} r" by (clarsimp simp: bij_betw_map_def bij_betw_empty_dom_exists)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. r = {} \<Longrightarrow> \<exists>t. bij_betw_map t {} r
theory Lib

lemma funpow_add [simp]:
  fixes f :: "'a \<Rightarrow> 'a"
  shows "(f ^^ a) ((f ^^ b) s) = (f ^^ (a + b)) s" by (metis comp_apply funpow_add)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (f ^^ a) ((f ^^ b) s) = (f ^^ (a + b)) s
theory Lib

lemma funpow_unfold:
  fixes f :: "'a \<Rightarrow> 'a"
  assumes "n > 0"
  shows "f ^^ n = (f ^^ (n - 1)) \<circ> f" by (metis Suc_diff_1 assms funpow_Suc_right)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f ^^ n = f ^^ (n - 1) \<circ> f
theory Lib

lemma relpow_unfold: "n > 0 \<Longrightarrow> S ^^ n = (S ^^ (n - 1)) O S" by (cases n, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> S ^^ n = S ^^ (n - 1) O S
theory Lib

lemma equiv_of_is_equiv_relation [simp]:
   "equiv UNIV (equiv_of proj)" by (auto simp: equiv_of_def intro!: equivI refl_onI symI transI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv UNIV (equiv_of proj)
theory Lib

lemma equiv_relation_to_projection:
  fixes R :: "('a \<times> 'a) set"
  assumes equiv: "equiv UNIV R"
  shows "\<exists>f :: 'a \<Rightarrow> 'a set. \<forall>x y. f x = f y \<longleftrightarrow> (x, y) \<in> R" apply (rule exI [of _ "\<lambda>x. {y. (x, y) \<in> R}"]) apply clarsimp apply (case_tac "(x, y) \<in> R") apply clarsimp apply (rule set_eqI) apply clarsimp apply (metis equivE sym_def trans_def equiv) apply (clarsimp) apply (metis UNIV_I equiv equivE mem_Collect_eq refl_on_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>f. \<forall>x y. (f x = f y) = ((x, y) \<in> R) proof (prove)
goal (1 subgoal):
 1. \<forall>x y. ({y. (x, y) \<in> R} = {ya. (y, ya) \<in> R}) = ((x, y) \<in> R) proof (prove)
goal (1 subgoal):
 1. \<And>x y. ({y. (x, y) \<in> R} = {ya. (y, ya) \<in> R}) = ((x, y) \<in> R) proof (prove)
goal (2 subgoals):
 1. \<And>x y. (x, y) \<in> R \<Longrightarrow> ({y. (x, y) \<in> R} = {ya. (y, ya) \<in> R}) = ((x, y) \<in> R)
 2. \<And>x y. (x, y) \<notin> R \<Longrightarrow> ({y. (x, y) \<in> R} = {ya. (y, ya) \<in> R}) = ((x, y) \<in> R) proof (prove)
goal (2 subgoals):
 1. \<And>x y. (x, y) \<in> R \<Longrightarrow> {y. (x, y) \<in> R} = {ya. (y, ya) \<in> R}
 2. \<And>x y. (x, y) \<notin> R \<Longrightarrow> ({y. (x, y) \<in> R} = {ya. (y, ya) \<in> R}) = ((x, y) \<in> R) proof (prove)
goal (2 subgoals):
 1. \<And>x y xa. (x, y) \<in> R \<Longrightarrow> (xa \<in> {y. (x, y) \<in> R}) = (xa \<in> {ya. (y, ya) \<in> R})
 2. \<And>x y. (x, y) \<notin> R \<Longrightarrow> ({y. (x, y) \<in> R} = {ya. (y, ya) \<in> R}) = ((x, y) \<in> R) proof (prove)
goal (2 subgoals):
 1. \<And>x y xa. (x, y) \<in> R \<Longrightarrow> ((x, xa) \<in> R) = ((y, xa) \<in> R)
 2. \<And>x y. (x, y) \<notin> R \<Longrightarrow> ({y. (x, y) \<in> R} = {ya. (y, ya) \<in> R}) = ((x, y) \<in> R) proof (prove)
goal (1 subgoal):
 1. \<And>x y. (x, y) \<notin> R \<Longrightarrow> ({y. (x, y) \<in> R} = {ya. (y, ya) \<in> R}) = ((x, y) \<in> R) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>(x, y) \<notin> R; {y. (x, y) \<in> R} = {ya. (y, ya) \<in> R}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Lib

lemma range_constant [simp]:
  "range (\<lambda>_. k) = {k}" by (clarsimp simp: image_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. range (\<lambda>_. k) = {k}
theory Lib

lemma dom_unpack:
  "dom (map_of (map (\<lambda>x. (f x, g x)) xs)) = set (map (\<lambda>x. f x) xs)" by (simp add: dom_map_of_conv_image_fst image_image)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom (map_of (map (\<lambda>x. (f x, g x)) xs)) = set (map f xs)
theory Lib

lemma fold_to_disj:
"fold (++) ms a x = Some y \<Longrightarrow> (\<exists>b \<in> set ms. b x = Some y) \<or> a x = Some y" by (induct ms arbitrary:a x y; clarsimp) blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fold (++) ms a x = Some y \<Longrightarrow> (\<exists>b\<in>set ms. b x = Some y) \<or> a x = Some y
theory Lib

lemma fold_ignore1:
  "a x = Some y \<Longrightarrow> fold (++) ms a x = Some y" by (induct ms arbitrary:a x y; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a x = Some y \<Longrightarrow> fold (++) ms a x = Some y
theory Lib

lemma fold_ignore2:
  "fold (++) ms a x = None \<Longrightarrow> a x = None" by (metis fold_ignore1 option.collapse)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fold (++) ms a x = None \<Longrightarrow> a x = None
theory Lib

lemma fold_ignore3:
  "fold (++) ms a x = None \<Longrightarrow> (\<forall>b \<in> set ms. b x = None)" by (induct ms arbitrary:a x; clarsimp) (meson fold_ignore2 map_add_None)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fold (++) ms a x = None \<Longrightarrow> \<forall>b\<in>set ms. b x = None
theory Lib

lemma fold_ignore4:
  "b \<in> set ms \<Longrightarrow> b x = Some y \<Longrightarrow> \<exists>y. fold (++) ms a x = Some y" using fold_ignore3 by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b \<in> set ms; b x = Some y\<rbrakk> \<Longrightarrow> \<exists>y. fold (++) ms a x = Some y proof (prove)
using this:
fold (++) ?ms ?a ?x = None \<Longrightarrow> \<forall>b\<in>set ?ms. b ?x = None

goal (1 subgoal):
 1. \<lbrakk>b \<in> set ms; b x = Some y\<rbrakk> \<Longrightarrow> \<exists>y. fold (++) ms a x = Some y
theory Lib

lemma fold_ignore5:"fold (++) ms a x = Some y \<Longrightarrow> a x = Some y \<or> (\<exists>b \<in> set ms. b x = Some y)" by (induct ms arbitrary:a x y; clarsimp) blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fold (++) ms a x = Some y \<Longrightarrow> a x = Some y \<or> (\<exists>b\<in>set ms. b x = Some y)
theory Lib

lemma dom_inter_nothing:"dom f \<inter> dom g = {} \<Longrightarrow> \<forall>x. f x = None \<or> g x = None" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom f \<inter> dom g = {} \<Longrightarrow> \<forall>x. f x = None \<or> g x = None
theory Lib

lemma fold_ignore6:
  "f x = None \<Longrightarrow> fold (++) ms f x = fold (++) ms Map.empty x" apply (induct ms arbitrary:f x; clarsimp simp:map_add_def) by (metis (no_types, lifting) fold_ignore1 option.collapse option.simps(4))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f x = None \<Longrightarrow> fold (++) ms f x = fold (++) ms (\<lambda>x. None) x proof (prove)
goal (1 subgoal):
 1. \<And>a ms f x. \<lbrakk>\<And>f x. f x = None \<Longrightarrow> fold (++) ms f x = fold (++) ms (\<lambda>x. None) x; f x = None\<rbrakk> \<Longrightarrow> fold (++) ms (\<lambda>x. case f x of None \<Rightarrow> a x | Some y \<Rightarrow> Some y) x = fold (++) ms a x
theory Lib

lemma fold_ignore7:
  "m x = m' x \<Longrightarrow> fold (++) ms m x = fold (++) ms m' x" apply (case_tac "m x") apply (frule_tac ms=ms in fold_ignore6) apply (cut_tac f=m' and ms=ms and x=x in fold_ignore6) apply clarsimp+ apply (rename_tac a) apply (cut_tac ms=ms and a=m and x=x and y=a in fold_ignore1, clarsimp) apply (cut_tac ms=ms and a=m' and x=x and y=a in fold_ignore1; clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m x = m' x \<Longrightarrow> fold (++) ms m x = fold (++) ms m' x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m x = m' x; m x = None\<rbrakk> \<Longrightarrow> fold (++) ms m x = fold (++) ms m' x
 2. \<And>a. \<lbrakk>m x = m' x; m x = Some a\<rbrakk> \<Longrightarrow> fold (++) ms m x = fold (++) ms m' x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m x = m' x; m x = None; fold (++) ms m x = fold (++) ms (\<lambda>x. None) x\<rbrakk> \<Longrightarrow> fold (++) ms m x = fold (++) ms m' x
 2. \<And>a. \<lbrakk>m x = m' x; m x = Some a\<rbrakk> \<Longrightarrow> fold (++) ms m x = fold (++) ms m' x proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m x = m' x; m x = None; fold (++) ms m x = fold (++) ms (\<lambda>x. None) x\<rbrakk> \<Longrightarrow> m' x = None
 2. \<lbrakk>m x = m' x; m x = None; fold (++) ms m x = fold (++) ms (\<lambda>x. None) x; fold (++) ms m' x = fold (++) ms (\<lambda>x. None) x\<rbrakk> \<Longrightarrow> fold (++) ms m x = fold (++) ms m' x
 3. \<And>a. \<lbrakk>m x = m' x; m x = Some a\<rbrakk> \<Longrightarrow> fold (++) ms m x = fold (++) ms m' x proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>Some a = m' x; m x = m' x\<rbrakk> \<Longrightarrow> fold (++) ms m x = fold (++) ms m' x proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>Some a = m' x; m x = m' x\<rbrakk> \<Longrightarrow> fold (++) ms m x = fold (++) ms m' x proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>Some a = m' x; m x = m' x; fold (++) ms m x = Some a\<rbrakk> \<Longrightarrow> fold (++) ms m x = fold (++) ms m' x proof (prove)
goal:
No subgoals!
theory Lib

lemma fold_ignore9:
  "\<lbrakk>fold (++) ms [x \<mapsto> y] x' = Some z; x = x'\<rbrakk> \<Longrightarrow> y = z" by (subst (asm) fold_ignore8) clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fold (++) ms [x \<mapsto> y] x' = Some z; x = x'\<rbrakk> \<Longrightarrow> y = z
theory Lib

lemma if_n_0_0:
  "((if P then n else 0) \<noteq> 0) = (P \<and> n \<noteq> 0)" by (simp split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((if P then n else (0::'a)) \<noteq> (0::'a)) = (P \<and> n \<noteq> (0::'a))
theory Lib

lemma map_comp_subset_dom:
  "dom (prj \<circ>\<^sub>m f) \<subseteq> dom f" unfolding dom_def by (auto simp: map_comp_Some_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom (prj \<circ>\<^sub>m f) \<subseteq> dom f proof (prove)
goal (1 subgoal):
 1. {a. (prj \<circ>\<^sub>m f) a \<noteq> None} \<subseteq> {a. f a \<noteq> None}
theory Lib

lemma dom_map_comp:
  "x \<in> dom (prj \<circ>\<^sub>m f) = (\<exists>y z. f x = Some y \<and> prj y = Some z)" by (fastforce simp: dom_def map_comp_Some_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x \<in> dom (prj \<circ>\<^sub>m f)) = (\<exists>y z. f x = Some y \<and> prj y = Some z)
theory Lib

lemma map_option_Some_eq2:
  "(Some y = map_option f x) = (\<exists>z. x = Some z \<and> f z = y)" by (metis map_option_eq_Some)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Some y = map_option f x) = (\<exists>z. x = Some z \<and> f z = y)
theory Lib

lemma singleton_eq_o2s:
  "({x} = set_option v) = (v = Some x)" by (cases v, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ({x} = set_option v) = (v = Some x)
theory Lib

lemma option_set_singleton_eq:
  "(set_option opt = {v}) = (opt = Some v)" by (cases opt, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (set_option opt = {v}) = (opt = Some v)
theory Lib

lemma map_option_comp2:
  "map_option (f o g) = map_option f o map_option g" by (simp add: option.map_comp fun_eq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_option (f \<circ> g) = map_option f \<circ> map_option g
theory Lib

lemma compD:
  "\<lbrakk>f \<circ> g = f \<circ> g'; g x = v \<rbrakk> \<Longrightarrow> f (g' x) = f v" by (metis comp_apply)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<circ> g = f \<circ> g'; g x = v\<rbrakk> \<Longrightarrow> f (g' x) = f v
theory Lib

lemma map_option_comp_eqE:
  assumes om: "map_option f \<circ> mp = map_option f \<circ> mp'"
  and     p1: "\<lbrakk> mp x = None; mp' x = None \<rbrakk> \<Longrightarrow> P"
  and     p2: "\<And>v v'. \<lbrakk> mp x = Some v; mp' x = Some v'; f v = f v' \<rbrakk> \<Longrightarrow> P"
  shows "P" proof (cases "mp x") case None hence "x \<notin> dom mp" by (simp add: domIff) hence "mp' x = None" by (simp add: map_option_eq_dom_eq [OF om] domIff) with None show ?thesis by (rule p1) next case (Some v) hence "x \<in> dom mp" by clarsimp then obtain v' where Some': "mp' x = Some v'" by (clarsimp simp add: map_option_eq_dom_eq [OF om]) with Some show ?thesis proof (rule p2) show "f v = f v'" using Some' compD [OF om, OF Some] by simp qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P proof (state)
goal (2 subgoals):
 1. mp x = None \<Longrightarrow> P
 2. \<And>a. mp x = Some a \<Longrightarrow> P proof (state)
this:
mp x = None

goal (2 subgoals):
 1. mp x = None \<Longrightarrow> P
 2. \<And>a. mp x = Some a \<Longrightarrow> P proof (prove)
using this:
mp x = None

goal (1 subgoal):
 1. x \<notin> dom mp proof (state)
this:
x \<notin> dom mp

goal (2 subgoals):
 1. mp x = None \<Longrightarrow> P
 2. \<And>a. mp x = Some a \<Longrightarrow> P proof (prove)
using this:
x \<notin> dom mp

goal (1 subgoal):
 1. mp' x = None proof (state)
this:
mp' x = None

goal (2 subgoals):
 1. mp x = None \<Longrightarrow> P
 2. \<And>a. mp x = Some a \<Longrightarrow> P proof (chain)
picking this:
mp x = None
mp' x = None proof (prove)
using this:
mp x = None
mp' x = None

goal (1 subgoal):
 1. P proof (state)
this:
P

goal (1 subgoal):
 1. \<And>a. mp x = Some a \<Longrightarrow> P proof (state)
goal (1 subgoal):
 1. \<And>a. mp x = Some a \<Longrightarrow> P proof (state)
this:
mp x = Some v

goal (1 subgoal):
 1. \<And>a. mp x = Some a \<Longrightarrow> P proof (prove)
using this:
mp x = Some v

goal (1 subgoal):
 1. x \<in> dom mp proof (state)
this:
x \<in> dom mp

goal (1 subgoal):
 1. \<And>a. mp x = Some a \<Longrightarrow> P proof (chain)
picking this:
x \<in> dom mp proof (prove)
using this:
x \<in> dom mp

goal (1 subgoal):
 1. (\<And>v'. mp' x = Some v' \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
mp' x = Some v'

goal (1 subgoal):
 1. \<And>a. mp x = Some a \<Longrightarrow> P proof (chain)
picking this:
mp x = Some v
mp' x = Some v' proof (prove)
using this:
mp x = Some v
mp' x = Some v'

goal (1 subgoal):
 1. P proof (state)
goal (1 subgoal):
 1. f v = f v' proof (prove)
goal (1 subgoal):
 1. f v = f v' proof (prove)
using this:
mp' x = Some v'
map_option f (mp' x) = map_option f (Some v)

goal (1 subgoal):
 1. f v = f v' proof (state)
this:
f v = f v'

goal:
No subgoals! proof (state)
this:
P

goal:
No subgoals!
theory Lib

lemma Some_the:
  "x \<in> dom f \<Longrightarrow> f x = Some (the (f x))" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> dom f \<Longrightarrow> f x = Some (the (f x))
theory Lib

lemma map_comp_update:
  "f \<circ>\<^sub>m (g(x \<mapsto> v)) = (f \<circ>\<^sub>m g)(x := f v)" by (rule ext, rename_tac y) (case_tac "g y"; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f \<circ>\<^sub>m g(x \<mapsto> v) = (f \<circ>\<^sub>m g)(x := f v)
theory Lib

lemma restrict_map_eqI:
  assumes req: "A |` S = B |` S"
  and     mem: "x \<in> S"
  shows   "A x = B x" proof - from mem have "A x = (A |` S) x" by simp also have "\<dots> = (B |` S) x" using req by simp also have "\<dots> = B x" using mem by simp finally show ?thesis . qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A x = B x proof (state)
goal (1 subgoal):
 1. A x = B x proof (chain)
picking this:
x \<in> S proof (prove)
using this:
x \<in> S

goal (1 subgoal):
 1. A x = (A |` S) x proof (state)
this:
A x = (A |` S) x

goal (1 subgoal):
 1. A x = B x proof (state)
this:
A x = (A |` S) x

goal (1 subgoal):
 1. A x = B x proof (prove)
goal (1 subgoal):
 1. (A |` S) x = (B |` S) x proof (prove)
using this:
A |` S = B |` S

goal (1 subgoal):
 1. (A |` S) x = (B |` S) x proof (state)
this:
(A |` S) x = (B |` S) x

goal (1 subgoal):
 1. A x = B x proof (state)
this:
(A |` S) x = (B |` S) x

goal (1 subgoal):
 1. A x = B x proof (prove)
goal (1 subgoal):
 1. (B |` S) x = B x proof (prove)
using this:
x \<in> S

goal (1 subgoal):
 1. (B |` S) x = B x proof (state)
this:
(B |` S) x = B x

goal (1 subgoal):
 1. A x = B x proof (chain)
picking this:
A x = B x proof (prove)
using this:
A x = B x

goal (1 subgoal):
 1. A x = B x proof (state)
this:
A x = B x

goal:
No subgoals!
theory Lib

lemma map_comp_eqI:
  assumes dm: "dom g = dom g'"
  and     fg: "\<And>x. x \<in> dom g' \<Longrightarrow> f (the (g' x)) = f (the (g x))"
  shows  "f \<circ>\<^sub>m g = f \<circ>\<^sub>m g'" apply (rule ext) apply (case_tac "x \<in> dom g") apply (frule subst [OF dm]) apply (clarsimp split: option.splits) apply (frule domI [where m = g']) apply (drule fg) apply simp apply (frule subst [OF dm]) apply clarsimp apply (drule not_sym) apply (clarsimp simp: map_comp_Some_iff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f \<circ>\<^sub>m g = f \<circ>\<^sub>m g' proof (prove)
goal (1 subgoal):
 1. \<And>x. (f \<circ>\<^sub>m g) x = (f \<circ>\<^sub>m g') x proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> dom g \<Longrightarrow> (f \<circ>\<^sub>m g) x = (f \<circ>\<^sub>m g') x
 2. \<And>x. x \<notin> dom g \<Longrightarrow> (f \<circ>\<^sub>m g) x = (f \<circ>\<^sub>m g') x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> dom g; x \<in> dom g'\<rbrakk> \<Longrightarrow> (f \<circ>\<^sub>m g) x = (f \<circ>\<^sub>m g') x
 2. \<And>x. x \<notin> dom g \<Longrightarrow> (f \<circ>\<^sub>m g) x = (f \<circ>\<^sub>m g') x proof (prove)
goal (2 subgoals):
 1. \<And>x y ya. \<lbrakk>g x = Some y; g' x = Some ya\<rbrakk> \<Longrightarrow> f y = f ya
 2. \<And>x. x \<notin> dom g \<Longrightarrow> (f \<circ>\<^sub>m g) x = (f \<circ>\<^sub>m g') x proof (prove)
goal (2 subgoals):
 1. \<And>x y ya. \<lbrakk>g x = Some y; g' x = Some ya; x \<in> dom g'\<rbrakk> \<Longrightarrow> f y = f ya
 2. \<And>x. x \<notin> dom g \<Longrightarrow> (f \<circ>\<^sub>m g) x = (f \<circ>\<^sub>m g') x proof (prove)
goal (2 subgoals):
 1. \<And>x y ya. \<lbrakk>g x = Some y; g' x = Some ya; f (the (g' x)) = f (the (g x))\<rbrakk> \<Longrightarrow> f y = f ya
 2. \<And>x. x \<notin> dom g \<Longrightarrow> (f \<circ>\<^sub>m g) x = (f \<circ>\<^sub>m g') x proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<notin> dom g \<Longrightarrow> (f \<circ>\<^sub>m g) x = (f \<circ>\<^sub>m g') x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<notin> dom g; x \<notin> dom g'\<rbrakk> \<Longrightarrow> (f \<circ>\<^sub>m g) x = (f \<circ>\<^sub>m g') x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>None \<noteq> (f \<circ>\<^sub>m g') x; g x = None\<rbrakk> \<Longrightarrow> \<exists>y. g' x = Some y proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>g x = None; (f \<circ>\<^sub>m g') x \<noteq> None\<rbrakk> \<Longrightarrow> \<exists>y. g' x = Some y proof (prove)
goal:
No subgoals!
theory Lib

lemma modify_map_id:
  "modify_map m p id = m" by (auto simp add: modify_map_def map_option_case split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. modify_map m p id = m
theory Lib

lemma modify_map_addr_com:
  assumes com: "x \<noteq> y"
  shows "modify_map (modify_map m x g) y f = modify_map (modify_map m y f) x g" by (rule ext) (simp add: modify_map_def map_option_case com split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. modify_map (modify_map m x g) y f = modify_map (modify_map m y f) x g