Theory TameProps

(* Author:     Tobias Nipkow
*)

section‹Tame Properties›

theory TameProps
imports Tame RTranCl
begin

lemma length_disj_filter_le: "∀x ∈ set xs. ¬(P x ∧ Q x) ⟹
 length(filter P xs) + length(filter Q xs) ≤ length xs"
by(induct xs) auto

lemma tri_quad_le_degree: "tri g v + quad g v ≤ degree g v"
proof -
  let ?fins = "[f ← facesAt g v . final f]"
  have "tri g v + quad g v =
        |[f ← ?fins . triangle f]| + |[f ← ?fins. |vertices f| = 4]|"
    by(simp add:tri_def quad_def)
  also have "… ≤ |[f ← facesAt g v. final f]|"
    by(rule length_disj_filter_le) simp
  also have "… ≤ |facesAt g v|" by(rule length_filter_le)
  finally show ?thesis by(simp add:degree_def)
qed

lemma faceCountMax_bound:
 "⟦ tame g; v ∈ 𝒱 g ⟧ ⟹ tri g v + quad g v ≤ 7"
using tri_quad_le_degree[of g v]
by(auto simp:tame_def tame11b_def split:if_split_asm)


lemma filter_tame_succs:
assumes invP: "invariant P succs" and fin: "⋀g. final g ⟹ succs g = []"
and ok_untame: "⋀g. P g ⟹ ¬ ok g ⟹ final g ∧ ¬ tame g"
and gg': "g [succs]→* g'"
shows "P g ⟹ final g' ⟹ tame g' ⟹ g [filter ok ∘ succs]→* g'"
using gg'
proof (induct rule:RTranCl.induct)
  case refl show ?case by(rule RTranCl.refl)
next
  case (succs h h' h'')
  hence "P h'"  using invP by(unfold invariant_def) blast
  show ?case
  proof cases
    assume "ok h'"
    thus ?thesis using succs ‹P h'› by(fastforce intro:RTranCl.succs)
  next
    assume "¬ ok h'" note fin_tame = ok_untame[OF ‹P h'› ‹¬ ok h'›]
    have "h'' = h'" using fin_tame
      by(rule_tac RTranCl.cases[OF succs(2)])(auto simp:fin)
    hence False using fin_tame succs by fast
    thus ?case ..
  qed
qed


definition untame :: "(graph ⇒ bool) ⇒ bool" where
"untame P ≡ ∀g. final g ∧ P g ⟶ ¬ tame g"


lemma filterout_untame_succs:
assumes invP: "invariant P f" and invPU: "invariant (λg. P g ∧  U g) f"
and untame: "untame(λg. P g ∧ U g)"
and new_untame: "⋀g g'. ⟦ P g; g' ∈ set(f g); g' ∉ set(f' g) ⟧ ⟹ U g'"
and gg': "g [f]→* g'"
shows "P g ⟹ final g' ⟹ tame g' ⟹ g [f']→* g'"
using gg'
proof (induct rule:RTranCl.induct)
  case refl show ?case by(rule RTranCl.refl)
next
  case (succs h h' h'')
  hence Ph': "P h'"  using invP by(unfold invariant_def) blast
  show ?case
  proof cases
    assume "h' ∈ set(f' h)"
    thus ?thesis using succs Ph' by(blast intro:RTranCl.succs)
  next
    assume "h' ∉ set(f' h)"
    with succs(4) succs(1) have "U h'" by (rule new_untame)
    hence False using Ph' RTranCl_inv[OF invPU] untame succs
      by (unfold untame_def) fast
    thus ?case ..
  qed
qed

end