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 Fs1; pre_iso_test Fs2  
  iso_test Fs1 Fs2 = (Fs1  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 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 "hset 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