Theory PMLinHOL_preliminaries

section‹Preliminaries›
text‹The following preliminaries are are shared between all embeddings introduced in 
the remainder of this paper.›

theory PMLinHOL_preliminaries 
  imports Main 
begin  

―‹Type declarations common for both the deep and shallow embedding›
typedecl 𝗐 ―‹Type for possible worlds› 
typedecl 𝒮 ―‹Type for propositional constant symbols› 
consts p::𝒮 q::𝒮  ―‹Some propositional constant symbols› 
type_synonym 𝒲 = "𝗐⇒bool" ―‹Type for sets of possible worlds› 
type_synonym ℛ = "𝗐⇒𝗐⇒bool" ―‹Type for accessibility relations› 
type_synonym 𝒱 = "𝒮⇒𝗐⇒bool" ―‹Type for valuation functions› 

―‹Some useful predicates for accessibility relations›
abbreviation(input) "reflexive ≡ λR::ℛ. ∀x. R x x"
abbreviation(input) "symmetric ≡ λR::ℛ. ∀x y. R x y ⟶ R y x"
abbreviation(input) "transitive ≡ λR::ℛ. ∀x y z. (R x y ∧ R y z) ⟶ R x z"
abbreviation(input) "equivrel ≡ λR::ℛ. reflexive R ∧ symmetric R ∧ transitive R"
abbreviation(input) "irreflexive ≡ λR::ℛ. ∀x. ¬R x x" 
abbreviation(input) "euclidean ≡ λR::ℛ. ∀x y z. R x y ∧ R x z ⟶ R y z"
abbreviation(input) "wellfounded ≡ λR::ℛ. ∀P::𝒲. (∀x. (∀y. R y x ⟶ P y) ⟶ P x) ⟶ (∀x. P x)" 
abbreviation(input) "converserel ≡ λR::ℛ. λy::𝗐. λx::𝗐. R x y" 
abbreviation(input) "conversewf ≡ λR::ℛ. wellfounded (converserel R)" 

―‹Bounded universal quantifier: ‹∀x:W. φ› stands for ‹∀x. W x ⟶ φ x››
abbreviation(input) BoundedAll::"𝒲⇒𝒲⇒bool" where "BoundedAll W φ ≡ ∀x. W x ⟶ φ x" 
syntax "_BoundedAll":: "pttrn⇒𝒲⇒bool⇒bool" ("(3∀(_/:_)./ _)" [0, 0, 10] 10)
translations "∀x:W. φ" ⇌ "CONST BoundedAll W (λx. φ)"

―‹Backward implication; useful for aestethic reasons›
abbreviation(input) Bimp (infixr "⟵" 50) where "φ ⟵ ψ ≡ ψ ⟶ φ"

―‹Some further settings› 
declare[[syntax_ambiguity_warning=false]] 
nitpick_params[user_axioms,expect=genuine,timeout=60]  

end