theory StateTranslationProofs_DR

lemma map_lift_over_upd:
  assumes inj_f: "inj_on f ({x} \<union> set_option y \<union> dom m \<union> ran m)"
  shows "(map_lift_over f (m(x := y)))
           = ((map_lift_over f m) (f x := map_option f y))" proof - have Q: "inj_on f (dom m \<union> ran m)"
      "inj_on f (insert x (dom m \<union> ran (m(x := y))))"
      "inj_on f (dom m)"
      "inj_on f (insert x (dom m))"
      "inj_on f (dom m - {x} \<union> ran (m(x := None)))"
      "inj_on f (dom m - {x})" apply (safe intro!: subset_inj_on[OF inj_f]) apply (auto simp: ran_def split: if_split_asm) done show ?thesis apply (simp add: map_lift_over_def Q del: inj_on_insert) apply (safe; rule ext; simp add: Q[THEN inv_into_f_f] domI cong del: imp_cong) apply (auto simp add: Q[THEN inv_into_f_f] domI inj_on_eq_iff[OF inj_f] ranI
                 simp del: inj_on_insert) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_lift_over f (m(x := y)) = (map_lift_over f m)(f x := map_option f y) proof (state)
goal (1 subgoal):
 1. map_lift_over f (m(x := y)) = (map_lift_over f m)(f x := map_option f y) proof (prove)
goal (1 subgoal):
 1. (inj_on f (dom m \<union> ran m) &&& inj_on f (insert x (dom m \<union> ran (m(x := y)))) &&& inj_on f (dom m)) &&& inj_on f (insert x (dom m)) &&& inj_on f (dom m - {x} \<union> ran (m(x := None))) &&& inj_on f (dom m - {x}) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>xa \<notin> ran m; \<nexists>y. m xa = Some y; y \<noteq> Some xa; xa \<notin> {}; xa \<in> ran (m(x := y))\<rbrakk> \<Longrightarrow> xa = x
 2. \<And>xa. \<lbrakk>xa \<notin> ran m; \<nexists>y. m xa = Some y; y \<noteq> Some xa; xa \<notin> {}; xa \<in> ran (m(x := None))\<rbrakk> \<Longrightarrow> xa = x proof (prove)
goal:
No subgoals! proof (state)
this:
inj_on f (dom m \<union> ran m)
inj_on f (insert x (dom m \<union> ran (m(x := y))))
inj_on f (dom m)
inj_on f (insert x (dom m))
inj_on f (dom m - {x} \<union> ran (m(x := None)))
inj_on f (dom m - {x})

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

goal:
No subgoals!