header{* 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 \<leftarrow> facesAt g v . final f]"
have "tri g v + quad g v =
|[f \<leftarrow> ?fins . triangle f]| + |[f \<leftarrow> ?fins. |vertices f| = 4]|"
by(simp add:tri_def quad_def)
also have "… ≤ |[f \<leftarrow> 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 ∈ \<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:split_if_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 o 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