(* 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'