Read about our upcoming Code of Conduct on this issue

Commit 52ffd95c authored by haftmann's avatar haftmann
Browse files

dedicated session for combinatorial material

parent 184d9cadd5ca
......@@ -2,7 +2,7 @@ section \<open>Affine Form\<close>
theory Affine_Form
imports
"HOL-Analysis.Multivariate_Analysis"
"HOL-Library.List_Permutation"
"HOL-Combinatorics.List_Permutation"
Affine_Arithmetic_Auxiliarities
Executable_Euclidean_Space
begin
......
......@@ -4,6 +4,7 @@ session Affine_Arithmetic (AFP) = "HOL-Analysis" +
options [timeout = 2400]
sessions
"HOL-Decision_Procs"
"HOL-Combinatorics"
"List-Index"
Deriving
Show
......
......@@ -6,7 +6,7 @@ theory Bell_Numbers
imports
"HOL-Library.FuncSet"
"HOL-Library.Monad_Syntax"
"HOL-Library.Stirling"
"HOL-Combinatorics.Stirling"
Card_Partitions.Injectivity_Solver
Card_Partitions.Card_Partitions
begin
......
theory Missing_Multiset2
imports "HOL-Library.Permutations"
imports "HOL-Combinatorics.Permutations"
Containers.Containers_Auxiliary (* only for a lemma *)
begin
......
......@@ -2,7 +2,7 @@ theory Unique_Factorization
imports
Polynomial_Interpolation.Ring_Hom_Poly
Polynomial_Factorization.Polynomial_Divisibility
"HOL-Library.Permutations"
"HOL-Combinatorics.Permutations"
"HOL-Computational_Algebra.Euclidean_Algorithm"
Containers.Containers_Auxiliary (* only for a lemma *)
Missing_Multiset2
......
......@@ -11,8 +11,8 @@ theory Bernoulli_FPS
imports
Bernoulli
"HOL-Computational_Algebra.Computational_Algebra"
"HOL-Combinatorics.Stirling"
"HOL-Number_Theory.Number_Theory"
"HOL-Library.Stirling"
begin
subsection \<open>Preliminaries\<close>
......
......@@ -5,6 +5,7 @@ session Bernoulli (AFP) = "HOL-Complex_Analysis" +
sessions
"HOL-Analysis"
"HOL-Number_Theory"
"HOL-Combinatorics"
"HOL-Computational_Algebra"
theories
Bernoulli
......
......@@ -15,6 +15,7 @@ session LEM (AFP) in "generated" = HOL +
session CakeML (AFP) = LEM +
options [timeout = 3600]
sessions
"HOL-Combinatorics"
Coinductive
IEEE_Floating_Point
Show
......
......@@ -57,8 +57,8 @@ theory "LemExtraDefs"
imports
Main
"HOL-Combinatorics.List_Permutation"
"HOL-Library.While_Combinator"
"HOL-Library.List_Permutation"
begin
hide_const (open) sign
......
......@@ -10,7 +10,7 @@ imports
"Lem_list"
"Lem_num"
"Lem"
"HOL-Library.List_Permutation"
"HOL-Combinatorics.List_Permutation"
begin
......
......@@ -4,7 +4,7 @@ section \<open>Cardinality of Set Partitions\<close>
theory Card_Partitions
imports
"HOL-Library.Stirling"
"HOL-Combinatorics.Stirling"
Set_Partition
Injectivity_Solver
begin
......
......@@ -3,6 +3,7 @@ chapter AFP
session Card_Partitions (AFP) = HOL +
options [timeout = 600]
sessions
"HOL-Combinatorics"
"HOL-Eisbach"
Discrete_Summation
theories
......
......@@ -10,7 +10,7 @@ section \<open>Linear orderings as relations\<close>
theory Linorder_Relations
imports
Complex_Main
"HOL-Library.Multiset_Permutations"
"HOL-Combinatorics.Multiset_Permutations"
"List-Index.List_Index"
begin
......
......@@ -3,6 +3,7 @@ chapter AFP
session Comparison_Sort_Lower_Bound (AFP) = Stirling_Formula +
options [timeout = 300]
sessions
"HOL-Combinatorics"
"List-Index"
Landau_Symbols
theories
......
......@@ -5,7 +5,7 @@ section \<open>Derangements\<close>
theory Derangements
imports
Complex_Main
"HOL-Library.Permutations"
"HOL-Combinatorics.Permutations"
begin
subsection \<open>Preliminaries\<close>
......@@ -17,7 +17,7 @@ lemma card_product_dependent:
shows "card {(x, y). x \<in> S \<and> y \<in> T x} = (\<Sum>x \<in> S. card (T x))"
using card_SigmaI[OF assms, symmetric] by (auto intro!: arg_cong[where f=card] simp add: Sigma_def)
subsubsection \<open>Additions to @{theory "HOL-Library.Permutations"} Theory\<close>
subsubsection \<open>Additions to @{theory "HOL-Combinatorics.Permutations"} Theory\<close>
lemma permutes_imp_bij':
assumes "p permutes S"
......
......@@ -4,6 +4,7 @@ session Derangements (AFP) = HOL +
options [timeout = 600]
sessions
"HOL-Library"
"HOL-Combinatorics"
theories
Derangements
document_files
......
......@@ -4,7 +4,7 @@
section \<open>Falling factorials\<close>
theory Factorials
imports Complex_Main "HOL-Library.Stirling"
imports Complex_Main "HOL-Combinatorics.Stirling"
begin
lemma pochhammer_0 [simp]: \<comment> \<open>TODO move\<close>
......
......@@ -4,6 +4,7 @@ session Discrete_Summation (AFP) = HOL +
options [timeout = 600]
sessions
"HOL-Library"
"HOL-Combinatorics"
theories
Examples
document_files
......
theory Bidirected_Digraph
imports
Digraph
"HOL-Library.Permutations"
"HOL-Combinatorics.Permutations"
begin
section \<open>Bidirected Graphs\<close>
......
theory Funpow
imports
"HOL-Library.FuncSet"
"HOL-Library.Permutations"
"HOL-Combinatorics.Permutations"
begin
section \<open>Auxiliary Lemmas about @{term "(^^)"}\<close>
......
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