# Theory TameProps

Up to index of Isabelle/HOL/Tame

theory TameProps
imports Tame RTranCl
begin

```(* ID:         \$Id: TameProps.thy,v 1.2 2006/01/11 19:40:47 nipkow Exp \$
Author:     Tobias Nipkow
*)

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]|"
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)
qed

lemma faceCountMax_bound:
"[| tame g; v ∈ \<V> g |] ==> tri g v + quad g v ≤ 6"
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|`

`  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'```