Theory LTS_Nontermination_Prover

theory LTS_Nontermination_Prover
imports Initial_Cooperation_Program Invariant_Proof_Checkers Transition_Removal Location_Addition Fresh_Variable_Addition Call_Graph_Scc_Decomp Cut_Transition_Split
theory LTS_Nontermination_Prover
  imports 
    Initial_Cooperation_Program 
    Invariant_Proof_Checkers 
    Transition_Removal 
    Show_LTS
    Location_Addition 
    Fresh_Variable_Addition 
    Call_Graph_Scc_Decomp
    Invariants_To_Assertions
    Cut_Transition_Split
begin
type_synonym ('f, 'v, 't) val_impl = "(('v × 't) × ('f, 'v, 't) exp) list"
type_synonym ('f, 'v, 't, 'l) state_impl = "('f, 'v, 't) val_impl × 'l"
type_synonym ('f,'v,'t,'l,'tr) transition_seq_impl =
  "(('tr × ('f,'v,'t,'l) transition_rule) × ('f, 'v, 't, 'l) state_impl) list"

datatype ('f,'v,'t,'l,'tr,'h) nontermination_proof =
  EquivalentState "('f, 'v, 't, 'l) state_impl" "('f,'v,'t,'l,'tr) transition_seq_impl" "('f,'v,'t,'l,'tr) transition_seq_impl"


definition val_of :: "('f, 'v, 't) val_impl ⇒ ('v,'t,('f, 'v, 't) exp) valuation"
  where
    "val_of ss = List.foldr (λ(x, t) σ. σ ∘s subst x t) ss Var"

definition state_of :: "('f, 'v, 't, 'l) state_impl ⇒ ('v, 't, ('f, 'v × 't) Term.term, 'l) state" where
  "state_of s ≡ (State (val_of (fst s)) (snd s))"

locale pre_nontermination_checker =
  pre_art_checker where type_fixer = type_fixer +
  transition_removal: pre_transition_removal_bounded
    where type_fixer = "TYPE(_)"
      and logic_checker = tc2
      and showsl_atom = sa2
      and negate_atom = ne2 +
  pre_transition_definability_checker
    where type_fixer = "TYPE(_)"
  for type_fixer :: "('f:: showl × 'v::showl × 't:: showl × ('f, 'v, 't) exp × 'h::{default,showl}) itself" +
    fixes hinter :: "'tr :: showl ⇒ 'h hint"

locale nontermination_checker =
  pre_nontermination_checker where type_fixer = type_fixer +
  art_checker where type_fixer = type_fixer +
  transition_removal: transition_removal_bounded
    where type_fixer = "TYPE(_)"
      and logic_checker = tc2
      and showsl_atom = sa2
      and negate_atom = ne2 +
  transition_definability_checker
    where type_fixer = "TYPE(_)"
  for type_fixer :: "('f:: showl × 'v::showl × 't:: showl × ('f, 'v, 't) exp × 'h::{default,showl}) itself"

context pre_nontermination_checker
begin

definition check_equal_states :: "('f, 'v, 't, 'l) state_impl ⇒ ('f, 'v, 't, 'l) state_impl ⇒ (String.literal ⇒ String.literal) + unit"
  where
  "check_equal_states s1 s2 =
  do {
     check (snd s1 = snd s2) (showsl_lit (STR ''different locations⏎''));
     check (fst s1 = fst s2) (showsl_lit (STR ''different valuations⏎''))
  }"

lemma check_equal_states:
  assumes "isOK(check_equal_states (v1,l1) (v2,l2))"
  shows "l1 = l2 ∧ (∀x. val_of v1 x = val_of v2 x)"
proof -
  note ok = assms[unfolded check_equal_states_def]
  from ok have "l1 = l2" "v1 = v2" by simp+
  thus ?thesis by auto
qed

definition check_transition_step :: " _ ⇒ _ ⇒ _"
  where
  "check_transition_step P τ = (
     case τ of (src, (lab, t), tgt) ⇒
     case t of Transition l r φ ⇒
       let α = δ (val_of (fst src)) (val_of (fst tgt)) (val_of (fst src)) in
       do {
         check ((lab, t) ∈ set (transitions_impl P)) (showsl_lit (STR ''transition not available⏎''));
         check (state_lts (lts_of P) (state_of tgt)) (showsl_lit (STR ''target is not a state⏎''));
         check (α ⊨ φ) (showsl_lit (STR ''condition not satisfied⏎''));
         check (snd src = l ∧ snd tgt = r)
           (showsl_lit (STR ''rule not applicable⏎''))})"

lemma check_transition_step:
  assumes "isOK(check_transition_step P (src, (lab, Transition l r φ), tgt))"
  and src:"state_lts (lts_of P) (state_of src)"
  shows "(state_of src, state_of tgt) ∈ transition (lts_of P) ∧ state_lts (lts_of P) (state_of tgt)"
proof -
  note ok = assms[unfolded check_transition_step_def split]
  let ?τ = "Transition l r φ"
  from ok have "(lab, ?τ) ∈ set (transitions_impl P)" by auto
  hence trans:"Transition l r φ ∈ transition_rules (lts_of P)"
    unfolding lts_of_def transitions_impl_def by (cases P, auto)
  let ?α = "δ (val_of (fst src)) (val_of (fst tgt)) (val_of (fst src))"
  from ok have sat:"?α ⊨ φ" and ass:"assignment (val_of (fst src))" unfolding state_of_def by simp+
  from ok have tgt:"state_lts (lts_of P) (state_of tgt)" by auto
  from ok have locs:"snd src = l ∧ snd tgt = r" by simp
  note mem = mem_transition_step_TransitionI[OF src tgt _ _ ass]
  have "(state_of src, state_of tgt) ∈ transition_step (state_lts (lts_of P)) ?τ"
    by (rule mem, insert sat locs, unfold state_of_def, auto)
  from mem_transitionI[OF _ this] trans show ?thesis by auto
qed


fun check_transition_seq
  where
   "check_transition_seq P src [] = return src"
 | "check_transition_seq P src ((τ, tgt) # ts) =
             (check_transition_seq P tgt ts ⤜
             (λ last. check_return (check_transition_step P (src, τ, tgt)) last))"

lemma check_transition_seq:
  assumes "(check_transition_seq P src ts) = return tgt"
  and src:"state_lts (lts_of P) (state_of src)"
  shows "(state_of src, state_of tgt) ∈ (transition (lts_of P))^^(length ts) ∧ state_lts (lts_of P) (state_of tgt)"
  using assms
proof(induct ts arbitrary:src)
  case Nil
  thus ?case by simp
next
  case (Cons t ts)
  let ?T = "transition (lts_of P)"
  obtain τ intermed where t:"t = (τ, intermed)" by (cases t, auto)
  obtain lab l r φ where τ:"τ = (lab, Transition l r φ)" by (cases τ, cases "snd τ", auto)
  note ok = Cons(2)[unfolded check_transition_seq.simps foldl.foldl_Cons t split]
  from ok have step:"isOK(check_transition_step P (src, τ, intermed))" by auto
  note step = step[unfolded τ, THEN check_transition_step, OF Cons(3)]
  from ok have "check_transition_seq P intermed ts = return tgt" by auto
  from Cons(1)[OF this] step have steps:"(state_of intermed, state_of tgt) ∈ ?T^^(length ts)"
    "state_lts (lts_of P) (state_of tgt)" by auto
  from relpow_Suc_I2[OF conjunct1[OF step] steps(1)] steps(2) show ?case by simp
qed

fun check_nontermination_proof :: "showsl ⇒ ('f,'v,'t,'l,'tr) lts_impl ⇒ ('f,'v,'t,'l,'tr,'h) nontermination_proof ⇒  _" where
  "check_nontermination_proof i P (nontermination_proof.EquivalentState sinit stem loop) = debug i (STR ''Equivalent state criterion'') (
    do {
    check (snd sinit ∈ set (initial P) ∧ state_lts (lts_of P) (state_of sinit)) (showsl_lit (STR ''initial state''));  
    loop_head1 ← check_transition_seq P sinit stem
      <+? (λ s. i o showsl_lit (STR '': error when checking stem sequence of lasso⏎'') o s);
    loop_head2 ← check_transition_seq P loop_head1 loop
      <+? (λ s. i o showsl_lit (STR '': error when checking loop sequence⏎'') o s);
    check (length loop ≠ 0) (showsl_lit (STR ''loop must have positive length''));
    check (loop_head1 = loop_head2) (showsl_lit (STR ''loop start and end do not match''))
   })"

lemma check_nontermination_proof:
  "lts_impl P ⟹ isOK(check_nontermination_proof i P ntprf) ⟹ ¬ lts_termination (lts_of P)" 
proof-
  assume P:"lts_impl P" and ok:"isOK(check_nontermination_proof i P ntprf)"
  let ?lts = "lts_of P"
  let ?T = "transition ?lts"
  let ?state = "λs. state_lts (lts_of P) (state_of s)"
  show ?thesis proof(cases ntprf)
    case (EquivalentState s0 stem loop)
    note ok = ok[unfolded this check_nontermination_proof.simps]
    let ?k = "length loop"
    from ok have s0:"state_lts ?lts (state_of s0)" by auto
    from ok obtain si where lh:"check_transition_seq P s0 stem = return si" by auto
    from check_transition_seq[OF lh s0] relpow_imp_rtrancl
      have si:"(state_of s0, state_of si) ∈ ?T*" "?state si" by auto
    from ok lh have "check_transition_seq P si loop = Inr si" by auto
    from check_transition_seq[OF this si(2)] have loop:"(state_of si, state_of si) ∈ ?T^^?k" by auto
    from ok have k:"?k > 0" by auto
    from k loop trancl_power have loop:"(state_of si, state_of si) ∈ ?T+" by blast
    from ok have s0:"state_of s0 ∈ (initial_states ?lts)"
      unfolding initial_states_def state_of_def by auto
    show ?thesis proof(cases "state_of s0 = state_of si")
      case True
      let ?f = "λi. state_of si"
      from loop have "chain (?T+) ?f" unfolding chain_def by auto
      with True s0 have "¬ SN_on (?T+) (initial_states ?lts)" unfolding SN_on_def by auto
      then show ?thesis using SN_on_trancl by auto
    next
      case False
      with si(1)[unfolded rtrancl_eq_or_trancl] have stem:"(state_of s0, state_of si) ∈ ?T+" by auto
      let ?f = "λi. (case i of 0 ⇒ state_of s0 | Suc j ⇒ state_of si)"
      { fix i
        have "(?f i, ?f (Suc i)) ∈ (transition (lts_of P))+" by (cases i, insert stem loop, auto)
      } note f = this
      have "∃f. f 0 ∈ initial_states (lts_of P) ∧ chain (?T+) f"
        unfolding chain_def by (rule exI[of _ ?f], insert f s0 , auto)
      hence "¬ SN_on (?T+) (initial_states ?lts)" unfolding SN_on_def by auto
      then show ?thesis using SN_on_trancl by auto
    qed
  qed
qed

definition check where
  "check P prf ≡ do {
     debug id (STR ''init - Check well-formedness'') (check_lts_impl P <+? (λ s. showsl_lit (STR ''input LTS is not well-formed'') o s));
     check_nontermination_proof id P prf
   }"

end

declare pre_nontermination_checker.check_transition_seq.simps[code]
declare pre_nontermination_checker.check_nontermination_proof.simps[code]
declare pre_nontermination_checker.check_def[code]


context nontermination_checker
begin

theorem sound: "isOK (check P prf) ⟹ ¬ lts_termination (lts_of P)"
  using check_nontermination_proof[of P _ "prf"]
  unfolding check_def by auto

end
end