(* ID: $Id: TameProps.thy,v 1.2 2006/01/11 19:40:47 nipkow Exp $
Author: Tobias Nipkow
*)
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∈ 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 ∈ \<V> g |] ==> tri g v + quad g v ≤ 6"
using tri_quad_le_degree[of g v]
by(auto simp:tame_def tame45_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(fastsimp 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.elims[OF succs(2)])(auto simp:fin)
hence False using fin_tame succs by fast
thus ?case ..
qed
qed
constdefs
untame :: "(graph => bool) => bool"
"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
lemma comp_map_tame_pres:
assumes invP: "invariant P succs"
and invPU: "invariant (%g. P g ∧ U g) succs" and untame: "untame U"
and f_fin: "!!g. final g ==> f g = g"
and invPUf: "invariant (%g. P g ∧ U g) (%g. [f g])"
and succs_f: "!!g0 g g'. P g0 ==> g ∈ set(succs g0) ==> g' ∈ set(succs g) ==>
U g' ∨ f g = g ∨ f g' = f g"
and gg': "g [succs]->* g'"
shows "P g ==> final g' ==> tame g' ==> g [map f 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 Ph': "P h'" using invP by(unfold invariant_def) blast
hence IH: "h' [map f o succs]->* h''" using succs by blast
thus ?case
proof (rule RTranCl_elim)
assume "h'' = h'"
moreover hence "f h' = h'" using f_fin[OF succs(5)] by simp
ultimately show ?case using succs(1)
by(force intro!: RTranCl.succs[OF _ RTranCl.refl])
next
fix h2
assume 1: "h' [map f o succs]-> h2" and
2: "h2 [map f o succs]->* h''"
from 1 obtain h1 where h1: "h1 ∈ set(succs h')" and [simp]: "h2 = f h1"
by force
{ assume Uh1: "U h1"
have invPU2: "invariant (%g. P g ∧ U g) (map f o succs)"
using invPU invPUf by(auto simp:invariant_def)
have Ph1: "P h1" using succs(1) succs(4) h1 invP
by(unfold invariant_def) blast
have PUh2: "P h2 ∧ U h2" using invariantE[OF invPUf] Ph1 Uh1 by auto
from RTranCl_inv[OF invPU2 2, OF PUh2]
have False using succs(5-6) untame by(auto simp:untame_def)
hence ?thesis ..
} moreover
{ assume "f h' = h'"
hence "h' ∈ set((map f o succs) h)" using succs(1) by force
hence ?thesis using IH by(rule RTranCl.succs)
} moreover
{ assume ff: "f h1 = f h'"
hence "h2 ∈ set((map f o succs) h)" using succs(1) by auto
hence ?thesis using 2 by(rule RTranCl.succs)
}
ultimately show ?thesis using succs_f[OF succs(4) succs(1) h1] by blast
qed
qed
end
lemma length_disj_filter_le:
∀x∈set xs. ¬ (P x ∧ Q x) ==> |filter P xs| + |filter Q xs| ≤ |xs|
lemma tri_quad_le_degree:
tri g v + quad g v ≤ degree g v
lemma faceCountMax_bound:
[| tame g; v ∈ \<V> g |] ==> tri g v + quad g v ≤ 6
lemma filter_tame_succs:
[| invariant P succs; !!g. final g ==> succs g = []; !!g. [| P g; ¬ ok g |] ==> final g ∧ ¬ tame g; g [succs]->* g'; P g; final g'; tame g' |] ==> g [filter ok o succs]->* g'
lemma filterout_untame_succs:
[| invariant P f; invariant (λg. P g ∧ U g) f; untame (λg. P g ∧ U g); !!g g'. [| P g; g' ∈ set (f g); g' ∉ set (f' g) |] ==> U g'; g [f]->* g'; P g; final g'; tame g' |] ==> g [f']->* g'
lemma comp_map_tame_pres:
[| invariant P succs; invariant (λg. P g ∧ U g) succs; untame U; !!g. final g ==> f g = g; invariant (λg. P g ∧ U g) (λg. [f g]); !!g0 g g'. [| P g0; g ∈ set (succs g0); g' ∈ set (succs g) |] ==> U g' ∨ f g = g ∨ f g' = f g; g [succs]->* g'; P g; final g'; tame g' |] ==> g [map f o succs]->* g'