Theory Sepref_HOL_Bindings

section HOL Setup
theory Sepref_HOL_Bindings
imports Sepref_Tool
begin

subsection Assertion Annotation
text Annotate an assertion to a term. The term must then be refined with this assertion.
(* TODO: Version for monadic expressions.*)
definition ASSN_ANNOT :: "('a  'ai  assn)  'a  'a" where [simp]: "ASSN_ANNOT A x  x"
context fixes A :: "'a  'ai  assn" begin
  sepref_register "PR_CONST (ASSN_ANNOT A)"
  lemma [def_pat_rules]: "ASSN_ANNOT$A  UNPROTECT (ASSN_ANNOT A)" by simp
  lemma [sepref_fr_rules]: "(Mreturn o (λx. x), RETURN o PR_CONST (ASSN_ANNOT A))  AdaA"
    by sepref_to_hoare vcg
    
end  

lemma annotate_assn: "x  ASSN_ANNOT A x" by simp


subsection Identity Relations
definition "IS_ID R  R=Id"
definition "IS_BELOW_ID R  RId"

lemma [safe_constraint_rules]: 
  "IS_ID Id"
  "IS_ID R1  IS_ID R2  IS_ID (R1  R2)"
  "IS_ID R  IS_ID (Roption_rel)"
  "IS_ID R  IS_ID (Rlist_rel)"
  "IS_ID R1  IS_ID R2  IS_ID (R1 ×r R2)"
  "IS_ID R1  IS_ID R2  IS_ID (R1,R2sum_rel)"
  by (auto simp: IS_ID_def)

lemma [safe_constraint_rules]: 
  "IS_BELOW_ID Id"
  "IS_BELOW_ID R  IS_BELOW_ID (Roption_rel)"
  "IS_BELOW_ID R1  IS_BELOW_ID R2  IS_BELOW_ID (R1 ×r R2)"
  "IS_BELOW_ID R1  IS_BELOW_ID R2  IS_BELOW_ID (R1,R2sum_rel)"
  by (auto simp: IS_ID_def IS_BELOW_ID_def option_rel_def sum_rel_def list_rel_def)

lemma IS_BELOW_ID_fun_rel_aux: "R1Id  IS_BELOW_ID R2  IS_BELOW_ID (R1  R2)"
  by (auto simp: IS_BELOW_ID_def dest: fun_relD)

corollary IS_BELOW_ID_fun_rel[safe_constraint_rules]: 
  "IS_ID R1  IS_BELOW_ID R2  IS_BELOW_ID (R1  R2)"
  using IS_BELOW_ID_fun_rel_aux[of Id R2]
  by (auto simp: IS_ID_def)


lemma IS_BELOW_ID_list_rel[safe_constraint_rules]: 
  "IS_BELOW_ID R  IS_BELOW_ID (Rlist_rel)"
  unfolding IS_BELOW_ID_def
proof safe
  fix l l'
  assume A: "RId" 
  assume "(l,l')Rlist_rel"
  thus "l=l'"
    apply induction
    using A by auto
qed

lemma IS_ID_imp_BELOW_ID[constraint_rules]: 
  "IS_ID R  IS_BELOW_ID R"
  by (auto simp: IS_ID_def IS_BELOW_ID_def )



subsection Inverse Relation

lemma inv_fun_rel_eq[simp]: "(AB)¯ = A¯B¯"
  by (auto dest: fun_relD)

lemma inv_option_rel_eq[simp]: "(Koption_rel)¯ = K¯option_rel"
  by (auto simp: option_rel_def)

lemma inv_prod_rel_eq[simp]: "(P ×r Q)¯ = P¯ ×r Q¯"
  by (auto)

lemma inv_sum_rel_eq[simp]: "(P,Qsum_rel)¯ = P¯,Q¯sum_rel"
  by (auto simp: sum_rel_def)

lemma inv_list_rel_eq[simp]: "(Rlist_rel)¯ = R¯list_rel"
  unfolding list_rel_def
  apply safe
  apply (subst list.rel_flip[symmetric])
  apply (simp add: conversep_iff[abs_def])
  apply (subst list.rel_flip[symmetric])
  apply (simp add: conversep_iff[abs_def])
  done

lemmas [constraint_simps] =
  Relation.converse_Id
  inv_fun_rel_eq
  inv_option_rel_eq
  inv_prod_rel_eq
  inv_sum_rel_eq
  inv_list_rel_eq


subsection Single Valued and Total Relations

(* TODO: Link to other such theories: Transfer, Autoref *)
definition "IS_LEFT_UNIQUE R  single_valued (R¯)"
definition "IS_LEFT_TOTAL R  Domain R = UNIV"
definition "IS_RIGHT_TOTAL R  Range R = UNIV"
abbreviation (input) "IS_RIGHT_UNIQUE  single_valued"

lemmas IS_RIGHT_UNIQUED = single_valuedD
lemma IS_LEFT_UNIQUED: "IS_LEFT_UNIQUE r; (y, x)  r; (z, x)  r  y = z"
  by (auto simp: IS_LEFT_UNIQUE_def dest: single_valuedD)

lemma prop2p:
  "IS_LEFT_UNIQUE R = left_unique (rel2p R)"
  "IS_RIGHT_UNIQUE R = right_unique (rel2p R)"
  "right_unique (rel2p (R¯)) = left_unique (rel2p R)"
  "IS_LEFT_TOTAL R = left_total (rel2p R)"
  "IS_RIGHT_TOTAL R = right_total (rel2p R)"
  by (auto 
    simp: IS_LEFT_UNIQUE_def left_unique_def single_valued_def
    simp: right_unique_def
    simp: IS_LEFT_TOTAL_def left_total_def
    simp: IS_RIGHT_TOTAL_def right_total_def
    simp: rel2p_def
    )

lemma p2prop:
  "left_unique P = IS_LEFT_UNIQUE (p2rel P)"
  "right_unique P = IS_RIGHT_UNIQUE (p2rel P)"
  "left_total P = IS_LEFT_TOTAL (p2rel P)"
  "right_total P = IS_RIGHT_TOTAL (p2rel P)"
  "bi_unique P  left_unique P  right_unique P"
  by (auto 
    simp: IS_LEFT_UNIQUE_def left_unique_def single_valued_def
    simp: right_unique_def bi_unique_alt_def
    simp: IS_LEFT_TOTAL_def left_total_def
    simp: IS_RIGHT_TOTAL_def right_total_def
    simp: p2rel_def
    )

lemmas [safe_constraint_rules] = 
  single_valued_Id  
  prod_rel_sv 
  list_rel_sv 
  option_rel_sv 
  sum_rel_sv

lemma [safe_constraint_rules]:
  "IS_LEFT_UNIQUE Id"
  "IS_LEFT_UNIQUE R1  IS_LEFT_UNIQUE R2  IS_LEFT_UNIQUE (R1×rR2)"
  "IS_LEFT_UNIQUE R1  IS_LEFT_UNIQUE R2  IS_LEFT_UNIQUE (R1,R2sum_rel)"
  "IS_LEFT_UNIQUE R  IS_LEFT_UNIQUE (Roption_rel)"
  "IS_LEFT_UNIQUE R  IS_LEFT_UNIQUE (Rlist_rel)"
  by (auto simp: IS_LEFT_UNIQUE_def prod_rel_sv sum_rel_sv option_rel_sv list_rel_sv)

lemma IS_LEFT_TOTAL_alt: "IS_LEFT_TOTAL R  (x. y. (x,y)R)"
  by (auto simp: IS_LEFT_TOTAL_def)

lemma IS_RIGHT_TOTAL_alt: "IS_RIGHT_TOTAL R  (x. y. (y,x)R)"
  by (auto simp: IS_RIGHT_TOTAL_def)

lemma [safe_constraint_rules]:
  "IS_LEFT_TOTAL Id"
  "IS_LEFT_TOTAL R1  IS_LEFT_TOTAL R2  IS_LEFT_TOTAL (R1×rR2)"
  "IS_LEFT_TOTAL R1  IS_LEFT_TOTAL R2  IS_LEFT_TOTAL (R1,R2sum_rel)"
  "IS_LEFT_TOTAL R  IS_LEFT_TOTAL (Roption_rel)"
  apply (auto simp: IS_LEFT_TOTAL_alt sum_rel_def option_rel_def list_rel_def)
  apply (rename_tac x; case_tac x; auto)
  apply (rename_tac x; case_tac x; auto)
  done

lemma [safe_constraint_rules]: "IS_LEFT_TOTAL R  IS_LEFT_TOTAL (Rlist_rel)"
  unfolding IS_LEFT_TOTAL_alt
proof safe
  assume A: "x.y. (x,y)R"
  fix l
  show "l'. (l,l')Rlist_rel"
    apply (induction l)
    using A
    by (auto simp: list_rel_split_right_iff)
qed

lemma [safe_constraint_rules]:
  "IS_RIGHT_TOTAL Id"
  "IS_RIGHT_TOTAL R1  IS_RIGHT_TOTAL R2  IS_RIGHT_TOTAL (R1×rR2)"
  "IS_RIGHT_TOTAL R1  IS_RIGHT_TOTAL R2  IS_RIGHT_TOTAL (R1,R2sum_rel)"
  "IS_RIGHT_TOTAL R  IS_RIGHT_TOTAL (Roption_rel)"
  apply (auto simp: IS_RIGHT_TOTAL_alt sum_rel_def option_rel_def) []
  apply (auto simp: IS_RIGHT_TOTAL_alt sum_rel_def option_rel_def) []
  apply (auto simp: IS_RIGHT_TOTAL_alt sum_rel_def option_rel_def) []
  apply (rename_tac x; case_tac x; auto)
  apply (clarsimp simp: IS_RIGHT_TOTAL_alt option_rel_def)
  apply (rename_tac x; case_tac x; auto)
  done

lemma [safe_constraint_rules]: "IS_RIGHT_TOTAL R  IS_RIGHT_TOTAL (Rlist_rel)"
  unfolding IS_RIGHT_TOTAL_alt
proof safe
  assume A: "x.y. (y,x)R"
  fix l
  show "l'. (l',l)Rlist_rel"
    apply (induction l)
    using A
    by (auto simp: list_rel_split_left_iff)
qed
  
lemma [constraint_simps]:
  "IS_LEFT_TOTAL (R¯)  IS_RIGHT_TOTAL R "
  "IS_RIGHT_TOTAL (R¯)  IS_LEFT_TOTAL R  "
  "IS_LEFT_UNIQUE (R¯)  IS_RIGHT_UNIQUE R"
  "IS_RIGHT_UNIQUE (R¯)  IS_LEFT_UNIQUE R "
  by (auto simp: IS_RIGHT_TOTAL_alt IS_LEFT_TOTAL_alt IS_LEFT_UNIQUE_def)

lemma [safe_constraint_rules]:
  "IS_RIGHT_UNIQUE A  IS_RIGHT_TOTAL B  IS_RIGHT_TOTAL (AB)"
  "IS_RIGHT_TOTAL A  IS_RIGHT_UNIQUE B  IS_RIGHT_UNIQUE (AB)"
  "IS_LEFT_UNIQUE A  IS_LEFT_TOTAL B  IS_LEFT_TOTAL (AB)"
  "IS_LEFT_TOTAL A  IS_LEFT_UNIQUE B  IS_LEFT_UNIQUE (AB)"
  apply (simp_all add: prop2p rel2p)
  (*apply transfer_step TODO: Isabelle 2016 *)
  apply (blast intro!: transfer_raw)+
  done

lemma [constraint_rules]: 
  "IS_BELOW_ID R  IS_RIGHT_UNIQUE R"
  "IS_BELOW_ID R  IS_LEFT_UNIQUE R"
  "IS_ID R  IS_RIGHT_TOTAL R"
  "IS_ID R  IS_LEFT_TOTAL R"
  by (auto simp: IS_BELOW_ID_def IS_ID_def IS_LEFT_UNIQUE_def IS_RIGHT_TOTAL_def IS_LEFT_TOTAL_def
    intro: single_valuedI)

thm constraint_rules

subsubsection Additional Parametricity Lemmas
(* TODO: Move. Problem: Depend on IS_LEFT_UNIQUE, which has to be moved to!*)

lemma param_distinct[param]: "IS_LEFT_UNIQUE A; IS_RIGHT_UNIQUE A  (distinct, distinct)  Alist_rel  bool_rel"  
  apply (fold rel2p_def)
  apply (simp add: rel2p)
  apply (rule distinct_transfer)
  apply (simp add: p2prop)
  done

lemma param_Image[param]: 
  assumes "IS_LEFT_UNIQUE A" "IS_RIGHT_UNIQUE A"
  shows "((``), (``))  A×rBset_rel  Aset_rel  Bset_rel"
  apply (clarsimp simp: set_rel_def; intro conjI)  
  apply (fastforce dest: IS_RIGHT_UNIQUED[OF assms(2)])
  apply (fastforce dest: IS_LEFT_UNIQUED[OF assms(1)])
  done

lemma pres_eq_iff_svb: "((=),(=))KKbool_rel  (single_valued K  single_valued (K¯))"
  apply (safe intro!: single_valuedI)
  apply (metis (full_types) IdD fun_relD1)
  apply (metis (full_types) IdD fun_relD1)
  by (auto dest: single_valuedD)

definition "IS_PRES_EQ R  ((=), (=))RRbool_rel"
lemma [constraint_rules]: "single_valued R; single_valued (R¯)  IS_PRES_EQ R"
  by (simp add: pres_eq_iff_svb IS_PRES_EQ_def)


subsection Bounded Assertions
definition "b_rel R P  R  UNIV×Collect P"
definition "b_assn A P  λx y. (P x) ** A x y"

lemma b_assn_pure_conv[constraint_simps]: "b_assn (pure R) P = pure (b_rel R P)"
  by (auto del: ext intro!: ext simp: b_rel_def b_assn_def pure_def pred_lift_extract_simps)
lemmas [sepref_import_rewrite, named_ss sepref_frame_normrel, fcomp_norm_unfold] 
  = b_assn_pure_conv[symmetric]

lemma b_rel_nesting[simp]: 
  "b_rel (b_rel R P1) P2 = b_rel R (λx. P1 x  P2 x)"
  by (auto simp: b_rel_def)
lemma b_rel_triv[simp]: 
  "b_rel R (λ_. True) = R"
  by (auto simp: b_rel_def)
lemma b_assn_nesting[simp]: 
  "b_assn (b_assn A P1) P2 = b_assn A (λx. P1 x  P2 x)"
  by (auto simp: b_assn_def pure_def pred_lift_extract_simps del: ext intro!: ext)
lemma b_assn_triv[simp]: 
  "b_assn A (λ_. True) = A"
  by (auto simp: b_assn_def pure_def pred_lift_extract_simps del: ext intro!: ext)

lemmas [constraint_simps,sepref_import_rewrite, named_ss sepref_frame_normrel, fcomp_norm_unfold]
  = b_rel_nesting b_assn_nesting

lemma b_rel_simp[simp]: "(x,y)b_rel R P  (x,y)R  P y"
  by (auto simp: b_rel_def)

lemma b_assn_simp[simp]: "b_assn A P x y = ((P x) ** A x y)"
  by (auto simp: b_assn_def)

lemma b_rel_Range[simp]: "Range (b_rel R P) = Range R  Collect P" by auto
lemma b_assn_rdom[simp]: "rdomp (b_assn R P) x  rdomp R x  P x"
  by (auto simp: rdomp_def pred_lift_extract_simps)


lemma b_rel_below_id[constraint_rules,relator_props]: 
  "IS_BELOW_ID R  IS_BELOW_ID (b_rel R P)"
  by (auto simp: IS_BELOW_ID_def)

lemma b_rel_left_unique[constraint_rules,relator_props]: 
  "IS_LEFT_UNIQUE R  IS_LEFT_UNIQUE (b_rel R P)"
  by (auto simp: IS_LEFT_UNIQUE_def single_valued_def)
  
lemma b_rel_right_unique[constraint_rules,relator_props]: 
  "IS_RIGHT_UNIQUE R  IS_RIGHT_UNIQUE (b_rel R P)"
  by (auto simp: single_valued_def)

― ‹Registered as safe rule, although may loose information in the 
    odd case that purity depends condition.
lemma b_assn_is_pure[safe_constraint_rules, simp]:
  "is_pure A  is_pure (b_assn A P)"
  by (auto simp: is_pure_conv b_assn_pure_conv)

lemma R_comp_brel_id_conv[fcomp_norm_simps]: "R O b_rel Id P = b_rel R P" by auto
  
  
― ‹Most general form
lemma b_assn_subtyping_match[sepref_frame_match_rules]:
  assumes "hn_ctxt (b_assn A P) x y  hn_ctxt A' x y"
  assumes "vassn_tag (hn_ctxt A x y); vassn_tag (hn_ctxt A' x y); P x  P' x"
  shows "hn_ctxt (b_assn A P) x y  hn_ctxt (b_assn A' P') x y"
  using assms
  unfolding hn_ctxt_def b_assn_def entails_def vassn_tag_def
  by (auto simp: pred_lift_extract_simps)
  
― ‹Simplified forms:
lemma b_assn_subtyping_match_eqA[sepref_frame_match_rules]:
  assumes "vassn_tag (hn_ctxt A x y); P x  P' x"
  shows "hn_ctxt (b_assn A P) x y  hn_ctxt (b_assn A P') x y"
  apply (rule b_assn_subtyping_match)
  subgoal 
    unfolding hn_ctxt_def b_assn_def entails_def vassn_tag_def
    by (auto simp: pred_lift_extract_simps)
  subgoal
    using assms .
  done  

lemma b_assn_subtyping_match_tR[sepref_frame_match_rules]:
  assumes "P x  hn_ctxt A x y  hn_ctxt A' x y"
  shows "hn_ctxt (b_assn A P) x y  hn_ctxt A' x y"
  using assms
  unfolding hn_ctxt_def b_assn_def entails_def
  by (auto simp: pred_lift_extract_simps)

lemma b_assn_subtyping_match_tL[sepref_frame_match_rules]:
  assumes "hn_ctxt A x y  hn_ctxt A' x y"
  assumes "vassn_tag (hn_ctxt A x y)  P' x"
  shows "hn_ctxt A x y  hn_ctxt (b_assn A' P') x y"
  using assms
  unfolding hn_ctxt_def b_assn_def entails_def vassn_tag_def
  by (auto simp: pred_lift_extract_simps)


lemma b_assn_subtyping_match_eqA_tR[sepref_frame_match_rules]: 
  "hn_ctxt (b_assn A P) x y  hn_ctxt A x y"
  unfolding hn_ctxt_def b_assn_def entails_def
  by (auto simp: pred_lift_extract_simps)

lemma b_assn_subtyping_match_eqA_tL[sepref_frame_match_rules]:
  assumes "vassn_tag (hn_ctxt A x y)  P' x"
  shows "hn_ctxt A x y  hn_ctxt (b_assn A P') x y"
  using assms
  unfolding hn_ctxt_def b_assn_def entails_def vassn_tag_def
  by (auto simp: pred_lift_extract_simps)

  
lemma b_rel_gen_merge:
  assumes A: "MERGE1 A f B g C"  
  shows "MERGE1 (b_assn A P) f (b_assn B Q) g (b_assn C (λx. P x  Q x))"  
  supply [vcg_rules] = MERGE1D[OF A]
  apply rule
  by vcg
  
lemmas b_rel_merge_eq[sepref_frame_merge_rules] = b_rel_gen_merge[where P=P and Q=P for P, simplified]
lemmas [sepref_frame_merge_rules] = b_rel_gen_merge
lemmas b_rel_merge_left[sepref_frame_merge_rules] = b_rel_gen_merge[where Q="λ_. True", simplified]
lemmas b_rel_merge_right[sepref_frame_merge_rules] = b_rel_gen_merge[where P="λ_. True", simplified]
  
(*  
― ‹General form›
lemma b_rel_subtyping_merge[sepref_frame_merge_rules]:
  assumes "hn_ctxt A x y ∨A hn_ctxt A' x y ⟹t hn_ctxt Am x y"
  shows "hn_ctxt (b_assn A P) x y ∨A hn_ctxt (b_assn A' P') x y ⟹t hn_ctxt (b_assn Am (λx. P x ∨ P' x)) x y"
  using assms
  unfolding hn_ctxt_def b_assn_def entailst_def entails_def
  by (fastforce simp: vassn_tag_def)
  
― ‹Simplified forms›
lemma b_rel_subtyping_merge_eqA[sepref_frame_merge_rules]:
  shows "hn_ctxt (b_assn A P) x y ∨A hn_ctxt (b_assn A P') x y ⟹t hn_ctxt (b_assn A (λx. P x ∨ P' x)) x y"
  apply (rule b_rel_subtyping_merge)
  by simp

lemma b_rel_subtyping_merge_tL[sepref_frame_merge_rules]:
  assumes "hn_ctxt A x y ∨A hn_ctxt A' x y ⟹t hn_ctxt Am x y"
  shows "hn_ctxt A x y ∨A hn_ctxt (b_assn A' P') x y ⟹t hn_ctxt Am x y"
  using b_rel_subtyping_merge[of A x y A' Am "λ_. True" P', simplified] assms .

lemma b_rel_subtyping_merge_tR[sepref_frame_merge_rules]:
  assumes "hn_ctxt A x y ∨A hn_ctxt A' x y ⟹t hn_ctxt Am x y"
  shows "hn_ctxt (b_assn A P) x y ∨A hn_ctxt A' x y ⟹t hn_ctxt Am x y"
  using b_rel_subtyping_merge[of A x y A' Am P "λ_. True", simplified] assms .

lemma b_rel_subtyping_merge_eqA_tL[sepref_frame_merge_rules]:
  shows "hn_ctxt A x y ∨A hn_ctxt (b_assn A P') x y ⟹t hn_ctxt A x y"
  using b_rel_subtyping_merge_eqA[of A "λ_. True" x y P', simplified] .

lemma b_rel_subtyping_merge_eqA_tR[sepref_frame_merge_rules]:
  shows "hn_ctxt (b_assn A P) x y ∨A hn_ctxt A x y ⟹t hn_ctxt A x y"
  using b_rel_subtyping_merge_eqA[of A P x y "λ_. True", simplified] .

(* TODO: Combinatorial explosion :( *)
lemma b_assn_invalid_merge1: "hn_invalid (b_assn A P) x y ∨A hn_invalid (b_assn A P') x y
  ⟹t hn_invalid (b_assn A (λx. P x ∨ P' x)) x y"
  by (sep_auto simp: hn_ctxt_def invalid_assn_def entailst_def)

lemma b_assn_invalid_merge2: "hn_invalid (b_assn A P) x y ∨A hn_invalid A x y
  ⟹t hn_invalid A x y"
  by (sep_auto simp: hn_ctxt_def invalid_assn_def entailst_def)
lemma b_assn_invalid_merge3: "hn_invalid A x y ∨A hn_invalid (b_assn A P) x y
  ⟹t hn_invalid A x y"
  by (sep_auto simp: hn_ctxt_def invalid_assn_def entailst_def)

lemma b_assn_invalid_merge4: "hn_invalid (b_assn A P) x y ∨A hn_ctxt (b_assn A P') x y
  ⟹t hn_invalid (b_assn A (λx. P x ∨ P' x)) x y"
  by (sep_auto simp: hn_ctxt_def invalid_assn_def entailst_def)
lemma b_assn_invalid_merge5: "hn_ctxt (b_assn A P') x y ∨A hn_invalid (b_assn A P) x y
  ⟹t hn_invalid (b_assn A (λx. P x ∨ P' x)) x y"
  by (sep_auto simp: hn_ctxt_def invalid_assn_def entailst_def)

lemma b_assn_invalid_merge6: "hn_invalid (b_assn A P) x y ∨A hn_ctxt A x y
  ⟹t hn_invalid A x y"
  by (sep_auto simp: hn_ctxt_def invalid_assn_def entailst_def)
lemma b_assn_invalid_merge7: "hn_ctxt A x y ∨A hn_invalid (b_assn A P) x y
  ⟹t hn_invalid A x y"
  by (sep_auto simp: hn_ctxt_def invalid_assn_def entailst_def)

lemma b_assn_invalid_merge8: "hn_ctxt (b_assn A P) x y ∨A hn_invalid A x y
  ⟹t hn_invalid A x y"
  by (sep_auto simp: hn_ctxt_def invalid_assn_def entailst_def)
lemma b_assn_invalid_merge9: "hn_invalid A x y ∨A hn_ctxt (b_assn A P) x y
  ⟹t hn_invalid A x y"
  by (sep_auto simp: hn_ctxt_def invalid_assn_def entailst_def)

lemmas b_assn_invalid_merge[sepref_frame_merge_rules] = 
  b_assn_invalid_merge1
  b_assn_invalid_merge2
  b_assn_invalid_merge3
  b_assn_invalid_merge4
  b_assn_invalid_merge5
  b_assn_invalid_merge6
  b_assn_invalid_merge7
  b_assn_invalid_merge8
  b_assn_invalid_merge9

*)



abbreviation nbn_rel :: "nat  (nat × nat) set" 
  ― ‹Natural numbers with upper bound.
  where "nbn_rel n  b_rel nat_rel (λx::nat. x<n)"  


lemma in_R_comp_nbn_conv: "(a,b)(R O nbn_rel N)  (a,b)R  b<N" by auto
lemma range_comp_nbn_conv: "Range (R O nbn_rel N) = Range R  {0..<N}"
  by (auto 0 3 simp: b_rel_def)

lemma mk_free_b_assn[sepref_frame_free_rules]:
  assumes "MK_FREE A f"  
  shows "MK_FREE (b_assn A P) f"  
proof -
  note [vcg_rules] = assms[THEN MK_FREED]
  show ?thesis by rule vcg
qed

lemma intf_of_b_rel[synth_rules]: "INTF_OF_REL R I  INTF_OF_REL (b_rel R P) I" by simp

lemma b_assn_intf[intf_of_assn]: "intf_of_assn V I  intf_of_assn (b_assn V P) I"
  by simp


text Introduce extra goal for bounded result
lemma hfref_bassn_resI:
  assumes "xs. rdomp (fst As) xs; C xs  a xs n SPEC P"
  assumes "(c,a)[C]a As  R"
  shows "(c,a)[C]a As  b_assn R P"
  apply rule
  apply (rule hn_refine_preI)
  apply (rule hn_refine_cons[rotated])
  apply (rule hn_refine_augment_res)
  apply (rule assms(2)[to_hnr, unfolded hn_ctxt_def autoref_tag_defs])
  apply simp
  apply (rule assms(1))
  apply (auto simp: rdomp_def sep_algebra_simps)
  done

  
  
subsection Tool Setup
lemmas [sepref_relprops] = 
  sepref_relpropI[of IS_LEFT_UNIQUE]
  sepref_relpropI[of IS_RIGHT_UNIQUE]
  sepref_relpropI[of IS_LEFT_TOTAL]
  sepref_relpropI[of IS_RIGHT_TOTAL]
  sepref_relpropI[of is_pure]
  sepref_relpropI[of "IS_PURE Φ" for Φ]
  sepref_relpropI[of IS_ID]
  sepref_relpropI[of IS_BELOW_ID]
 


lemma [sepref_relprops_simps]:
  "CONSTRAINT (IS_PURE IS_ID) A  CONSTRAINT (IS_PURE IS_BELOW_ID) A"
  "CONSTRAINT (IS_PURE IS_ID) A  CONSTRAINT (IS_PURE IS_LEFT_TOTAL) A"
  "CONSTRAINT (IS_PURE IS_ID) A  CONSTRAINT (IS_PURE IS_RIGHT_TOTAL) A"
  "CONSTRAINT (IS_PURE IS_BELOW_ID) A  CONSTRAINT (IS_PURE IS_LEFT_UNIQUE) A"
  "CONSTRAINT (IS_PURE IS_BELOW_ID) A  CONSTRAINT (IS_PURE IS_RIGHT_UNIQUE) A"
  by (auto 
    simp: IS_ID_def IS_BELOW_ID_def IS_PURE_def IS_LEFT_UNIQUE_def
    simp: IS_LEFT_TOTAL_def IS_RIGHT_TOTAL_def
    simp: single_valued_below_Id)

declare True_implies_equals[sepref_relprops_simps]

lemma [sepref_relprops_transform]: "single_valued (R¯) = IS_LEFT_UNIQUE R"
  by (auto simp: IS_LEFT_UNIQUE_def)

  
subsection Default Initializers  
text We define a generic algorithm scheme to determine the abstract counterpart of
  the terminit::'a::llvm_rep value wrt. an assertion. This is important for 
  initializing container data structures directly from zero-initializing calloc›, 
  rather than having to memset› each array.

definition is_init :: "('a  'c::llvm_rep  assn)  'a  bool" 
  where "is_init A i  is_pure A  (init,i)  the_pure A"
  
lemma is_init_id_assn[sepref_gen_algo_rules]: "GEN_ALGO init (is_init id_assn)"
  by (auto simp: GEN_ALGO_def is_init_def)
  
  
subsection Arithmetics

subsubsection Connecting to Standard Operation Abstraction from LLVM-RS

text We will hide the connection behind an additional abstraction layer, 
  introduced by definitions. So, the definitions from this locale should not 
  be used by the end-user.

context standard_opr_abstraction begin
  definition "rel  br α I"

  lemma assn_is_rel: "assn = pure rel"
    unfolding pure_def rel_def in_br_conv assn_def
    apply (intro ext)
    apply (auto simp: pred_lift_extract_simps)
    done
    
  abbreviation (input) sepref_assn where "sepref_assn  pure rel"  

  lemma hn_un_op:
    assumes "is_un_op PRE cop xmop aop"  
    shows "(cop,(RETURN o aop))  [λa. PRE TYPE('c) a]a sepref_assnk  sepref_assn"
    unfolding assn_is_rel[symmetric]
    apply sepref_to_hoare
    supply [vcg_rules] = un_op_tmpl[OF assms]
    by vcg
      
  lemma hn_bin_op:
    assumes "is_bin_op PRE cop xmop aop"  
    shows "(uncurry cop,uncurry (RETURN oo aop))  [λ(a,b). PRE TYPE('c) a b]a sepref_assnk *a sepref_assnk  sepref_assn"
    unfolding assn_is_rel[symmetric]
    apply sepref_to_hoare
    supply [vcg_rules] = bin_op_tmpl[OF assms]
    by vcg
    
  lemma hn_cmp_op:  
    assumes "is_cmp_op cop xmop aop"
    shows "(uncurry cop, uncurry (RETURN oo aop))  sepref_assnk *a sepref_assnk a bool.sepref_assn"
    unfolding assn_is_rel[symmetric] bool.assn_is_rel[symmetric]
    apply sepref_to_hoare
    supply [vcg_rules] = cmp_op_tmpl[OF assms]
    by vcg
    

end

subsubsection Operator Setup

text Not-Equals is an operator in LLVM, but not in HOL
definition [simp]: "op_neq a b  ab"  
(* TODO: Maybe have this pattern rule only for certain types.
  Otherwise, op_neq has to be implemented by every type that has custom eq-operator!

  The best solution would, or course, be to have a generic algorithm!
*)
lemma op_neq_pat[def_pat_rules]: "Not$((=)$a$b)  op_neq$a$b" by simp
sepref_register op_neq_word: "op_neq :: _ word  _"


text For technical reasons, we need the operands as parameters to the operators 
  on the concrete side of refinement theorems. Thus, we define the following shortcut
  for comparison operators.     
(* TODO/FIXME: This, in turn, relies on LLVM-inlining of from_bool (comparison)! 
  Perhaps we should directly generate the ll_icmp instructions
*)  
definition [llvm_inline]: "lift_cmp_op c a b  from_bool (c a b)"  
  


   
subsubsection Boolean

definition "bool1_rel  bool.rel"
abbreviation "bool1_assn  (pure bool1_rel)"

lemma bool_const_refine[sepref_import_param]:
  "(0,False)bool1_rel"  
  "(1,True)bool1_rel"  
  by (auto simp: bool1_rel_def bool.rel_def in_br_conv)
  

lemma hn_bool_ops[sepref_fr_rules]:
  "(uncurry ll_and, uncurry (RETURN ∘∘ (∧)))  bool1_assnk *a bool1_assnk a bool1_assn"
  "(uncurry ll_or, uncurry (RETURN ∘∘ (∨)))  bool1_assnk *a bool1_assnk a bool1_assn"
  "(uncurry ll_xor, uncurry (RETURN ∘∘ (op_neq)))  bool1_assnk *a bool1_assnk a bool1_assn"
  "(ll_not1, RETURN  Not)  bool1_assnk a bool1_assn"
  using bool_bin_ops[THEN bool.hn_bin_op, folded bool1_rel_def, unfolded to_hfref_post]
    and bool_un_ops[THEN bool.hn_un_op, folded bool1_rel_def]
  unfolding op_neq_def  
  by simp_all

text We define an implies connective, using sepref
sepref_definition ll_implies is "uncurry (RETURN oo (⟶))" :: "bool1_assnk *a bool1_assnk a bool1_assn"
  unfolding imp_conv_disj
  by sepref

declare ll_implies_def[llvm_inline]
declare ll_implies.refine[sepref_fr_rules]

lemma is_init_bool[sepref_gen_algo_rules]:
  "GEN_ALGO False (is_init bool1_assn)"
  unfolding GEN_ALGO_def is_init_def
  unfolding bool1_rel_def bool.rel_def
  by (simp add: in_br_conv)

subsubsection Direct Word Arithmetic

abbreviation "word_rel  (Id::(_::len word × _) set)"
abbreviation "word_assn  (id_assn::_::len word  _)"
abbreviation word_assn' :: "'a::len itself  'a word  'a word  llvm_amemory  bool" 
  where "word_assn' _  word_assn"

(* TODO: Move *)  
definition ll_not :: "'a::len word  'a word llM" where 
  [llvm_inline]: "ll_not a  doM { a  ll_sub 0 a; ll_sub a 1 }"
  
context llvm_prim_arith_setup begin
  
  lemma ll_not_normalize[vcg_normalize_simps]: "ll_not a = Mreturn (~~a)"
    unfolding ll_not_def
    supply [simp] = NOT_eq
    by vcg_normalize
  
end  


context begin  
  interpretation llvm_prim_arith_setup .  

context fixes a::num begin  
  sepref_register 
    "numeral a :: _ word"  
    "0 :: _ word"
    "1 :: _ word"

  lemma word_numeral_param[sepref_import_param]:
    "(numeral a,PR_CONST (numeral a))  word_rel"  
    "(0,0)word_rel"
    "(1,1)word_rel"
    by auto
        
end
  
   
sepref_register 
  plus_word: "(+):: _ word  _"  
  minus_word: "(-):: _ word  _"  
  times_word: "(*):: _ word  _"  
  and_word: "(AND):: _ word  _"  
  or_word: "(OR):: _ word  _"  
  xor_word: "(XOR):: _ word  _"  
  
lemma word_param_imports[sepref_import_param]:
  "((+),(+))  word_rel  word_rel  word_rel"
  "((-),(-))  word_rel  word_rel  word_rel"
  "((*),(*))  word_rel  word_rel  word_rel"
  "((AND),(AND))  word_rel  word_rel  word_rel"
  "((OR),(OR))  word_rel  word_rel  word_rel"
  "((XOR),(XOR))  word_rel  word_rel  word_rel"
  by simp_all

sepref_register 
  not_word: "(NOT):: _ word  _"  

lemma hn_word_NOT[sepref_fr_rules]: "(ll_not,RETURN o (NOT))  word_assnk a word_assn"
  by sepref_to_hoare vcg
  
sepref_register 
  div_word: "(div):: _ word  _"  
  mod_word: "(mod):: _ word  _"  
  sdiv_word: "(sdiv):: _ word  _"  
  smod_word: "(smod):: _ word  _"  
  
lemma hn_word_div_op[sepref_fr_rules]:
  "(uncurry (ll_udiv),uncurry (RETURN oo (div)))  [λ(_,d). d0]a word_assnk *a word_assnk  word_assn"  
  "(uncurry (ll_urem),uncurry (RETURN oo (mod)))  [λ(_,d). d0]a word_assnk *a word_assnk  word_assn"  
  "(uncurry (ll_sdiv),uncurry (RETURN oo (sdiv)))  [λ(c,d). d0  in_srange (sdiv) c d]a word_assnk *a word_assnk  word_assn"  
  "(uncurry (ll_srem),uncurry (RETURN oo (smod)))  [λ(c,d). d0  in_srange (sdiv) c d]a word_assnk *a word_assnk  word_assn"  
  by (sepref_to_hoare; vcg; fail)+

sepref_register 
  eq_word: "(=):: _ word  _"  
  neq_word: "op_neq:: _ word  _"  
  ult_word: "(<):: _ word  _"  
  ule_word: "(≤):: _ word  _"  
  slt_word: "(<s):: _ word  _"  
  sle_word: "(≤s):: _ word  _"  
    
lemma hn_word_icmp_op[sepref_fr_rules]:
  "(uncurry (ll_icmp_eq), uncurry (RETURN oo (=)))  word_assnk *a word_assnk a bool1_assn"
  "(uncurry (ll_icmp_ne), uncurry (RETURN oo (op_neq)))  word_assnk *a word_assnk a bool1_assn"
  "(uncurry (ll_icmp_ult), uncurry (RETURN oo (<)))  word_assnk *a word_assnk a bool1_assn"
  "(uncurry (ll_icmp_ule), uncurry (RETURN oo (≤)))  word_assnk *a word_assnk a bool1_assn"
  "(uncurry (ll_icmp_slt), uncurry (RETURN oo (λa b. a <s b)))  word_assnk *a word_assnk a bool1_assn"
  "(uncurry (ll_icmp_sle), uncurry (RETURN oo (λa b. a <=s b)))  word_assnk *a word_assnk a bool1_assn"
  unfolding bool1_rel_def bool.rel_def
  supply [simp] = in_br_conv
  apply (sepref_to_hoare; vcg; fail)+
  done
  
  
lemma is_init_word[sepref_gen_algo_rules]:
  "GEN_ALGO 0 (is_init word_assn)"
  unfolding GEN_ALGO_def is_init_def
  by (simp)
  
end  
      

subsubsection Integer by Word
  
definition "sint_rel  sint.rel"
abbreviation "sint_assn  pure sint_rel"  

abbreviation (input) "sint_rel' TYPE('a::len)  sint_rel :: ('a word × _) set"
abbreviation (input) "sint_assn' TYPE('a::len)  sint_assn :: _  'a word  _"


definition [simp]: "sint_const TYPE('a::len) c  (c::int)"
context fixes c::int begin
  sepref_register "sint_const TYPE('a::len) c" :: "int"
end


lemma fold_sint:
  "0 = sint_const TYPE('a::len) 0"  
  "1 = sint_const TYPE('a::len) 1"  
  "-1  (sint_const TYPE('a::len) (-1))"  
  "numeral n  (sint_const TYPE('a::len) (numeral n))"
  "-(numeral n)  (sint_const TYPE('a::len) (-numeral n))"
  by simp_all


lemma hn_sint_0[sepref_import_param]:
  "(0,sint_const TYPE('a) 0)  sint_rel' TYPE('a::len)"
  by (auto simp: sint_rel_def sint.rel_def in_br_conv)

lemma hn_sint_1[sepref_fr_rules]:
  "LENGTH('a)1  hn_refine  (Mreturn 1)  (sint_assn' TYPE('a::len)) (λ_. True) (RETURN$PR_CONST (sint_const TYPE('a) 1))"
  apply sepref_to_hoare unfolding sint_rel_def sint.rel_def in_br_conv by vcg

lemma hn_sint_minus_1[sepref_fr_rules]:
  "hn_refine  (Mreturn (-1))  (sint_assn' TYPE('a::len)) (λ_. True) (RETURN$PR_CONST (sint_const TYPE('a) (-1)))"
  apply sepref_to_hoare unfolding sint_rel_def sint.rel_def in_br_conv by vcg
  
lemma hn_sint_numeral[sepref_fr_rules]:
  "numeral n  sints LENGTH('a)  
    hn_refine  (Mreturn (numeral n))  (sint_assn' TYPE('a::len)) (λ_. True) (RETURN$(PR_CONST (sint_const TYPE('a) (numeral n))))"
  apply sepref_to_hoare unfolding sint_rel_def sint.rel_def in_br_conv 
  apply vcg'
  by (auto simp: sbintrunc_mod2p min_sint_def max_sint_def ll_const_signed_aux)

lemma hn_sint_minus_numeral[sepref_fr_rules]:
  "-numeral n  sints LENGTH('a)  
    hn_refine  (Mreturn (-numeral n))  (sint_assn' TYPE('a::len)) (λ_. True) (RETURN$(PR_CONST (sint_const TYPE('a) (-numeral n))))"
  apply sepref_to_hoare unfolding sint_rel_def sint.rel_def in_br_conv 
  apply vcg'
  apply (auto simp: sbintrunc_mod2p min_sint_def max_sint_def ll_const_signed_aux)
  by (smt diff_Suc_less int_mod_eq' len_gt_0 neg_numeral_le_numeral power_strict_increasing_iff)

  
sepref_register 
  plus_int: "(+)::int_"    :: "int  int  int"
  minus_int: "(-)::int_"   :: "int  int  int"
  times_int: "(*)::int_"  :: "int  int  int"
  sdiv_int: "(sdiv)::int_" :: "int  int  int"
  smod_int: "(smod)::int_" :: "int  int  int"
  
sepref_register 
  eq_int: "(=)::int_"        :: "int  int  bool"
  op_neq_int: "op_neq::int_" :: "int  int  bool"
  lt_int: "(<)::int_"        :: "int  int  bool"
  le_int: "(≤)::int_"        :: "int  int  bool"
  
sepref_register    
  and_int: "(AND):: int  _"  
  or_int: "(OR):: int  _"  
  xor_int: "(XOR):: int  _"
  shiftr_int: "(<<) :: int  nat  int"
  shiftl_int: "(>>) :: int  nat  int"


thm sint_cmp_ops[THEN sint.hn_cmp_op, folded sint_rel_def, unfolded to_hfref_post]  
thm sint_bin_ops[THEN sint.hn_bin_op, folded sint_rel_def, unfolded to_hfref_post]  
  
lemma hn_sint_ops[sepref_fr_rules]:
  "(uncurry ll_add, uncurry (RETURN ∘∘ (+)))
     [λ(a, b). a + b  sints LENGTH('a)]a sint_assnk *a sint_assnk  sint_assn' TYPE('a::len)"
  "(uncurry ll_sub, uncurry (RETURN ∘∘ (-)))
     [λ(a, b). a - b  sints LENGTH('a)]a sint_assnk *a sint_assnk  sint_assn' TYPE('a::len)"
  "(uncurry ll_mul, uncurry (RETURN ∘∘ (*)))
     [λ(a, b). a * b  sints LENGTH('a)]a sint_assnk *a sint_assnk  sint_assn' TYPE('a::len)"
  "(uncurry ll_sdiv, uncurry (RETURN ∘∘ (sdiv)))
     [λ(a, b). b  0  a sdiv b  sints LENGTH('a)]a sint_assnk *a sint_assnk  sint_assn' TYPE('a::len)"
  "(uncurry ll_srem, uncurry (RETURN ∘∘ (smod)))
     [λ(a, b). b  0  a sdiv b  sints LENGTH('a)]a sint_assnk *a sint_assnk  sint_assn' TYPE('a::len)"
    
  "(uncurry ll_icmp_eq, uncurry (RETURN ∘∘ (=)))  sint_assnk *a sint_assnk a bool1_assn"
  "(uncurry ll_icmp_ne, uncurry (RETURN ∘∘ (op_neq)))  sint_assnk *a sint_assnk a bool1_assn"
  "(uncurry ll_icmp_sle, uncurry (RETURN ∘∘ (≤)))  sint_assnk *a sint_assnk a bool1_assn"
  "(uncurry ll_icmp_slt, uncurry (RETURN ∘∘ (<)))  sint_assnk *a sint_assnk a bool1_assn"
  unfolding op_neq_def
  using sint_bin_ops[THEN sint.hn_bin_op, folded sint_rel_def, unfolded to_hfref_post]
    and sint_cmp_ops[THEN sint.hn_cmp_op, folded sint_rel_def bool1_rel_def, unfolded to_hfref_post]
  apply simp_all
  done


      
definition [simp]: "sint_init TYPE('a::len)  0::int"

(* TODO: Add rule for 0 *)
lemma is_init_sint[sepref_gen_algo_rules]:
  "GEN_ALGO (sint_init TYPE('a::len)) (is_init (sint_assn' TYPE('a)))"
  unfolding GEN_ALGO_def sint_init_def is_init_def
  unfolding sint_rel_def sint.rel_def
  by (simp add: in_br_conv)
  
lemma is_init_sint0[sepref_gen_algo_rules]: 
  "GEN_ALGO (sint_const TYPE('a::len) 0) (is_init (sint_assn' TYPE('a)))"
  using is_init_sint[where 'a='a]
  by simp
  

subsubsection Natural Numbers by Unsigned Word

sepref_register 
  plus_nat: "(+)::nat_"    :: "nat  nat  nat"
  minus_nat: "(-)::nat_"   :: "nat  nat  nat"
  times_nat: "(*)::nat_"  :: "nat  nat  nat"
  div_nat: "(div)::nat_"   :: "nat  nat  nat"
  mod_nat: "(mod)::nat_"   :: "nat  nat  nat"
  
sepref_register 
  eq_nat: "(=)::nat_"        :: "nat  nat  bool"
  op_neq_nat: "op_neq::nat_" :: "nat  nat  bool"
  lt_nat: "(<)::nat_"        :: "nat  nat  bool"
  le_nat: "(≤)::nat_"        :: "nat  nat  bool"
  
sepref_register    
  and_nat: "(AND):: nat  _"  
  or_nat: "(OR):: nat  _"  
  xor_nat: "(XOR):: nat  _"  
  shiftr_nat: "(<<) :: nat  _  _"
  shiftl_nat: "(>>) :: nat  _  _"


definition unat_rel :: "('a::len word × nat) set" where "unat_rel  unat.rel"
abbreviation "unat_assn  pure unat_rel"  

abbreviation (input) "unat_rel' TYPE('a::len)  unat_rel :: ('a word × _) set"
abbreviation (input) "unat_assn' TYPE('a::len)  unat_assn :: _  'a word  _"


definition [simp]: "unat_const TYPE('a::len) c  (c::nat)"
context fixes c::nat begin
  sepref_register "unat_const TYPE('a::len) c" :: "nat"
end

lemma fold_unat:
  "0 = unat_const TYPE('a::len) 0"  
  "1 = unat_const TYPE('a::len) 1"  
  "numeral n  (unat_const TYPE('a::len) (numeral n))"
  by simp_all

  
lemma hn_unat_0[sepref_fr_rules]:
  "hn_refine  (Mreturn 0)  (unat_assn' TYPE('a::len)) (λ_. True) (RETURN$PR_CONST (unat_const TYPE('a) 0))"
  apply sepref_to_hoare
  unfolding unat_rel_def unat.rel_def in_br_conv
  apply vcg
  done
  
lemma hn_unat_1[sepref_fr_rules]:
  "hn_refine  (Mreturn 1)  (unat_assn' TYPE('a::len)) (λ_. True) (RETURN$PR_CONST (unat_const TYPE('a) 1))"
  apply sepref_to_hoare
  unfolding unat_rel_def unat.rel_def in_br_conv
  apply vcg
  done
  
  
lemma hn_unat_numeral[sepref_fr_rules]:
  "numeral n  unats LENGTH('a)  
    hn_refine  (Mreturn (numeral n))  (unat_assn' TYPE('a::len)) (λ_. True) (RETURN$(PR_CONST (unat_const TYPE('a) (numeral n))))"
  apply sepref_to_hoare unfolding unat_rel_def unat.rel_def in_br_conv 
  apply vcg' 
  by (metis id_apply max_unat_def mod_less of_nat_eq_id take_bit_eq_mod unat_bintrunc unsigned_numeral)

  
lemma hn_unat_ops[sepref_fr_rules]:
  "(uncurry ll_add, uncurry (RETURN ∘∘ (+)))  [λ(a, b). a + b < max_unat LENGTH('a)]a unat_assnk *a unat_assnk  unat_assn' TYPE('a::len)"
  "(λx. ll_add x 1, (RETURN  Suc))  [λa. Suc a < max_unat LENGTH('a)]a unat_assnk  unat_assn' TYPE('a)"
  "(uncurry ll_sub, uncurry (RETURN ∘∘ (-)))  [λ(a, b). b  a]a unat_assnk *a unat_assnk  unat_assn"
  "(uncurry ll_mul, uncurry (RETURN ∘∘ (*)))  [λ(a, b). a * b < max_unat LENGTH('a)]a unat_assnk *a unat_assnk  unat_assn' TYPE('a::len)"
  "(uncurry ll_udiv, uncurry (RETURN ∘∘ (div)))  [λ(a, b). b  0]a unat_assnk *a unat_assnk  unat_assn"
  "(uncurry ll_urem, uncurry (RETURN ∘∘ (mod)))  [λ(a, b). b  0]a unat_assnk *a unat_assnk  unat_assn"
  
  "(uncurry ll_and, uncurry (RETURN ∘∘ (AND)))  unat_assnk *a unat_assnk a unat_assn"
  "(uncurry ll_or, uncurry (RETURN ∘∘ (OR)))  unat_assnk *a unat_assnk a unat_assn"
  "(uncurry ll_xor, uncurry (RETURN ∘∘ (XOR)))  unat_assnk *a unat_assnk a unat_assn"
  
  "(uncurry ll_icmp_eq, uncurry (RETURN ∘∘ (=)))  unat_assnk *a unat_assnk a bool1_assn"
  "(uncurry ll_icmp_ne, uncurry (RETURN ∘∘ (op_neq)))  unat_assnk *a unat_assnk a bool1_assn"
  "(uncurry ll_icmp_ule, uncurry (RETURN ∘∘ (≤)))  unat_assnk *a unat_assnk a bool1_assn"
  "(uncurry ll_icmp_ult, uncurry (RETURN ∘∘ (<)))  unat_assnk *a unat_assnk a bool1_assn"  
  unfolding op_neq_def
  
  using unat_bin_ops[THEN unat.hn_bin_op, folded unat_rel_def]
    and unat_un_ops[THEN unat.hn_un_op, folded unat_rel_def]
    and unat_bin_ops_bitwise[THEN unat.hn_bin_op, folded unat_rel_def]
    and unat_cmp_ops[THEN unat.hn_cmp_op, folded unat_rel_def bool1_rel_def]
  by (simp_all add: prod_casesK)
  
definition [simp]: "unat_init TYPE('a::len)  0::nat"

lemma is_init_unat[sepref_gen_algo_rules]:
  "GEN_ALGO (unat_init TYPE('a::len)) (is_init (unat_assn' TYPE('a)))"
  unfolding GEN_ALGO_def unat_init_def is_init_def
  unfolding unat_rel_def unat.rel_def
  by (simp add: in_br_conv)
  
lemma is_init_unat0[sepref_gen_algo_rules]: 
  "GEN_ALGO (unat_const TYPE('a::len2) 0) (is_init (unat_assn' TYPE('a)))"
  using is_init_unat[where 'a='a]
  by simp

lemma exists_pure_conv:
  (x. ((x = a)) s) = s
  by (auto intro!: exI[of _ a] simp: pure_true_conv pred_lift_def)

lemma unat_distr_shr: "unat (ai >> k) = (unat ai >> k)"
  by (metis drop_bit_eq_div shiftr_div_2n' shiftr_def)

lemma bit_lshift_unat_assn[sepref_fr_rules]:
  (uncurry ll_lshr, uncurry (RETURN oo (>>)))  [λ(a,b). b < LENGTH('a)]a
    (unat_assn' TYPE('a::len2))k *a (unat_assn)k  (unat_assn)
  apply sepref_to_hoare
  unfolding ll_lshr_def op_lift_arith2_def Let_def
  apply (vcg)
  subgoal by (auto simp: shift_ovf_def unat_rel_def unat.rel_def word_to_lint_to_uint_conv in_br_conv)
  subgoal by (simp add: sep_algebra_simps bitLSHR'_def word_to_lint_to_uint_conv
        unat_rel_def unat.rel_def in_br_conv POSTCOND_def unat_distr_shr exists_pure_conv
        flip: word_to_lint_lshr)

  done

lemma unat_distr_shl:
  "unat a << k < max_unat LENGTH('l)  k < LENGTH('l)   unat (a << k) = unat (a::'l::len word) << k"
  apply (auto simp: shiftl_def push_bit_eq_mult)
  by (metis max_unat_def unat_mult_lem unat_power_lower)

lemma bit_shiftl_unat_assn[sepref_fr_rules]:
  (uncurry ll_shl, uncurry (RETURN oo (<<)))  [λ(a,b). b < LENGTH('a)  (a << b) < max_unat LENGTH('a)]a
    (unat_assn' TYPE('a::len2))k *a (unat_assn)k  (unat_assn)
proof -
  show ?thesis
    apply sepref_to_hoare
    unfolding ll_shl_def op_lift_arith2_def Let_def
    apply (vcg)
    subgoal by (auto simp: shift_ovf_def unat_rel_def unat.rel_def word_to_lint_to_uint_conv in_br_conv)
    subgoal apply (simp add: sep_algebra_simps bitSHL'_def word_to_lint_to_uint_conv
          unat_rel_def unat.rel_def in_br_conv POSTCOND_def unat_distr_shr exists_pure_conv unat_distr_shl
          flip: word_to_lint_shl)
      done
    done
qed

subsubsection Natural Numbers by Signed Word

definition snat_rel :: "('a::len2 word × nat) set" where "snat_rel  snat.rel"
abbreviation "snat_assn  pure snat_rel"  

abbreviation (input) "snat_rel' TYPE('a::len2)  snat_rel :: ('a word × _) set"
abbreviation (input) "snat_assn' TYPE('a::len2)  snat_assn :: _  'a word  _"

(* TODO: Too many snat_rel_ < max_snat lemma variants! *)
lemma snat_rel_range: "Range (snat_rel' TYPE('l)) = {0..<max_snat LENGTH('l::len2)}"
  (* TODO: Clean up proof! *)
  apply (auto simp: Range_iff snat_rel_def snat.rel_def in_br_conv)
  subgoal for x
    apply (rule exI[where x="word_of_int (int x)"])
    apply (auto simp: max_snat_def snat_invar_def)
    subgoal
      by (metis One_nat_def snat_eq_unat_aux1 snat_in_bounds_aux unat_of_nat_len)
    subgoal
      by (simp add: More_Word.of_nat_power not_msb_from_less)
    done
  done


definition [simp]: "snat_const TYPE('a::len2) c  (c::nat)"
context fixes c::nat begin
  sepref_register "snat_const TYPE('a::len2) c" :: "nat"
end


lemma fold_snat:
  "0 = snat_const TYPE('a::len2) 0"  
  "1 = snat_const TYPE('a::len2) 1"  
  "numeral n  (snat_const TYPE('a::len2) (numeral n))"
  by simp_all

(* TODO: Move, and use for proofs about snat in LLVM_Shallow_RS *)  
lemma snat_invar_0: "snat_invar (0)"  
  by (simp add: snat_invar_def)

lemma snat_invar_1: "snat_invar (1)"  
  by (simp add: snat_invar_def)
  
lemma snat_invar_numeral: " numeral a < max_snat LENGTH('a::len2)  
  snat_invar (numeral a::'a word)"
  by (metis (full_types) One_nat_def ll_const_signed_nat_aux2 max_snat_def snat_invar_def)
  
  
lemma hn_snat_0[sepref_fr_rules]:
  "hn_refine  (Mreturn 0)  (snat_assn' TYPE('a::len2)) (λ_. True) (RETURN$PR_CONST (snat_const TYPE('a) 0))"
  apply sepref_to_hoare
  unfolding snat_rel_def snat.rel_def in_br_conv
  supply [simp] = snat_invar_0
  apply vcg
  done
  
lemma hn_snat_1[sepref_fr_rules]:
  "hn_refine  (Mreturn 1)  (snat_assn' TYPE('a::len2)) (λ_. True) (RETURN$PR_CONST (snat_const TYPE('a) 1))"
  apply sepref_to_hoare
  unfolding snat_rel_def snat.rel_def in_br_conv
  supply [simp] = snat_invar_1
  apply vcg
  done
  
  
lemma hn_snat_numeral[sepref_fr_rules]:
  "numeral n  snats LENGTH('a)  
    hn_refine  (Mreturn (numeral n))  (snat_assn' TYPE('a::len2)) (λ_. True) (RETURN$(PR_CONST (snat_const TYPE('a) (numeral n))))"
  apply sepref_to_hoare unfolding snat_rel_def snat.rel_def in_br_conv 
  supply [simp] = snat_invar_numeral
  apply vcg'
  done
  
lemma hn_snat_ops[sepref_fr_rules]:
  "(uncurry ll_add, uncurry (RETURN ∘∘ (+)))  [λ(a, b). a + b < max_snat LENGTH('a)]a snat_assnk *a snat_assnk  snat_assn' TYPE('a::len2)"
  "(λx. ll_add x 1, (RETURN  Suc))  [λa. Suc a < max_snat LENGTH('a)]a snat_assnk  snat_assn' TYPE('a::len2)"
  "(uncurry ll_sub, uncurry (RETURN ∘∘ (-)))  [λ(a, b). b  a]a snat_assnk *a snat_assnk  snat_assn"
  "(uncurry ll_mul, uncurry (RETURN ∘∘ (*)))  [λ(a, b). a * b < max_snat LENGTH('a)]a snat_assnk *a snat_assnk  snat_assn' TYPE('a::len2)"
  "(uncurry ll_udiv, uncurry (RETURN ∘∘ (div)))  [λ(a, b). b  0]a snat_assnk *a snat_assnk  snat_assn"
  "(uncurry ll_urem, uncurry (RETURN ∘∘ (mod)))  [λ(a, b). b  0]a snat_assnk *a snat_assnk  snat_assn"
  
  "(uncurry ll_icmp_eq, uncurry (RETURN ∘∘ (=)))  snat_assnk *a snat_assnk a bool1_assn"
  "(uncurry ll_icmp_ne, uncurry (RETURN ∘∘ (op_neq)))  snat_assnk *a snat_assnk a bool1_assn"
  "(uncurry ll_icmp_sle, uncurry (RETURN ∘∘ (≤)))  snat_assnk *a snat_assnk a bool1_assn"
  "(uncurry ll_icmp_slt, uncurry (RETURN ∘∘ (<)))  snat_assnk *a snat_assnk a bool1_assn"  
  unfolding op_neq_def
  using snat_bin_ops[THEN snat.hn_bin_op, folded snat_rel_def]
    and snat_un_ops[THEN snat.hn_un_op, folded snat_rel_def]
    and snat_cmp_ops[THEN snat.hn_cmp_op, folded snat_rel_def bool1_rel_def]
  by simp_all
  
lemma exists_eq_star_conv: "(λs. (x. ((x = k) ∧* F) s)) = F"
  by (auto simp: sep_algebra_simps sep_conj_def pred_lift_extract_simps)

lemma bit_lshift_snat_assn[sepref_fr_rules]:
  (uncurry ll_lshr, uncurry (RETURN oo (>>)))  [λ(a,b). b < LENGTH('a)]a
    (snat_assn' TYPE('a::len2))k *a (snat_assn)k  (snat_assn)
  apply sepref_to_hoare
  unfolding ll_lshr_def op_lift_arith2_def Let_def
  apply (vcg)
  subgoal by (auto simp: shift_ovf_def snat_rel_def snat.rel_def word_to_lint_to_uint_conv in_br_conv snat_invar_alt snat_eq_unat_aux1)
  subgoal for b bi a ai F s
    apply (simp add: sep_algebra_simps bitLSHR'_def word_to_lint_to_uint_conv
        snat_rel_def unat.rel_def in_br_conv POSTCOND_def unat_distr_shr exists_pure_conv
        cnv_snat_to_uint(1)
        flip: word_to_lint_lshr snat_eq_unat_aux2)    

    apply (simp add: snat.rel_def in_br_conv)
    apply (auto simp add: snat_def snat_invar_alt)
    apply (subgoal_tac "nat (sint (ai >> unat bi)) = nat (sint ai) >> nat (sint bi)  unat (ai >> unat bi) < 2 ^ n")
    apply (auto simp: exists_eq_star_conv sep_empty_def)
    subgoal
      by (metis add_diff_cancel_left' nat_power_minus_less nat_uint_eq sint_eq_uint snat_invar_alt snat_invar_def unat_distr_shr unat_shiftr_less_t2n)
    subgoal 
      by (metis add_diff_cancel_left' nat_power_minus_less unat_shiftr_less_t2n)
    done
  done

lemma bit_shiftl_snat_assn[sepref_fr_rules]:
  (uncurry ll_shl, uncurry (RETURN oo (<<)))  [λ(a,b). b < LENGTH('a)  (a << b) < max_snat LENGTH('a)]a
    (snat_assn' TYPE('a::len2))k *a (snat_assn)k  (snat_assn)
proof -
  have H: nat (bi) < LENGTH('a :: len2) 
       nat (uint (ai :: 'a word) * 2 ^ nat (bi)) < max_unat LENGTH('a) 
       nat (bintrunc (size ai) (uint ai << nat (bi))) = nat (uint ai * 2 ^ nat (bi)) for bi ai
    by (smt (z3) max_unat_def mult.commute nat_mult_distrib nat_uint_eq push_bit_eq_mult shiftl_def 
      size_word.rep_eq uint_power_lower uint_word_arith_bintrs(3) unat_mult_lem zero_le_power)
  have H': nat (bi) < LENGTH('a :: len2) 
       nat (uint (ai :: 'a word) * 2 ^ nat (bi)) < max_snat LENGTH('a) 
       nat (bintrunc (size ai) (uint ai << nat (bi))) = nat (uint ai * 2 ^ nat (bi)) for bi ai
    using H[of bi ai] apply (auto simp: max_snat_def max_unat_def)
    using nat_less_numeral_power_cancel_iff snat_in_bounds_aux by blast

  show ?thesis
  proof (sepref_to_hoare, vcg)
    fix bi ai :: 'a word and  a b asf and s :: "llvm_val memory"
    assume
       le: b < LENGTH('a)  a << b < max_snat LENGTH('a) and
       a: (ai, a)  snat_rel and
       b: (bi, b)  snat_rel and
       state: STATE asf  s
    have nat (uint ai) << nat (uint bi) < 2 ^ (LENGTH('a) - Suc 0)
      using le a b
      apply (auto simp: snat_rel_def snat.rel_def in_br_conv) 
      apply (auto simp: max_snat_def snat_def snat_invar_alt)
      by (simp add: msb_unat_big sint_eq_uint)
    (*then have ‹(uint ai) << nat (uint bi) < 2 ^ (LENGTH('a) - Suc 0)›
      using le a b unfolding shiftr_int_def
      by (metis Groups.mult_ac(2) nat_eq_numeral_power_cancel_iff nat_less_numeral_power_cancel_iff nat_mult_distrib push_bit_eq_mult rel_simps(27) shiftl_def zero_le_power)
      *)
    then have le': ai << nat (uint bi) < 2 ^ (LENGTH('a) - Suc 0)
      using le 
      by (metis (mono_tags, lifting) Suc_0_lt_2p_len_of Suc_lessD 
        diff_Suc_less len_gt_0 
        len_not_eq_0 mult_0_right nat_uint_eq nat_zero_less_power_iff push_bit_eq_mult shiftl_def 
        snat_in_bounds_aux unat_2tp_if unat_mult_lem word_less_nat_alt)

    have [simp]: nat (bintrunc (size ai) (uint ai << nat (uint bi))) = nat (uint ai * 2 ^ nat (uint bi))
      using le a b 
      apply (auto simp: snat_rel_def snat.rel_def in_br_conv) 
      apply (auto simp: max_snat_def snat_def snat_invar_alt)
      by (smt (z3) H' One_nat_def diff_Suc_Suc diff_zero max_snat_def nat_mult_distrib nat_uint_eq 
          push_bit_eq_mult shiftl_def sint_eq_uint snat_invar_alt snat_invar_def uint_lt_0 
          uint_power_lower unat_2tp_if)
   have - (3 * 2 ^ (LENGTH('a) - Suc 0))  uint ai * 2 ^ nat (uint bi)
     by (smt int_nat_eq nat_mult_distrib of_nat_mult uint_add_ge0 zero_le_power)
   moreover have uint ai * 2 ^ nat (uint bi) < 3 * 2 ^ (LENGTH('a) - Suc 0)
     apply (subst nat_less_eq_zless[symmetric], simp, subst nat_mult_distrib)
     using le a b
     apply (auto simp: snat_rel_def snat.rel_def in_br_conv) 
     apply (auto simp: max_snat_def snat_def snat_invar_alt)
     by (smt (z3) shiftl_def Groups.mult_ac(2) One_nat_def Word.of_nat_unat nat (take_bit (size ai) (uint ai << nat (uint bi))) = nat (uint ai * 2 ^ nat (uint bi)) diff_Suc_1 le' le_less_trans lessI nat_less_numeral_power_cancel_iff nat_mult_distrib nat_power_eq nat_uint_eq nat_zero_less_power_iff not_le of_nat_numeral semiring_1_class.of_nat_power uint_power_lower uint_shiftl unat_arith_simps(2) unat_power_lower zero_less_nat_eq)
   moreover have ¬2 ^ (LENGTH('a) - Suc 0)  uint ai * 2 ^ nat (uint bi)
     using le
     apply (subst nat_le_eq_zle[symmetric], simp, subst nat_mult_distrib)
     using H'[of uint bi ai]  le a b
     by (auto simp: sint_uint word_size uint_shiftl sbintrunc_If
      shiftl_int_def max_snat_def max_unat_def snat_rel_def snat.rel_def br_def
      cnv_snat_to_uint(1) nat_power_eq nat_shiftr_div)
   moreover have ¬uint ai * 2 ^ nat (uint bi) < - (2 ^ (LENGTH('a) - Suc 0))
     apply (subst nat_less_eq_zless[symmetric], simp, subst nat_mult_distrib)
     using le a b
     by (auto simp: snat_rel_def snat.rel_def in_br_conv) 
   ultimately have nat (sint (ai << nat (uint bi))) = nat (uint ai * 2 ^ nat (uint bi))
     using H'[of uint bi ai]  le a b
     apply (auto simp: sint_uint word_size uint_shiftl sbintrunc_If shiftl_def
      shiftl_int_def max_snat_def max_unat_def snat_rel_def snat.rel_def)
     by (simp add: push_bit_eq_mult signed_take_bit_int_eq_self)
   have [simp]: ¬ msb (ai << nat (uint bi))
     apply (subst msb_shiftl_word[OF _])
     using le le' a b state
     unfolding snat_rel_def snat.rel_def br_def
     by (auto simp: br_def snat_def ll_shl_def wp_return
        op_lift_arith2_def Let_def shift_ovf_def word_to_lint_to_uint_conv bitSHL'_def
        nat_div_distrib nat_power_eq pred_lift_merge_simps sint_eq_uint max_snat_def
          cnv_snat_to_uint(1) in_br_conv snat.rel_def snat_invar_def
          POSTCOND_def STATE_extract(2) shiftr_div_2n 
       uint_shiftl exists_pure_conv)
   show wpa ( asf) (ll_shl ai bi)
         (λr s. EXTRACT (POSTCOND asf
               ((((ai, a)  snat_rel) ∧*
                 ((bi, b)  snat_rel) ∧*
                 True ∧*
                 (λs. x. (((r, x)  snat_rel) ∧* (x = a << b)) s))) s))
         s
     using le a b state
     unfolding snat_rel_def snat.rel_def br_def
     apply (auto simp: br_def snat_def ll_shl_def wpa_return
        op_lift_arith2_def Let_def shift_ovf_def word_to_lint_to_uint_conv bitSHL'_def
        nat_div_distrib nat_power_eq pred_lift_merge_simps sint_eq_uint max_snat_def
        cnv_snat_to_uint(1) in_br_conv snat.rel_def snat_invar_def
      simp flip: word_to_lint_shl nat_uint_eq)
     apply (simp_all add: POSTCOND_def STATE_extract EXTRACT_def shiftr_div_2n 
       uint_shiftl exists_pure_conv )
    
     apply (subgoal_tac "nat (take_bit (size ai) (uint ai << unat bi)) = unat ai << unat bi")
     apply (metis nat_uint_eq shiftl_def uint_shiftl)
     by (metis nat_uint_eq push_bit_eq_mult shiftl_def snat_in_bounds_aux uint_shiftl unat_mult_lem unat_power_lower)
  qed
qed


definition [simp]: "snat_init TYPE('a::len)  0::nat"

lemma is_init_snat[sepref_gen_algo_rules]:
  "GEN_ALGO (snat_init TYPE('a::len2)) (is_init (snat_assn' TYPE('a)))"
  unfolding GEN_ALGO_def snat_init_def is_init_def
  unfolding snat_rel_def snat.rel_def
  by (simp add: snat_invar_0 in_br_conv)
  
lemma is_init_snat0[sepref_gen_algo_rules]: 
  "GEN_ALGO (snat_const TYPE('a::len2) 0) (is_init (snat_assn' TYPE('a)))"
  using is_init_snat[where 'a='a]
  by simp

subsubsection Ad-Hoc Method to Annotate Number Constructors  
lemma annot_num_const_cong: 
  "a b. snat_const a b = snat_const a b" 
  "a b. sint_const a b = sint_const a b" 
  "a b. unat_const a b = unat_const a b" 
  "ASSERT Φ = ASSERT Φ"
  "WHILEIT I = WHILEIT I"
  by simp_all
  
lemma unat_const_fold: 
  "0 = unat_const TYPE('a::len) 0"
  "1 = unat_const TYPE('a::len) 1"
  "numeral n = unat_const TYPE('a::len) (numeral n)"
  by simp_all
  
lemma snat_const_fold: 
  "0 = snat_const TYPE('a::len2) 0"
  "1 = snat_const TYPE('a::len2) 1"
  "numeral n = snat_const TYPE('a::len2) (numeral n)"
  by simp_all

lemma sint_const_fold: 
  "0 = sint_const TYPE('a::len) 0"
  "1 = sint_const TYPE('a::len) 1"
  "numeral n = sint_const TYPE('a::len) (numeral n)"
  "-sint_const TYPE('a::len) c = sint_const TYPE('a::len) (-c)"
  by simp_all
  
    
lemma hfref_absfun_convI: "CNV g g'  (f,g')  hfref P C A R CP  (f,g)  hfref P C A R CP" by simp

method annot_sint_const for T::"'a::len itself" = 
  (rule hfref_absfun_convI),
  (simp only: sint_const_fold[where 'a='a] cong: annot_num_const_cong),
  (rule CNV_I)
  
method annot_snat_const for T::"'a::len2 itself" = 
  (rule hfref_absfun_convI),
  (simp only: snat_const_fold[where 'a='a] cong: annot_num_const_cong),
  (rule CNV_I)
  
method annot_unat_const for T::"'a::len itself" = 
  (rule hfref_absfun_convI),
  (simp only: unat_const_fold[where 'a='a] cong: annot_num_const_cong),
  (rule CNV_I)
  
  
subsubsection Casting  
(* TODO: Add other casts *)
  
context fixes T :: "'a::len2 itself" begin
  definition [simp]: "unat_snat_upcast_aux  let _=TYPE('a) in id::natnat"

  sepref_decl_op unat_snat_upcast: "unat_snat_upcast_aux" :: "nat_rel  nat_rel" .
end  

context fixes T :: "'a::len itself" begin
  definition [simp]: "snat_unat_downcast_aux  let _=TYPE('a) in id::natnat"

  sepref_decl_op snat_unat_downcast: "snat_unat_downcast_aux" :: "nat_rel  nat_rel" .
end  

context fixes T :: "'a::len2 itself" begin
  definition [simp]: "snat_snat_upcast_aux  let _=TYPE('a) in id::natnat"

  sepref_decl_op snat_snat_upcast: "snat_snat_upcast_aux" :: "nat_rel  nat_rel" .

  definition [simp]: "snat_snat_downcast_aux  let _=TYPE('a) in id::natnat"

  sepref_decl_op snat_snat_downcast: "snat_snat_downcast_aux" :: "nat_rel  nat_rel" .
  
end

context fixes T :: "'a::len itself" begin
  definition [simp]: "unat_unat_upcast_aux  let _=TYPE('a) in id::natnat"
  definition [simp]: "unat_unat_downcast_aux  let _=TYPE('a) in id::natnat"

  sepref_decl_op unat_unat_upcast: "unat_unat_upcast_aux" :: "nat_rel  nat_rel" .
  sepref_decl_op unat_unat_downcast: "unat_unat_downcast_aux" :: "nat_rel  nat_rel" .
end

sepref_decl_op unat_snat_conv: "id::nat_" :: "nat_rel  nat_rel" .
sepref_decl_op snat_unat_conv: "id::nat_" :: "nat_rel  nat_rel" .


lemma annot_unat_snat_upcast: "x = op_unat_snat_upcast TYPE('l::len2) x" by simp 
lemma annot_snat_unat_downcast: "x = op_snat_unat_downcast TYPE('l::len) x" by simp 
lemma annot_snat_snat_upcast: "x = op_snat_snat_upcast TYPE('l::len2) x" by simp 
lemma annot_snat_snat_downcast: "x = op_snat_snat_downcast TYPE('l::len2) x" by simp 
lemma annot_unat_snat_conv: "x = op_unat_snat_conv x" by simp 
lemma annot_unat_unat_upcast: "x = op_unat_unat_upcast TYPE('l::len) x" by simp 
lemma annot_unat_unat_downcast: "x = op_unat_unat_downcast TYPE('l::len) x" by simp 
lemma annot_snat_unat_conv: "x = op_snat_unat_conv x" by simp  

lemma in_unat_rel_conv_assn: "((xi, x)  unat_rel) = unat.assn x xi"
  by (auto simp: unat_rel_def unat.assn_is_rel pure_app_eq)

lemma in_snat_rel_conv_assn: "((xi, x)  snat_rel) = snat.assn x xi"
  by (auto simp: snat_rel_def snat.assn_is_rel pure_app_eq)

context fixes BIG :: "'big::len2" and SMALL :: "'small::len" begin  
  lemma unat_snat_upcast_refine: 
    "(unat_snat_upcast TYPE('big::len2), PR_CONST (mop_unat_snat_upcast TYPE('big::len2)))  [λ_. is_up' UCAST('small  'big)]a (unat_assn' TYPE('small::len))k  snat_assn"
    supply [simp] = in_unat_rel_conv_assn in_snat_rel_conv_assn
    apply sepref_to_hoare
    apply simp
    by vcg'
  
  sepref_decl_impl (ismop) unat_snat_upcast_refine fixes 'big 'small by simp
  
  
  lemma snat_unat_downcast_refine: 
    "(snat_unat_downcast TYPE('small), PR_CONST (mop_snat_unat_downcast TYPE('small))) 
       [λx. is_down' UCAST('big  'small)  x<max_unat LENGTH('small)]a (snat_assn' TYPE('big))k  unat_assn"
    supply [simp] = in_unat_rel_conv_assn in_snat_rel_conv_assn
    apply sepref_to_hoare
    apply simp
    by vcg'
  
  sepref_decl_impl (ismop) snat_unat_downcast_refine fixes 'big 'small by simp
end

context fixes BIG :: "'big::len2" and SMALL :: "'small::len2" begin  
  lemma snat_snat_upcast_refine: 
    "(snat_snat_upcast TYPE('big::len2), PR_CONST (mop_snat_snat_upcast TYPE('big::len2)))  [λ_. is_up' UCAST('small  'big)]a (snat_assn' TYPE('small::len2))k  snat_assn"
    supply [simp] = in_unat_rel_conv_assn in_snat_rel_conv_assn
    apply sepref_to_hoare
    apply simp
    by vcg'
  
  sepref_decl_impl (ismop) snat_snat_upcast_refine fixes 'big 'small by simp
  
  lemma snat_snat_downcast_refine: 
    "(snat_snat_downcast TYPE('small), PR_CONST (mop_snat_snat_downcast TYPE('small))) 
       [λx. is_down' UCAST('big  'small)  x<max_snat LENGTH('small)]a (snat_assn' TYPE('big))k  snat_assn"
    supply [simp] = in_unat_rel_conv_assn in_snat_rel_conv_assn
    apply sepref_to_hoare
    apply simp
    by vcg'
  
  sepref_decl_impl (ismop) snat_snat_downcast_refine fixes 'big 'small by simp
  
end

context fixes BIG :: "'big::len" and SMALL :: "'small::len" begin  
  lemma unat_unat_upcast_refine: 
    "(unat_unat_upcast TYPE('big), PR_CONST (mop_unat_unat_upcast TYPE('big)))  [λ_. is_up' UCAST('small  'big)]a (unat_assn' TYPE('small::len))k  unat_assn"
    supply [simp] = in_unat_rel_conv_assn
    apply sepref_to_hoare
    apply simp
    by vcg'
  
  sepref_decl_impl (ismop) unat_unat_upcast_refine fixes 'big 'small by simp
  
  lemma unat_unat_downcast_refine: 
    "(unat_unat_downcast TYPE('small), PR_CONST (mop_unat_unat_downcast TYPE('small))) 
       [λx. is_down' UCAST('big  'small)  x<max_unat LENGTH('small)]a (unat_assn' TYPE('big::len))k  unat_assn"
    supply [simp] = in_unat_rel_conv_assn
    apply sepref_to_hoare
    apply simp
    by vcg'
  
  sepref_decl_impl (ismop) unat_unat_downcast_refine fixes 'big 'small by simp
end

  
context fixes T::"'l::len2" begin
  lemma unat_snat_conv_refine: "(λx. x, op_unat_snat_conv) 
     [λx. x<max_snat LENGTH('l::len2)]f unat_rel' TYPE('l)  snat_rel' TYPE('l)"
    by (force 
      intro!: frefI 
      simp: snat_rel_def unat_rel_def snat.rel_def unat.rel_def
      simp: in_br_conv max_snat_def snat_invar_alt
      simp: snat_eq_unat(1)
      )
      
  sepref_decl_impl unat_snat_conv_refine[sepref_param] fixes 'l by auto
  
  lemma snat_unat_conv_refine: "(λx. x, op_snat_unat_conv)
     snat_rel' TYPE('l)  unat_rel' TYPE('l)"
    by (force
      intro!: frefI
      simp: snat_rel_def unat_rel_def snat.rel_def unat.rel_def
      simp: in_br_conv max_snat_def snat_invar_alt
      simp: snat_eq_unat(1)
      )

  sepref_decl_impl snat_unat_conv_refine[sepref_param] fixes 'l .
end


text Converting to Word
sepref_register "of_nat :: _  _ word "
lemma of_nat_word_refine[sepref_import_param]: 
  "(id,of_nat)  unat_rel' TYPE('a::len)  word_rel"
  by (auto simp: unat_rel_def unat.rel_def in_br_conv)



subsubsection Bit-Shifting

sepref_register 
  shl_word: "(<<):: _ word  _"  
  lshr_word: "(>>):: _ word  _"  
  ashr_word: "(>>>):: _ word  _"  

context begin

interpretation llvm_prim_arith_setup .
  
lemma shl_hnr_unat[sepref_fr_rules]: "(uncurry ll_shl,uncurry (RETURN oo (<<)))  [λ(a,b). b < LENGTH('a)]a (word_assn :: 'a::len word  _)k *a unat_assnk  word_assn"
  unfolding unat_rel_def unat.assn_is_rel[symmetric] unat.assn_def
  apply sepref_to_hoare
  by vcg'

lemma lshr_hnr_unat[sepref_fr_rules]: "(uncurry ll_lshr,uncurry (RETURN oo (>>)))  [λ(a,b). b < LENGTH('a)]a (word_assn :: 'a::len word  _)k *a unat_assnk  word_assn"
  unfolding unat_rel_def unat.assn_is_rel[symmetric] unat.assn_def
  apply sepref_to_hoare
  by vcg'

lemma ashr_hnr_unat[sepref_fr_rules]: "(uncurry ll_ashr,uncurry (RETURN oo (>>>)))  [λ(a,b). b < LENGTH('a)]a (word_assn :: 'a::len word  _)k *a unat_assnk  word_assn"
  unfolding unat_rel_def unat.assn_is_rel[symmetric] unat.assn_def
  apply sepref_to_hoare
  by vcg'

lemma shl_hnr_snat[sepref_fr_rules]: "(uncurry ll_shl,uncurry (RETURN oo (<<)))  [λ(a,b). b < LENGTH('a)]a (word_assn :: 'a::len2 word  _)k *a snat_assnk  word_assn"
  unfolding snat_rel_def snat.assn_is_rel[symmetric] snat.assn_def
  supply [simp] = snat_eq_unat
  apply sepref_to_hoare
  by vcg'
  
lemma lshr_hnr_snat[sepref_fr_rules]: "(uncurry ll_lshr,uncurry (RETURN oo (>>)))  [λ(a,b). b < LENGTH('a)]a (word_assn :: 'a::len2 word  _)k *a snat_assnk  word_assn"
  unfolding snat_rel_def snat.assn_is_rel[symmetric] snat.assn_def
  supply [simp] = snat_eq_unat
  apply sepref_to_hoare
  by vcg'

lemma ashr_hnr_snat[sepref_fr_rules]: "(uncurry ll_ashr,uncurry (RETURN oo (>>>)))  [λ(a,b). b < LENGTH('a)]a (word_assn :: 'a::len2 word  _)k *a snat_assnk  word_assn"
  unfolding snat_rel_def snat.assn_is_rel[symmetric] snat.assn_def
  supply [simp] = snat_eq_unat
  apply sepref_to_hoare
  by vcg'
  
      
end

subsubsection Bounds Solver Setup


lemma in_unat_rel_boundsD[sepref_bounds_dest]: "(w, n)  unat_rel' TYPE('l)  n < max_unat LENGTH('l::len)"
  by (simp add: unat_rel_def unat.rel_def in_br_conv)

(*lemma snat_rel_imp_less_max_snat: 
  "⟦(x,n)∈snat_rel' TYPE('l::len2); L = LENGTH('l)⟧ ⟹ n<max_snat L"
  by (auto simp: snat_rel_def snat.rel_def in_br_conv)
*)
  
lemma in_snat_rel_boundsD[sepref_bounds_dest]: 
  "(w, n)  snat_rel' TYPE('l)  n < max_snat LENGTH('l::len2)"
  by (auto simp: snat_rel_def snat.rel_def in_br_conv)
  
lemma in_sint_rel_boundsD[sepref_bounds_dest]: 
  "(w,i)sint_rel' TYPE('l::len)  min_sint LENGTH('l)  i  i < max_sint LENGTH('l)"
  by (auto simp: sint_rel_def sint.rel_def in_br_conv)
  
lemmas [sepref_bounds_simps] = max_snat_def max_unat_def max_sint_def min_sint_def
  
subsection Default Inlinings
lemmas [llvm_inline] = id_def

subsection HOL Combinators

subsubsection If

lemma CP_simp_join_triv: "CP_simplify (CP_JOIN CP1 CP2) (λr. CP1 r  CP2 r)"
  unfolding CP_defs by simp

lemma hn_if_aux:
  assumes P: "Γ  hn_val bool1_rel a a' ** Γ1"
  assumes RT: "a  hn_refine (hn_val bool1_rel a a' ** Γ1) b' Γ2b R CP1 b"
  assumes RE: "¬a  hn_refine (hn_val bool1_rel a a' ** Γ1) c' Γ2c R CP2 c"
  assumes MERGE: "MERGE Γ2b fb Γ2c fc Γ'"
  assumes CP_JOIN: "CP_simplify (CP_JOIN CP1 CP2) CP'"
  shows "hn_refine Γ 
    (llc_if a' (doM {rb'; fb; Mreturn r}) (doM {rc'; fc; Mreturn r})) 
    Γ' R CP' (if a then b else c)"
  apply (rule hn_refine_nofailI)  
  apply (rule hn_refine_cons_pre[OF P])
proof (cases a, goal_cases)
  assume NF: "nofail (if a then b else c)"
  
  have [vcg_normalize_simps, named_ss fri_prepare_simps]: "hn_val bool1_rel = bool.assn"
    unfolding bool1_rel_def bool.assn_is_rel hn_ctxt_def ..
  
  note [vcg_rules] = MERGED[OF MERGE]  
    
  from CP_JOIN have [simp]: 
    "CP1 r  CP' r"
    "CP2 r  CP' r"
    for r
    unfolding CP_defs by auto
  
  {
    case [simp]: 1
    from NF have [simp]: "nofail b" by simp
  
    note [vcg_rules] = RT[THEN hn_refineD, simplified]
  
    show ?case by rule vcg
  }
  {
    case [simp]: 2
    from NF have [simp]: "nofail c" by simp
  
    note [vcg_rules] = RE[THEN hn_refineD, simplified]
  
    show ?case by rule vcg
  }  
qed    


lemma hn_if[sepref_comb_rules]:
  assumes P: "Γ  hn_val bool1_rel a a' ** Γ1"
  assumes RT: "a  hn_refine (hn_val bool1_rel a a' ** Γ1) b' Γ2b R CP1 b"
  assumes RE: "¬a  hn_refine (hn_val bool1_rel a a' ** Γ1) c' Γ2c R CP2 c"
  assumes MERGE: "TERM If  MERGE Γ2b fb Γ2c fc Γ'"
  assumes CP_JOIN: "CP_simplify (CP_JOIN CP1 CP2) CP'"
  shows "hn_refine Γ 
    (llc_if a' (doM {rb'; fb; Mreturn r}) (doM {rc'; fc; Mreturn r})) 
    Γ' R CP' (If$a$b$c)"
  using P RT RE MERGE[OF TERMI] CP_JOIN
  unfolding APP_def PROTECT2_def 
  by (rule hn_if_aux)


subsubsection While  
(* TODO: Move WHILE-stuff to HOL-Bindings Theory *)
lemma WHILEIT_pat[def_pat_rules]:
  "WHILEIT$I  UNPROTECT (WHILEIT I)"
  "WHILET  PR_CONST (WHILEIT (λ_. True))"
  by (simp_all add: WHILET_def)

lemma id_WHILEIT[id_rules]: 
  "PR_CONST (WHILEIT I) ::i TYPE(('a  bool)  ('a  'a nres)  'a  'a nres)"
  by simp

lemma WHILE_arities[sepref_monadify_arity]:
  (*"WHILET ≡ WHILEIT$(λ2_. True)"*)
  "PR_CONST (WHILEIT I)  λ2b f s. SP (PR_CONST (WHILEIT I))$(λ2s. b$s)$(λ2s. f$s)$s"
  by (simp_all add: WHILET_def)

lemma WHILEIT_comb[sepref_monadify_comb]:
  "PR_CONST (WHILEIT I)$(λ2x. b x)$f$s  
    Refine_Basic.bind$(EVAL$s)$(λ2s. 
      SP (PR_CONST (monadic_WHILEIT I))$(λ2x. (EVAL$(b x)))$f$s
    )"
  by (simp_all add: WHILEIT_to_monadic)
  
lemma monadic_WHILEIT_pat[def_pat_rules]:
  "monadic_WHILEIT$I  UNPROTECT (monadic_WHILEIT I)"
  by auto  
    
lemma id_monadic_WHILEIT[id_rules]: 
  "PR_CONST (monadic_WHILEIT I) ::i TYPE(('a  bool nres)  ('a  'a nres)  'a  'a nres)"
  by simp
    
lemma monadic_WHILEIT_arities[sepref_monadify_arity]:
  "PR_CONST (monadic_WHILEIT I)  λ2b f s. SP (PR_CONST (monadic_WHILEIT I))$(λ2s. b$s)$(λ2s. f$s)$s"
  by (simp)

lemma monadic_WHILEIT_comb[sepref_monadify_comb]:
  "PR_CONST (monadic_WHILEIT I)$b$f$s  
    Refine_Basic.bind$(EVAL$s)$(λ2s. 
      SP (PR_CONST (monadic_WHILEIT I))$b$f$s
    )"
  by (simp)
  
  
lemma hn_refine_add_invalid: (* Very customized rule for manual derivation of while *)
  "hn_refine (hn_ctxt Rs a b ** Γ) c Γ' R CP m  hn_refine (hn_ctxt Rs a b ** Γ) c (hn_invalid Rs a b ** Γ') R CP m"
  by (smt hn_refine_frame' invalidate_clone' sep_conj_commute sep_conj_left_commute)
  
lemma hn_monadic_WHILE_aux:
  assumes FR: "P  hn_ctxt Rs s' s0 ** Γ"
  assumes b_ref: "s s'. I s'  hn_refine 
    (hn_ctxt Rs s' s ** Γ)
    (b s)
    (Γb s' s)
    (pure bool1_rel)
    (CP_ignore s)
    (b' s')"
  assumes b_fr: "s' s. Γb s' s  hn_ctxt Rs s' s ** Γ"

  assumes f_ref: "s' s. I s'  hn_refine
    (hn_ctxt Rs s' s ** Γ)
    (f s)
    (Γf s' s)
    Rs
    (CP s)
    (f' s')"
  assumes f_fr: "s' s. Γf s' s  hn_ctxt Rsf s' s ** Γ"
  assumes free: "MK_FREE Rsf fr"
  (*assumes PREC: "precise Rs"*)
  shows "hn_refine (P) (llc_while b (λs. doM {r  f s; fr s; Mreturn r}) s0) (hn_invalid Rs s' s0 ** Γ) Rs (CP** s0) (monadic_WHILEIT I b' f' s')"
  apply1 (rule hn_refine_cons_pre[OF FR])
  apply (rule hn_refine_add_invalid)
  
  apply (rule hn_refine_synthI)
  unfolding monadic_WHILEIT_def
  focus (rule hnr_RECT_cp[where F'="λs' s. Γ" and Ry=Rs and C="CP** s0"])
    apply1 (rule hnr_ASSERT)
    focus (rule hn_refine_cons_cp_only)
      
      focus (rule hnr_bind_manual_free)
        applyS (rule b_ref; simp)
        apply1 (rule hn_refine_cons_pre, sep_drule b_fr, rule entails_refl)
        focus (rule hn_if_aux[OF _ _ _ MERGE_triv CP_simp_join_triv])
          apply (fri_rotate entails_pre_cong :-1) apply (rule conj_entails_mono[OF entails_refl]) apply (rule entails_refl)
          focus (* Then-Part *)
            apply1 (rule hn_refine_cons_pre, sep_drule drop_hn_val, simp, rule entails_refl)
            apply (rule hnr_bind_manual_free)
            applyS (rule f_ref, simp)
            apply1 (rule hn_refine_cons_pre, sep_drule f_fr, simp, rule entails_refl)
            apply (rule hnr_freeI[OF free])
            apply (drule (1) rtranclp.rtrancl_into_rtrancl)
            apply (rule hn_refine_cons_pre[rotated], assumption)
            applyS (simp add: sep_conj_c; rule entails_refl)
            solved
          focus (* Else-Part *)  
            apply (rule hn_refine_cons_post)
            apply (rule hn_refine_frame[OF hnr_RETURN_pass])
            apply (fri_rotate entails_pre_cong :1) apply (rule entails_refl)
            apply1 (sep_drule drop_hn_invalid)
            apply1 (sep_drule drop_hn_val)
            apply (simp)
            solved
            
        solved
      solved
      applyS (meson r_into_rtranclp rtranclp.rtrancl_refl rtranclp_trans)
    solved  
    focus apply pf_mono_prover solved
    applyS blast
    solved
  subgoal by (simp add: llc_while_def Mwhile_def llc_if_def cong: if_cong)
  subgoal ..
  subgoal ..
  done

lemmas [CP_simps] = APP_def[abs_def]  
  
lemma hn_monadic_WHILE_lin[sepref_comb_rules]:
  assumes "INDEP Rs"
  assumes FR: "P  hn_ctxt Rs s' s ** Γ"
  assumes b_ref: "s s'. I s'  hn_refine 
    (hn_ctxt Rs s' s ** Γ)
    (b s)
    (Γb s' s)
    (pure bool1_rel)
    (CP_ignore s)
    (b' s')"
  assumes b_fr: "s' s. TERM (monadic_WHILEIT,''cond'')  Γb s' s  hn_ctxt Rs s' s ** Γ"

  assumes f_ref: "s' s. I s'  hn_refine
    (hn_ctxt Rs s' s ** Γ)
    (f s)
    (Γf s' s)
    Rs
    (CP s)
    (f' s')"
  assumes f_fr: "s' s. TERM (monadic_WHILEIT,''body'')  Γf s' s  hn_ctxt Rsf s' s ** Γ"
  assumes CP_simp: "s. CP_simplify (CP_RPT CP s) (CP' s)"
  assumes free: "TERM (monadic_WHILEIT,''free-old-state'')  MK_FREE Rsf fr"
  shows "hn_refine 
    P 
    (llc_while b (λs. doM {r  f s; fr s; Mreturn r}) s) 
    (hn_invalid Rs s' s ** Γ)
    Rs 
    (CP'$s)
    (PR_CONST (monadic_WHILEIT I)$(λ2s'. b' s')$(λ2s'. f' s')$(s'))"
  apply (rule hn_refine_cons_cp_only)  
  using assms(2-6) free
  unfolding APP_def PROTECT2_def CONSTRAINT_def PR_CONST_def
  apply (rule hn_monadic_WHILE_aux)
  apply (assumption | rule TERMI)+
  using CP_simp unfolding CP_defs by blast

  
subsubsection Let
lemma hn_let[sepref_comb_rules]:
  "hn_refine Γ c Γ' R CP (Refine_Basic.bind$(PASS$v)$(λ2x. f x))  hn_refine Γ c Γ' R CP (Let$v$(λ2x. f x))" 
  by simp
    
subsection Unit

lemma unit_hnr[sepref_import_param]: "((),())unit_rel" by auto
  
  
subsection "Product"


lemmas [sepref_import_rewrite, named_ss sepref_frame_normrel, fcomp_norm_unfold] = prod_assn_pure_conv[symmetric]


(* TODO Add corresponding rules for other types and add to datatype snippet *)
lemma intf_of_prod_assn[intf_of_assn]:
  assumes "intf_of_assn A TYPE('a)" "intf_of_assn B TYPE('b)"
  shows "intf_of_assn (prod_assn A B) TYPE('a * 'b)"
  by simp

lemma pure_prod[constraint_rules]: 
  assumes P1: "is_pure P1" and P2: "is_pure P2"
  shows "is_pure (prod_assn P1 P2)"
proof -
  from P1 obtain P1' where P1': "x x'. P1 x x' = (P1' x x')"
    using is_pureE by blast
  from P2 obtain P2' where P2': "x x'. P2 x x' = (P2' x x')"
    using is_pureE by blast

  show ?thesis proof
    fix x x'
    show "prod_assn P1 P2 x x' =
          (case (x, x') of ((a1, a2), c1, c2)  P1' a1 c1  P2' a2 c2)"
      unfolding prod_assn_def
      apply (simp add: P1' P2' sep_algebra_simps split: prod.split)
      done
  qed
qed

lemma prod_frame_match[sepref_frame_match_rules]:
  assumes "hn_ctxt A (fst x) (fst y)  hn_ctxt A' (fst x) (fst y)"
  assumes "hn_ctxt B (snd x) (snd y)  hn_ctxt B' (snd x) (snd y)"
  shows "hn_ctxt (prod_assn A B) x y  hn_ctxt (prod_assn A' B') x y"
  apply (cases x; cases y; simp)
  apply (simp add: hn_ctxt_def)
  apply (rule conj_entails_mono)
  using assms apply (auto simp: hn_ctxt_def)
  done

lemma prod_frame_merge[sepref_frame_merge_rules]:
  assumes "MERGE1 A frl1 A' frr1 Am"  
  assumes "MERGE1 B frl2 B' frr2 Bm"  
  shows "MERGE1 
    (prod_assn A B) (λ(a,b). doM {frl1 a; frl2 b}) 
    (prod_assn A' B') (λ(a,b). doM {frr1 a; frr2 b}) 
    (prod_assn Am Bm)"
  supply [vcg_rules] = MERGE1D[OF assms(1)] MERGE1D[OF assms(2)]
  by rule vcg
    
  

lemma entt_invalid_prod: "hn_invalid (prod_assn A B) p p'  hn_ctxt (prod_assn (invalid_assn A) (invalid_assn B)) p p'"
  unfolding hn_ctxt_def invalid_assn_def prod_assn_def
  by (auto split: prod.splits simp: entails_def pred_lift_extract_simps dest: pure_part_split_conj)

lemma gen_merge_cons_left: "LL'  MERGE L' fl R fr M  MERGE L fl R fr M"  
  unfolding MERGE_def 
  by (metis (mono_tags, lifting) cons_rule[where Q=Q and Q'=Q for Q] entails_def)
  
lemma gen_merge_cons_right: "RR'  MERGE L fl R' fr M  MERGE L fl R fr M"  
  unfolding MERGE_def
  by (metis (mono_tags, lifting) cons_rule[where Q=Q and Q'=Q for Q] entails_def)
  
lemmas gen_merge_cons = gen_merge_cons_left gen_merge_cons_right

lemmas invalid_prod_merge[sepref_frame_merge_rules] = gen_merge_cons[OF entt_invalid_prod]

lemma prod_assn_ctxt: "prod_assn A1 A2 x y = z  hn_ctxt (prod_assn A1 A2) x y = z"
  by (simp add: hn_ctxt_def)

(* TODO: Move *)  
lemma drop_pureD: "is_pure A  hn_ctxt A a b  "
  by (auto simp: is_pure_def entails_def pred_lift_extract_simps hn_ctxt_def)
  
lemma hn_case_prod_aux:
  assumes FR: "Γ  hn_ctxt (prod_assn P1 P2) p' p ** Γ1"
  assumes Pair: "a1 a2 a1' a2'. p'=(a1',a2'); CP_assm (p=(a1,a2)) 
     hn_refine (hn_ctxt P1 a1' a1 ** hn_ctxt P2 a2' a2 ** Γ1 ** hn_invalid (prod_assn P1 P2) p' p) (f a1 a2) 
          (hn_ctxt P1' a1' a1 ** hn_ctxt P2' a2' a2 ** hn_ctxt XX1 p' p ** Γ1') (R a1' a2' a1 a2) (CP a1 a2) (f' a1' a2')"
  assumes PURE: "Sepref_Basic.is_pure XX1"
  shows "hn_refine Γ (case_prod f p) (hn_ctxt (prod_assn P1' P2') p' p ** Γ1')
    (R (fst p') (snd p') (fst p) (snd p)) (CP_SPLIT CP p) (case_prod f' p')" (is "?G Γ")
    apply1 (rule hn_refine_cons_pre[OF FR])
    apply1 extract_hnr_invalids
    apply1 (cases p; cases p'; simp add: prod_assn_pair_conv[THEN prod_assn_ctxt])
    apply (rule hn_refine_cons_cp[OF _ Pair _ entails_refl])
    applyS (simp add: hn_ctxt_def)
    applyS simp
    applyS (simp add: CP_defs)
    subgoal
      using PURE apply (sep_drule drop_pureD[OF PURE])
      by (simp add: hn_ctxt_def sep_conj_c)
    applyS (simp add: CP_defs)
    done
  
    
(* TODO: This has caused "ENTER MATCH" unifier problems with flex-flex pairs. So disabled by default,
  and hn_case_prod_simple' is enabled, where the result cannot depend on the elements of the pair. *)    
lemma hn_case_prod':
  assumes FR: "Γ  hn_ctxt (prod_assn P1 P2) p' p ** Γ1"
  assumes Pair: "a1 a2 a1' a2'. p'=(a1',a2'); CP_assm (p=(a1,a2)) 
     hn_refine (hn_ctxt P1 a1' a1 ** hn_ctxt P2 a2' a2 ** Γ1 ** hn_invalid (prod_assn P1 P2) p' p) (f a1 a2) 
          (Γ2 a1 a2 a1' a2') (R a1' a2' a1 a2) (CP a1 a2) (f' a1' a2')"
  assumes FR2: "a1 a2 a1' a2'. Γ2 a1 a2 a1' a2'  hn_ctxt P1' a1' a1 ** hn_ctxt P2' a2' a2 ** hn_ctxt XX1 p' p ** Γ1'"        
  assumes PURE: "CONSTRAINT Sepref_Basic.is_pure XX1"
  shows "hn_refine Γ (case_prod f p) (hn_ctxt (prod_assn P1' P2') p' p ** Γ1')
    (R (fst p') (snd p') (fst p) (snd p)) (CP_SPLIT CP p) (case_prod$(λ2a b. f' a b)$p')" (is "?G Γ")
    unfolding autoref_tag_defs PROTECT2_def
    apply (rule hn_case_prod_aux[OF _ hn_refine_cons_post])
    apply fact
    apply fact
    using FR2 apply blast
    using PURE by simp

lemma hn_case_prod_simple'[sepref_comb_rules]:
  assumes FR: "Γ  hn_ctxt (prod_assn P1 P2) p' p ** Γ1"
  assumes Pair: "a1 a2 a1' a2'. p'=(a1',a2'); CP_assm (p=(a1,a2)) 
     hn_refine (hn_ctxt P1 a1' a1 ** hn_ctxt P2 a2' a2 ** Γ1 ** hn_invalid (prod_assn P1 P2) p' p) (f a1 a2) 
          (Γ2 a1 a2 a1' a2') R (CP a1 a2) (f' a1' a2')"
  assumes FR2: "a1 a2 a1' a2'. Γ2 a1 a2 a1' a2'  hn_ctxt P1' a1' a1 ** hn_ctxt P2' a2' a2 ** hn_ctxt XX1 p' p ** Γ1'"        
  assumes PURE: "CONSTRAINT Sepref_Basic.is_pure XX1"
  shows "hn_refine Γ (case_prod f p) (hn_ctxt (prod_assn P1' P2') p' p ** Γ1')
    R (CP_SPLIT CP p) (case_prod$(λ2a b. f' a b)$p')" (is "?G Γ")
    unfolding autoref_tag_defs PROTECT2_def
    apply (rule hn_case_prod_aux[OF _ hn_refine_cons_post])
    apply fact
    apply fact
    using FR2 apply blast
    using PURE by simp
    
    
lemma hn_Pair[sepref_fr_rules]: "
  (uncurry (Mreturn oo Pair), uncurry (RETURN oo Pair))  [λ_. True]c Ad *a Bd  A×aB [λ(x1,x2) r. r=(x1,x2)]c"
  by sepref_to_hoare vcg
    
(*
lemma fst_hnr[sepref_fr_rules]: "(Mreturn o fst,RETURN o fst) ∈ (prod_assn A B)da A"
  by sepref_to_hoare vcg
lemma snd_hnr[sepref_fr_rules]: "(Mreturn o snd,RETURN o snd) ∈ (prod_assn A B)da B"
  by sepref_to_hoare sep_auto
*)

lemmas [constraint_simps] = prod_assn_pure_conv
lemmas [sepref_import_param] = param_prod_swap

lemma rdomp_prodD[dest!]: "rdomp (prod_assn A B) (a,b)  rdomp A a  rdomp B b"
  unfolding rdomp_def prod_assn_def
  by (auto simp: sep_conj_def)

subsection Option  

   
lemma option_patterns[def_pat_rules]: 
  "(=)$x$None  is_None$x"
  "(=)$None$x  is_None$x"
  "op_neq$x$None  Not$(is_None$x)"
  "op_neq$None$x  Not$(is_None$x)"
  apply (all rule eq_reflection)
  by (auto split: option.splits)

  
text Option type via unused implementation value  
locale dflt_option =   
  fixes dflt and A :: "'a  'c::llvm_rep  assn" and is_dflt
  assumes UU: "A a dflt = sep_false"
  assumes CMP: "llvm_htriple  (is_dflt k) (λr. bool.assn (k=dflt) r)"
begin
  
  definition "option_assn a c  if c=dflt then (a=None) else EXS aa. (a=Some aa) ** A aa c"
  
  lemma hn_None[sepref_fr_rules]: "(uncurry0 (Mreturn dflt), uncurry0 (RETURN None))  unit_assnk a option_assn"  
    apply sepref_to_hoare unfolding option_assn_def 
    apply vcg'
    done
  
  lemma hn_Some[sepref_fr_rules]: "(Mreturn, RETURN o Some)  Ad a option_assn"  
    apply sepref_to_hoare
    subgoal for a c
      apply (cases "c=dflt")
      using UU apply simp
      unfolding option_assn_def
      apply vcg
      done
    done
  
  lemma hn_the[sepref_fr_rules]: "(Mreturn, RETURN o the)  [λx. x  None]a option_assnd  A"
    apply sepref_to_hoare
    unfolding option_assn_def 
    apply clarsimp
    apply vcg'
    done
    
  lemma hn_is_None[sepref_fr_rules]: "(is_dflt, RETURN o is_None)  option_assnk a bool1_assn"
    unfolding bool1_rel_def bool.assn_is_rel[symmetric]
    apply sepref_to_hoare
    unfolding option_assn_def 
    apply clarsimp
    supply CMP[vcg_rules]
    apply vcg'
    done
    
  definition [llvm_inline]: "free_option fr c  doM { dis_dflt c; llc_if d (Mreturn ()) (fr c) }"
  
  lemma mk_free_option[sepref_frame_free_rules]:
    assumes [THEN MK_FREED, vcg_rules]: "MK_FREE A fr"  
    shows "MK_FREE option_assn (free_option fr)"
    apply rule
    unfolding free_option_def option_assn_def
    apply clarsimp
    supply CMP[vcg_rules]
    apply vcg
    done
    
  lemma option_assn_pure[safe_constraint_rules]:
    assumes "is_pure A" 
    shows "is_pure option_assn"  
  proof -
    from assms obtain P where [simp]: "A = (λa c. (P a c))"
      unfolding is_pure_def by blast
  
    show ?thesis  
      apply (rule is_pureI[where P'="λa c. if c=dflt then a=None else aa. a=Some aa  P aa c"])
      unfolding option_assn_def
      by (auto simp: sep_algebra_simps pred_lift_extract_simps)
      
  qed    
    
    
end    

lemmas [named_ss llvm_pre_simp cong] = refl[of "dflt_option.free_option _"]


locale dflt_pure_option = dflt_option +
  assumes A_pure[safe_constraint_rules]: "is_pure A"
begin
  find_theorems MK_FREE is_pure

  lemma A_free[sepref_frame_free_rules]: "MK_FREE A (λ_. Mreturn ())"
    by (rule mk_free_is_pure[OF A_pure])

end  

(* TODO: Redundancies with dflt_option *)
(* TODO: Setup id-op phase to identify those operations *)
text Option type via unused implementation value, own set of operations.  
locale dflt_option_private =   
  fixes dflt and A :: "'a  'c::llvm_rep  assn" and is_dflt
  assumes UU: "A a dflt = sep_false"
  assumes CMP: "llvm_htriple  (is_dflt k) (λr. bool.assn (k=dflt) r)"
begin
  
  definition "option_assn a c  if c=dflt then (a=None) else EXS aa. (a=Some aa) ** A aa c"

  definition None where [simp]: "None  Option.None"
  definition Some where [simp]: "Some  Option.Some"
  definition the where [simp]: "the  Option.the"
  definition is_None where [simp]: "is_None  Autoref_Bindings_HOL.is_None"
  
  lemmas fold_None = None_def[symmetric]
  lemmas fold_Some = Some_def[symmetric]
  lemmas fold_the = the_def[symmetric]
  lemmas fold_is_None = is_None_def[symmetric]
  
  lemma fold_is_None2: 
    "a = None  is_None a"
    "None = a  is_None a"
    by (auto simp: is_None_def None_def split: option.split)
  
  lemmas fold_option = fold_None fold_Some fold_the fold_is_None fold_is_None2
  
  sepref_register None Some the is_None
  
    
  lemma hn_None[sepref_fr_rules]: "(uncurry0 (Mreturn dflt), uncurry0 (RETURN None))  unit_assnk a option_assn"  
    apply sepref_to_hoare unfolding option_assn_def None_def
    apply vcg'
    done
  
  lemma hn_Some[sepref_fr_rules]: "(Mreturn, RETURN o Some)  Ad a option_assn"  
    apply sepref_to_hoare
    subgoal for a c
      apply (cases "c=dflt")
      using UU apply simp
      unfolding option_assn_def Some_def
      apply vcg
      done
    done
  
  lemma hn_the[sepref_fr_rules]: "(Mreturn, RETURN o the)  [λx. x  Option.None]a option_assnd  A"
    apply sepref_to_hoare
    unfolding option_assn_def the_def
    apply clarsimp
    apply vcg'
    done
    
  lemma hn_is_None[sepref_fr_rules]: "(is_dflt, RETURN o is_None)  option_assnk a bool1_assn"
    unfolding bool1_rel_def bool.assn_is_rel[symmetric]
    apply sepref_to_hoare
    unfolding option_assn_def is_None_def
    apply clarsimp
    supply CMP[vcg_rules]
    apply vcg'
    done
    
  definition [llvm_inline]: "free_option fr c  doM { dis_dflt c; llc_if d (Mreturn ()) (fr c) }"
    
  lemma mk_free_option[sepref_frame_free_rules]:
    assumes [THEN MK_FREED, vcg_rules]: "MK_FREE A fr"  
    shows "MK_FREE option_assn (free_option fr)"
    apply rule
    unfolding free_option_def option_assn_def
    apply clarsimp
    supply CMP[vcg_rules]
    apply vcg
    done
    
  lemma option_assn_pure[safe_constraint_rules]:
    assumes "is_pure A" 
    shows "is_pure option_assn"  
  proof -
    from assms obtain P where [simp]: "A = (λa c. (P a c))"
      unfolding is_pure_def by blast
  
    show ?thesis  
      apply (rule is_pureI[where P'="λa c. if c=dflt then a=Option.None else aa. a=Option.Some aa  P aa c"])
      unfolding option_assn_def
      by (auto simp: sep_algebra_simps pred_lift_extract_simps)
      
  qed    
    
    
end    

lemmas [named_ss llvm_pre_simp cong] = refl[of "dflt_option_private.free_option _"]


locale dflt_pure_option_private = dflt_option_private +
  assumes A_pure[safe_constraint_rules]: "is_pure A"
begin
  lemma A_free[sepref_frame_free_rules]: "MK_FREE A (λ_. Mreturn ())"
    by (rule mk_free_is_pure[OF A_pure])

end  



interpretation snat: dflt_pure_option "-1" snat_assn "ll_icmp_eq (-1)"
  apply unfold_locales
  subgoal
    apply (auto simp: snat_rel_def pure_def pred_lift_extract_simps del: ext intro!: ext)
    apply (auto simp: snat.rel_def in_br_conv snat_invar_def)
    done
  subgoal proof goal_cases
    case 1
    interpret llvm_prim_arith_setup .
    show ?case
      unfolding bool.assn_def
      apply vcg'
      done
    qed
  subgoal by simp  
  done

abbreviation snat_option_assn' :: "'a itself  nat option  'a::len2 word  llvm_amemory  bool" where
  "snat_option_assn' _  snat.option_assn"
  
  
subsection Additional Operations  

text Additional operations, for which we need the basic framework already set up.
  
subsubsection Subtraction that Saturates at 0 on Underflow  
  
definition op_nat_sub_ovf :: "nat  nat  nat" where "op_nat_sub_ovf a b  if ab then 0 else a-b"
lemma op_nat_sub_ovf_is_sub[simp]: "op_nat_sub_ovf = (-)"
  unfolding op_nat_sub_ovf_def by (auto split: if_split del: ext intro!: ext)

lemma fold_nat_sub_ovf: "(-) = op_nat_sub_ovf" by simp
  
sepref_definition snat_sub_ovf_impl [llvm_inline] is "uncurry (RETURN oo op_nat_sub_ovf)" 
  :: "(snat_assn' TYPE('l::len2))k *a (snat_assn' TYPE('l::len2))k a snat_assn' TYPE('l::len2)"
  unfolding op_nat_sub_ovf_def 
  apply (annot_snat_const "TYPE('l)")
  by sepref
  
declare snat_sub_ovf_impl.refine[sepref_fr_rules]
  


subsection Ad-Hoc Regression Tests  
  
sepref_definition example1 is "λx. doN {ASSERT (x{-10..10});
    RETURN (x<5  x2  x-2  0)}" :: "(sint_assn' TYPE(7))k a (bool1_assn)" 
  apply (annot_sint_const "TYPE(7)")
  apply sepref
  done

sepref_definition example2 is "λx. doN {ASSERT (x{-10..10}); RETURN (x+(-1) * (7 smod 15) - 3 sdiv 2)}" :: "(sint_assn' TYPE(7))k a (sint_assn' TYPE(7))" 
  apply (annot_sint_const "TYPE(7)")
  apply sepref
  done

sepref_definition example1n is "λx. doN {ASSERT (x{2..10});
    RETURN (x<5  x2  x-2  0)}" :: "(snat_assn' TYPE(7))k a (bool1_assn)" 
  apply (annot_snat_const "TYPE(7)")
  apply sepref
  done

sepref_definition example2n is "λx. doN {ASSERT (x{5..10}); RETURN ((x-1) * (7 mod 15) - 3 div 2)}" 
  :: "(snat_assn' TYPE(7))k a (snat_assn' TYPE(7))" 
  apply (annot_snat_const "TYPE(7)")
  apply sepref
  done
  
      
lemmas [llvm_code] = example1_def example2_def example1n_def example2n_def  
  
llvm_deps example1 example2 example1n example2n

export_llvm example1 example2 example1n example2n
  

definition example3_abs :: "'a::len word  'a word  'a word nres" where "example3_abs a b  do {
    (a,b)  WHILET (λ(a,b). ab) (λ(a,b). if a<b then RETURN (a,b-a) else RETURN (a-b,b)) (a,b);
    RETURN a
  }"

sepref_definition example3 is "uncurry example3_abs" :: "word_assnk *a word_assnk a word_assn"
  unfolding example3_abs_def
  apply sepref_dbg_keep
  done

definition example3n_abs :: "nat  nat  nat nres" where "example3n_abs a b  do {
    (a,b)  WHILET (λ(a,b). ab) (λ(a,b). if a<b then RETURN (a,b-a) else RETURN (a-b,b)) (a,b);
    RETURN a
  }"

sepref_definition example3n is "uncurry example3n_abs" :: "(snat_assn' TYPE(32))k *a (snat_assn' TYPE(32))k a (snat_assn' TYPE(32))"
  unfolding example3n_abs_def
  apply sepref_dbg_keep
  done
  
  
    
lemmas [llvm_code] = example3_def example3n_def  
export_llvm
  "example3 :: 32 word  _"
  "example3 :: 64 word  _"
  "example3n"


sepref_definition example4n is "λx. do {
       x  RETURN (x >> 1);
       ASSERT ((x << 1) < max_snat 7);
       RETURN ((x << 1) > x)
   }" :: "(snat_assn' TYPE(7))k a (bool1_assn)" 
  apply (annot_snat_const "TYPE(7)")
  apply sepref_dbg_keep
  done

lemmas [llvm_code] = example4n_def

llvm_deps example4n

export_llvm example4n

(* TODO: Characters as i8 *)  
  
end