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.›
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)) ∈ A⇧d→⇩aA"
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 ≡ R⊆Id"
lemma [safe_constraint_rules]:
"IS_ID Id"
"IS_ID R1 ⟹ IS_ID R2 ⟹ IS_ID (R1 → R2)"
"IS_ID R ⟹ IS_ID (⟨R⟩option_rel)"
"IS_ID R ⟹ IS_ID (⟨R⟩list_rel)"
"IS_ID R1 ⟹ IS_ID R2 ⟹ IS_ID (R1 ×⇩r R2)"
"IS_ID R1 ⟹ IS_ID R2 ⟹ IS_ID (⟨R1,R2⟩sum_rel)"
by (auto simp: IS_ID_def)
lemma [safe_constraint_rules]:
"IS_BELOW_ID Id"
"IS_BELOW_ID R ⟹ IS_BELOW_ID (⟨R⟩option_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,R2⟩sum_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: "R1⊇Id ⟹ 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 (⟨R⟩list_rel)"
unfolding IS_BELOW_ID_def
proof safe
fix l l'
assume A: "R⊆Id"
assume "(l,l')∈⟨R⟩list_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]: "(A→B)¯ = A¯→B¯"
by (auto dest: fun_relD)
lemma inv_option_rel_eq[simp]: "(⟨K⟩option_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,Q⟩sum_rel)¯ = ⟨P¯,Q¯⟩sum_rel"
by (auto simp: sum_rel_def)
lemma inv_list_rel_eq[simp]: "(⟨R⟩list_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›
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,R2⟩sum_rel)"
"IS_LEFT_UNIQUE R ⟹ IS_LEFT_UNIQUE (⟨R⟩option_rel)"
"IS_LEFT_UNIQUE R ⟹ IS_LEFT_UNIQUE (⟨R⟩list_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,R2⟩sum_rel)"
"IS_LEFT_TOTAL R ⟹ IS_LEFT_TOTAL (⟨R⟩option_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 (⟨R⟩list_rel)"
unfolding IS_LEFT_TOTAL_alt
proof safe
assume A: "∀x.∃y. (x,y)∈R"
fix l
show "∃l'. (l,l')∈⟨R⟩list_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,R2⟩sum_rel)"
"IS_RIGHT_TOTAL R ⟹ IS_RIGHT_TOTAL (⟨R⟩option_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 (⟨R⟩list_rel)"
unfolding IS_RIGHT_TOTAL_alt
proof safe
assume A: "∀x.∃y. (y,x)∈R"
fix l
show "∃l'. (l',l)∈⟨R⟩list_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 (A→B)"
"IS_RIGHT_TOTAL A ⟹ IS_RIGHT_UNIQUE B ⟹ IS_RIGHT_UNIQUE (A→B)"
"IS_LEFT_UNIQUE A ⟹ IS_LEFT_TOTAL B ⟹ IS_LEFT_TOTAL (A→B)"
"IS_LEFT_TOTAL A ⟹ IS_LEFT_UNIQUE B ⟹ IS_LEFT_UNIQUE (A→B)"
apply (simp_all add: prop2p rel2p)
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›
lemma param_distinct[param]: "⟦IS_LEFT_UNIQUE A; IS_RIGHT_UNIQUE A⟧ ⟹ (distinct, distinct) ∈ ⟨A⟩list_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×⇩rB⟩set_rel → ⟨A⟩set_rel → ⟨B⟩set_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: "((=),(=))∈K→K→bool_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 ≡ ((=), (=))∈R→R→bool_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)
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
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)
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]
abbreviation nbn_rel :: "nat ⇒ (nat × nat) set"
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 \<^term>‹init::'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_assn⇧k → 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_assn⇧k *⇩a sepref_assn⇧k → 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_assn⇧k *⇩a sepref_assn⇧k →⇩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 ≡ a≠b"
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. ›
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_assn⇧k *⇩a bool1_assn⇧k →⇩a bool1_assn"
"(uncurry ll_or, uncurry (RETURN ∘∘ (∨))) ∈ bool1_assn⇧k *⇩a bool1_assn⇧k →⇩a bool1_assn"
"(uncurry ll_xor, uncurry (RETURN ∘∘ (op_neq))) ∈ bool1_assn⇧k *⇩a bool1_assn⇧k →⇩a bool1_assn"
"(ll_not1, RETURN ∘ Not) ∈ bool1_assn⇧k →⇩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_assn⇧k *⇩a bool1_assn⇧k →⇩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"
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_assn⇧k →⇩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). d≠0]⇩a word_assn⇧k *⇩a word_assn⇧k → word_assn"
"(uncurry (ll_urem),uncurry (RETURN oo (mod))) ∈ [λ(_,d). d≠0]⇩a word_assn⇧k *⇩a word_assn⇧k → word_assn"
"(uncurry (ll_sdiv),uncurry (RETURN oo (sdiv))) ∈ [λ(c,d). d≠0 ∧ in_srange (sdiv) c d]⇩a word_assn⇧k *⇩a word_assn⇧k → word_assn"
"(uncurry (ll_srem),uncurry (RETURN oo (smod))) ∈ [λ(c,d). d≠0 ∧ in_srange (sdiv) c d]⇩a word_assn⇧k *⇩a word_assn⇧k → 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_assn⇧k *⇩a word_assn⇧k →⇩a bool1_assn"
"(uncurry (ll_icmp_ne), uncurry (RETURN oo (op_neq))) ∈ word_assn⇧k *⇩a word_assn⇧k →⇩a bool1_assn"
"(uncurry (ll_icmp_ult), uncurry (RETURN oo (<))) ∈ word_assn⇧k *⇩a word_assn⇧k →⇩a bool1_assn"
"(uncurry (ll_icmp_ule), uncurry (RETURN oo (≤))) ∈ word_assn⇧k *⇩a word_assn⇧k →⇩a bool1_assn"
"(uncurry (ll_icmp_slt), uncurry (RETURN oo (λa b. a <s b))) ∈ word_assn⇧k *⇩a word_assn⇧k →⇩a bool1_assn"
"(uncurry (ll_icmp_sle), uncurry (RETURN oo (λa b. a <=s b))) ∈ word_assn⇧k *⇩a word_assn⇧k →⇩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_assn⇧k *⇩a sint_assn⇧k → sint_assn' TYPE('a::len)"
"(uncurry ll_sub, uncurry (RETURN ∘∘ (-)))
∈ [λ(a, b). a - b ∈ sints LENGTH('a)]⇩a sint_assn⇧k *⇩a sint_assn⇧k → sint_assn' TYPE('a::len)"
"(uncurry ll_mul, uncurry (RETURN ∘∘ (*)))
∈ [λ(a, b). a * b ∈ sints LENGTH('a)]⇩a sint_assn⇧k *⇩a sint_assn⇧k → sint_assn' TYPE('a::len)"
"(uncurry ll_sdiv, uncurry (RETURN ∘∘ (sdiv)))
∈ [λ(a, b). b ≠ 0 ∧ a sdiv b ∈ sints LENGTH('a)]⇩a sint_assn⇧k *⇩a sint_assn⇧k → sint_assn' TYPE('a::len)"
"(uncurry ll_srem, uncurry (RETURN ∘∘ (smod)))
∈ [λ(a, b). b ≠ 0 ∧ a sdiv b ∈ sints LENGTH('a)]⇩a sint_assn⇧k *⇩a sint_assn⇧k → sint_assn' TYPE('a::len)"
"(uncurry ll_icmp_eq, uncurry (RETURN ∘∘ (=))) ∈ sint_assn⇧k *⇩a sint_assn⇧k →⇩a bool1_assn"
"(uncurry ll_icmp_ne, uncurry (RETURN ∘∘ (op_neq))) ∈ sint_assn⇧k *⇩a sint_assn⇧k →⇩a bool1_assn"
"(uncurry ll_icmp_sle, uncurry (RETURN ∘∘ (≤))) ∈ sint_assn⇧k *⇩a sint_assn⇧k →⇩a bool1_assn"
"(uncurry ll_icmp_slt, uncurry (RETURN ∘∘ (<))) ∈ sint_assn⇧k *⇩a sint_assn⇧k →⇩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"
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_assn⇧k *⇩a unat_assn⇧k → unat_assn' TYPE('a::len)"
"(λx. ll_add x 1, (RETURN ∘ Suc)) ∈ [λa. Suc a < max_unat LENGTH('a)]⇩a unat_assn⇧k → unat_assn' TYPE('a)"
"(uncurry ll_sub, uncurry (RETURN ∘∘ (-))) ∈ [λ(a, b). b ≤ a]⇩a unat_assn⇧k *⇩a unat_assn⇧k → unat_assn"
"(uncurry ll_mul, uncurry (RETURN ∘∘ (*))) ∈ [λ(a, b). a * b < max_unat LENGTH('a)]⇩a unat_assn⇧k *⇩a unat_assn⇧k → unat_assn' TYPE('a::len)"
"(uncurry ll_udiv, uncurry (RETURN ∘∘ (div))) ∈ [λ(a, b). b ≠ 0]⇩a unat_assn⇧k *⇩a unat_assn⇧k → unat_assn"
"(uncurry ll_urem, uncurry (RETURN ∘∘ (mod))) ∈ [λ(a, b). b ≠ 0]⇩a unat_assn⇧k *⇩a unat_assn⇧k → unat_assn"
"(uncurry ll_and, uncurry (RETURN ∘∘ (AND))) ∈ unat_assn⇧k *⇩a unat_assn⇧k →⇩a unat_assn"
"(uncurry ll_or, uncurry (RETURN ∘∘ (OR))) ∈ unat_assn⇧k *⇩a unat_assn⇧k →⇩a unat_assn"
"(uncurry ll_xor, uncurry (RETURN ∘∘ (XOR))) ∈ unat_assn⇧k *⇩a unat_assn⇧k →⇩a unat_assn"
"(uncurry ll_icmp_eq, uncurry (RETURN ∘∘ (=))) ∈ unat_assn⇧k *⇩a unat_assn⇧k →⇩a bool1_assn"
"(uncurry ll_icmp_ne, uncurry (RETURN ∘∘ (op_neq))) ∈ unat_assn⇧k *⇩a unat_assn⇧k →⇩a bool1_assn"
"(uncurry ll_icmp_ule, uncurry (RETURN ∘∘ (≤))) ∈ unat_assn⇧k *⇩a unat_assn⇧k →⇩a bool1_assn"
"(uncurry ll_icmp_ult, uncurry (RETURN ∘∘ (<))) ∈ unat_assn⇧k *⇩a unat_assn⇧k →⇩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 ⇒ _"
lemma snat_rel_range: "Range (snat_rel' TYPE('l)) = {0..<max_snat LENGTH('l::len2)}"
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
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_assn⇧k *⇩a snat_assn⇧k → snat_assn' TYPE('a::len2)"
"(λx. ll_add x 1, (RETURN ∘ Suc)) ∈ [λa. Suc a < max_snat LENGTH('a)]⇩a snat_assn⇧k → snat_assn' TYPE('a::len2)"
"(uncurry ll_sub, uncurry (RETURN ∘∘ (-))) ∈ [λ(a, b). b ≤ a]⇩a snat_assn⇧k *⇩a snat_assn⇧k → snat_assn"
"(uncurry ll_mul, uncurry (RETURN ∘∘ (*))) ∈ [λ(a, b). a * b < max_snat LENGTH('a)]⇩a snat_assn⇧k *⇩a snat_assn⇧k → snat_assn' TYPE('a::len2)"
"(uncurry ll_udiv, uncurry (RETURN ∘∘ (div))) ∈ [λ(a, b). b ≠ 0]⇩a snat_assn⇧k *⇩a snat_assn⇧k → snat_assn"
"(uncurry ll_urem, uncurry (RETURN ∘∘ (mod))) ∈ [λ(a, b). b ≠ 0]⇩a snat_assn⇧k *⇩a snat_assn⇧k → snat_assn"
"(uncurry ll_icmp_eq, uncurry (RETURN ∘∘ (=))) ∈ snat_assn⇧k *⇩a snat_assn⇧k →⇩a bool1_assn"
"(uncurry ll_icmp_ne, uncurry (RETURN ∘∘ (op_neq))) ∈ snat_assn⇧k *⇩a snat_assn⇧k →⇩a bool1_assn"
"(uncurry ll_icmp_sle, uncurry (RETURN ∘∘ (≤))) ∈ snat_assn⇧k *⇩a snat_assn⇧k →⇩a bool1_assn"
"(uncurry ll_icmp_slt, uncurry (RETURN ∘∘ (<))) ∈ snat_assn⇧k *⇩a snat_assn⇧k →⇩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 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›
context fixes T :: "'a::len2 itself" begin
definition [simp]: "unat_snat_upcast_aux ≡ let _=TYPE('a) in id::nat⇒nat"
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::nat⇒nat"
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::nat⇒nat"
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::nat⇒nat"
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::nat⇒nat"
definition [simp]: "unat_unat_downcast_aux ≡ let _=TYPE('a) in id::nat⇒nat"
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_assn⇧k → 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_assn⇧k → 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_assn⇧k → 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_assn⇧k → 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_assn⇧k → 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_assn⇧k → 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 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 CP⇩1 CP⇩2) (λr. CP⇩1 r ∨ CP⇩2 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 CP⇩1 b"
assumes RE: "¬a ⟹ hn_refine (hn_val bool1_rel a a' ** Γ1) c' Γ2c R CP⇩2 c"
assumes MERGE: "MERGE Γ2b fb Γ2c fc Γ'"
assumes CP_JOIN: "CP_simplify (CP_JOIN CP⇩1 CP⇩2) CP'"
shows "hn_refine Γ
(llc_if a' (doM {r←b'; fb; Mreturn r}) (doM {r←c'; 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]:
"CP⇩1 r ⟹ CP' r"
"CP⇩2 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 CP⇩1 b"
assumes RE: "¬a ⟹ hn_refine (hn_val bool1_rel a a' ** Γ1) c' Γ2c R CP⇩2 c"
assumes MERGE: "TERM If ⟹ MERGE Γ2b fb Γ2c fc Γ'"
assumes CP_JOIN: "CP_simplify (CP_JOIN CP⇩1 CP⇩2) CP'"
shows "hn_refine Γ
(llc_if a' (doM {r←b'; fb; Mreturn r}) (doM {r←c'; 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›
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]:
"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:
"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' s⇩0 ** Γ"
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"
shows "hn_refine (P) (llc_while b (λs. doM {r ← f s; fr s; Mreturn r}) s⇩0) (hn_invalid Rs s' s⇩0 ** Γ) Rs (CP⇧*⇧* s⇩0) (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⇧*⇧* s⇩0"])
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
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
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]
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: "L⊢L' ⟹ 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: "R⊢R' ⟹ 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)
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
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 A⇧d *⇩a B⇧d → A×⇩aB [λ(x⇩1,x⇩2) r. r=(x⇩1,x⇩2)]⇩c"
by sepref_to_hoare vcg
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_assn⇧k →⇩a option_assn"
apply sepref_to_hoare unfolding option_assn_def
apply vcg'
done
lemma hn_Some[sepref_fr_rules]: "(Mreturn, RETURN o Some) ∈ A⇧d →⇩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_assn⇧d → 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_assn⇧k →⇩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 { d←is_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
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_assn⇧k →⇩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) ∈ A⇧d →⇩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_assn⇧d → 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_assn⇧k →⇩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 { d←is_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 a≤b 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 ∧ x≠2 ⟶ 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 ∧ x≠2 ⟶ 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). a≠b) (λ(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_assn⇧k *⇩a word_assn⇧k →⇩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). a≠b) (λ(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
end