theory Lib

lemma is_inv_com:
  "is_inv f g \<Longrightarrow> is_inv g f" apply (unfold is_inv_def) apply safe apply (clarsimp simp: ran_def dom_def set_eq_iff) apply (erule_tac x=a in allE) apply clarsimp apply (clarsimp simp: ran_def dom_def set_eq_iff) apply blast apply (clarsimp simp: ran_def dom_def set_eq_iff) apply (erule_tac x=x in allE) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_inv f g \<Longrightarrow> is_inv g f proof (prove)
goal (1 subgoal):
 1. ran f = dom g \<and> (\<forall>x y. f x = Some y \<longrightarrow> g y = Some x) \<Longrightarrow> ran g = dom f \<and> (\<forall>x y. g x = Some y \<longrightarrow> f y = Some x) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>ran f = dom g; \<forall>x y. f x = Some y \<longrightarrow> g y = Some x; x \<in> ran g\<rbrakk> \<Longrightarrow> \<exists>y. f x = Some y
 2. \<And>x y. \<lbrakk>ran f = dom g; \<forall>x y. f x = Some y \<longrightarrow> g y = Some x; f x = Some y\<rbrakk> \<Longrightarrow> x \<in> ran g
 3. \<And>x y. \<lbrakk>ran f = dom g; \<forall>x y. f x = Some y \<longrightarrow> g y = Some x; g x = Some y\<rbrakk> \<Longrightarrow> f y = Some x proof (prove)
goal (3 subgoals):
 1. \<And>x a. \<lbrakk>\<forall>x. (\<exists>a. f a = Some x) = (\<exists>y. g x = Some y); \<forall>x y. f x = Some y \<longrightarrow> g y = Some x; g a = Some x\<rbrakk> \<Longrightarrow> \<exists>y. f x = Some y
 2. \<And>x y. \<lbrakk>ran f = dom g; \<forall>x y. f x = Some y \<longrightarrow> g y = Some x; f x = Some y\<rbrakk> \<Longrightarrow> x \<in> ran g
 3. \<And>x y. \<lbrakk>ran f = dom g; \<forall>x y. f x = Some y \<longrightarrow> g y = Some x; g x = Some y\<rbrakk> \<Longrightarrow> f y = Some x proof (prove)
goal (3 subgoals):
 1. \<And>x a. \<lbrakk>\<forall>x y. f x = Some y \<longrightarrow> g y = Some x; g a = Some x; (\<exists>aa. f aa = Some a) = (\<exists>y. g a = Some y)\<rbrakk> \<Longrightarrow> \<exists>y. f x = Some y
 2. \<And>x y. \<lbrakk>ran f = dom g; \<forall>x y. f x = Some y \<longrightarrow> g y = Some x; f x = Some y\<rbrakk> \<Longrightarrow> x \<in> ran g
 3. \<And>x y. \<lbrakk>ran f = dom g; \<forall>x y. f x = Some y \<longrightarrow> g y = Some x; g x = Some y\<rbrakk> \<Longrightarrow> f y = Some x proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>ran f = dom g; \<forall>x y. f x = Some y \<longrightarrow> g y = Some x; f x = Some y\<rbrakk> \<Longrightarrow> x \<in> ran g
 2. \<And>x y. \<lbrakk>ran f = dom g; \<forall>x y. f x = Some y \<longrightarrow> g y = Some x; g x = Some y\<rbrakk> \<Longrightarrow> f y = Some x proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>\<forall>x. (\<exists>a. f a = Some x) = (\<exists>y. g x = Some y); \<forall>x y. f x = Some y \<longrightarrow> g y = Some x; f x = Some y\<rbrakk> \<Longrightarrow> \<exists>a. g a = Some x
 2. \<And>x y. \<lbrakk>ran f = dom g; \<forall>x y. f x = Some y \<longrightarrow> g y = Some x; g x = Some y\<rbrakk> \<Longrightarrow> f y = Some x proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>ran f = dom g; \<forall>x y. f x = Some y \<longrightarrow> g y = Some x; g x = Some y\<rbrakk> \<Longrightarrow> f y = Some x proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>x. (\<exists>a. f a = Some x) = (\<exists>y. g x = Some y); \<forall>x y. f x = Some y \<longrightarrow> g y = Some x; g x = Some y\<rbrakk> \<Longrightarrow> f y = Some x proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>x y. f x = Some y \<longrightarrow> g y = Some x; g x = Some y; (\<exists>a. f a = Some x) = (\<exists>y. g x = Some y)\<rbrakk> \<Longrightarrow> f y = Some x proof (prove)
goal:
No subgoals!