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
*)

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 xQ 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 gU g) f; untame (λg. P gU 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 gU g) succs; untame U;
     !!g. final g ==> f g = g; invariant (λg. P gU g) (λg. [f g]);
     !!g0 g g'.
        [| P g0; g ∈ set (succs g0); g' ∈ set (succs g) |]
        ==> U g'f g = gf g' = f g;
     g [succs]->* g'; P g; final g'; tame g' |]
  ==> g [map f o succs]->* g'