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 c⇩1 T c⇩4" assumes "P c⇩1" assumes "¬ P c⇩4" obtains T⇩1 c⇩2 c⇩3 T⇩2 where "T = T⇩1 @ c⇩3 # T⇩2" and "trace c⇩1 T⇩1 c⇩2" and "∀x∈set T⇩1. P x" and "P c⇩2" and "c⇩2 ⇒ c⇩3" and "¬ P c⇩3" and "trace c⇩3 T⇩2 c⇩4" proof- from assms have "∃ T⇩1 c⇩2 c⇩3 T⇩2 . (T = T⇩1 @ c⇩3 # T⇩2 ∧ trace c⇩1 T⇩1 c⇩2 ∧ (∀x∈set T⇩1. P x) ∧ P c⇩2 ∧ c⇩2 ⇒ c⇩3 ∧ ¬ P c⇩3 ∧ trace c⇩3 T⇩2 c⇩4)" 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 T⇩1 c⇩2 c⇩3 T⇩2 where "T = T⇩1 @ c⇩3 # T⇩2 ∧ trace conf' T⇩1 c⇩2 ∧ (∀x∈set T⇩1. P x) ∧ P c⇩2 ∧ c⇩2 ⇒ c⇩3 ∧ ¬ P c⇩3 ∧ trace c⇩3 T⇩2 end" by auto with True have "conf' # T = (conf' # T⇩1) @ c⇩3 # T⇩2 ∧ trace conf (conf' # T⇩1) c⇩2 ∧ (∀x∈set (conf' # T⇩1). P x) ∧ P c⇩2 ∧ c⇩2 ⇒ c⇩3 ∧ ¬ P c⇩3 ∧ trace c⇩3 T⇩2 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 "c⇩3 ⇒ c⇩4" assumes "stack c⇩2 ≲ stack c⇩3" assumes "¬ stack c⇩2 ≲ stack c⇩4" shows "stack c⇩3 = stack c⇩2" and "stack c⇩4 = tl (stack c⇩2)" proof- from one_step_only[OF assms(1)] have "stack c⇩3 = stack c⇩2 ∧ stack c⇩4 = tl (stack c⇩2)" proof(elim disjE exE) assume "stack c⇩3 = stack c⇩4" with assms(2,3) have False by auto thus ?thesis.. next fix x note `stack c⇩2 ≲ stack c⇩3` also assume "stack c⇩4 = x # stack c⇩3" hence "stack c⇩3 ≲ stack c⇩4" by simp finally have "stack c⇩2 ≲ stack c⇩4". with assms(3) show ?thesis.. next fix x assume c⇩3: "stack c⇩3 = x # stack c⇩4" with assms(2) obtain L where L: "x # stack c⇩4 = L @ stack c⇩2" unfolding extends_def by auto show ?thesis proof(cases L) case Nil with c⇩3 L have "stack c⇩3 = stack c⇩2" by simp moreover from Nil c⇩3 L have "stack c⇩4 = tl (stack c⇩2)" by (cases "stack c⇩2") auto ultimately show ?thesis.. next case (Cons y L') with L have "stack c⇩4 = L' @ stack c⇩2" by simp hence "stack c⇩2 ≲ stack c⇩4" by simp with assms(3) show ?thesis.. qed qed thus "stack c⇩3 = stack c⇩2" and "stack c⇩4 = tl (stack c⇩2)" by auto qed lemma bal_consE: assumes "bal c⇩1 (c⇩2 # T) c⇩5" and c⇩2: "stack c⇩2 = s # stack c⇩1" obtains T⇩1 c⇩3 c⇩4 T⇩2 where "T = T⇩1 @ c⇩4 # T⇩2" and "bal c⇩2 T⇩1 c⇩3" and "c⇩3 ⇒ c⇩4" "bal c⇩4 T⇩2 c⇩5" using assms(1) proof(rule balE) assume c⇩5: "stack c⇩5 = stack c⇩1" assume T: "∀ c' ∈ set (c⇩2 # T). stack c⇩1 ≲ stack c'" assume "trace c⇩1 (c⇩2 # T) c⇩5" hence "c⇩1 ⇒ c⇩2" and "trace c⇩2 T c⇩5" by (auto elim: trace_consE) note `trace c⇩2 T c⇩5` moreover have "stack c⇩2 ≲ stack c⇩2" by simp moreover have "¬ (stack c⇩2 ≲ stack c⇩5)" unfolding c⇩5 c⇩2 by simp ultimately obtain T⇩1 c⇩3 c⇩4 T⇩2 where "T = T⇩1 @ c⇩4 # T⇩2" and "trace c⇩2 T⇩1 c⇩3" and "∀ c' ∈ set T⇩1. stack c⇩2 ≲ stack c'" and "stack c⇩2 ≲ stack c⇩3" and "c⇩3 ⇒ c⇩4" and "¬ stack c⇩2 ≲ stack c⇩4" and "trace c⇩4 T⇩2 c⇩5" by (rule traceWhile) show ?thesis proof (rule that) show "T = T⇩1 @ c⇩4 # T⇩2" by fact from `c⇩3 ⇒ c⇩4` `stack c⇩2 ≲ stack c⇩3` `¬ stack c⇩2 ≲ stack c⇩4` have "stack c⇩3 = stack c⇩2" and c⇩2': "stack c⇩4 = tl (stack c⇩2)" by (rule stack_passes_lower_bound)+ from `trace c⇩2 T⇩1 c⇩3` `∀ a ∈ set T⇩1. stack c⇩2 ≲ stack a` this(1) show "bal c⇩2 T⇩1 c⇩3".. show "c⇩3 ⇒ c⇩4" by fact have c⇩4: "stack c⇩4 = stack c⇩1" using c⇩2 c⇩2' by simp note `trace c⇩4 T⇩2 c⇩5` moreover have "∀ a∈set T⇩2. stack c⇩4 ≲ stack a" using c⇩4 T `T = _` by auto moreover have "stack c⇩5 = stack c⇩4" unfolding c⇩4 c⇩5.. ultimately show "bal c⇩4 T⇩2 c⇩5".. qed qed end end