Theory Transition_Removal

theory Transition_Removal
  imports 
    Cooperation_Program
    Ord.Lexicographic_Orders
    Ord.Non_Inf_Orders
begin

hide_const (open) FuncSet.Pi

datatype ('e,'t,'l,'tr,'h) transition_removal_info = Transition_removal_info
  (rank: "'l sharp ⇒ 'e")
  (removed: "'tr list")
  (dom_type: "'t")
  (bound_exp: "'e")
  (hinter: "'tr ⇒ 'h hint")


lemma(in Order_Pair.order_pair) chain_imp_le:
  assumes chain: "chain NS seq" and ij: "i ≤ j" shows "(seq i, seq j) ∈ NS"
proof-
  have "(seq i, seq (i+k)) ∈ NS" for k
  proof(induct k)
    case 0 show ?case by (auto intro: refl_NS_point)
  next
    case (Suc k)
    have "(seq (i+k), seq (i + Suc k)) ∈ NS" using chain by auto
    from trans_NS_point[OF Suc this] show ?case by auto
  qed
  from this[of "j-i"] ij show ?thesis by auto
qed

lemma(in SN_order_pair) chain_imp_chain_not_less:
  assumes chain: "chain NS f" shows "∃j. chain (NS-S) (shift f j)"
proof-
  from chain non_strict_ending[of f NS S] NS_O_S SN obtain j where 
    steps: "⋀ i. i ≥ j ⟹ (f i, f (Suc i)) ∈ NS - S" by (auto simp: SN_def)
  show ?thesis
    by (rule exI[of _ j], insert steps, auto)
qed

lemma(in SN_order_pair) no_chain_less[simp]: "chain S f ⟷ False" using SN by auto

lemma(in SN_order_pair) wf_order_set: "class.wf_order (λx y. (y,x) ∈ NS ∪ S) (λx y. (y,x) ∈ S)"
  apply (unfold_locales)
  apply (auto dest: trans_NS_point trans_S_point compat_NS_S_point compat_S_NS_point intro: refl_NS_point SN_induct[OF SN])
  done

context lts begin

context
  fixes less_eq less :: "'m ⇒ 'm ⇒ bool"
  assumes wf_order: "class.wf_order less_eq less"
begin

interpretation wf_order less_eq less by (fact wf_order)
interpretation ord_syntax less_eq less.

lemma transition_removal_via_rank:
  fixes rank :: "('v,'t,'d,'l sharp) state ⇒ 'm"
    and P :: "('f,'v,'t,'l sharp) lts"
  assumes TD: "∀τ ∈ TD. is_sharp_transition τ"
      and NS: "⋀ s t τ. τ ∉ TD ⟹ τ ∈ sharp_transitions_of P ⟹ s ∈ reachable_states P ⟹ t ∈ reachable_states P
                ⟹ (s,t) ∈ transition_step_lts P τ ⟹ rank s ⊒ rank t"
      and S: "⋀ s t τ. τ ∈ TD ⟹ s ∈ reachable_states P ⟹ t ∈ reachable_states P
                ⟹ (s,t) ∈ transition_step_lts P τ ⟹ rank s ⊐ rank t"
      and cSN: "cooperation_SN (delete_transitions P TD)"
  shows "cooperation_SN P"
  unfolding indexed_rewriting.cooperation_SN_on_as_SN_on_traverse
proof(intro allI impI SN_onI)
  interpret indexed_rewriting "transition_step_lts P" .
  let ?P = "delete_transitions P TD"
  fix τs seq
  assume τs: "τs ⊆ sharp_transitions_of P"
     and τs0: "τs ≠ {}"
     and init: "seq 0 ∈ transitions_steps_lts P (flat_transitions_of P) `` initial_states P"
     and chain: "chain (traverse τs) seq"
  have trans: "transitions_step_lts P τs ⊆ transition P" by (insert τs, auto)
  { fix i
    from chain[rule_format, of i]
    obtain subseq l
    where first: "subseq 0 = seq i" and last: "subseq l = seq (Suc i)" and trav: "traversed τs subseq l"
      by (rule mem_traverseE)
    have reach: "seq i ∈ reachable_states P"
    proof (induct i)
      case 0 show ?case by(rule subsetD[OF _ init], rule Image_subsetI, rule rtrancl_mono, auto)
    next
      case (Suc i)
      from chain have "step seq i ∈ traverse τs" by auto
      with traverse_subset_Induces[of "τs"]
      have "step seq i ∈ (transitions_step_lts P τs)⇧*" by auto
      also have "... ⊆ (transition P)⇧*" by (fact rtrancl_mono[OF trans])
      finally have "step seq i ∈ ...".
      with Suc have "seq (Suc i) ∈ (transition P)⇧* `` reachable_states P" by fast
      then show ?case by auto
    qed
    { fix j τs' assume jl: "j ≤ l"
      have "traversed τs' subseq j ⟹ τs' ⊆ τs ⟹
        subseq j ∈ reachable_states P ∧
        (τs' ∩ TD = {} ⟶ rank (seq i) ⊒ rank (subseq j)) ∧
        (τs' ∩ TD ≠ {} ⟶ rank (seq i) ⊐ rank (subseq j))"
      proof(insert first jl, induct rule: traversed.induct)
        case (base subseq) with reach show ?case by auto
      next
        case IH: (step τs' subseq j τ')
        then have weak: "τs' ∩ TD = {} ⟹ rank (seq i) ⊒ rank (subseq j)"
              and strict: "τs' ∩ TD ≠ {} ⟹ rank (seq i) ⊐ rank (subseq j)"
              and step: "(subseq j, subseq (Suc j)) ∈ transition_step_lts P τ'"
              and jl: "j < l"
              and τ': "τ' ∈ τs"
              and τs': "τs' ⊆ τs"
              and reach: "subseq j ∈ reachable_states P" by auto
        from IH traversed_imp_chain[OF trav] have "step subseq j ∈ transitions_step_lts P τs" by auto
        also have "... ⊆ transition P" by (rule trans)
        finally have "step subseq j ∈ ...".
        with reach have "subseq (Suc j) ∈ transition P `` reachable_states P" by auto
        also have "... ⊆ reachable_states P" by (rule rtrancl_image_unfold_right)
        finally have *: "subseq (Suc j) ∈ ...".
        have weak_step: "insert τ' τs' ∩ TD = {} ⟹ rank (subseq j) ⊒ rank (subseq (Suc j))"
          apply(intro NS[OF _ _ reach * step]) using τ' τs τs' by auto
        also note weak
        finally have **: "insert τ' τs' ∩ TD = {} ⟹ rank (seq i) ⊒ rank (subseq (Suc j))" by auto
        {
          assume "insert τ' τs' ∩ TD ≠ {}"
          then obtain τ where τ: "τ ∈ insert τ' τs' ∩ TD" by auto
          then consider "τ = τ' ∧ τ ∈ TD" | "τ ∈ τs' ∩ TD" by auto
          then have "rank (seq i) ⊐ rank (subseq (Suc j))"
          proof(cases)
            case 1 with reach step *
            have now: "rank (subseq j) ⊐ rank (subseq (Suc j))" by(intro S[of τ], auto)
            show ?thesis
            proof (cases "τs' ∩ TD = {}")
              case True
              note now also note weak[OF True] finally show ?thesis.
            next
              case False
              note now also note strict[OF False] finally show ?thesis.
            qed
          next
            case 2
            with strict have prev: "rank (seq i) ⊐ rank (subseq j)" by auto
            show ?thesis
            proof (cases "τ' ∈ TD")
              case True note S[OF True reach * step] also note prev finally show ?thesis.
            next
              case False from NS[OF False _ reach * step] τ' τs
              have "rank (subseq (Suc j)) ⊑ rank (subseq j)" by auto
              also note prev finally show ?thesis.
            qed
          qed
        }
        with * ** show ?case by auto
      qed
    }
    note this[OF le_refl trav subset_refl, unfolded first last, THEN conjunct2, THEN conjunct2]
  }
  then have "τ ∈ τs ∩ TD ⟹ chain (rel_of (⊐)) (rank ∘ seq)" for τ by auto
  then have disj: "τs ∩ TD = {}" using SN by blast
  with τs
  have τs2: "τs ⊆ sharp_transitions_of ?P" by auto
  note init
  also have "transitions_steps_lts P (flat_transitions_of P) `` initial_states P ⊆
    transitions_steps_lts P (flat_transitions_of ?P) `` initial_states ?P"
    by (intro Image_mono rtrancl_mono, insert TD, auto)
  finally have init2: "seq 0 ∈ ...".
  have "¬ SN_on (traverse τs) (Induces (flat_transitions_of ?P) `` initial_states ?P)"
    by (fact not_SN_onI[OF init2 chain])
  with τs0 τs2 have "¬ cooperation_SN ?P" by (unfold indexed_rewriting.cooperation_SN_on_as_SN_on_traverse, auto)
  with cSN show False by auto
qed

end
end

subsection ‹General implementation›

locale pre_transition_removal = lts where type_fixer = "TYPE('f×'t×'d)"
  for type_fixer :: "('f × 'v × 't × 'd × 'l × 'tr :: showl) itself"
  and check_weak check_strict :: "'tr × ('f,'v,'t,'l sharp) transition_rule ⇒ showsl check"
  and TD :: "'tr list"
  and Pi :: "('f,'v,'t,'l sharp,'tr) lts_impl"
begin

definition "processor ≡
  do {check_allm (λ(tr,τ).
    (if tr ∈ set TD then
      check (is_sharp_transition τ)
        (showsl_lit (STR ''non-sharp transition '') ∘ showsl tr ∘ showsl_lit (STR '' cannot be removed'')) ⪢
      check_strict (tr,τ) <+? (λs. showsl_lit (STR ''Failed to strictly orient transition '') ∘ showsl tr ∘ showsl_nl ∘ s)
     else if is_sharp_transition τ then
      check_weak (tr,τ) <+? (λs. showsl_lit (STR ''Failed to weakly orient transition '') ∘ showsl tr ∘ showsl_nl ∘ s)
    else succeed)) (transitions_impl Pi)
  ;return (del_transitions_impl Pi TD)
  } <+? (λ s. showsl_lit (STR ''Failed to eliminate transitions '') ∘ showsl_list TD ∘ showsl_lit (STR '':⏎'') ∘ s)"

lemma processorD:
  assumes "processor = return Pi'"
  shows "Pi' = del_transitions_impl Pi TD"
    and "(tr,τ) ∈ set (transitions_impl Pi) ⟹ is_sharp_transition τ ⟹
         tr ∉ set TD ⟹ isOK(check_weak (tr,τ))"
    and "(tr,τ) ∈ set (transitions_impl Pi) ⟹ tr ∈ set TD ⟹ is_sharp_transition τ"
    and "(tr,τ) ∈ set (transitions_impl Pi) ⟹ tr ∈ set TD ⟹ isOK(check_strict (tr,τ))"
    and "sub_lts_impl Pi' Pi" 
  using assms[unfolded processor_def]
  by (induct Pi, auto simp: del_transitions_impl_def diff_by_label_def mset_filter)

end

declare pre_transition_removal.processor_def[code]

subsection ‹Abstract transition removal using well-founded ranking functions›

locale transition_removal =
  logic where type_fixer = "TYPE('f×'t×'d)" +
  pre_transition_removal where type_fixer = type_fixer +
  wf_order less_eq less
  for type_fixer :: "('f × 'v × 't × 'd × 'l × 'tr :: showl) itself"
  and less_eq less :: "'m ⇒ 'm ⇒ bool"
  and rank :: "('v,'t,'d,'l sharp) state ⇒ 'm" +
  assumes check_weak:
    "⋀tr τ s t.
       isOK (check_weak (tr, τ)) ⟹
       lts_impl Pi ⟹
       (tr,τ) ∈ set (transitions_impl Pi) ⟹
       s ∈ reachable_states (lts_of Pi) ⟹
       t ∈ reachable_states (lts_of Pi) ⟹
       (s, t) ∈ transition_step_lts (lts_of Pi) τ ⟹
       less_eq (rank t) (rank s)"
  assumes check_strict: 
    "⋀tr τ s t.
       isOK (check_strict (tr, τ)) ⟹
       lts_impl Pi ⟹
       (tr,τ) ∈ set (transitions_impl Pi) ⟹
       s ∈ reachable_states (lts_of Pi) ⟹
       t ∈ reachable_states (lts_of Pi) ⟹
       (s, t) ∈ transition_step_lts (lts_of Pi) τ ⟹
       less (rank t) (rank s)"
begin

interpretation ord_syntax less_eq less.

lemma sound:
  assumes ret: "processor = return Pi'"
      and SN: "cooperation_SN_impl Pi'"
  shows "cooperation_SN_impl Pi"
proof(intro cooperation_SN_implI transition_removal_via_rank[OF wf_order_axioms, of _ "lts_of Pi"] conjI)
  assume Pi: "lts_impl Pi"
  let ?TD = "{τ | τ tr. (tr,τ) ∈ set (transitions_impl Pi) ∧ tr ∈ set TD}"
  note * = processorD[OF ret]
  from *(3)
  show "∀τ ∈ ?TD. is_sharp_transition τ" by auto
  show "cooperation_SN (delete_transitions (lts_of Pi) ?TD)"
  proof(rule cooperation_SN_sub_lts)
    note del = del_transitions_impl[of Pi TD]
    show sub: "sub_lts (delete_transitions (lts_of Pi) ?TD) (lts_of (del_transitions_impl Pi TD))"
      using del by auto
    from sub_lts_impl[OF del(1) Pi] SN *
    show "cooperation_SN (lts_of (del_transitions_impl Pi TD))" by auto
  qed
  fix s t τ
  assume s: "s ∈ reachable_states (lts_of Pi)" "t ∈ reachable_states (lts_of Pi)" and st: "(s, t) ∈ transition_step_lts (lts_of Pi) τ"
  { assume τ: "τ ∉ ?TD" "τ ∈ {τ ∈ transition_rules (lts_of Pi). is_sharp_transition τ}"
    from τ obtain tr where tr: "(tr,τ) ∈ set (transitions_impl Pi)" by auto
    from τ(1) tr have "tr ∉ set TD" by auto
    with *(2)[OF tr] τ have weak: "isOK (check_weak (tr, τ))" by auto
    from lts_impl[OF Pi] tr show "rank s ⊒ rank t" by (elim ltsE, auto intro!: check_weak[OF weak Pi _ s st])
  }
  { assume τ: "τ ∈ ?TD"
    from τ obtain tr where tr: "(tr,τ) ∈ set (transitions_impl Pi)" "tr ∈ set TD" by auto
    from s st lts_impl[OF Pi] tr
    show "rank s ⊐ rank t" by (elim ltsE, auto intro!: check_strict[OF *(4)[OF tr] Pi])
  }
qed

end

subsection ‹Checking ordering via formulas›

text ‹These locales are just for avoiding duplicate assumptions›

locale order_checker =
  logic_checker
  for less_eq less
  and dom_type
  and less_eq_formula (infix "⊑⇩f" 50)
  and less_formula (infix "⊏⇩f" 50) +
  assumes less_eq_type: "⋀s t. s :⇩f dom_type ⟹ t :⇩f dom_type ⟹ formula (s ⊑⇩f t)"
      and less_type: "⋀s t. s :⇩f dom_type ⟹ t :⇩f dom_type ⟹ formula (s ⊏⇩f t)"
      and less_eq_encode: "⋀α s t. assignment α ⟹ s :⇩f dom_type ⟹ t :⇩f dom_type ⟹
        α ⊨ s ⊑⇩f t ⟷ less_eq (⟦s⟧α) (⟦t⟧α)"
      and less_encode: "⋀α s t. assignment α ⟹ s :⇩f dom_type ⟹ t :⇩f dom_type ⟹
        α ⊨ s ⊏⇩f t ⟷ less (⟦s⟧α) (⟦t⟧α)"
begin

notation less_eq_formula (infix "⊑⇩f" 50)
notation less_formula (infix "⊏⇩f" 50)

end

subsection ‹Concrete transition removal via single well-founded ranking function›

locale pre_transition_removal_wf =
  pre_lts_checker where type_fixer = "TYPE('f × 'v trans_var × 't × 'd × 'h)"
  for type_fixer :: "('f::showl × 'v::showl × 't::showl × 'd × 'h::{default,showl}) itself"
  and less_eq_formula less_formula ::
    "('f,'v trans_var,'t) exp ⇒ ('f,'v trans_var,'t) exp ⇒ ('f,'v trans_var,'t) exp formula"
begin

notation less_eq_formula (infix "⊑⇩f" 50)
notation less_formula (infix "⊏⇩f" 50)

context
  fixes rank_exp :: "'l :: showl sharp ⇒ ('f,'v,'t) exp"
    and dom_type :: "'t"
    and hinter :: "'tr :: showl ⇒ 'h hint"
    and TD :: "'tr list"
    and Pi :: "('f,'v,'t,'l sharp,'tr) lts_impl"
begin

fun check_rank_weak where
  "check_rank_weak (tr, Transition l r φ) =
   check_formula (hinter tr) (Disjunction [
― ‹ position 0 › rename_vars Post (rank_exp r) ⊑⇩f rename_vars Pre (rank_exp l),
― ‹ position 1 › False⇩f,
― ‹ position 2 › ¬⇩f rename_vars Pre (assertion_of Pi l),
― ‹ position 3 › ¬⇩f φ
― ‹ position 4, disabled: ¬ rename_vars Post (assertion_of Pi r) ›
   ])"

fun check_rank_strict where
  "check_rank_strict (tr, Transition l r φ) =
   check_formula (hinter tr) (Disjunction [
― ‹ position 0 › rename_vars Post (rank_exp r) ⊏⇩f rename_vars Pre (rank_exp l),
― ‹ position 1 › False⇩f,
― ‹ position 2 › ¬⇩f rename_vars Pre (assertion_of Pi l),
― ‹ position 3 › ¬⇩f φ
― ‹ position 4, disabled: ¬ rename_vars Post (assertion_of Pi r) ›
   ])"

interpretation body: pre_transition_removal
  where check_weak = check_rank_weak
    and check_strict = check_rank_strict
    and TD = TD
    and Pi = Pi
    and type_fixer="TYPE(_)".

definition processor where
  "processor ≡ check_allm (λl.
    check (rank_exp l :⇩f dom_type)
      (showsl_lit (STR ''Ill-typed rank⏎'') o showsl (rank_exp l) o showsl_lit (STR ''⏎on location '') o showsl l)
   ) (nodes_lts_impl Pi) ⪢ body.processor"

end

term processor

end



locale transition_removal_wf =
  wf_order less_eq less +
  pre_transition_removal_wf where type_fixer = type_fixer +
  order_checker
    where type_fixer = "TYPE(_)"
      and less_eq_formula = less_eq_formula
      and less_formula = less_formula
  for type_fixer :: "('f::showl × 'v::showl × 't::showl × 'd × 'h :: {default,showl}) itself"
begin

interpretation ord_syntax less_eq less.

context
  fixes rank_exp :: "'l :: showl sharp ⇒ ('f,'v,'t) exp"
    and hinter :: "'tr :: showl ⇒ 'h hint"
    and Pi :: "('f,'v,'t,'l sharp,'tr :: showl) lts_impl"
    and TD :: "'tr list"
  assumes rank_type: "⋀l. l ∈ set (nodes_lts_impl Pi) ⟹ rank_exp l :⇩f dom_type"
begin

definition rank where [simp]: "rank s ≡ ⟦rank_exp (state.location s)⟧ (state.valuation s)"

lemma formula_less_eq:
  "⋀l r. l ∈ set (nodes_lts_impl Pi) ⟹ r ∈ set (nodes_lts_impl Pi) ⟹
   formula (rename_vars f (rank_exp l) ⊑⇩f rename_vars g (rank_exp r))"
  using less_eq_type by (auto simp:rank_type)

lemma formula_less:
  "⋀l r. l ∈ set (nodes_lts_impl Pi) ⟹ r ∈ set (nodes_lts_impl Pi) ⟹
   formula (rename_vars f (rank_exp l) ⊏⇩f rename_vars g (rank_exp r))"
  using less_type by (auto simp:rank_type)

abbreviation weak where "weak ≡ check_rank_weak rank_exp hinter Pi"
abbreviation strict where "strict ≡ check_rank_strict rank_exp hinter Pi"
interpretation body: transition_removal
  where less_eq = less_eq
    and less = less
    and check_weak = weak
    and check_strict = strict
    and rank = rank
    and type_fixer = "TYPE(_)"
proof
  assume ltsi: "lts_impl Pi"
  note [intro] = lts_impl_formula_assertion_of[OF ltsi]
  let ?I = "assertion_of Pi"
  let ?preI = "λl. rename_vars Pre (?I l)"
  let ?postI = "λl. rename_vars Post (?I l)"
  let ?preR = "λl. rename_vars Pre (rank_exp l)"
  let ?postR = "λl. rename_vars Post (rank_exp l)"
  fix s t τ tr
  assume τ: "(tr, τ) ∈ set (transitions_impl Pi)"
     and s: "s ∈ reachable_states (lts_of Pi)"
     and t: "t ∈ reachable_states (lts_of Pi)" 
     and st: "(s, t) ∈ transition_step_lts (lts_of Pi) τ"
  define α β where "α ≡ state.valuation s" "β ≡ state.valuation t"
  with st have [simp]: "s = State α (source τ)" "t = State β (target τ)"
   by (subst state.collapse[symmetric], unfold state.inject, auto)
  from st τ have l: "source τ ∈ set (nodes_lts_impl Pi)" and r: "target τ ∈ set (nodes_lts_impl Pi)"
    by (auto simp: nodes_lts_def)
  from st have α: "assignment α" and β: "assignment β" by auto
  from reachable_state[OF s] have sat: "α ⊨ ?I (state.location s)" by auto
  from reachable_state[OF t] have sat2: "β ⊨ ?I (state.location t)" by auto
  { assume ok: "isOK (weak (tr, τ))"
    show "rank s ⊒ rank t"
    proof(cases τ)
      case [simp]: (Transition l r ψ)
      have imp: "⊨⇩f Disjunction [?postR r ⊑⇩f ?preR l, False⇩f, ¬⇩f ?preI l, ¬⇩f ψ ― ‹, ¬ ?postI r›]"
        apply (rule check_formula[OF ok[simplified]])
        by (insert τ ltsi l r, auto intro!: formula_less_eq elim: lts_implE)
      from st obtain γ
      where ass: "assignment (pre_post_inter α β γ)" and sat3: "pre_post_inter α β γ ⊨ ψ" by auto
      show ?thesis
        apply (unfold rank_def, fold α_β_def)
        apply (rule iffD1[OF less_eq_encode[OF ass, of "?postR _" "?preR _", simplified]])
        using sat sat2 sat3 validD[OF imp ass] ass rank_type l r
        apply (auto simp: map_form_not[symmetric])
        done
    qed
  }
  { assume ok: "isOK (strict (tr,τ))"
    show "rank s ⊐ rank t"
    proof(cases τ)
      case [simp]: (Transition l r ψ)
      have imp: "⊨⇩f Disjunction [?postR r ⊏⇩f ?preR l, False⇩f, ¬⇩f ?preI l, ¬⇩f ψ ― ‹, ¬ ?postI r ›]"
        by (rule check_formula, rule ok[simplified], insert τ ltsi l r, auto intro: formula_less elim: lts_implE)
      from st obtain γ
      where ass: "assignment (pre_post_inter α β γ)" and sat3: "pre_post_inter α β γ ⊨ ψ" by auto
      from sat sat2 sat3 validD[OF imp ass] ass rank_type l r
      show "rank s ⊐ rank t" by (simp add: less_encode)
    qed
  }
qed

lemmas body_sound = body.sound

end

lemma sound:
  assumes "processor rank_exp dom_type h TD Pi = return Pi'"
  shows "cooperation_SN_impl Pi' ⟹ cooperation_SN_impl Pi"
  by (rule body_sound, insert assms, auto simp: processor_def)

end


subsection ‹Transition removal with bounds›

locale pre_transition_removal_bounded =
  pre_lts_checker where type_fixer = "TYPE('f×'v trans_var×'t×'d×'h)"
  for type_fixer :: "('f::showl × 'v::showl × 't::showl × 'd × 'h::{default,showl}) itself"
  and dom_type :: 't
  and less_eq_formula :: "('f,'v trans_var,'t) exp ⇒ ('f,'v trans_var,'t) exp ⇒ ('f,'v trans_var,'t) exp formula" (infix "⊑⇩f" 50)
  and less_formula :: "('f,'v trans_var,'t) exp ⇒ ('f,'v trans_var,'t) exp ⇒ ('f,'v trans_var,'t) exp formula" (infix "⊏⇩f" 50)
  and is_constant :: "('f,'v trans_var,'t) exp ⇒ bool"
begin

abbreviation "less_bounded_formula info s t ≡ s ⊏⇩f t ∧⇩f (rename_vars Pre (bound_exp info)) ⊑⇩f t"

context
  fixes info :: "(('f,'v,'t) exp, 't, 'l :: showl, 'tr :: showl, 'h) transition_removal_info"
begin

interpretation body: pre_transition_removal_wf
  where type_fixer = "TYPE(_)"
    and less_eq_formula = less_eq_formula and less_formula = "less_bounded_formula info".

definition processor where "processor Pi ≡ do {
  check (bound_exp info :⇩f dom_type) (showsl_lit (STR ''Ill-typed bound: '') o showsl (bound_exp info) );
  check (is_constant (rename_vars Pre (bound_exp info))) (showsl_lit (STR ''Non-constant bound: '') o showsl (bound_exp info));
  body.processor (rank info) dom_type (hinter info) (removed info) Pi
}"

end

end


locale transition_removal_bounded =
  pre_transition_removal_bounded where type_fixer = type_fixer +
  order_checker where type_fixer = "TYPE(_)" +
  non_inf_quasi_order less_eq less
  for type_fixer :: "('f::showl × 'v::showl × 't::showl × 'd × 'h::{default,showl}) itself" +
  assumes is_constant: "⋀e α β. is_constant e ⟹ ⟦e⟧ α = ⟦e⟧ β"
begin

interpretation ord_syntax less_eq less.

context
  fixes info :: "(('f,'v,'t) exp, 't, 'l :: showl, 'tr :: showl, 'h) transition_removal_info"
    and bound :: 'd
  assumes bound_type[simp]: "bound_exp info :⇩f dom_type"
      and bound[simp]: "⋀α. ⟦rename_vars Pre (bound_exp info)⟧ α = bound"
begin

interpretation wf: wf_order less_eq "less_bounded bound" by (fact bounded)

interpretation body: transition_removal_wf
  where type_fixer = "TYPE(_)"
    and less = "less_bounded bound"
    and less_formula = "less_bounded_formula info"
  by (unfold_locales, auto simp: less_encode less_eq_encode intro!: less_eq_type less_type)

lemmas body_sound = body.sound

end

lemma sound:
  assumes ok: "processor info Pi = return Pi'" and SN: "cooperation_SN_impl Pi'"
  shows "cooperation_SN_impl Pi"
proof-
  let ?b = "rename_vars Pre (bound_exp info)"
  note ok = ok[unfolded processor_def, simplified]
  from ok is_constant obtain bound where "⋀α. ⟦?b⟧α = bound" by auto
  from body_sound[OF _ this _ SN] ok show ?thesis by auto
qed

end


subsection ‹Lexicographic ranking›

context ord begin

definition lex_leq_bounded where
  "lex_leq_bounded bs xs ys ≡ ord_list.less_eq (map (λb. (less_eq, less_bounded b)) bs) xs ys"

definition lex_less_bounded where
  "lex_less_bounded bs xs ys ≡ ord_list.less (map (λb. (less_eq, less_bounded b)) bs) xs ys"

end

context ord_syntax begin

abbreviation lex_leq_bounded where "lex_leq_bounded ≡ ord.lex_leq_bounded less_eq less"
abbreviation lex_less_bounded where "lex_less_bounded ≡ ord.lex_less_bounded less_eq less"

end

context quasi_order begin

interpretation bounded_list: quasi_order_list "map (λb. (less_eq, less_bounded b)) bs"
  by (unfold quasi_order_list_def, auto intro: bounded)

lemma lex_bounded: "class.quasi_order (lex_leq_bounded bs) (lex_less_bounded bs)"
  by (unfold lex_leq_bounded_def lex_less_bounded_def, unfold_locales)

end

context non_inf_quasi_order begin

interpretation bounded_list: wf_order_list "map (λb. (less_eq, less_bounded b)) bs"
  by (unfold wf_order_list_def, auto intro: bounded)


lemma lex_bounded: "class.wf_order (lex_leq_bounded bs) (lex_less_bounded bs)"
  by (unfold lex_leq_bounded_def lex_less_bounded_def, unfold_locales)

end

context prelogic begin

abbreviation eval_list where "eval_list α ts ≡ map (λ t. ⟦t⟧ α) ts"

abbreviation rename_vars_exp_list :: "_ ⇒ ('f,'v,'t) exp list ⇒ _"
  where "rename_vars_exp_list f es ≡ map (rename_vars f) es"

adhoc_overloading rename_vars rename_vars_exp_list

end

context pre_transition_removal_bounded begin

abbreviation bound_exps where "bound_exps info ≡ map (rename_vars_exp Pre) (bound_exp info)"

fun lex_leq_formula where
  "lex_leq_formula [b] [x] [y] = (x ⊑⇩f y)"
| "lex_leq_formula (b#b'#bs) (x#x'#xs) (y#y'#ys) =
   (x ⊏⇩f y ∧⇩f b ⊑⇩f y ∨⇩f Conjunction [x ⊑⇩f y, lex_leq_formula (b'#bs) (x'#xs) (y'#ys)])"
| "lex_leq_formula [] [] [] = True⇩f"
| "lex_leq_formula _ _ _ = False⇩f"

lemma lex_leq_formula_code: 
  "lex_leq_formula xs ys zs = (case xs of 
     [] ⇒ (case ys of [] ⇒ (case zs of [] ⇒ True⇩f | _ ⇒ False⇩f) | _ ⇒ False⇩f)
  | x # xs ⇒ (case ys of [] ⇒ False⇩f 
  | y # ys ⇒ (case zs of [] ⇒ False⇩f 
  | z # zs ⇒ (case xs 
    of [] ⇒ (case ys of [] ⇒ (case zs of [] ⇒ y ⊑⇩f z | _ ⇒ False⇩f) | _ ⇒ False⇩f)
    | _ ⇒ (case ys of [] ⇒ False⇩f | _ ⇒ (case zs of [] ⇒ False⇩f 
    | _ ⇒ y ⊏⇩f z ∧⇩f x ⊑⇩f z ∨⇩f Conjunction [y ⊑⇩f z, lex_leq_formula xs ys zs]))))))" 
  by (cases xs; cases ys; cases zs; cases "tl xs"; cases "tl ys"; cases "tl zs", auto)

fun lex_less_formula where
  "lex_less_formula [b] [x] [y] = (x ⊏⇩f y ∧⇩f b ⊑⇩f y)"
| "lex_less_formula (b#b'#bs) (x#x'#xs) (y#y'#ys) =
   (x ⊏⇩f y ∧⇩f b ⊑⇩f y ∨⇩f Conjunction [x ⊑⇩f y, lex_less_formula (b'#bs) (x'#xs) (y'#ys)])"
| "lex_less_formula _ _ _ = False⇩f"

lemma lex_less_formula_code: 
  "lex_less_formula xs ys zs = (case xs of 
     [] ⇒ False⇩f
  | x # xs ⇒ (case ys of [] ⇒ False⇩f 
  | y # ys ⇒ (case zs of [] ⇒ False⇩f 
  | z # zs ⇒ (case xs 
    of [] ⇒ (case ys of [] ⇒ (case zs of [] ⇒ y ⊏⇩f z ∧⇩f x ⊑⇩f z | _ ⇒ False⇩f) | _ ⇒ False⇩f)
    | _ ⇒ (case ys of [] ⇒ False⇩f | _ ⇒ (case zs of [] ⇒ False⇩f 
    | _ ⇒ y ⊏⇩f z ∧⇩f x ⊑⇩f z ∨⇩f Conjunction [y ⊑⇩f z, lex_less_formula xs ys zs]))))))" 
  by (cases xs; cases ys; cases zs; cases "tl xs"; cases "tl ys"; cases "tl zs", auto)

context
  fixes info :: "(('f,'v,'t) exp list, 't, 'l :: showl, 'tr :: showl, 'h) transition_removal_info"
    and Pi :: "('f,'v,'t,'l sharp,'tr) lts_impl"
begin

fun check_lex_weak where
  "check_lex_weak (tr, Transition l r φ) = do {
      let ψ = lex_leq_formula (bound_exps info) (rename_vars Post (rank info r)) (rename_vars Pre (rank info l));
      check (formula ψ) (showsl_lit (STR ''lex-leq does not encode valid formula'') o showsl_nl o showsl ψ); 
      check_formula (hinter info tr) (Disjunction [
 ― ‹ position 0 › ψ,
 ― ‹ position 1 › False⇩f,
 ― ‹ position 2 › ¬⇩f rename_vars Pre (assertion_of Pi l),
 ― ‹ position 3 › ¬⇩f φ
 ― ‹ position 4, disabled: ¬ rename_vars Post (assertion_of Pi r) ›
    ])}"

fun check_lex_strict where
  "check_lex_strict (tr, Transition l r φ) = do {
      let ψ = lex_less_formula (bound_exps info) (rename_vars Post (rank info r)) (rename_vars Pre (rank info l));
      check (formula ψ) (showsl_lit (STR ''lex-less does not encode valid formula'') o showsl_nl o showsl ψ);
      check_formula (hinter info tr) (Disjunction [
 ― ‹ position 0 › ψ,
 ― ‹ position 1 › False⇩f,
 ― ‹ position 2 › ¬⇩f rename_vars Pre (assertion_of Pi l),
 ― ‹ position 3 › ¬⇩f φ
 ― ‹ position 4, disabled: ¬ rename_vars Post (assertion_of Pi r) ›
    ])}"


interpretation lex_body: pre_transition_removal
  where type_fixer = "TYPE(_)"
    and check_weak = check_lex_weak
    and check_strict = check_lex_strict
    and TD = "removed info" and Pi = Pi.

definition lex_processor where "lex_processor ≡
  do {
    check_allm (λl.
      check_allm (λe.
        check (e :⇩f dom_type) (showsl_lit (STR ''Unexpected type of expression:⏎'') o showsl e)
      ) (rank info l)
    ) (nodes_lts_impl Pi);
    check_allm (λe.
      check (e :⇩f dom_type) (showsl_lit (STR ''Unexpected type of bound: '') o showsl e)
    ) (bound_exp info);
    check_allm (λe.
      check (is_constant e) (showsl_lit (STR ''Non-constant bound: '') o showsl e)
    ) (bound_exps info);
    lex_body.processor
  }"


end

end

context transition_removal_bounded begin

context
  fixes info :: "(('f,'v,'t) exp list, 't, 'l :: showl, 'tr :: showl, 'h) transition_removal_info"
    and Pi :: "('f,'v,'t,'l sharp,'tr) lts_impl"
    and bounds :: "'d list"
  assumes ranks_type: "⋀e l. l ∈ set (nodes_lts_impl Pi) ⟹ e ∈ set (rank info l) ⟹ e :⇩f dom_type"
      and bounds_type: "⋀be. be ∈ set (bound_exp info) ⟹ be :⇩f dom_type"
      and bounds: "⋀ α. eval_list α (bound_exps info) = bounds"
begin

interpretation ord_syntax less_eq less.

abbreviation ranks where "ranks s ≡ eval_list (state.valuation s) (rank info (state.location s))"

lemma ranks_type_rename:
  "l ∈ set (nodes_lts_impl Pi) ⟹ e ∈ rename_vars f ` set (rank info l) ⟹ e :⇩f dom_type"
  using ranks_type by auto

lemma bound_exps_type:
  "be ∈ set (bound_exps info) ⟹ be :⇩f dom_type"
  using bounds_type by auto

lemma lex_leq_sound:
  defines "bes ≡ bound_exps info"
  assumes α: "assignment α"
      and x: "⋀x. x ∈ set xs ⟹ x :⇩f dom_type"
      and y: "⋀y. y ∈ set ys ⟹ y :⇩f dom_type"
  shows "α ⊨ lex_leq_formula bes xs ys ⟹ lex_leq_bounded (eval_list α bes) (eval_list α xs) (eval_list α ys)"
  using bound_exps_type[folded bes_def] x y
  apply (induct bes xs ys rule:lex_leq_formula.induct)
  using less_eq_encode[OF α] less_encode[OF α] by (auto simp:lex_leq_bounded_def lexcomp.less_eq_def)

lemma lex_less_sound:
  defines "bes ≡ bound_exps info"
  assumes α: "assignment α"
      and x: "⋀x. x ∈ set xs ⟹ x :⇩f dom_type"
      and y: "⋀y. y ∈ set ys ⟹ y :⇩f dom_type"
      and sat: "α ⊨ (lex_less_formula bes xs ys)"
  shows "lex_less_bounded (eval_list α bes) (eval_list α xs) (eval_list α ys)"
  using bound_exps_type[folded bes_def] x y sat
  apply (induct bes xs ys rule: lex_less_formula.induct)
  using less_eq_encode[OF α] less_encode[OF α] 
  by (auto simp: lex_less_bounded_def lexcomp.less_def)

abbreviation "weak ≡ check_lex_weak info Pi"
abbreviation strict where "strict ≡ check_lex_strict info Pi"

interpretation lex_wf: wf_order "lex_leq_bounded bounds" "lex_less_bounded bounds" by (fact lex_bounded)

interpretation lex_body: transition_removal
  where type_fixer = "TYPE(_)"
    and less_eq = "lex_leq_bounded bounds"
    and less = "lex_less_bounded bounds"
    and check_weak = weak
    and check_strict = strict
    and TD = "removed info"
    and rank = ranks
proof unfold_locales
  assume Pi: "lts_impl Pi"
  note [intro] = lts_impl_formula_assertion_of[OF Pi]
  let ?I = "assertion_of Pi"
  let ?preI = "λl. rename_vars Pre (?I l)"
  let ?postI = "λl. rename_vars Post (?I l)"
  let ?preR = "λl. rename_vars Pre (rank info l)"
  let ?postR = "λl. rename_vars Post (rank info l)"
  let ?bnd = "bound_exps info" 
  fix s t τ tr
  assume τ: "(tr, τ) ∈ set (transitions_impl Pi)"
     and s: "s ∈ reachable_states (lts_of Pi)"
     and t: "t ∈ reachable_states (lts_of Pi)" 
     and st: "(s, t) ∈ transition_step_lts (lts_of Pi) τ"
  define α β where "α ≡ state.valuation s" "β ≡ state.valuation t"
  with st have [simp]: "s = State α (source τ)" "t = State β (target τ)"
   by (subst state.collapse[symmetric], unfold state.inject, auto)
  from st τ have l: "source τ ∈ set (nodes_lts_impl Pi)" and r: "target τ ∈ set (nodes_lts_impl Pi)"
    by (auto simp: nodes_lts_def)
  from st have α: "assignment α" and β: "assignment β" by auto
  from reachable_state[OF s] have sat: "α ⊨ ?I (state.location s)" by auto
  from reachable_state[OF t] have sat2: "β ⊨ ?I (state.location t)" by auto

  { assume ok: "isOK (weak (tr, τ))"
    show "lex_leq_bounded bounds (ranks t) (ranks s)"
    proof(cases τ)
      case *[simp]: (Transition l r φ)
      from st obtain γ where γ: "assignment γ" and "δ α β γ ⊨ φ" by auto
      with sat sat2 have sat3: "δ α β γ ⊨ ?preI l ∧⇩f ?postI r ∧⇩f φ" by auto
      from lts_impl_transitions_impl[OF Pi τ] lts_impl_formula_assertion_of[OF Pi] ok[simplified] α β γ
      have "δ α β γ ⊨ Disjunction [lex_leq_formula ?bnd (?postR r) (?preR l), False⇩f, ¬⇩f ?preI l, ¬⇩f φ ― ‹, ¬ ?postI r›]"
        by (intro validD check_formula, auto)
      with sat3 have "δ α β γ ⊨ lex_leq_formula ?bnd (?postR r) (?preR l)"
        by auto
      from lex_leq_sound[OF _ _ _ this, unfolded bounds] α β γ l r
      show ?thesis by (auto simp: o_def ranks_type_rename)
    qed
  }
  { assume ok: "isOK (strict (tr, τ))"
    show "lex_less_bounded bounds (ranks t) (ranks s)"
    proof(cases τ)
      case *[simp]: (Transition l r φ)
      from st obtain γ where γ: "assignment γ" and "δ α β γ ⊨ φ" by auto
      with sat sat2 have sat3: "δ α β γ ⊨ ?preI l ∧⇩f ?postI r ∧⇩f φ" by auto
      from lts_impl_transitions_impl[OF Pi τ] lts_impl_formula_assertion_of[OF Pi] ok[simplified] α β γ
      have "δ α β γ ⊨ Disjunction [lex_less_formula ?bnd (?postR r) (?preR l), False⇩f, ¬⇩f ?preI l, ¬⇩f φ ― ‹, ¬ ?postI r›]"
        by (intro validD check_formula, auto)
      with sat3
      have "δ α β γ ⊨ lex_less_formula ?bnd (?postR r) (?preR l)" by auto
      from lex_less_sound[OF _ _ _ this, unfolded bounds] α β γ l r
      show ?thesis by (auto simp: o_def ranks_type_rename)
    qed
  }
qed

lemmas lex_body_sound = lex_body.sound

end

lemma lex_sound:
  assumes ok: "lex_processor info Pi = return Pi'"
      and "cooperation_SN_impl Pi'" (is ?SN)
  shows "cooperation_SN_impl Pi"
proof (rule lex_body_sound)
  note * = ok[unfolded lex_processor_def, simplified]
  show "l ∈ set (nodes_lts_impl Pi) ⟹ e ∈ set (rank info l) ⟹ e :⇩f dom_type" for l e
     using * by auto
  show "pre_transition_removal.processor
    (weak info Pi) (local.strict info Pi) (removed info) Pi = return Pi'" using * by auto
  show ?SN using ‹?SN›.
  show "be ∈ set (bound_exp info) ⟹ be :⇩f dom_type" for be using * by auto
  show "⋀α. eval_list α (bound_exps info) = eval_list undefined (bound_exps info)"
  proof (unfold list_eq_iff_nth_eq length_map, safe)
    fix α i assume i: "i < length (bound_exp info)"
    with * have "is_constant (bound_exps info ! i)" by auto
    from is_constant[OF this] i
    show "eval_list α (bound_exps info) ! i = eval_list undefined (bound_exps info) ! i" by auto
  qed
qed

end

lemmas transition_removal_code[code] =
  pre_transition_removal_wf.check_rank_strict.simps
  pre_transition_removal_wf.check_rank_weak.simps
  pre_transition_removal_wf.processor_def
  pre_transition_removal_bounded.processor_def
  pre_transition_removal_bounded.lex_processor_def
  pre_transition_removal_bounded.check_lex_strict.simps
  pre_transition_removal_bounded.check_lex_weak.simps
  pre_transition_removal_bounded.lex_less_formula_code
  pre_transition_removal_bounded.lex_leq_formula_code

end