Theory BalancedTraces

theory BalancedTraces
imports Main
begin

locale traces = 
  fixes step :: "'c => 'c => bool"  (infix "⇒" 50) 
begin

abbreviation steps (infix "⇒*" 50) where "steps ≡ step**"

inductive trace :: "'c ⇒ 'c list ⇒ 'c ⇒ bool"  where
  trace_nil[iff]: "trace final [] final"
| trace_cons[intro]: "trace conf' T final ⟹ conf ⇒ conf' ⟹ trace conf (conf'#T) final"

inductive_cases trace_consE: "trace conf (conf'#T) final"

lemma trace_induct_final[consumes 1, case_names trace_nil trace_cons]:
  "trace x1 x2 final ⟹ P final [] final ⟹ (⋀conf' T  conf. trace conf' T final ⟹ P conf' T final ⟹ conf ⇒ conf' ⟹ P conf (conf' # T) final) ⟹ P x1 x2 final"
  by (induction rule:trace.induct) auto

lemma build_trace:
  "c ⇒* c' ⟹ ∃ T. trace c T c'"
proof(induction rule: converse_rtranclp_induct)
  have "trace c' [] c'"..
  thus "∃T. trace c' T c'"..
next
  fix y z
  assume "y ⇒ z"
  assume "∃T. trace z T c'"
  then obtain T where "trace z T c'"..
  with ‹y ⇒ z›
  have "trace y (z#T) c'" by auto
  thus "∃T. trace y T c'" by blast
qed

lemma destruct_trace:  "trace c T c' ⟹ c ⇒* c'"
  by (induction rule:trace.induct) auto

lemma traceWhile:
  assumes "trace c1 T c4"
  assumes "P c1"
  assumes "¬ P c4"
  obtains  T1 c2 c3 T2
  where "T = T1 @ c3 # T2"  and "trace c1 T1 c2" and "∀x∈set T1.  P x" and "P c2" and "c2 ⇒ c3" and "¬ P c3" and "trace c3 T2 c4"
proof-
  from assms
  have "∃ T1 c2 c3 T2 . (T = T1 @ c3 # T2 ∧ trace c1 T1 c2 ∧ (∀x∈set T1. P x) ∧ P c2 ∧ c2 ⇒ c3 ∧ ¬ P c3 ∧ trace c3 T2 c4)"
  proof(induction)
    case trace_nil thus ?case by auto
  next
    case (trace_cons conf' T "end" conf)
    thus ?case 
    proof (cases "P conf'")
    case True
      from trace_cons.IH[OF True ‹¬ P end›]
      obtain T1 c2 c3 T2 where "T = T1 @ c3 # T2 ∧ trace conf' T1 c2 ∧ (∀x∈set T1. P x) ∧ P c2 ∧ c2 ⇒ c3 ∧ ¬ P c3 ∧ trace c3 T2 end" by auto
      with True
      have "conf' # T = (conf' # T1) @ c3 # T2 ∧ trace conf (conf' # T1) c2 ∧ (∀x∈set (conf' # T1). P x)  ∧ P c2 ∧ c2 ⇒ c3 ∧ ¬ P c3  ∧ trace c3 T2 end" by (auto intro: trace_cons)
      thus ?thesis by blast
    next
    case False with trace_cons
      have "conf' # T = [] @ conf' # T ∧ (∀x∈set []. P x) ∧ P conf ∧ conf ⇒ conf' ∧ ¬ P conf' ∧ trace conf' T end" by auto
      thus ?thesis by blast
    qed
  qed
  thus ?thesis by (auto intro: that)
qed

lemma traces_list_all:
  "trace c T c' ⟹ P c' ⟹ (⋀ c c'. c ⇒ c' ⟹ P c' ⟹ P c) ⟹ (∀ x∈set T. P x) ∧ P c"
  by (induction rule:trace.induct) auto

lemma trace_nil[simp]: "trace c [] c' ⟷ c = c'"
  by (metis list.distinct(1) trace.cases traces.trace_nil)
  
end

definition extends :: "'a list ⇒ 'a list ⇒ bool" (infix "≲" 50) where
  "S ≲ S' = (∃ S''. S' = S'' @ S)"

lemma extends_refl[simp]: "S ≲ S" unfolding extends_def by auto
lemma extends_cons[simp]: "S ≲ x # S" unfolding extends_def by auto
lemma extends_append[simp]: "S ≲ L @ S" unfolding extends_def by auto
lemma extends_not_cons[simp]: "¬ (x # S) ≲ S" unfolding extends_def by auto
lemma extends_trans[trans]: "S ≲ S' ⟹ S' ≲ S'' ⟹ S ≲ S''" unfolding extends_def by auto

locale balance_trace = traces + 
  fixes stack :: "'a ⇒ 's list"
  assumes one_step_only: "c ⇒ c' ⟹ (stack c) = (stack c') ∨ (∃ x.  stack c' = x # stack c) ∨  (∃ x. stack c = x # stack c')"
begin

inductive bal :: "'a ⇒ 'a list ⇒ 'a ⇒ bool" where
  balI[intro]: "trace c T c' ⟹ ∀c'∈ set T. stack c ≲ stack c' ⟹ stack c' = stack c ⟹ bal c T c'"

inductive_cases balE: "bal c T c'"

lemma bal_nil[simp]: "bal c [] c' ⟷ c = c'"
  by (auto elim: balE trace.cases)
  

lemma bal_stackD: "bal c T c' ⟹ stack c' = stack c" by (auto dest: balE)

lemma stack_passes_lower_bound:
  assumes "c3 ⇒ c4" 
  assumes "stack c2 ≲ stack c3" 
  assumes "¬ stack c2 ≲ stack c4" 
  shows "stack c3 = stack c2" and "stack c4 = tl (stack c2)"
proof-  
  from one_step_only[OF assms(1)]
  have "stack c3 = stack c2 ∧ stack c4 = tl (stack c2)"
  proof(elim disjE exE)
    assume "stack c3 = stack c4" with assms(2,3)
    have False by auto
    thus ?thesis..
  next
    fix x
    note ‹stack c2 ≲ stack c3›
    also
    assume "stack c4 = x # stack c3"
    hence "stack c3 ≲ stack c4" by simp
    finally
    have "stack c2 ≲ stack c4".
    with assms(3) show ?thesis..
  next
    fix x
    assume c3: "stack c3 = x # stack c4"
    with assms(2)
    obtain L where L: "x # stack c4 = L @ stack c2" unfolding extends_def by auto
    show ?thesis
    proof(cases L)
      case Nil with c3 L have "stack c3 = stack c2" by simp
      moreover
      from  Nil  c3 L have "stack c4 = tl (stack c2)" by (cases "stack c2") auto
      ultimately
      show ?thesis..
    next
      case (Cons y L')
      with L have "stack c4 = L' @ stack c2" by simp
      hence "stack c2 ≲ stack c4" by simp
      with assms(3) show ?thesis..
    qed
  qed
  thus "stack c3 = stack c2" and "stack c4 = tl (stack c2)" by auto
qed


lemma bal_consE:
  assumes "bal c1 (c2 # T) c5"
  and c2: "stack c2 = s # stack c1"
  obtains T1 c3 c4 T2
  where "T = T1 @ c4 # T2" and  "bal c2 T1 c3" and "c3 ⇒ c4" "bal c4 T2 c5"
using assms(1)
proof(rule balE)
  
  assume c5: "stack c5 = stack c1"
  assume T: "∀ c' ∈ set (c2 # T). stack c1 ≲ stack c'"

  assume "trace c1 (c2 # T) c5"
  hence "c1 ⇒ c2" and "trace c2 T c5" by (auto elim: trace_consE)

  note ‹trace c2 T c5›
  moreover
  have "stack c2 ≲ stack c2" by simp
  moreover
  have "¬ (stack c2 ≲ stack c5)" unfolding c5 c2  by simp
  ultimately
  obtain T1 c3 c4 T2
    where "T = T1 @ c4 # T2" and "trace c2 T1 c3" and "∀ c' ∈ set T1. stack c2 ≲ stack c'" 
     and "stack c2 ≲ stack c3" and "c3 ⇒ c4" and "¬ stack c2 ≲ stack c4" and "trace c4 T2 c5"
     by (rule traceWhile)

  show ?thesis
  proof (rule that)
    show "T = T1 @ c4 # T2" by fact

    from ‹c3 ⇒ c4› ‹stack c2 ≲ stack c3› ‹¬ stack c2 ≲ stack c4›
    have "stack c3 = stack c2" and c2': "stack c4 = tl (stack c2)" by (rule stack_passes_lower_bound)+

    from  ‹trace c2 T1 c3› ‹∀ a ∈ set T1. stack c2 ≲ stack a› this(1)
    show "bal c2 T1 c3"..

    show "c3 ⇒ c4" by fact

    have c4: "stack c4 = stack c1" using c2 c2' by simp

    note  ‹trace c4 T2 c5› 
    moreover
    have "∀ a∈set T2. stack c4 ≲ stack a" using c4 T ‹T = _›  by auto
    moreover
    have "stack c5 = stack c4" unfolding c4 c5..
    ultimately
    show "bal c4 T2 c5"..
  qed
qed

end


end