# Theory Abstract_Impl

theory Abstract_Impl
imports BDT Refine_Lib Option_Helpers
```section‹Abstract ITE Implementation›
theory Abstract_Impl
imports BDT
Automatic_Refinement.Refine_Lib
Option_Helpers
begin

datatype ('a, 'ni) IFEXD = TD | FD | IFD 'a 'ni 'ni

locale bdd_impl_pre =
fixes R :: "'s ⇒ ('ni × ('a :: linorder) ifex) set"
fixes I :: "'s ⇒ bool"
begin
definition les:: "'s ⇒ 's ⇒ bool" where
"les s s' == ∀ni n. (ni, n) ∈ R s ⟶ (ni, n) ∈ R s'"
end

locale bdd_impl = bdd_impl_pre R for R :: "'s ⇒ ('ni × ('a :: linorder) ifex) set" +
fixes Timpl :: "'s ⇀ ('ni × 's)"
fixes Fimpl :: "'s ⇀ ('ni × 's)"
fixes IFimpl :: "'a ⇒ 'ni ⇒ 'ni ⇒ 's ⇀ ('ni × 's)"
fixes DESTRimpl :: "'ni  ⇒ 's ⇀ ('a, 'ni) IFEXD"

assumes Timpl_rule: "I s ⟹ ospec (Timpl s) (λ(ni, s'). (ni, Trueif) ∈ R s' ∧ I s' ∧ les s s')"
assumes Fimpl_rule: "I s ⟹ ospec (Fimpl s) (λ(ni, s'). (ni, Falseif) ∈ R s' ∧ I s' ∧ les s s')"
assumes IFimpl_rule: "⟦I s; (ni1,n1) ∈ R s;(ni2,n2) ∈ R s⟧
⟹ ospec (IFimpl v ni1 ni2 s) (λ(ni, s'). (ni, IFC v n1 n2) ∈ R s' ∧ I s' ∧ les s s')"

assumes DESTRimpl_rule1: "I s ⟹ (ni, Trueif) ∈ R s ⟹ ospec (DESTRimpl ni s) (λr. r = TD)"
assumes DESTRimpl_rule2: "I s ⟹ (ni, Falseif) ∈ R s ⟹ ospec (DESTRimpl ni s) (λr. r = FD)"
assumes DESTRimpl_rule3: "I s ⟹ (ni, IF v n1 n2) ∈ R s ⟹
ospec (DESTRimpl ni s)
(λr. ∃ni1 ni2. r = (IFD v ni1 ni2) ∧ (ni1, n1) ∈ R s ∧ (ni2, n2) ∈ R s)"
begin

lemma les_refl[simp,intro!]:"les s s" by (auto simp add: les_def)
lemma les_trans[trans]:"les s1 s2 ⟹ les s2 s3 ⟹ les s1 s3" by (auto simp add: les_def)
lemmas DESTRimpl_rules = DESTRimpl_rule1 DESTRimpl_rule2 DESTRimpl_rule3

lemma DESTRimpl_rule_useless:
"I s ⟹ (ni, n) ∈ R s ⟹ ospec (DESTRimpl ni s) (λr. (case r of
TD ⇒ (ni, Trueif) ∈ R s |
FD ⇒ (ni, Falseif) ∈ R s |
IFD v nt ne ⇒ (∃t e. n = IF v t e ∧ (ni, IF v t e) ∈ R s)))"
by(cases n; clarify; drule (1) DESTRimpl_rules; drule ospecD2; clarsimp)
lemma DESTRimpl_rule:
"I s ⟹ (ni, n) ∈ R s ⟹ ospec (DESTRimpl ni s) (λr. (case n of
Trueif ⇒ r = TD |
Falseif ⇒ r = FD |
IF v t e ⇒ (∃tn en. r = IFD v tn en ∧ (tn,t) ∈ R s ∧ (en,e) ∈ R s)))"
by(cases n; clarify; drule (1) DESTRimpl_rules; drule ospecD2; clarsimp)

definition "case_ifexi fti ffi fii ni s ≡ do {
dest ← DESTRimpl ni s;
case dest of
TD ⇒ fti s
| FD ⇒ ffi s
| IFD v ti ei ⇒ fii v ti ei s}"

lemma case_ifexi_rule:
assumes INV: "I s"
assumes NI: "(ni,n)∈R s"
assumes FTI: "⟦ n = Trueif ⟧ ⟹ ospec (fti s) (λ(r,s'). (r,ft) ∈ Q s ∧ I' s')"
assumes FFI: "⟦ n = Falseif ⟧ ⟹ ospec (ffi s) (λ(r,s'). (r,ff) ∈ Q s ∧ I' s')"
assumes FII: "⋀ti ei v t e. ⟦ n = IF v t e; (ti,t)∈R s; (ei,e)∈R s ⟧ ⟹ ospec (fii v ti ei s) (λ(r,s'). (r,fi v t e) ∈ Q s ∧ I' s')"
shows "ospec (case_ifexi fti ffi fii ni s) (λ(r,s'). (r,case_ifex ft ff fi n) ∈ Q s ∧ I' s')"
unfolding case_ifexi_def
apply (cases n)
subgoal
apply (rule obind_rule)
apply (rule DESTRimpl_rule1[OF INV])
using NI FTI by (auto)
subgoal
apply (rule obind_rule)
apply (rule DESTRimpl_rule2[OF INV])
using NI FFI by (auto)
subgoal
apply (rule obind_rule)
apply (rule DESTRimpl_rule3[OF INV])
using NI FII by (auto)
done

abbreviation "return x ≡ λs. Some (x,s)"

primrec lowest_tops_impl where
"lowest_tops_impl [] s = Some (None,s)" |
"lowest_tops_impl (e#es) s =
case_ifexi
(λs. lowest_tops_impl es s)
(λs. lowest_tops_impl es s)
(λv t e s. do {
(rec,s) ← lowest_tops_impl es s;
(case rec of
Some u ⇒ Some ((Some (min u v)), s) |
None ⇒ Some ((Some v), s))
}) e s"

declare lowest_tops_impl.simps[simp del]

fun lowest_tops_alt where
"lowest_tops_alt [] = None" |
"lowest_tops_alt (e#es) = (
let rec = lowest_tops_alt es in
case_ifex
rec
rec
(λv t e. (case rec of
Some u ⇒ (Some (min u v)) |
None ⇒ (Some v))
) e
)"

lemma lowest_tops_alt: "lowest_tops l = lowest_tops_alt l"
by (induction l rule: lowest_tops.induct) (auto split: option.splits simp: lowest_tops.simps)

lemma lowest_tops_impl_R:
assumes "list_all2 (in_rel (R s)) li l" "I s"
shows "ospec (lowest_tops_impl li s) (λ(r,s'). r = lowest_tops l ∧ s'=s)"
unfolding lowest_tops_alt
using assms apply (induction rule: list_all2_induct)
subgoal
apply (rule case_ifexi_rule[where Q="λs. Id", unfolded pair_in_Id_conv])
apply assumption+
apply (rule obind_rule)
apply assumption
apply (clarsimp split: option.splits)
done
done

definition restrict_top_impl where
"restrict_top_impl e vr vl s =
case_ifexi
(return e)
(return e)
(λv te ee. return (if v = vr then (if vl then te else ee) else e))
e s
"

lemma restrict_top_alt: "restrict_top n var val = (case n of
(IF v t e) ⇒ (if v = var then (if val then t else e) else (IF v t e))
| _ ⇒ n)"
apply (induction n var val rule: restrict_top.induct)
apply (simp_all)
done

lemma restrict_top_impl_spec: "I s ⟹ (ni,n) ∈ R s ⟹ ospec (restrict_top_impl ni vr vl s) (λ(res,s'). (res, restrict_top n vr vl) ∈ R s ∧ s'=s)"
unfolding restrict_top_impl_def restrict_top_alt
by (rule case_ifexi_rule[where I'="λs'. s'=s" and Q="R", simplified]) auto

partial_function(option) ite_impl where
"ite_impl i t e s = do {
(lt,_) ← lowest_tops_impl [i, t, e] s;
(case lt of
Some a ⇒ do {
(ti,_) ← restrict_top_impl i a True s;
(tt,_) ← restrict_top_impl t a True s;
(te,_) ← restrict_top_impl e a True s;
(fi,_) ← restrict_top_impl i a False s;
(ft,_) ← restrict_top_impl t a False s;
(fe,_) ← restrict_top_impl e a False s;
(tb,s) ← ite_impl ti tt te s;
(fb,s) ← ite_impl fi ft fe s;
IFimpl a tb fb s}
| None ⇒ case_ifexi (λ_.(Some (t,s))) (λ_.(Some (e,s))) (λ_ _ _ _. None) i s
)}"

lemma ite_impl_R: "I s
⟹ in_rel (R s) ii i ⟹ in_rel (R s) ti t ⟹ in_rel (R s) ei e
⟹ ospec (ite_impl ii ti ei s) (λ(r, s'). (r, ifex_ite i t e) ∈ R s' ∧ I s' ∧ les s s')"
proof(induction i t e arbitrary: s ii ti ei rule: ifex_ite.induct, goal_cases)
case (1 i t e s ii ti ei) note goal1 = 1
have la2: "list_all2 (in_rel (R s)) [ii,ti,ei] [i,t,e]" using goal1(4-6) by simp
show ?case proof(cases "lowest_tops [i,t,e]")
case None from goal1(3-6) show ?thesis
apply(subst ite_impl.simps)
apply(rule obind_rule[where Q="λ(r, s'). r = lowest_tops [i,t,e] ∧ s'=s"])
apply(rule ospec_cons)
apply(rule lowest_tops_impl_R[OF la2])
apply(assumption)
apply(clarsimp split: prod.splits)
apply(clarsimp)
apply(rule ospec_cons)
apply(rule case_ifexi_rule[where I'="λs'. s'=s"])
using None by (auto split: prod.splits ifex.splits simp: lowest_tops.simps)
next
case (Some lv)
note mIH = goal1(1,2)[OF Some]
from goal1(3-6) show ?thesis
apply(subst ite_impl.simps)
apply(rule obind_rule[where Q="λ(r, s'). r = lowest_tops [i,t,e]"])
apply(rule ospec_cons)
apply(rule lowest_tops_impl_R[OF la2])
apply(assumption)
apply(clarsimp split: prod.splits)
apply(clarsimp)
(* take care of all those restrict_tops *)
apply(rule obind_rule, rule restrict_top_impl_spec, assumption+, clarsimp split: prod.splits)+
apply(rule obind_rule)
apply(rule mIH(1))
apply(simp;fail)+
apply(clarsimp)
apply(rule obind_rule)
apply(rule mIH(2))
apply(simp split: prod.splits)
apply(rule ospec_cons)
apply(rule IFimpl_rule)
using les_def les_trans by blast+
qed
qed

lemma case_ifexi_mono[partial_function_mono]:
assumes [partial_function_mono]:
"mono_option (λF. fti F s)"
"mono_option (λF. ffi F s)"
"⋀x31 x32 x33. mono_option (λF. fii F x31 x32 x33 s)"
shows "mono_option (λF. case_ifexi (fti F) (ffi F) (fii F) ni s)"
unfolding case_ifexi_def by (tactic ‹Partial_Function.mono_tac @{context} 1›)

partial_function(option) val_impl :: "'ni ⇒ ('a ⇒ bool) ⇒ 's ⇒ (bool×'s) option"
where
"val_impl e ass s = case_ifexi
(λs. Some (True,s))
(λs. Some (False,s))
(λv t e s. val_impl (if ass v then t else e) ass s)
e  s"

lemma "I s ⟹ (ni,n) ∈ R s ⟹ ospec (val_impl ni ass s) (λ(r,s'). r = (val_ifex n ass) ∧ s'=s)"
apply (induction n arbitrary: ni)
subgoal
apply (subst val_impl.simps)
apply (rule ospec_cons)
apply (rule case_ifexi_rule[where I'="λs'. s'=s" and Q="λs. Id"]; assumption?)
by auto
subgoal
apply (subst val_impl.simps)
apply (rule ospec_cons)
apply (rule case_ifexi_rule[where I'="λs'. s'=s" and Q="λs. Id"]; assumption?)
by auto
subgoal
apply (subst val_impl.simps)
apply (subst val_ifex.simps)
apply (clarsimp; intro impI conjI)
apply (rule ospec_cons)
apply (rule case_ifexi_rule[where I'="λs'. s'=s" and Q="λs. Id"]; assumption?)
apply (simp; fail)
apply (simp; fail)
apply (rule ospec_cons)
apply (rprems; simp; fail)
apply (simp; fail)
apply (simp; fail)
apply (rule ospec_cons)
apply (rule case_ifexi_rule[where I'="λs'. s'=s" and Q="λs. Id"]; assumption?)
apply (simp; fail)
apply (simp; fail)
apply(simp)
apply (rule ospec_cons)
apply (rprems; simp; fail)
apply (simp; fail)
apply (simp; fail)
done
done

end

locale bdd_impl_cmp_pre = bdd_impl_pre
begin

definition "map_invar_impl m s =
(∀ii ti ei ri. m (ii,ti,ei) = Some ri ⟶
(∃i t e. ((ri,ifex_ite_opt i t e) ∈ R s) ∧ (ii,i) ∈ R s ∧ (ti,t) ∈ R s ∧ (ei,e) ∈ R s))"

lemma map_invar_impl_les: "map_invar_impl m s ⟹ les s s' ⟹ map_invar_impl m s'"
unfolding map_invar_impl_def bdd_impl_pre.les_def by blast

lemma map_invar_impl_update: "map_invar_impl m s ⟹
(ii,i) ∈ R s ⟹ (ti,t) ∈ R s ⟹ (ei,e) ∈ R s ⟹
(ri, ifex_ite_opt i t e) ∈ R s ⟹ map_invar_impl (m((ii,ti,ei) ↦ ri)) s"
unfolding map_invar_impl_def by auto

end

locale bdd_impl_cmp = bdd_impl + bdd_impl_cmp_pre +
fixes M :: "'a ⇒ ('b × 'b × 'b) ⇒ 'b option"
fixes U :: "'a ⇒ ('b × 'b × 'b) ⇒ 'b ⇒ 'a"
fixes cmp :: "'b ⇒ 'b ⇒ bool"
assumes cmp_rule1: "I s ⟹ (ni, i) ∈ R s ⟹ (ni', i) ∈ R s ⟹ cmp ni ni'"
assumes cmp_rule2: "I s ⟹ cmp ni ni' ⟹ (ni, i) ∈ R s ⟹ (ni', i') ∈ R s ⟹ i = i'"
assumes map_invar_rule1: "I s ⟹ map_invar_impl (M s) s"
assumes map_invar_rule2: "I s ⟹ (ii,it) ∈ R s ⟹ (ti,tt) ∈ R s ⟹ (ei,et) ∈ R s ⟹
(ri, ifex_ite_opt it tt et) ∈ R s ⟹ U s (ii,ti,ei) ri = s' ⟹
I s'"
assumes map_invar_rule3: "I s ⟹ R (U s (ii, ti, ei) ri) = R s"
begin

lemma cmp_rule_eq: "I s ⟹  (ni, i) ∈ R s ⟹ (ni', i') ∈ R s ⟹ cmp ni ni' ⟷ i = i'"
using cmp_rule1 cmp_rule2 by force

lemma DESTRimpl_Some: "I s ⟹ (ni, i) ∈ R s ⟹ ospec (DESTRimpl ni s) (λr. True)"
apply(cases i)
apply(auto intro: ospec_cons dest: DESTRimpl_rules)
done

fun param_opt_impl where
"param_opt_impl i t e s =  do {
ii ← DESTRimpl i s;
ti ← DESTRimpl t s;
ei ← DESTRimpl e s;
(tn,s) ← Timpl s;
(fn,s) ← Fimpl s;
Some ((if ii = TD then Some t else
if ii = FD then Some e else
if ti = TD ∧ ei = FD then Some i else
if cmp t e then Some t else
if ei = TD ∧ cmp i t then Some tn else
if ti = FD ∧ cmp i e then Some fn else
None), s)}"

declare param_opt_impl.simps[simp del]

lemma param_opt_impl_lesI:
assumes "I s" "(ii,i) ∈ R s" "(ti,t) ∈ R s" "(ei,e) ∈ R s"
shows "ospec (param_opt_impl ii ti ei s)
(λ(r,s'). I s' ∧ les s s')"
using assms apply(subst param_opt_impl.simps)
by (auto simp add: param_opt_def les_def intro!: obind_rule
dest: DESTRimpl_Some Timpl_rule Fimpl_rule)

lemma param_opt_impl_R:
assumes "I s" "(ii,i) ∈ R s" "(ti,t) ∈ R s" "(ei,e) ∈ R s"
shows "ospec (param_opt_impl ii ti ei s)
(λ(r,s'). case r of None ⇒ param_opt i t e = None
| Some r ⇒ (∃r'. param_opt i t e  = Some r' ∧ (r, r') ∈ R s'))"
using assms apply(subst param_opt_impl.simps)
apply(rule obind_rule)
apply(rule DESTRimpl_rule; assumption)
apply(rule obind_rule)
apply(rule DESTRimpl_rule; assumption)
apply(rule obind_rule)
apply(rule DESTRimpl_rule; assumption)
apply(rule obind_rule)
apply(rule Timpl_rule; assumption)
apply(safe)
apply(rule obind_rule)
apply(rule Fimpl_rule; assumption)
by (auto simp add: param_opt_def les_def cmp_rule_eq split: ifex.splits)

partial_function(option) ite_impl_opt where
"ite_impl_opt i t e s = do {
(ld, s) ←  param_opt_impl i t e s;
(case ld of Some b ⇒ Some (b, s) |
None ⇒
do {
(lt,_) ← lowest_tops_impl [i, t, e] s;
(case lt of
Some a ⇒ do {
(ti,_) ← restrict_top_impl i a True s;
(tt,_) ← restrict_top_impl t a True s;
(te,_) ← restrict_top_impl e a True s;
(fi,_) ← restrict_top_impl i a False s;
(ft,_) ← restrict_top_impl t a False s;
(fe,_) ← restrict_top_impl e a False s;
(tb,s) ← ite_impl_opt ti tt te s;
(fb,s) ← ite_impl_opt fi ft fe s;
IFimpl a tb fb s}
| None ⇒ case_ifexi (λ_.(Some (t,s))) (λ_.(Some (e,s))) (λ_ _ _ _. None) i s
)})}"

lemma ospec_and: "ospec f P ⟹ ospec f Q ⟹ ospec f (λx. P x ∧ Q x)"
using ospecD2 by force

lemma ite_impl_opt_R: "
I s
⟹ in_rel (R s) ii i ⟹ in_rel (R s) ti t ⟹ in_rel (R s) ei e
⟹ ospec (ite_impl_opt ii ti ei s) (λ(r, s'). (r, ifex_ite_opt i t e) ∈ R s' ∧ I s' ∧ les s s')"
proof(induction i t e arbitrary: s ii ti ei rule: ifex_ite_opt.induct, goal_cases)
note ifex_ite_opt.simps[simp del] restrict_top.simps[simp del]
case (1 i t e s ii ti ei) note goal1 = 1
have la2: "list_all2 (in_rel (R s)) [ii,ti,ei] [i,t,e]" using goal1(4-6) by simp
note mIH = goal1(1,2)
from goal1(3-6) show ?case
apply(cases "param_opt i t e")
defer
apply(subst ite_impl_opt.simps)
apply(rule obind_rule)
apply(rule ospec_and[OF param_opt_impl_R param_opt_impl_lesI])
apply(auto simp add: les_def ifex_ite_opt.simps split: option.splits)[9]
(* param_opt i t e = None *)
apply(frule param_opt_lowest_tops_lem)
apply(clarsimp)
apply(subst ite_impl_opt.simps)
apply(rule obind_rule)
apply(rule ospec_and[OF param_opt_impl_R param_opt_impl_lesI])
apply(auto split: option.splits)[8]
apply(clarsimp split: option.splits)
apply(rule obind_rule[where Q="λ(r, s'). r = lowest_tops [i,t,e]"])
apply(rule ospec_cons)
apply(rule lowest_tops_impl_R)
using les_def apply(fastforce)
apply(assumption)
apply(fastforce)
using BDT.param_opt_lowest_tops_lem apply(clarsimp split: prod.splits)
(* take care of all those restrict_tops *)
apply(rule obind_rule, rule restrict_top_impl_spec, assumption, auto simp add: les_def split: prod.splits)+
apply(rule obind_rule)
apply(rule mIH(1))
apply(clarsimp)
apply(rule obind_rule)
apply(rule mIH(2))
apply(rule ospec_cons)
apply(rule IFimpl_rule)
done
qed

partial_function(option) ite_impl_lu where
"ite_impl_lu i t e s = do {
(case M s (i,t,e) of Some b ⇒ Some (b,s) | None ⇒ do {
(ld, s) ←  param_opt_impl i t e s;
(case ld of Some b ⇒ Some (b, s) |
None ⇒
do {
(lt,_) ← lowest_tops_impl [i, t, e] s;
(case lt of
Some a ⇒ do {
(ti,_) ← restrict_top_impl i a True s;
(tt,_) ← restrict_top_impl t a True s;
(te,_) ← restrict_top_impl e a True s;
(fi,_) ← restrict_top_impl i a False s;
(ft,_) ← restrict_top_impl t a False s;
(fe,_) ← restrict_top_impl e a False s;
(tb,s) ← ite_impl_lu ti tt te s;
(fb,s) ← ite_impl_lu fi ft fe s;
(r,s) ← IFimpl a tb fb s;
let s = U s (i,t,e) r;
Some (r,s)
} |
None ⇒ None
)})})}"

declare ifex_ite_opt.simps[simp del]

lemma ite_impl_lu_R: "I s
⟹ (ii,i) ∈ R s ⟹ (ti,t) ∈ R s ⟹ (ei,e) ∈ R s
⟹ ospec (ite_impl_lu ii ti ei s)
(λ(r, s'). (r, ifex_ite_opt i t e) ∈ R s' ∧ I s' ∧ les s s')"
proof(induction i t e arbitrary: s ii ti ei rule: ifex_ite_opt.induct, goal_cases)
note restrict_top.simps[simp del]
case (1 i t e s ii ti ei) note goal1 = 1
have la2: "list_all2 (in_rel (R s)) [ii,ti,ei] [i,t,e]" using goal1(4-6) by simp
note mIH = goal1(1,2)
from goal1(3-6) show ?case
apply(subst ite_impl_lu.simps)
apply(cases "M s (ii, ti, ei)")
defer
(* M s (ii, ti, ei) = Some a *)
apply(frule map_invar_rule1)
apply(simp only: option.simps ospec.simps prod.simps simp_thms les_refl)
apply(subst (asm) map_invar_impl_def)
apply(erule allE[where x = ii])
apply(erule allE[where x = ti])
apply(erule allE[where x = ei])
apply(rename_tac a)
apply(erule_tac x = a in allE)
apply(metis cmp_rule_eq)
(* M s (ii, ti, ei) = Some a *)
apply(clarsimp)
apply(cases "param_opt i t e")
defer
(* param_opt i t e = Some a *)
apply(rule obind_rule)
apply(rule ospec_and[OF param_opt_impl_R param_opt_impl_lesI])
apply(auto simp add: map_invar_impl_les ifex_ite_opt.simps  split: option.splits)[9]
(* param_opt i t e = None *)
apply(frule param_opt_lowest_tops_lem)
apply(clarsimp)
apply(rule obind_rule)
apply(rule ospec_and[OF param_opt_impl_R param_opt_impl_lesI])
apply(auto split: option.splits)[8]
apply(clarsimp split: option.splits)
apply(rule_tac obind_rule[where Q="λ(r, s'). r = lowest_tops [i,t,e]"])
apply(rule ospec_cons)
apply(rule lowest_tops_impl_R)
using les_def apply(fastforce)
apply(assumption)
apply(fastforce)
using BDT.param_opt_lowest_tops_lem apply(clarsimp split: prod.splits)
apply(rule obind_rule, rule restrict_top_impl_spec, assumption+, auto simp add: les_def split: prod.splits)+
apply(rule obind_rule)
apply(rule mIH(1))
apply(clarsimp)
apply(rule obind_rule)
apply(rule mIH(2))
apply(rule obind_rule)
apply(rule IFimpl_rule)
apply(simp)
apply(safe)
using map_invar_rule3 apply(presburger)
apply(rule map_invar_rule2)
prefer 6 apply(blast)
apply(blast)
apply(blast)
apply(blast)
apply(blast)