Up to index of Isabelle/HOL/Tame
theory ArchCompProps(* ID: $Id: ArchCompProps.thy,v 1.2 2006/01/18 07:20:42 nipkow Exp $
Author: Tobias Nipkow
*)
header "Completeness of Archive Test"
theory ArchCompProps
imports TameEnumProps ArchComp
begin
corollary iso_test_correct:
"[| pre_iso_test Fs1; pre_iso_test Fs2 |] ==>
iso_test (nof_vertices Fs1,Fs1) (nof_vertices Fs2,Fs2) = (Fs1 \<simeq> Fs2)"
by(simp add:pre_iso_test_def iso_correct inj_on_rotate_min_iff[symmetric]
distinct_map nof_vertices_def length_remdups_concat)
lemma same_imp_iso_subset:
assumes pre1: "!!gs g. gsopt = Some gs ==> g ∈ set gs ==> pre_iso_test g"
and pre2: "!!g. g ∈ set arch ==> pre_iso_test g"
and same: "same gsopt arch"
shows "∃gs. gsopt = Some gs ∧ set gs ⊆\<simeq> set arch"
proof -
obtain gs where [simp]: "gsopt = Some gs" and test: "!!g. g ∈ set gs ==>
∃h ∈ set arch. iso_test (nof_vertices g,g) (nof_vertices h,h)"
using same by(force simp:same_def split:option.splits
dest: in_set_lookup_trie_of_listD)
have "set gs ⊆\<simeq> set arch"
proof (auto simp:iso_subseteq_def iso_in_def)
fix g assume g: "g∈set gs"
obtain h where h: "h ∈ set arch" and
test: "iso_test (nof_vertices g,g) (nof_vertices h,h)"
using test[OF g] by blast
thus "∃h∈set arch. g \<simeq> h"
using h pre1[OF _ g] pre2[OF h] by (auto simp:iso_test_correct)
qed
thus ?thesis by auto
qed
lemma enum_finals_tree:
"∀g. final g --> next g = [] ==> enum_finals next n todo Fs0 = Some Fs ==>
set Fs = set Fs0 ∪ fgraph ` {h. ∃g ∈ set todo. g [next]->* h ∧ final h}"
apply(induct n fixing: todo Fs0) apply simp
apply (clarsimp simp:image_def neq_Nil_conv split:split_if_asm)
apply(rule equalityI)
apply (blast intro:RTranCl.refl)
apply(rule)
apply simp
apply(erule disjE) apply blast
apply (erule exE conjE)+
apply(erule disjE) apply (fastsimp elim:RTranCl_elim)
apply(blast)
apply(rule equalityI)
apply (blast intro:succs)
apply(rule)
apply simp
apply(erule disjE) apply blast
apply (erule exE conjE)+
apply(erule disjE) apply (fastsimp elim:RTranCl_elim)
apply(blast)
done
lemma next_tame_of_final: "∀g. final g --> next_tamep g = []"
by(auto simp: next_tame_def next_tame1_def next_tame0_def
nonFinals_def filter_empty_conv finalGraph_def)
lemma tameEnum_TameEnum: "tameEnum p n = Some Fs ==> set Fs = fgraph ` TameEnump"
by(simp add: tameEnum_def TameEnumP_def enum_finals_tree[OF next_tame_of_final])
lemma mgp_pre_iso_test: "minGraphProps g ==> pre_iso_test(fgraph g)"
apply(simp add:pre_iso_test_def fgraph_def image_def)
apply(rule conjI) apply(blast dest: mgp_vertices_nonempty[symmetric])
apply(rule conjI) apply(blast intro:minGraphProps)
apply(drule minGraphProps11)
apply(simp add:normFaces_def normFace_def verticesFrom_def minVertex_def
rotate_min_def map_compose[symmetric] o_def)
done
theorem combine_evals:
"∀g ∈ set arch. pre_iso_test g ==> same (tameEnum p n) arch
==> fgraph ` TameEnump ⊆\<simeq> set arch"
apply(subgoal_tac "∃gs. tameEnum p n = Some gs ∧ set gs ⊆\<simeq> set arch")
apply(fastsimp simp: image_def dest: tameEnum_TameEnum)
apply(fastsimp intro!: same_imp_iso_subset simp: image_def
dest: tameEnum_TameEnum mgp_TameEnum mgp_pre_iso_test)
done
end
corollary iso_test_correct:
[| pre_iso_test Fs1; pre_iso_test Fs2 |] ==> iso_test (nof_vertices Fs1, Fs1) (nof_vertices Fs2, Fs2) = Fs1 \<simeq> Fs2
lemma same_imp_iso_subset:
[| !!gs g. [| gsopt = Some gs; g ∈ set gs |] ==> pre_iso_test g; !!g. g ∈ set arch ==> pre_iso_test g; same gsopt arch |] ==> ∃gs. gsopt = Some gs ∧ set gs ⊆\<simeq> set arch
lemma enum_finals_tree:
[| ∀g. final g --> next g = []; enum_finals next n todo Fs0 = Some Fs |] ==> set Fs = set Fs0 ∪ fgraph ` {h. ∃g∈set todo. g [next]->* h ∧ final h}
lemma next_tame_of_final:
∀g. final g --> next_tamep g = []
lemma tameEnum_TameEnum:
tameEnum p n = Some Fs ==> set Fs = fgraph ` TameEnump
lemma mgp_pre_iso_test:
minGraphProps g ==> pre_iso_test (fgraph g)
theorem combine_evals:
[| ∀g∈set arch. pre_iso_test g; same (tameEnum p n) arch |] ==> fgraph ` TameEnump ⊆\<simeq> set arch