theory StateTranslationProofs_DR

lemma map_lift_over_if_eq_twice:
  assumes inj_f: "inj_on f (dom m \<union> ran m \<union> {y, y'} \<union> set_option z \<union> set_option z')"
  shows
  "map_lift_over f (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)
       = (\<lambda>x. if map_lift_over f m x = Some (f y) then map_option f z
              else if map_lift_over f m x = Some (f y') then map_option f z'
              else map_lift_over f m x)"
  (is "map_lift_over f ?ifeq = ?rhs") proof - from inj_f have 1: "inj_on f (dom m \<union> ran m)" "inj_on f (dom m)" by (auto simp: inj_on_Un) have "dom ?ifeq \<subseteq> dom m" by (auto split: if_split_asm) with inj_f have 2: "inj_on f (dom ?ifeq)" by (auto elim!: subset_inj_on) have "dom ?ifeq \<union> ran ?ifeq \<subseteq> dom m \<union> ran m \<union> set_option z \<union> set_option z'" by (auto simp: ran_def) with inj_f have "inj_on f (dom ?ifeq \<union> ran ?ifeq)" by (auto elim!: subset_inj_on) note Q = 1 2 this note if_split[split del] if_cong[cong] show ?thesis apply (simp add: map_lift_over_def Q) apply (rule ext) apply (case_tac "x \<in> f ` dom ?ifeq") apply clarsimp apply (subst if_P, fastforce split: if_split_asm)+ apply (simp add: Q[THEN inv_into_f_f] domI ranI inj_on_eq_iff[OF inj_f]
               split: if_split_asm) apply (subst if_not_P, simp, rule allI, fastforce)+ apply (auto simp: option_map_def Q[THEN inv_into_f_f] domI ranI
                      inj_on_eq_iff[OF inj_f]
               split: if_split option.split) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_lift_over f (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) = (\<lambda>x. if map_lift_over f m x = Some (f y) then map_option f z else if map_lift_over f m x = Some (f y') then map_option f z' else map_lift_over f m x) proof (state)
goal (1 subgoal):
 1. map_lift_over f (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) = (\<lambda>x. if map_lift_over f m x = Some (f y) then map_option f z else if map_lift_over f m x = Some (f y') then map_option f z' else map_lift_over f m x) proof (chain)
picking this:
inj_on f (dom m \<union> ran m \<union> {y, y'} \<union> set_option z \<union> set_option z') proof (prove)
using this:
inj_on f (dom m \<union> ran m \<union> {y, y'} \<union> set_option z \<union> set_option z')

goal (1 subgoal):
 1. inj_on f (dom m \<union> ran m) &&& inj_on f (dom m) proof (state)
this:
inj_on f (dom m \<union> ran m)
inj_on f (dom m)

goal (1 subgoal):
 1. map_lift_over f (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) = (\<lambda>x. if map_lift_over f m x = Some (f y) then map_option f z else if map_lift_over f m x = Some (f y') then map_option f z' else map_lift_over f m x) proof (prove)
goal (1 subgoal):
 1. dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) \<subseteq> dom m proof (state)
this:
dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) \<subseteq> dom m

goal (1 subgoal):
 1. map_lift_over f (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) = (\<lambda>x. if map_lift_over f m x = Some (f y) then map_option f z else if map_lift_over f m x = Some (f y') then map_option f z' else map_lift_over f m x) proof (chain)
picking this:
inj_on f (dom m \<union> ran m \<union> {y, y'} \<union> set_option z \<union> set_option z')
dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) \<subseteq> dom m proof (prove)
using this:
inj_on f (dom m \<union> ran m \<union> {y, y'} \<union> set_option z \<union> set_option z')
dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) \<subseteq> dom m

goal (1 subgoal):
 1. inj_on f (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) proof (state)
this:
inj_on f (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x))

goal (1 subgoal):
 1. map_lift_over f (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) = (\<lambda>x. if map_lift_over f m x = Some (f y) then map_option f z else if map_lift_over f m x = Some (f y') then map_option f z' else map_lift_over f m x) proof (prove)
goal (1 subgoal):
 1. dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) \<union> ran (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) \<subseteq> dom m \<union> ran m \<union> set_option z \<union> set_option z' proof (state)
this:
dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) \<union> ran (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) \<subseteq> dom m \<union> ran m \<union> set_option z \<union> set_option z'

goal (1 subgoal):
 1. map_lift_over f (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) = (\<lambda>x. if map_lift_over f m x = Some (f y) then map_option f z else if map_lift_over f m x = Some (f y') then map_option f z' else map_lift_over f m x) proof (chain)
picking this:
inj_on f (dom m \<union> ran m \<union> {y, y'} \<union> set_option z \<union> set_option z')
dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) \<union> ran (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) \<subseteq> dom m \<union> ran m \<union> set_option z \<union> set_option z' proof (prove)
using this:
inj_on f (dom m \<union> ran m \<union> {y, y'} \<union> set_option z \<union> set_option z')
dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) \<union> ran (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) \<subseteq> dom m \<union> ran m \<union> set_option z \<union> set_option z'

goal (1 subgoal):
 1. inj_on f (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) \<union> ran (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) proof (state)
this:
inj_on f (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) \<union> ran (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x))

goal (1 subgoal):
 1. map_lift_over f (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) = (\<lambda>x. if map_lift_over f m x = Some (f y) then map_option f z else if map_lift_over f m x = Some (f y') then map_option f z' else map_lift_over f m x) proof (state)
this:
inj_on f (dom m \<union> ran m)
inj_on f (dom m)
inj_on f (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x))
inj_on f (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) \<union> ran (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x))

goal (1 subgoal):
 1. map_lift_over f (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) = (\<lambda>x. if map_lift_over f m x = Some (f y) then map_option f z else if map_lift_over f m x = Some (f y') then map_option f z' else map_lift_over f m x) proof (state)
this:
?P (if ?Q then ?x else ?y) = ((?Q \<longrightarrow> ?P ?x) \<and> (\<not> ?Q \<longrightarrow> ?P ?y))
\<lbrakk>?b = ?c; ?c \<Longrightarrow> ?x = ?u; \<not> ?c \<Longrightarrow> ?y = ?v\<rbrakk> \<Longrightarrow> (if ?b then ?x else ?y) = (if ?c then ?u else ?v)

goal (1 subgoal):
 1. map_lift_over f (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) = (\<lambda>x. if map_lift_over f m x = Some (f y) then map_option f z else if map_lift_over f m x = Some (f y') then map_option f z' else map_lift_over f m x) proof (prove)
goal (1 subgoal):
 1. map_lift_over f (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) = (\<lambda>x. if map_lift_over f m x = Some (f y) then map_option f z else if map_lift_over f m x = Some (f y') then map_option f z' else map_lift_over f m x) proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. if \<exists>ya. f ya = x \<and> ya \<in> dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) then map_option f (if m (inv_into (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) f x) = Some y then z else if m (inv_into (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) f x) = Some y' then z' else m (inv_into (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) f x)) else None) = (\<lambda>x. if (if \<exists>y. f y = x \<and> y \<in> dom m then map_option f (m (inv_into (dom m) f x)) else None) = Some (f y) then map_option f z else if (if \<exists>y. f y = x \<and> y \<in> dom m then map_option f (m (inv_into (dom m) f x)) else None) = Some (f y') then map_option f z' else if \<exists>y. f y = x \<and> y \<in> dom m then map_option f (m (inv_into (dom m) f x)) else None) proof (prove)
goal (1 subgoal):
 1. \<And>x. (if \<exists>ya. f ya = x \<and> ya \<in> dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) then map_option f (if m (inv_into (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) f x) = Some y then z else if m (inv_into (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) f x) = Some y' then z' else m (inv_into (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) f x)) else None) = (if (if \<exists>y. f y = x \<and> y \<in> dom m then map_option f (m (inv_into (dom m) f x)) else None) = Some (f y) then map_option f z else if (if \<exists>y. f y = x \<and> y \<in> dom m then map_option f (m (inv_into (dom m) f x)) else None) = Some (f y') then map_option f z' else if \<exists>y. f y = x \<and> y \<in> dom m then map_option f (m (inv_into (dom m) f x)) else None) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> f ` dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) \<Longrightarrow> (if \<exists>ya. f ya = x \<and> ya \<in> dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) then map_option f (if m (inv_into (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) f x) = Some y then z else if m (inv_into (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) f x) = Some y' then z' else m (inv_into (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) f x)) else None) = (if (if \<exists>y. f y = x \<and> y \<in> dom m then map_option f (m (inv_into (dom m) f x)) else None) = Some (f y) then map_option f z else if (if \<exists>y. f y = x \<and> y \<in> dom m then map_option f (m (inv_into (dom m) f x)) else None) = Some (f y') then map_option f z' else if \<exists>y. f y = x \<and> y \<in> dom m then map_option f (m (inv_into (dom m) f x)) else None)
 2. \<And>x. x \<notin> f ` dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) \<Longrightarrow> (if \<exists>ya. f ya = x \<and> ya \<in> dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) then map_option f (if m (inv_into (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) f x) = Some y then z else if m (inv_into (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) f x) = Some y' then z' else m (inv_into (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) f x)) else None) = (if (if \<exists>y. f y = x \<and> y \<in> dom m then map_option f (m (inv_into (dom m) f x)) else None) = Some (f y) then map_option f z else if (if \<exists>y. f y = x \<and> y \<in> dom m then map_option f (m (inv_into (dom m) f x)) else None) = Some (f y') then map_option f z' else if \<exists>y. f y = x \<and> y \<in> dom m then map_option f (m (inv_into (dom m) f x)) else None) proof (prove)
goal (2 subgoals):
 1. \<And>xa ya. (if m xa = Some y then z else if m xa = Some y' then z' else m xa) = Some ya \<Longrightarrow> (if \<exists>ya. f ya = f xa \<and> ya \<in> dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) then map_option f (if m (inv_into (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) f (f xa)) = Some y then z else if m (inv_into (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) f (f xa)) = Some y' then z' else m (inv_into (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) f (f xa))) else None) = (if (if \<exists>y. f y = f xa \<and> y \<in> dom m then map_option f (m (inv_into (dom m) f (f xa))) else None) = Some (f y) then map_option f z else if (if \<exists>y. f y = f xa \<and> y \<in> dom m then map_option f (m (inv_into (dom m) f (f xa))) else None) = Some (f y') then map_option f z' else if \<exists>y. f y = f xa \<and> y \<in> dom m then map_option f (m (inv_into (dom m) f (f xa))) else None)
 2. \<And>x. x \<notin> f ` dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) \<Longrightarrow> (if \<exists>ya. f ya = x \<and> ya \<in> dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) then map_option f (if m (inv_into (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) f x) = Some y then z else if m (inv_into (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) f x) = Some y' then z' else m (inv_into (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) f x)) else None) = (if (if \<exists>y. f y = x \<and> y \<in> dom m then map_option f (m (inv_into (dom m) f x)) else None) = Some (f y) then map_option f z else if (if \<exists>y. f y = x \<and> y \<in> dom m then map_option f (m (inv_into (dom m) f x)) else None) = Some (f y') then map_option f z' else if \<exists>y. f y = x \<and> y \<in> dom m then map_option f (m (inv_into (dom m) f x)) else None) proof (prove)
goal (2 subgoals):
 1. \<And>xa ya. (if m xa = Some y then z else if m xa = Some y' then z' else m xa) = Some ya \<Longrightarrow> map_option f (if m (inv_into (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) f (f xa)) = Some y then z else if m (inv_into (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) f (f xa)) = Some y' then z' else m (inv_into (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) f (f xa))) = (if map_option f (m (inv_into (dom m) f (f xa))) = Some (f y) then map_option f z else if map_option f (m (inv_into (dom m) f (f xa))) = Some (f y') then map_option f z' else map_option f (m (inv_into (dom m) f (f xa))))
 2. \<And>x. x \<notin> f ` dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) \<Longrightarrow> (if \<exists>ya. f ya = x \<and> ya \<in> dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) then map_option f (if m (inv_into (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) f x) = Some y then z else if m (inv_into (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) f x) = Some y' then z' else m (inv_into (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) f x)) else None) = (if (if \<exists>y. f y = x \<and> y \<in> dom m then map_option f (m (inv_into (dom m) f x)) else None) = Some (f y) then map_option f z else if (if \<exists>y. f y = x \<and> y \<in> dom m then map_option f (m (inv_into (dom m) f x)) else None) = Some (f y') then map_option f z' else if \<exists>y. f y = x \<and> y \<in> dom m then map_option f (m (inv_into (dom m) f x)) else None) proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<notin> f ` dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) \<Longrightarrow> (if \<exists>ya. f ya = x \<and> ya \<in> dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) then map_option f (if m (inv_into (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) f x) = Some y then z else if m (inv_into (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) f x) = Some y' then z' else m (inv_into (dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)) f x)) else None) = (if (if \<exists>y. f y = x \<and> y \<in> dom m then map_option f (m (inv_into (dom m) f x)) else None) = Some (f y) then map_option f z else if (if \<exists>y. f y = x \<and> y \<in> dom m then map_option f (m (inv_into (dom m) f x)) else None) = Some (f y') then map_option f z' else if \<exists>y. f y = x \<and> y \<in> dom m then map_option f (m (inv_into (dom m) f x)) else None) proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<notin> f ` dom (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) \<Longrightarrow> None = (if (if \<exists>y. f y = x \<and> y \<in> dom m then map_option f (m (inv_into (dom m) f x)) else None) = Some (f y) then map_option f z else if (if \<exists>y. f y = x \<and> y \<in> dom m then map_option f (m (inv_into (dom m) f x)) else None) = Some (f y') then map_option f z' else if \<exists>y. f y = x \<and> y \<in> dom m then map_option f (m (inv_into (dom m) f x)) else None) proof (prove)
goal:
No subgoals! proof (state)
this:
map_lift_over f (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x) = (\<lambda>x. if map_lift_over f m x = Some (f y) then map_option f z else if map_lift_over f m x = Some (f y') then map_option f z' else map_lift_over f m x)

goal:
No subgoals!