theory Lib

lemma map_option_eq_dom_eq:
  assumes ome: "map_option f \<circ> g = map_option f \<circ> g'"
  shows   "dom g = dom g'" proof (rule set_eqI) fix x { assume "x \<in> dom g" hence "Some (f (the (g x))) = (map_option f \<circ> g) x" by (auto simp: map_option_case split: option.splits) also have "\<dots> = (map_option f \<circ> g') x" by (simp add: ome) finally have "x \<in> dom g'" by (auto simp: map_option_case split: option.splits) } moreover { assume "x \<in> dom g'" hence "Some (f (the (g' x))) = (map_option f \<circ> g') x" by (auto simp: map_option_case split: option.splits) also have "\<dots> = (map_option f \<circ> g) x" by (simp add: ome) finally have "x \<in> dom g" by (auto simp: map_option_case split: option.splits) } ultimately show "(x \<in> dom g) = (x \<in> dom g')" by auto qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom g = dom g' proof (state)
goal (1 subgoal):
 1. \<And>x. (x \<in> dom g) = (x \<in> dom g') proof (state)
goal (1 subgoal):
 1. \<And>x. (x \<in> dom g) = (x \<in> dom g') proof (state)
goal (1 subgoal):
 1. \<And>x. (x \<in> dom g) = (x \<in> dom g') proof (state)
this:
x \<in> dom g

goal (1 subgoal):
 1. \<And>x. (x \<in> dom g) = (x \<in> dom g') proof (prove)
using this:
x \<in> dom g

goal (1 subgoal):
 1. Some (f (the (g x))) = (map_option f \<circ> g) x proof (state)
this:
Some (f (the (g x))) = (map_option f \<circ> g) x

goal (1 subgoal):
 1. \<And>x. (x \<in> dom g) = (x \<in> dom g') proof (state)
this:
Some (f (the (g x))) = (map_option f \<circ> g) x

goal (1 subgoal):
 1. \<And>x. (x \<in> dom g) = (x \<in> dom g') proof (prove)
goal (1 subgoal):
 1. (map_option f \<circ> g) x = (map_option f \<circ> g') x proof (state)
this:
(map_option f \<circ> g) x = (map_option f \<circ> g') x

goal (1 subgoal):
 1. \<And>x. (x \<in> dom g) = (x \<in> dom g') proof (chain)
picking this:
Some (f (the (g x))) = (map_option f \<circ> g') x proof (prove)
using this:
Some (f (the (g x))) = (map_option f \<circ> g') x

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

goal (1 subgoal):
 1. \<And>x. (x \<in> dom g) = (x \<in> dom g') proof (state)
this:
x \<in> dom g \<Longrightarrow> x \<in> dom g'

goal (1 subgoal):
 1. \<And>x. (x \<in> dom g) = (x \<in> dom g') proof (state)
this:
x \<in> dom g \<Longrightarrow> x \<in> dom g'

goal (1 subgoal):
 1. \<And>x. (x \<in> dom g) = (x \<in> dom g') proof (state)
this:
x \<in> dom g \<Longrightarrow> x \<in> dom g'

goal (1 subgoal):
 1. \<And>x. (x \<in> dom g) = (x \<in> dom g') proof (state)
this:
x \<in> dom g'

goal (1 subgoal):
 1. \<And>x. (x \<in> dom g) = (x \<in> dom g') proof (prove)
using this:
x \<in> dom g'

goal (1 subgoal):
 1. Some (f (the (g' x))) = (map_option f \<circ> g') x proof (state)
this:
Some (f (the (g' x))) = (map_option f \<circ> g') x

goal (1 subgoal):
 1. \<And>x. (x \<in> dom g) = (x \<in> dom g') proof (state)
this:
Some (f (the (g' x))) = (map_option f \<circ> g') x

goal (1 subgoal):
 1. \<And>x. (x \<in> dom g) = (x \<in> dom g') proof (prove)
goal (1 subgoal):
 1. (map_option f \<circ> g') x = (map_option f \<circ> g) x proof (state)
this:
(map_option f \<circ> g') x = (map_option f \<circ> g) x

goal (1 subgoal):
 1. \<And>x. (x \<in> dom g) = (x \<in> dom g') proof (chain)
picking this:
Some (f (the (g' x))) = (map_option f \<circ> g) x proof (prove)
using this:
Some (f (the (g' x))) = (map_option f \<circ> g) x

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

goal (1 subgoal):
 1. \<And>x. (x \<in> dom g) = (x \<in> dom g') proof (state)
this:
x \<in> dom g' \<Longrightarrow> x \<in> dom g

goal (1 subgoal):
 1. \<And>x. (x \<in> dom g) = (x \<in> dom g') proof (chain)
picking this:
x \<in> dom g \<Longrightarrow> x \<in> dom g'
x \<in> dom g' \<Longrightarrow> x \<in> dom g proof (prove)
using this:
x \<in> dom g \<Longrightarrow> x \<in> dom g'
x \<in> dom g' \<Longrightarrow> x \<in> dom g

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

goal:
No subgoals!