# Theory Plane1Props

Up to index of Isabelle/HOL/Tame

theory Plane1Props
imports Plane1 PlaneProps Tame
begin

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

lemma next_plane_subset:

`  ∀f∈\<F> g. vertices f ≠ [] ==> set (next_planep g) ⊆ set (next_plane0p g)`

lemma mgp_next_plane0_if_next_plane:

`  [| minGraphProps g; g' ∈ set (next_planep g) |] ==> g' ∈ set (next_plane0p g)`

lemma inv_inv_next_plane:

`  invariant Invariants.inv next_planep`