Theory RPO_Memoized

(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2011-2015)
Author:  Guillaume Allais (2011)
Author:  René Thiemann <rene.thiemann@uibk.ac.at> (2011-2015)
License: LGPL (see file COPYING.LESSER)
*)
theory RPO_Memoized
imports
  RPO
  RPO_Impl
  "../Auxiliaries/Multiset_Extension_Impl"
  TA.SubList
  "../Auxiliaries/Memories"
begin

(** A memoized computation of type 'a is a computation that,
    given an environment of type 'm computes and 'a and a
    new environment of type 'm. **)

type_synonym ('m, 'a) memo = "'m ⇒ ('a × 'm)"

(** Type synonyms for precedence and tagging functions. **)
type_synonym 'f prec_fct = "('f × nat ⇒ 'f × nat ⇒ bool × bool) × ('f × nat ⇒ bool)"
type_synonym 'f status_fct = "'f × nat ⇒ order_tag"

(** Efficient versions of all and any for the specific cases that
    we are interested in. **)

fun any_nstri_efficient_m :: "('a ⇒ ('m, bool × bool) memo) ⇒ 'a list ⇒ ('m, bool) memo"
where
  "any_nstri_efficient_m f []       m = (False, m)" |
  "any_nstri_efficient_m f (a # as) m = (let ((_, ns), m') = f a m in
     if ns then (True, m') else any_nstri_efficient_m f as m')"

fun all_stri_efficient_m :: "('a ⇒ ('m, bool × bool) memo) ⇒ 'a list ⇒ ('m, bool) memo"
where
  "all_stri_efficient_m f []       m = (True, m)" |
  "all_stri_efficient_m f (a # as) m = (let ((s, _), m') = f a m in
     if s then all_stri_efficient_m f as m' else (False, m'))"

(** congruence lemmas needed for rpo's termination proof **)

lemma any_nstri_efficient_m[fundef_cong]:
  assumes "⋀ s m. s ∈ set ss ⟹ f s m = g s m"
  shows "any_nstri_efficient_m f ss m = any_nstri_efficient_m g ss m"
using assms proof (induct ss arbitrary: m)
  case (Cons s ss)
  show ?case 
  proof (cases "f s m")
    case (Pair res m')
    with Cons have rec: "any_nstri_efficient_m f ss m' = any_nstri_efficient_m g ss m'" by auto
    from Pair rec show ?thesis 
      by (simp add: Cons(2)[of s m, simplified], cases res, auto)    
  qed
qed simp

lemma all_stri_efficient_m [fundef_cong] : 
  assumes "⋀ t m. t ∈ set ts ⟹ f t m = g t m"
  shows "all_stri_efficient_m f ts m = all_stri_efficient_m g ts m"
using assms proof (induct ts arbitrary: m)
  case (Cons t ts)
  show ?case 
  proof (cases "f t m")
    case (Pair res m')
    with Cons have rec: "all_stri_efficient_m f ts m' = all_stri_efficient_m g ts m'" by auto
    from Pair rec show ?thesis 
      by (simp add: Cons(2)[of t m, simplified], cases res, auto)    
  qed
qed simp

(** Efficient filter **)

fun filter_not_stri_efficient_m_aux :: "('a ⇒ ('m, bool × bool) memo) ⇒ 'a list ⇒ 'a list ⇒ ('m, 'a list) memo"
where
  "filter_not_stri_efficient_m_aux f []       bs m = (bs, m)" |
  "filter_not_stri_efficient_m_aux f (a # as) bs m = (
    let ((s, _), m') = f a m in
    if s
    then filter_not_stri_efficient_m_aux f as bs m'
    else filter_not_stri_efficient_m_aux f as (a # bs) m')"

definition filter_not_stri_efficient_m:: "('a ⇒ ('m, bool × bool) memo) ⇒ 'a list ⇒ ('m, 'a list) memo"
where
  "filter_not_stri_efficient_m f as m ≡ let (ys, m') = filter_not_stri_efficient_m_aux f as [] m in (rev ys, m')"

(** congruence lemmas needed for rpo's termination proof **)

lemma filter_not_stri_efficient_m_aux[fundef_cong]: 
  assumes "⋀ a b m. a ∈ set as ⟹ f a m = g a m"
  shows "filter_not_stri_efficient_m_aux f as bs m =
   filter_not_stri_efficient_m_aux g as bs m"
using assms proof (induct as arbitrary: bs m)
  case (Cons a as bs m)
  show ?case
  proof (cases "f a m")
  case (Pair sns m')
    obtain s ns where Psns: "sns = (s, ns)" by (cases sns) auto
    from Pair and Psns and Cons(2) have "g a m = ((s, ns), m')" by simp
    with Psns and Pair and Cons show ?thesis by simp
  qed
qed auto
    
lemma filter_not_stri_efficient_m[fundef_cong]: 
  assumes "⋀ a b m. a ∈ set as ⟹ f a m = g a m"
  shows "filter_not_stri_efficient_m f as m =
   filter_not_stri_efficient_m g as m"
unfolding filter_not_stri_efficient_m_def
using assms and filter_not_stri_efficient_m_aux
by force

(** These lemmas are needed for the termination prover to be able
    to find a decreasing lexographic order for mul_ext_efficient_m. **)

lemma filter_not_stri_efficient_m_aux_subseq:
  "subseq (rev (fst (filter_not_stri_efficient_m_aux f as bs m))) ((rev bs) @ as)"
proof (induct as arbitrary: bs m)
  case (Cons a as)
  obtain sns m' where P1: "f a m = (sns, m')" by (cases "f a m") auto
  obtain s ns where P2: "sns = (s, ns)" by (cases sns) auto
  show ?case
  proof (cases s)
    case True
    with Cons [of "bs" m'] P1 P2
    have e1: "subseq (rev (fst (filter_not_stri_efficient_m_aux f (a # as) bs m))) ((rev bs) @ as)"
      by simp
    note subseq_refl = subseq_order.order.refl
    from e1 list_emb_append_mono [OF subseq_refl [of "rev bs"] list_emb_Cons [OF subseq_refl [of as], of a]]
      and subseq_trans show ?thesis by simp
  next
    case False with Cons [of "a # bs" m'] P1 P2 show ?thesis by simp
  qed
qed auto

lemma filter_not_stri_efficient_m_subseq:
  "subseq (fst (filter_not_stri_efficient_m f as m)) as"
proof -
  obtain ys m' where Hrew: "filter_not_stri_efficient_m_aux f as [] m = (ys, m')"
    by (cases "filter_not_stri_efficient_m_aux f as [] m") auto
  with filter_not_stri_efficient_m_aux_subseq[of f as "[]" m]
  have "subseq (rev ys) as" by simp
  thus ?thesis using Hrew unfolding filter_not_stri_efficient_m_def by simp
qed

lemma filter_not_stri_efficient_m_submultiset:
  "mset (fst (filter_not_stri_efficient_m f as m)) ⊆# mset as"
  using subseq_submultiset filter_not_stri_efficient_m_subseq by force

lemma filter_not_stri_efficient_m_subset:
  "set (fst (filter_not_stri_efficient_m f as m)) ≤ set as"
  using subseq_subset filter_not_stri_efficient_m_subseq by force

lemma length_filter_not_stri_efficient_m[simp]:
 "length (fst (filter_not_stri_efficient_m f as m)) ≤ length as"
  using list_emb_length filter_not_stri_efficient_m_subseq by force

fun diag_l :: "('a × 'b) ⇒ (('a × 'a) × 'b)" where
  "diag_l (a, b) = ((a, a), b)"

(** Efficient version of lex_ext **)

fun lex_ext_efficient_m :: "('a ⇒ 'a ⇒ ('m, bool × bool) memo) ⇒ 'a list ⇒ 'a list ⇒ ('m, bool × bool) memo"
where
  "lex_ext_efficient_m f []     []     m = ((False, True), m)" |
  "lex_ext_efficient_m f (_#_)  []     m = ((True, True), m)" |
  "lex_ext_efficient_m f []     (_#_)  m = ((False, False), m)" |
  "lex_ext_efficient_m f (a#as) (b#bs) m = (let ((s,ns),m') = f a b m in
     if s then ((True, True), m')
          else if ns then (lex_ext_efficient_m f as bs m')
                     else ((False, False), m'))"

(** congruence lemmas needed for rpo's termination proof **)

lemma lex_ext_efficient_m_cong[fundef_cong] : fixes f g ss ts m
  assumes "⋀ s t m. ⟦s ∈ set ss; t ∈ set ts⟧ ⟹ f s t m = g s t m"
  shows "lex_ext_efficient_m f ss ts m = lex_ext_efficient_m g ss ts m"
using assms 
proof (induct ss arbitrary: ts m)
  case Nil
  thus ?case by (cases ts, auto)
next
  case (Cons s ss) note oCons = this
  show ?case 
  proof (cases ts)
    case (Cons t ts')
    with oCons have id: "g s t m = f s t m" by simp
    show ?thesis
    proof (cases "f s t m")
      case (Pair res m')
      from oCons Cons have id2: "lex_ext_efficient_m f ss ts' m' = lex_ext_efficient_m g ss ts' m'" by auto
      show ?thesis
        by (simp add: Pair Cons id, cases res, auto simp: id2)
    qed
  qed auto
qed

(** Efficient version of mul_ext **)

fun mul_ext_efficient_m :: "('a ⇒ 'a ⇒ ('m, bool × bool) memo) ⇒ 'a list ⇒ 'a list ⇒ ('m, bool × bool) memo"
and mul_ex_dom_efficient_m :: "('a ⇒ 'a ⇒ ('m, bool × bool) memo) ⇒ 'a list ⇒ 'a list ⇒ 'a ⇒ 'a list ⇒ ('m, bool × bool) memo"
where
  "mul_ext_efficient_m f [] []       m = ((False, True), m)"
| "mul_ext_efficient_m f [] _        m = ((False, False),m)"
| "mul_ext_efficient_m f _  []       m = ((True, True), m)"
| "mul_ext_efficient_m f xs (y # ys) m = mul_ex_dom_efficient_m f xs [] y ys m"

| "mul_ex_dom_efficient_m f []       xs' y ys m = ((False, False), m)"
| "mul_ex_dom_efficient_m f (x # xs) xs' y ys m =
    (let ((s, ns), m') = f x y m in
      if s then
        let (ys', m2) = filter_not_stri_efficient_m (f x) ys m' in
        let ((s', ns'), m3) = mul_ext_efficient_m f (xs @ xs') ys' m2 in
        if ns' then ((True, True), m3) else mul_ex_dom_efficient_m f xs (x # xs') y ys m3
      else if ns then
        let ((s2, ns2), m4) = mul_ext_efficient_m f (xs @ xs') ys m' in
        if s2 then ((True, True), m4) else
          let ((s3, ns3), m5) = mul_ex_dom_efficient_m f xs (x # xs') y ys m4 in
          if s3 then ((True, True), m5) else ((False, ns2 ∨ ns3), m5)
      else mul_ex_dom_efficient_m f xs (x # xs') y ys m')"

lemma mul_ext_efficient_m_cong[fundef_cong]:
  assumes "⋀x y m. x ∈ set xs ⟹ y ∈ set ys ⟹ f x y m = g x y m"
  shows "mul_ext_efficient_m f xs ys m = mul_ext_efficient_m g xs ys m"
proof -
  note * = mul_ext_efficient_m.simps[simp del] mul_ex_dom_efficient_m.simps[simp del] and
       p = prod.collapse and r = refl
  have "(⋀x' y' m. x' ∈ set xs ⟹ y' ∈ set ys ⟹ f x' y' m = g x' y' m) ⟹
        mul_ext_efficient_m f xs ys m = mul_ext_efficient_m g xs ys m"
       "(⋀x' y' m. x' ∈ set (xs @ xs') ⟹ y' ∈ set (y # ys) ⟹ f x' y' m = g x' y' m) ⟹
        mul_ex_dom_efficient_m f xs xs' y ys m = mul_ex_dom_efficient_m g xs xs' y ys m" for xs' y
  proof (induct f xs ys m and f xs xs' y ys m rule: mul_ext_efficient_m_mul_ex_dom_efficient_m.induct)
    case (6 f x xs xs' y ys m)
    have [simp]: "f x y m = g x y m" (is "_ = ?g") using 6(6) by auto
    obtain s ns m' where [simp]: "g x y m = ((s, ns), m')" by (metis prod.collapse)
    have [simp]: "filter_not_stri_efficient_m (f x) ys m' = filter_not_stri_efficient_m (g x) ys m'"
      using 6(6) by (auto intro: filter_not_stri_efficient_m)
    obtain ys' m2 where [simp]: "filter_not_stri_efficient_m (g x) ys m' = (ys', m2)" by (metis prod.collapse)
    have [simp]: "s ⟹ mul_ext_efficient_m f (xs @ xs') ys' m2 = mul_ext_efficient_m g (xs @ xs') ys' m2"
      using 6(6) filter_not_stri_efficient_m_subset[of "g x" ys m']
      by (auto intro!: 6(1)[OF r p p _ r, of _ _ m'])
    obtain s' ns' m3 where [simp]: "mul_ext_efficient_m g (xs @ xs') ys' m2 = ((s', ns'), m3)" by (metis prod.collapse)
    have [simp]: "¬ s ⟹ ns ⟹ mul_ext_efficient_m f (xs @ xs') ys m' = mul_ext_efficient_m g (xs @ xs') ys m'"
      using 6(6) by (auto intro: 6(3)[OF r p p])
    obtain s2 ns2 m4 where [simp]: "mul_ext_efficient_m g (xs @ xs') ys m' = ((s2, ns2), m4)" by (metis prod.collapse)
    have [simp]: "¬ s ⟹ ns ⟹ ¬ s2 ⟹ mul_ex_dom_efficient_m f xs (x # xs') y ys m4 = mul_ex_dom_efficient_m g xs (x # xs') y ys m4"
      using 6(6) by (auto intro: 6(4)[OF r p p _ _ r p p, of m', simplified])
    show ?case unfolding mul_ex_dom_efficient_m.simps using 6(6)
    by (auto intro: 6(2)[OF r p p _ r p r p p, of m', simplified]
      6(5)[OF r p p, simplified])
  qed (auto simp: *)
  then show ?thesis using assms by auto
qed

(** Efficient version of rpo that uses a memory. *)

fun rpo_efficient_m ::
 "('m, ('f,'v) term × ('f, 'v) term, bool × bool) memory ⇒ 'f prec_fct ⇒ 'f status_fct ⇒
  ('f,'v) term ⇒ ('f,'v) term ⇒ ('m, bool × bool) memo" where
 "rpo_efficient_m model pr tag s t m = (case (memory.lookup model m (s,t)) of
      Some v ⇒ (v, m)
    | None ⇒ let (res, res_m) =
    (case (s,t) of
       (Var x, Var y) ⇒ ((False, x = y), m)
     | (Var x, Fun g ts) ⇒ ((False, ts = [] ∧ (snd pr) (g,0)), m)
     | (Fun f ss, Var y) ⇒ diag_l (any_nstri_efficient_m (λs. rpo_efficient_m model pr tag s (Var y)) ss m)
     | (Fun f ss, Fun g ts) ⇒
     (let (any, m') = any_nstri_efficient_m (λs. rpo_efficient_m model pr tag s (Fun g ts)) ss m in
      if any then ((True, True), m')
             else let m = length ss in let n = length ts in
                  let (prs, prns) = fst pr (f,m) (g,n) in
                  if prns
                  then let (all, m'') = all_stri_efficient_m (rpo_efficient_m model pr tag (Fun f ss)) ts m' in
                       if all
                       then if prs
                            then ((True, True), m'')
                            else let cf = tag (f,m) in
                                 if cf = tag (g,n)
                                 then if cf = Mul
                                      then mul_ext_efficient_m (rpo_efficient_m model pr tag) ss ts m''
                                      else lex_ext_efficient_m (rpo_efficient_m model pr tag) ss ts m''
                                 else let b = (n = 0) in ((m ≠ 0 ∧ b, b), m'')
                       else ((False, False), m'')
                  else ((False, False), m')
    )) in (res, memory.store model res_m ((s, t), res)))"


(** Now that all the functions are defined and proved terminating,
    we prove their soundness. This soundness is obviously true iff
    the provided memory is satisfactory. *)

locale memoized_rpo =
  fixes model :: "('m, ('f,'v) term × ('f, 'v) term, bool × bool)memory"
  fixes model_P  :: "('m, ('f, 'v)term × ('f, 'v)term, bool × bool)memory ⇒ 'm
                    ⇒ ((('f, 'v)term × ('f, 'v)term) ⇒ bool × bool) ⇒ bool"
  assumes model_satisfactory: "satisfactory model_P model"
begin

abbreviation rpo_efficient where "rpo_efficient ≡ rpo_efficient_m model"
definition m_rpo_valid where
  "m_rpo_valid pr tag m = model_P model m (λp. rpo_unbounded_impl pr tag (fst p) (snd p))"

lemma lookup_valid:
  assumes "model_P model m f"
  shows "valid model m f"
using model_satisfactory assms by simp

lemma store_valid:
  assumes "model_P model M f"
  shows "model_P model (memory.store model M (a, f a)) f"
using model_satisfactory assms by (cases a) auto

(** Our auxiliary functions are sound. *)

lemma any_nstri_efficient_m_sound:
  assumes "⋀s m. s ∈ set ss ∧ m_valid f m ⟹ fst (fE s m) = f s t ∧ m_valid f (snd (fE s m))"
  and "m_valid f m"
  shows "m_valid f (snd (any_nstri_efficient_m fE ss m))
         ∧ fst (any_nstri_efficient_m fE ss m) = (∃ s ∈ set ss. snd (f s t))"
using assms proof (induct ss arbitrary: m)
case Nil
  have "any_nstri_efficient_m fE [] m = (False,m)" by simp
  moreover have "(∃ s ∈ set []. snd (f s t)) = False" by simp
  ultimately show ?case using Nil(2) by simp
next
case (Cons u us)
  obtain v m' where fE_val: "fE u m = (v, m')" by (cases "fE u m") auto
  hence m':"snd (fE u m) = m'" by simp
  from Cons have u_vals_sound:"fst (fE u m) = f u t ∧ m_valid f (snd (fE u m))" by simp
  with m' have m'_valid:"m_valid f m'" by (simp add: assms)
  obtain s ns where v_def: "v = (s, ns)" by (cases v) auto
  with u_vals_sound fE_val have f_val:"f u t = (s, ns)" by simp
  show ?case
  proof (cases ns)
  case True
    with v_def fE_val have "snd (any_nstri_efficient_m fE (u # us) m) = m'" by simp
    with m'_valid have valid_memory: "m_valid f (snd (any_nstri_efficient_m fE (u # us) m))" by simp
    from True v_def fE_val have any_nstri_efficient_m_val:
     "fst (any_nstri_efficient_m fE (u # us) m) = True" by simp
    from True f_val have ex_val:"(∃ s ∈ set (u # us). snd (f s t)) = True" by simp
    with any_nstri_efficient_m_val valid_memory show ?thesis by simp
  next
  case False
    with v_def fE_val have any_nstri_efficient_m_val:
     "any_nstri_efficient_m fE (u # us) m = any_nstri_efficient_m fE us m'" by simp
    from Cons(2) have "⋀s m. s ∈ set us ∧ m_valid f m ⟹ fst (fE s m) = f s t
     ∧ m_valid f (snd (fE s m))" by simp
    with Cons(1)[of m'] m'_valid have rec:"m_valid f (snd (any_nstri_efficient_m fE us m'))
     ∧ fst (any_nstri_efficient_m fE us m') = (∃ s ∈ set us. snd (f s t))" by simp
    from f_val False have ex_val:"(∃ s ∈ set (u # us). snd (f s t)) = (∃s ∈ set us. snd (f s t))"
     by simp
    with rec any_nstri_efficient_m_val show ?thesis by simp
  qed
qed

lemma all_stri_efficient_m_sound:
  assumes "⋀t m. t ∈ set ts ∧ m_valid f m ⟹ fst (fE t m) = f s t ∧ m_valid f (snd (fE t m))"
  and "m_valid f m"
  shows "m_valid f (snd (all_stri_efficient_m fE ts m))
   ∧ fst (all_stri_efficient_m fE ts m) = (∀ t ∈ set ts. fst (f s t))"
using assms proof (induct ts arbitrary: m)
case Nil
  have "all_stri_efficient_m fE [] m = (True, m)" by simp
  moreover have "(∀ t ∈ set []. fst (f s t)) = True" by simp
  ultimately show ?case using Nil(2) by simp
next
case (Cons u us)
  obtain v m' where fE_val: "fE u m = (v, m')" by (cases "fE u m") auto
  hence m':"snd (fE u m) = m'" by simp
  from Cons have u_vals_sound:"fst (fE u m) = f s u ∧ m_valid f (snd (fE u m))" by simp
  with m' have m'_valid: "m_valid f m'" by (simp add: assms)
  obtain stri nstri where v_def: "v = (stri, nstri)" by (cases v) auto
  with u_vals_sound fE_val have f_val:"f s u = (stri, nstri)" by simp
  show ?case
  proof (cases stri)
  case False
    with v_def fE_val have "snd (all_stri_efficient_m fE (u # us) m) = m'" by simp
    with m'_valid have valid_memory:"m_valid f (snd (all_stri_efficient_m fE (u # us) m))" by simp
    from False v_def fE_val have all_stri_efficient_m_val:
     "fst (all_stri_efficient_m fE (u # us) m) = False" by simp
    with False f_val valid_memory show ?thesis by simp
  next
  case True
    with v_def fE_val have all_stri_efficient_m_val:
     "all_stri_efficient_m fE (u # us) m = all_stri_efficient_m fE us m'" by simp
    from Cons(2) have "⋀t m. t ∈ set us ∧ m_valid f m ⟹ fst (fE t m) = f s t
     ∧ m_valid f (snd (fE t m))" by simp
    with Cons(1)[of m'] m'_valid have rec:"m_valid f (snd (all_stri_efficient_m fE us m'))
     ∧ fst (all_stri_efficient_m fE us m') = (∀ t ∈ set us. fst (f s t))" by simp
    from f_val True have all_val:"(∀ t ∈ set (u # us). fst (f s t)) = (∀ t ∈ set us. fst (f s t))"
     by simp
    with rec all_stri_efficient_m_val show ?thesis by simp
  qed
qed

lemma filter_not_stri_efficient_m_aux_sound:
  assumes "⋀t m. t ∈ set ts ∧ model_P model m f ⟹ fst (fE t m) = f (s, t) ∧ model_P model (snd (fE t m)) f"
  and "model_P model m f"
  and "∀ t ∈ set res. ¬ fst (f (s, t))"
  shows "model_P model (snd (filter_not_stri_efficient_m_aux fE ts res m)) f
   ∧ rev (fst (filter_not_stri_efficient_m_aux fE ts res m)) = [t← ((rev res) @ ts) . ¬ fst (f (s, t))]"
using assms proof (induct ts arbitrary: m res)
case Nil show ?case
  proof (rule conjI)
    from Nil(2) show "model_P model (snd (filter_not_stri_efficient_m_aux fE [] res m)) f" by simp
    from Nil(3) show "rev (fst (filter_not_stri_efficient_m_aux fE [] res m))
     = [t← (rev res @ []) . ¬ fst (f (s, t))]" by (induct res, simp_all)
  qed
next
case (Cons u us)
  obtain v m' where fE_val: "fE u m = (v, m')" by (cases "fE u m") auto
  hence m':"snd (fE u m) = m'" by simp
  from Cons have u_vals_sound:"fst (fE u m) = f (s, u) ∧ model_P model (snd (fE u m)) f" by simp
  with m' have m'_valid: "model_P model m' f" by (simp add: assms)
  obtain stri nstri where v_def: "v = (stri, nstri)" by (cases v) auto
  with u_vals_sound fE_val have f_val:"f (s, u) = (stri, nstri)" by simp
  show ?case
  proof (cases stri)
  case True
    with v_def fE_val
     have all_stri_efficient_m_val: "filter_not_stri_efficient_m_aux fE (u # us) res m
     = filter_not_stri_efficient_m_aux fE us res m'" by simp
    from f_val True have nfsu: "(¬ fst (f (s, u))) = False" by simp
    from Cons(2) have "⋀t m. t ∈ set us ∧ model_P model m f ⟹ fst (fE t m) = f (s, t)
     ∧ model_P model (snd (fE t m)) f" by simp
    with Cons(1)[of m' res] Cons(4) m'_valid all_stri_efficient_m_val nfsu
     show ?thesis by simp
  next
  case False
    with v_def fE_val
     have all_stri_efficient_m_val: "filter_not_stri_efficient_m_aux fE (u # us) res m
      = filter_not_stri_efficient_m_aux fE us (u # res) m'" by simp
    from Cons(4) False f_val have acc_sound: "∀t ∈ set (u # res). ¬ fst (f (s, t))" by simp
    from Cons(2) have "⋀t m. t ∈ set us ∧ model_P model m f ⟹ fst (fE t m) = f (s, t)
     ∧ model_P model (snd (fE t m)) f" by simp
    with Cons(1)[of m' "u # res"] acc_sound m'_valid all_stri_efficient_m_val
     show ?thesis by simp
  qed
qed

lemma filter_not_stri_efficient_m_sound:
  assumes "⋀t m. t ∈ set ts ∧ model_P model m f ⟹ fst (fE t m) = f (s, t) ∧ model_P model (snd (fE t m)) f"
  and "model_P model m f"
  shows "model_P model (snd (filter_not_stri_efficient_m fE ts m)) f
   ∧ fst (filter_not_stri_efficient_m fE ts m) = [y←ts . ¬ fst (f (s, y))]"
proof -
obtain ys m' where Hrew: "filter_not_stri_efficient_m_aux fE ts [] m = (ys, m')"
 by (cases "filter_not_stri_efficient_m_aux fE ts [] m") auto
from filter_not_stri_efficient_m_aux_sound[OF assms(1) assms(2), of ts "λ_ m. m" "[]"] assms Hrew
show ?thesis unfolding filter_not_stri_efficient_m_def by simp
qed

(** lex_ext_efficient_m is sound **)

declare lex_ext_unbounded.simps[simp]

lemma lex_ext_efficient_m_sound:
  assumes "⋀t s m.  s ∈ set ss ∧ t ∈ set ts ∧ model_P model m f ⟹ fst (fE s t m) = f (s, t)
   ∧ model_P model (snd (fE s t m)) f"
  and "model_P model m f"
  shows "model_P model (snd (lex_ext_efficient_m fE ss ts m)) f
   ∧ fst (lex_ext_efficient_m fE ss ts m) = lex_ext_unbounded (λs t. f (s, t)) ss ts"
using assms proof (induct ss ts arbitrary: m rule: List.list_induct2')
case (1 m)
  have "lex_ext_efficient_m fE [] [] m = ((False,True),m)" by simp
  moreover have "lex_ext_unbounded (λ s t. f (s, t)) [] [] = (False, True)" by simp
  ultimately show ?case using 1(2) by simp
next
case (2 a as m)
  have "lex_ext_efficient_m fE (a # as) [] m = ((True,True),m)" by simp
  moreover have "lex_ext_unbounded (λs t. f (s, t)) (a # as) [] = (True, True)" by simp
  ultimately show ?case using 2(2) by simp
next
case (3 b bs m)
  have "lex_ext_efficient_m fE [] (b # bs) m = ((False,False),m)" by simp
  moreover have "lex_ext_unbounded (λs t. f (s, t)) [] (b # bs)  = (False, False)" by simp
  ultimately show ?case using 3(2) by simp
next
case (4 a as b bs m)
  obtain v m' where fE_val: "fE a b m = (v, m')" by (cases "fE a b m") auto
  from 4(2)[of a b m] 4(3) have fE_sound: "fst (fE a b m) = f (a, b) ∧ model_P model (snd (fE a b m)) f"
   by simp
  with fE_val have m'_valid: "model_P model m' f" by simp
  obtain s ns where v_def: "v = (s, ns)" by (cases v) auto
  with fE_sound fE_val have f_val:"f (a, b) = (s,ns)" by simp
  show ?case
  proof (cases s)
  case True
    with fE_val v_def have lex_ext_efficient_m_val:
     "lex_ext_efficient_m fE (a # as) (b # bs) m = ((True,True),m')" by simp
    from f_val True
     have lex_ext_unbounded_val:"lex_ext_unbounded (λs t. f (s, t)) (a # as) (b # bs) = (True,True)"
     by simp
    with m'_valid lex_ext_efficient_m_val show ?thesis by simp
  next
  case False note sFalse = this
    show ?thesis
    proof (cases ns)
    case True
      from 4(2) have "⋀s t m. s ∈ set as ∧ t ∈ set bs ∧ model_P model m f ⟹ fst (fE s t m) = f (s, t)
       ∧ model_P model (snd (fE s t m)) f" by simp
      from this 4(1)[of m'] m'_valid have rec: "model_P model (snd (lex_ext_efficient_m fE as bs m')) f
       ∧ fst (lex_ext_efficient_m fE as bs m') = lex_ext_unbounded (λs t. f (s, t)) as bs"
       by simp
      from sFalse True v_def fE_val
       have lex_ext_efficient_m_val: "lex_ext_efficient_m fE (a # as) (b # bs) m
       = lex_ext_efficient_m fE  as bs m'" by simp
      from sFalse True f_val
       have lex_ext_unbounded_val:"lex_ext_unbounded (λs t. f (s, t)) (a # as) (b # bs)
       = lex_ext_unbounded (λs t. f (s, t)) as bs" by simp
      with lex_ext_efficient_m_val rec show ?thesis by simp
    next
    case False
      with sFalse v_def fE_val have lex_ext_efficient_m_val:
       "lex_ext_efficient_m fE (a # as) (b # bs) m = ((False,False),m')" by simp
      from sFalse False f_val 
       have lex_ext_unbounded_val: "lex_ext_unbounded (λs t. f (s, t)) (a # as) (b # bs) = (False,False)"
       by simp
      with lex_ext_efficient_m_val m'_valid show ?thesis by simp
    qed
  qed
qed

declare lex_ext_unbounded.simps[simp del]

(** mul_ext_efficient_m is sound *)

lemma mul_ext_impl_s_imp_ns:
  "fst (mul_ext_impl f xs ys) ⟹ snd (mul_ext_impl f xs ys)"
by (auto simp: mul_ext_impl_sound0 mult2_impl_sound mult2_alt_ns_conv)

lemma mul_ex_dom_s_imp_ns:
  "fst (mul_ex_dom f xs xs' y ys) ⟹ snd (mul_ex_dom f xs xs' y ys)"
by (auto simp:mul_ext_impl_sound0 mult2_impl_sound mult2_alt_ns_conv)

lemma mul_ext_efficient_m_sound:
  assumes "⋀t s m. s ∈ set ps ∧ t ∈ set qs ∧ model_P model m f ⟹ fst (fE s t m) = f (s, t)
   ∧ model_P model (snd (fE s t m)) f"
  and "model_P model m f"
  shows
   "model_P model (snd (mul_ext_efficient_m fE ps qs m)) f
     ∧ fst (mul_ext_efficient_m fE ps qs m) = mul_ext_impl (λs t. f (s, t)) ps qs"
proof -
  note * = mul_ext_efficient_m.simps[simp del] mul_ex_dom_efficient_m.simps[simp del]
       mul_ext_impl.simps[simp del] mul_ex_dom.simps[simp del] and filter.simps[simp del]
       and p = prod.collapse and r = refl
  have
    "(⋀m. model_P model m f ⟹
      (⋀x y. x ∈ set xs ⟹ y ∈ set ys ⟹
        fst (fE x y m) = f (x, y) ∧ model_P model (snd (fE x y m)) f)) ⟹
     model_P model m f ⟹ model_P model (snd (mul_ext_efficient_m fE xs ys m)) f
       ∧ fst (mul_ext_efficient_m fE xs ys m) = mul_ext_impl (λx y. f (x, y)) xs ys"
    "(⋀m. model_P model m f ⟹
      (⋀x z. x ∈ set (xs @ xs') ⟹ z ∈ set (y # ys) ⟹
        fst (fE x z m) = f (x, z) ∧ model_P model (snd (fE x z m)) f)) ⟹
     model_P model m f ⟹ model_P model (snd (mul_ex_dom_efficient_m fE xs xs' y ys m)) f
       ∧ fst (mul_ex_dom_efficient_m fE xs xs' y ys m) = mul_ex_dom (λx y. f (x, y)) xs xs' y ys"
    for xs xs' y ys
  proof (induct fE xs ys m and fE xs xs' y ys m rule: mul_ext_efficient_m_mul_ex_dom_efficient_m.induct)
    case (6 fE x xs xs' y ys m)
    have "model_P model (snd (fE x y m)) f ∧ fst (fE x y m) = f (x, y)" using 6(6,7) by auto
    then obtain s ns m' where [simp]: "fE x y m = ((s, ns), m')" "model_P model m' f" "f (x, y) = (s, ns)"
       by (metis prod.collapse)
    have "s ⟹ model_P model (snd (filter_not_stri_efficient_m (fE x) ys m')) f ∧
      fst (filter_not_stri_efficient_m (fE x) ys m') = [y←ys . ¬ fst (f (x, y))]"
      using 6(6) by (intro filter_not_stri_efficient_m_sound) auto
    then obtain ys' m2 where [simp]: "s ⟹ filter_not_stri_efficient_m (fE x) ys m' = (ys', m2)"
       "s ⟹ model_P model m2 f" and ys'[simp]: "s ⟹ [y←ys . ¬ fst (f (x, y))] = ys'" by (metis prod.collapse)
    have "s ⟹ set ys' ⊆ set ys" unfolding ys'[symmetric] by (auto simp del: ys')
    then have "s ⟹ model_P model (snd (mul_ext_efficient_m fE (xs @ xs') ys' m2)) f ∧
      fst (mul_ext_efficient_m fE (xs @ xs') ys' m2) = mul_ext_impl (λx y. f (x, y)) (xs @ xs') ys'"
      using 6(6) by (intro 6(1)[OF r p p _ r p, of m', simplified]) auto
    then obtain s' ns' m3 where [simp]: "s ⟹ mul_ext_efficient_m fE (xs @ xs') ys' m2 = ((s', ns'), m3)"
       "s ⟹ mul_ext_impl (λx y. f (x, y)) (xs @ xs') ys' = (s', ns')"
       "s ⟹ model_P model m3 f" "s ⟹ s' ⟹ ns'" by (metis prod.collapse mul_ext_impl_s_imp_ns)
    have x: "s ⟹ ¬ ns' ⟹ model_P model (snd (mul_ex_dom_efficient_m fE xs (x # xs') y ys m3)) f ∧
      fst (mul_ex_dom_efficient_m fE xs (x # xs') y ys m3) = mul_ex_dom (λx y. f (x, y)) xs (x # xs') y ys"
      using 6(6) by (intro 6(2)[OF r p p _ r p p p p, of m']) auto
    have "¬ s ⟹ ns ⟹ model_P model (snd (mul_ext_efficient_m fE (xs @ xs') ys m')) f ∧
      fst (mul_ext_efficient_m fE (xs @ xs') ys m') = mul_ext_impl (λx y. f (x, y)) (xs @ xs') ys"
      using 6(6) by (intro 6(3)[OF r p p, simplified]) auto
    then obtain s2 ns2 m4 where [simp]: "¬ s ⟹ ns ⟹ mul_ext_efficient_m fE (xs @ xs') ys m' = ((s2, ns2), m4)"
      "¬ s ⟹ ns ⟹ model_P model m4 f" "¬ s ⟹ ns ⟹ mul_ext_impl (λx y. f (x, y)) (xs @ xs') ys = (s2, ns2)"
      "¬ s ⟹ ns ⟹ s2 ⟹ ns2" by (metis prod.collapse mul_ext_impl_s_imp_ns)
    have "¬ s ⟹ ns ⟹ ¬ s2 ⟹ model_P model (snd (mul_ex_dom_efficient_m fE xs (x # xs') y ys m4)) f ∧
      fst (mul_ex_dom_efficient_m fE xs (x # xs') y ys m4) = mul_ex_dom (λx y. f (x, y)) xs (x # xs') y ys"
      using 6(6) by (intro 6(4)[OF r p p _ _ r p p, of m']) auto
    then obtain s3 ns3 m5 where [simp]: "¬ s ⟹ ns ⟹ ¬ s2 ⟹ mul_ex_dom_efficient_m fE xs (x # xs') y ys m4 = ((s3, ns3), m5)"
      "¬ s ⟹ ns ⟹ ¬ s2 ⟹ mul_ex_dom (λx y. f (x, y)) xs (x # xs') y ys = (s3, ns3)"
      "¬ s ⟹ ns ⟹ ¬ s2 ⟹ model_P model m5 f"
      "¬ s ⟹ ns ⟹ ¬ s2 ⟹ s3 ⟹ ns3" by (metis prod.collapse mul_ex_dom_s_imp_ns)
    have y: "¬ s ⟹ ¬ ns ⟹ model_P model (snd (mul_ex_dom_efficient_m fE xs (x # xs') y ys m')) f ∧
      fst (mul_ex_dom_efficient_m fE xs (x # xs') y ys m') = mul_ex_dom (λx y. f (x, y)) xs (x # xs') y ys"
    using 6(6) by (intro 6(5)[OF r p p, simplified]) auto
    show ?case unfolding mul_ex_dom_efficient_m.simps(2) mul_ex_dom.simps(2)
    using x y by simp
  qed (auto simp: *)
  then show ?thesis using assms by simp
qed

(** The efficient version of RPO is sound *)

lemma m_rpo_valid_sound:
  assumes "m_rpo_valid pr tag m"
  and "memory.lookup model m (p,q) = Some v"
  shows "rpo_unbounded_impl pr tag p q = v"
using assms lookup_valid[of m "λp. rpo_unbounded_impl pr tag (fst p) (snd p)"]
unfolding m_rpo_valid_def valid_def by (cases v) auto

lemma store_rpo_sound :
  assumes "m_rpo_valid pr tag m"
  and "rpo_unbounded_impl pr tag s t = v"
  shows "m_rpo_valid pr tag (memory.store model m ((s,t),v))"
using assms store_valid[of m "λp. rpo_unbounded_impl pr tag (fst p) (snd p)"]
unfolding m_rpo_valid_def by auto

lemma rpo_efficient_sound:
 assumes "m_rpo_valid pr tag m"
 shows "m_rpo_valid pr tag (snd (rpo_efficient pr tag p q m))
  ∧ fst (rpo_efficient pr tag p q m) = rpo_unbounded_impl pr tag p q"
proof (cases "memory.lookup model m (p, q)")
case (Some v) thus ?thesis using assms m_rpo_valid_sound by simp
next
case None thus ?thesis using assms
  proof (induct p arbitrary: q m)
  case (Var x q m) thus ?case using store_rpo_sound by (cases q) auto
  next
  case (Fun f ss q m) note IH = this
    {
      fix s m assume s_in_ss: "s ∈ set ss" and m_valid: "m_rpo_valid pr tag m"
      have "fst (rpo_efficient pr tag s q m) = rpo_unbounded_impl pr tag s q
       ∧ m_rpo_valid pr tag (snd (rpo_efficient pr tag s q m))"
      proof (cases "memory.lookup model m (s, q)")
      case (Some v) thus ?thesis using m_valid m_rpo_valid_sound by simp
      next
      case None from IH(1)[OF s_in_ss None m_valid] show ?thesis by simp
      qed
    }
    hence rec: "⋀s m. s ∈ set ss ⟹ m_rpo_valid pr tag m ⟹
     fst (rpo_efficient pr tag s q m) = rpo_unbounded_impl pr tag s q
       ∧ m_rpo_valid pr tag (snd (rpo_efficient pr tag s q m))" by simp
    thus ?case using IH(2) IH(3)
    proof (induct q arbitrary: m)
    case (Var y m) note Hq = this
      obtain v m' where any_ns: "any_nstri_efficient_m (λs. rpo_efficient pr tag s (Var y))
       ss m = (v, m')" by (cases "any_nstri_efficient_m (λs. rpo_efficient pr tag s (Var y)) ss m") auto
      with any_nstri_efficient_m_sound[of ss "λf M. model_P model M (λp. f (fst p) (snd p))",
       OF _ Hq(3)[unfolded m_rpo_valid_def], of "λs. rpo_efficient pr tag s (Var y)" "Var y"] Hq(1)
       have any_ns': "(∃s∈set ss. snd (rpo_unbounded_impl pr tag s (Var y))) = v"
       and m'_valid: "m_rpo_valid pr tag m'" unfolding m_rpo_valid_def by auto
      show ?case using Hq(2) any_ns any_ns' m'_valid store_rpo_sound by simp
    next
    case (Fun g ts) note Hq = this
      obtain any m' where any_ns: "any_nstri_efficient_m (λs. rpo_efficient pr tag s (Fun g ts))
       ss m = (any, m')"
       by (cases "any_nstri_efficient_m (λs. rpo_efficient pr tag s (Fun g ts)) ss m") auto
      with any_nstri_efficient_m_sound[of ss "λf M. model_P model M (λp. f (fst p) (snd p))",
       OF _ Hq(4)[unfolded m_rpo_valid_def], of "λs. rpo_efficient pr tag s (Fun g ts)"] Hq(2)
       have any_ns': "(∃s∈set ss. snd (rpo_unbounded_impl pr tag s (Fun g ts))) = any"
        and m'_valid: "m_rpo_valid pr tag m'" unfolding m_rpo_valid_def by auto
      show ?case
      proof (cases any)
      case True note Hany = this
        thus ?thesis using Hq(3) Hq(4) any_ns any_ns' m'_valid store_rpo_sound by simp
      next
      case False note Hany = this
        let ?m = "length ss"
        let ?n = "length ts"
        obtain s ns where Hpr: "fst pr (f, ?m) (g,?n) = (s, ns)" by force
        show ?thesis
        proof (cases ns)
        case False with Hq(3) any_ns any_ns' Hany Hpr m'_valid store_rpo_sound show ?thesis by simp
        next
        case True note Hns = this
          obtain all m2 where all_s: "all_stri_efficient_m (rpo_efficient_m model pr tag
           (Fun f ss)) ts m' = (all, m2)"
           by (cases "all_stri_efficient_m (rpo_efficient_m model pr tag (Fun f ss)) ts m'") auto
          {
            fix t m
            assume t_in_ts: "t ∈ set ts" and m_valid: "m_rpo_valid pr tag m"
            have "fst (rpo_efficient pr tag (Fun f ss) t m) = rpo_unbounded_impl pr tag (Fun f ss) t
             ∧ m_rpo_valid pr tag (snd (rpo_efficient pr tag (Fun f ss) t m))"
            proof (cases "memory.lookup model m (Fun f ss, t)")
            case (Some v) thus ?thesis using m_valid m_rpo_valid_sound by simp
            next
            case None
              {
                fix s m'
                assume s_in_ss: "s ∈ set ss" and m'_valid: "m_rpo_valid pr tag m'"
                have "fst (rpo_efficient pr tag s t m') = rpo_unbounded_impl pr tag s t ∧
                 m_rpo_valid pr tag (snd (rpo_efficient pr tag s t m'))"
                proof (cases "memory.lookup model m' (s, t)")
                case (Some v) thus ?thesis using m'_valid m_rpo_valid_sound by simp
                next
                case None from IH(1)[OF s_in_ss None m'_valid] show ?thesis by simp
                qed
              }
              with Hq(1)[OF t_in_ts _ None m_valid] IH(1) show ?thesis by simp
            qed  
          }
          with all_stri_efficient_m_sound[of ts "λf M. model_P model M (λp. f (fst p) (snd p))",
           OF _ m'_valid[unfolded m_rpo_valid_def], of "rpo_efficient pr tag (Fun f ss)"] all_s
           have all_s': "(∀t∈set ts. fst (rpo_unbounded_impl pr tag (Fun f ss) t)) = all"
            and m2_valid: "m_rpo_valid pr tag m2" unfolding m_rpo_valid_def by auto
          show ?thesis
          proof (cases s)
          case True
            with Hq(3) any_ns any_ns' all_s all_s' Hany Hns Hpr m2_valid store_rpo_sound
             show ?thesis by simp
          next
          case False note Hs = this
            show ?thesis
            proof (cases all)
            case False note Hall = this
              from Hq(3) any_ns any_ns' all_s all_s' Hall Hany Hns Hpr Hs store_rpo_sound
               m2_valid show ?thesis by (simp add: all_s' Hall)
            next
            case True note Hall = this
              let ?cf = "tag (f, ?m)"
              let ?cg = "tag (g, ?n)"
              show ?thesis
              proof (cases "?cf = ?cg")
              case False
                with Hq(3) any_ns any_ns' all_s all_s' Hall Hany Hns Hs Hpr m2_valid store_rpo_sound
                 show ?thesis by (cases ts, simp_all)
              next
              case True note cfg = this
                {
                  fix t s m
                  assume s_in_ss: "s ∈ set ss" and t_in_ts: "t ∈ set ts"
                   and m_valid: "m_rpo_valid pr tag m"
                  have "fst (rpo_efficient pr tag s t m) = rpo_unbounded_impl pr tag s t
                   ∧ m_rpo_valid pr tag (snd (rpo_efficient pr tag s t m))"
                  proof (cases "memory.lookup model m (s, t)")
                  case (Some v) thus ?thesis using m_valid m_rpo_valid_sound by simp
                  next
                  case None from IH(1)[OF s_in_ss None m_valid] show ?thesis by simp
                  qed
                } note rec = this
                show ?thesis
                proof (cases ?cf)
                case Mul note cf = this
                  obtain v m3 where mext: "mul_ext_efficient_m (rpo_efficient pr tag) ss ts m2
                   = (v, m3)" by (cases "mul_ext_efficient_m (rpo_efficient pr tag) ss ts m2") auto
                  from rpo_unbounded_impl_sound[of "pr" tag] rpo_unbounded_stri_imp_nstri[of "pr" tag]
                   have Himp: "∀ x y. fst (rpo_unbounded_impl pr tag x y) ⟶ snd (rpo_unbounded_impl
                   pr tag x y)" by metis
                  from mul_ext_efficient_m_sound[of ss ts "λp. rpo_unbounded_impl pr tag (fst p) (snd p)"
                   "rpo_efficient pr tag" m2] Himp m2_valid[unfolded m_rpo_valid_def] mext rec
                   have mext': "mul_ext_impl (rpo_unbounded_impl pr tag) ss ts = v"
                   and m3_valid: "m_rpo_valid pr tag m3" unfolding m_rpo_valid_def by auto
                  with Hq(3) any_ns any_ns' all_s all_s' Hall Hany Hns Hs Hpr cfg cf mext
                   and store_rpo_sound show ?thesis unfolding mul_ext_impl_sound by simp
                next
                case Lex note cf = this
                  obtain v m3 where lext: "lex_ext_efficient_m (rpo_efficient pr tag) ss ts m2
                   = (v, m3)" by (cases "lex_ext_efficient_m (rpo_efficient pr tag) ss ts m2") auto
                  from lex_ext_efficient_m_sound[OF _ m2_valid[unfolded m_rpo_valid_def],
                   of ss ts "rpo_efficient pr tag"] lext rec
                   have lext': "lex_ext_unbounded (rpo_unbounded_impl pr tag) ss ts = v"
                   and m3_valid: "m_rpo_valid pr tag m3" unfolding m_rpo_valid_def by auto
                  with Hq(3) any_ns any_ns' all_s all_s' Hall Hany Hns Hs Hpr cfg cf lext
                   and store_rpo_sound show ?thesis by simp
                qed
              qed
            qed
          qed
        qed
      qed
    qed
  qed
qed

definition memoized_rpo where
  "memoized_rpo pr tag p q ≡ fst (rpo_efficient pr tag p q (memory.empty model ()))"

lemma memoized_rpo_sound:
  "memoized_rpo = rpo_unbounded_impl"
proof-
{
  fix "pr" tag p q
  from rpo_efficient_sound[of "pr" tag "memory.empty model ()"]
   model_satisfactory[unfolded satisfactory_def]
   have "memoized_rpo pr tag p q = rpo_unbounded_impl pr tag p q"
   unfolding m_rpo_valid_def memoized_rpo_def
   by simp
} thus ?thesis by (rule_tac HOL.ext)+
qed

end

(** Now that we have a parametrized version of RPO, we can try the algorithm
    with different kinds of memory implementations *)

(** Using Nagele's first model. *)


global_interpretation memoized_rpo_1 : memoized_rpo lm valid
  defines efficient_rpo_1 = memoized_rpo_1.memoized_rpo
using satisfactory_lm by unfold_locales (auto simp: efficient_rpo_1_def)

theorem rpo_efficient_1_sound: "rpo_unbounded_impl = efficient_rpo_1"
by (simp add: memoized_rpo_1.memoized_rpo_sound efficient_rpo_1_def)

(** Using Nagele's second model. *)

global_interpretation memoized_rpo_2 : memoized_rpo l2m l2m_valid
  defines efficient_rpo_2 = memoized_rpo_2.memoized_rpo
using satisfactory_l2m by (unfold_locales) (simp_all add: efficient_rpo_2_def)

theorem rpo_efficient_2_sound: "rpo_unbounded_impl = efficient_rpo_2"
  by (simp add: memoized_rpo_2.memoized_rpo_sound)

declare rpo_efficient_2_sound[code]

end