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 [!]