Theory ArchCompProps

Up to index of Isabelle/HOL/Tame

theory ArchCompProps
imports TameEnumProps ArchComp
begin

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