Theory ArchComp

(*  ID:         $Id: ArchComp.thy,v 1.4 2006/01/18 07:20:42 nipkow Exp $
    Author:     Tobias Nipkow
*)

header "Comparing Enumeration and Achive"

theory ArchComp
imports TameEnum TrieList Arch
begin

consts qsort :: "('a => 'a => bool) * 'a list => 'a list"
recdef qsort "measure (size o snd)"
    "qsort(le, [])   = []"
    "qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y]) @ [x] @
                       qsort(le, [y:xs . le x y])"
(hints recdef_simp: length_filter_le[THEN le_less_trans])

constdefs
 nof_vertices :: "'a fgraph => nat"
"nof_vertices == length o remdups o concat"

 fgraph :: "graph => nat fgraph"
"fgraph g == map vertices (faces g)"

 hash :: "nat fgraph => nat list"
"hash fs == let n = nof_vertices fs in
   [n, size fs] @
   qsort (%x y. y < x, map (%i. foldl (op +) 0 (map size [f:fs. i mem f]))
                           [0..<n])"

consts
 enum_finals :: "(graph => graph list) => nat => graph list => nat fgraph list
                 => nat fgraph list option"
primrec
"enum_finals succs 0 todo fins = None"
"enum_finals succs (Suc n) todo fins =
 (if todo = [] then Some fins
  else let g = hd todo; todo' = tl todo in
    if final g then enum_finals succs n todo' (fgraph g # fins)
    else enum_finals succs n (succs g @ todo') fins)"

constdefs
 tameEnum :: "nat => nat => nat fgraph list option"
"tameEnum p n == enum_finals (next_tame p) n [Seed p] []"

 diff2 :: "nat fgraph list => nat fgraph list =>
           (nat * nat fgraph) list * (nat * nat fgraph)list"
"diff2 fgs ags ==
 let xfgs = map (%fs. (nof_vertices fs, fs)) fgs;
     xags = map (%fs. (nof_vertices fs, fs)) ags in
 (filter (%xfg. ~list_ex (iso_test xfg) xags) xfgs,
  filter (%xag. ~list_ex (iso_test xag) xfgs) xags)"

 same :: "nat fgraph list option => nat fgraph list => bool"
"same fgso ags == case fgso of None => False | Some fgs =>
 let niso_test = (%fs1 fs2. iso_test (nof_vertices fs1,fs1)
                                     (nof_vertices fs2,fs2));
     tfgs = trie_of_list hash fgs;
     tags = trie_of_list hash ags in
 (list_all (%fg. list_ex (niso_test fg) (lookup_trie tags (hash fg))) fgs &
  list_all (%ag. list_ex (niso_test ag) (lookup_trie tfgs (hash ag))) ags)"

constdefs
 pre_iso_test :: "vertex fgraph => bool"
"pre_iso_test Fs ≡
 [] ∉ set Fs ∧ (∀F∈set Fs. distinct F) ∧ distinct (map rotate_min Fs)"

lemma pre_iso_test3: "∀g ∈ set Tri. pre_iso_test g"
by evaluation

lemma pre_iso_test4: "∀g ∈ set Quad. pre_iso_test g"
by evaluation

lemma pre_iso_test5: "∀g ∈ set Pent. pre_iso_test g"
by evaluation

lemma pre_iso_test6: "∀g ∈ set Hex. pre_iso_test g"
by evaluation

lemma pre_iso_test7: "∀g ∈ set Hept. pre_iso_test g"
by evaluation

lemma pre_iso_test8: "∀g ∈ set Oct. pre_iso_test g"
by evaluation


ML"set Toplevel.timing"

lemma same3: "same (tameEnum 0 800000) Tri"
by evaluation

lemma same4: "same (tameEnum 1 8000000) Quad"
by evaluation

lemma same5: "same (tameEnum 2 20000000) Pent"
by evaluation

lemma same6: "same (tameEnum 3 4000000) Hex"
by evaluation

lemma same7: "same (tameEnum 4 1000000) Hept"
by evaluation

lemma same8: "same (tameEnum 5 2000000) Oct"
by evaluation

ML"reset Toplevel.timing"

end