Diffusion afp-devel 5172f1f451e6

merge from afp 2020
5172f1f451e6
Actions

Tags

None

Subscribers

None

Description

merge from afp 2020

Details

Provenance

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

Authored on

Parents

rAFP16b4ee88928e: metadata and website for EFSMs
rAFPa33da03f735c: fix for the new, simpler power_diff_1_eq

Branches

Unknown

Tags

Unknown

Event Timeline

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP5172f1f451e6: merge from afp 2020.Sep 19 2020, 8:27 AM

Merged Changes

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

a33da03f735c fix for the new, simpler power_diff_1_eq
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
210e8c4c943d fix Inductive_Inference
Author
Lars Hupel <lars.hupel@mytum.de>
Browse Repository
No Builds
No Audits
efbce6681b7a dropped junk
Author
florian.haftmann
Browse Repository
No Builds
No Audits
58bc7e81bc7f integrated generic conversions into word corpse
Author
florian.haftmann
Browse Repository
No Builds
No Audits
85d5b6c0bb92 adjusted to changes in distribution
Author
florian.haftmann
Browse Repository
No Builds
No Audits
f682365c61ce tuned proof
Author
florian.haftmann
Browse Repository
No Builds
No Audits
6d6d59e3f9f1 a tiny bit of beautification
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
90b7048e6e0a proper Unix line ending;
Author
makarius
Browse Repository
No Builds
No Audits
5d0b5731d5d7 prefer current mathpartir.sty from underlying TeX distribution;
Author
makarius
Browse Repository
No Builds
No Audits
f199a36357f5 update PAC_Checker to latest Isabelle
Author
mathias.fleury
Browse Repository
No Builds
No Audits
b39b8408a202 saturation framework: tiebreaker lifting locale improvement
Author
Sophie Tourret <stourret@mpi-inf.mpg.de>
Browse Repository
No Builds
No Audits
5d6a17e03f20 merge
Author
Sophie Tourret <stourret@mpi-inf.mpg.de>
Browse Repository
No Builds
No Audits
9e9d54326ae0 saturation framework: correction of static_to_dynamic lemma statement
Author
Sophie Tourret <stourret@mpi-inf.mpg.de>
Browse Repository
No Builds
No Audits
2fb39c7dd7ff merge from afp-2020
Author
kleing
Browse Repository
No Builds
No Audits
aade54113506 saturation framework: completes standard_lifting restructuration
Author
Sophie Tourret <stourret@mpi-inf.mpg.de>
Browse Repository
No Builds
No Audits
21bc345f5a27 generalized signed_take_bit
Author
florian.haftmann
Browse Repository
No Builds
No Audits
3c01c6d69e78 more on conversions
Author
florian.haftmann
Browse Repository
No Builds
No Audits
d99a51136b97 saturation framework: fills standard lifting locale
Author
Sophie Tourret <stourret@mpi-inf.mpg.de>
Browse Repository
No Builds
No Audits
0a2b5e06621c renamings
Author
blanchette
Browse Repository
No Builds
No Audits
075c0450120d tuned notation
Author
blanchette
Browse Repository
No Builds
No Audits
f15cc3b9e238 a repair and considerable reformatting
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
a22073e6cb92 tuning
Author
blanchette
Browse Repository
No Builds
No Audits
cb48e644eda2 adapted to "subst" of Isabelle/e5fcbf6dc687;
Author
makarius
Browse Repository
No Builds
No Audits
59b5d2617e31 more systematic support for special directories (see Isabelle/5894859c5c84);
Author
makarius
Browse Repository
No Builds
No Audits
516d4e0ad2e0 fix latex compilation of saturation framework
Author
Sophie Tourret <stourret@mpi-inf.mpg.de>
Browse Repository
No Builds
No Audits
f87125c95a68 removal of library theorems that were already in Isabelle main
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
91ce4a639768 comments in saturation framework
Author
Sophie Tourret <stourret@mpi-inf.mpg.de>
Browse Repository
No Builds
No Audits
f22a73cc49a1 tuned arrows, and proofs
Author
blanchette
Browse Repository
No Builds
No Audits
c812b6895caa variable renaming
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
023af1e22f70 more on conversions
Author
florian.haftmann
Browse Repository
No Builds
No Audits
656918360168 merged
Author
paulson
Browse Repository
No Builds
No Audits
9c86034d4adf the last quantifier tweaks
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
bfee570e953e mild renamings in saturation framework
Author
blanchette
Browse Repository
No Builds
No Audits
ef75bcbbe619 merged
Author
paulson
Browse Repository
No Builds
No Audits
aa61d7d2a5fc quantifier fixes
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
9f61d06c57fc simplified 'length = 0'
Author
blanchette
Browse Repository
No Builds
No Audits
f42d5b45465d adapted uses of vcg_tc_simp in Aggregation_Algebras and…
Author
Walter Guttmann <walter.guttmann@canterbury.ac.nz>
Browse Repository
No Builds
No Audits
c1979202233d tuned document
Author
blanchette
Browse Repository
No Builds
No Audits
e4e449d5b763 merged two theory files and cleaned up some locales
Author
blanchette
Browse Repository
No Builds
No Audits
5a968d3e072b fixes for Relational_Disjoint_Set_Forests (AFP 2020 -> devel)
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
a51281787c8b merge of AFP 2020, fixed some proofs, but Relational_Disjoint_Set_Forests stays…
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
821ca76f3c0d sitegen for Saturation_Framework_Extensions (and also for five other entries)
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
ac00f34583b0 new entry Saturation_Framework_Extensions
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
a41d53bc4c69 a proof of concept for generic conversions
Author
florian.haftmann
Browse Repository
No Builds
No Audits
a7b99e8a1d84 tuned
Author
florian.haftmann
Browse Repository
No Builds
No Audits
d4c56b2760cf reversing all the lex crap
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
c47e491d6c30 merged
Author
paulson
Browse Repository
No Builds
No Audits
242c8f6d0ace more lex fixes, some tricky
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
7d42634829a4 removed double underscores + tuned comments
Author
blanchette
Browse Repository
No Builds
No Audits
52090471320f bring title of document in sync with title of entry
Author
blanchette
Browse Repository
No Builds
No Audits

Changes (139)
Show All Changes

Very Large Commit

This commit is very large. Load each file individually.

Path

Size

metadata/

Extended_Finite_State_Machine_Inference

Code_Generation.thy

SelectionStrategies.thy

Subsumption.thy

Code_Target_FSet.thy

Code_Target_List.thy

Code_Target_Set.thy

Drinks_Subsumption.thy

Distinguishing_Guards.thy

Increment_Reset.thy

Least_Upper_Bound.thy

PTA_Generalisation.thy

Same_Register.thy

Store_Reuse.thy

Store_Reuse_Subsumption.thy

Weak_Subsumption.thy

Extended_Finite_State_Machines

AExp_Lexorder.thy

GExp_Lexorder.thy

Transition_Lexorder.thy

Value_Lexorder.thy

Drinks_Machine.thy

Drinks_Machine_2.thy

Drinks_Machine_LTL.thy

Goedel_HFSet_Semantic

Goedel_HFSet_Semanticless

Coding_Predicates.thy

Pf_Predicates.thy

Pseudo_Coding.thy

Goedel_Incompleteness

Abstract_Encoding.thy

Abstract_First_Goedel.thy

Abstract_First_Goedel_Rosser.thy

Abstract_Jeroslow_Encoding.thy

Abstract_Representability.thy

Abstract_Second_Goedel.thy

All_Abstract.thy

Derivability_Conditions.thy

Diagonalization.thy

Goedel_Formula.thy

Jeroslow_Original.thy

Jeroslow_Simplified.thy

Loeb_Formula.thy

Rosser_Formula.thy

Standard_Model_More.thy

Robinson_Arithmetic

Robinson_Arithmetic.thy

Syntax_Independent_Logic

Deduction_Q.thy

Natural_Deduction.thy

Pseudo_Term.thy

Standard_Model.thy

Syntax_Arith.thy

Automated_Stateful_Protocol_Verification.html

Extended_Finite_State_Machine_Inference.html

Extended_Finite_State_Machines.html

Featherweight_OCL.html

Goedel_HFSet_Semantic.html

Goedel_HFSet_Semanticless.html

Goedel_Incompleteness.html

HereditarilyFinite.html

Incompleteness.html

Robinson_Arithmetic.html

Stateful_Protocol_Composition_and_Typing.html

Syntax_Independent_Logic.html

UPF_Firewall.html

statistics.html

rAFP5172f1f451e6

metadata/metadata

thys/Extended_Finite_State_Machine_Inference/Code_Generation.thy

thys/Extended_Finite_State_Machine_Inference/EFSM_Dot.thy

thys/Extended_Finite_State_Machine_Inference/Inference.thy

thys/Extended_Finite_State_Machine_Inference/ROOT

thys/Extended_Finite_State_Machine_Inference/SelectionStrategies.thy

thys/Extended_Finite_State_Machine_Inference/Subsumption.thy

thys/Extended_Finite_State_Machine_Inference/code-targets/Code_Target_FSet.thy

thys/Extended_Finite_State_Machine_Inference/code-targets/Code_Target_List.thy

thys/Extended_Finite_State_Machine_Inference/code-targets/Code_Target_Set.thy

thys/Extended_Finite_State_Machine_Inference/document/root.bib

thys/Extended_Finite_State_Machine_Inference/document/root.tex

thys/Extended_Finite_State_Machine_Inference/efsm2sal.thy

thys/Extended_Finite_State_Machine_Inference/examples/Drinks_Subsumption.thy

thys/Extended_Finite_State_Machine_Inference/heuristics/Distinguishing_Guards.thy

thys/Extended_Finite_State_Machine_Inference/heuristics/Group_By.thy

thys/Extended_Finite_State_Machine_Inference/heuristics/Increment_Reset.thy

thys/Extended_Finite_State_Machine_Inference/heuristics/Least_Upper_Bound.thy

thys/Extended_Finite_State_Machine_Inference/heuristics/PTA_Generalisation.thy

thys/Extended_Finite_State_Machine_Inference/heuristics/Same_Register.thy

thys/Extended_Finite_State_Machine_Inference/heuristics/Store_Reuse.thy

thys/Extended_Finite_State_Machine_Inference/heuristics/Store_Reuse_Subsumption.thy

thys/Extended_Finite_State_Machine_Inference/heuristics/Weak_Subsumption.thy

thys/Extended_Finite_State_Machines/AExp.thy

thys/Extended_Finite_State_Machines/AExp_Lexorder.thy

thys/Extended_Finite_State_Machines/EFSM.thy

thys/Extended_Finite_State_Machines/EFSM_LTL.thy

thys/Extended_Finite_State_Machines/FSet_Utils.thy

thys/Extended_Finite_State_Machines/GExp.thy

thys/Extended_Finite_State_Machines/GExp_Lexorder.thy

thys/Extended_Finite_State_Machines/README.md

thys/Extended_Finite_State_Machines/ROOT

thys/Extended_Finite_State_Machines/Transition.thy

thys/Extended_Finite_State_Machines/Transition_Lexorder.thy

thys/Extended_Finite_State_Machines/Trilean.thy

thys/Extended_Finite_State_Machines/VName.thy

thys/Extended_Finite_State_Machines/Value.thy

thys/Extended_Finite_State_Machines/Value_Lexorder.thy

thys/Extended_Finite_State_Machines/document/root.bib

thys/Extended_Finite_State_Machines/document/root.tex

thys/Extended_Finite_State_Machines/examples/Drinks_Machine.thy

thys/Extended_Finite_State_Machines/examples/Drinks_Machine_2.thy

thys/Extended_Finite_State_Machines/examples/Drinks_Machine_LTL.thy

thys/Goedel_HFSet_Semantic/Instance.thy

thys/Goedel_HFSet_Semantic/ROOT

thys/Goedel_HFSet_Semantic/document/root.tex

thys/Goedel_HFSet_Semanticless/Coding.thy

thys/Goedel_HFSet_Semanticless/Coding_Predicates.thy

thys/Goedel_HFSet_Semanticless/Functions.thy

thys/Goedel_HFSet_Semanticless/Goedel_I.thy

thys/Goedel_HFSet_Semanticless/II_Prelims.thy

thys/Goedel_HFSet_Semanticless/Instance.thy

thys/Goedel_HFSet_Semanticless/Pf_Predicates.thy

thys/Goedel_HFSet_Semanticless/Predicates.thy

thys/Goedel_HFSet_Semanticless/Pseudo_Coding.thy

thys/Goedel_HFSet_Semanticless/Quote.thy

thys/Goedel_HFSet_Semanticless/ROOT

thys/Goedel_HFSet_Semanticless/Sigma.thy

thys/Goedel_HFSet_Semanticless/SyntaxN.thy

thys/Goedel_HFSet_Semanticless/document/root.tex

thys/Goedel_Incompleteness/Abstract_Encoding.thy

thys/Goedel_Incompleteness/Abstract_First_Goedel.thy

thys/Goedel_Incompleteness/Abstract_First_Goedel_Rosser.thy

thys/Goedel_Incompleteness/Abstract_Jeroslow_Encoding.thy

thys/Goedel_Incompleteness/Abstract_Representability.thy

thys/Goedel_Incompleteness/Abstract_Second_Goedel.thy

thys/Goedel_Incompleteness/All_Abstract.thy

thys/Goedel_Incompleteness/Deduction2.thy

thys/Goedel_Incompleteness/Derivability_Conditions.thy

thys/Goedel_Incompleteness/Diagonalization.thy

thys/Goedel_Incompleteness/Goedel_Formula.thy

thys/Goedel_Incompleteness/Jeroslow_Original.thy

thys/Goedel_Incompleteness/Jeroslow_Simplified.thy

thys/Goedel_Incompleteness/Loeb.thy

thys/Goedel_Incompleteness/Loeb_Formula.thy

thys/Goedel_Incompleteness/ROOT

thys/Goedel_Incompleteness/Rosser_Formula.thy

thys/Goedel_Incompleteness/Standard_Model_More.thy

thys/Goedel_Incompleteness/Tarski.thy

thys/Goedel_Incompleteness/document/root.bib

thys/Goedel_Incompleteness/document/root.tex

thys/ROOTS

thys/Robinson_Arithmetic/Instance.thy

thys/Robinson_Arithmetic/ROOT

thys/Robinson_Arithmetic/Robinson_Arithmetic.thy

thys/Robinson_Arithmetic/document/root.tex

thys/Syntax_Independent_Logic/Deduction.thy

thys/Syntax_Independent_Logic/Deduction_Q.thy

thys/Syntax_Independent_Logic/Natural_Deduction.thy

thys/Syntax_Independent_Logic/Prelim.thy

thys/Syntax_Independent_Logic/Pseudo_Term.thy

thys/Syntax_Independent_Logic/ROOT

thys/Syntax_Independent_Logic/Standard_Model.thy

thys/Syntax_Independent_Logic/Syntax.thy

thys/Syntax_Independent_Logic/Syntax_Arith.thy

thys/Syntax_Independent_Logic/document/root.bib

thys/Syntax_Independent_Logic/document/root.tex

web/entries/Automated_Stateful_Protocol_Verification.html

web/entries/Core_DOM.html

web/entries/Extended_Finite_State_Machine_Inference.html

web/entries/Extended_Finite_State_Machines.html

web/entries/Featherweight_OCL.html

web/entries/FinFun.html

web/entries/Goedel_HFSet_Semantic.html

web/entries/Goedel_HFSet_Semanticless.html

web/entries/Goedel_Incompleteness.html

web/entries/HereditarilyFinite.html

web/entries/Incompleteness.html

web/entries/Nominal2.html

web/entries/Robinson_Arithmetic.html

web/entries/Stateful_Protocol_Composition_and_Typing.html

web/entries/Syntax_Independent_Logic.html

web/entries/UPF.html

web/entries/UPF_Firewall.html

web/index.html

web/rss.xml

web/statistics.html

web/topics.html