kings-crown/FVELER_Isabelle huggingface dataset:
theory Nondet_While_Loop_Rules

lemma snd_whileLoopE_unfold:
  "\<lbrakk> \<not> snd (whileLoopE C B r s); (Inr r', s') \<in> fst (B r s); C r s \<rbrakk> \<Longrightarrow> \<not> snd (whileLoopE C B r' s')" unfolding whileLoopE_def by (fastforce simp: lift_def dest: snd_whileLoop_unfold)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> snd (whileLoopE C
  B r s); (Inr r', s') \<in> fst (B r s); C r s\<rbrakk> \<Longrightarrow> \<not> snd (whileLoopE C
  B r' s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift B) (Inr r) s); (Inr r', s') \<in> fst (B r s); C r s\<rbrakk> \<Longrightarrow> \<not> snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift B) (Inr r') s')
theory Nondet_While_Loop_Rules

lemma whileLoop_cong[cong]:
  "\<lbrakk> \<And>r s. C r s = C' r s; \<And>r s. C r s \<Longrightarrow> B r s = B' r s \<rbrakk> \<Longrightarrow> whileLoop C B = whileLoop C' B'" by (clarsimp simp: whileLoop_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r s. C r s = C' r s; \<And>r s. C r s \<Longrightarrow> B r s = B' r s\<rbrakk> \<Longrightarrow> whileLoop C
  B = whileLoop C'
  B'
theory Nondet_While_Loop_Rules

lemma whileLoopE_cong[cong]:
  "\<lbrakk> \<And>r s. C r s = C' r s ; \<And>r s. C r s \<Longrightarrow> B r s = B' r s \<rbrakk> \<Longrightarrow> whileLoopE C B = whileLoopE C' B'" unfolding whileLoopE_def by (rule whileLoop_cong[THEN arg_cong]; clarsimp simp: lift_def throwError_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r s. C r s = C' r s; \<And>r s. C r s \<Longrightarrow> B r s = B' r s\<rbrakk> \<Longrightarrow> whileLoopE C
  B = whileLoopE C'
  B' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r s. C r s = C' r s; \<And>r s. C r s \<Longrightarrow> B r s = B' r s\<rbrakk> \<Longrightarrow> (\<lambda>r. whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift B) (Inr r)) = (\<lambda>r. whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C' v s)
  (lift B') (Inr r))
theory Nondet_While_Loop_Rules

lemma whileLoop_terminates_wf:
  "wf {(x, y). C (fst y) (snd y) \<and> x \<in> fst (B (fst y) (snd y)) \<and> whileLoop_terminates C B (fst y) (snd y)}" apply (rule wfI[where A="UNIV" and B="{(r, s). whileLoop_terminates C B r s}"]; clarsimp) apply (erule whileLoop_terminates.induct; blast) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wf {(x, y). C (fst y) (snd y) \<and> x \<in> fst (B (fst y) (snd y)) \<and> whileLoop_terminates C B (fst y) (snd y)} proof (prove)
goal (1 subgoal):
 1. \<And>a b P. \<lbrakk>\<forall>a b. (\<forall>aa ba. C a b \<and> (aa, ba) \<in> fst (B a b) \<and> whileLoop_terminates C B a b \<longrightarrow> P (aa, ba)) \<longrightarrow> P (a, b); whileLoop_terminates C B a b\<rbrakk> \<Longrightarrow> P (a, b) proof (prove)
goal:
No subgoals!
theory Nondet_While_Loop_Rules

lemma whileLoop_results_induct_lemma1:
  "\<lbrakk> (a, b) \<in> whileLoop_results C B; b = Some (x, y) \<rbrakk> \<Longrightarrow> \<not> C x y" by (induct rule: whileLoop_results.induct) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a, b) \<in> whileLoop_results C B; b = Some (x, y)\<rbrakk> \<Longrightarrow> \<not> C x y
theory Nondet_While_Loop_Rules

lemma whileLoop_results_induct_lemma1':
  "\<lbrakk> (a, b) \<in> whileLoop_results C B; a \<noteq> b \<rbrakk> \<Longrightarrow> \<exists>x. a = Some x \<and> C (fst x) (snd x)" by (induct rule: whileLoop_results.induct) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a, b) \<in> whileLoop_results C B; a \<noteq> b\<rbrakk> \<Longrightarrow> \<exists>x. a = Some x \<and> C (fst x) (snd x)
theory Nondet_While_Loop_Rules

lemma whileLoop_results_induct_lemma3 [consumes 1]:
  assumes result: "(Some (r, s), Some (r', s')) \<in> whileLoop_results C B"
  and inv_start: "I r s"
  and inv_step: "\<And>r s r' s'. \<lbrakk> I r s; C r s; (r', s') \<in> fst (B r s) \<rbrakk> \<Longrightarrow> I r' s'"
  shows "I r' s'" apply (rule whileLoop_results_induct_lemma2 [where P="case_prod I" and y="(r', s')" and x="(r, s)",
                                               simplified case_prod_unfold, simplified]) apply (rule result) apply simp apply simp apply fact apply (erule (1) inv_step) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. I r' s' proof (prove)
goal (5 subgoals):
 1. (?a, ?b) \<in> whileLoop_results ?C ?B
 2. ?a = Some (r, s)
 3. ?b = Some (r', s')
 4. I r s
 5. \<And>s t. \<lbrakk>I (fst s) (snd s); t \<in> fst (?B (fst s) (snd s)); ?C (fst s) (snd s)\<rbrakk> \<Longrightarrow> I (fst t) (snd t) proof (prove)
goal (4 subgoals):
 1. Some (r, s) = Some (r, s)
 2. Some (r', s') = Some (r', s')
 3. I r s
 4. \<And>s t. \<lbrakk>I (fst s) (snd s); t \<in> fst (B (fst s) (snd s)); C (fst s) (snd s)\<rbrakk> \<Longrightarrow> I (fst t) (snd t) proof (prove)
goal (3 subgoals):
 1. Some (r', s') = Some (r', s')
 2. I r s
 3. \<And>s t. \<lbrakk>I (fst s) (snd s); t \<in> fst (B (fst s) (snd s)); C (fst s) (snd s)\<rbrakk> \<Longrightarrow> I (fst t) (snd t) proof (prove)
goal (2 subgoals):
 1. I r s
 2. \<And>s t. \<lbrakk>I (fst s) (snd s); t \<in> fst (B (fst s) (snd s)); C (fst s) (snd s)\<rbrakk> \<Longrightarrow> I (fst t) (snd t) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>I (fst s) (snd s); t \<in> fst (B (fst s) (snd s)); C (fst s) (snd s)\<rbrakk> \<Longrightarrow> I (fst t) (snd t) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>t \<in> fst (B (fst s) (snd s)); C (fst s) (snd s)\<rbrakk> \<Longrightarrow> (fst t, snd t) \<in> fst (B (fst s) (snd s)) proof (prove)
goal:
No subgoals!
theory Nondet_While_Loop_Rules

lemma fst_whileLoop_cond_false:
  assumes loop_result: "(r', s') \<in> fst (whileLoop C B r s)"
  shows "\<not> C r' s'" using loop_result by (rule in_whileLoop_induct, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> C r' s' proof (prove)
using this:
(r', s') \<in> fst (whileLoop C
  B r s)

goal (1 subgoal):
 1. \<not> C r' s'
theory Nondet_While_Loop_Rules

lemma snd_whileLoop:
  assumes init_I: "I r s"
    and cond_I: "C r s"
    and non_term: "\<And>r. \<lbrace> \<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s) \<rbrace> B r \<exists>\<lbrace> \<lambda>r' s'. C r' s' \<and> I r' s' \<rbrace>"
  shows "snd (whileLoop C B r s)" apply (clarsimp simp: whileLoop_def) apply (erule (1) whileLoop_terminates_results[OF non_term _ _ init_I cond_I]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. snd (whileLoop C
  B r s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(Some (r, s), None) \<notin> whileLoop_results C B; whileLoop_terminates C B r s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Nondet_While_Loop_Rules

lemma whileLoop_wp:
  "\<lbrakk> \<And>r. \<lbrace> \<lambda>s. I r s \<and> C r s \<rbrace> B r \<lbrace> I \<rbrace>;
     \<And>r s. \<lbrakk> I r s; \<not> C r s \<rbrakk> \<Longrightarrow> Q r s \<rbrakk> \<Longrightarrow>
  \<lbrace> I r \<rbrace> whileLoop C B r \<lbrace> Q \<rbrace>" by (rule valid_whileLoop)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>I\<rbrace>; \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s\<rbrakk> \<Longrightarrow> \<lbrace>I r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>
theory Nondet_While_Loop_Rules

lemma whileLoop_valid_inv:
  "(\<And>r. \<lbrace> \<lambda>s. I r s \<and> C r s \<rbrace> B r \<lbrace> I \<rbrace>) \<Longrightarrow> \<lbrace> I r \<rbrace> whileLoop C B r \<lbrace> I \<rbrace>" apply (fastforce intro: whileLoop_wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>I\<rbrace>) \<Longrightarrow> \<lbrace>I r\<rbrace> whileLoop C
  B r \<lbrace>I\<rbrace> proof (prove)
goal:
No subgoals!
theory Nondet_While_Loop_Rules

lemma valid_whileLoop_cond_fail:
  assumes pre_implies_post: "\<And>s. P r s \<Longrightarrow> Q r s"
      and pre_implies_fail: "\<And>s. P r s \<Longrightarrow> \<not> C r s"
    shows "\<lbrace> P r \<rbrace> whileLoop C B r \<lbrace> Q \<rbrace>" using assms apply (clarsimp simp: valid_def) apply (subst (asm) whileLoop_cond_fail) apply blast apply (clarsimp simp: return_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> proof (prove)
using this:
P r ?s \<Longrightarrow> Q r ?s
P r ?s \<Longrightarrow> \<not> C r ?s

goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<And>s. P r s \<Longrightarrow> Q r s; \<And>s. P r s \<Longrightarrow> \<not> C r s; P r s; (a, b) \<in> fst (whileLoop C
  B r s)\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>\<And>s. P r s \<Longrightarrow> Q r s; \<And>s. P r s \<Longrightarrow> \<not> C r s; P r s\<rbrakk> \<Longrightarrow> \<not> C r s
 2. \<And>s a b. \<lbrakk>\<And>s. P r s \<Longrightarrow> Q r s; \<And>s. P r s \<Longrightarrow> \<not> C r s; P r s; (a, b) \<in> fst (return r s)\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<And>s. P r s \<Longrightarrow> Q r s; \<And>s. P r s \<Longrightarrow> \<not> C r s; P r s; (a, b) \<in> fst (return r s)\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal:
No subgoals!
theory Nondet_While_Loop_Rules

lemma whileLoop_wp_inv [wp]:
  "\<lbrakk> \<And>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>I\<rbrace>; \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s \<rbrakk>
   \<Longrightarrow> \<lbrace> I r \<rbrace> whileLoop_inv C B r I M \<lbrace> Q \<rbrace>" apply (clarsimp simp: whileLoop_inv_def) apply (rule valid_whileLoop [where P=I and I=I], auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>I\<rbrace>; \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s\<rbrakk> \<Longrightarrow> \<lbrace>I r\<rbrace> whileLoop_inv C B r I M \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>I\<rbrace>; \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s\<rbrakk> \<Longrightarrow> \<lbrace>I r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> proof (prove)
goal:
No subgoals!
theory Nondet_While_Loop_Rules

lemma whileLoopE_wp:
  "\<lbrakk> \<And>r. \<lbrace> \<lambda>s. I r s \<and> C r s \<rbrace> B r \<lbrace> I \<rbrace>, \<lbrace> A \<rbrace>;
     \<And>r s. \<lbrakk> I r s; \<not> C r s \<rbrakk> \<Longrightarrow> Q r s \<rbrakk> \<Longrightarrow>
  \<lbrace> I r \<rbrace> whileLoopE C B r \<lbrace> Q \<rbrace>, \<lbrace> A \<rbrace>" by (rule validE_whileLoopE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>I\<rbrace>, \<lbrace>A\<rbrace>; \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s\<rbrakk> \<Longrightarrow> \<lbrace>I r\<rbrace> whileLoopE C
  B r \<lbrace>Q\<rbrace>, \<lbrace>A\<rbrace>
theory Nondet_While_Loop_Rules

lemma empty_fail_whileLoopE[empty_fail_cond, intro!, wp]:
  assumes "\<And>r. empty_fail (B r)"
  shows "empty_fail (whileLoopE C B r)" by (clarsimp simp: whileLoopE_def assms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (whileLoopE C
  B r)
theory Nondet_While_Loop_Rules

lemma empty_fail_whileM[empty_fail_cond, intro!, wp]:
  "\<lbrakk> empty_fail C; empty_fail B \<rbrakk> \<Longrightarrow> empty_fail (whileM C B)" unfolding whileM_def by (wpsimp wp: empty_fail_whileLoop empty_fail_bind)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_fail C; empty_fail B\<rbrakk> \<Longrightarrow> empty_fail (whileM C B) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_fail C; empty_fail B\<rbrakk> \<Longrightarrow> empty_fail (do c <- C;
whileLoop (\<lambda>c s. c)
  (\<lambda>_. do B;
C
od) c;
return ()
od)
theory Nondet_While_Loop_Rules

lemma whileLoop_results_bisim:
  assumes base: "(a, b) \<in> whileLoop_results C B"
    and vars1: "Q = (case a of Some (r, s) \<Rightarrow> Some (rt r, st s) | _ \<Rightarrow> None)"
    and vars2: "R = (case b of Some (r, s) \<Rightarrow> Some (rt r, st s) | _ \<Rightarrow> None)"
    and inv_init: "case a of Some (r, s) \<Rightarrow> I r s | _ \<Rightarrow> True"
    and inv_step: "\<And>r s r' s'. \<lbrakk> I r s; C r s; (r', s') \<in> fst (B r s) \<rbrakk> \<Longrightarrow> I r' s'"
    and cond_match: "\<And>r s. I r s \<Longrightarrow> C r s = C' (rt r) (st s)"
    and fail_step: "\<And>r s. \<lbrakk>C r s; snd (B r s); I r s\<rbrakk>
                         \<Longrightarrow> (Some (rt r, st s), None) \<in> whileLoop_results C' B'"
    and refine: "\<And>r s r' s'. \<lbrakk> I r s; C r s; (r', s') \<in>  fst (B r s) \<rbrakk>
                            \<Longrightarrow> (rt r', st s') \<in> fst (B' (rt r) (st s))"
  shows "(Q, R) \<in> whileLoop_results C' B'" apply (subst vars1, subst vars2) apply (rule whileLoop_results_bisim_helper) apply (rule assms; assumption?)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Q, R) \<in> whileLoop_results C' B' proof (prove)
goal (1 subgoal):
 1. (case a of None \<Rightarrow> None | Some (r, s) \<Rightarrow> Some (rt r, st s), case b of None \<Rightarrow> None | Some (r, s) \<Rightarrow> Some (rt r, st s)) \<in> whileLoop_results C' B' proof (prove)
goal (6 subgoals):
 1. (a, b) \<in> whileLoop_results ?C ?B
 2. case a of None \<Rightarrow> True | Some (r, s) \<Rightarrow> ?I r s
 3. \<And>r s r' s'. \<lbrakk>?I r s; ?C r s; (r', s') \<in> fst (?B r s)\<rbrakk> \<Longrightarrow> ?I r' s'
 4. \<And>r s. ?I r s \<Longrightarrow> ?C r s = C' (rt r) (st s)
 5. \<And>r s. \<lbrakk>?C r s; snd (?B r s); ?I r s\<rbrakk> \<Longrightarrow> (Some (rt r, st s), None) \<in> whileLoop_results C' B'
 6. \<And>r s r' s'. \<lbrakk>?I r s; ?C r s; (r', s') \<in> fst (?B r s)\<rbrakk> \<Longrightarrow> (rt r', st s') \<in> fst (B' (rt r) (st s)) proof (prove)
goal:
No subgoals!
theory Nondet_While_Loop_Rules

lemma snd_X_return[simp]:
  "snd ((A >>= (\<lambda>a. return (X a))) s) = snd (A s)" by (clarsimp simp: return_def bind_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. snd ((do a <- A;
return (X a)
od) s) = snd (A s)
theory Nondet_While_Loop_Rules

lemma isr_Inr_projr:
  "\<not> isl a \<Longrightarrow> (a = Inr b) = (b = projr a)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> isl a \<Longrightarrow> (a = Inr b) = (b = projr a)
theory Nondet_While_Loop_Rules

lemma validNF_whileLoop:
  assumes pre: "\<And>s. P r s \<Longrightarrow> I r s"
  and inv: "\<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s \<rbrace> B r \<lbrace> \<lambda>r' s'. I r' s' \<and> ((r', s'), (r, s)) \<in> R \<rbrace>!"
  and wf: "wf R"
  and post_cond: "\<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s"
  shows "\<lbrace>P r\<rbrace> whileLoop C B r \<lbrace>Q\<rbrace>!" apply rule apply (rule valid_whileLoop) apply fact apply (insert inv, clarsimp simp: validNF_def valid_def split: prod.splits, force)[1] apply (metis post_cond) apply (unfold no_fail_def) apply (intro allI impI) apply (rule not_snd_whileLoop [where I=I and R=R]) apply (auto intro: assms) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>! proof (prove)
goal (2 subgoals):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>
 2. no_fail (P r) (whileLoop C
  B r) proof (prove)
goal (4 subgoals):
 1. \<And>s. P r s \<Longrightarrow> ?I3 r s
 2. \<And>r. \<lbrace>\<lambda>s. ?I3 r s \<and> C r s\<rbrace> B r \<lbrace>?I3\<rbrace>
 3. \<And>r s. \<lbrakk>?I3 r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s
 4. no_fail (P r) (whileLoop C
  B r) proof (prove)
goal (3 subgoals):
 1. \<And>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>I\<rbrace>
 2. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s
 3. no_fail (P r) (whileLoop C
  B r) proof (prove)
goal (2 subgoals):
 1. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s
 2. no_fail (P r) (whileLoop C
  B r) proof (prove)
goal (1 subgoal):
 1. no_fail (P r) (whileLoop C
  B r) proof (prove)
goal (1 subgoal):
 1. \<forall>s. P r s \<longrightarrow> \<not> snd (whileLoop C
  B r s) proof (prove)
goal (1 subgoal):
 1. \<And>s. P r s \<Longrightarrow> \<not> snd (whileLoop C
  B r s) proof (prove)
goal (3 subgoals):
 1. \<And>s. P r s \<Longrightarrow> I r s
 2. \<And>s ra sa. P r s \<Longrightarrow> \<lbrace>\<lambda>s'. I ra s' \<and> C ra s' \<and> s' = sa\<rbrace> B ra \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), ra, sa) \<in> R\<rbrace>!
 3. \<And>s. P r s \<Longrightarrow> wf R proof (prove)
goal:
No subgoals!
theory Nondet_While_Loop_Rules

lemma validNF_whileLoop_inv [wp]:
  assumes inv: "\<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s \<rbrace> B r \<lbrace> \<lambda>r' s'. I r' s' \<and> ((r', s'), (r, s)) \<in> R \<rbrace>!"
  and wf: "wf R"
  and post_cond: "\<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s"
  shows "\<lbrace>I r\<rbrace> whileLoop_inv C B r I R \<lbrace>Q\<rbrace>!" apply (clarsimp simp: whileLoop_inv_def) apply (rule validNF_whileLoop [where I=I and R=R]) apply simp apply (rule inv) apply (rule wf) apply (metis post_cond) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>I r\<rbrace> whileLoop_inv C B r I R \<lbrace>Q\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>I r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>! proof (prove)
goal (4 subgoals):
 1. \<And>s. I r s \<Longrightarrow> I r s
 2. \<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!
 3. wf R
 4. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (3 subgoals):
 1. \<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!
 2. wf R
 3. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (2 subgoals):
 1. wf R
 2. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal:
No subgoals!
theory Nondet_While_Loop_Rules

lemma validNF_whileLoop_inv_measure [wp]:
  assumes inv: "\<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s \<rbrace> B r \<lbrace> \<lambda>r' s'. I r' s' \<and> M r' s' < M r s \<rbrace>!"
  and post_cond: "\<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s"
  shows "\<lbrace>I r\<rbrace> whileLoop_inv C B r I (measure' (\<lambda>(r, s). M r s)) \<lbrace>Q\<rbrace>!" apply (clarsimp simp: whileLoop_inv_def) apply (rule validNF_whileLoop[where R="measure' (\<lambda>(r, s). M r s)" and I=I]) apply simp apply clarsimp apply (rule inv) apply simp apply (metis post_cond) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>I r\<rbrace> whileLoop_inv C B r I (measure' (\<lambda>(r, s). M r s)) \<lbrace>Q\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>I r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>! proof (prove)
goal (4 subgoals):
 1. \<And>s. I r s \<Longrightarrow> I r s
 2. \<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> measure' (\<lambda>(r, s). M r s)\<rbrace>!
 3. wf (measure' (\<lambda>(r, s). M r s))
 4. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (3 subgoals):
 1. \<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> measure' (\<lambda>(r, s). M r s)\<rbrace>!
 2. wf (measure' (\<lambda>(r, s). M r s))
 3. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (3 subgoals):
 1. \<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> M r' s' < M r s\<rbrace>!
 2. wf (measure' (\<lambda>(r, s). M r s))
 3. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (2 subgoals):
 1. wf (measure' (\<lambda>(r, s). M r s))
 2. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal:
No subgoals!
theory Nondet_While_Loop_Rules

lemma validNF_whileLoop_inv_measure_twosteps:
  assumes inv: "\<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<rbrace> B r \<lbrace> \<lambda>r' s'. I r' s' \<rbrace>!"
  assumes measure: "\<And>r m. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> M r s = m \<rbrace> B r \<lbrace> \<lambda>r' s'. M r' s' < m \<rbrace>"
  and post_cond: "\<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s"
  shows "\<lbrace>I r\<rbrace> whileLoop_inv C B r I (measure' (\<lambda>(r, s). M r s)) \<lbrace>Q\<rbrace>!" apply (rule validNF_whileLoop_inv_measure) apply (rule validNF_weaken_pre) apply (rule validNF_post_comb_conj_L) apply (rule inv) apply (rule measure) apply fast apply (metis post_cond) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>I r\<rbrace> whileLoop_inv C B r I (measure' (\<lambda>(r, s). M r s)) \<lbrace>Q\<rbrace>! proof (prove)
goal (2 subgoals):
 1. \<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> M r' s' < M r s\<rbrace>!
 2. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (3 subgoals):
 1. \<And>r s. \<lbrace>?Q3 r s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> M r' s' < M r s\<rbrace>!
 2. \<And>r s sa. I r sa \<and> C r sa \<and> sa = s \<Longrightarrow> ?Q3 r s sa
 3. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (4 subgoals):
 1. \<And>r s. \<lbrace>?P'6 r s\<rbrace> B r \<lbrace>I\<rbrace>!
 2. \<And>r s. \<lbrace>?P6 r s\<rbrace> B r \<lbrace>\<lambda>rv sa. M rv sa < M r s\<rbrace>
 3. \<And>r s sa. I r sa \<and> C r sa \<and> sa = s \<Longrightarrow> ?P6 r s sa \<and> ?P'6 r s sa
 4. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (3 subgoals):
 1. \<And>r s. \<lbrace>?P6 r s\<rbrace> B r \<lbrace>\<lambda>rv sa. M rv sa < M r s\<rbrace>
 2. \<And>r s sa. I r sa \<and> C r sa \<and> sa = s \<Longrightarrow> ?P6 r s sa \<and> I r sa \<and> C r sa
 3. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (2 subgoals):
 1. \<And>r s sa. I r sa \<and> C r sa \<and> sa = s \<Longrightarrow> (I r sa \<and> C r sa \<and> M r sa = M r s) \<and> I r sa \<and> C r sa
 2. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal:
No subgoals!
theory Nondet_While_Loop_Rules

lemma wf_custom_measure:
  "\<lbrakk> \<And>a b. (a, b) \<in> R \<Longrightarrow> f a < (f :: 'a \<Rightarrow> nat) b \<rbrakk> \<Longrightarrow>  wf R" by (metis in_measure wf_def wf_measure)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>a b. (a, b) \<in> R \<Longrightarrow> f a < f b) \<Longrightarrow> wf R