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

Download this file

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 \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"qsort le [] = []"
| "qsort le (x#xs) = qsort le [y\<leftarrow>xs . ~ le x y] @ [x] @
qsort le [y\<leftarrow>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 \<Rightarrow> nat" where
"nof_vertices = length o remdups o concat"
definition fgraph :: "graph \<Rightarrow> nat fgraph" where
"fgraph g = map vertices (faces g)"
definition hash :: "nat fgraph \<Rightarrow> 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\<leftarrow>fs. i \<in> set f]))
[0..<n]))"
primrec enum_finals :: "(graph \<Rightarrow> graph list) \<Rightarrow> nat \<Rightarrow> graph list \<Rightarrow> nat fgraph list
\<Rightarrow> 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 \<Rightarrow> nat \<Rightarrow> nat fgraph list option" where
"tameEnum p n = enum_finals (next_tame p) n [Seed p] []"
definition diff2 :: "nat fgraph list \<Rightarrow> nat fgraph list \<Rightarrow>
(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 \<Rightarrow> nat fgraph list \<Rightarrow> bool" where
"same fgso ags = (case fgso of None \<Rightarrow> False | Some fgs \<Rightarrow>
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 \<Rightarrow> bool" where
"pre_iso_test Fs \<longleftrightarrow>
[] \<notin> set Fs \<and> (\<forall>F\<in>set Fs. distinct F) \<and> distinct (map rotate_min Fs)"
end

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:





No, thanks