Commit 679b36ee authored by wenzelm's avatar wenzelm
Browse files

updated imports;

avoid confusion due to theory_qualifier;
parent 0927c83a0ea2
section \<open>Breadth First Search\<close>
theory Augmenting_Path_BFS
imports
"../Flow_Networks/Lib/Refine_Add_Fofu"
"../Flow_Networks/Graph_Impl"
Maxflow_Lib.Refine_Add_Fofu
Flow_Networks.Graph_Impl
begin
text \<open>
In this theory, we present a verified breadth-first search
......
section \<open>Combination with Network Checker\<close>
theory Edka_Checked_Impl
imports "../Flow_Networks/NetCheck" EdmondsKarp_Impl
imports Flow_Networks.NetCheck EdmondsKarp_Impl
begin
text \<open>
In this theory, we combine the Edmonds-Karp implementation with the
......
......@@ -2,8 +2,8 @@ section \<open>Implementation of the Edmonds-Karp Algorithm\<close>
theory EdmondsKarp_Impl
imports
EdmondsKarp_Algo
"Augmenting_Path_BFS"
"../Refine_Imperative_HOL/IICF/IICF"
Augmenting_Path_BFS
Refine_Imperative_HOL.IICF
begin
text \<open>We now implement the Edmonds-Karp algorithm.
......
section \<open>Edmonds-Karp Algorithm\<close>
theory EdmondsKarp_Termination_Abstract imports
"../Flow_Networks/Ford_Fulkerson"
Flow_Networks.Ford_Fulkerson
begin
lemma mlex_fst_decrI:
......
section \<open>The Ford-Fulkerson Method\<close>
theory FordFulkerson_Algo
imports
"../Flow_Networks/Ford_Fulkerson"
"../Flow_Networks/Lib/Refine_Add_Fofu"
Flow_Networks.Ford_Fulkerson
Maxflow_Lib.Refine_Add_Fofu
begin
text \<open>In this theory, we formalize the abstract Ford-Fulkerson
method, which is independent of how an augmenting path is chosen\<close>
......
(* TODO: That's quite specific to the BFS alg. Move to Edka! *)
theory Graph_Impl
imports "Lib/Refine_Add_Fofu" Graph
imports Maxflow_Lib.Refine_Add_Fofu Graph
begin
-- \<open>Fixing capacities to integer values\<close>
......
theory Fofu_Abs_Base
imports
Complex_Main
"~~/src/HOL/Library/Rewrite"
"../../Automatic_Refinement/Lib/Misc"
"../../Refine_Imperative_HOL/Lib/Sepref_Misc"
"../../Program-Conflict-Analysis/LTS"
"HOL-Library.Rewrite"
Automatic_Refinement.Misc
Refine_Imperative_HOL.Sepref_Misc
"Program-Conflict-Analysis.LTS"
begin
(* TODO: Move *)
......
theory Fofu_Impl_Base
imports
Fofu_Abs_Base
"../../Refine_Imperative_HOL/IICF/IICF"
"../../Refine_Imperative_HOL/Sepref_ICF_Bindings"
"~~/src/HOL/Library/Rewrite"
Refine_Imperative_HOL.IICF
Refine_Imperative_HOL.Sepref_ICF_Bindings
"HOL-Library.Rewrite"
begin
hide_type (open) List_Seg.node
......
theory Refine_Add_Fofu
imports
Fofu_Impl_Base
"../../DFS_Framework/Misc/DFS_Framework_Refine_Aux"
DFS_Framework.DFS_Framework_Refine_Aux
begin
hide_type (open) List_Seg.node
......
section \<open>Checking for Valid Network\<close>
theory NetCheck
imports
"Lib/Refine_Add_Fofu"
"Network"
"Graph_Impl"
"../DFS_Framework/Examples/Reachable_Nodes"
Maxflow_Lib.Refine_Add_Fofu
Network
Graph_Impl
DFS_Framework.Reachable_Nodes
begin
text \<open>
This theory contains code to read a network from an edge list,
......
section \<open>Implementation of Flow Networks\<close>
theory Network_Impl
imports
"Lib/Refine_Add_Fofu"
Maxflow_Lib.Refine_Add_Fofu
Ford_Fulkerson
begin
......
......@@ -8,8 +8,8 @@ session Maxflow_Lib (AFP) = Sepref_IICF +
DFS_Framework
Refine_Imperative_HOL
theories
"../DFS_Framework/DFS_Framework"
"../DFS_Framework/Examples/Reachable_Nodes"
DFS_Framework.DFS_Framework
DFS_Framework.Reachable_Nodes
"Lib/Fofu_Abs_Base"
"Lib/Fofu_Impl_Base"
"Lib/Refine_Add_Fofu"
......
(* Author: Andreas Lochbihler, ETH Zurich *)
theory MFMC_Finite imports
"EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract"
EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
"HOL-Library.While_Combinator"
begin
......
......@@ -7,7 +7,7 @@ matrices with given marginals based on a proof by Georg Kellerer
(Funktionen auf Produkträumen mit vorgegebenen Marginal-Funktionen).\<close>
theory Matrix_For_Marginals
imports "MFMC_Misc" "HOL-Library.Diagonal_Subsequence" "MFMC_Finite"
imports MFMC_Misc "HOL-Library.Diagonal_Subsequence" MFMC_Finite
begin
lemma bounded_matrix_for_marginals_finite:
......
......@@ -7,7 +7,7 @@ session "MFMC_Countable" (AFP) = "HOL-Probability" +
"HOL-Library.Transitive_Closure_Table"
"HOL-Library.Bourbaki_Witt_Fixpoint"
"HOL-Library.While_Combinator"
"EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract"
EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
theories
Max_Flow_Min_Cut_Countable
Rel_PMF_Characterisation
......
section \<open>FIFO Push Relabel Algorithm\<close>
theory Fifo_Push_Relabel
imports
"../Flow_Networks/Lib/Refine_Add_Fofu"
Maxflow_Lib.Refine_Add_Fofu
Generic_Push_Relabel
begin
text \<open>The FIFO push-relabel algorithm maintains a first-in-first-out queue
......
section \<open>Generic Push Relabel Algorithm\<close>
theory Generic_Push_Relabel
imports
"../Flow_Networks/Lib/Fofu_Abs_Base"
"../Flow_Networks/Ford_Fulkerson"
Maxflow_Lib.Fofu_Abs_Base
Flow_Networks.Ford_Fulkerson
begin
......
section "Topological Ordering of Graphs"
theory Graph_Topological_Ordering
imports
"../Refine_Imperative_HOL/Lib/Sepref_Misc"
"../List-Index/List_Index"
Refine_Imperative_HOL.Sepref_Misc
"List-Index.List_Index"
begin
subsection \<open>List-Before Relation\<close>
......
......@@ -2,8 +2,8 @@ section \<open>Tools for Implementing Push-Relabel Algorithms\<close>
theory Prpu_Common_Impl
imports
Prpu_Common_Inst
"../Flow_Networks/Network_Impl"
"../Flow_Networks/NetCheck"
Flow_Networks.Network_Impl
Flow_Networks.NetCheck
begin
subsection \<open>Basic Operations\<close>
......
theory Prpu_Common_Inst
imports
"../Flow_Networks/Lib/Refine_Add_Fofu"
Maxflow_Lib.Refine_Add_Fofu
Generic_Push_Relabel
begin
......
......@@ -3,7 +3,7 @@ chapter AFP
session Prpu_Maxflow (AFP) = Flow_Networks +
options [timeout = 600]
theories [document = false]
"../Net_Check/NetCheck"
Flow_Networks.NetCheck
theories
Generic_Push_Relabel
Prpu_Common_Inst
......
......@@ -2,7 +2,7 @@ section \<open>Relabel-to-Front Algorithm\<close>
theory Relabel_To_Front
imports
Prpu_Common_Inst
"Graph_Topological_Ordering"
Graph_Topological_Ordering
begin
text \<open>As an example for an implementation, Cormen et al.\ discuss the
relabel-to-front algorithm.
......
......@@ -70,17 +70,17 @@ session Refine_Imperative_HOL (AFP) = Sepref_Prereq +
(* Smaller Sessions: *)
session Sepref_Basic (AFP) = Sepref_Prereq +
options [document = false, timeout = 300, theory_qualifier = Refine_Imperative_HOL]
options [document = false, timeout = 300]
sessions
"HOL-Eisbach"
"List-Index"
Refine_Imperative_HOL
theories [document = false]
Sepref
Refine_Imperative_HOL.Sepref
session Sepref_IICF (AFP) = Sepref_Basic +
options [document = false, timeout = 600, theory_qualifier = Refine_Imperative_HOL]
options [document = false, timeout = 600]
sessions
Refine_Imperative_HOL
theories [document = false]
"IICF/IICF"
Refine_Imperative_HOL.IICF
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment