Theory RPO_Impl

(*
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_Impl
imports 
  RPO 
  "../Auxiliaries/Multiset_Extension_Impl"
begin

(* Implementation of RPO *)

fun
  rpo_unbounded_impl :: "('f × nat ⇒ 'f × nat ⇒ bool × bool) × ('f × nat ⇒ bool) ⇒
  ('f × nat ⇒ order_tag) ⇒ ('f, 'v) term ⇒ ('f, 'v) term ⇒ bool × bool"
where
  "rpo_unbounded_impl _  _ (Var x) (Var y) = (False, x = y)" |
  "rpo_unbounded_impl pr _ (Var x) (Fun g ts) = (False, ts = [] ∧ (snd pr) (g,0))" |
  "rpo_unbounded_impl pr c (Fun f ss) (Var y) = (let con = (∃ s ∈ set ss. snd (rpo_unbounded_impl pr c s (Var y))) in (con,con))" |
  "rpo_unbounded_impl pr c (Fun f ss) (Fun g ts) = (
    if (∃ s ∈ set ss. snd (rpo_unbounded_impl pr c s (Fun g ts)))
    then (True,True)
    else (case (fst pr) (f,length ss) (g,length ts) of (prs,prns) ⇒
         if prns ∧ (∀ t ∈ set ts. fst (rpo_unbounded_impl pr c (Fun f ss) t))
         then if prs
              then (True,True) 
              else let cf = c (f, length ss) in
                   if cf = c (g, length ts)
                   then if cf = Mul
                        then mul_ext (rpo_unbounded_impl pr c) ss ts
                        else lex_ext_unbounded (rpo_unbounded_impl pr c) ss ts
                   else (ss ≠ [] ∧ ts = [], ts = [])
         else (False,False)))"

(* Soundness lemma *)
lemma rpo_unbounded_impl_sound:
  shows "rpo_unbounded pr c s t = rpo_unbounded_impl pr c s t" (is "?e pr c s t")
proof (induct rule: rpo_unbounded.induct[where P = ?e])
case (2 p c x g ts) show ?case by (simp add: prl_nat_def)
next
case (4 p c f ss g ts) note IH = this
  from 4(1) have s: "⋀ s. s ∈ set ss ⟹ ?e p c s (Fun g ts)" by simp
  let ?cond = "∃ s ∈ set ss. snd (rpo_unbounded_impl p c s (Fun g ts))"
  show ?case
  proof (cases ?cond)
  case True
    with s have "∃ s ∈ set ss. snd (rpo_unbounded p c s (Fun g ts))" by simp
    with True show ?thesis by simp
  next
  case False note oFalse = this
    with s have oFalse2: "¬ (∃s ∈ set ss. snd (rpo_unbounded p c s (Fun g ts)))"
     by simp
    obtain prns prs where Hsns: "(fst p) (f,length ss) (g,length ts) = (prs, prns)" by force
    from 4(2)[OF oFalse2 Hsns[symmetric]]
     have t: "⋀ t. t ∈ set ts ⟹ ?e p c (Fun f ss) t" by force
    show ?thesis
    proof (cases "prns ∧ (∀t∈set ts. fst (rpo_unbounded_impl p c (Fun f ss) t))")
    case False
      show ?thesis
      proof (cases "prns")
      case False thus ?thesis by (simp add: oFalse oFalse2 Hsns)
      next
      case True
        with False have Hf1: "¬ (∀t∈set ts. fst (rpo_unbounded_impl p c (Fun f ss) t))" by simp
        with t have Hf2: "¬ (∀t∈set ts. fst (rpo_unbounded p c (Fun f ss) t))" by auto
        show ?thesis by (simp add: oFalse oFalse2 Hf1 Hf2)
      qed         
    next
    case True
      hence prns: "prns" and Hts: "∀t∈set ts. fst (rpo_unbounded_impl p c (Fun f ss) t)"
       by auto
      from Hts and t have Hts2: "∀t∈set ts. fst (rpo_unbounded p c (Fun f ss) t)" by auto
      show ?thesis
      proof (cases "prs")
      case True thus ?thesis by (simp add: oFalse oFalse2 Hsns prns Hts Hts2)
      next
      case False note prs = this
        show ?thesis
        proof (cases "c (f,length ss) = c (g,length ts)")
        case False thus ?thesis
         by (cases "c (f,length ss)", simp_all add: oFalse oFalse2 Hsns prns Hts Hts2)
        next
        case True note cfg = this
          show ?thesis
          proof (cases "c (f,length ss)")
          case Mul note cf = this
            with cfg have cg: "c (g,length ts) = Mul" by simp
            {
              fix x y
              assume x_in_ss: "x ∈ set ss" and y_in_ts: "y ∈ set ts"
              from 4(3)[OF oFalse2 Hsns[symmetric] _ prs cfg cf
                x_in_ss y_in_ts] prns Hts2
              have "rpo_unbounded p c x y = rpo_unbounded_impl p c x y" by auto
            }
            note Hrpo1 = this
            have "mul_ext (rpo_unbounded p c) ss ts = mul_ext (rpo_unbounded_impl p c) ss ts"
              by (rule mul_ext_cong[OF refl refl], insert Hrpo1, auto)
            thus ?thesis by (simp add: oFalse oFalse2 Hsns prns prs Hts Hts2 cf cg)
          next
            case Lex note cf = this
            with cfg have cg: "c (g,length ts) = Lex" by simp
            from cfg cf have ncf: "c (f,length ss) ≠ Mul" by simp
            {
              fix i
              assume iss: "i < length ss" and its: "i < length ts"
              from nth_mem_mset[OF iss] and in_multiset_in_set
              have in_ss: "ss ! i ∈ set ss" by force
              from nth_mem_mset[OF its] and in_multiset_in_set
              have in_ts: "ts ! i ∈ set ts" by force
              from 4(4)[OF oFalse2 Hsns[symmetric] _ prs cfg ncf iss its]
                prns Hts2
              have "rpo_unbounded p c (ss ! i) (ts ! i)
                = rpo_unbounded_impl p c (ss ! i) (ts ! i)" by simp
            }
            with lex_ext_unbounded_cong[of ss ss ts ts]
            have Hlex1: "lex_ext_unbounded (rpo_unbounded_impl p c) ss ts
              = lex_ext_unbounded (rpo_unbounded p c) ss ts" by metis
            thus ?thesis
              by (simp add: oFalse oFalse2 Hsns prns prs Hts Hts2 cfg cg)
          qed
        qed
      qed
    qed
  qed 
qed auto

(** Extracting code **)

lemma [code]: "rpo_unbounded = rpo_unbounded_impl"
  by (intro ext, simp add: rpo_unbounded_impl_sound)

end