kings-crown/FVELER_Isabelle huggingface dataset:
theory Heap_List

lemma heap_path_distinct_next_not_in:
  "\<lbrakk>heap_path hp st xs ed; distinct xs; p \<notin> set xs; hp p = Some np;
    sym_heap hp hp'; st \<noteq> Some np\<rbrakk>
  \<Longrightarrow> np \<notin> set xs" by (fastforce dest!: heap_path_distinct_sym_prev_cases[simplified])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_path hp st xs ed; distinct xs; p \<notin> set xs; hp p = Some np; sym_heap hp hp'; st \<noteq> Some np\<rbrakk> \<Longrightarrow> np \<notin> set xs
theory Heap_List

lemma heap_ls_next_not_in:
  "\<lbrakk>heap_ls hp st xs; p \<notin> set xs; hp p = Some np; sym_heap hp hp'; st \<noteq> Some np\<rbrakk>
  \<Longrightarrow> np \<notin> set xs" by (fastforce dest!: heap_ls_prev_cases[simplified])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; p \<notin> set xs; hp p = Some np; sym_heap hp hp'; st \<noteq> Some np\<rbrakk> \<Longrightarrow> np \<notin> set xs
theory Heap_List

lemma sym_heap_prev_None_is_start:
  "\<lbrakk>heap_ls hp st xs; sym_heap hp hp'; p \<in> set xs; hp' p = None\<rbrakk>
   \<Longrightarrow> Some p = st" using split_list_last heap_path_sym_heap_non_nil_lookup_prev by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; sym_heap hp hp'; p \<in> set xs; hp' p = None\<rbrakk> \<Longrightarrow> Some p = st proof (prove)
using this:
?x \<in> set ?xs \<Longrightarrow> \<exists>ys zs. ?xs = ys @ ?x # zs \<and> ?x \<notin> set zs
\<lbrakk>heap_ls ?hp ?x (?xs @ ?z # ?ys); sym_heap ?hp ?hp'; ?xs \<noteq> []\<rbrakk> \<Longrightarrow> ?hp' ?z = Some (last ?xs)

goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; sym_heap hp hp'; p \<in> set xs; hp' p = None\<rbrakk> \<Longrightarrow> Some p = st
theory Heap_List

lemma not_last_next_not_None:
  "\<lbrakk>heap_ls hp st xs; p \<in> set xs; p \<noteq> last xs\<rbrakk> \<Longrightarrow> hp p \<noteq> None" by (fastforce intro: heap_path_head dest: split_list)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; p \<in> set xs; p \<noteq> last xs\<rbrakk> \<Longrightarrow> hp p \<noteq> None
theory Heap_List

lemma not_head_prev_not_None:
  "\<lbrakk>heap_ls hp st xs; p \<in> set xs; p \<noteq> hd xs; sym_heap hp hp'\<rbrakk>
   \<Longrightarrow> hp' p \<noteq> None" using sym_heap_prev_None_is_start heap_path_head by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; p \<in> set xs; p \<noteq> hd xs; sym_heap hp hp'\<rbrakk> \<Longrightarrow> hp' p \<noteq> None proof (prove)
using this:
\<lbrakk>heap_ls ?hp ?st ?xs; sym_heap ?hp ?hp'; ?p \<in> set ?xs; ?hp' ?p = None\<rbrakk> \<Longrightarrow> Some ?p = ?st
\<lbrakk>heap_path ?hp ?st ?xs ?y; ?xs \<noteq> []\<rbrakk> \<Longrightarrow> ?st = Some (hd ?xs)

goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; p \<in> set xs; p \<noteq> hd xs; sym_heap hp hp'\<rbrakk> \<Longrightarrow> hp' p \<noteq> None
theory Heap_List

lemma takeWhile_neq_notin_same:
  "x \<notin> set xs \<Longrightarrow> takeWhile ((\<noteq>) x) xs = xs" using takeWhile_eq_all_conv by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<notin> set xs \<Longrightarrow> takeWhile ((\<noteq>) x) xs = xs proof (prove)
using this:
(takeWhile ?P ?xs = ?xs) = (\<forall>x\<in>set ?xs. ?P x)

goal (1 subgoal):
 1. x \<notin> set xs \<Longrightarrow> takeWhile ((\<noteq>) x) xs = xs
theory Heap_List

lemma heap_ls_next_takeWhile_append_sym:
  "\<lbrakk>heap_ls hp st xs; np \<in> set xs; st \<noteq> Some np; hp p = Some np; sym_heap hp hp'\<rbrakk>
  \<Longrightarrow>takeWhile ((\<noteq>) np) xs = (takeWhile ((\<noteq>) p) xs) @ [p]" apply (frule (3) heap_ls_prev_cases, simp) apply (fastforce elim!: heap_ls_next_takeWhile_append) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; np \<in> set xs; st \<noteq> Some np; hp p = Some np; sym_heap hp hp'\<rbrakk> \<Longrightarrow> takeWhile ((\<noteq>) np) xs = takeWhile ((\<noteq>) p) xs @ [p] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; np \<in> set xs; st \<noteq> Some np; hp p = Some np; sym_heap hp hp'; p \<in> set xs\<rbrakk> \<Longrightarrow> takeWhile ((\<noteq>) np) xs = takeWhile ((\<noteq>) p) xs @ [p] proof (prove)
goal:
No subgoals!
theory Heap_List

lemma heap_ls_prepend:
  "\<lbrakk>heap_ls hp st xs; new \<notin> set xs; xs \<noteq> []\<rbrakk>
   \<Longrightarrow> heap_ls (hp(new := Some (hd xs))) (Some new) (new # xs)" apply simp apply (erule heap_path_heap_upd_not_in[rotated]) apply (frule (1) heap_path_head) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; new \<notin> set xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> heap_ls (hp(new \<mapsto> hd xs)) (Some new) (new # xs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; new \<notin> set xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> heap_ls (hp(new \<mapsto> hd xs)) (Some (hd xs)) xs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> heap_ls hp (Some (hd xs)) xs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; xs \<noteq> []; st = Some (hd xs)\<rbrakk> \<Longrightarrow> heap_ls hp (Some (hd xs)) xs proof (prove)
goal:
No subgoals!
theory Heap_List

lemma heap_ls_append:
  "\<lbrakk>heap_ls hp st xs; xs \<noteq> []; new \<notin> set xs\<rbrakk>
   \<Longrightarrow> heap_ls (hp(last xs := Some new, new := None)) st (xs @ [new])" apply (frule heap_ls_distinct) apply simp apply (rule heap_path_heap_upd_not_in) apply (fastforce simp: heap_path_last_update) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; xs \<noteq> []; new \<notin> set xs\<rbrakk> \<Longrightarrow> heap_ls (hp(last xs \<mapsto> new, new := None)) st (xs @ [new]) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; xs \<noteq> []; new \<notin> set xs; distinct xs\<rbrakk> \<Longrightarrow> heap_ls (hp(last xs \<mapsto> new, new := None)) st (xs @ [new]) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; xs \<noteq> []; new \<notin> set xs; distinct xs\<rbrakk> \<Longrightarrow> heap_path (hp(last xs \<mapsto> new, new := None)) st xs (Some new) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>heap_ls hp st xs; xs \<noteq> []; new \<notin> set xs; distinct xs\<rbrakk> \<Longrightarrow> heap_path (hp(last xs \<mapsto> new)) st xs (Some new)
 2. \<lbrakk>heap_ls hp st xs; xs \<noteq> []; new \<notin> set xs; distinct xs\<rbrakk> \<Longrightarrow> new \<notin> set xs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; xs \<noteq> []; new \<notin> set xs; distinct xs\<rbrakk> \<Longrightarrow> new \<notin> set xs proof (prove)
goal:
No subgoals!
theory Heap_List

lemma heap_ls_list_insert_before:
  "\<lbrakk>heap_ls hp st (xs @ ys); new \<notin> set (xs @ ys); xs \<noteq> []; ys \<noteq> []\<rbrakk>
   \<Longrightarrow> heap_ls (hp(last xs := Some new, new := Some (hd ys))) st
               (list_insert_before (xs @ ys) (hd ys) new)" apply (frule heap_ls_distinct) apply (subst list_insert_before_distinct; fastforce?) apply simp apply (rule conjI)
   \<comment> \<open>the path until new\<close> apply (fastforce intro: heap_path_heap_upd_not_in heap_path_last_update)
  \<comment> \<open>the path from hd ys\<close> apply (metis disjoint_iff_not_equal heap_path_head heap_path_heap_upd_not_in last_in_set) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st (xs @ ys); new \<notin> set (xs @ ys); xs \<noteq> []; ys \<noteq> []\<rbrakk> \<Longrightarrow> heap_ls (hp(last xs \<mapsto> new, new \<mapsto> hd ys)) st (list_insert_before (xs @ ys) (hd ys) new) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st (xs @ ys); new \<notin> set (xs @ ys); xs \<noteq> []; ys \<noteq> []; distinct (xs @ ys)\<rbrakk> \<Longrightarrow> heap_ls (hp(last xs \<mapsto> new, new \<mapsto> hd ys)) st (list_insert_before (xs @ ys) (hd ys) new) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st (xs @ ys); new \<notin> set (xs @ ys); xs \<noteq> []; ys \<noteq> []; distinct (xs @ ys)\<rbrakk> \<Longrightarrow> heap_ls (hp(last xs \<mapsto> new, new \<mapsto> hd ys)) st (xs @ new # ys) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>x. heap_path hp st xs x \<and> heap_ls hp x ys; new \<notin> set xs \<and> new \<notin> set ys; xs \<noteq> []; ys \<noteq> []; distinct xs \<and> distinct ys \<and> set xs \<inter> set ys = {}\<rbrakk> \<Longrightarrow> heap_path (hp(last xs \<mapsto> new, new \<mapsto> hd ys)) st xs (Some new) \<and> heap_ls (hp(last xs \<mapsto> new, new \<mapsto> hd ys)) (Some (hd ys)) ys proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<exists>x. heap_path hp st xs x \<and> heap_ls hp x ys; new \<notin> set xs \<and> new \<notin> set ys; xs \<noteq> []; ys \<noteq> []; distinct xs \<and> distinct ys \<and> set xs \<inter> set ys = {}\<rbrakk> \<Longrightarrow> heap_path (hp(last xs \<mapsto> new, new \<mapsto> hd ys)) st xs (Some new)
 2. \<lbrakk>\<exists>x. heap_path hp st xs x \<and> heap_ls hp x ys; new \<notin> set xs \<and> new \<notin> set ys; xs \<noteq> []; ys \<noteq> []; distinct xs \<and> distinct ys \<and> set xs \<inter> set ys = {}\<rbrakk> \<Longrightarrow> heap_ls (hp(last xs \<mapsto> new, new \<mapsto> hd ys)) (Some (hd ys)) ys proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>x. heap_path hp st xs x \<and> heap_ls hp x ys; new \<notin> set xs \<and> new \<notin> set ys; xs \<noteq> []; ys \<noteq> []; distinct xs \<and> distinct ys \<and> set xs \<inter> set ys = {}\<rbrakk> \<Longrightarrow> heap_ls (hp(last xs \<mapsto> new, new \<mapsto> hd ys)) (Some (hd ys)) ys proof (prove)
goal:
No subgoals!
theory Heap_List

lemma heap_ls_remove_singleton:
  "heap_ls hp st [x] \<Longrightarrow> heap_ls (hp(x := None)) None []" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_ls hp st [x] \<Longrightarrow> heap_ls (hp(x := None)) None []
theory Heap_List

lemma heap_ls_remove_head_not_singleton:
  "\<lbrakk>heap_ls hp st xs; tl xs \<noteq> []\<rbrakk>
   \<Longrightarrow> heap_ls (hp(hd xs := None)) (Some (hd (tl xs))) (tl xs)" apply (frule heap_ls_distinct) apply (cases xs; simp) apply clarsimp apply (frule heap_path_head) apply fastforce apply (fastforce elim!: heap_path_heap_upd_not_in) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; tl xs \<noteq> []\<rbrakk> \<Longrightarrow> heap_ls (hp(hd xs := None)) (Some (hd (tl xs))) (tl xs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; tl xs \<noteq> []; distinct xs\<rbrakk> \<Longrightarrow> heap_ls (hp(hd xs := None)) (Some (hd (tl xs))) (tl xs) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>st = Some a \<and> heap_ls hp (hp a) list; list \<noteq> []; a \<notin> set list \<and> distinct list; xs = a # list\<rbrakk> \<Longrightarrow> heap_ls (hp(a := None)) (Some (hd list)) list proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>list \<noteq> []; xs = a # list; st = Some a; heap_ls hp (hp a) list; a \<notin> set list; distinct list\<rbrakk> \<Longrightarrow> heap_ls (hp(a := None)) (Some (hd list)) list proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>list \<noteq> []; xs = a # list; st = Some a; heap_ls hp (hp a) list; a \<notin> set list; distinct list\<rbrakk> \<Longrightarrow> list \<noteq> []
 2. \<And>a list. \<lbrakk>list \<noteq> []; xs = a # list; st = Some a; heap_ls hp (hp a) list; a \<notin> set list; distinct list; hp a = Some (hd list)\<rbrakk> \<Longrightarrow> heap_ls (hp(a := None)) (Some (hd list)) list proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>list \<noteq> []; xs = a # list; st = Some a; heap_ls hp (hp a) list; a \<notin> set list; distinct list; hp a = Some (hd list)\<rbrakk> \<Longrightarrow> heap_ls (hp(a := None)) (Some (hd list)) list proof (prove)
goal:
No subgoals!
theory Heap_List

lemma heap_ls_remove_last_not_singleton:
  "\<lbrakk>heap_ls hp st xs; butlast xs \<noteq> []\<rbrakk>
   \<Longrightarrow> heap_ls (hp((last (butlast xs)) := None)) st (butlast xs)" apply (frule heap_ls_distinct) apply (frule distinct_butlast) apply (fastforce dest: heap_path_last_update heap_path_butlast) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; butlast xs \<noteq> []\<rbrakk> \<Longrightarrow> heap_ls (hp(last (butlast xs) := None)) st (butlast xs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; butlast xs \<noteq> []; distinct xs\<rbrakk> \<Longrightarrow> heap_ls (hp(last (butlast xs) := None)) st (butlast xs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; butlast xs \<noteq> []; distinct xs; distinct (butlast xs)\<rbrakk> \<Longrightarrow> heap_ls (hp(last (butlast xs) := None)) st (butlast xs) proof (prove)
goal:
No subgoals!
theory Trace_Strengthen_Setup

lemma strengthen_hoare[strg]:
  "\<lbrakk>\<And>r s. st F (\<longrightarrow>) (Q r s) (R r s)\<rbrakk>
   \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>) (\<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>)" by (cases F, auto elim: hoare_strengthen_post)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>r s. st F (\<longrightarrow>) (Q r s) (R r s)) \<Longrightarrow> st F (\<longrightarrow>) \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>
theory Trace_Strengthen_Setup

lemma strengthen_validE_R_cong[strg]:
  "\<lbrakk>\<And>r s. st F (\<longrightarrow>) (Q r s) (R r s)\<rbrakk>
   \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -) (\<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, -)" by (cases F, auto intro: hoare_post_imp_R)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>r s. st F (\<longrightarrow>) (Q r s) (R r s)) \<Longrightarrow> st F (\<longrightarrow>) \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, - \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, -
theory Trace_Strengthen_Setup

lemma strengthen_validE_cong[strg]:
  "\<lbrakk>\<And>r s. st F (\<longrightarrow>) (Q r s) (R r s); \<And>r s. st F (\<longrightarrow>) (S r s) (T r s)\<rbrakk>
   \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>S\<rbrace>) (\<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>T\<rbrace>)" by (cases F, auto elim: hoare_post_impErr)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r s. st F (\<longrightarrow>) (Q r s) (R r s); \<And>r s. st F (\<longrightarrow>) (S r s) (T r s)\<rbrakk> \<Longrightarrow> st F (\<longrightarrow>) \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>S\<rbrace> \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>T\<rbrace>
theory Trace_Strengthen_Setup

lemma strengthen_validE_E_cong[strg]:
  "\<lbrakk>\<And>r s. st F (\<longrightarrow>) (S r s) (T r s)\<rbrakk>
   \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f -, \<lbrace>S\<rbrace>) (\<lbrace>P\<rbrace> f -, \<lbrace>T\<rbrace>)" by (cases F, auto elim: hoare_post_impErr simp: validE_E_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>r s. st F (\<longrightarrow>) (S r s) (T r s)) \<Longrightarrow> st F (\<longrightarrow>) \<lbrace>P\<rbrace> f -, \<lbrace>S\<rbrace> \<lbrace>P\<rbrace> f -, \<lbrace>T\<rbrace>
theory Trace_Strengthen_Setup

lemma strengthen_validI[strg]:
  "\<lbrakk>\<And>r s0 s. st F (\<longrightarrow>) (Q r s0 s) (Q' r s0 s)\<rbrakk>
   \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace>,\<lbrace>G\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>Q\<rbrace>) (\<lbrace>P\<rbrace>,\<lbrace>G\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>Q'\<rbrace>)" by (cases F, auto elim: rg_strengthen_post)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>r s0 s. st F (\<longrightarrow>) (Q r s0 s) (Q' r s0 s)) \<Longrightarrow> st F (\<longrightarrow>) \<lbrace>P\<rbrace>, \<lbrace>G\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>Q\<rbrace> \<lbrace>P\<rbrace>, \<lbrace>G\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>Q'\<rbrace>
theory Trace_Strengthen_Setup

lemma wpfix_strengthen_hoare:
  "\<lbrakk>\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s); \<And>r s. st F (\<longrightarrow>) (Q r s) (Q' r s)\<rbrakk>
   \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>) (\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>)" by (cases F, auto elim: hoare_chain)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s); \<And>r s. st F (\<longrightarrow>) (Q r s) (Q' r s)\<rbrakk> \<Longrightarrow> st F (\<longrightarrow>) \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>
theory Trace_Strengthen_Setup

lemma wpfix_strengthen_validE_R_cong:
  "\<lbrakk>\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s); \<And>r s. st F (\<longrightarrow>) (Q r s) (Q' r s)\<rbrakk>
   \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -) (\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>, -)" by (cases F, auto elim: hoare_chainE simp: validE_R_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s); \<And>r s. st F (\<longrightarrow>) (Q r s) (Q' r s)\<rbrakk> \<Longrightarrow> st F (\<longrightarrow>) \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, - \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>, -
theory Trace_Strengthen_Setup

lemma wpfix_strengthen_validE_cong:
  "\<lbrakk>\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s); \<And>r s. st F (\<longrightarrow>) (Q r s) (R r s);
    \<And>r s. st F (\<longrightarrow>) (S r s) (T r s)\<rbrakk>
   \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>S\<rbrace>) (\<lbrace>P'\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>T\<rbrace>)" by (cases F, auto elim: hoare_chainE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s); \<And>r s. st F (\<longrightarrow>) (Q r s) (R r s); \<And>r s. st F (\<longrightarrow>) (S r s) (T r s)\<rbrakk> \<Longrightarrow> st F (\<longrightarrow>) \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>S\<rbrace> \<lbrace>P'\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>T\<rbrace>
theory Trace_Strengthen_Setup

lemma wpfix_strengthen_validE_E_cong:
  "\<lbrakk>\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s); \<And>r s. st F (\<longrightarrow>) (S r s) (T r s)\<rbrakk>
   \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f -, \<lbrace>S\<rbrace>) (\<lbrace>P'\<rbrace> f -, \<lbrace>T\<rbrace>)" by (cases F, auto elim: hoare_chainE simp: validE_E_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s); \<And>r s. st F (\<longrightarrow>) (S r s) (T r s)\<rbrakk> \<Longrightarrow> st F (\<longrightarrow>) \<lbrace>P\<rbrace> f -, \<lbrace>S\<rbrace> \<lbrace>P'\<rbrace> f -, \<lbrace>T\<rbrace>
theory Trace_Strengthen_Setup

lemma wpfix_no_fail_cong:
  "\<lbrakk>\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s)\<rbrakk>
   \<Longrightarrow> st F (\<longrightarrow>) (no_fail P f) (no_fail P' f)" by (cases F, auto elim: no_fail_pre)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s)) \<Longrightarrow> st F (\<longrightarrow>) (no_fail P f) (no_fail P' f)
theory Triv_Refinement

lemma triv_refinement_mono_bind:
  "triv_refinement a c \<Longrightarrow> triv_refinement (a >>= b) (c >>= b)"
  "(\<forall>x. triv_refinement (b x) (d x)) \<Longrightarrow> triv_refinement (a >>= b) (a >>= d)" apply (simp add: triv_refinement_def bind_def) apply (intro allI UN_mono; simp) apply (simp only: triv_refinement_def bind_def' split_def) apply (intro Un_mono allI order_refl UN_mono image_mono) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (triv_refinement a c \<Longrightarrow> triv_refinement (a >>= b) (c >>= b)) &&& (\<forall>x. triv_refinement (b x) (d x) \<Longrightarrow> triv_refinement (a >>= b) (a >>= d)) proof (prove)
goal (2 subgoals):
 1. \<forall>s. c s \<subseteq> a s \<Longrightarrow> \<forall>s. (\<Union>x\<in>c s. case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` b rv s) \<subseteq> (\<Union>x\<in>a s. case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` b rv s)
 2. \<forall>x. triv_refinement (b x) (d x) \<Longrightarrow> triv_refinement (a >>= b) (a >>= d) proof (prove)
goal (1 subgoal):
 1. \<forall>x. triv_refinement (b x) (d x) \<Longrightarrow> triv_refinement (a >>= b) (a >>= d) proof (prove)
goal (1 subgoal):
 1. \<forall>x s. d x s \<subseteq> b x s \<Longrightarrow> \<forall>s. (\<lambda>xs. (xs, Failed)) ` {xs. (xs, Failed) \<in> a s} \<union> (\<lambda>xs. (xs, Incomplete)) ` {xs. (xs, Incomplete) \<in> a s} \<union> (\<Union>p\<in>{p. (fst p, Result (fst (snd p), snd (snd p))) \<in> a s}. (\<lambda>pa. (fst pa @ fst p, snd pa)) ` d (fst (snd p)) (snd (snd p))) \<subseteq> (\<lambda>xs. (xs, Failed)) ` {xs. (xs, Failed) \<in> a s} \<union> (\<lambda>xs. (xs, Incomplete)) ` {xs. (xs, Incomplete) \<in> a s} \<union> (\<Union>p\<in>{p. (fst p, Result (fst (snd p), snd (snd p))) \<in> a s}. (\<lambda>pa. (fst pa @ fst p, snd pa)) ` b (fst (snd p)) (snd (snd p))) proof (prove)
goal (1 subgoal):
 1. \<And>s p. \<lbrakk>\<forall>x s. d x s \<subseteq> b x s; p \<in> {p. (fst p, Result (fst (snd p), snd (snd p))) \<in> a s}\<rbrakk> \<Longrightarrow> d (fst (snd p)) (snd (snd p)) \<subseteq> b (fst (snd p)) (snd (snd p)) proof (prove)
goal:
No subgoals!
theory Triv_Refinement

lemma triv_refinement_trans:
  "triv_refinement f g \<Longrightarrow> triv_refinement g h
    \<Longrightarrow> triv_refinement f h" by (auto simp add: triv_refinement_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>triv_refinement f g; triv_refinement g h\<rbrakk> \<Longrightarrow> triv_refinement f h
theory Triv_Refinement

lemma triv_refinement_bind:
  "triv_refinement a c
    \<Longrightarrow> (\<forall>x. triv_refinement (b x) (d x))
    \<Longrightarrow> triv_refinement (bind a b) (bind c d)" by (metis triv_refinement_mono_bind triv_refinement_trans)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>triv_refinement a c; \<forall>x. triv_refinement (b x) (d x)\<rbrakk> \<Longrightarrow> triv_refinement (a >>= b) (c >>= d)
theory Triv_Refinement

lemma triv_refinement_mono_parallel:
  "triv_refinement a b \<Longrightarrow> triv_refinement (parallel a c) (parallel b c)" apply (simp add: triv_refinement_def parallel_def split_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. triv_refinement a b \<Longrightarrow> triv_refinement (parallel a c) (parallel b c) proof (prove)
goal (1 subgoal):
 1. \<forall>s. b s \<subseteq> a s \<Longrightarrow> \<forall>s. {p. \<exists>f_steps. length f_steps = length (fst p) \<and> (map (\<lambda>p. (if fst p then fst (snd p) else Env, snd (snd p))) (zip f_steps (fst p)), snd p) \<in> b s \<and> (map (\<lambda>p. (if fst p then Env else fst (snd p), snd (snd p))) (zip f_steps (fst p)), snd p) \<in> c s} \<subseteq> {p. \<exists>f_steps. length f_steps = length (fst p) \<and> (map (\<lambda>p. (if fst p then fst (snd p) else Env, snd (snd p))) (zip f_steps (fst p)), snd p) \<in> a s \<and> (map (\<lambda>p. (if fst p then Env else fst (snd p), snd (snd p))) (zip f_steps (fst p)), snd p) \<in> c s} proof (prove)
goal:
No subgoals!