kings-crown/FVELER_Isabelle huggingface dataset:
theory CutMon

lemma cutMon_walk_bindE:
  "cutMon ((=) s) (f >>=E g) =
   (cutMon ((=) s) f >>=E (\<lambda>rv. cutMon (\<lambda>s'. (Inr rv, s') \<in> fst (f s)) (g rv)))" apply (simp add: bindE_def cutMon_walk_bind) apply (rule bind_cong, rule refl) apply (simp add: cutMon_def lift_def fail_def split: if_split_asm) apply (clarsimp split: sum.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cutMon ((=) s) (f >>=E g) = doE rv <- cutMon ((=) s) f;
cutMon (\<lambda>s'. (Inr rv, s') \<in> fst (f s)) (g rv)
odE proof (prove)
goal (1 subgoal):
 1. do rv <- cutMon ((=) s) f;
cutMon (\<lambda>s'. (rv, s') \<in> fst (f s)) (lift g rv)
od = cutMon ((=) s) f >>= lift (\<lambda>rv. cutMon (\<lambda>s'. (Inr rv, s') \<in> fst (f s)) (g rv)) proof (prove)
goal (1 subgoal):
 1. \<And>v sa s'. (v, s') \<in> fst (cutMon ((=) s) f sa) \<Longrightarrow> cutMon (\<lambda>s'. (v, s') \<in> fst (f s)) (lift g v) s' = lift (\<lambda>rv. cutMon (\<lambda>s'. (Inr rv, s') \<in> fst (f s)) (g rv)) v s' proof (prove)
goal (1 subgoal):
 1. \<And>v sa s'. \<lbrakk>s = sa; (v, s') \<in> fst (f sa)\<rbrakk> \<Longrightarrow> (case v of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> g x) s' = (case v of Inl x \<Rightarrow> throwError x | Inr v' \<Rightarrow> \<lambda>sa. if (Inr v', sa) \<in> fst (f s) then g v' sa else fail sa) s' proof (prove)
goal:
No subgoals!
theory CutMon

lemma cutMon_walk_if:
  "cutMon ((=) s) (if P then f else g) = (if P then cutMon ((=) s) f else cutMon ((=) s) g)" by (simp add: cutMon_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cutMon ((=) s) (if P then f else g) = (if P then cutMon ((=) s) f else cutMon ((=) s) g)
theory CutMon

lemma cutMon_valid_drop:
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> cutMon R f \<lbrace>Q\<rbrace>" by (simp add: cutMon_def valid_def fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> cutMon R f \<lbrace>Q\<rbrace>
theory CutMon

lemma cutMon_validE_drop:
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> cutMon R f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by (simp add: validE_def cutMon_valid_drop)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> cutMon R f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory CutMon

lemma snd_cutMon:
  "snd (cutMon P f s) = (P s \<longrightarrow> snd (f s))" by (simp add: cutMon_def fail_def split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. snd (cutMon P f s) = (P s \<longrightarrow> snd (f s))
theory CutMon

lemma cutMon_assert_opt:
  "cutMon P (gets_the f >>= g) = gets_the (\<lambda>s. if P s then f s else None) >>= g" by (simp add: cutMon_def gets_the_def exec_gets
                bind_assoc fun_eq_iff assert_opt_def
         split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cutMon P (gets_the f >>= g) = gets_the (\<lambda>s. if P s then f s else None) >>= g
theory CutMon

lemma empty_fail_use_cutMon:
  "\<lbrakk> \<And>s. empty_fail (cutMon ((=) s) f) \<rbrakk> \<Longrightarrow> empty_fail f" by (fastforce simp add: empty_fail_def cutMon_def split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. empty_fail (cutMon ((=) s) f)) \<Longrightarrow> empty_fail f
theory CutMon

lemma empty_fail_drop_cutMon:
  "empty_fail f \<Longrightarrow> empty_fail (cutMon P f)" by (simp add: empty_fail_def fail_def cutMon_def split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail f \<Longrightarrow> empty_fail (cutMon P f)
theory CutMon

lemma empty_fail_cutMon:
  "\<lbrakk> \<And>s. P s \<Longrightarrow> empty_fail (cutMon ((=) s) f) \<rbrakk> \<Longrightarrow> empty_fail (cutMon P f)" by (fastforce simp: empty_fail_def cutMon_def fail_def split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. P s \<Longrightarrow> empty_fail (cutMon ((=) s) f)) \<Longrightarrow> empty_fail (cutMon P f)
theory Oblivious

lemma oblivious_return[simp]:
  "oblivious f (return x)" by (simp add: oblivious_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oblivious f (return x)
theory Oblivious

lemma oblivious_fail[simp]:
  "oblivious f fail" by (simp add: oblivious_def fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oblivious f fail
theory Oblivious

lemma oblivious_assert[simp]:
  "oblivious f (assert x)" by (simp add: assert_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oblivious f (assert x)
theory Oblivious

lemma oblivious_assert_opt[simp]:
  "oblivious f (assert_opt fn)" by (simp add: assert_opt_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oblivious f (assert_opt fn)
theory Oblivious

lemma oblivious_gets[simp]:
  "oblivious f (gets f') = (\<forall>s. f' (f s) = f' s)" by (fastforce simp add: oblivious_def simpler_gets_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oblivious f (gets f') = (\<forall>s. f' (f s) = f' s)
theory Oblivious

lemma oblivious_liftM:
  "oblivious f m \<Longrightarrow> oblivious f (liftM g m)" by (simp add: liftM_def oblivious_bind)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oblivious f m \<Longrightarrow> oblivious f (liftM g m)
theory Oblivious

lemma oblivious_modify[simp]:
  "oblivious f (modify f') = (\<forall>s. f' (f s) = f (f' s))" apply (simp add: oblivious_def simpler_modify_def) apply (rule ball_cong[where A=UNIV, OF refl, simplified]) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oblivious f (modify f') = (\<forall>s. f' (f s) = f (f' s)) proof (prove)
goal (1 subgoal):
 1. (\<forall>s. f (f' s) = f' (f s) \<and> f' (f s) = f (f' s)) = (\<forall>s. f' (f s) = f (f' s)) proof (prove)
goal (1 subgoal):
 1. \<And>x. (f (f' x) = f' (f x) \<and> f' (f x) = f (f' x)) = (f' (f x) = f (f' x)) proof (prove)
goal:
No subgoals!
theory Oblivious

lemma oblivious_returnOk[simp]:
  "oblivious f (returnOk e)" by (simp add: returnOk_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oblivious f (returnOk e)
theory Oblivious

lemma oblivious_assertE[simp]:
  "oblivious f (assertE P)" by (simp add: assertE_def split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oblivious f (assertE P)
theory Oblivious

lemma oblivious_throwError[simp]:
  "oblivious f (throwError e)" by (simp add: throwError_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oblivious f (throwError e)
theory Oblivious

lemma oblivious_bindE:
  "\<lbrakk> oblivious u f; \<And>v. oblivious u (g v) \<rbrakk> \<Longrightarrow> oblivious u (f >>=E (\<lambda>v. g v))" apply (simp add: bindE_def) apply (erule oblivious_bind) apply (simp add: lift_def split: sum.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>oblivious u f; \<And>v. oblivious u (g v)\<rbrakk> \<Longrightarrow> oblivious u (f >>=E g) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>oblivious u f; \<And>v. oblivious u (g v)\<rbrakk> \<Longrightarrow> oblivious u (f >>= lift g) proof (prove)
goal (1 subgoal):
 1. \<And>rv. (\<And>v. oblivious u (g v)) \<Longrightarrow> oblivious u (lift g rv) proof (prove)
goal:
No subgoals!
theory Oblivious

lemma oblivious_catch:
  "\<lbrakk> oblivious u f; \<And>v. oblivious u (g v) \<rbrakk> \<Longrightarrow> oblivious u (catch f g)" apply (simp add: catch_def) apply (erule oblivious_bind) apply (simp split: sum.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>oblivious u f; \<And>v. oblivious u (g v)\<rbrakk> \<Longrightarrow> oblivious u (f <catch> g) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>oblivious u f; \<And>v. oblivious u (g v)\<rbrakk> \<Longrightarrow> oblivious u (do x <- f;
case x of Inl e \<Rightarrow> g e | Inr b \<Rightarrow> return b
od) proof (prove)
goal (1 subgoal):
 1. \<And>rv. (\<And>v. oblivious u (g v)) \<Longrightarrow> oblivious u (case rv of Inl e \<Rightarrow> g e | Inr b \<Rightarrow> return b) proof (prove)
goal:
No subgoals!
theory Oblivious

lemma oblivious_when[simp]:
  "oblivious f (when P m) = (P \<longrightarrow> oblivious f m)" by (simp add: when_def split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oblivious f (when P m) = (P \<longrightarrow> oblivious f m)
theory Oblivious

lemma oblivious_whenE[simp]:
  "oblivious f (whenE P g) = (P \<longrightarrow> oblivious f g)" by (simp add: whenE_def split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oblivious f (whenE P g) = (P \<longrightarrow> oblivious f g)
theory Oblivious

lemma select_f_oblivious[simp]:
  "oblivious f (select_f v)" by (simp add: oblivious_def select_f_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oblivious f (select_f v)
theory Oblivious

lemma oblivious_select:
  "oblivious f (select S)" by (simp add: oblivious_def select_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oblivious f (select S)
theory Injection_Handler

lemma injection_wp:
  "\<lbrakk> t = injection_handler f; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>,\<lbrace>\<lambda>ft. E (f ft)\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> t m \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" unfolding injection_handler_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t = injection_handler f; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>ft. E (f ft)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> t m \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t = (\<lambda>m. m <handle2> (\<lambda>ft. throwError (f ft))); \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>ft. E (f ft)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> t m \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory Injection_Handler

lemma injection_wp_E:
  "\<lbrakk> t = injection_handler f; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>,- \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> t m \<lbrace>Q\<rbrace>,-" by (simp add: validE_R_def injection_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t = injection_handler f; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> t m \<lbrace>Q\<rbrace>, -
theory Injection_Handler

lemma injection_bindE:
  "\<lbrakk> t = injection_handler f; t2 = injection_handler f \<rbrakk>
    \<Longrightarrow> t (x >>=E y) = (t2 x) >>=E (\<lambda>rv. t (y rv))" apply (simp add: injection_handler_def bindE_def handleE'_def bind_assoc) apply (rule arg_cong [where f="bind x"]) apply (fastforce simp: lift_def throwError_def split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t = injection_handler f; t2 = injection_handler f\<rbrakk> \<Longrightarrow> t (x >>=E y) = doE rv <- t2 x;
t (y rv)
odE proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t = injection_handler f; t2 = injection_handler f\<rbrakk> \<Longrightarrow> do x <- x;
lift y x >>= case_sum (\<lambda>e. throwError (f e)) (\<lambda>v'. return (Inr v'))
od = do x <- x;
(case x of Inl e \<Rightarrow> throwError (f e) | Inr v' \<Rightarrow> return (Inr v')) >>= lift (\<lambda>rv. y rv >>= case_sum (\<lambda>e. throwError (f e)) (\<lambda>v'. return (Inr v')))
od proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t = injection_handler f; t2 = injection_handler f\<rbrakk> \<Longrightarrow> (\<lambda>x. lift y x >>= case_sum (\<lambda>e. throwError (f e)) (\<lambda>v'. return (Inr v'))) = (\<lambda>x. (case x of Inl e \<Rightarrow> throwError (f e) | Inr v' \<Rightarrow> return (Inr v')) >>= lift (\<lambda>rv. y rv >>= case_sum (\<lambda>e. throwError (f e)) (\<lambda>v'. return (Inr v')))) proof (prove)
goal:
No subgoals!
theory Injection_Handler

lemma injection_liftE:
  "t = injection_handler f \<Longrightarrow> t (liftE x) = liftE x" by (simp add: injection_handler_def handleE'_def liftE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t = injection_handler f \<Longrightarrow> t (liftE x) = liftE x
theory Injection_Handler

lemma id_injection:
  "id = injection_handler id" proof - have P: "case_sum throwError (\<lambda>v. return (Inr v)) = return" by (auto simp: throwError_def split: sum.splits) show ?thesis by (auto simp: injection_handler_def handleE'_def P) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. id = injection_handler id proof (state)
goal (1 subgoal):
 1. id = injection_handler id proof (prove)
goal (1 subgoal):
 1. case_sum throwError (\<lambda>v. return (Inr v)) = return proof (state)
this:
case_sum throwError (\<lambda>v. return (Inr v)) = return

goal (1 subgoal):
 1. id = injection_handler id proof (prove)
goal (1 subgoal):
 1. id = injection_handler id proof (state)
this:
id = injection_handler id

goal:
No subgoals!
theory Injection_Handler

lemma injection_handler_assertE:
  "injection_handler inject (assertE f) = assertE f" by (simp add: assertE_liftE injection_liftE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. injection_handler inject (assertE f) = assertE f
theory Nondet_While_Loop_Rules_Completeness

lemma valid_path_not_empty:
  "valid_path C B xs \<Longrightarrow> xs \<noteq> []" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_path C B xs \<Longrightarrow> xs \<noteq> []
theory Nondet_While_Loop_Rules_Completeness

lemma shortest_path_length_same [simp]:
  "\<lbrakk> \<not> C (fst a) (snd a); Q (fst a) (snd a) \<rbrakk> \<Longrightarrow> shortest_path_length C B a Q = 1" apply (clarsimp simp: shortest_path_length_def) apply (rule Least_equality) apply (rule exI [where x="[a]"]) apply clarsimp apply (rule Suc_leI) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> C (fst a) (snd a); Q (fst a) (snd a)\<rbrakk> \<Longrightarrow> shortest_path_length C B a Q = 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> C (fst a) (snd a); Q (fst a) (snd a)\<rbrakk> \<Longrightarrow> (LEAST n. \<exists>l. valid_path C B l \<and> hd l = a \<and> Q (fst (last l)) (snd (last l)) \<and> length l = n) = Suc 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> C (fst a) (snd a); Q (fst a) (snd a)\<rbrakk> \<Longrightarrow> \<exists>l. valid_path C B l \<and> hd l = a \<and> Q (fst (last l)) (snd (last l)) \<and> length l = Suc 0
 2. \<And>y. \<lbrakk>\<not> C (fst a) (snd a); Q (fst a) (snd a); \<exists>l. valid_path C B l \<and> hd l = a \<and> Q (fst (last l)) (snd (last l)) \<and> length l = y\<rbrakk> \<Longrightarrow> Suc 0 \<le> y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> C (fst a) (snd a); Q (fst a) (snd a)\<rbrakk> \<Longrightarrow> valid_path C B [a] \<and> hd [a] = a \<and> Q (fst (last [a])) (snd (last [a])) \<and> length [a] = Suc 0
 2. \<And>y. \<lbrakk>\<not> C (fst a) (snd a); Q (fst a) (snd a); \<exists>l. valid_path C B l \<and> hd l = a \<and> Q (fst (last l)) (snd (last l)) \<and> length l = y\<rbrakk> \<Longrightarrow> Suc 0 \<le> y proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>\<not> C (fst a) (snd a); Q (fst a) (snd a); \<exists>l. valid_path C B l \<and> hd l = a \<and> Q (fst (last l)) (snd (last l)) \<and> length l = y\<rbrakk> \<Longrightarrow> Suc 0 \<le> y proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>\<not> C (fst a) (snd a); Q (fst a) (snd a); \<exists>l. valid_path C B l \<and> hd l = a \<and> Q (fst (last l)) (snd (last l)) \<and> length l = y\<rbrakk> \<Longrightarrow> 0 < y proof (prove)
goal:
No subgoals!
theory Nondet_While_Loop_Rules_Completeness

lemma valid_path_simp:
  "valid_path C B l =
        (((\<exists>r s. l = [(r, s)] \<and> \<not> C r s) \<or>
              (\<exists>r s r' s' xs. l = (r, s)#(r', s')#xs \<and> C r s \<and> (r', s') \<in> fst (B r s) \<and> valid_path C B ((r', s')#xs))))" apply (cases l rule: remdups_adj.cases) apply clarsimp apply clarsimp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_path C B l = ((\<exists>r s. l = [(r, s)] \<and> \<not> C r s) \<or> (\<exists>r s r' s' xs. l = (r, s) # (r', s') # xs \<and> C r s \<and> (r', s') \<in> fst (B r s) \<and> valid_path C B ((r', s') # xs))) proof (prove)
goal (3 subgoals):
 1. l = [] \<Longrightarrow> valid_path C B l = ((\<exists>r s. l = [(r, s)] \<and> \<not> C r s) \<or> (\<exists>r s r' s' xs. l = (r, s) # (r', s') # xs \<and> C r s \<and> (r', s') \<in> fst (B r s) \<and> valid_path C B ((r', s') # xs)))
 2. \<And>x. l = [x] \<Longrightarrow> valid_path C B l = ((\<exists>r s. l = [(r, s)] \<and> \<not> C r s) \<or> (\<exists>r s r' s' xs. l = (r, s) # (r', s') # xs \<and> C r s \<and> (r', s') \<in> fst (B r s) \<and> valid_path C B ((r', s') # xs)))
 3. \<And>x y xs. l = x # y # xs \<Longrightarrow> valid_path C B l = ((\<exists>r s. l = [(r, s)] \<and> \<not> C r s) \<or> (\<exists>r s r' s' xs. l = (r, s) # (r', s') # xs \<and> C r s \<and> (r', s') \<in> fst (B r s) \<and> valid_path C B ((r', s') # xs))) proof (prove)
goal (2 subgoals):
 1. \<And>x. l = [x] \<Longrightarrow> valid_path C B l = ((\<exists>r s. l = [(r, s)] \<and> \<not> C r s) \<or> (\<exists>r s r' s' xs. l = (r, s) # (r', s') # xs \<and> C r s \<and> (r', s') \<in> fst (B r s) \<and> valid_path C B ((r', s') # xs)))
 2. \<And>x y xs. l = x # y # xs \<Longrightarrow> valid_path C B l = ((\<exists>r s. l = [(r, s)] \<and> \<not> C r s) \<or> (\<exists>r s r' s' xs. l = (r, s) # (r', s') # xs \<and> C r s \<and> (r', s') \<in> fst (B r s) \<and> valid_path C B ((r', s') # xs))) proof (prove)
goal (1 subgoal):
 1. \<And>x y xs. l = x # y # xs \<Longrightarrow> valid_path C B l = ((\<exists>r s. l = [(r, s)] \<and> \<not> C r s) \<or> (\<exists>r s r' s' xs. l = (r, s) # (r', s') # xs \<and> C r s \<and> (r', s') \<in> fst (B r s) \<and> valid_path C B ((r', s') # xs))) proof (prove)
goal:
No subgoals!
theory Nondet_While_Loop_Rules_Completeness

lemma shortest_path_exists:
  "\<lbrakk> \<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<exists>\<lbrace> Q \<rbrace> \<rbrakk> \<Longrightarrow>
       \<exists>l. valid_path C B l
              \<and> shortest_path_length C B (r, s) Q = length l
              \<and> hd l = (r, s)
              \<and> Q (fst (last l)) (snd (last l))" apply (frule path_exists) apply (clarsimp simp: simp: shortest_path_length_def) apply (rule LeastI2_ex) apply force apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace> \<Longrightarrow> \<exists>l. valid_path C B l \<and> shortest_path_length C B (r, s) Q = length l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace>; \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l))\<rbrakk> \<Longrightarrow> \<exists>l. valid_path C B l \<and> shortest_path_length C B (r, s) Q = length l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>\<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace>; valid_path C B l; hd l = (r, s); Q (fst (last l)) (snd (last l))\<rbrakk> \<Longrightarrow> \<exists>l. valid_path C B l \<and> (LEAST n. \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) \<and> length l = n) = length l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (prove)
goal (2 subgoals):
 1. \<And>l. \<lbrakk>\<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace>; valid_path C B l; hd l = (r, s); Q (fst (last l)) (snd (last l))\<rbrakk> \<Longrightarrow> \<exists>a l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) \<and> length l = a
 2. \<And>l x. \<lbrakk>\<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace>; valid_path C B l; hd l = (r, s); Q (fst (last l)) (snd (last l)); \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) \<and> length l = x\<rbrakk> \<Longrightarrow> \<exists>l. valid_path C B l \<and> x = length l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (prove)
goal (1 subgoal):
 1. \<And>l x. \<lbrakk>\<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace>; valid_path C B l; hd l = (r, s); Q (fst (last l)) (snd (last l)); \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) \<and> length l = x\<rbrakk> \<Longrightarrow> \<exists>l. valid_path C B l \<and> x = length l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (prove)
goal:
No subgoals!
theory Nondet_While_Loop_Rules_Completeness

lemma shortest_path_is_shortest:
  "\<lbrakk> valid_path C B l; Q (fst (last l)) (snd (last l)) \<rbrakk> \<Longrightarrow> shortest_path_length C B (hd l) Q \<le> length l" apply (clarsimp simp: simp: shortest_path_length_def) apply (rule Least_le) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_path C B l; Q (fst (last l)) (snd (last l))\<rbrakk> \<Longrightarrow> shortest_path_length C B (hd l) Q \<le> length l proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_path C B l; Q (fst (last l)) (snd (last l))\<rbrakk> \<Longrightarrow> (LEAST n. \<exists>la. valid_path C B la \<and> hd la = hd l \<and> Q (fst (last la)) (snd (last la)) \<and> length la = n) \<le> length l proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_path C B l; Q (fst (last l)) (snd (last l))\<rbrakk> \<Longrightarrow> \<exists>la. valid_path C B la \<and> hd la = hd l \<and> Q (fst (last la)) (snd (last la)) \<and> length la = length l proof (prove)
goal:
No subgoals!
theory NonDetMonadLemmaBucket

lemma distinct_tuple_helper:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. distinct (x # xs rv s)\<rbrace> \<Longrightarrow>
   \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. distinct (x # (map fst (zip (xs rv s) (ys rv s))))\<rbrace>" apply (erule hoare_strengthen_post) apply (erule distinct_prefix) apply (simp add: map_fst_zip_prefix) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. distinct (x # xs rv s)\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. distinct (x # map fst (zip (xs rv s) (ys rv s)))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. distinct (x # xs rv s) \<Longrightarrow> distinct (x # map fst (zip (xs rv s) (ys rv s))) proof (prove)
goal (1 subgoal):
 1. \<And>rv s. x # map fst (zip (xs rv s) (ys rv s)) \<le> x # xs rv s proof (prove)
goal:
No subgoals!
theory NonDetMonadLemmaBucket

lemma gets_the_validE_R_wp:
  "\<lbrace>\<lambda>s. f s \<noteq> None \<and> isRight (the (f s)) \<and> Q (theRight (the (f s))) s\<rbrace>
     gets_the f
   \<lbrace>Q\<rbrace>,-" apply (simp add: gets_the_def validE_R_def validE_def) apply (wp | wpc | simp add: assert_opt_def)+ apply (clarsimp split: split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. f s \<noteq> None \<and> isRight (the (f s)) \<and> Q (theRight (the (f s))) s\<rbrace> gets_the f \<lbrace>Q\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<exists>y. f s = Some y) \<and> isRight (the (f s)) \<and> Q (theRight (the (f s))) s\<rbrace> gets f >>= assert_opt \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> True | Inr r \<Rightarrow> Q r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>y. f s = Some y) \<and> isRight (the (f s)) \<and> Q (theRight (the (f s))) s \<Longrightarrow> case the (f s) of Inl e \<Rightarrow> True | Inr r \<Rightarrow> Q r s proof (prove)
goal:
No subgoals!
theory NonDetMonadLemmaBucket

lemma return_bindE:
  "isRight v \<Longrightarrow> return v >>=E f = f (theRight v)" by (cases v; clarsimp simp: return_returnOk)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isRight v \<Longrightarrow> return v >>=E f = f (theRight v)