Up to index of Isabelle/HOL/Tame
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
lemma pre_iso_test3:
∀g∈set Tri. pre_iso_test g [!]
lemma pre_iso_test4:
∀g∈set Quad. pre_iso_test g [!]
lemma pre_iso_test5:
∀g∈set Pent. pre_iso_test g [!]
lemma pre_iso_test6:
∀g∈set Hex. pre_iso_test g [!]
lemma pre_iso_test7:
∀g∈set Hept. pre_iso_test g [!]
lemma pre_iso_test8:
∀g∈set Oct. pre_iso_test g [!]
lemma same3:
same (tameEnum 0 800000) Tri [!]
lemma same4:
same (tameEnum 1 8000000) Quad [!]
lemma same5:
same (tameEnum 2 20000000) Pent [!]
lemma same6:
same (tameEnum 3 4000000) Hex [!]
lemma same7:
same (tameEnum 4 1000000) Hept [!]
lemma same8:
same (tameEnum 5 2000000) Oct [!]