Some more rules for Lib

lib/Corres_UL.thy

@@ -793,6 +793,9 @@ lemma corres_stateAssert_implied:
    apply (wp | rule no_fail_pre)+
   done
 
+lemmas corres_stateAssert_ignore =
+  corres_stateAssert_implied[where P=P and P'=P for P, simplified, rotated]
+
 lemma corres_stateAssert_r:
   "corres_underlying sr nf nf' r P Q f (g ()) \<Longrightarrow>
    corres_underlying sr nf nf' r P (Q and P') f (stateAssert P' [] >>= g)"

lib/HaskellLib_H.thy

@@ -15,6 +15,7 @@ imports
   More_Numeral_Type
   Monads.Nondet_VCG
   Monads.Reader_Option_Monad
+  Monads.Reader_Option_VCG
 begin
 
 abbreviation (input) "flip \<equiv> swp"
@@ -528,6 +529,26 @@ definition ohaskell_fail :: "unit list \<Rightarrow> ('s, 'a) lookup" where
 definition ohaskell_assert :: "bool \<Rightarrow> unit list \<Rightarrow> ('s, unit) lookup" where
   "ohaskell_assert P ls \<equiv> if P then oreturn () else ofail"
 
+lemma no_ofail_ohaskell_assert[wp]:
+  "no_ofail (\<lambda>_. P) (ohaskell_assert P [])"
+  by (clarsimp simp: no_ofail_def ohaskell_assert_def)
+
+lemma ohaskell_assert_wp[wp]:
+  "\<lblot>\<lambda>s. Q \<longrightarrow> P () s\<rblot> ohaskell_assert Q [] \<lblot>P\<rblot>"
+  apply (clarsimp simp: ohaskell_assert_def)
+  apply (intro conjI; wpsimp)
+  done
+
+lemma ohaskell_assert_sp:
+  "\<lblot>P\<rblot> ohaskell_assert Q [] \<lblot>\<lambda>_ s. P s \<and> Q\<rblot>"
+  apply (clarsimp simp: ohaskell_assert_def)
+  apply (intro conjI; wpsimp)
+  done
+
+lemma gets_the_ohaskell_assert:
+  "gets_the (ohaskell_assert P []) = assert P"
+  by (clarsimp simp: ohaskell_assert_def split: if_splits)
+
 lemmas omonad_defs = omonad_defs ohaskell_assert_def ohaskell_fail_def
 
 end

lib/Heap_List.thy

@@ -83,14 +83,25 @@ lemma heap_path_end_unique:
   "heap_path hp x xs y \<Longrightarrow> heap_path hp x xs y' \<Longrightarrow> y = y'"
   by (induct xs arbitrary: x; clarsimp)
 
-lemma heap_path_head:
-  "heap_path hp x xs y \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> x = Some (hd xs)"
-  by (induct xs arbitrary: x; clarsimp)
+lemma heap_path_head':
+  "heap_path hp st xs y \<Longrightarrow> xs \<noteq> [] \<longrightarrow> st = Some (hd xs)"
+  by (induct xs arbitrary: st; clarsimp)
+
+lemmas heap_path_head = heap_path_head'[rule_format]
 
 lemma heap_path_non_nil_lookup_next:
   "heap_path hp x (xs@z#ys) y \<Longrightarrow> hp z = (case ys of [] \<Rightarrow> y | _ \<Rightarrow> Some (hd ys))"
   by (cases ys; fastforce)
 
+lemma heap_ls_next_of_hd:
+  "\<lbrakk>a = hd ls; heap_ls hp st ls; Suc 0 < length ls\<rbrakk> \<Longrightarrow> hp a = Some (hd (tl ls))"
+  apply (cut_tac hp=hp and xs="[]" and z=a and ys="tl ls" in heap_path_non_nil_lookup_next)
+   apply (prop_tac "ls \<noteq> []", fastforce)
+   apply fastforce
+  apply (cases "tl ls"; clarsimp)
+  apply (cases ls; clarsimp)
+  done
+
 lemma heap_path_prefix:
   "heap_path hp st ls ed \<Longrightarrow> \<forall>xs\<le>ls. heap_path hp st xs (if xs = [] then st else hp (last xs))"
   apply clarsimp
@@ -235,6 +246,28 @@ lemma heap_path_sym_heap_non_nil_lookup_prev:
   apply (fastforce dest: sym_heapD1)
   done
 
+lemma heap_ls_prev_of_last:
+  "\<lbrakk>t = last ls; Suc 0 < length ls; heap_ls hp st ls; sym_heap hp hp'\<rbrakk>
+   \<Longrightarrow> hp' t = Some (last (butlast ls))"
+  apply (cut_tac hp=hp and xs="butlast ls" and z=t and ys="[]"
+              in heap_path_sym_heap_non_nil_lookup_prev)
+     apply (prop_tac "ls \<noteq> []", fastforce)
+     apply fastforce
+    apply fastforce
+   apply (fastforce intro!: length_gt_1_imp_butlast_nonempty)
+  apply assumption
+  done
+
+lemma ptr_in_middle_prev_next:
+  "\<lbrakk>heap_ls hp st (xs @ ptr # ys); xs \<noteq> []; ys \<noteq> []; sym_heap hp hp'\<rbrakk>
+   \<Longrightarrow> hp' ptr = Some (last xs) \<and> hp ptr = Some (hd ys)"
+  apply (rule conjI)
+   apply (fastforce dest: heap_path_sym_heap_non_nil_lookup_prev)
+  apply (cut_tac hp=hp in heap_path_non_nil_lookup_next)
+   apply fastforce
+  apply (cases ys; clarsimp)
+  done
+
 lemma heap_ls_no_loops:
   "\<lbrakk>heap_ls hp st xs; p \<in> set xs\<rbrakk> \<Longrightarrow> hp p \<noteq> Some p"
   apply (frule heap_ls_distinct)

lib/Lib.thy

@@ -1913,6 +1913,37 @@ lemma length_takeWhile_gt:
   apply simp
   done
 
+lemma map_fst_filter_zip[simp]:
+ "map fst (filter (\<lambda>(_, x). P x) (zip ls (map f ls))) = filter (\<lambda>x. P (f x)) ls"
+  by (induction ls; clarsimp)
+
+lemma map_fst_dropWhile_zip[simp]:
+ "map fst (dropWhile (\<lambda>(_, x). P x) (zip ls (map f ls))) = dropWhile (\<lambda>x. P (f x)) ls"
+  by (induction ls; clarsimp)
+
+lemma map_fst_takeWhile_zip[simp]:
+ "map fst (takeWhile (\<lambda>(_, x). P x) (zip ls (map f ls))) = takeWhile (\<lambda>x. P (f x)) ls"
+  by (induction ls; clarsimp)
+
+lemma suffix_tl:
+  "suffix xs ys \<Longrightarrow> suffix (tl xs) ys"
+  apply (clarsimp simp: suffix_def)
+  apply (metis append.assoc append_Cons append_Nil list.exhaust_sel list.sel(2))
+  done
+
+lemma nonempty_proper_suffix_split:
+  "\<lbrakk>sfx \<noteq> []; sfx \<noteq> queue; suffix sfx queue\<rbrakk> \<Longrightarrow> (\<exists>xs ys. xs \<noteq> [] \<and> queue = xs @ hd sfx # ys)"
+  apply (clarsimp simp: suffix_def)
+  apply (fastforce simp: neq_Nil_conv)
+  done
+
+lemma nonempty_proper_suffix_split_distinct:
+  "\<lbrakk>sfx \<noteq> []; sfx \<noteq> queue; suffix sfx queue; distinct queue\<rbrakk>
+   \<Longrightarrow> \<exists>xs ys. xs \<noteq> [] \<and> queue = xs @ hd sfx # ys \<and> hd queue \<noteq> hd sfx"
+  apply (frule (2) nonempty_proper_suffix_split)
+  apply (cases sfx; fastforce)
+  done
+
 lemma hd_drop_conv_nth2:
   "n < length xs \<Longrightarrow> hd (drop n xs) = xs ! n"
   by (rule hd_drop_conv_nth) clarsimp
@@ -2032,6 +2063,22 @@ lemma filter_eq_If:
   "distinct xs \<Longrightarrow> filter (\<lambda>v. v = x) xs = (if x \<in> set xs then [x] else [])"
   by (induct xs) auto
 
+lemma filter_last_equals_butlast:
+  "\<lbrakk>distinct q; q \<noteq> []\<rbrakk> \<Longrightarrow> filter ((\<noteq>) (last q)) q = butlast q"
+  apply (induct q rule: length_induct)
+  apply (rename_tac list)
+  apply (case_tac list; simp)
+  apply (fastforce simp: filter_id_conv)
+  done
+
+lemma filter_middle_distinct:
+  "\<lbrakk>distinct q; q = ys @ t # zs\<rbrakk> \<Longrightarrow> filter ((\<noteq>) t) q = ys @ zs"
+  apply (induct q rule: length_induct)
+  apply (rename_tac list)
+  apply (case_tac list; simp)
+  apply (subst filter_True | fastforce)+
+  done
+
 lemma (in semigroup_add) foldl_assoc:
 shows "foldl (+) (x+y) zs = x + (foldl (+) y zs)"
   by (induct zs arbitrary: y) (simp_all add:add.assoc)
@@ -2562,6 +2609,18 @@ lemma fun_upd_swap:
   "a \<noteq> c \<Longrightarrow>  hp(c := d, a := b) = hp(a := b, c := d)"
   by fastforce
 
+lemma list_not_head:
+  "Suc 0 < length ls \<Longrightarrow> ls \<noteq> [hd ls]"
+  by (cases ls; clarsimp)
+
+lemma list_not_last:
+  "Suc 0 < length ls \<Longrightarrow> ls \<noteq> [last ls]"
+  by (cases ls; clarsimp)
+
+lemma length_tail_nonempty:
+  "Suc 0 < length list \<Longrightarrow> tl list \<noteq> []"
+  by (cases list, simp, simp)
+
 text \<open>Prevent clarsimp and others from creating Some from not None by folding this and unfolding
   again when safe.\<close>
 

lib/ListLibLemmas.thy

@@ -397,6 +397,20 @@ lemma set_list_insert_before:
   apply fastforce
   done
 
+lemma takeWhile_dropWhile_insert_list_before:
+  "\<lbrakk>distinct ls; sorted (map f ls); sfx \<noteq> []; suffix sfx ls;
+    \<forall>pfx v. pfx @ sfx = ls \<and> v \<in> set pfx \<longrightarrow> f v \<le> f new; f new < f (hd sfx)\<rbrakk> \<Longrightarrow>
+   map fst (takeWhile (\<lambda>(_, t). t \<le> f new) (zip ls (map f ls)))
+    @ new
+    # map fst (dropWhile (\<lambda>(_, t). t \<le> f new) (zip ls (map f ls)))
+   = list_insert_before ls (hd sfx) new"
+  apply (cases sfx; simp)
+  apply (simp add: suffix_def map_fst_takeWhile_zip map_fst_dropWhile_zip)
+  apply (elim exE, rename_tac xs)
+  apply (cut_tac xs=xs and ys="a # list" and new=new in list_insert_before_distinct)
+    apply auto
+  done
+
 lemma list_remove_removed:
   "set (list_remove list x) = (set list) - {x}"
   apply (induct list,simp+)
@@ -423,6 +437,16 @@ lemma list_remove_none: "x \<notin> set list \<Longrightarrow> list_remove list
   apply clarsimp+
   done
 
+lemma list_remove_append[simp]:
+  "list_remove (xs @ ys) t = list_remove xs t @ list_remove ys t"
+  by (induct xs) auto
+
+lemma list_remove_middle_distinct:
+  "\<lbrakk>distinct q; q = ys @ t # zs\<rbrakk> \<Longrightarrow> list_remove q t = ys @ zs"
+  apply (induct q rule: length_induct)
+  apply (simp add: list_remove_none)
+  done
+
 lemma replace_distinct: "x \<notin> set list \<Longrightarrow> distinct list \<Longrightarrow> distinct (list_replace list y x)"
   apply (induct list)
   apply (simp add: list_replace_def)+
@@ -1117,4 +1141,28 @@ lemma map2_append1:
   "map2 f (as @ bs) cs = map2 f as (take (length as) cs) @ map2 f bs (drop (length as) cs)"
   by (simp add: map_def zip_append1)
 
+lemma sorted_lastD:
+  "\<lbrakk> sorted xs; xs \<noteq> [] \<rbrakk> \<Longrightarrow> \<forall>x\<in>set xs. x \<le> last xs"
+  by (induct xs, auto)
+
+lemma sorted_last_leD:
+  "\<lbrakk> sorted xs; y \<ge> last xs ; xs \<noteq> [] \<rbrakk> \<Longrightarrow> \<forall>x\<in>set xs. x \<le> y"
+  by (fastforce dest: sorted_lastD)
+
+lemma length_gt_1_imp_butlast_nonempty:
+  "Suc 0 < length xs \<Longrightarrow> butlast xs \<noteq> []"
+  by (cases xs; clarsimp)
+
+lemma not_last_in_set_butlast:
+  "\<lbrakk>ptr \<in> set ls; ptr \<noteq> last ls\<rbrakk> \<Longrightarrow> ptr \<in> set (butlast ls)"
+  apply (induct ls; simp)
+  apply fastforce
+  done
+
+lemma distinct_in_butlast_not_last:
+  "\<lbrakk>distinct ls; x \<in> set (butlast ls)\<rbrakk> \<Longrightarrow> x \<noteq> last ls"
+  apply (induct ls; simp)
+  apply force
+  done
+
 end

lib/MonadicRewrite.thy

@@ -760,6 +760,12 @@ lemma monadic_rewrite_corres_r:
 lemmas corres_gets_the_bind
   = monadic_rewrite_corres_l[OF monadic_rewrite_bind_head[OF monadic_rewrite_gets_the_gets]]
 
+text \<open>Interaction with @{term oblivious}\<close>
+
+lemma oblivious_monadic_rewrite:
+  "oblivious f m \<Longrightarrow> monadic_rewrite F E \<top> (do modify f; m od) (do m; modify f od)"
+  by (clarsimp simp: monadic_rewrite_def oblivious_modify_swap)
+
 text \<open>Tool integration\<close>
 
 lemma wpc_helper_monadic_rewrite:

lib/Monads/reader_option/Reader_Option_ND.thy

@@ -106,6 +106,10 @@ lemma gets_the_assert:
   "gets_the (oassert P) = assert P"
   by (simp add: oassert_def assert_def gets_the_fail gets_the_return)
 
+lemma gets_the_assert_opt:
+  "gets_the (oassert_opt P) = assert_opt P"
+  by (simp add: oassert_opt_def assert_opt_def gets_the_return gets_the_fail split: option.splits)
+
 lemma gets_the_if_distrib:
   "gets_the (if P then f else g) = (if P then gets_the f else gets_the g)"
   by simp

lib/Monads/reader_option/Reader_Option_VCG.thy

@@ -97,6 +97,12 @@ lemma asks_SomeD:
   "\<lbrakk>asks f s = Some r; Q (f s) s\<rbrakk> \<Longrightarrow> Q r s"
   by (rule use_ovalid[OF asks_wp])
 
+lemma oassert_wp[wp]:
+  "\<lblot>\<lambda>s. Q \<longrightarrow> P () s\<rblot> oassert Q \<lblot>P\<rblot>"
+  apply (simp add: oassert_def)
+  apply (intro conjI; wpsimp)
+  done
+
 lemma ogets_wp[wp]:
   "ovalid (\<lambda>s. P (f s) s) (ogets f) P"
   by wp
@@ -109,6 +115,10 @@ lemma oskip_wp[wp]:
   "ovalid (\<lambda>s. P () s) oskip P"
   by (simp add: ovalid_def oskip_def)
 
+lemma ovalid_if_split:
+  "\<lbrakk> P \<Longrightarrow> \<lblot>Q\<rblot> f \<lblot>S\<rblot>; \<not>P \<Longrightarrow> \<lblot>R\<rblot> g \<lblot>S\<rblot> \<rbrakk> \<Longrightarrow> \<lblot>\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not>P \<longrightarrow> R s)\<rblot> if P then f else g \<lblot>S\<rblot>"
+  by simp
+
 lemma ovalid_case_prod[wp]:
   assumes "(\<And>x y. ovalid (P x y) (B x y) Q)"
   shows "ovalid (case v of (x, y) \<Rightarrow> P x y) (case v of (x, y) \<Rightarrow> B x y) Q"
@@ -124,6 +134,11 @@ lemma owhile_ovalid[wp]:
    apply auto
   done
 
+lemma assert_opt_ovalid:
+  "\<lblot>\<lambda>s. \<forall>y. x = Some y \<longrightarrow> Q y s\<rblot> oassert_opt x \<lblot>Q\<rblot>"
+  unfolding oassert_opt_def
+  by (case_tac x; wpsimp)
+
 definition ovalid_property where "ovalid_property P x = (\<lambda>s f. (\<forall>r. Some r = x s f \<longrightarrow> P r s))"
 
 lemma ovalid_is_triple[wp_trip]:
@@ -359,7 +374,7 @@ lemma ovalidNF_pre_imp:
   "\<lbrakk> \<And>s. P' s \<Longrightarrow> P s; ovalidNF P f Q \<rbrakk> \<Longrightarrow> ovalidNF P' f Q"
   by (simp add: ovalidNF_def)
 
-lemma no_ofail_pre_imp:
+lemma no_ofail_pre_imp[wp_pre]:
   "\<lbrakk> no_ofail P f; \<And>s. P' s \<Longrightarrow> P s \<rbrakk> \<Longrightarrow> no_ofail P' f"
   by (simp add: no_ofail_def)
 

lib/clib/Corres_UL_C.thy

@@ -309,6 +309,14 @@ lemma ccorres_to_vcg:
   apply fastforce
   done
 
+lemma ccorres_to_vcg_Normal:
+  "\<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] a c; no_fail Q a\<rbrakk>
+   \<Longrightarrow> \<Gamma> \<turnstile> {s'. P s \<and> Q s \<and> s' \<in> P' \<and> (s, s') \<in> srel} c UNIV"
+  apply (frule (1) ccorres_to_vcg_with_prop[where R="\<top>\<top>" and s=s])
+   apply wpsimp
+  apply (fastforce elim: conseqPost)
+  done
+
 lemma ccorres_to_vcg_gets_the:
   "\<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] (gets_the r) c; no_ofail P r\<rbrakk>
    \<Longrightarrow> \<Gamma> \<turnstile> (P' \<inter> {s'. (s, s') \<in> srel \<and> P s})