Diffusion afp-devel 2548b08bc3c4

merge from AFP 2023
2548b08bc3c4
Actions

Tags

None

Subscribers

None

Description

merge from AFP 2023

Details

Provenance

Rene Thiemann <rene.thiemann@uibk.ac.at>

Authored on

Parents

rAFP00fb7d6558e5: metadata and sitegen for MFOTL_Checker
rAFPdb43b58419ea: Removed unnecessary theory file 'Doob_Convergence.thy'

Branches

Unknown

Tags

Unknown

Event Timeline

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP2548b08bc3c4: merge from AFP 2023.Fri, Apr 19, 1:11 PM

Merged Changes

This commit merges a very large number of changes. Only the first 50 are shown.

ac2384b8b86d merged
Author
paulson
Browse Repository
No Builds
No Audits
105bd5da5e7e Updated KnuthMorrisPratt to include new definitions by Christian Zimmerer using…
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
db43b58419ea Removed unnecessary theory file 'Doob_Convergence.thy'
Author
Ata Keskin <ata.keskin@tum.de>
Browse Repository
No Builds
No Audits
59321c4a59e5 Updated Doob_Convergence to use the newest version of Martingales
Author
Ata Keskin <ata.keskin@tum.de>
Browse Repository
No Builds
No Audits
d8aa8cc91178 added equivalence of concepts between First_Order_Terms.Position and HOL…
Author
desharna
Browse Repository
No Builds
No Audits
900cfb1adad1 added lemmas inj_on_Fun_fun[simp], inj_on_Fun_args[simp], and inj_on_Fun[simp]
Author
desharna
Browse Repository
No Builds
No Audits
7f16aa37c534 proper getopts;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
5b2e7d535aff tuned: use explicit keys;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
2f55893686bc tuned;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
114c5bc73eff merged
Author
nipkow
Browse Repository
No Builds
No Audits
95692a54af6b tuned names
Author
nipkow
Browse Repository
No Builds
No Audits
408a29902df3 Removed inactive DOI
Author
Thibault Dardinier <thibault.dardinier@inf.ethz.ch>
Browse Repository
No Builds
No Audits
e0dfdf1b8ed4 Removed inactive DOI
Author
Thibault Dardinier <thibault.dardinier@inf.ethz.ch>
Browse Repository
No Builds
No Audits
d81723aa95cb added monotonicity lemmas of lex/mul-ext
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
d8fb49658d5f more showl-real instantiation to Show_Real thy
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
1c2509fdeac7 added showl-functions for terms and contexts
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
a52546d735ec merge
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
c61a0a701a26 added many results on first-order terms, added positions
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
eaea08280462 updated docs;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
c34ca8a848b0 proper keys (amending 36cf00eeb9e4);
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
6539b6f3e1cf add separate Isabelle tool for metadata editing;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
d2e29e073f08 better defaults;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
bec250baad75 clarified AFP base dir: usually given by environment;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
8fd1acd065c6 activate slow metadata checks by default;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
bd75044b84f8 fix broken metadata introduced by 20b8a26117af;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
81de808826f9 updated:Standard_Borel_Spaces
Author
Michikazu Hirata <hirata.m.ac@m.titech.ac.jp>
Browse Repository
No Builds
No Audits
2db006965e8e fix document generator: _ -> -
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
62f87ac53318 update: Standard_Borel_Spaces
Author
Michikazu Hirata <hirata.m.ac@m.titech.ac.jp>
Browse Repository
No Builds
No Audits
bbd1dc798620 Merged
Author
Thibault Dardinier <thibault.dardinier@inf.ethz.ch>
Browse Repository
No Builds
No Audits
20b8a26117af Updated HyperHoareLogic entry: Additional rules
Author
Thibault Dardinier <thibault.dardinier@inf.ethz.ch>
Browse Repository
No Builds
No Audits
f7ec8c203092 tune imports
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
c60abfef602f polished theory
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
f5b7116751a9 documented recent changes
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
43c62567dc63 documented changes in Show-entry
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
b086e875e09b use new XML-transformer from IsaFoR, developed by A. Yamada
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
b95e62c4c808 provide additional argument so that code-generation in SML/Eval does not fail
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
8e2e746ba2c0 drop explicit injectivity proof, provide parsers for nat and int instead and…
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
f96cdc08e452 clarified check roots module;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
05b5fea0d115 tuned;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
14d24fbe8ffa tuned error messages;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
9bff600ba0bc updated Standard Borel and S-finite measure monad
Author
Michikazu Hirata <hirata.m.ac@m.titech.ac.jp>
Browse Repository
No Builds
No Audits
a6d153d38d4b Multirelations_Heterogeneous: added Hoare rules for multirelations
Author
Walter Guttmann <walter.guttmann@canterbury.ac.nz>
Browse Repository
No Builds
No Audits
c60cdb60c99c tuned proofs: avoid z3 to make it work on arm64-linux;
Author
makarius
Browse Repository
No Builds
No Audits
b5c20c32ec87 tuned proofs: avoid z3 to make it work on arm64-linux;
Author
makarius
Browse Repository
No Builds
No Audits
d874320a81ca tuned proofs: avoid z3 to make it work on arm64-linux;
Author
makarius
Browse Repository
No Builds
No Audits
31fcd760227c tuned proofs: avoid z3 to make it work on arm64-linux;
Author
makarius
Browse Repository
No Builds
No Audits
ec1c704f4022 tuned proofs: avoid z3 to make it work on arm64-linux;
Author
makarius
Browse Repository
No Builds
No Audits
09e32ec351bb v1.0.1.0
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
df6613b912d9 v1.0.1.0
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
1d9d53077605 Median_Method: Add converse of lemma median_est and simplify (corresponding)…
Author
Emin Karayel <me@eminkarayel.de>
Browse Repository
No Builds
No Audits

Changes (202)
Show All Changes

Very Large Commit

This commit is very large. Load each file individually.

Path

Size

Broadcast_Psi.toml

ConcurrentHOL.toml

MFOTL_Checker.toml

Uncertainty_Principle.toml

Bisim_Struct_Cong.thy

Bisim_Subst.thy

Bisimulation.thy

Broadcast_Chain.thy

Broadcast_Frame.thy

Broadcast_Thms.thy

Sim_Struct_Cong.thy

Aczel_Sequences.thy

CImperativeHOL.thy

TSO_Code_Gen.thy

Floyd_Warshall.thy

Combinators.thy

ConcurrentHOL.thy

Constructions.thy

Lifted_Predicates.thy

Local_State.thy

More_Lattices.thy

Safety_Logic.thy

Assume_Guarantee.thy

Inhabitation.thy

Safety_Closure.thy

WickersonDoddsParkinson.thy

Example-Submission/

Checker_Code.thy

Proof_Object.thy

Proof_System.thy

Uncertainty_Principle

Uncertainty_Principle.thy

gammie/

munive/

pohjola/

raszyk/

traytel/

weber/

data/

coinductive/

mfotl_monitor/

optics/

qhlprover/

Approximation_Algorithms.html

Broadcast_Psi.html

Coinductive.html

Combinatorics_Words.html

Commuting_Hermitian.html

ConcurrentHOL.html

CubicalCategories.html

Efficient_Weighted_Path_Order.html

Frequency_Moments.html

HoareForDivergence.html

HyperHoareLogic.html

Hypergraph_Colourings.html

List_Update.html

MFODL_Monitor_Optimized.html

MFOTL_Checker.html

MFOTL_Monitor.html

OmegaCatoidsQuantales.html

Polygonal_Number_Theorem.html

Prim_Dijkstra_Simple.html

Propositional_Proof_Systems.html

Psi_Calculi.html

Quantales_Converse.html

Relational_Cardinality.html

S_Finite_Measure_Monad.html

Standard_Borel_Spaces.html

Uncertainty_Principle.html

Wieferich_Kempner.html

uncertainty_principle

statistics/

topics/

computer-science/

algorithms/

concurrency/

process-calculi/

data-management-systems/

logic/

general-logic/

temporal-logic/

mathematics/

physics/

quantum-information/

rAFP2548b08bc3c4

metadata/authors.toml

metadata/entries/Broadcast_Psi.toml

metadata/entries/ConcurrentHOL.toml

metadata/entries/MFOTL_Checker.toml

metadata/entries/Uncertainty_Principle.toml

thys/Broadcast_Psi/Bisim_Pres.thy

thys/Broadcast_Psi/Bisim_Struct_Cong.thy

thys/Broadcast_Psi/Bisim_Subst.thy

thys/Broadcast_Psi/Bisimulation.thy

thys/Broadcast_Psi/Broadcast_Chain.thy

thys/Broadcast_Psi/Broadcast_Frame.thy

thys/Broadcast_Psi/Broadcast_Thms.thy

thys/Broadcast_Psi/ROOT

thys/Broadcast_Psi/Semantics.thy

thys/Broadcast_Psi/Sim_Pres.thy

thys/Broadcast_Psi/Sim_Struct_Cong.thy

thys/Broadcast_Psi/Simulation.thy

thys/Broadcast_Psi/document/root.bib

thys/Broadcast_Psi/document/root.tex

thys/ConcurrentHOL/Aczel_Sequences.thy

thys/ConcurrentHOL/CImperativeHOL/CImperativeHOL.thy

thys/ConcurrentHOL/CImperativeHOL/Heap.thy

thys/ConcurrentHOL/CImperativeHOL/Ix.thy

thys/ConcurrentHOL/CImperativeHOL/TSO.sml

thys/ConcurrentHOL/CImperativeHOL/TSO.thy

thys/ConcurrentHOL/CImperativeHOL/TSO_Code_Gen.thy

thys/ConcurrentHOL/CImperativeHOL/ex/Floyd_Warshall.thy

thys/ConcurrentHOL/CImperativeHOL/ex/TSO_litmus.thy

thys/ConcurrentHOL/Closures.thy

thys/ConcurrentHOL/Combinators.thy

thys/ConcurrentHOL/ConcurrentHOL.thy

thys/ConcurrentHOL/Constructions.thy

thys/ConcurrentHOL/Galois.thy

thys/ConcurrentHOL/HOL_Basis.thy

thys/ConcurrentHOL/Heyting.thy

thys/ConcurrentHOL/Lifted_Predicates.thy

thys/ConcurrentHOL/Local_State.thy

thys/ConcurrentHOL/More_Lattices.thy

thys/ConcurrentHOL/Next_Imp.thy

thys/ConcurrentHOL/Programs.thy

thys/ConcurrentHOL/ROOT

thys/ConcurrentHOL/Refinement.thy

thys/ConcurrentHOL/Safety_Logic.thy

thys/ConcurrentHOL/Stability.thy

thys/ConcurrentHOL/TLS.thy

thys/ConcurrentHOL/document/root.bib

thys/ConcurrentHOL/document/root.tex

thys/ConcurrentHOL/ex/Assume_Guarantee.thy

thys/ConcurrentHOL/ex/Atomic.thy

thys/ConcurrentHOL/ex/BFS.thy

thys/ConcurrentHOL/ex/Exceptions.thy

thys/ConcurrentHOL/ex/FindP.thy

thys/ConcurrentHOL/ex/Inhabitation.thy

thys/ConcurrentHOL/ex/Safety_Closure.thy

thys/ConcurrentHOL/ex/WickersonDoddsParkinson.thy

thys/ConcurrentHOL/tools/Strengthen.thy

thys/Example-Submission/ROOT

thys/MFOTL_Checker/Checker.thy

thys/MFOTL_Checker/Checker_Code.thy

thys/MFOTL_Checker/Event_Data.thy

thys/MFOTL_Checker/Examples.thy

thys/MFOTL_Checker/Formula.thy

thys/MFOTL_Checker/Monitor.thy

thys/MFOTL_Checker/Partition.thy

thys/MFOTL_Checker/Prelim.thy

thys/MFOTL_Checker/Proof_Object.thy

thys/MFOTL_Checker/Proof_System.thy

thys/MFOTL_Checker/ROOT

thys/MFOTL_Checker/Trace.thy

thys/MFOTL_Checker/document/root.bib

thys/MFOTL_Checker/document/root.tex

thys/ROOTS

thys/Uncertainty_Principle/ROOT

thys/Uncertainty_Principle/Uncertainty_Principle.thy

thys/Uncertainty_Principle/document/root.bib

thys/Uncertainty_Principle/document/root.tex

web/authors/gammie/index.html

web/authors/gammie/index.xml

web/authors/herasimau/index.html

web/authors/herasimau/index.xml

web/authors/index.html

web/authors/index.json

web/authors/lima/index.html

web/authors/lima/index.xml

web/authors/munive/index.html

web/authors/munive/index.xml

web/authors/pohjola/index.html

web/authors/pohjola/index.xml

web/authors/raabjerg/index.html

web/authors/raabjerg/index.xml

web/authors/raszyk/index.html

web/authors/raszyk/index.xml

web/authors/traytel/index.html

web/authors/traytel/index.xml

web/authors/treml/index.html

web/authors/treml/index.xml

web/authors/weber/index.html

web/authors/weber/index.xml

web/data/keywords.json

web/dependencies/coinductive/index.html

web/dependencies/coinductive/index.xml

web/dependencies/index.html

web/dependencies/index.json

web/dependencies/mfotl_monitor/index.html

web/dependencies/mfotl_monitor/index.xml

web/dependencies/optics/index.html

web/dependencies/optics/index.xml

web/dependencies/psi_calculi/index.html

web/dependencies/psi_calculi/index.xml

web/dependencies/qhlprover/index.html

web/dependencies/qhlprover/index.xml

web/entries/Approximation_Algorithms.html

web/entries/Broadcast_Psi.html

web/entries/Catoids.html

web/entries/Coinductive.html

web/entries/Combinatorics_Words.html

web/entries/Commuting_Hermitian.html

web/entries/ConcurrentHOL.html

web/entries/CubicalCategories.html

web/entries/Efficient_Weighted_Path_Order.html

web/entries/Frequency_Moments.html

web/entries/HoareForDivergence.html

web/entries/HyperHoareLogic.html

web/entries/Hypergraph_Colourings.html

web/entries/List_Update.html

web/entries/MFODL_Monitor_Optimized.html

web/entries/MFOTL_Checker.html

web/entries/MFOTL_Monitor.html

web/entries/OmegaCatoidsQuantales.html

web/entries/Optics.html

web/entries/Polygonal_Number_Theorem.html

web/entries/Prim_Dijkstra_Simple.html

web/entries/Propositional_Proof_Systems.html

web/entries/Psi_Calculi.html

web/entries/QHLProver.html

web/entries/Quantales_Converse.html

web/entries/ROBDD.html

web/entries/Relational_Cardinality.html

web/entries/S_Finite_Measure_Monad.html

web/entries/Standard_Borel_Spaces.html

web/entries/Transport.html

web/entries/Uncertainty_Principle.html

web/entries/Wieferich_Kempner.html

web/entries/index.html

web/entries/index.xml

web/index.html

web/index.json

web/index.xml

web/sessions/broadcast_psi/index.html

web/sessions/concurrenthol/index.html

web/sessions/index.xml

web/sessions/mfotl_checker/index.html

web/sessions/uncertainty_principle/index.html

web/sitemap.xml

web/statistics/index.html

web/topics/computer-science/algorithms/index.html

web/topics/computer-science/algorithms/index.xml

web/topics/computer-science/concurrency/index.html

web/topics/computer-science/concurrency/index.xml

web/topics/computer-science/concurrency/process-calculi/index.html

web/topics/computer-science/concurrency/process-calculi/index.xml

web/topics/computer-science/data-management-systems/index.html

web/topics/computer-science/data-management-systems/index.xml

web/topics/computer-science/index.xml

web/topics/index.html

web/topics/logic/general-logic/index.xml

web/topics/logic/general-logic/temporal-logic/index.html

web/topics/logic/general-logic/temporal-logic/index.xml

web/topics/logic/index.xml

web/topics/mathematics/index.xml

web/topics/mathematics/physics/index.xml

web/topics/mathematics/physics/quantum-information/index.html

web/topics/mathematics/physics/quantum-information/index.xml