theory ADT_C

lemma setUserMem_C_def_foldl:
  "setUserMem_C um \<equiv>
   modify (\<lambda>s. s\<lparr>globals := (globals s)\<lparr>t_hrs_' :=
     (foldl (%f p. f(p := the (um p))) (fst (t_hrs_' (globals s)))
            (filter (%p. p : dom um) enum),
      snd (t_hrs_' (globals s))) \<rparr>\<rparr>)" apply (rule eq_reflection) apply (simp add: setUserMem_C_def) apply (rule arg_cong[where f=modify]) apply (rule ext) apply (rule_tac f=globals_update in arg_cong2) apply (rule ext) apply (rule_tac f=t_hrs_'_update in arg_cong2) apply (rule ext) apply simp_all apply (rule ext) apply (simp add: foldl_fun_upd_value) apply (intro conjI impI) apply clarsimp apply (clarsimp split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. setUserMem_C um \<equiv> modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>t_hrs_' := (foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals s))) (filter (\<lambda>p. p \<in> dom um) enum), snd (t_hrs_' (globals s)))\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. setUserMem_C um = modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>t_hrs_' := (foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals s))) (filter (\<lambda>p. p \<in> dom um) enum), snd (t_hrs_' (globals s)))\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>t_hrs_' := (\<lambda>p. case um p of None \<Rightarrow> fst (t_hrs_' (globals s)) p | Some x \<Rightarrow> x, snd (t_hrs_' (globals s)))\<rparr>\<rparr>) = modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>t_hrs_' := (foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals s))) (filter (\<lambda>p. p \<in> dom um) enum), snd (t_hrs_' (globals s)))\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. s\<lparr>globals := globals s\<lparr>t_hrs_' := (\<lambda>p. case um p of None \<Rightarrow> fst (t_hrs_' (globals s)) p | Some x \<Rightarrow> x, snd (t_hrs_' (globals s)))\<rparr>\<rparr>) = (\<lambda>s. s\<lparr>globals := globals s\<lparr>t_hrs_' := (foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals s))) (filter (\<lambda>p. p \<in> dom um) enum), snd (t_hrs_' (globals s)))\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. s\<lparr>globals := globals s\<lparr>t_hrs_' := (\<lambda>p. case um p of None \<Rightarrow> fst (t_hrs_' (globals s)) p | Some x \<Rightarrow> x, snd (t_hrs_' (globals s)))\<rparr>\<rparr> = s\<lparr>globals := globals s\<lparr>t_hrs_' := (foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals s))) (filter (\<lambda>p. p \<in> dom um) enum), snd (t_hrs_' (globals s)))\<rparr>\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>s. (\<lambda>_. globals s\<lparr>t_hrs_' := (\<lambda>p. case um p of None \<Rightarrow> fst (t_hrs_' (globals s)) p | Some x \<Rightarrow> x, snd (t_hrs_' (globals s)))\<rparr>) = (\<lambda>_. globals s\<lparr>t_hrs_' := (foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals s))) (filter (\<lambda>p. p \<in> dom um) enum), snd (t_hrs_' (globals s)))\<rparr>)
 2. \<And>s. s = s proof (prove)
goal (2 subgoals):
 1. \<And>s _. globals s\<lparr>t_hrs_' := (\<lambda>p. case um p of None \<Rightarrow> fst (t_hrs_' (globals s)) p | Some x \<Rightarrow> x, snd (t_hrs_' (globals s)))\<rparr> = globals s\<lparr>t_hrs_' := (foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals s))) (filter (\<lambda>p. p \<in> dom um) enum), snd (t_hrs_' (globals s)))\<rparr>
 2. \<And>s. s = s proof (prove)
goal (3 subgoals):
 1. \<And>s _. (\<lambda>_. (\<lambda>p. case um p of None \<Rightarrow> fst (t_hrs_' (globals s)) p | Some x \<Rightarrow> x, snd (t_hrs_' (globals s)))) = (\<lambda>_. (foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals s))) (filter (\<lambda>p. p \<in> dom um) enum), snd (t_hrs_' (globals s))))
 2. \<And>s _. globals s = globals s
 3. \<And>s. s = s proof (prove)
goal (3 subgoals):
 1. \<And>s _ _. (\<lambda>p. case um p of None \<Rightarrow> fst (t_hrs_' (globals s)) p | Some x \<Rightarrow> x, snd (t_hrs_' (globals s))) = (foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals s))) (filter (\<lambda>p. p \<in> dom um) enum), snd (t_hrs_' (globals s)))
 2. \<And>s _. globals s = globals s
 3. \<And>s. s = s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<lambda>p. case um p of None \<Rightarrow> fst (t_hrs_' (globals s)) p | Some x \<Rightarrow> x) = foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals s))) (filter (\<lambda>p. p \<in> dom um) enum) proof (prove)
goal (1 subgoal):
 1. \<And>s p. (case um p of None \<Rightarrow> fst (t_hrs_' (globals s)) p | Some x \<Rightarrow> x) = foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals s))) (filter (\<lambda>p. p \<in> dom um) enum) p proof (prove)
goal (1 subgoal):
 1. \<And>s p. (p \<in> dom um \<longrightarrow> (case um p of None \<Rightarrow> fst (t_hrs_' (globals s)) p | Some x \<Rightarrow> x) = the (um p)) \<and> (p \<notin> dom um \<longrightarrow> (case um p of None \<Rightarrow> fst (t_hrs_' (globals s)) p | Some x \<Rightarrow> x) = fst (t_hrs_' (globals s)) p) proof (prove)
goal (2 subgoals):
 1. \<And>s p. p \<in> dom um \<Longrightarrow> (case um p of None \<Rightarrow> fst (t_hrs_' (globals s)) p | Some x \<Rightarrow> x) = the (um p)
 2. \<And>s p. p \<notin> dom um \<Longrightarrow> (case um p of None \<Rightarrow> fst (t_hrs_' (globals s)) p | Some x \<Rightarrow> x) = fst (t_hrs_' (globals s)) p proof (prove)
goal (1 subgoal):
 1. \<And>s p. p \<notin> dom um \<Longrightarrow> (case um p of None \<Rightarrow> fst (t_hrs_' (globals s)) p | Some x \<Rightarrow> x) = fst (t_hrs_' (globals s)) p proof (prove)
goal:
No subgoals!