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