Theory ArchCompAux

(*  Author: Tobias Nipkow  *)

section ‹Comparing Enumeration and Archive›

theory ArchCompAux
imports TameEnum Trie.Tries Maps Arch Worklist
begin

function qsort :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ 'a list" where
"qsort le []       = []" |
"qsort le (x#xs) = qsort le [y←xs . ¬ le x y] @ [x] @
                   qsort le [y←xs . le x y]"
by pat_completeness auto
termination by (relation "measure (size ∘ snd)")
  (auto simp add: length_filter_le [THEN le_less_trans])

definition nof_vertices :: "'a fgraph ⇒ nat" where
"nof_vertices = length ∘ remdups ∘ concat"

definition fgraph :: "graph ⇒ nat fgraph" where
"fgraph g = map vertices (faces g)"

definition hash :: "nat fgraph ⇒ nat list" where
  "hash fs = (let n = nof_vertices fs in
     [n, size fs] @
     qsort (λx y. y < x) (map (λi. foldl (+) 0 (map size [f←fs. i ∈ set f]))
                             [0..<n]))"
(*
definition diff2 :: "nat fgraph list ⇒ nat fgraph list
   ⇒ nat fgraph list * nat fgraph list" where
"diff2 fgs ags =
 (let tfgs = trie_of_list hash fgs;
      tags = trie_of_list hash ags in
  (filter (λfg. ¬list_ex (iso_test fg) (lookup_trie tags (hash fg))) fgs,
   filter (λag. ¬list_ex (iso_test ag) (lookup_trie tfgs (hash ag))) ags))"
*)
definition samet :: "(nat,nat fgraph) tries option ⇒ nat fgraph list ⇒ bool"
where
  "samet fgto ags = (case fgto of None ⇒ False | Some tfgs ⇒
   let tags = tries_of_list hash ags in
   (all_tries (λfg. list_ex (iso_test fg) (lookup_tries tags (hash fg))) tfgs ∧
    all_tries (λag. list_ex (iso_test ag) (lookup_tries tfgs (hash ag))) tags))"

definition pre_iso_test :: "vertex fgraph ⇒ bool" where
  "pre_iso_test Fs ⟷
   [] ∉ set Fs ∧ (∀F∈set Fs. distinct F) ∧ distinct (map rotate_min Fs)"


interpretation map:
  maps "Trie None []" update_trie lookup_tries invar_trie
proof (standard, goal_cases)
  case 1 show ?case by(rule ext) simp
next
  case 2 show ?case by(rule ext) (simp add: lookup_update)
next
  case 3 show ?case by(simp)
next
  case 4 thus ?case by (simp add: invar_trie_update)
qed

lemma set_of_conv: "set_tries = maps.set_of lookup_tries"
by(rule ext) (auto simp add: set_tries_def map.set_of_def)

end