kings-crown/FVELER_Isabelle huggingface dataset:
theory EquivValidTutorial

lemma work_at_desk_preserves_window_equiv:
  "\<lbrace>|window_equivalence|, P\<rbrace>
     work_at_desk
   \<lbrace>|window_equivalence|\<rbrace>" unfolding work_at_desk_def apply wp \<comment> \<open> Instead of \<open>apply(wp add:modify_ev)\<close> \<close> unfolding window_equivalence_def by force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (\<lambda>_ _. True) window_equivalence P work_at_desk proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (\<lambda>_ _. True) window_equivalence P (do modify (\<lambda>s. s\<lparr>desk := inbox s\<rparr>);
modify (\<lambda>s. s\<lparr>desk := job s (desk s)\<rparr>);
modify (\<lambda>s. s\<lparr>outbox := desk s\<rparr>)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> (\<forall>s t. True \<and> window_equivalence s t \<longrightarrow> True \<and> window_equivalence (s\<lparr>desk := inbox s\<rparr>) (t\<lparr>desk := inbox t\<rparr>)) \<and> (\<forall>s t. True \<and> window_equivalence s t \<longrightarrow> True \<and> window_equivalence (s\<lparr>desk := job s (desk s)\<rparr>) (t\<lparr>desk := job t (desk t)\<rparr>)) \<and> (\<forall>s t. True \<and> window_equivalence s t \<longrightarrow> True \<and> window_equivalence (s\<lparr>outbox := desk s\<rparr>) (t\<lparr>outbox := desk t\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> (\<forall>s t. True \<and> window s = window t \<longrightarrow> True \<and> window (s\<lparr>desk := inbox s\<rparr>) = window (t\<lparr>desk := inbox t\<rparr>)) \<and> (\<forall>s t. True \<and> window s = window t \<longrightarrow> True \<and> window (s\<lparr>desk := job s (desk s)\<rparr>) = window (t\<lparr>desk := job t (desk t)\<rparr>)) \<and> (\<forall>s t. True \<and> window s = window t \<longrightarrow> True \<and> window (s\<lparr>outbox := desk s\<rparr>) = window (t\<lparr>outbox := desk t\<rparr>))
theory EquivValidTutorial

lemma sanitise_desk_preserves_window_equiv:
  "\<lbrace>|window_equivalence|, P\<rbrace>
     sanitise_desk
   \<lbrace>|window_equivalence|\<rbrace>" unfolding sanitise_desk_def apply(rule pre_ev) apply wp \<comment> \<open> Instead of \<open>apply(wp add:modify_ev)\<close> \<close> unfolding window_equivalence_def by force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (\<lambda>_ _. True) window_equivalence P sanitise_desk proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (\<lambda>_ _. True) window_equivalence P (modify (desk_update (\<lambda>_. 0::'a))) proof (prove)
goal (2 subgoals):
 1. equiv_valid_inv (\<lambda>_ _. True) window_equivalence ?Q (modify (desk_update (\<lambda>_. 0::'a)))
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> \<forall>s t. True \<and> window_equivalence s t \<longrightarrow> True \<and> window_equivalence (s\<lparr>desk := 0::'a\<rparr>) (t\<lparr>desk := 0::'a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> \<forall>s t. True \<and> window s = window t \<longrightarrow> True \<and> window (s\<lparr>desk := 0::'a\<rparr>) = window (t\<lparr>desk := 0::'a\<rparr>)
theory EquivValidTutorial

lemma work_sanitise_reveal_preserves_window_equiv:
  "\<lbrace>|window_equivalence|, \<top>\<rbrace>
     work_sanitise_reveal
   \<lbrace>|window_equivalence|\<rbrace>" unfolding work_sanitise_reveal_def apply(wp add:reveal_const_desk_preserves_window_equiv[where c=0]
               sanitise_desk_preserves_window_equiv
               sanitise_desk_sets_zero
               work_at_desk_preserves_window_equiv) by force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (\<lambda>_ _. True) window_equivalence (\<lambda>_. True) work_sanitise_reveal proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (\<lambda>_ _. True) window_equivalence (\<lambda>_. True) (do work_at_desk;
sanitise_desk;
reveal_desk_to_window
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> K ?P10 s \<and> K ?P11 s
theory EquivValidTutorial

lemma reveal_desk_equiv_window_equiv_using_ev2:
  "\<lbrace>|desk_equivalence and window_equivalence|, \<top>\<rbrace>
     reveal_desk_to_window
   \<lbrace>|desk_equivalence and window_equivalence|\<rbrace>" unfolding reveal_desk_to_window_def apply(clarsimp simp:equiv_valid_def2)
  \<comment> \<open> After peeling back to \<open>equiv_valid_2\<close> form, we can use its \<open>modify\<close> rule. \<close> find_theorems intro apply(rule modify_ev2) unfolding desk_equivalence_def window_equivalence_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (\<lambda>_ _. True) (desk_equivalence and window_equivalence) (\<lambda>_. True) reveal_desk_to_window proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (\<lambda>_ _. True) (desk_equivalence and window_equivalence) (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>window := desk s\<rparr>)) proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv_inv (\<lambda>_ _. True) (desk_equivalence and window_equivalence) (=) (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>window := desk s\<rparr>)) proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv_inv (\<lambda>_ _. True) (desk_equivalence and window_equivalence) (=) (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>window := desk s\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>True; (desk_equivalence and window_equivalence) s t; True; True\<rbrakk> \<Longrightarrow> () = () \<and> True \<and> (desk_equivalence and window_equivalence) (s\<lparr>window := desk s\<rparr>) (t\<lparr>window := desk t\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>True; ((\<lambda>r1 r2. desk r1 = desk r2) and (\<lambda>r1 r2. window r1 = window r2)) s t; True; True\<rbrakk> \<Longrightarrow> () = () \<and> True \<and> ((\<lambda>r1 r2. desk r1 = desk r2) and (\<lambda>r1 r2. window r1 = window r2)) (s\<lparr>window := desk s\<rparr>) (t\<lparr>window := desk t\<rparr>)
theory EquivValidTutorial

lemma pitfall1_using_bind_ev:
  "\<lbrace>|\<top>\<top>|, (\<lambda>s. desk s = c)\<rbrace>
     do
       s \<leftarrow> get;
       return (desk s)
     od
   \<lbrace>|\<top>\<top>|\<rbrace>"
  \<comment> \<open> Using the bind rule for \<open>equiv_valid\<close> splits the goal into
      two \<open>equiv_valid\<close> statements, one for each of \<open>get\<close> and \<open>return\<close>.
      It will ask us to prove them in reverse order. \<close> apply(rule bind_ev_pre)
     \<comment> \<open> The \<open>wp\<close> tool discharges the \<open>return (desk s)\<close> part trivially: \<close> apply wp
    \<comment> \<open> But the return value of \<open>get\<close> is the entire state: \<close> apply(clarsimp simp:equiv_valid_def2 equiv_valid_2_def) apply(clarsimp simp add:get_def)
    \<comment> \<open> This causes us to get stuck, because we have no idea whether the state
        is equivalent for parts of the room other than the desk. \<close> oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (\<lambda>_ _. True) (\<lambda>_ _. True) (\<lambda>s. desk s = c) (do s <- get;
return (desk s)
od) proof (prove)
goal (4 subgoals):
 1. \<And>rv. equiv_valid_inv (\<lambda>_ _. True) (\<lambda>_ _. True) (?Q rv) (return (desk rv))
 2. equiv_valid_inv (\<lambda>_ _. True) (\<lambda>_ _. True) ?P' get
 3. \<lbrace>?P''\<rbrace> get \<lbrace>?Q\<rbrace>
 4. \<And>s. desk s = c \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (3 subgoals):
 1. equiv_valid_inv (\<lambda>_ _. True) (\<lambda>_ _. True) ?P' get
 2. \<lbrace>?P''\<rbrace> get \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>s. desk s = c \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (3 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (get s); (aa, ba) \<in> fst (get t); ?P' s; ?P' t\<rbrakk> \<Longrightarrow> a = aa
 2. \<lbrace>?P''\<rbrace> get \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>s. desk s = c \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (3 subgoals):
 1. \<And>s t. \<lbrakk>?P' s; ?P' t\<rbrakk> \<Longrightarrow> s = t
 2. \<lbrace>?P''\<rbrace> get \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>s. desk s = c \<Longrightarrow> ?P' s \<and> ?P'' s
theory EquivValidTutorial

lemma "equiv_valid_inv I A P f" unfolding equiv_valid_def2 equiv_valid_2_def oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A P f proof (prove)
goal (1 subgoal):
 1. \<forall>s t. P s \<and> P t \<and> I s t \<and> A s t \<longrightarrow> (\<forall>(rva, s')\<in>fst (f s). \<forall>(rvb, t')\<in>fst (f t). rva = rvb \<and> I s' t' \<and> A s' t')
theory EquivValidTutorial

lemma reveal_desk_equiv_to_window_equiv:
  "\<lbrace>|desk_equivalence|, \<top>\<rbrace>  \<comment> \<open> Pre-equivalence: The value of \<open>desk\<close> is
                                 the same initially in both runs. \<close>
     reveal_desk_to_window
   \<lbrace>|window_equivalence|\<rbrace>" \<comment> \<open> Post-equivalence: The value of \<open>window\<close> is required to be
                                the same at the end of both runs; no longer so for \<open>desk\<close>. \<close> unfolding reveal_desk_to_window_def apply(rule modify_ev'') unfolding window_equivalence_def desk_equivalence_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid (\<lambda>_ _. True) desk_equivalence window_equivalence (\<lambda>_. True) reveal_desk_to_window proof (prove)
goal (1 subgoal):
 1. equiv_valid (\<lambda>_ _. True) desk_equivalence window_equivalence (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>window := desk s\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>True; desk_equivalence s t; True; True\<rbrakk> \<Longrightarrow> True \<and> window_equivalence (s\<lparr>window := desk s\<rparr>) (t\<lparr>window := desk t\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>True; desk s = desk t; True; True\<rbrakk> \<Longrightarrow> True \<and> window (s\<lparr>window := desk s\<rparr>) = window (t\<lparr>window := desk t\<rparr>)
theory GraphProof

lemma exec_graph_n_Gamma_deterministic:
  "(stack, stack') \<in> exec_graph_n Gamma n
    \<Longrightarrow> (stack, stack'') \<in> exec_graph_n (adds ++ Gamma) n
    \<Longrightarrow> \<forall>gf \<in> ran Gamma. \<forall>nn fname inps outps.
        (Call nn fname inps outps) \<in> ran (function_graph gf) \<longrightarrow> fname \<notin> dom adds
    \<Longrightarrow> stack'' = stack'" using exec_graph_step_Gamma_deterministic apply (induct n arbitrary: stack' stack'', simp_all add: exec_graph_n_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(stack, stack') \<in> exec_graph_n Gamma n; (stack, stack'') \<in> exec_graph_n (adds ++ Gamma) n; \<forall>gf\<in>ran Gamma. \<forall>nn fname inps outps. node.Call nn fname inps outps \<in> ran (function_graph gf) \<longrightarrow> fname \<notin> dom adds\<rbrakk> \<Longrightarrow> stack'' = stack' proof (prove)
using this:
\<lbrakk>(?stack, ?stack') \<in> exec_graph_step ?Gamma; (?stack, ?stack'') \<in> exec_graph_step (?adds ++ ?Gamma); \<forall>gf\<in>ran ?Gamma. \<forall>nn fname inps outps. node.Call nn fname inps outps \<in> ran (function_graph gf) \<longrightarrow> fname \<notin> dom ?adds\<rbrakk> \<Longrightarrow> ?stack'' = ?stack'

goal (1 subgoal):
 1. \<lbrakk>(stack, stack') \<in> exec_graph_n Gamma n; (stack, stack'') \<in> exec_graph_n (adds ++ Gamma) n; \<forall>gf\<in>ran Gamma. \<forall>nn fname inps outps. node.Call nn fname inps outps \<in> ran (function_graph gf) \<longrightarrow> fname \<notin> dom adds\<rbrakk> \<Longrightarrow> stack'' = stack' proof (prove)
goal (1 subgoal):
 1. \<And>n stack' stack''. \<lbrakk>\<And>stack' stack''. \<lbrakk>(stack, stack') \<in> exec_graph_step Gamma ^^ n; (stack, stack'') \<in> exec_graph_step (adds ++ Gamma) ^^ n\<rbrakk> \<Longrightarrow> stack'' = stack'; (stack, stack') \<in> exec_graph_step Gamma ^^ n O exec_graph_step Gamma; (stack, stack'') \<in> exec_graph_step (adds ++ Gamma) ^^ n O exec_graph_step (adds ++ Gamma); \<forall>gf\<in>ran Gamma. \<forall>nn fname. (\<exists>inps outps. node.Call nn fname inps outps \<in> ran (function_graph gf)) \<longrightarrow> fname \<notin> dom adds; \<And>stack stack' Gamma stack'' adds. \<lbrakk>(stack, stack') \<in> exec_graph_step Gamma; (stack, stack'') \<in> exec_graph_step (adds ++ Gamma); \<forall>gf\<in>ran Gamma. \<forall>nn fname. (\<exists>inps outps. node.Call nn fname inps outps \<in> ran (function_graph gf)) \<longrightarrow> fname \<notin> dom adds\<rbrakk> \<Longrightarrow> stack'' = stack'\<rbrakk> \<Longrightarrow> stack'' = stack' proof (prove)
goal:
No subgoals!
theory GraphProof

lemma step_implies_continuing:
  "(stack, stack') \<in> exec_graph_step Gamma
    \<Longrightarrow> continuing stack" by (simp add: exec_graph_step_def continuing_def
         split: list.split_asm prod.split_asm next_node.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (stack, stack') \<in> exec_graph_step Gamma \<Longrightarrow> continuing stack
theory GraphProof

lemma exec_trace_nat_trace:
  "tr \<in> exec_trace Gamma f \<Longrightarrow> tr \<in> nat_trace_rel continuing (exec_graph_step Gamma)" by (clarsimp simp add: exec_trace_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tr \<in> exec_trace Gamma f \<Longrightarrow> tr \<in> nat_trace_rel continuing (exec_graph_step Gamma)
theory GraphProof

lemma tuple_switch_simps[simp]:
  "tuple_switch vs True = snd vs"
  "tuple_switch vs False = fst vs" by (auto simp: tuple_switch_def switch_val_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tuple_switch vs True = snd vs &&& tuple_switch vs False = fst vs
theory GraphProof

lemma trace_addr_SomeD:
  "trace_addr tr n = Some nn \<Longrightarrow> \<exists>st g. tr n = Some [(nn, st, g)]" by (simp add: trace_addr_def split: option.split_asm list.split_asm prod.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. trace_addr tr n = Some nn \<Longrightarrow> \<exists>st g. tr n = Some [(nn, st, g)]
theory GraphProof

lemma trace_addr_SomeI:
  "\<exists>x. tr n = Some [(nn, x)] \<Longrightarrow> trace_addr tr n = Some nn" by (clarsimp simp add: trace_addr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>x. tr n = Some [(nn, x)] \<Longrightarrow> trace_addr tr n = Some nn
theory GraphProof

lemma visit_known:
  "tr i = Some [(nn, st, g)]
    \<Longrightarrow> restrs_condition tr restrs i
    \<Longrightarrow> (\<forall>j < i. trace_addr tr j = Some nn \<longrightarrow> \<not> restrs_condition tr restrs j)
    \<Longrightarrow> visit tr nn restrs = Some st" apply (clarsimp simp: visit_def) apply (subst Least_equality, blast intro: trace_addr_SomeI) apply (blast intro: linorder_not_le[THEN iffD1]) apply (auto simp: trace_addr_SomeI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr i = Some [(nn, st, g)]; restrs_condition tr restrs i; \<forall>j<i. trace_addr tr j = Some nn \<longrightarrow> \<not> restrs_condition tr restrs j\<rbrakk> \<Longrightarrow> visit tr nn restrs = Some st proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr i = Some [(nn, st, g)]; restrs_condition tr restrs i; \<forall>j<i. trace_addr tr j = Some nn \<longrightarrow> \<not> restrs_condition tr restrs j\<rbrakk> \<Longrightarrow> ((\<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some nn) \<longrightarrow> fst (snd (hd (the (tr (LEAST i. restrs_condition tr restrs i \<and> trace_addr tr i = Some nn))))) = st) \<and> (\<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some nn) proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>tr i = Some [(nn, st, g)]; restrs_condition tr restrs i; \<forall>j<i. trace_addr tr j = Some nn \<longrightarrow> \<not> restrs_condition tr restrs j; restrs_condition tr restrs y \<and> trace_addr tr y = Some nn\<rbrakk> \<Longrightarrow> i \<le> y
 2. \<lbrakk>tr i = Some [(nn, st, g)]; restrs_condition tr restrs i; \<forall>j<i. trace_addr tr j = Some nn \<longrightarrow> \<not> restrs_condition tr restrs j\<rbrakk> \<Longrightarrow> ((\<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some nn) \<longrightarrow> fst (snd (hd (the (tr i)))) = st) \<and> (\<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some nn) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr i = Some [(nn, st, g)]; restrs_condition tr restrs i; \<forall>j<i. trace_addr tr j = Some nn \<longrightarrow> \<not> restrs_condition tr restrs j\<rbrakk> \<Longrightarrow> ((\<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some nn) \<longrightarrow> fst (snd (hd (the (tr i)))) = st) \<and> (\<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some nn) proof (prove)
goal:
No subgoals!
theory GraphProof

lemma fold_invariant:
  "(\<forall>x \<in> set xs. \<forall> s. g (f x s) = g s) \<Longrightarrow> g s = v \<Longrightarrow> g (fold f xs s) = v" by (induct xs arbitrary: s, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set xs. \<forall>s. g (f x s) = g s; g s = v\<rbrakk> \<Longrightarrow> g (fold f xs s) = v
theory GraphProof

lemma var_acc_var_upd:
  "var_acc s (var_upd s' v st)
    = (if s = s' then v else var_acc s st)" by (cases st, simp add: var_acc_def var_upd_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. var_acc s (var_upd s' v st) = (if s = s' then v else var_acc s st)
theory GraphProof

lemma var_acc_save_vals_distinct:
  "distinct xs \<Longrightarrow> length xs = length vs
    \<Longrightarrow> map (\<lambda>i. var_acc i (save_vals xs vs st)) xs = vs" apply (induct xs arbitrary: vs st) apply simp apply (case_tac vs, simp_all add: save_vals_def) apply (rule fold_invariant) apply (clarsimp simp: var_acc_var_upd elim!: in_set_zipE) apply (simp add: var_acc_var_upd) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; length xs = length vs\<rbrakk> \<Longrightarrow> map (\<lambda>i. var_acc i (save_vals xs vs st)) xs = vs proof (prove)
goal (2 subgoals):
 1. \<And>vs st. \<lbrakk>distinct []; length [] = length vs\<rbrakk> \<Longrightarrow> map (\<lambda>i. var_acc i (save_vals [] vs st)) [] = vs
 2. \<And>x1 xs vs st. \<lbrakk>\<And>vs st. \<lbrakk>distinct xs; length xs = length vs\<rbrakk> \<Longrightarrow> map (\<lambda>i. var_acc i (save_vals xs vs st)) xs = vs; distinct (x1 # xs); length (x1 # xs) = length vs\<rbrakk> \<Longrightarrow> map (\<lambda>i. var_acc i (save_vals (x1 # xs) vs st)) (x1 # xs) = vs proof (prove)
goal (1 subgoal):
 1. \<And>x1 xs vs st. \<lbrakk>\<And>vs st. \<lbrakk>distinct xs; length xs = length vs\<rbrakk> \<Longrightarrow> map (\<lambda>i. var_acc i (save_vals xs vs st)) xs = vs; distinct (x1 # xs); length (x1 # xs) = length vs\<rbrakk> \<Longrightarrow> map (\<lambda>i. var_acc i (save_vals (x1 # xs) vs st)) (x1 # xs) = vs proof (prove)
goal (1 subgoal):
 1. \<And>x1 xs vs st a list. \<lbrakk>\<And>vs st. length list = length vs \<Longrightarrow> map (\<lambda>i. var_acc i (fold (\<lambda>(x, y). var_upd x y) (zip xs vs) st)) xs = vs; x1 \<notin> set xs \<and> distinct xs; length xs = length list; vs = a # list\<rbrakk> \<Longrightarrow> var_acc x1 (fold (\<lambda>(x, y). var_upd x y) (zip xs list) (var_upd x1 a st)) = a proof (prove)
goal (2 subgoals):
 1. \<And>x1 xs vs st a list. \<lbrakk>\<And>vs st. length list = length vs \<Longrightarrow> map (\<lambda>i. var_acc i (fold (\<lambda>(x, y). var_upd x y) (zip xs vs) st)) xs = vs; x1 \<notin> set xs \<and> distinct xs; length xs = length list; vs = a # list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (zip xs list). \<forall>s. var_acc x1 ((case x of (x, xa) \<Rightarrow> var_upd x xa) s) = var_acc x1 s
 2. \<And>x1 xs vs st a list. \<lbrakk>\<And>vs st. length list = length vs \<Longrightarrow> map (\<lambda>i. var_acc i (fold (\<lambda>(x, y). var_upd x y) (zip xs vs) st)) xs = vs; x1 \<notin> set xs \<and> distinct xs; length xs = length list; vs = a # list\<rbrakk> \<Longrightarrow> var_acc x1 (var_upd x1 a st) = a proof (prove)
goal (1 subgoal):
 1. \<And>x1 xs vs st a list. \<lbrakk>\<And>vs st. length list = length vs \<Longrightarrow> map (\<lambda>i. var_acc i (fold (\<lambda>(x, y). var_upd x y) (zip xs vs) st)) xs = vs; x1 \<notin> set xs \<and> distinct xs; length xs = length list; vs = a # list\<rbrakk> \<Longrightarrow> var_acc x1 (var_upd x1 a st) = a proof (prove)
goal:
No subgoals!
theory GraphProof

lemma wf_graph_function_acc_vars_save_vals:
  "\<lbrakk> wf_graph_function f ilen olen; xs = function_inputs f; length vs = ilen \<rbrakk>
    \<Longrightarrow> acc_vars xs (save_vals xs vs st) = vs" by (cases f, simp add: acc_vars_def wf_graph_function_def
                         var_acc_save_vals_distinct)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_graph_function f ilen olen; xs = function_inputs f; length vs = ilen\<rbrakk> \<Longrightarrow> acc_vars xs (save_vals xs vs st) = vs
theory GraphProof

lemma wf_graph_function_length_function_inputs:
  "wf_graph_function f ilen olen \<Longrightarrow> length (function_inputs f) = ilen" by (cases f, simp_all add: wf_graph_function_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wf_graph_function f ilen olen \<Longrightarrow> length (function_inputs f) = ilen
theory GraphProof

lemma Collect_less_Suc:
  "{i. i < Suc n \<and> P i} = {i. i < n \<and> P i} \<union> (if P n then {n} else {})" by (auto simp: less_Suc_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {i. i < Suc n \<and> P i} = {i. i < n \<and> P i} \<union> (if P n then {n} else {})
theory GraphProof

lemma trace_addr_trace_bottom_addr_eq:
  "trace_addr tr i = Some addr \<Longrightarrow> trace_bottom_addr tr i = Some addr" by (clarsimp simp: trace_bottom_addr_def dest!: trace_addr_SomeD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. trace_addr tr i = Some addr \<Longrightarrow> trace_bottom_addr tr i = Some addr