Theory Sepref_Conc_Post
section ‹Concrete Equality Constraints›
theory Sepref_Conc_Post
imports
Main
Automatic_Refinement.Misc
begin
subsection ‹Basic Combinators›
named_theorems CP_defs
definition [CP_defs]: "CP_JOIN CP⇩1 CP⇩2 ≡ λr. CP⇩1 r ∨ CP⇩2 r"
definition [CP_defs]: "CP_EX CP ≡ λr. ∃x. CP x r"
definition [CP_defs]: "CP_SEQ CP⇩1 CP⇩2 ≡ λr. ∃x. CP⇩1 x ∧ CP⇩2 x r"
definition [CP_defs]: "CP_RPT CP ≡ CP⇧*⇧*"
definition [CP_defs]: "CP_SPLIT CP p ≡ λr. case p of (a,b) ⇒ CP a b r"
definition [CP_defs]: "CP_EX32 CP ≡ λ(x⇩1,x⇩2). ∃x⇩3. CP (x⇩1,x⇩2,x⇩3)"
definition [CP_defs]: "CP_pred P ≡ P::bool"
subsection ‹Normalization›
subsubsection ‹Simplification›
named_theorems CP_simps
lemma [CP_simps]:
"CP_SEQ (λ_. True) CP = CP_EX CP"
"CP_EX (λ_. P) = P"
by (auto simp add: CP_defs)
lemma [CP_simps]: "CP_SEQ (λr. r = x) CP = CP x"
by (simp add: CP_defs)
lemma [CP_simps]: "CP_JOIN A A = A"
by (simp add: CP_defs)
lemma [CP_simps]: "p=(a,b) ⟷ fst p = a ∧ snd p = b" by auto
lemma [CP_simps]: "case_prod f = (λp. f (fst p) (snd p))" by auto
subsubsection ‹Monotonicity›
definition [CP_defs]: "CP_TAG x ≡ x::bool"
definition [CP_defs]: "CP_HANDLE x ≡ x::bool"
lemma CP_HANDLEI: "X ⟹ CP_HANDLE X" by (simp add: CP_defs)
lemma CP_HANDLED: "CP_HANDLE X ⟹ X" by (simp add: CP_defs)
named_theorems CP_monos
lemma CP_JOIN_mono[CP_monos]:
"CP_JOIN A B r ⟹ ⟦ ⋀r. A r ⟹ CP_TAG (A' r); ⋀r. B r ⟹ CP_TAG (B' r) ⟧ ⟹ CP_JOIN A' B' r"
by (auto simp: CP_defs)
lemma CP_EX_mono[CP_monos]: "CP_EX A r ⟹ ⟦⋀x r. A x r ⟹ CP_TAG (A' x r)⟧ ⟹ CP_EX A' r"
by (auto simp: CP_defs)
lemma CP_EX32_mono[CP_monos]: "CP_EX32 A r ⟹ ⟦⋀r. A r ⟹ CP_TAG (A' r)⟧ ⟹ CP_EX32 A' r"
by (auto simp: CP_defs)
lemma CP_SEQ_mono[CP_monos]: "CP_SEQ A B r ⟹ ⟦⋀x. A x ⟹ CP_TAG (A' x); ⋀x r. B x r ⟹ CP_TAG (B' x r)⟧ ⟹ CP_SEQ A' B' r"
by (auto simp: CP_defs)
lemma CP_RPT_mono[CP_monos]: "CP_RPT A x r ⟹ ⟦ ⋀x r. A x r ⟹ CP_TAG (A' x r) ⟧ ⟹ CP_RPT A' x r"
apply (auto simp: CP_defs)
by (metis mono_rtranclp)
lemma CP_SPLIT_unfold[CP_simps]: "CP_SPLIT P = (λp. P (fst p) (snd p))"
by (auto simp: CP_defs split: prod.splits)
lemma CP_tagI: "A ⟹ CP_TAG A"
by (auto simp: CP_defs)
lemma CP_tag_cong: "CP_TAG A = CP_TAG A" by simp
subsection ‹Combinator Normalization›
subsubsection ‹Basics›
text ‹Transfer information into tag›
lemma CP_tag_resolve1:
assumes "a=b"
assumes "CP_TAG B"
shows "CP_TAG (a=b ∧ B)"
using assms by auto
lemma CP_tag_resolve2:
assumes "CP_pred P"
assumes "CP_TAG B"
shows "CP_TAG (P ∧ B)"
using assms by (auto simp: CP_defs)
lemma CP_tag_triv: "CP_TAG True"
by (auto simp: CP_TAG_def)
method cp_resolve_tag = (((determ ‹erule CP_tag_resolve1 CP_tag_resolve2›)+)?,rule CP_tag_triv)
text ‹Explode products›
method cp_explode_prod = (simp only: prod_eq_iff prod.inject cnv_conj_to_meta fst_conv snd_conv cong: CP_tag_cong)
subsubsection ‹Plain equality›
method handle_plain_eqs =
drule asm_rl[of "_=_"] asm_rl[of "_∧_"] asm_rl[of True] asm_rl[of "CP_pred _"],
(elim conjE)?,
cp_resolve_tag
subsubsection ‹Sequence›
lemma CP_SEQE:
assumes "CP_SEQ (λx. A x) (λx r. B x r) r"
obtains x where "A x" "B x r"
using assms by (auto simp: CP_defs)
method handle_CP_SEQ =
drule CP_HANDLED,
erule CP_SEQE,
(elim conjE)?,
cp_explode_prod?,
cp_resolve_tag
subsubsection ‹Ex›
lemma CP_EXE:
assumes "CP_EX (λx. A x) r"
obtains x where "A x r"
using assms by (auto simp: CP_defs)
method handle_CP_EX =
drule CP_HANDLED,
erule CP_EXE,
(elim conjE)?,
cp_explode_prod?,
cp_resolve_tag
subsubsection ‹Ex32›
lemma CP_EX32E:
assumes "CP_EX32 CP r"
obtains x where "CP (fst r,snd r,x)"
using assms by (auto simp: CP_defs)
method handle_CP_EX32 =
drule CP_HANDLED,
erule CP_EX32E,
(elim conjE)?,
cp_explode_prod?,
cp_resolve_tag
subsubsection ‹Join›
lemma handle_join_take:
assumes "CP_JOIN (λr. a r ∧ as r) bs r"
assumes "⋀r. bs r ⟹ a r"
obtains "a r" "CP_JOIN as bs r"
using assms
by (auto simp: CP_defs)
lemma handle_join_drop:
assumes "CP_JOIN (λr. a r ∧ as r) bs r"
obtains "CP_JOIN as bs r"
using assms
by (auto simp: CP_defs)
lemma handle_join_last_take:
assumes "CP_JOIN (λr. a r) bs r"
assumes "⋀r. bs r ⟹ a r"
obtains "a r"
using assms
by (auto simp: CP_defs)
lemma handle_join_last_drop:
"CP_JOIN (λr. a r) bs r ⟹ P ⟹ P" .
method handle_CP_JOIN =
drule CP_HANDLED,
drule asm_rl[of "CP_JOIN _ _ _"],
(simp only: prod_eq_iff conj_assoc)?,
(((erule handle_join_take, blast) | erule handle_join_drop)+)?,
((erule handle_join_last_take, blast) | erule handle_join_last_drop),
cp_resolve_tag
subsubsection ‹Repeat›
lemma CP_RPT_split_conj: "CP_RPT (λa b. A a b ∧ B a b) a b ⟹ CP_RPT A a b ∧ CP_RPT B a b"
by (simp add: CP_RPT_mono CP_tag_triv)
lemma handle_rpt_take:
"CP_RPT (λa b. f b = f a) a b ⟹ f b = f a"
by (smt (verit, del_insts) CP_RPT_def rtranclp_induct)
method handle_CP_RPT =
(drule CP_HANDLED),
(elim CP_RPT_split_conj[elim_format] conjE handle_rpt_take[elim_format])?,
cp_resolve_tag
method cp_normalize_step =
drule CP_monos[THEN CP_HANDLEI] | handle_plain_eqs|handle_CP_SEQ|handle_CP_EX|handle_CP_EX32|handle_CP_JOIN|handle_CP_RPT
method cp_normalize =
(simp only: CP_simps cong: CP_tag_cong)?;
(determ ‹cp_normalize_step›)+
subsection ‹High-Level Methods›
definition [CP_defs]: "CP_assm CP ≡ (CP::bool)"
definition [CP_defs]: "CP_cond CP ≡ (CP::bool)"
definition [CP_defs]: "CP_simplify A B ≡ ∀r. A r ⟶ B r"
named_theorems cp_solve_cond_pre
lemma [cp_solve_cond_pre]: "CP_cond True"
by (auto simp: CP_defs)
lemma cp_simplify_expose_assmI:
assumes "CP_assm CP"
assumes "CP ⟶ CP_TAG CP'"
shows "CP'"
using assms by (auto simp: CP_defs)
method cp_simplify_expose_assm =
determ ‹drule cp_simplify_expose_assmI›,
determ ‹((thin_tac "_")+)?›, rule impI,
(cp_normalize;fail)
method cp_solve_cond =
solves ‹intro cp_solve_cond_pre› |
((cp_simplify_expose_assm+)?;
auto simp: CP_cond_def CP_pred_def CP_simps)
lemma CP_simplify_triv: "CP_simplify (λ_. True) (λ_. True)"
by (auto simp: CP_defs)
lemma CP_simplifyI:
assumes "⋀r. A r ⟶ CP_TAG (B r)"
shows "CP_simplify A B"
using assms by (auto simp: CP_defs)
method cp_simplify =
rule CP_simplify_triv
|
rule CP_simplifyI,
determ ‹((thin_tac "_")+)?›, rule impI,
(cp_normalize;fail)
thm CP_simps
end