theory TcbAcc_AI

lemma fold_fun_upd:
  "distinct keys \<Longrightarrow>
   foldl (\<lambda>s (k, v). s(k := v)) s (zip keys vals) key
   = (if key \<in> set (take (length vals) keys)
      then vals ! (the_index keys key)
      else s key)" apply (induct keys arbitrary: vals s) apply simp apply (case_tac vals, simp_all split del: if_split) apply (case_tac "key = a", simp_all split del: if_split) apply clarsimp apply (drule in_set_takeD) apply simp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct keys \<Longrightarrow> foldl (\<lambda>s (k, v). s(k := v)) s (zip keys vals) key = (if key \<in> set (take (length vals) keys) then vals ! the_index keys key else s key) proof (prove)
goal (2 subgoals):
 1. \<And>vals s. distinct [] \<Longrightarrow> foldl (\<lambda>s (x, y). s(x := y)) s (zip [] vals) key = (if key \<in> set (take (length vals) []) then vals ! the_index [] key else s key)
 2. \<And>a keys vals s. \<lbrakk>\<And>vals s. distinct keys \<Longrightarrow> foldl (\<lambda>s (x, y). s(x := y)) s (zip keys vals) key = (if key \<in> set (take (length vals) keys) then vals ! the_index keys key else s key); distinct (a # keys)\<rbrakk> \<Longrightarrow> foldl (\<lambda>s (x, y). s(x := y)) s (zip (a # keys) vals) key = (if key \<in> set (take (length vals) (a # keys)) then vals ! the_index (a # keys) key else s key) proof (prove)
goal (1 subgoal):
 1. \<And>a keys vals s. \<lbrakk>\<And>vals s. distinct keys \<Longrightarrow> foldl (\<lambda>s (x, y). s(x := y)) s (zip keys vals) key = (if key \<in> set (take (length vals) keys) then vals ! the_index keys key else s key); distinct (a # keys)\<rbrakk> \<Longrightarrow> foldl (\<lambda>s (x, y). s(x := y)) s (zip (a # keys) vals) key = (if key \<in> set (take (length vals) (a # keys)) then vals ! the_index (a # keys) key else s key) proof (prove)
goal (1 subgoal):
 1. \<And>a keys vals s aa list. \<lbrakk>\<And>vals s. foldl (\<lambda>s (x, y). s(x := y)) s (zip keys vals) key = (if key \<in> set (take (length vals) keys) then vals ! the_index keys key else s key); a \<notin> set keys \<and> distinct keys; vals = aa # list\<rbrakk> \<Longrightarrow> (if key \<in> set (take (length list) keys) then list ! the_index keys key else (s(a := aa)) key) = (if key = a \<or> key \<in> set (take (length list) keys) then vals ! the_index (a # keys) key else s key) proof (prove)
goal (2 subgoals):
 1. \<And>a keys vals s aa list. \<lbrakk>\<And>vals s. foldl (\<lambda>s (x, y). s(x := y)) s (zip keys vals) a = (if a \<in> set (take (length vals) keys) then vals ! the_index keys key else s key); a \<notin> set keys \<and> distinct keys; vals = aa # list; key = a\<rbrakk> \<Longrightarrow> (if a \<in> set (take (length list) keys) then list ! the_index keys key else (s(a := aa)) key) = aa
 2. \<And>a keys vals s aa list. \<lbrakk>\<And>vals s. foldl (\<lambda>s (x, y). s(x := y)) s (zip keys vals) key = (if key \<in> set (take (length vals) keys) then vals ! the_index keys key else s key); a \<notin> set keys \<and> distinct keys; vals = aa # list; key \<noteq> a\<rbrakk> \<Longrightarrow> (if key \<in> set (take (length list) keys) then list ! the_index keys key else (s(a := aa)) key) = (if key \<in> set (take (length list) keys) then vals ! the_index (a # keys) key else s key) proof (prove)
goal (2 subgoals):
 1. \<And>keys aa list. \<lbrakk>\<And>vals s. foldl (\<lambda>s (x, y). s(x := y)) s (zip keys vals) key = (if key \<in> set (take (length vals) keys) then vals ! the_index keys key else s key); key \<notin> set keys; distinct keys; key \<in> set (take (length list) keys)\<rbrakk> \<Longrightarrow> list ! the_index keys key = aa
 2. \<And>a keys vals s aa list. \<lbrakk>\<And>vals s. foldl (\<lambda>s (x, y). s(x := y)) s (zip keys vals) key = (if key \<in> set (take (length vals) keys) then vals ! the_index keys key else s key); a \<notin> set keys \<and> distinct keys; vals = aa # list; key \<noteq> a\<rbrakk> \<Longrightarrow> (if key \<in> set (take (length list) keys) then list ! the_index keys key else (s(a := aa)) key) = (if key \<in> set (take (length list) keys) then vals ! the_index (a # keys) key else s key) proof (prove)
goal (2 subgoals):
 1. \<And>keys aa list. \<lbrakk>\<And>vals s. foldl (\<lambda>s (x, y). s(x := y)) s (zip keys vals) key = (if key \<in> set (take (length vals) keys) then vals ! the_index keys key else s key); key \<notin> set keys; distinct keys; key \<in> set keys\<rbrakk> \<Longrightarrow> list ! the_index keys key = aa
 2. \<And>a keys vals s aa list. \<lbrakk>\<And>vals s. foldl (\<lambda>s (x, y). s(x := y)) s (zip keys vals) key = (if key \<in> set (take (length vals) keys) then vals ! the_index keys key else s key); a \<notin> set keys \<and> distinct keys; vals = aa # list; key \<noteq> a\<rbrakk> \<Longrightarrow> (if key \<in> set (take (length list) keys) then list ! the_index keys key else (s(a := aa)) key) = (if key \<in> set (take (length list) keys) then vals ! the_index (a # keys) key else s key) proof (prove)
goal (1 subgoal):
 1. \<And>a keys vals s aa list. \<lbrakk>\<And>vals s. foldl (\<lambda>s (x, y). s(x := y)) s (zip keys vals) key = (if key \<in> set (take (length vals) keys) then vals ! the_index keys key else s key); a \<notin> set keys \<and> distinct keys; vals = aa # list; key \<noteq> a\<rbrakk> \<Longrightarrow> (if key \<in> set (take (length list) keys) then list ! the_index keys key else (s(a := aa)) key) = (if key \<in> set (take (length list) keys) then vals ! the_index (a # keys) key else s key) proof (prove)
goal:
No subgoals!