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 "xset 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  (xset 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  (xset 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  (xset (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  (xset []. 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)  ( xset 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 " aset 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