kings-crown/FVELER_Isabelle huggingface dataset:
theory Lib

lemma tl_drop_1 :
  "tl xs = drop 1 xs" by (simp add: drop_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tl xs = drop 1 xs
theory Lib

lemma upto_0_to_4:
  "[0..<4] = 0 # [1..<4]" by (subst upt_rec) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. [0..<4] = 0 # [1..<4]
theory Lib

lemma disjEI:
  "\<lbrakk> P \<or> Q; P \<Longrightarrow> R; Q \<Longrightarrow> S \<rbrakk>
     \<Longrightarrow> R \<or> S" by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<or> Q; P \<Longrightarrow> R; Q \<Longrightarrow> S\<rbrakk> \<Longrightarrow> R \<or> S
theory Lib

lemma dom_fun_upd2:
  "s x = Some z \<Longrightarrow> dom (s (x \<mapsto> y)) = dom s" by (simp add: insert_absorb domI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s x = Some z \<Longrightarrow> dom (s(x \<mapsto> y)) = dom s
theory Lib

lemma foldl_True :
  "foldl (\<or>) True bs" by (induct bs) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. foldl (\<or>) True bs
theory Lib

lemma image_set_comp:
  "f ` {g x | x. Q x} = (f \<circ> g) ` {x. Q x}" by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f ` {g x |x. Q x} = (f \<circ> g) ` {x. Q x}
theory Lib

lemma mutual_exE:
  "\<lbrakk> \<exists>x. P x; \<And>x. P x \<Longrightarrow> Q x \<rbrakk> \<Longrightarrow> \<exists>x. Q x" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>x. P x; \<And>x. P x \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> \<exists>x. Q x
theory Lib

lemma nat_diff_eq:
  fixes x :: nat
  shows "\<lbrakk> x - y = x - z; y < x\<rbrakk> \<Longrightarrow> y = z" by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x - y = x - z; y < x\<rbrakk> \<Longrightarrow> y = z
theory Lib

lemma comp_upd_simp:
  "(f \<circ> (g (x := y))) = ((f \<circ> g) (x := f y))" by (rule fun_upd_comp)

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

lemma dom_option_map:
  "dom (map_option f o m) = dom m" by (rule dom_map_option_comp)

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

lemma drop_imp:
  "P \<Longrightarrow> (A \<longrightarrow> P) \<and> (B \<longrightarrow> P)" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow> (A \<longrightarrow> P) \<and> (B \<longrightarrow> P)
theory Lib

lemma inj_on_fun_updI2:
  "\<lbrakk> inj_on f A; y \<notin> f ` (A - {x}) \<rbrakk> \<Longrightarrow> inj_on (f(x := y)) A" by (rule inj_on_fun_upd_strongerI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj_on f A; y \<notin> f ` (A - {x})\<rbrakk> \<Longrightarrow> inj_on (f(x := y)) A
theory Lib

lemma inj_on_fun_upd_elsewhere:
  "x \<notin> S \<Longrightarrow> inj_on (f (x := y)) S = inj_on f S" by (simp add: inj_on_def) blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<notin> S \<Longrightarrow> inj_on (f(x := y)) S = inj_on f S
theory Lib

lemma not_Some_eq_tuple:
  "(\<forall>y z. x \<noteq> Some (y, z)) = (x = None)" by (cases x, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>y z. x \<noteq> Some (y, z)) = (x = None)
theory Lib

lemma Int_image_empty:
  "\<lbrakk> \<And>x y. f x \<noteq> g y \<rbrakk>
       \<Longrightarrow> f ` S \<inter> g ` T = {}" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. f x \<noteq> g y) \<Longrightarrow> f ` S \<inter> g ` T = {}
theory Lib

lemma Max_prop:
  "\<lbrakk> Max S \<in> S \<Longrightarrow> P (Max S); (S :: ('a :: {finite, linorder}) set) \<noteq> {} \<rbrakk> \<Longrightarrow> P (Max S)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Max S \<in> S \<Longrightarrow> P (Max S); S \<noteq> {}\<rbrakk> \<Longrightarrow> P (Max S)
theory Lib

lemma Min_prop:
  "\<lbrakk> Min S \<in> S \<Longrightarrow> P (Min S); (S :: ('a :: {finite, linorder}) set) \<noteq> {} \<rbrakk> \<Longrightarrow> P (Min S)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Min S \<in> S \<Longrightarrow> P (Min S); S \<noteq> {}\<rbrakk> \<Longrightarrow> P (Min S)
theory Lib

lemma findSomeD:
  "find P xs = Some x \<Longrightarrow> P x \<and> x \<in> set xs" by (induct xs) (auto split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. find P xs = Some x \<Longrightarrow> P x \<and> x \<in> set xs
theory Lib

lemma findNoneD:
  "find P xs = None \<Longrightarrow> \<forall>x \<in> set xs. \<not>P x" by (induct xs) (auto split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. find P xs = None \<Longrightarrow> \<forall>x\<in>set xs. \<not> P x
theory Lib

lemma dom_upd:
  "dom (\<lambda>x. if x = y then None else f x) = dom f - {y}" by (rule set_eqI) (auto split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom (\<lambda>x. if x = y then None else f x) = dom f - {y}
theory Lib

lemma is_inv_NoneD:
  assumes "g x = None"
  assumes "is_inv f g"
  shows "x \<notin> ran f" proof - from assms have "x \<notin> dom g" by (auto simp: ran_def) moreover from assms have "ran f = dom g" by (simp add: is_inv_def) ultimately show ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<notin> ran f proof (state)
goal (1 subgoal):
 1. x \<notin> ran f proof (chain)
picking this:
g x = None
is_inv f g proof (prove)
using this:
g x = None
is_inv f g

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

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

goal (1 subgoal):
 1. x \<notin> ran f proof (chain)
picking this:
g x = None
is_inv f g proof (prove)
using this:
g x = None
is_inv f g

goal (1 subgoal):
 1. ran f = dom g proof (state)
this:
ran f = dom g

goal (1 subgoal):
 1. x \<notin> ran f proof (chain)
picking this:
x \<notin> dom g
ran f = dom g proof (prove)
using this:
x \<notin> dom g
ran f = dom g

goal (1 subgoal):
 1. x \<notin> ran f proof (state)
this:
x \<notin> ran f

goal:
No subgoals!
theory Lib

lemma is_inv_SomeD:
  "\<lbrakk> f x = Some y; is_inv f g \<rbrakk> \<Longrightarrow> g y = Some x" by (simp add: is_inv_def)

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

lemma is_inv_inj:
  "is_inv f g \<Longrightarrow> inj_on f (dom f)" apply (frule is_inv_com) apply (clarsimp simp: inj_on_def) apply (drule (1) is_inv_SomeD) apply (auto dest: is_inv_SomeD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_inv f g \<Longrightarrow> inj_on f (dom f) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_inv f g; is_inv g f\<rbrakk> \<Longrightarrow> inj_on f (dom f) proof (prove)
goal (1 subgoal):
 1. \<And>x y ya. \<lbrakk>is_inv f g; is_inv g f; f y = Some ya; f x = Some ya\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<And>x y ya. \<lbrakk>is_inv f g; is_inv g f; f x = Some ya; g ya = Some y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal:
No subgoals!
theory Lib

lemma ran_upd':
  "\<lbrakk>inj_on f (dom f); f y = Some z\<rbrakk> \<Longrightarrow> ran (f (y := None)) = ran f - {z}" by (force simp: ran_def inj_on_def dom_def intro!: set_eqI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj_on f (dom f); f y = Some z\<rbrakk> \<Longrightarrow> ran (f(y := None)) = ran f - {z}
theory Lib

lemma is_inv_None_upd:
  "\<lbrakk> is_inv f g; g x = Some y\<rbrakk> \<Longrightarrow> is_inv (f(y := None)) (g(x := None))" apply (subst is_inv_def) apply (clarsimp simp: dom_upd) apply (drule is_inv_SomeD, erule is_inv_com) apply (frule is_inv_inj) apply (auto simp: ran_upd' is_inv_def dest: is_inv_SomeD is_inv_inj) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_inv f g; g x = Some y\<rbrakk> \<Longrightarrow> is_inv (f(y := None)) (g(x := None)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_inv f g; g x = Some y\<rbrakk> \<Longrightarrow> ran (f(y := None)) = dom (g(x := None)) \<and> (\<forall>xa ya. (f(y := None)) xa = Some ya \<longrightarrow> (g(x := None)) ya = Some xa) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_inv f g; g x = Some y\<rbrakk> \<Longrightarrow> ran (f(y := None)) = dom g - {x} \<and> (\<forall>xa. xa \<noteq> y \<longrightarrow> (\<forall>y. (y = x \<longrightarrow> f xa \<noteq> Some x) \<and> (y \<noteq> x \<longrightarrow> f xa = Some y \<longrightarrow> g y = Some xa))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_inv f g; f y = Some x\<rbrakk> \<Longrightarrow> ran (f(y := None)) = dom g - {x} \<and> (\<forall>xa. xa \<noteq> y \<longrightarrow> (\<forall>y. (y = x \<longrightarrow> f xa \<noteq> Some x) \<and> (y \<noteq> x \<longrightarrow> f xa = Some y \<longrightarrow> g y = Some xa))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_inv f g; f y = Some x; inj_on f (dom f)\<rbrakk> \<Longrightarrow> ran (f(y := None)) = dom g - {x} \<and> (\<forall>xa. xa \<noteq> y \<longrightarrow> (\<forall>y. (y = x \<longrightarrow> f xa \<noteq> Some x) \<and> (y \<noteq> x \<longrightarrow> f xa = Some y \<longrightarrow> g y = Some xa))) proof (prove)
goal:
No subgoals!
theory Lib

lemma is_inv_inj2:
  "is_inv f g \<Longrightarrow> inj_on g (dom g)" using is_inv_com is_inv_inj by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_inv f g \<Longrightarrow> inj_on g (dom g) proof (prove)
using this:
is_inv ?f ?g \<Longrightarrow> is_inv ?g ?f
is_inv ?f ?g \<Longrightarrow> inj_on ?f (dom ?f)

goal (1 subgoal):
 1. is_inv f g \<Longrightarrow> inj_on g (dom g)
theory Lib

lemma is_inv_eq:
  "is_inv f g = (\<forall>x y. (f x = Some y) = (g y = Some x))" proof assume "\<forall>x y. (f x = Some y) = (g y = Some x)" thus "is_inv f g" by (auto simp: is_inv_def ran_def) next assume "is_inv f g" moreover from this have "is_inv g f" by (rule is_inv_com) ultimately show "\<forall>x y. (f x = Some y) = (g y = Some x)" unfolding is_inv_def by blast qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_inv f g = (\<forall>x y. (f x = Some y) = (g y = Some x)) proof (state)
goal (2 subgoals):
 1. is_inv f g \<Longrightarrow> \<forall>x y. (f x = Some y) = (g y = Some x)
 2. \<forall>x y. (f x = Some y) = (g y = Some x) \<Longrightarrow> is_inv f g proof (state)
this:
\<forall>x y. (f x = Some y) = (g y = Some x)

goal (2 subgoals):
 1. is_inv f g \<Longrightarrow> \<forall>x y. (f x = Some y) = (g y = Some x)
 2. \<forall>x y. (f x = Some y) = (g y = Some x) \<Longrightarrow> is_inv f g proof (prove)
using this:
\<forall>x y. (f x = Some y) = (g y = Some x)

goal (1 subgoal):
 1. is_inv f g proof (state)
this:
is_inv f g

goal (1 subgoal):
 1. is_inv f g \<Longrightarrow> \<forall>x y. (f x = Some y) = (g y = Some x) proof (state)
goal (1 subgoal):
 1. is_inv f g \<Longrightarrow> \<forall>x y. (f x = Some y) = (g y = Some x) proof (state)
this:
is_inv f g

goal (1 subgoal):
 1. is_inv f g \<Longrightarrow> \<forall>x y. (f x = Some y) = (g y = Some x) proof (state)
this:
is_inv f g

goal (1 subgoal):
 1. is_inv f g \<Longrightarrow> \<forall>x y. (f x = Some y) = (g y = Some x) proof (chain)
picking this:
is_inv f g proof (prove)
using this:
is_inv f g

goal (1 subgoal):
 1. is_inv g f proof (state)
this:
is_inv g f

goal (1 subgoal):
 1. is_inv f g \<Longrightarrow> \<forall>x y. (f x = Some y) = (g y = Some x) proof (chain)
picking this:
is_inv f g
is_inv g f proof (prove)
using this:
is_inv f g
is_inv g f

goal (1 subgoal):
 1. \<forall>x y. (f x = Some y) = (g y = Some x) proof (prove)
using this:
ran f = dom g \<and> (\<forall>x y. f x = Some y \<longrightarrow> g y = Some x)
ran g = dom f \<and> (\<forall>x y. g x = Some y \<longrightarrow> f y = Some x)

goal (1 subgoal):
 1. \<forall>x y. (f x = Some y) = (g y = Some x) proof (state)
this:
\<forall>x y. (f x = Some y) = (g y = Some x)

goal:
No subgoals!
theory Lib

lemma the_inv_map_def2:
  "the_inv_map m = (Some \<circ> the_inv_into (dom m) (the \<circ> m)) |` (ran m)" apply (rule ext) apply (clarsimp simp: the_inv_map_def the_inv_into_def dom_def) apply (rule_tac f=The in arg_cong) apply (rule ext) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. the_inv_map m = (Some \<circ> the_inv_into (dom m) (the \<circ> m)) |` ran m proof (prove)
goal (1 subgoal):
 1. \<And>x. the_inv_map m x = ((Some \<circ> the_inv_into (dom m) (the \<circ> m)) |` ran m) x proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> ran m \<Longrightarrow> (THE xa. m xa = Some x) = (THE y. (\<exists>ya. m y = Some ya) \<and> the (m y) = x) proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> ran m \<Longrightarrow> (\<lambda>xa. m xa = Some x) = (\<lambda>y. (\<exists>ya. m y = Some ya) \<and> the (m y) = x) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. x \<in> ran m \<Longrightarrow> (m xa = Some x) = ((\<exists>y. m xa = Some y) \<and> the (m xa) = x) proof (prove)
goal:
No subgoals!
theory Lib

lemma dom_comp_Some[simp]: "dom (comp Some f) = UNIV" by (simp add: dom_def)

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

lemma is_inv_the_inv_map:
  "inj_on m (dom m) \<Longrightarrow> is_inv m (the_inv_map m)" apply (simp add: is_inv_def) apply (intro conjI allI impI) apply (simp add: the_inv_map_def2) apply (auto simp add: the_inv_map_def inj_on_def dom_def intro: ranI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj_on m (dom m) \<Longrightarrow> is_inv m (the_inv_map m) proof (prove)
goal (1 subgoal):
 1. inj_on m (dom m) \<Longrightarrow> ran m = dom (the_inv_map m) \<and> (\<forall>x y. m x = Some y \<longrightarrow> the_inv_map m y = Some x) proof (prove)
goal (2 subgoals):
 1. inj_on m (dom m) \<Longrightarrow> ran m = dom (the_inv_map m)
 2. \<And>x y. \<lbrakk>inj_on m (dom m); m x = Some y\<rbrakk> \<Longrightarrow> the_inv_map m y = Some x proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>inj_on m (dom m); m x = Some y\<rbrakk> \<Longrightarrow> the_inv_map m y = Some x proof (prove)
goal:
No subgoals!
theory Lib

lemma the_the_inv_mapI:
  "inj_on m (dom m) \<Longrightarrow> m x = Some y \<Longrightarrow> the (the_inv_map m y) = x" by (auto simp: the_inv_map_def ran_def inj_on_def dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj_on m (dom m); m x = Some y\<rbrakk> \<Longrightarrow> the (the_inv_map m y) = x
theory Lib

lemma eq_restrict_map_None:
  "restrict_map m A x = None \<longleftrightarrow> x ~: (A \<inter> dom m)" by (auto simp: restrict_map_def split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((m |` A) x = None) = (x \<notin> A \<inter> dom m)
theory Lib

lemma eq_the_inv_map_None[simp]: "the_inv_map m x = None \<longleftrightarrow> x\<notin>ran m" by (simp add: the_inv_map_def2 eq_restrict_map_None)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (the_inv_map m x = None) = (x \<notin> ran m)
theory Lib

lemma is_inv_unique:
  "is_inv f g \<Longrightarrow> is_inv f h \<Longrightarrow> g=h" apply (rule ext) apply (clarsimp simp: is_inv_def dom_def Collect_eq ran_def) apply (drule_tac x=x in spec)+ apply (case_tac "g x", clarsimp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_inv f g; is_inv f h\<rbrakk> \<Longrightarrow> g = h proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_inv f g; is_inv f h\<rbrakk> \<Longrightarrow> g x = h x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>b. (\<exists>a. f a = Some b) = (\<exists>y. h b = Some y); \<forall>x y. f x = Some y \<longrightarrow> g y = Some x; \<forall>b. (\<exists>y. g b = Some y) = (\<exists>y. h b = Some y); \<forall>x y. f x = Some y \<longrightarrow> h y = Some x\<rbrakk> \<Longrightarrow> g x = h x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x y. f x = Some y \<longrightarrow> g y = Some x; \<forall>x y. f x = Some y \<longrightarrow> h y = Some x; (\<exists>a. f a = Some x) = (\<exists>y. h x = Some y); (\<exists>y. g x = Some y) = (\<exists>y. h x = Some y)\<rbrakk> \<Longrightarrow> g x = h x proof (prove)
goal:
No subgoals!
theory Lib

lemma range_convergence1:
  "\<lbrakk> \<forall>z. x < z \<and> z \<le> y \<longrightarrow> P z; \<forall>z > y. P (z :: 'a :: linorder) \<rbrakk> \<Longrightarrow> \<forall>z > x. P z" using not_le by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> P z; \<forall>z>y. P z\<rbrakk> \<Longrightarrow> \<forall>z>x. P z proof (prove)
using this:
(\<not> ?x \<le> ?y) = (?y < ?x)

goal (1 subgoal):
 1. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> P z; \<forall>z>y. P z\<rbrakk> \<Longrightarrow> \<forall>z>x. P z
theory Lib

lemma range_convergence2:
  "\<lbrakk> \<forall>z. x < z \<and> z \<le> y \<longrightarrow> P z; \<forall>z. z > y \<and> z < w \<longrightarrow> P (z :: 'a :: linorder) \<rbrakk>
     \<Longrightarrow> \<forall>z. z > x \<and> z < w \<longrightarrow> P z" using range_convergence1[where P="\<lambda>z. z < w \<longrightarrow> P z" and x=x and y=y] by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> P z; \<forall>z. y < z \<and> z < w \<longrightarrow> P z\<rbrakk> \<Longrightarrow> \<forall>z. x < z \<and> z < w \<longrightarrow> P z proof (prove)
using this:
\<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> z < w \<longrightarrow> P z; \<forall>z>y. z < w \<longrightarrow> P z\<rbrakk> \<Longrightarrow> \<forall>z>x. z < w \<longrightarrow> P z

goal (1 subgoal):
 1. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> P z; \<forall>z. y < z \<and> z < w \<longrightarrow> P z\<rbrakk> \<Longrightarrow> \<forall>z. x < z \<and> z < w \<longrightarrow> P z
theory Lib

lemma map_comp_eq:
  "f \<circ>\<^sub>m g = case_option None f \<circ> g" apply (rule ext) apply (case_tac "g x") by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f \<circ>\<^sub>m g = case_option None f \<circ> g proof (prove)
goal (1 subgoal):
 1. \<And>x. (f \<circ>\<^sub>m g) x = (case_option None f \<circ> g) x proof (prove)
goal (2 subgoals):
 1. \<And>x. g x = None \<Longrightarrow> (f \<circ>\<^sub>m g) x = (case_option None f \<circ> g) x
 2. \<And>x a. g x = Some a \<Longrightarrow> (f \<circ>\<^sub>m g) x = (case_option None f \<circ> g) x
theory Lib

lemma dom_If_Some:
   "dom (\<lambda>x. if x \<in> S then Some v else f x) = (S \<union> dom f)" by (auto split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom (\<lambda>x. if x \<in> S then Some v else f x) = S \<union> dom f
theory Lib

lemma foldl_fun_upd_const:
  "foldl (\<lambda>s x. s(f x := v)) s xs
    = (\<lambda>x. if x \<in> f ` set xs then v else s x)" by (induct xs arbitrary: s) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. foldl (\<lambda>s x. s(f x := v)) s xs = (\<lambda>x. if x \<in> f ` set xs then v else s x)
theory Lib

lemma foldl_id:
  "foldl (\<lambda>s x. s) s xs = s" by (induct xs) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. foldl (\<lambda>s x. s) s xs = s
theory Lib

lemma ball_to_all:
  "(\<And>x. (x \<in> A) = (P x)) \<Longrightarrow> (\<forall>x \<in> A. B x) = (\<forall>x. P x \<longrightarrow> B x)" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. (x \<in> A) = P x) \<Longrightarrow> (\<forall>x\<in>A. B x) = (\<forall>x. P x \<longrightarrow> B x)
theory Lib

lemma case_option_If:
  "case_option P (\<lambda>x. Q) v = (if v = None then P else Q)" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case v of None \<Rightarrow> P | Some x \<Rightarrow> Q) = (if v = None then P else Q)
theory Lib

lemma case_option_If2:
  "case_option P Q v = If (v \<noteq> None) (Q (the v)) P" by (simp split: option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case v of None \<Rightarrow> P | Some x \<Rightarrow> Q x) = (if v \<noteq> None then Q (the v) else P)
theory Lib

lemma if3_fold:
  "(if P then x else if Q then y else x) = (if P \<or> \<not> Q then x else y)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if P then x else if Q then y else x) = (if P \<or> \<not> Q then x else y)
theory Lib

lemma rtrancl_insert:
  assumes x_new: "\<And>y. (x,y) \<notin> R"
  shows "R^* `` insert x S = insert x (R^* `` S)" proof - have "R^* `` insert x S = R^* `` ({x} \<union> S)" by simp also have "R^* `` ({x} \<union> S) = R^* `` {x} \<union> R^* `` S" by (subst Image_Un) simp also have "R^* `` {x} = {x}" by (meson Image_closed_trancl Image_singleton_iff subsetI x_new) finally show ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R\<^sup>* `` insert x S = insert x (R\<^sup>* `` S) proof (state)
goal (1 subgoal):
 1. R\<^sup>* `` insert x S = insert x (R\<^sup>* `` S) proof (prove)
goal (1 subgoal):
 1. R\<^sup>* `` insert x S = R\<^sup>* `` ({x} \<union> S) proof (state)
this:
R\<^sup>* `` insert x S = R\<^sup>* `` ({x} \<union> S)

goal (1 subgoal):
 1. R\<^sup>* `` insert x S = insert x (R\<^sup>* `` S) proof (state)
this:
R\<^sup>* `` insert x S = R\<^sup>* `` ({x} \<union> S)

goal (1 subgoal):
 1. R\<^sup>* `` insert x S = insert x (R\<^sup>* `` S) proof (prove)
goal (1 subgoal):
 1. R\<^sup>* `` ({x} \<union> S) = R\<^sup>* `` {x} \<union> R\<^sup>* `` S proof (state)
this:
R\<^sup>* `` ({x} \<union> S) = R\<^sup>* `` {x} \<union> R\<^sup>* `` S

goal (1 subgoal):
 1. R\<^sup>* `` insert x S = insert x (R\<^sup>* `` S) proof (state)
this:
R\<^sup>* `` ({x} \<union> S) = R\<^sup>* `` {x} \<union> R\<^sup>* `` S

goal (1 subgoal):
 1. R\<^sup>* `` insert x S = insert x (R\<^sup>* `` S) proof (prove)
goal (1 subgoal):
 1. R\<^sup>* `` {x} = {x} proof (state)
this:
R\<^sup>* `` {x} = {x}

goal (1 subgoal):
 1. R\<^sup>* `` insert x S = insert x (R\<^sup>* `` S) proof (chain)
picking this:
R\<^sup>* `` insert x S = {x} \<union> R\<^sup>* `` S proof (prove)
using this:
R\<^sup>* `` insert x S = {x} \<union> R\<^sup>* `` S

goal (1 subgoal):
 1. R\<^sup>* `` insert x S = insert x (R\<^sup>* `` S) proof (state)
this:
R\<^sup>* `` insert x S = insert x (R\<^sup>* `` S)

goal:
No subgoals!
theory Lib

lemma ran_del_subset:
  "y \<in> ran (f (x := None)) \<Longrightarrow> y \<in> ran f" by (auto simp: ran_def split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. y \<in> ran (f(x := None)) \<Longrightarrow> y \<in> ran f
theory Lib

lemma trancl_sub_lift:
  assumes sub: "\<And>p p'. (p,p') \<in> r \<Longrightarrow> (p,p') \<in> r'"
  shows "(p,p') \<in> r^+ \<Longrightarrow> (p,p') \<in> r'^+" by (fastforce intro: trancl_mono sub)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (p, p') \<in> r\<^sup>+ \<Longrightarrow> (p, p') \<in> r'\<^sup>+
theory Lib

lemma rtrancl_simulate_weak:
  assumes r: "(x,z) \<in> R\<^sup>*"
  assumes s: "\<And>y. (x,y) \<in> R \<Longrightarrow> (y,z) \<in> R\<^sup>* \<Longrightarrow> (x,y) \<in> R' \<and> (y,z) \<in> R'\<^sup>*"
  shows "(x,z) \<in> R'\<^sup>*" apply (rule converse_rtranclE[OF r]) apply simp apply (frule (1) s) apply clarsimp by (rule converse_rtrancl_into_rtrancl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, z) \<in> R'\<^sup>* proof (prove)
goal (2 subgoals):
 1. x = z \<Longrightarrow> (x, z) \<in> R'\<^sup>*
 2. \<And>y. \<lbrakk>(x, y) \<in> R; (y, z) \<in> R\<^sup>*\<rbrakk> \<Longrightarrow> (x, z) \<in> R'\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>(x, y) \<in> R; (y, z) \<in> R\<^sup>*\<rbrakk> \<Longrightarrow> (x, z) \<in> R'\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>(x, y) \<in> R; (y, z) \<in> R\<^sup>*; (x, y) \<in> R' \<and> (y, z) \<in> R'\<^sup>*\<rbrakk> \<Longrightarrow> (x, z) \<in> R'\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>(x, y) \<in> R; (y, z) \<in> R\<^sup>*; (x, y) \<in> R'; (y, z) \<in> R'\<^sup>*\<rbrakk> \<Longrightarrow> (x, z) \<in> R'\<^sup>*