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