Theory ArchCompProps

(*  Author: Tobias Nipkow  *)

section "Completeness of Archive Test"

theory ArchCompProps
imports TameEnumProps ArchCompAux
begin
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 o_def)
done

corollary iso_test_correct:
 "⟦ pre_iso_test Fs⇩1; pre_iso_test Fs⇩2 ⟧ ⟹
  iso_test Fs⇩1 Fs⇩2 = (Fs⇩1 ≃ Fs⇩2)"
by(simp add:pre_iso_test_def iso_correct inj_on_rotate_min_iff[symmetric]
            distinct_map nof_vertices_def length_remdups_concat)

lemma trie_all_eq_set_of_trie:
  "invar_trie t ⟹ all_trie (list_all P) t = (∀v ∈ set_tries t. P v)"
by(simp add: all_trie_eq_ran set_tries_eq_ran)

lemma samet_imp_iso_seteq:
assumes pre1: "⋀gs g. gsopt = Some gs ⟹ g ∈ set_tries gs ⟹ pre_iso_test g"
and pre2: "⋀g. g ∈ set arch ⟹ pre_iso_test g"
and inv: "⋀gs. gsopt = Some gs ⟹ invar_trie gs"
and same: "samet gsopt arch"
shows "∃gs. gsopt = Some gs ∧ set_tries gs =⇩≃ set arch"
proof -
  obtain gs where [simp]: "gsopt = Some gs" and test1: "⋀g. g ∈ set_tries gs ⟹
    ∃h ∈ set arch. iso_test g h" and test2: "⋀g. g ∈ set arch ⟹
    ∃h ∈ set_tries gs. iso_test g h"
    using same inv
    by(force simp: samet_def trie_all_eq_set_of_trie invar_of_list all_tries_def
      split:option.splits
      dest: in_set_lookup_of_listD in_set_lookup_set_triesD)
  have "set_tries gs ⊆⇩≃ set arch"
  proof (auto simp:qle_gr.defs)
    fix g assume g: "g ∈ set_tries gs"
    obtain h where h: "h ∈ set arch" and test: "iso_test g h"
      using test1[OF g] by blast
    thus "∃h∈set arch. g ≃ h"
      using h pre1[OF _ g] pre2[OF h] by (auto simp:iso_test_correct)
  qed
  moreover
  have "set arch ⊆⇩≃ set_tries gs"
  proof (auto simp:qle_gr.defs)
    fix g assume g: "g ∈ set arch"
    obtain h where h: "h ∈ set_tries gs" and test: "iso_test g h"
      using test2[OF g] by blast
    thus "∃h ∈ set_tries gs. g ≃ h"
      using h pre1[OF _ h] pre2[OF g] by (auto simp:iso_test_correct)
  qed
  ultimately show ?thesis by (auto simp: qle_gr.seteq_qle_def)
qed

lemma samet_imp_iso_subseteq:
assumes pre1: "⋀gs g. gsopt = Some gs ⟹ g ∈ set_tries gs ⟹ pre_iso_test g"
and pre2: "⋀g. g ∈ set arch ⟹ pre_iso_test g"
and inv: "⋀gs. gsopt = Some gs ⟹ invar_trie gs"
and same: "samet gsopt arch"
shows "∃gs. gsopt = Some gs ∧ set_tries gs ⊆⇩≃ set arch"
using qle_gr.seteq_qle_def assms samet_imp_iso_seteq by metis

global_interpretation set_mod_trie:
  set_mod_maps "Trie None []" update_trie lookup_tries invar_trie "(≃)" iso_test pre_iso_test hash
  defines insert_mod_trie = "set_mod_maps.insert_mod update_trie lookup_tries iso_test hash"
  and worklist_tree_coll_trie = "set_modulo.worklist_tree_coll (Trie None []) insert_mod_trie"
  and worklist_tree_coll_aux_trie = "set_modulo.worklist_tree_coll_aux insert_mod_trie"
  and insert_mod2_trie = "set_modulo.insert_mod2 insert_mod_trie"
  by standard (simp_all add: iso_test_correct)

definition enum_filter_finals ::
  "(graph ⇒ graph list) ⇒ graph list
   ⇒ (nat,nat fgraph) tries option" where
"enum_filter_finals succs = set_mod_trie.worklist_tree_coll succs final fgraph"

definition tameEnumFilter :: "nat ⇒ (nat,nat fgraph)tries option" where
"tameEnumFilter p = enum_filter_finals (next_tame p) [Seed p]"

lemma TameEnum_tameEnumFilter:
  "tameEnumFilter p = Some t ⟹  set_tries t  =⇩≃ fgraph ` TameEnum⇘p⇙"
apply(auto simp: tameEnumFilter_def TameEnumP_def enum_filter_finals_def)
apply(drule set_mod_trie.worklist_tree_coll_equiv[OF _ inv_inv_next_tame])
apply (auto simp: set_of_conv inv_Seed mgp_pre_iso_test RTranCl_conv)
done

lemma tameEnumFilter_subseteq_TameEnum:
  "tameEnumFilter p = Some t ⟹ set_tries t ⊆ fgraph ` TameEnum⇘p⇙"
by(auto simp add:tameEnumFilter_def TameEnumP_def enum_filter_finals_def
     set_of_conv inv_Seed mgp_pre_iso_test RTranCl_conv
     dest!: set_mod_trie.worklist_tree_coll_subseteq[OF _ inv_inv_next_tame])


lemma inv_tries_tameEnumFilter:
  "tameEnumFilter p = Some t ⟹ invar_trie t"
unfolding tameEnumFilter_def enum_filter_finals_def
by(erule set_mod_trie.worklist_tree_coll_inv)

theorem combine_evals_filter:
 "∀g ∈ set arch. pre_iso_test g ⟹ samet (tameEnumFilter p) arch
  ⟹ fgraph ` TameEnum⇘p⇙ ⊆⇩≃ set arch"
apply(subgoal_tac "∃t. tameEnumFilter p = Some t ∧ set_tries t ⊆⇩≃ set arch")
 apply(metis TameEnum_tameEnumFilter qle_gr.seteq_qle_def qle_gr.subseteq_qle_trans)
apply(fastforce intro!: samet_imp_iso_subseteq
  dest: inv_tries_tameEnumFilter tameEnumFilter_subseteq_TameEnum mgp_TameEnum mgp_pre_iso_test)
done

end