Theory Abstract_Impl

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 by (simp add: lowest_tops_impl.simps)
   subgoal
     apply (simp add: lowest_tops_impl.simps)
     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(simp add: None 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(simp add: Some 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 add: les_def;fail)+
        apply(simp split: prod.splits)
        apply(rule ospec_cons)
         apply(rule IFimpl_rule)
           apply(simp add: les_def;fail)+
           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(simp add: les_def;fail)+
    apply(clarsimp)
     apply(rule obind_rule)
     apply(rule mIH(2))
          apply(simp add: les_def;fail)+
    apply(simp add: ifex_ite_opt.simps split: prod.splits)
    apply(rule ospec_cons)
     apply(rule IFimpl_rule)
       apply(auto simp add: les_def;fail)+
    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(simp add: map_invar_impl_les les_def;fail)+
    apply(clarsimp)
    apply(rule obind_rule)
     apply(rule mIH(2))
          apply(simp add: map_invar_impl_les les_def;fail)+
    apply(simp add: ifex_ite_opt.simps split: prod.splits)
    apply(rule obind_rule)
     apply(rule IFimpl_rule)
       apply(simp)
      apply(auto simp add: les_def)[2]
    apply(clarsimp simp add: les_def)
    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)
     apply(clarsimp simp add: ifex_ite_opt.simps)
    using map_invar_rule3 by presburger
qed

end
end