Theory More_B_Assn

theory More_B_Assn
  imports Base_MEC
begin

  definition op_bound_val:: "('a⇒bool) ⇒ 'a ⇒ 'a" where "op_bound_val P x = x"
  
  definition mop_bound_val :: "('a⇒bool) ⇒ 'a ⇒ 'a nres" where "mop_bound_val P x = do{ ASSERT (P x); RETURN x }"

  lemmas [simp] = op_bound_val_def mop_bound_val_def
  
  context 
    fixes P :: "'a ⇒ bool"
  begin
    sepref_register "op_bound_val P" 
    sepref_register "mop_bound_val P" 
  end
  
  lemma op_bound_val_refine[sepref_fr_rules]: "(Mreturn,RETURN o PR_CONST (op_bound_val P)) ∈ [λx. P x]⇩a A⇧d → b_assn A P"
    apply sepref_to_hoare
    unfolding op_bound_val_def
    apply vcg
    done
  
  lemma mop_bound_val_refine[sepref_fr_rules]: "(Mreturn,PR_CONST (mop_bound_val P)) ∈ A⇧d →⇩a b_assn A P"
    apply sepref_to_hoare
    unfolding mop_bound_val_def
    supply [simp] = refine_pw_simps 
    apply vcg
    done


  lemma "b_assn A P a c ⊢ ↑P a ∧* A a c"
    by simp

  definition "open_b_assn x = RETURN x"

  lemma "hn_refine (b_assn A P a c) (Mreturn c) □ A (λ r. r = c) (open_b_assn a)"
    apply(sepref_to_hoare)
    unfolding open_b_assn_def
    apply vcg
    done


  definition b_assn_open_block :: "'a ⇒ ('a ⇒ 'b nres) ⇒ 'b nres" where "b_assn_open_block x f = f x"

  lemma hn_b_assn_open_block[sepref_comb_rules]:
    assumes "Γ ⊢ hn_ctxt (b_assn A B) x xi ∧* Γ⇩1"
    assumes "B x ⟹ hn_refine (hn_ctxt A x xi ∧* Γ⇩1) fi Γ⇩2 R CP (f x)"
    assumes "Γ⇩2 ⊢ hn_ctxt A x xi ∧* Γ⇩3"
    shows "hn_refine (Γ) (fi) (hn_ctxt (b_assn A B) x xi ∧* Γ⇩3) R CP (b_assn_open_block$x$(λ⇩2 x. f x))"
    apply(rule hn_refine_cons_pre[OF assms(1)])
    apply(cases "B x")     
    unfolding hn_ctxt_def
    subgoal 
      apply (simp add: sep_algebra_simps b_assn_open_block_def)
      apply(rule hn_refine_cons[OF _ assms(2)])
      apply(simp add: hn_ctxt_def)
      apply(simp)
      using assms(3)[unfolded hn_ctxt_def] apply simp
      apply simp
      done
    subgoal by simp
    done

  lemma b_assn_open_block_mono[refine_mono]: 
    "⟦⋀a. f a ≤ f' a⟧ ⟹ b_assn_open_block x f ≤ b_assn_open_block x f'"
    unfolding b_assn_open_block_def
    by refine_mono

  lemma b_assn_open_block_arity[sepref_monadify_arity]: "b_assn_open_block ≡ λ⇩2x f. SP b_assn_open_block$x$(λ⇩2a. f$a)"
    by simp

  lemma b_assn_open_block_comb[sepref_monadify_comb]:  
    "b_assn_open_block$x$f = Refine_Basic.bind$(EVAL$x)$(λ⇩2x. SP b_assn_open_block$x$f)"
    by simp

  lemma b_assn_open_block_mono_flat[refine_mono]: 
    "⟦⋀a. flat_ge (f a) (f' a)⟧ ⟹ flat_ge (b_assn_open_block x f) (b_assn_open_block x f')"
    unfolding b_assn_open_block_def
    by refine_mono

  lemma WITH_SPLIT_rule[refine_vcg]:
      assumes "f x ≤ SPEC P"
      shows "b_assn_open_block x f ≤ SPEC P"  
      using assms(1) unfolding b_assn_open_block_def
      by simp

  lemma WITH_split_refine[refine]:
      assumes "f' x' ≤⇓R (f x)"
      shows "b_assn_open_block x' f' ≤⇓R (b_assn_open_block x f)"
      unfolding b_assn_open_block_def
      using assms
      by auto


  lemma aux1: assumes "(fi,f) ∈ [P]⇩a A⇧k *⇩a B⇧k → C" shows "(fi,f) ∈ [P]⇩a A⇧k *⇩a (b_assn B Q)⇧k → C"
    apply sepref_to_hoare 
    apply(rule htriple_pure_preI)
    apply(rule cons_rule)
    apply(rule assms[simplified, THEN hfrefD, THEN hn_refineD] )
    apply assumption
    apply simp
    apply assumption
    apply (simp add: sep_algebra_simps)
    apply (auto simp add: sep_algebra_simps dest!: pure_part_split_conj)
    done

end