## [7cfccc]: thys / Flyspeck-Tame / ArchCompAux.thy  Maximize  Restore  History

### 64 lines (51 with data), 2.8 kB

 ``` 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63``` ```(* Author: Tobias Nipkow *) header {* Comparing Enumeration and Archive *} theory ArchCompAux imports TameEnum TrieList Arch 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 o snd)") (auto simp add: length_filter_le [THEN le_less_trans]) definition nof_vertices :: "'a fgraph \ nat" where "nof_vertices = length o remdups o 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 (op +) 0 (map size [f\fs. i \ set f])) [0.. graph list) \ nat \ graph list \ nat fgraph list \ nat fgraph list option" where "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)" definition tameEnum :: "nat \ nat \ nat fgraph list option" where "tameEnum p n = enum_finals (next_tame p) n [Seed p] []" definition diff2 :: "nat fgraph list \ nat fgraph list \ (nat * nat fgraph) list * (nat * nat fgraph)list" where "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))" definition same :: "nat fgraph list option \ nat fgraph list \ bool" where "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))" definition pre_iso_test :: "vertex fgraph \ bool" where "pre_iso_test Fs \ [] \ set Fs \ (\F\set Fs. distinct F) \ distinct (map rotate_min Fs)" end ```