diff --git a/metadata/entries/Safe_Range_RC.toml b/metadata/entries/Safe_Range_RC.toml
new file mode 100644
--- /dev/null
+++ b/metadata/entries/Safe_Range_RC.toml
@@ -0,0 +1,61 @@
+
+
+title = "Making Arbitrary Relational Calculus Queries Safe-Range"
+date = 2022-09-28
+topics = [
+ "Logic/General logic/Classical first-order logic",
+]
+abstract = """
+The relational calculus (RC), i.e., first-order logic with equality
+but without function symbols, is a concise, declarative database query
+language. In contrast to relational algebra or SQL, which are the
+traditional query languages of choice in the database community, RC
+queries can evaluate to an infinite relation. Moreover, even in cases
+where the evaluation result of an RC query would be finite it is not
+clear how to efficiently compute it. Safe-range RC is an interesting
+syntactic subclass of RC, because all safe-range queries evaluate to a
+finite result and it is well-known
+how to evaluate such queries by translating them to relational
+algebra. We formalize and prove correct our
+recent translation of an arbitrary RC query into a pair of
+safe-range queries. Assuming an infinite domain, the two queries have
+the following meaning: The first is closed and characterizes the
+original query's relative safety, i.e., whether given a fixed
+database (interpretation of atomic predicates with finite relations),
+the original query evaluates to a finite relation. The second
+safe-range query is equivalent to the original query, if the latter is
+relatively safe. The formalization uses the Refinement Framework to
+go from the non-deterministic algorithm described in the paper to a
+deterministic, executable query translation. Our executable query
+translation is a first step towards a verified tool that efficiently
+evaluates arbitrary RC queries. This very problem is also solved by
+the AFP entry Eval_FO
+with a theoretically incomparable but practically worse time
+complexity. (The latter is demonstrated by our
+empirical evaluation.)"""
+license = "bsd"
+note = ""
+
+[authors]
+
+[authors.raszyk]
+email = "raszyk_email"
+
+[authors.traytel]
+homepage = "traytel_homepage"
+
+[contributors]
+
+[notify]
+raszyk = "raszyk_email1"
+traytel = "traytel_email2"
+
+[history]
+
+[extra]
+
+[related]
diff --git a/thys/ROOTS b/thys/ROOTS
--- a/thys/ROOTS
+++ b/thys/ROOTS
@@ -1,706 +1,707 @@
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
Implicational_Logic
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
Padic_Field
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
Risk_Free_Lending
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
+Safe_Range_RC
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
Stalnaker_Logic
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/Safe_Range_RC/Examples.thy b/thys/Safe_Range_RC/Examples.thy
new file mode 100644
--- /dev/null
+++ b/thys/Safe_Range_RC/Examples.thy
@@ -0,0 +1,110 @@
+section \Examples\
+
+(*<*)
+theory Examples
+imports Restrict_Frees_Impl
+begin
+(*>*)
+
+global_interpretation extra_cp: simplification cp cpropagated
+ defines RB = "simplification.rb_impl_det cp"
+ and assemble = "simplification.assemble cp"
+ and SPLIT = "simplification.split_impl_det cp"
+ by standard (auto simp only: sat_cp fv_cp rrb_cp gen_Gen_cp cpropagated_cp cpropagated_cp_triv
+ cpropagated_sub Let_def is_Bool_def fv.simps cp.simps cpropagated_simps nocp.simps cpropagated_nocp split: if_splits)
+
+subsection \Restricting Bounds in the "Suspicious Users" Query\
+
+context
+ fixes b s p u :: nat and B P S
+ defines "b \ 0"
+ and "s \ Suc 0"
+ and "p \ Suc (Suc 0)"
+ and "u \ Suc (Suc (Suc 0))"
+ and "B \ \b. Pred ''B'' [Var b] :: (string, string) fmla"
+ and "P \ \b p. Pred ''P'' [Var b, Var p] :: (string, string) fmla"
+ and "S \ \p u s. Pred ''S'' [Var p, Var u, Var s] :: (string, string) fmla"
+ notes cp.simps[simp del]
+begin
+
+definition Q_susp_user where
+ "Q_susp_user = Conj (B b) (Exists s (Forall p (Impl (P b p) (S p u s))))"
+definition Q_susp_user_rb :: "(string, string) fmla" where
+ "Q_susp_user_rb = Conj (B b) (Disj (Exists s (Conj (Forall p (Impl (P b p) (S p u s))) (Exists p (S p u s)))) (Forall p (Neg (P b p))))"
+
+lemma ex_rb_Q_susp_user: "the_res (RB Q_susp_user) = Q_susp_user_rb"
+ by code_simp
+
+end
+
+subsection \Splitting a Disjunction of Predicates\
+
+context
+ fixes x y :: nat and B P
+ defines "x \ 0"
+ and "y \ 1"
+ and "B \ \b. Pred ''B'' [Var b] :: (string, string) fmla"
+ and "P \ \b p. Pred ''P'' [Var b, Var p] :: (string, string) fmla"
+ notes cp.simps[simp del]
+begin
+
+definition Q_disj where
+ "Q_disj = Disj (B x) (P x y)"
+definition Q_disj_split_fin :: "(string, string) fmla" where
+ "Q_disj_split_fin = Conj (Disj (B x) (P x y)) (P x y)"
+definition Q_disj_split_inf :: "(string, string) fmla" where
+ "Q_disj_split_inf = Exists x (B x)"
+
+lemma ex_split_Q_disj: "the_res (SPLIT Q_disj) = (Q_disj_split_fin, Q_disj_split_inf)"
+ by code_simp
+
+end
+
+subsection \Splitting a Conjunction with an Equality\
+
+context
+ fixes x u v :: nat and B
+ defines "x \ 0"
+ and "u \ 1"
+ and "v \ 2"
+ and "B \ \b. Pred ''B'' [Var b] :: (string, string) fmla"
+ notes cp.simps[simp del]
+begin
+
+definition Q_eq where
+ "Q_eq = Conj (B x) (u \ v)"
+definition Q_eq_split_fin :: "(string, string) fmla" where
+ "Q_eq_split_fin = Bool False"
+definition Q_eq_split_inf :: "(string, string) fmla" where
+ "Q_eq_split_inf = Exists x (B x)"
+
+lemma ex_split_Q_eq: "the_res (SPLIT Q_eq) = (Q_eq_split_fin, Q_eq_split_inf)"
+ by code_simp
+
+end
+
+subsection \Splitting the "Suspicious Users" Query\
+
+context
+ fixes b s p u :: nat and B P S
+ defines "b \ 0"
+ and "s \ Suc 0"
+ and "p \ Suc (Suc 0)"
+ and "u \ Suc (Suc (Suc 0))"
+ and "B \ \b. Pred ''B'' [Var b] :: (string, string) fmla"
+ and "P \ \b p. Pred ''P'' [Var b, Var p] :: (string, string) fmla"
+ and "S \ \p u s. Pred ''S'' [Var p, Var u, Var s] :: (string, string) fmla"
+ notes cp.simps[simp del]
+begin
+
+definition "Q_susp_user_split_fin = Conj Q_susp_user_rb (Exists s (Exists p (S p u s)))"
+definition "Q_susp_user_split_inf = Exists b (Conj (B b) (Forall p (Neg (P b p))))"
+
+lemma ex_split_Q_susp_user: "the_res (SPLIT Q_susp_user) = (Q_susp_user_split_fin, Q_susp_user_split_inf)"
+ by code_simp
+
+end
+
+(*<*)
+end
+(*>*)
\ No newline at end of file
diff --git a/thys/Safe_Range_RC/Preliminaries.thy b/thys/Safe_Range_RC/Preliminaries.thy
new file mode 100644
--- /dev/null
+++ b/thys/Safe_Range_RC/Preliminaries.thy
@@ -0,0 +1,460 @@
+section \Preliminaries\
+
+(*<*)
+theory Preliminaries
+imports "List-Index.List_Index"
+begin
+(*>*)
+
+subsection \Iterated Function Update\
+
+abbreviation fun_upds ("_[_ :=\<^sup>* _]" [90, 0, 0] 91) where
+ "f[xs :=\<^sup>* ys] \ fold (\(x, y) f. f(x := y)) (zip xs ys) f"
+
+fun restrict where
+ "restrict A (x # xs) (y # ys) = (if x \ A then y # restrict (A - {x}) xs ys else restrict A xs ys)"
+| "restrict A _ _ = []"
+
+fun extend :: "nat set \ nat list \ 'a list \ 'a list set" where
+ "extend A (x # xs) ys = (if x \ A
+ then (\zs \ extend (A - {x}) xs (tl ys). {hd ys # zs})
+ else (\z \ UNIV. \zs \ extend A xs ys. {z # zs}))"
+| "extend A _ _ = {[]}"
+
+fun lookup where
+ "lookup (x # xs) (y # ys) z = (if x = z then y else lookup xs ys z)"
+| "lookup _ _ _ = undefined"
+
+lemma extend_nonempty: "extend A xs ys \ {}"
+ by (induct xs arbitrary: A ys) auto
+
+lemma length_extend: "zs \ extend A xs ys \ length zs = length xs"
+ by (induct xs arbitrary: A ys zs) (auto split: if_splits)
+
+lemma ex_lookup_extend: "x \ A \ x \ set xs \ \zs \ extend A xs ys. lookup xs zs x = d"
+proof (induct xs arbitrary: A ys)
+ case (Cons a xs)
+ from Cons(1)[of "A - {a}" "tl ys"] Cons(1)[of A ys] Cons(2-) show ?case
+ by (auto simp: ex_in_conv extend_nonempty)
+qed simp
+
+lemma restrict_extend: "A \ set xs \ length ys = card A \ zs \ extend A xs ys \ restrict A xs zs = ys"
+proof (induct xs arbitrary: A ys zs)
+ case (Cons a xs)
+ then have "finite A"
+ by (elim finite_subset) auto
+ with Cons(1)[of "A - {a}" "tl ys" "tl zs"] Cons(1)[of A ys "tl zs"] Cons(2-) show ?case
+ by (cases ys) (auto simp: subset_insert_iff split: if_splits)
+qed simp
+
+lemma fun_upds_notin[simp]: "length xs = length ys \ x \ set xs \ (\[xs :=\<^sup>* ys]) x = \ x"
+ by (induct xs ys arbitrary: \ rule: list_induct2) auto
+
+lemma fun_upds_twist: "length xs = length ys \ a \ set xs \ \(a := x)[xs :=\<^sup>* ys] = (\[xs :=\<^sup>* ys])(a := x)"
+ by (induct xs ys arbitrary: \ rule: list_induct2) (auto simp: fun_upd_twist)
+
+lemma fun_upds_twist_apply: "length xs = length ys \ a \ set xs \ a \ b \ (\(a := x)[xs :=\<^sup>* ys]) b = (\[xs :=\<^sup>* ys]) b"
+ by (induct xs ys arbitrary: \ rule: list_induct2) (auto simp: fun_upd_twist)
+
+lemma fun_upds_extend:
+ "x \ A \ A \ set xs \ distinct xs \ sorted xs \ length ys = card A \ zs \ extend A xs ys \
+ (\[xs :=\<^sup>* zs]) x = (\[sorted_list_of_set A :=\<^sup>* ys]) x"
+proof (induct xs arbitrary: A ys zs \)
+ case (Cons a xs)
+ then have fin[simp]: "finite A"
+ by (elim finite_subset) auto
+ from Cons(2-) have "a \ A \ Min A = a" if "a \ A"
+ by (intro Min_eqI) auto
+ with Cons(2) fin have *: "a \ A \ sorted_list_of_set A = a # sorted_list_of_set (A - {a})"
+ by (subst sorted_list_of_set_nonempty) auto
+ show ?case
+ using Cons(1)[of "A - {a}" "tl ys"] Cons(1)[of A ys] Cons(2-)
+ by (cases ys; cases "x = a")
+ (auto simp add: subset_insert_iff * fun_upds_twist_apply length_extend simp del: fun_upd_apply split: if_splits)
+qed simp
+
+lemma fun_upds_map_self: "\[xs :=\<^sup>* map \ xs] = \"
+ by (induct xs arbitrary: \) auto
+
+lemma fun_upds_single: "distinct xs \ \[xs :=\<^sup>* map (\(y := d)) xs] = (if y \ set xs then \(y := d) else \)"
+ by (induct xs arbitrary: \) (auto simp: fun_upds_twist)
+
+subsection \Lists and Sets\
+
+lemma find_index_less_size: "\x \ set xs. P x \ find_index P xs < size xs"
+ by (induct xs) auto
+
+lemma index_less_size: "x \ set xs \ index xs x < size xs"
+ by (simp add: index_def find_index_less_size)
+
+lemma fun_upds_in: "length xs = length ys \ distinct xs \ x \ set xs \ (\[xs :=\<^sup>* ys]) x = ys ! index xs x"
+ by (induct xs ys arbitrary: \ rule: list_induct2) auto
+
+lemma remove_nth_index: "remove_nth (index ys y) ys = remove1 y ys"
+ by (induct ys) auto
+
+lemma index_remove_nth: "distinct xs \ x \ set xs \ index (remove_nth i xs) x = (if index xs x < i then index xs x else if i = index xs x then length xs - 1 else index xs x - 1)"
+ by (induct i xs rule: remove_nth.induct) (auto simp: not_less intro!: Suc_pred split: if_splits)
+
+lemma insert_nth_nth_index:
+ "y \ z \ y \ set ys \ z \ set ys \ length ys = Suc (length xs) \ distinct ys \
+ insert_nth (index ys y) x xs ! index ys z =
+ xs ! index (remove1 y ys) z"
+ by (subst nth_insert_nth;
+ auto simp: remove_nth_index[symmetric] index_remove_nth dest: index_less_size intro!: arg_cong[of _ _ "nth xs"] index_eqI)
+
+lemma index_lt_index_remove: "index xs x < index xs y \ index xs x = index (remove1 y xs) x"
+ by (induct xs) auto
+
+lemma index_gt_index_remove: "index xs x > index xs y \ index xs x = Suc (index (remove1 y xs) x)"
+proof (induct xs)
+ case (Cons z xs)
+ then show ?case
+ by (cases "z = x") auto
+qed simp
+
+lemma lookup_map[simp]: "x \ set xs \ lookup xs (map f xs) x = f x"
+ by (induct xs) auto
+
+lemma in_set_remove_cases: "P z \ (\x \ set (remove1 z xs). P x) \ x \ set xs \ P x"
+ by (cases "x = z") auto
+
+lemma insert_remove_id: "x \ X \ X = insert x (X - {x})"
+ by auto
+
+lemma infinite_surj: "infinite A \ A \ f ` B \ infinite B"
+ by (elim contrapos_nn finite_surj)
+
+class infinite =
+ fixes to_nat :: "'a \ nat"
+ assumes surj_to_nat: "surj to_nat"
+begin
+
+lemma infinite_UNIV: "infinite (UNIV :: 'a set)"
+ using surj_to_nat by (intro infinite_surj[of UNIV to_nat]) auto
+
+end
+
+instantiation nat :: infinite begin
+definition to_nat_nat :: "nat \ nat" where "to_nat_nat = id"
+instance by standard (auto simp: to_nat_nat_def)
+end
+
+instantiation list :: (type) infinite begin
+definition to_nat_list :: "'a list \ nat" where "to_nat_list = length"
+instance by standard (auto simp: image_iff to_nat_list_def intro!: exI[of _ "replicate _ _"])
+end
+
+subsection \Equivalence Closure and Classes\
+
+definition symcl where
+ "symcl r = {(x, y). (x, y) \ r \ (y, x) \ r}"
+
+definition transymcl where
+ "transymcl r = trancl (symcl r)"
+
+lemma symclp_symcl_eq[pred_set_conv]: "symclp (\x y. (x, y) \ r) = (\x y. (x, y) \ symcl r)"
+ by (auto simp: symclp_def symcl_def fun_eq_iff)
+
+definition "classes Qeq = quotient (Field Qeq) (transymcl Qeq)"
+
+lemma Field_symcl[simp]: "Field (symcl r) = Field r"
+ unfolding symcl_def Field_def by auto
+
+lemma Domain_symcl[simp]: "Domain (symcl r) = Field r"
+ unfolding symcl_def Field_def by auto
+
+lemma Field_trancl[simp]: "Field (trancl r) = Field r"
+ unfolding Field_def by auto
+
+lemma Field_transymcl[simp]: "Field (transymcl r) = Field r"
+ unfolding transymcl_def by auto
+
+lemma eqclass_empty_iff[simp]: "r `` {x} = {} \ x \ Domain r"
+ by auto
+
+lemma sym_symcl[simp]: "sym (symcl r)"
+ unfolding symcl_def sym_def by auto
+
+lemma in_symclI:
+ "(a,b) \ r \ (a,b) \ symcl r"
+ "(a,b) \ r \ (b,a) \ symcl r"
+ by (auto simp: symcl_def)
+
+lemma sym_transymcl: "sym (transymcl r)"
+ by (simp add: sym_trancl transymcl_def)
+
+lemma symcl_insert:
+ "symcl (insert (x, y) Qeq) = insert (y, x) (insert (x, y) (symcl Qeq))"
+ by (auto simp: symcl_def)
+
+lemma equiv_transymcl: "Equiv_Relations.equiv (Field Qeq) (transymcl Qeq)"
+ by (auto simp: Equiv_Relations.equiv_def sym_trancl refl_on_def transymcl_def
+ dest: FieldI1 FieldI2 Field_def[THEN equalityD1, THEN set_mp]
+ intro: r_r_into_trancl[of x _ _ x for x] elim!: in_symclI)
+
+lemma equiv_quotient_no_empty_class: "Equiv_Relations.equiv A r \ {} \ A // r"
+ by (auto simp: quotient_def refl_on_def sym_def Equiv_Relations.equiv_def)
+
+lemma classes_cover: "\(classes Qeq) = Field Qeq"
+ by (simp add: Union_quotient classes_def equiv_transymcl)
+
+lemma classes_disjoint: "X \ classes Qeq \ Y \ classes Qeq \ X = Y \ X \ Y = {}"
+ using quotient_disj[OF equiv_transymcl]
+ by (auto simp: classes_def)
+
+lemma classes_nonempty: "{} \ classes Qeq"
+ using equiv_quotient_no_empty_class[OF equiv_transymcl]
+ by (auto simp: classes_def)
+
+definition "class x Qeq = (if \X \ classes Qeq. x \ X then Some (THE X. X \ classes Qeq \ x \ X) else None)"
+
+lemma class_Some_eq: "class x Qeq = Some X \ X \ classes Qeq \ x \ X"
+ unfolding class_def
+ by (auto 0 3 dest: classes_disjoint del: conjI intro!: the_equality[of _ X]
+ conjI[of "(\X\classes Qeq. x \ X)"] intro: theI[where P="\X. X \ classes Qeq \ x \ X"])
+
+lemma class_None_eq: "class x Qeq = None \ x \ Field Qeq"
+ by (simp add: class_def classes_cover[symmetric] split: if_splits)
+
+lemma insert_Image_triv: "x \ r \ insert (x, y) Qeq `` r = Qeq `` r"
+ by auto
+
+lemma Un1_Image_triv: "Domain B \ r = {} \ (A \ B) `` r = A `` r"
+ by auto
+
+lemma Un2_Image_triv: "Domain A \ r = {} \ (A \ B) `` r = B `` r"
+ by auto
+
+lemma classes_empty: "classes {} = {}"
+ unfolding classes_def by auto
+
+lemma ex_class: "x \ Field Qeq \ \X. class x Qeq = Some X \ x \ X"
+ by (metis Union_iff class_Some_eq classes_cover)
+
+lemma equivD:
+ "Equiv_Relations.equiv A r \ refl_on A r"
+ "Equiv_Relations.equiv A r \ sym r"
+ "Equiv_Relations.equiv A r \ trans r"
+ by (blast elim: Equiv_Relations.equivE)+
+
+lemma transymcl_into:
+ "(x, y) \ r \ (x, y) \ transymcl r"
+ "(x, y) \ r \ (y, x) \ transymcl r"
+ unfolding transymcl_def by (blast intro: in_symclI r_into_trancl')+
+
+lemma transymcl_self:
+ "(x, y) \ r \ (x, x) \ transymcl r"
+ "(x, y) \ r \ (y, y) \ transymcl r"
+ unfolding transymcl_def by (blast intro: in_symclI(1) in_symclI(2) r_r_into_trancl)+
+
+lemma transymcl_trans: "(x, y) \ transymcl r \ (y, z) \ transymcl r \ (x, z) \ transymcl r"
+ using equiv_transymcl[THEN equivD(3), THEN transD] .
+
+lemma transymcl_sym: "(x, y) \ transymcl r \ (y, x) \ transymcl r"
+ using equiv_transymcl[THEN equivD(2), THEN symD] .
+
+lemma edge_same_class: "X \ classes Qeq \ (a, b) \ Qeq \ a \ X \ b \ X"
+ unfolding classes_def by (elim quotientE) (auto elim!: transymcl_trans transymcl_into)
+
+lemma Field_transymcl_self: "a \ Field Qeq \ (a, a) \