Skip to content
GitLab
Menu
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
isa-afp
afp-devel
Commits
5c7a3b0533b3
Commit
63b5296c
authored
Feb 23, 2021
by
haftmann
Browse files
more specific name
parent
f92a0d6fefa1
Changes
16
Hide whitespace changes
Inline
Side-by-side
thys/Affine_Arithmetic/Affine_Form.thy
View file @
5c7a3b05
...
...
@@ -2,7 +2,7 @@ section \<open>Affine Form\<close>
theory Affine_Form
imports
"HOL-Analysis.Multivariate_Analysis"
"HOL-Library.Permutation"
"HOL-Library.
List_
Permutation"
Affine_Arithmetic_Auxiliarities
Executable_Euclidean_Space
begin
...
...
thys/Berlekamp_Zassenhaus/Missing_Multiset2.thy
View file @
5c7a3b05
theory Missing_Multiset2
imports "HOL-Library.Multiset" "HOL-Library.Permutation" "HOL-Library.Permutations"
imports "HOL-Library.Multiset" "HOL-Library.
List_
Permutation" "HOL-Library.Permutations"
Containers.Containers_Auxiliary (* only for a lemma *)
begin
...
...
thys/Buchi_Complementation/Complementation_Final.thy
View file @
5c7a3b05
...
...
@@ -6,7 +6,7 @@ imports
"Formula"
"Transition_Systems_and_Automata.NBA_Translate"
"Transition_Systems_and_Automata.NGBA_Algorithms"
"HOL-Library.Permutation"
"HOL-Library.
List_
Permutation"
begin
subsection \<open>Syntax\<close>
...
...
thys/CakeML/generated/LemExtraDefs.thy
View file @
5c7a3b05
...
...
@@ -57,7 +57,7 @@ theory "LemExtraDefs"
imports
Main
"HOL-Library.Permutation"
"HOL-Library.
List_
Permutation"
"HOL-Library.While_Combinator"
begin
...
...
thys/CakeML/generated/Lem_sorting.thy
View file @
5c7a3b05
...
...
@@ -10,7 +10,7 @@ imports
"Lem_list"
"Lem_num"
"Lem"
"HOL-Library.Permutation"
"HOL-Library.
List_
Permutation"
begin
...
...
thys/Chandy_Lamport/Snapshot.thy
View file @
5c7a3b05
...
...
@@ -3,7 +3,7 @@ section \<open>The Chandy--Lamport algorithm\<close>
theory Snapshot
imports
"HOL-Library.Sublist"
"HOL-Library.Permutation"
"HOL-Library.
List_
Permutation"
Distributed_System
Trace
Util
...
...
thys/Chandy_Lamport/Util.thy
View file @
5c7a3b05
...
...
@@ -4,7 +4,7 @@ theory Util
imports
Main
"HOL-Library.Sublist"
"HOL-Library.Permutation"
"HOL-Library.
List_
Permutation"
begin
...
...
thys/Completeness/PermutationLemmas.thy
View file @
5c7a3b05
section "Permutation Lemmas"
theory PermutationLemmas
imports "HOL-Library.Permutation" "HOL-Library.Multiset"
imports "HOL-Library.
List_
Permutation" "HOL-Library.Multiset"
begin
\<comment> \<open>following function is very close to that in multisets- now we can make the connection that x <~~> y iff the multiset of x is the same as that of y\<close>
...
...
thys/Groebner_Macaulay/Hilbert_Function.thy
View file @
5c7a3b05
...
...
@@ -3,7 +3,7 @@
section \<open>Direct Decompositions and Hilbert Functions\<close>
theory Hilbert_Function
imports Dube_Prelims Degree_Section "HOL-Library.Permutation"
imports Dube_Prelims Degree_Section "HOL-Library.
List_
Permutation"
begin
subsection \<open>Direct Decompositions\<close>
...
...
thys/MuchAdoAboutTwo/MuchAdoAboutTwo.thy
View file @
5c7a3b05
...
...
@@ -8,7 +8,7 @@ section \<open>Much Ado about Two\<close>
(*<*)
theory MuchAdoAboutTwo
imports "HOL-Library.Permutation"
imports "HOL-Library.
List_
Permutation"
begin
(*>*)
...
...
@@ -1436,7 +1436,7 @@ proof -
using Multiset.set_eq_iff_mset_eq_distinct
[where x=js and y="[0..<k + 1]"] by simp
thus "js <~~> [0..<k + 1]"
using
Permutation.
mset_eq_perm [where xs=js and ys="[0..<k + 1]"]
using mset_eq_perm [where xs=js and ys="[0..<k + 1]"]
by simp
qed
...
...
@@ -1517,7 +1517,7 @@ proof (rule ccontr)
let ?r = "i - j"
from A1 and A3 have "distinct (xs @ ys)"
using
Permutation.
perm_distinct_iff [where xs="xs @ ys"] by auto
using perm_distinct_iff [where xs="xs @ ys"] by auto
hence xs_ys_inter_empty: "set xs \<inter> set ys = {}" by simp
from A2 and Figure_7_trans have
...
...
@@ -1528,7 +1528,7 @@ proof (rule ccontr)
proof -
have "i \<in> set js" using A4 and A3 by simp
hence "i \<in> set [0..<k + 1]"
using A1 and
Permutation.
perm_set_eq by blast
using A1 and perm_set_eq by blast
hence "i \<le> k" by auto
thus ?thesis using i_j by simp
qed
...
...
@@ -1560,12 +1560,12 @@ proof -
by blast
hence "sorted js" using partitions_sorted by blast
moreover have "distinct js"
using A1 and
Permutation.
perm_distinct_iff and List.distinct_upt by blast
using A1 and perm_distinct_iff and List.distinct_upt by blast
moreover have "sorted [0..<k + 1]"
using List.sorted_upt by blast
moreover have "distinct [0..<k + 1]" by simp
moreover have "set js = set [0..<k + 1]"
using A1 and
Permutation.
perm_set_eq by blast
using A1 and perm_set_eq by blast
ultimately show "js = [0..<k + 1]" using List.sorted_distinct_set_unique
by blast
qed
...
...
thys/Polynomial_Factorization/ROOT
View file @
5c7a3b05
...
...
@@ -34,7 +34,7 @@ session "JNF-AFP-Lib" (AFP) in "Lib" = "HOL-Algebra" +
"HOL-Library.Monad_Syntax"
"HOL-Library.More_List"
"HOL-Library.Multiset"
"HOL-Library.Permutation"
"HOL-Library.
List_
Permutation"
"HOL-Library.Permutations"
"HOL-Library.IArray"
"HOL-Library.Phantom_Type"
...
...
thys/Program-Conflict-Analysis/Interleave.thy
View file @
5c7a3b05
...
...
@@ -4,7 +4,7 @@
*)
section "List Interleaving Operator"
theory Interleave
imports Main "HOL-Library.Permutation" Misc
imports Main "HOL-Library.
List_
Permutation" Misc
begin
text_raw \<open>\label{thy:Interleave}\<close>
...
...
thys/Selection_Heap_Sort/Sort.thy
View file @
5c7a3b05
...
...
@@ -5,7 +5,7 @@ section \<open>Locale Sort\<close>
theory Sort
imports Main
"HOL-Library.Permutation"
"HOL-Library.
List_
Permutation"
begin
text \<open>
...
...
thys/Simpl/ex/Quicksort.thy
View file @
5c7a3b05
...
...
@@ -29,7 +29,7 @@ USA
section "Example: Quicksort on Heap Lists"
theory Quicksort
imports "../Vcg" "../HeapList" "HOL-Library.Permutation"
imports "../Vcg" "../HeapList" "HOL-Library.
List_
Permutation"
begin
record globals_heap =
...
...
thys/Simplex/Simplex.thy
View file @
5c7a3b05
...
...
@@ -8,7 +8,7 @@ theory Simplex
Rel_Chain
Simplex_Algebra
"HOL-Library.RBT_Mapping"
"HOL-Library.Permutation"
"HOL-Library.
List_
Permutation"
"HOL-Library.Code_Target_Numeral"
begin
...
...
thys/Simplex/Simplex_Auxiliary.thy
View file @
5c7a3b05
...
...
@@ -2,7 +2,7 @@
section \<open>Auxiliary Results\<close>
theory Simplex_Auxiliary
imports
"HOL-Library.Permutation"
"HOL-Library.
List_
Permutation"
"HOL-Library.Mapping"
begin
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment