diff --git a/metadata/entries/SCC_Bloemen_Sequential.toml b/metadata/entries/SCC_Bloemen_Sequential.toml
new file mode 100644
--- /dev/null
+++ b/metadata/entries/SCC_Bloemen_Sequential.toml
@@ -0,0 +1,30 @@
+title = "Correctness of a Set-based Algorithm for Computing Strongly Connected Components of a Graph"
+date = 2022-08-17
+topics = [
+ "Computer science/Algorithms/Graph",
+]
+abstract = """
+We prove the correctness of a sequential algorithm for computing
+maximal strongly connected components (SCCs) of a graph due to Vincent
+Bloemen."""
+license = "bsd"
+note = ""
+
+[authors]
+
+[authors.merz]
+email = "merz_email"
+
+[authors.trelat]
+email = "trelat_email"
+
+[contributors]
+
+[notify]
+trelat = "trelat_email"
+
+[history]
+
+[extra]
+
+[related]
diff --git a/metadata/entries/Separation_Logic_Unbounded.toml b/metadata/entries/Separation_Logic_Unbounded.toml
new file mode 100644
--- /dev/null
+++ b/metadata/entries/Separation_Logic_Unbounded.toml
@@ -0,0 +1,54 @@
+title = "Unbounded Separation Logic"
+date = 2022-09-05
+topics = [
+ "Computer science/Programming languages/Logics",
+]
+abstract = """
+Many separation logics support fractional permissions to distinguish
+between read and write access to a heap location, for instance, to
+allow concurrent reads while enforcing exclusive writes. Fractional
+permissions extend to composite assertions such as (co)inductive
+predicates and magic wands by allowing those to be multiplied by a
+fraction. Typical separation logic proofs require that this
+multiplication has three key properties: it needs to distribute over
+assertions, it should permit fractions to be factored out from
+assertions, and two fractions of the same assertion should be
+combinable into one larger fraction. Existing formal semantics
+incorporating fractional assertions into a separation logic define
+multiplication semantically (via models), resulting in a semantics in
+which distributivity and combinability do not hold for key resource
+assertions such as magic wands, and fractions cannot be factored out
+from a separating conjunction. By contrast, existing automatic
+separation logic verifiers define multiplication syntactically,
+resulting in a different semantics for which it is unknown whether
+distributivity and combinability hold for all assertions. In this
+entry (which accompanies an OOPSLA'22
+paper), we present and formalize an unbounded version of
+separation logic, a novel semantics for separation logic assertions
+that allows states to hold more than a full permission to a heap
+location during the evaluation of an assertion. By reimposing upper
+bounds on the permissions held per location at statement boundaries,
+we retain key properties of separation logic, in particular, we prove
+that the frame rule still holds. We also prove that our assertion
+semantics unifies semantic and syntactic multiplication and thereby
+reconciles the discrepancy between separation logic theory and tools
+and enjoys distributivity, factorisability, and combinability."""
+license = "bsd"
+note = ""
+
+[authors]
+
+[authors.dardinier]
+homepage = "dardinier_homepage"
+
+[contributors]
+
+[notify]
+dardinier = "dardinier_email"
+
+[history]
+
+[extra]
+
+[related]
diff --git a/thys/ROOTS b/thys/ROOTS
--- a/thys/ROOTS
+++ b/thys/ROOTS
@@ -1,701 +1,702 @@
ADS_Functor
AI_Planning_Languages_Semantics
AODV
AVL-Trees
AWN
Abortable_Linearizable_Modules
Abs_Int_ITP2012
Abstract-Hoare-Logics
Abstract-Rewriting
Abstract_Completeness
Abstract_Soundness
Ackermanns_not_PR
Actuarial_Mathematics
Adaptive_State_Counting
Affine_Arithmetic
Aggregation_Algebras
Akra_Bazzi
Algebraic_Numbers
Algebraic_VCs
Allen_Calculus
Amicable_Numbers
Amortized_Complexity
AnselmGod
Applicative_Lifting
Approximation_Algorithms
Architectural_Design_Patterns
Aristotles_Assertoric_Syllogistic
Arith_Prog_Rel_Primes
ArrowImpossibilityGS
Attack_Trees
Auto2_HOL
Auto2_Imperative_HOL
AutoFocus-Stream
Automated_Stateful_Protocol_Verification
Automatic_Refinement
AxiomaticCategoryTheory
BDD
BD_Security_Compositional
BNF_CC
BNF_Operations
BTree
Banach_Steinhaus
Belief_Revision
Bell_Numbers_Spivey
BenOr_Kozen_Reif
Berlekamp_Zassenhaus
Bernoulli
Bertrands_Postulate
Bicategory
BinarySearchTree
Binding_Syntax_Theory
Binomial-Heaps
Binomial-Queues
BirdKMP
Blue_Eyes
Bondy
Boolean_Expression_Checkers
Boolos_Curious_Inference
Bounded_Deducibility_Security
Buchi_Complementation
Budan_Fourier
Buffons_Needle
Buildings
BytecodeLogicJmlTypes
C2KA_DistributedSystems
CAVA_Automata
CAVA_LTL_Modelchecker
CCS
CISC-Kernel
CRYSTALS-Kyber
CRDT
CSP_RefTK
CYK
CZH_Elementary_Categories
CZH_Foundations
CZH_Universal_Constructions
CakeML
CakeML_Codegen
Call_Arity
Card_Equiv_Relations
Card_Multisets
Card_Number_Partitions
Card_Partitions
Cartan_FP
Case_Labeling
Catalan_Numbers
Category
Category2
Category3
Cauchy
Cayley_Hamilton
Certification_Monads
Chandy_Lamport
Chord_Segments
Circus
Clean
Clique_and_Monotone_Circuits
ClockSynchInst
Closest_Pair_Points
CoCon
CoSMeDis
CoSMed
CofGroups
Coinductive
Coinductive_Languages
Collections
Combinable_Wands
Combinatorics_Words
Combinatorics_Words_Graph_Lemma
Combinatorics_Words_Lyndon
Commuting_Hermitian
Comparison_Sort_Lower_Bound
Compiling-Exceptions-Correctly
Complete_Non_Orders
Completeness
Complex_Bounded_Operators
Complex_Geometry
Complx
ComponentDependencies
ConcurrentGC
ConcurrentIMP
Concurrent_Ref_Alg
Concurrent_Revisions
Conditional_Simplification
Conditional_Transfer_Rule
Consensus_Refined
Constructive_Cryptography
Constructive_Cryptography_CM
Constructor_Funs
Containers
CoreC++
Core_DOM
Core_SC_DOM
Correctness_Algebras
Cotangent_PFD_Formula
Count_Complex_Roots
CryptHOL
CryptoBasedCompositionalProperties
Cubic_Quartic_Equations
DFS_Framework
DOM_Components
DPT-SAT-Solver
DataRefinementIBP
Datatype_Order_Generator
Decl_Sem_Fun_PL
Decreasing-Diagrams
Decreasing-Diagrams-II
Dedekind_Real
Deep_Learning
Delta_System_Lemma
Density_Compiler
Dependent_SIFUM_Refinement
Dependent_SIFUM_Type_Systems
Depth-First-Search
Derangements
Deriving
Descartes_Sign_Rule
Design_Theory
Dict_Construction
Differential_Dynamic_Logic
Differential_Game_Logic
Digit_Expansions
Dijkstra_Shortest_Path
Diophantine_Eqns_Lin_Hom
Dirichlet_L
Dirichlet_Series
DiscretePricing
Discrete_Summation
DiskPaxos
Dominance_CHK
DPRM_Theorem
DynamicArchitectures
Dynamic_Tables
E_Transcendental
Echelon_Form
EdmondsKarp_Maxflow
Efficient-Mergesort
Elliptic_Curves_Group_Law
Encodability_Process_Calculi
Epistemic_Logic
Equivalence_Relation_Enumeration
Ergodic_Theory
Error_Function
Euler_MacLaurin
Euler_Partition
Eval_FO
Example-Submission
Extended_Finite_State_Machine_Inference
Extended_Finite_State_Machines
FFT
FLP
FOL-Fitting
FOL_Axiomatic
FOL_Harrison
FOL_Seq_Calc1
FOL_Seq_Calc2
FOL_Seq_Calc3
FSM_Tests
Factor_Algebraic_Polynomial
Factored_Transition_System_Bounding
Falling_Factorial_Sum
Farkas
FeatherweightJava
Featherweight_OCL
Fermat3_4
FileRefinement
FinFun
Finger-Trees
Finite-Map-Extras
Finite_Automata_HF
Finite_Fields
Finitely_Generated_Abelian_Groups
First_Order_Terms
First_Welfare_Theorem
Fishburn_Impossibility
Fisher_Yates
Fishers_Inequality
Flow_Networks
Floyd_Warshall
Flyspeck-Tame
FocusStreamsCaseStudies
Forcing
Formal_Puiseux_Series
Formal_SSA
Formula_Derivatives
Foundation_of_geometry
Fourier
FO_Theory_Rewriting
Free-Boolean-Algebra
Free-Groups
Frequency_Moments
Fresh_Identifiers
FunWithFunctions
FunWithTilings
Functional-Automata
Functional_Ordered_Resolution_Prover
Furstenberg_Topology
GPU_Kernel_PL
Gabow_SCC
GaleStewart_Games
Gale_Shapley
Game_Based_Crypto
Gauss-Jordan-Elim-Fun
Gauss_Jordan
Gauss_Sums
Gaussian_Integers
GenClock
General-Triangle
Generalized_Counting_Sort
Generic_Deriving
Generic_Join
GewirthPGCProof
Girth_Chromatic
GoedelGod
Goedel_HFSet_Semantic
Goedel_HFSet_Semanticless
Goedel_Incompleteness
Goodstein_Lambda
GraphMarkingIBP
Graph_Saturation
Graph_Theory
Green
Groebner_Bases
Groebner_Macaulay
Gromov_Hyperbolicity
Grothendieck_Schemes
Group-Ring-Module
HOL-CSP
HOLCF-Prelude
HRB-Slicing
Hahn_Jordan_Decomposition
Hales_Jewett
Heard_Of
Hello_World
HereditarilyFinite
Hermite
Hermite_Lindemann
Hidden_Markov_Models
Higher_Order_Terms
Hoare_Time
Hood_Melville_Queue
HotelKeyCards
Huffman
Hybrid_Logic
Hybrid_Multi_Lane_Spatial_Logic
Hybrid_Systems_VCs
HyperCTL
Hyperdual
IEEE_Floating_Point
IFC_Tracking
IMAP-CRDT
IMO2019
IMP2
IMP2_Binary_Heap
IMP_Compiler
IMP_Compiler_Reuse
IP_Addresses
Imperative_Insertion_Sort
Impossible_Geometry
Incompleteness
Incredible_Proof_Machine
Independence_CH
Inductive_Confidentiality
Inductive_Inference
InfPathElimination
InformationFlowSlicing
InformationFlowSlicing_Inter
Integration
Interpolation_Polynomials_HOL_Algebra
Interpreter_Optimizations
Interval_Arithmetic_Word32
Intro_Dest_Elim
Involutions2Squares
Iptables_Semantics
Irrational_Series_Erdos_Straus
Irrationality_J_Hancl
Irrationals_From_THEBOOK
IsaGeoCoq
Isabelle_C
Isabelle_Marries_Dirac
Isabelle_Meta_Model
IsaNet
Jacobson_Basic_Algebra
Jinja
JinjaDCI
JinjaThreads
JiveDataStoreModel
Jordan_Hoelder
Jordan_Normal_Form
KAD
KAT_and_DRA
KBPs
KD_Tree
Key_Agreement_Strong_Adversaries
Khovanskii_Theorem
Kleene_Algebra
Knights_Tour
Knot_Theory
Knuth_Bendix_Order
Knuth_Morris_Pratt
Koenigsberg_Friendship
Kruskal
Kuratowski_Closure_Complement
LLL_Basis_Reduction
LLL_Factorization
LOFT
LTL
LTL_Master_Theorem
LTL_Normal_Form
LTL_to_DRA
LTL_to_GBA
Lam-ml-Normalization
LambdaAuth
LambdaMu
Lambda_Free_EPO
Lambda_Free_KBOs
Lambda_Free_RPOs
Lambert_W
Landau_Symbols
Laplace_Transform
Latin_Square
LatticeProperties
Launchbury
Laws_of_Large_Numbers
Lazy-Lists-II
Lazy_Case
Lehmer
Lifting_Definition_Option
Lifting_the_Exponent
LightweightJava
LinearQuantifierElim
Linear_Inequalities
Linear_Programming
Linear_Recurrences
Liouville_Numbers
List-Index
List-Infinite
List_Interleaving
List_Inversions
List_Update
LocalLexing
Localization_Ring
Locally-Nameless-Sigma
Logging_Independent_Anonymity
Lowe_Ontological_Argument
Lower_Semicontinuous
Lp
LP_Duality
Lucas_Theorem
MDP-Algorithms
MDP-Rewards
MFMC_Countable
MFODL_Monitor_Optimized
MFOTL_Monitor
MSO_Regex_Equivalence
Markov_Models
Marriage
Mason_Stothers
Matrices_for_ODEs
Matrix
Matrix_Tensor
Matroids
Max-Card-Matching
Median_Method
Median_Of_Medians_Selection
Menger
Mereology
Mersenne_Primes
Metalogic_ProofChecker
MiniML
MiniSail
Minimal_SSA
Minkowskis_Theorem
Minsky_Machines
Modal_Logics_for_NTS
Modular_Assembly_Kit_Security
Modular_arithmetic_LLL_and_HNF_algorithms
Monad_Memo_DP
Monad_Normalisation
MonoBoolTranAlgebra
MonoidalCategory
Monomorphic_Monad
MuchAdoAboutTwo
Multiset_Ordering_NPC
Multi_Party_Computation
Multirelations
Myhill-Nerode
Name_Carrying_Type_Inference
Nano_JSON
Nash_Williams
Nat-Interval-Logic
Native_Word
Nested_Multisets_Ordinals
Network_Security_Policy_Verification
Neumann_Morgenstern_Utility
No_FTL_observers
Nominal2
Noninterference_CSP
Noninterference_Concurrent_Composition
Noninterference_Generic_Unwinding
Noninterference_Inductive_Unwinding
Noninterference_Ipurge_Unwinding
Noninterference_Sequential_Composition
NormByEval
Nullstellensatz
Number_Theoretic_Transform
Octonions
OpSets
Open_Induction
Optics
Optimal_BST
Orbit_Stabiliser
Order_Lattice_Props
Ordered_Resolution_Prover
Ordinal
Ordinal_Partitions
Ordinals_and_Cardinals
Ordinary_Differential_Equations
PAC_Checker
Package_logic
PAL
PCF
PLM
POPLmark-deBruijn
PSemigroupsConvolution
Padic_Ints
Pairing_Heap
Paraconsistency
Parity_Game
Partial_Function_MR
Partial_Order_Reduction
Password_Authentication_Protocol
Pell
Perfect-Number-Thm
Perron_Frobenius
Physical_Quantities
Pi_Calculus
Pi_Transcendental
Planarity_Certificates
Pluennecke_Ruzsa_Inequality
Poincare_Bendixson
Poincare_Disc
Polynomial_Factorization
Polynomial_Interpolation
Polynomials
Pop_Refinement
Posix-Lexing
Possibilistic_Noninterference
Power_Sum_Polynomials
Pratt_Certificate
Prefix_Free_Code_Combinators
Presburger-Automata
Prim_Dijkstra_Simple
Prime_Distribution_Elementary
Prime_Harmonic_Series
Prime_Number_Theorem
Priority_Queue_Braun
Priority_Search_Trees
Probabilistic_Noninterference
Probabilistic_Prime_Tests
Probabilistic_System_Zoo
Probabilistic_Timed_Automata
Probabilistic_While
Program-Conflict-Analysis
Progress_Tracking
Projective_Geometry
Projective_Measurements
Promela
Proof_Strategy_Language
PropResPI
Propositional_Proof_Systems
Prpu_Maxflow
PseudoHoops
Psi_Calculi
Ptolemys_Theorem
Public_Announcement_Logic
QHLProver
QR_Decomposition
Quantales
Quasi_Borel_Spaces
Quaternions
Quick_Sort_Cost
RIPEMD-160-SPARK
ROBDD
RSAPSS
Ramsey-Infinite
Random_BSTs
Random_Graph_Subgraph_Threshold
Randomised_BSTs
Randomised_Social_Choice
Rank_Nullity_Theorem
Real_Impl
Real_Power
Real_Time_Deque
Recursion-Addition
Recursion-Theory-I
Refine_Imperative_HOL
Refine_Monadic
RefinementReactive
Regex_Equivalence
Registers
Regression_Test_Selection
Regular-Sets
Regular_Algebras
Regular_Tree_Relations
Relation_Algebra
Relational-Incorrectness-Logic
Relational_Disjoint_Set_Forests
Relational_Forests
Relational_Method
Relational_Minimum_Spanning_Trees
Relational_Paths
Rep_Fin_Groups
ResiduatedTransitionSystem
Residuated_Lattices
Resolution_FOL
Rewrite_Properties_Reduction
Rewriting_Z
Ribbon_Proofs
Robbins-Conjecture
Robinson_Arithmetic
Root_Balanced_Tree
Roth_Arithmetic_Progressions
Routing
Roy_Floyd_Warshall
SATSolverVerification
SC_DOM_Components
SDS_Impossibility
SIFPL
SIFUM_Type_Systems
SPARCv8
Safe_Distance
Safe_OCL
Saturation_Framework
Saturation_Framework_Extensions
SCC_Bloemen_Sequential
Schutz_Spacetime
Secondary_Sylow
Security_Protocol_Refinement
Selection_Heap_Sort
SenSocialChoice
Separata
Separation_Algebra
Separation_Logic_Imperative_HOL
+Separation_Logic_Unbounded
SequentInvertibility
Shadow_DOM
Shadow_SC_DOM
Shivers-CFA
ShortestPath
Show
Sigma_Commit_Crypto
Signature_Groebner
Simpl
Simple_Firewall
Simplex
Simplicial_complexes_and_boolean_functions
SimplifiedOntologicalArgument
Skew_Heap
Skip_Lists
Slicing
Sliding_Window_Algorithm
Smith_Normal_Form
Smooth_Manifolds
Sophomores_Dream
Solidity
Sort_Encodings
Source_Coding_Theorem
SpecCheck
Special_Function_Bounds
Splay_Tree
Sqrt_Babylonian
Stable_Matching
Statecharts
Stateful_Protocol_Composition_and_Typing
Stellar_Quorums
Stern_Brocot
Stewart_Apollonius
Stirling_Formula
Stochastic_Matrices
Stone_Algebras
Stone_Kleene_Relation_Algebras
Stone_Relation_Algebras
Store_Buffer_Reduction
Stream-Fusion
Stream_Fusion_Code
Strong_Security
Sturm_Sequences
Sturm_Tarski
Stuttering_Equivalence
Subresultants
Subset_Boolean_Algebras
SumSquares
Sunflowers
SuperCalc
Surprise_Paradox
Symmetric_Polynomials
Syntax_Independent_Logic
Szemeredi_Regularity
Szpilrajn
TESL_Language
TLA
Tail_Recursive_Functions
Tarskis_Geometry
Taylor_Models
Three_Circles
Timed_Automata
Topological_Semantics
Topology
TortoiseHare
Transcendence_Series_Hancl_Rucki
Transformer_Semantics
Transition_Systems_and_Automata
Transitive-Closure
Transitive-Closure-II
Transitive_Models
Treaps
Tree-Automata
Tree_Decomposition
Triangle
Trie
Twelvefold_Way
Tycon
Types_Tableaus_and_Goedels_God
Types_To_Sets_Extension
UPF
UPF_Firewall
UTP
Universal_Hash_Families
Universal_Turing_Machine
UpDown_Scheme
Valuation
Van_Emde_Boas_Trees
Van_der_Waerden
VectorSpace
VeriComp
Verified-Prover
Verified_SAT_Based_AI_Planning
VerifyThis2018
VerifyThis2019
Vickrey_Clarke_Groves
Virtual_Substitution
VolpanoSmith
VYDRA_MDL
WHATandWHERE_Security
WOOT_Strong_Eventual_Consistency
WebAssembly
Weight_Balanced_Trees
Weighted_Arithmetic_Geometric_Mean
Weighted_Path_Order
Well_Quasi_Orders
Wetzels_Problem
Winding_Number_Eval
Word_Lib
WorkerWrapper
X86_Semantics
XML
Youngs_Inequality
ZFC_in_HOL
Zeta_3_Irrational
Zeta_Function
pGCL
diff --git a/thys/Separation_Logic_Unbounded/.#ROOT b/thys/Separation_Logic_Unbounded/.#ROOT
new file mode 120000
--- /dev/null
+++ b/thys/Separation_Logic_Unbounded/.#ROOT
@@ -0,0 +1,1 @@
+nipkow@lapnipkow1.local.3458
\ No newline at end of file
diff --git a/thys/Separation_Logic_Unbounded/AutomaticVerifiers.thy b/thys/Separation_Logic_Unbounded/AutomaticVerifiers.thy
new file mode 100644
--- /dev/null
+++ b/thys/Separation_Logic_Unbounded/AutomaticVerifiers.thy
@@ -0,0 +1,427 @@
+section \Fractional Predicates and Magic Wands in Automatic Separation Logic Verifiers\
+
+text \This section corresponds to Section 5 of the paper~\cite{UnboundedSL}.\
+
+theory AutomaticVerifiers
+ imports FixedPoint WandProperties
+begin
+
+context logic
+begin
+
+subsection \Syntactic multiplication\
+
+text \The following definition corresponds to Figure 6 of the paper~\cite{UnboundedSL}.\
+
+fun syn_mult :: "'b \ ('a, 'b, 'c, 'd) assertion \ ('a, 'b, 'c, 'd) assertion" where
+ "syn_mult \ (Star A B) = Star (syn_mult \ A) (syn_mult \ B)"
+| "syn_mult \ (Wand A B) = Wand (syn_mult \ A) (syn_mult \ B)"
+| "syn_mult \ (Or A B) = Or (syn_mult \ A) (syn_mult \ B)"
+| "syn_mult \ (And A B) = And (syn_mult \ A) (syn_mult \ B)"
+| "syn_mult \ (Imp A B) = Imp (syn_mult \ A) (syn_mult \ B)"
+| "syn_mult \ (Mult \ A) = syn_mult (smult \ \) A"
+| "syn_mult \ (Exists x A) = Exists x (syn_mult \ A)"
+| "syn_mult \ (Forall x A) = Forall x (syn_mult \ A)"
+| "syn_mult \ (Wildcard A) = Wildcard A"
+| "syn_mult \ A = Mult \ A"
+
+definition div_state where
+ "div_state \ \ = (SOME r. \ = \ \ r)"
+
+lemma div_state_ok:
+ "\ = \ \ (div_state \ \)"
+ by (metis (mono_tags) div_state_def someI_ex unique_inv)
+
+text \The following theorem corresponds to Theorem 6 of the paper~\cite{UnboundedSL}.\
+
+theorem syn_sen_mult_same:
+ "\, s, \ \ syn_mult \ A \ \, s, \ \ Mult \ A"
+proof (induct A arbitrary: \ \ s)
+ case (Exists x A)
+ show ?case (is "?A \ ?B")
+ proof
+ show "?B \ ?A"
+ using Exists.hyps by auto
+ show "?A \ ?B"
+ using Exists.hyps by fastforce
+ qed
+next
+ case (Forall x A)
+ then show ?case
+ by (metis dot_forall1 dot_forall2 entails_def sat.simps(9) syn_mult.simps(8))
+next
+ case (Star A B)
+ show ?case (is "?P \ ?Q")
+ proof
+ show "?P \ ?Q"
+ proof -
+ assume ?P
+ then obtain a b where "a, s, \ \ syn_mult \ A" "b, s, \ \ syn_mult \ B"
+ "Some \ = a \ b" by auto
+ then obtain "a, s, \ \ Mult \ A" "b, s, \ \ Mult \ B"
+ using Star.hyps(1) Star.hyps(2) Star.prems by blast
+ then show ?Q
+ by (meson \Some \ = a \ b\ dot_star2 entails_def sat.simps(2))
+ qed
+ assume ?Q
+ then obtain a b where "a, s, \ \ Mult \ A" "b, s, \ \ Mult \ B" "Some \ = a \ b"
+ by (meson dot_star1 entails_def sat.simps(2))
+ then show ?P
+ using Star.hyps(1) Star.hyps(2) Star.prems by force
+ qed
+next
+ case (Mult p A)
+ show ?case (is "?P \ ?Q")
+ proof
+ show "?P \ ?Q"
+ proof -
+ assume ?P
+ then have "\, s, \ \ syn_mult (smult p \) A" by auto
+ then have "\, s, \ \ Mult (smult p \) A"
+ using Mult.hyps by blast
+ then show ?Q
+ by (metis dot_mult2 logic.entails_def logic_axioms smult_comm)
+ qed
+ assume ?Q
+ then obtain a where "a, s, \ \ A" "\ = \ \ (p \ a)" by auto
+ then show ?P
+ using Mult.hyps double_mult smult_comm by auto
+ qed
+next
+ case (Wand A B)
+ show ?case (is "?P \ ?Q")
+ proof
+ show "?P \ ?Q"
+ proof -
+ assume "\, s, \ \ syn_mult \ (Wand A B)"
+ then have "\, s, \ \ Wand (syn_mult \ A) (syn_mult \ B)"
+ by auto
+ moreover have "div_state \ \, s, \ \ Wand A B"
+ proof (rule sat_wand)
+ fix a b
+ assume "a, s, \ \ A \ Some b = div_state \ \ \ a"
+ then have "Some (\ \ b) = \ \ (\ \ a)"
+ using div_state_ok plus_mult by presburger
+ moreover have "\ \ a, s, \ \ Mult \ A"
+ using \a, s, \ \ A \ Some b = div_state \ \ \ a\ by auto
+ then have "\ \ a, s, \ \ syn_mult \ A"
+ using Wand.hyps(1) Wand.prems by blast
+ then have "\ \ b, s, \ \ syn_mult \ B"
+ using \\, s, \ \ Wand (syn_mult \ A) (syn_mult \ B)\ calculation by auto
+ ultimately show "b, s, \ \ B"
+ by (metis Wand.hyps(2) Wand.prems can_divide sat.simps(1))
+ qed
+ then show "\, s, \ \ Mult \ (Wand A B)"
+ by (metis div_state_ok sat.simps(1))
+ qed
+ assume "\, s, \ \ Mult \ (Wand A B)"
+ then have "div_state \ \, s, \ \ Wand A B"
+ by (metis div_state_ok can_divide sat.simps(1))
+ have "\, s, \ \ Wand (syn_mult \ A) (syn_mult \ B)"
+ proof (rule sat_wand)
+ fix a b assume "a, s, \ \ syn_mult \ A \ Some b = \ \ a"
+ then have "Some (div_state \ b) = div_state \ \ \ div_state \ a"
+ by (metis div_state_ok plus_mult unique_inv)
+ then have "div_state \ b, s, \ \ B"
+ by (metis (no_types, lifting) Wand.hyps(1) \a, s, \ \ syn_mult \ A \ Some b = \ \ a\ \div_state \ \, s, \ \ Wand A B\ div_state_ok logic.can_divide logic_axioms sat.simps(1) sat.simps(3))
+ then show "b, s, \ \ syn_mult \ B"
+ using Wand.hyps(2) div_state_ok sat.simps(1) by blast
+ qed
+ then show "\, s, \ \ syn_mult \ (Wand A B)"
+ by simp
+ qed
+next
+ case (And A B)
+ show ?case (is "?P \ ?Q")
+ proof
+ show "?P \ ?Q"
+ proof -
+ assume ?P
+ then obtain "\, s, \ \ syn_mult \ A" "\, s, \ \ syn_mult \ B"
+ by auto
+ then show ?Q
+ by (meson And.hyps(1) And.hyps(2) dot_and2 logic.entails_def logic_axioms sat.simps(7))
+ qed
+ assume ?Q then show ?P
+ using And.hyps(1) And.hyps(2) And.prems by auto
+ qed
+next
+ case (Imp A B)
+ show ?case (is "?P \ ?Q")
+ proof
+ show "?P \ ?Q"
+ by (metis Imp.hyps(1) Imp.hyps(2) sat.simps(1) sat.simps(5) syn_mult.simps(5) unique_inv)
+ assume ?Q then show ?P
+ by (metis Imp.hyps(1) Imp.hyps(2) Imp.prems can_divide sat.simps(1) sat.simps(5) syn_mult.simps(5))
+ qed
+next
+ case (Wildcard A)
+ then show ?case
+ by (metis DotWild entails_def equivalent_def syn_mult.simps(9))
+qed (auto)
+
+
+
+subsection \Monotonicity and fixed point\
+
+(* Bool means positive *)
+fun pos_neg_rec_call :: "bool \ ('a, 'b, 'c, 'd) assertion \ bool" where
+ "pos_neg_rec_call b Pred \ b"
+| "pos_neg_rec_call b (Mult _ A) \ pos_neg_rec_call b A"
+| "pos_neg_rec_call b (Exists _ A) \ pos_neg_rec_call b A"
+| "pos_neg_rec_call b (Forall _ A) \ pos_neg_rec_call b A"
+| "pos_neg_rec_call b (Star A B) \ pos_neg_rec_call b A \ pos_neg_rec_call b B"
+| "pos_neg_rec_call b (Or A B) \ pos_neg_rec_call b A \ pos_neg_rec_call b B"
+| "pos_neg_rec_call b (And A B) \ pos_neg_rec_call b A \ pos_neg_rec_call b B"
+| "pos_neg_rec_call b (Wand A B) \ pos_neg_rec_call (\ b) A \ pos_neg_rec_call b B"
+| "pos_neg_rec_call b (Imp A B) \ pos_neg_rec_call (\ b) A \ pos_neg_rec_call b B"
+| "pos_neg_rec_call _ (Sem _) \ True"
+| "pos_neg_rec_call b (Bounded A) \ pos_neg_rec_call b A"
+| "pos_neg_rec_call b (Wildcard A) \ pos_neg_rec_call b A"
+
+
+lemma pos_neg_rec_call_mono:
+ assumes "pos_neg_rec_call b A"
+ shows "(b \ monotonic (applies_eq A)) \ (\