kings-crown/FVELER_Isabelle huggingface dataset:
theory GraphProof

lemma restr_trace_refine_Restr1_offset:
  "induct_var (NextNode n) iv
    \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 (restrs_list ((n, [iv + 1 ..< iv + j]) # rs1)) rs2 orel tr tr'
    \<Longrightarrow> j \<noteq> 0
    \<Longrightarrow> distinct (map fst rs1)
    \<Longrightarrow> wf_graph_function f1 ilen olen \<Longrightarrow> Gamma1 fn1 = Some f1
    \<Longrightarrow> pc' n (restrs_list ((n, [iv]) # (restrs_visit rs1 (NextNode n) f1))) tr
    \<Longrightarrow> \<not> pc' n (restrs_list ((n, [iv + (j - 1)]) # (restrs_visit rs1 (NextNode n) f1))) tr
    \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 (restrs_list rs1) rs2 orel tr tr'" by (rule restr_trace_refine_Restr1[where i="iv + 1" and j="iv + j"], simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>induct_var (NextNode n) iv; restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 (restrs_list ((n, [iv + 1..<iv + j]) # rs1)) rs2 orel tr tr'; j \<noteq> 0; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; pc' n (restrs_list ((n, [iv]) # restrs_visit rs1 (NextNode n) f1)) tr; \<not> pc' n (restrs_list ((n, [iv + (j - 1)]) # restrs_visit rs1 (NextNode n) f1)) tr\<rbrakk> \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 (restrs_list rs1) rs2 orel tr tr'
theory GraphProof

lemma restr_trace_refine_Restr2_offset:
  "induct_var (NextNode n) iv
    \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 (restrs_list ((n, [iv + 1 ..< iv + j]) # rs2)) orel tr tr'
    \<Longrightarrow> j \<noteq> 0
    \<Longrightarrow> distinct (map fst rs2)
    \<Longrightarrow> wf_graph_function f2 ilen olen \<Longrightarrow> Gamma2 fn2 = Some f2
    \<Longrightarrow> pc' n (restrs_list ((n, [iv]) # (restrs_visit rs2 (NextNode n) f2))) tr'
    \<Longrightarrow> \<not> pc' n (restrs_list ((n, [iv + (j - 1)]) # (restrs_visit rs2 (NextNode n) f2))) tr'
    \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 (restrs_list rs2) orel tr tr'" by (rule restr_trace_refine_Restr2[where i="iv + 1" and j="iv + j"], simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>induct_var (NextNode n) iv; restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 (restrs_list ((n, [iv + 1..<iv + j]) # rs2)) orel tr tr'; j \<noteq> 0; distinct (map fst rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; pc' n (restrs_list ((n, [iv]) # restrs_visit rs2 (NextNode n) f2)) tr'; \<not> pc' n (restrs_list ((n, [iv + (j - 1)]) # restrs_visit rs2 (NextNode n) f2)) tr'\<rbrakk> \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 (restrs_list rs2) orel tr tr'
theory GraphProof

lemma restr_trace_refine_PCCases1:
  "pc nn rs1 tr
        \<longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 rs2 orel tr tr'
    \<Longrightarrow> \<not> pc nn rs1 tr
        \<longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 rs2 orel tr tr'
    \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 rs2 orel tr tr'" by metis

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pc nn rs1 tr \<longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 rs2 orel tr tr'; \<not> pc nn rs1 tr \<longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 rs2 orel tr tr'\<rbrakk> \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 rs2 orel tr tr'
theory GraphProof

lemma restr_trace_refine_PCCases2:
  "pc nn rs2 tr'
        \<longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 rs2 orel tr tr'
    \<Longrightarrow> \<not> pc nn rs2 tr'
        \<longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 rs2 orel tr tr'
    \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 rs2 orel tr tr'" by metis

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pc nn rs2 tr' \<longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 rs2 orel tr tr'; \<not> pc nn rs2 tr' \<longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 rs2 orel tr tr'\<rbrakk> \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 rs2 orel tr tr'
theory global_asm_stmt_gref

lemma global_acc_valid:
  "global_acc_valid t_hrs_' t_hrs_'_update" by (simp add: global_acc_valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global_acc_valid t_hrs_' t_hrs_'_update
theory global_asm_stmt_gref

lemma t_hrs_ghost'state_update_globals_swap[simp]:
  "t_hrs_' (gswap (ghost'state_'_update f gs)) = t_hrs_' (gswap gs)" by (simp add: ghost'state_update_globals_swap)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t_hrs_' (gswap (ghost'state_'_update f gs)) = t_hrs_' (gswap gs)
theory global_asm_stmt_gref

lemma t_hrs_phantom_machine_state_'_update_globals_swap[simp]:
  "t_hrs_' (gswap (phantom_machine_state_'_update f gs)) = t_hrs_' (gswap gs)" by (simp add: phantom_machine_state_'_update_globals_swap)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t_hrs_' (gswap (phantom_machine_state_'_update f gs)) = t_hrs_' (gswap gs)
theory global_asm_stmt_gref

lemma globals_swap_twice[simp]:
  "gswap (gswap gs) = gs" by (metis globals_swap_twice_helper globals_list_distinct
            globals_list_valid global_acc_valid)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gswap (gswap gs) = gs
theory global_asm_stmt_gref

lemma t_hrs_'_update_hmu_triv[simp]:
  "f (hrs_mem (t_hrs_' gs)) = hrs_mem (t_hrs_' gs)
    \<Longrightarrow> t_hrs_'_update (hrs_mem_update f) gs = gs" by (cases gs, auto simp add: hrs_mem_update_def hrs_mem_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f (hrs_mem (t_hrs_' gs)) = hrs_mem (t_hrs_' gs) \<Longrightarrow> t_hrs_'_update (hrs_mem_update f) gs = gs
theory inf_loop_gref

lemma globals_list_valid:
  "globals_list_valid symbol_table t_hrs_' t_hrs_'_update globals_list" apply (rule globals_list_valid_optimisation[OF _ _ globals_list_ok]) apply (simp_all add: globals_list_def globals_list_valid_def
                       global_data_defs
                  del: distinct_prop.simps split del: if_split) apply (simp add: global_data_swappable_def global_data_def) apply (simp_all add: global_data_valid)? apply (simp_all add: global_data_valid_def addressed_global_data_def
                   const_global_data_def global_data_ok_def global_data_def
                   to_bytes_p_from_bytes)? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. globals_list_valid symbol_table t_hrs_' t_hrs_'_update global_data_list proof (prove)
goal (2 subgoals):
 1. distinct_prop global_data_swappable (filter is_global_data global_data_list)
 2. \<forall>g\<in>set global_data_list. global_data_valid t_hrs_' t_hrs_'_update g proof (prove)
goal (2 subgoals):
 1. distinct_prop global_data_swappable [global_data ''redundant_global'' redundant_global_' redundant_global_'_update]
 2. global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''another_redundant_global'' another_redundant_global) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''redundant_global'' redundant_global_' redundant_global_'_update) proof (prove)
goal (1 subgoal):
 1. global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''another_redundant_global'' another_redundant_global) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''redundant_global'' redundant_global_' redundant_global_'_update) proof (prove)
goal (1 subgoal):
 1. global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''another_redundant_global'' another_redundant_global) proof (prove)
goal:
No subgoals!
theory inf_loop_gref

lemma global_acc_valid:
  "global_acc_valid t_hrs_' t_hrs_'_update" by (simp add: global_acc_valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global_acc_valid t_hrs_' t_hrs_'_update
theory inf_loop_gref

lemma phantom_machine_state_'_update_globals_swap[simp]:
  "phantom_machine_state_' (gswap gs) = phantom_machine_state_' gs
    \<and> gswap (phantom_machine_state_'_update f gs) = phantom_machine_state_'_update f (gswap gs)" apply (rule globals_swap_ex_swap) apply (simp only: globals_list_def global_data_defs list.simps ball_simps
                     is_global_data_simps simp_thms) apply (simp_all add: global_data_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. phantom_machine_state_' (gswap gs) = phantom_machine_state_' gs \<and> gswap (phantom_machine_state_'_update f gs) = phantom_machine_state_'_update f (gswap gs) proof (prove)
goal (2 subgoals):
 1. \<forall>x\<in>set global_data_list. is_global_data x \<longrightarrow> (case x of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v v' gs. s' v (phantom_machine_state_'_update f gs) = phantom_machine_state_'_update f (s' v gs)) \<and> (\<forall>v gs. g' (phantom_machine_state_'_update f gs) = g' gs) \<and> (\<forall>v gs. phantom_machine_state_' (s' v gs) = phantom_machine_state_' gs))
 2. (\<forall>v v' gs. t_hrs_'_update v (phantom_machine_state_'_update f gs) = phantom_machine_state_'_update f (t_hrs_'_update v gs)) \<and> (\<forall>v gs. phantom_machine_state_' (t_hrs_'_update v gs) = phantom_machine_state_' gs) \<and> (\<forall>v gs. t_hrs_' (phantom_machine_state_'_update f gs) = t_hrs_' gs) proof (prove)
goal (2 subgoals):
 1. case global_data ''redundant_global'' redundant_global_' redundant_global_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (phantom_machine_state_'_update f gs) = phantom_machine_state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (phantom_machine_state_'_update f gs) = g' gs) \<and> (\<forall>v gs. phantom_machine_state_' (s' v gs) = phantom_machine_state_' gs)
 2. (\<forall>v v' gs. t_hrs_'_update v (phantom_machine_state_'_update f gs) = phantom_machine_state_'_update f (t_hrs_'_update v gs)) \<and> (\<forall>v gs. phantom_machine_state_' (t_hrs_'_update v gs) = phantom_machine_state_' gs) \<and> (\<forall>v gs. t_hrs_' (phantom_machine_state_'_update f gs) = t_hrs_' gs) proof (prove)
goal:
No subgoals!
theory inf_loop_gref

lemma t_hrs_ghost'state_update_globals_swap[simp]:
  "t_hrs_' (gswap (ghost'state_'_update f gs)) = t_hrs_' (gswap gs)" by (simp add: ghost'state_update_globals_swap)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t_hrs_' (gswap (ghost'state_'_update f gs)) = t_hrs_' (gswap gs)
theory inf_loop_gref

lemma t_hrs_phantom_machine_state_'_update_globals_swap[simp]:
  "t_hrs_' (gswap (phantom_machine_state_'_update f gs)) = t_hrs_' (gswap gs)" by (simp add: phantom_machine_state_'_update_globals_swap)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t_hrs_' (gswap (phantom_machine_state_'_update f gs)) = t_hrs_' (gswap gs)
theory inf_loop_gref

lemma globals_swap_twice[simp]:
  "gswap (gswap gs) = gs" by (metis globals_swap_twice_helper globals_list_distinct
            globals_list_valid global_acc_valid)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gswap (gswap gs) = gs
theory inf_loop_gref

lemma t_hrs_'_update_hmu_triv[simp]:
  "f (hrs_mem (t_hrs_' gs)) = hrs_mem (t_hrs_' gs)
    \<Longrightarrow> t_hrs_'_update (hrs_mem_update f) gs = gs" by (cases gs, auto simp add: hrs_mem_update_def hrs_mem_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f (hrs_mem (t_hrs_' gs)) = hrs_mem (t_hrs_' gs) \<Longrightarrow> t_hrs_'_update (hrs_mem_update f) gs = gs
theory global_array_swap_gref

lemma global_acc_valid:
  "global_acc_valid t_hrs_' t_hrs_'_update" by (simp add: global_acc_valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global_acc_valid t_hrs_' t_hrs_'_update
theory global_array_swap_gref

lemma phantom_machine_state_'_update_globals_swap[simp]:
  "phantom_machine_state_' (gswap gs) = phantom_machine_state_' gs
    \<and> gswap (phantom_machine_state_'_update f gs) = phantom_machine_state_'_update f (gswap gs)" apply (rule globals_swap_ex_swap) apply (simp only: globals_list_def global_data_defs list.simps ball_simps
                     is_global_data_simps simp_thms) apply (simp_all add: global_data_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. phantom_machine_state_' (gswap gs) = phantom_machine_state_' gs \<and> gswap (phantom_machine_state_'_update f gs) = phantom_machine_state_'_update f (gswap gs) proof (prove)
goal (2 subgoals):
 1. \<forall>x\<in>set global_data_list. is_global_data x \<longrightarrow> (case x of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v v' gs. s' v (phantom_machine_state_'_update f gs) = phantom_machine_state_'_update f (s' v gs)) \<and> (\<forall>v gs. g' (phantom_machine_state_'_update f gs) = g' gs) \<and> (\<forall>v gs. phantom_machine_state_' (s' v gs) = phantom_machine_state_' gs))
 2. (\<forall>v v' gs. t_hrs_'_update v (phantom_machine_state_'_update f gs) = phantom_machine_state_'_update f (t_hrs_'_update v gs)) \<and> (\<forall>v gs. phantom_machine_state_' (t_hrs_'_update v gs) = phantom_machine_state_' gs) \<and> (\<forall>v gs. t_hrs_' (phantom_machine_state_'_update f gs) = t_hrs_' gs) proof (prove)
goal (2 subgoals):
 1. (case global_data ''a_modified_global'' a_modified_global_' a_modified_global_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (phantom_machine_state_'_update f gs) = phantom_machine_state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (phantom_machine_state_'_update f gs) = g' gs) \<and> (\<forall>v gs. phantom_machine_state_' (s' v gs) = phantom_machine_state_' gs)) \<and> (case global_data ''toplevel'' toplevel_' toplevel_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (phantom_machine_state_'_update f gs) = phantom_machine_state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (phantom_machine_state_'_update f gs) = g' gs) \<and> (\<forall>v gs. phantom_machine_state_' (s' v gs) = phantom_machine_state_' gs))
 2. (\<forall>v v' gs. t_hrs_'_update v (phantom_machine_state_'_update f gs) = phantom_machine_state_'_update f (t_hrs_'_update v gs)) \<and> (\<forall>v gs. phantom_machine_state_' (t_hrs_'_update v gs) = phantom_machine_state_' gs) \<and> (\<forall>v gs. t_hrs_' (phantom_machine_state_'_update f gs) = t_hrs_' gs) proof (prove)
goal:
No subgoals!
theory global_array_swap_gref

lemma t_hrs_ghost'state_update_globals_swap[simp]:
  "t_hrs_' (gswap (ghost'state_'_update f gs)) = t_hrs_' (gswap gs)" by (simp add: ghost'state_update_globals_swap)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t_hrs_' (gswap (ghost'state_'_update f gs)) = t_hrs_' (gswap gs)
theory global_array_swap_gref

lemma t_hrs_phantom_machine_state_'_update_globals_swap[simp]:
  "t_hrs_' (gswap (phantom_machine_state_'_update f gs)) = t_hrs_' (gswap gs)" by (simp add: phantom_machine_state_'_update_globals_swap)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t_hrs_' (gswap (phantom_machine_state_'_update f gs)) = t_hrs_' (gswap gs)
theory global_array_swap_gref

lemma globals_swap_twice[simp]:
  "gswap (gswap gs) = gs" by (metis globals_swap_twice_helper globals_list_distinct
            globals_list_valid global_acc_valid)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gswap (gswap gs) = gs
theory global_array_swap_gref

lemma t_hrs_'_update_hmu_triv[simp]:
  "f (hrs_mem (t_hrs_' gs)) = hrs_mem (t_hrs_' gs)
    \<Longrightarrow> t_hrs_'_update (hrs_mem_update f) gs = gs" by (cases gs, auto simp add: hrs_mem_update_def hrs_mem_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f (hrs_mem (t_hrs_' gs)) = hrs_mem (t_hrs_' gs) \<Longrightarrow> t_hrs_'_update (hrs_mem_update f) gs = gs