Theory PhiSem_CF_Basic
chapter ‹Basic Control Flow›
theory PhiSem_CF_Basic
imports PhiSem_Generic_Boolean "HOL-Library.While_Combinator"
begin
section ‹Instructions›
subsection ‹Non-Branching Selection›
definition op_sel :: "TY ⇒ (VAL × VAL × VAL, VAL) proc'"
where "op_sel TY =
φM_caseV (λvc. φM_caseV (λva vb.
φM_getV 𝖻𝗈𝗈𝗅 sem_dest_bool vc (λc.
φM_getV TY id va (λa.
φM_getV TY id vb (λb.
Return (φarg (if c then a else b)))))))"
subsection ‹Branch›
definition op_if :: "'ret proc
⇒ 'ret proc
⇒ (VAL,'ret) proc'"
where "op_if brT brF v =
φM_getV 𝖻𝗈𝗈𝗅 sem_dest_bool v (λc. (if c then brT else brF))"
subsection ‹While Loop›
inductive SemDoWhile :: "VAL proc ⇒ resource ⇒ unit comp ⇒ bool" where
"Success (φarg (sem_mk_bool False)) res ∈ f s ⟹ SemDoWhile f s (Success (φarg ()) res)"
| "Success (φarg (sem_mk_bool True)) res ∈ f s ⟹ SemDoWhile f res s'' ⟹ SemDoWhile f s s''"
| "Abnormal v e ∈ f s ⟹ SemDoWhile f s (Abnormal v e)"
| "NonTerm ∈ f s ⟹ SemDoWhile f s NonTerm"
| "AssumptionBroken ∈ f s ⟹ SemDoWhile f s AssumptionBroken"
| "Invalid ∈ f s ⟹ SemDoWhile f s Invalid"
lemma "∄ y. SemDoWhile ((λres. Return (φarg (sem_mk_bool True)) res) :: VAL proc) res y"
apply rule apply (elim exE) subgoal for y
apply (induct "((λres. Return (φarg (sem_mk_bool True)) (res::resource)) :: VAL proc)" res y
rule: SemDoWhile.induct)
apply (simp_all add: Return_def det_lift_def) . .
definition op_do_while :: " VAL proc ⇒ unit proc"
where "op_do_while f s = Collect (SemDoWhile f s)"
subsection ‹Recursion›
inductive SemRec :: "(('a,'b) proc' ⇒ ('a,'b) proc')
⇒ 'a φarg ⇒ resource ⇒ 'b comp set ⇒ bool"
where
SemRec_I0: "(⋀g. F g x res = y) ⟹ SemRec F x res y"
| SemRec_IS: "SemRec (F o F) x res y ⟹ SemRec F x res y"
definition op_fix_point :: "(('a,'b) proc' ⇒ ('a,'b) proc')
⇒ ('a,'b) proc'"
where "op_fix_point F x s = (if (∃t. SemRec F x s t) then The (SemRec F x s) else {})"
ML ‹Synchronized.change Phi_Syntax.semantic_oprs (Symtab.update (\<^const_name>‹op_fix_point›, 0))›
subsubsection ‹Simple Properties›
lemma SemRec_IR: "SemRec F x r y ⟹ SemRec (F o F) x r y"
by (induct rule: SemRec.induct, rule SemRec_I0, simp)
lemma SemRec_deterministic:
assumes "SemRec c s r s1" and "SemRec c s r s2" shows "s1 = s2"
proof -
have "SemRec c s r s1 ⟹ (∀s2. SemRec c s r s2 ⟶ s1 = s2)"
apply (induct rule: SemRec.induct)
apply clarify
subgoal for F a b y s2 apply (rotate_tac 1)
apply (induct rule: SemRec.induct) by auto
apply clarify apply (blast intro: SemRec_IR) done
thus ?thesis using assms by simp
qed
lemma SemRec_deterministic2: " SemRec body s r x ⟹ The (SemRec body s r) = x"
using SemRec_deterministic by (metis theI_unique)
section ‹Abstraction of Procedures›
subsubsection ‹Syntax for Annotations›
consts Invariant :: ‹bool ⇒ bool› ("Inv: _" [100] 36)
consts Guard :: ‹bool ⇒ bool› ("Guard: _" [100] 36)
consts End :: ‹bool ⇒ bool› ("End: _" [100] 36)
consts Transition :: ‹'a ⇒ bool› ("Transition: _" [100] 36)
subsection ‹Branch-like›
lemma sel_φapp:
‹ Semantic_Type' (a ⦂ A) TY
⟹ Semantic_Type' (b ⦂ B) TY
⟹ 𝗉𝗋𝗈𝖼 op_sel TY (φV_pair rawc (φV_pair rawa rawb)) ⦃
c ⦂ 𝗏𝖺𝗅[rawc] 𝔹❟ a ⦂ 𝗏𝖺𝗅[rawa] A❟ b ⦂ 𝗏𝖺𝗅[rawb] B
⟼ (if c then a else b) ⦂ 𝗏𝖺𝗅 (if c then A else B)
⦄›
unfolding op_sel_def
by ((cases rawc; cases rawb; cases rawa; cases c; simp add: Semantic_Type'_def subset_iff),
rule, rule, rule, simp add: φexpns WT_bool, blast, rule, simp add: φexpns WT_bool, rule,
simp add: φexpns WT_bool, rule, simp add: φexpns WT_bool, rule, rule, rule,
simp add: φexpns WT_bool, blast, rule, simp add: φexpns WT_bool, rule, simp add: φexpns WT_bool,
rule, simp add: φexpns WT_bool)
lemma branch_φapp:
‹ (𝗉𝗋𝖾𝗆𝗂𝗌𝖾 C ⟶ 𝗉𝗋𝗈𝖼 br⇩T ⦃ X ⟼ Y⇩T ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E⇩T )
⟹ (𝗉𝗋𝖾𝗆𝗂𝗌𝖾 ¬ C ⟶ 𝗉𝗋𝗈𝖼 br⇩F ⦃ X ⟼ Y⇩F ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E⇩F )
⟹ (⋀v. If C (Y⇩T v) (Y⇩F v) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y v @tag invoke_br_join)
⟹ 𝗉𝗋𝗈𝖼 op_if br⇩T br⇩F rawc ⦃ C ⦂ 𝗏𝖺𝗅[rawc] 𝔹❟ X ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 (λe. (E⇩T e 𝗌𝗎𝖻𝗃 C) + (E⇩F e 𝗌𝗎𝖻𝗃 ¬ C)) ›
unfolding op_if_def Premise_def Action_Tag_def
by (cases rawc; cases C; simp; rule; simp add: φexpns WT_bool;
insert φCONSEQ view_shift_by_implication view_shift_refl; blast)
proc "if":
requires C: ‹𝗉𝗋𝗈𝖼 cond ⦃ X ⟼ 𝗏𝖺𝗅 C ⦂ 𝔹❟ X1 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E ›
and brT: ‹𝗉𝗋𝖾𝗆𝗂𝗌𝖾 C ⟶ 𝗉𝗋𝗈𝖼 brT ⦃ X1 ⟼ Y⇩T ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E⇩T ›
and brF: ‹𝗉𝗋𝖾𝗆𝗂𝗌𝖾 ¬ C ⟶ 𝗉𝗋𝗈𝖼 brF ⦃ X1 ⟼ Y⇩F ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E⇩F ›
and BC: ‹(⋀v. If C (Y⇩T v) (Y⇩F v) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y v @tag invoke_br_join)›
input ‹X›
output ‹Y›
throws ‹E + E⇩T + E⇩F›
❴ C branch brT brF BC ❵ .
ML ‹Synchronized.change Phi_Syntax.semantic_oprs (Symtab.update (\<^const_name>‹if›, 3))›
subsection ‹Loops›
lemma "__DoWhile__rule_φapp":
" 𝗉𝗋𝗈𝖼 body ⦃ X x 𝗌𝗎𝖻𝗃 x. P x ⟼ (∃*x'. 𝗏𝖺𝗅 P x' ⦂ 𝔹❟ X x') ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E
⟹ 𝗉𝗋𝗈𝖼 op_do_while body ⦃ X x 𝗌𝗎𝖻𝗃 x. P x ⟼ X x' 𝗌𝗎𝖻𝗃 x'. ¬ P x' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E "
unfolding op_do_while_def φProcedure_def
apply (simp add: less_eq_BI_iff LooseState_expn')
apply (rule allI impI conjI)+
subgoal for comp R s
apply (rotate_tac 2)
apply (induct body comp s rule: SemDoWhile.induct;
clarsimp simp add: times_list_def INTERP_SPEC)
apply fastforce
subgoal premises prems for res f s s'' c u v proof -
have t1: ‹∃uu. (∃x. (∃u v. uu = u * v ∧ u ⊨ X x ∧ v ⊨ R ∧ u ## v) ∧ P x) ∧ s ⊨ INTERP_RES uu›
using prems(5) prems(6) prems(7) prems(8) prems(9) by blast
show ?thesis
by (insert ‹∀_ _. (∃_. _) ⟶ _›[THEN spec[where x=s], THEN spec[where x=R], THEN mp, OF t1]
prems(1) prems(3), fastforce)
qed
apply fastforce
by blast .
proc (nodef) do_while:
requires ‹𝗉𝖺𝗋𝖺𝗆 ( X' x 𝗌𝗎𝖻𝗃 x. Inv: invariant x ∧ Guard: cond x)›
and V: ‹𝗋CALL X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ( X' x 𝗌𝗎𝖻𝗃 x. invariant x ∧ cond x) 𝗐𝗂𝗍𝗁 Any›
and B: ‹∀x. 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 cond x ⟶ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 invariant x
⟶ 𝗉𝗋𝗈𝖼 body ⦃ X' x ⟼ (𝗏𝖺𝗅 cond x' ⦂ 𝔹❟ X' x' 𝗌𝗎𝖻𝗃 x'. invariant x') ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E ›
input ‹X›
output ‹X' x' 𝗌𝗎𝖻𝗃 x'. invariant x' ∧ ¬ cond x'›
throws E
❴
apply_rule V[unfolded Action_Tag_def]
apply_rule "__DoWhile__rule_φapp"[where P=cond and X=‹λx'. X' x' 𝗌𝗎𝖻𝗃 invariant x'›, simplified]
❴ B ❵ !!
❵ .
ML ‹Synchronized.change Phi_Syntax.semantic_oprs (Symtab.update (\<^const_name>‹op_do_while›, 2))›
proc while:
requires ‹𝗉𝖺𝗋𝖺𝗆 ( X x 𝗌𝗎𝖻𝗃 x. Inv: invariant x ∧ Guard: cond x)›
and V: "X' 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ((X x 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R) 𝗌𝗎𝖻𝗃 x. invariant x) 𝗐𝗂𝗍𝗁 Any"
and C: "∀x. 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 invariant x ⟶ 𝗉𝗋𝗈𝖼 Cond ⦃ X x❟ R ⟼ 𝗏𝖺𝗅 cond x' ⦂ 𝔹❟ X x'❟ R 𝗌𝗎𝖻𝗃 x'. invariant x' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E1"
and B: "∀x. 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 invariant x ⟶ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 cond x ⟶ 𝗉𝗋𝗈𝖼 Body ⦃ X x❟ R ⟼ X x'❟ R 𝗌𝗎𝖻𝗃 x'. invariant x' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E2"
input ‹X'›
output ‹X x❟ R 𝗌𝗎𝖻𝗃 x. invariant x ∧ ¬ cond x›
throws ‹E1 + E2›
❴ V C
branch ❴
do_while ‹X vars❟ R 𝗌𝗎𝖻𝗃 vars. Inv: invariant vars ∧ Guard: cond vars›
❴ B C ❵
❵
❴ ❵ for ‹R❟ X vars 𝗌𝗎𝖻𝗃 vars. invariant vars ∧ ¬ cond vars› ;;
❵ .
ML ‹Synchronized.change Phi_Syntax.semantic_oprs (Symtab.update (\<^const_name>‹while›, 3))›
proc (nodef) refine_while
[unfolded φType_def[where T=‹X::'a ⇒ (FIC_N ⇒ FIC) BI›]]:
requires ‹𝗉𝖺𝗋𝖺𝗆 (X x 𝗌𝗎𝖻𝗃 x. Inv: invariant x ∧ Guard: cond x ∧ Transition: f x)›
and V: "X' 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 (X x 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R) 𝗌𝗎𝖻𝗃 invariant x 𝗐𝗂𝗍𝗁 Any"
and C: "∀x. 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 invariant x ⟶ 𝗉𝗋𝗈𝖼 Cond ⦃ R❟ X x ⟼ R❟ X x❟ 𝗏𝖺𝗅 cond x ⦂ 𝔹 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E1"
and B: "∀x. 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 invariant x ⟶ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 cond x ⟶ 𝗉𝗋𝗈𝖼 Body ⦃ R❟ X x ⟼ R❟ X x' 𝗌𝗎𝖻𝗃 x'. x' = f x ∧ invariant x' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E2"
input ‹X'›
output ‹R❟ X x' 𝗌𝗎𝖻𝗃 x'. x' = While_Combinator.while cond f x ∧ invariant x'›
throws ‹E1 + E2›
apply (represent_BI_pred_in_φType X)
❴ V
while ‹x' ⦂ X 𝗌𝗎𝖻𝗃 x' i.
Inv: (x' = (f ^^ i) x ∧ (∀k < i. cond ((f ^^ k) x)) ∧ (∀k ≤ i. invariant ((f ^^ k) x)) ) ∧
Guard: cond x'›
❴ C ❵
❴ B ❵ certified by (clarsimp, rule exI[where x=‹i+1›],
auto simp add: less_Suc_eq_le φ,
(insert le_eq_less_or_eq the_φ(5) the_φ(7), fastforce)[1],
metis funpow.simps(2) le_SucE o_apply the_φ(6) the_φlemmata(3) the_φlemmata(4)) ；
have [φreason add]:
‹⋀y. 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 (f ^^ y) x = While_Combinator.while cond f x
⟹ X ((f ^^ y) x) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X (While_Combinator.while cond f x)›
by (simp add: Premise_def)
❵ certified
by (auto simp add: While_Combinator.while_def while_option_def φ; auto_sledgehammer) .
subsection ‹Recursion›
lemma "__op_recursion_simp__":
"(⋀g x' v'. (⋀x'' v''. 𝗉𝗋𝗈𝖼 g v'' ⦃ X x'' v'' ⟼ λret. Y x'' ret ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E x'')
⟹ 𝗉𝗋𝗈𝖼 F g v' ⦃ X x' v' ⟼ λret. Y x' ret ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E x' )
⟹ ∀x v. 𝗉𝗋𝗈𝖼 op_fix_point F v ⦃ X x v ⟼ λret. Y x ret ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E x"
unfolding op_fix_point_def φProcedure_def atomize_all
apply (clarsimp simp add: SemRec_deterministic2 less_eq_BI_iff del: subsetI)
subgoal for x v comp a R w
apply (rotate_tac 1) apply (induct rule: SemRec.induct)
subgoal premises prems for F v res y
using prems(4)[of ‹λ_ _. {AssumptionBroken}› x v, simplified, THEN spec[where x=res],
THEN spec[where x=R], THEN mp, OF prems(2), unfolded prems(1)] prems(3) by blast
by (smt (z3) comp_apply) .
text ‹Instead, we use a variant of the above rule which in addition annotates the names
of the values.›
lemma "__op_recursion__":
"(⋀g x' (v':: 'a φarg <named> 'names).
P x'
⟹ PROP Labelled label (Technical
(⋀x'' (v''::'a φarg <named> 'names).
P x'' ⟹
𝗉𝗋𝗈𝖼 g (case_named id v'') ⦃ case_named (X x'') v'' ⟼ λret. Y x'' ret ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E x''))
⟹ 𝗉𝗋𝗈𝖼 F g (case_named id v') ⦃ case_named (X x') v' ⟼ λret. Y x' ret ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E x' )
⟹ PROP Pure.prop (
P x ⟹
𝗉𝗋𝗈𝖼 op_fix_point F v ⦃ X x v ⟼ λret. Y x ret ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E x
)"
unfolding op_fix_point_def φProcedure_def atomize_all φarg_forall φarg_All Technical_def
Pure.prop_def
apply (clarsimp simp add: SemRec_deterministic2 less_eq_BI_iff del: subsetI)
subgoal for comp a R w
apply (rotate_tac 2) apply (induct rule: SemRec.induct)
subgoal premises prems for F v res y
using prems(4)[OF prems(5),
of ‹λ_ _. {AssumptionBroken}› v, simplified, THEN spec[where x=res],
THEN spec[where x=R], THEN mp, OF prems(2), unfolded prems(1)]
prems(3) by blast
by (smt (z3) comp_apply) .
ML_file ‹library/basic_recursion.ML›
attribute_setup recursive = ‹Scan.repeat (Scan.lift Parse.term) >> (fn vars =>
Phi_Modifier.wrap_to_attribute (fn (ctxt,sequent) =>
case Phi_Toplevel.name_of_the_building_procedure ctxt
of NONE => error "Name binding of the recursive procedure is mandatory."
| SOME b => (
let
in if Binding.is_empty b
then error "A recursive procedure cannot be anonymous."
else if null vars then tracing "You may want to use syntax ‹recursive vars› to indicate \
\variables varying throught recursive calls." else ();
PhiSem_Control_Flow.basic_recursive_mod Syntax.read_terms b vars (ctxt,sequent)
end
)
))›
subsection ‹Syntax›
syntax "_while_" :: ‹do_binds ⇒ do_binds ⇒ do_binds›
("((2𝗐𝗁𝗂𝗅𝖾 {//(_))//(2} {//(_))//})" [11,11] 20)
"_if_" :: ‹do_binds ⇒ do_binds ⇒ do_binds ⇒ do_binds›
("((2𝗂𝖿 {//(_))//(2} 𝗍𝗁𝖾𝗇 {//(_))//(2} 𝖾𝗅𝗌𝖾 {//(_))//})" [11,11,11] 20)
"_fix_point_" :: ‹idt ⇒ idt ⇒ do_binds ⇒ do_bind› ("((2𝖿𝗂𝗑 _ '(_') {//)(_)//})" [100,100,10] 20)
optional_translations (do_notation)
"_while_ C B" <= "CONST PhiSem_CF_Basic.while C B"
"_while_ C B" <= "_while_ (_do_block C) B"
"_while_ C B" <= "_while_ C (_do_block B)"
"_if_ C A B" <= "CONST PhiSem_CF_Basic.if TY C A B"
"_if_ C A B" <= "_if_ (_do_block C) A B"
"_if_ C A B" <= "_if_ C (_do_block A) B"
"_if_ C A B" <= "_if_ C A (_do_block B)"
"_fix_point_ f arg B" <= "CONST op_fix_point (λf arg. B)"
end