Theory Plane1Props

(* ID:         $Id: Plane1Props.thy,v 1.1 2006/01/04 13:44:00 nipkow Exp $
   Author:     Gertrud Bauer, Tobias Nipkow
*)

theory Plane1Props
imports Plane1 PlaneProps Tame
begin


lemma next_plane_subset:
  "∀f ∈ \<F> g. vertices f ≠ [] ==>
   set (next_planep g) ⊆ set (next_plane0p g)"
apply(clarsimp simp:next_plane0_def next_plane_def minimalFace_def finalGraph_def)
apply(rule_tac x = "minimal (size o vertices) (nonFinals g)" in bexI)
 apply(rule_tac x = "minimalVertex g (minimal (size o vertices) (nonFinals g))" in bexI)
  apply blast
 apply(subgoal_tac "∀f∈set (nonFinals g). vertices f ≠ []")
  apply(simp add:minimalVertex_def)
 apply(simp add:nonFinals_def)
apply simp
done

lemma mgp_next_plane0_if_next_plane:
  "minGraphProps g ==> g [next_planep]-> g' ==> g [next_plane0p]-> g'"
using next_plane_subset by(blast dest: mgp_vertices_nonempty)

lemma inv_inv_next_plane: "invariant inv next_planep"
apply(rule inv_subset[OF inv_inv_next_plane0])
apply(blast dest: mgp_next_plane0_if_next_plane[OF inv_mgp])
done




end