diff options
Diffstat (limited to 'SymbolicModalLogic/MuCalculus.lean')
| -rw-r--r-- | SymbolicModalLogic/MuCalculus.lean | 39 |
1 files changed, 18 insertions, 21 deletions
diff --git a/SymbolicModalLogic/MuCalculus.lean b/SymbolicModalLogic/MuCalculus.lean index cad6a75..73d04f4 100644 --- a/SymbolicModalLogic/MuCalculus.lean +++ b/SymbolicModalLogic/MuCalculus.lean @@ -74,14 +74,19 @@ end Formula section Semantics -class Model (Λ : Type) [Modalities Λ] (F : Type → Type) [Functor F] [LawfulFunctor F] where +class Model (Λ : Type) [Modalities Λ] (F : Type → Type) [Functor F] where lifting {X : Type} (l : Λ) : (args : Modalities.signature l → Set X) → Set (F X) + +abbrev Model.lift {Λ : Type} [Modalities Λ] (l : Λ) (F : Type → Type) [Functor F] [Model Λ F] {X : Type} : (args : Modalities.signature l → Set X) → Set (F X) := + Model.lifting l + +class LawfulModel (Λ : Type) [Modalities Λ] (F : Type → Type) [Functor F] [LawfulFunctor F] [Model Λ F] where lifting_natural {X Y : Type} (f : X → Y) (l : Λ) (args : Modalities.signature l → Set Y) : - (lifting l fun a ↦ f ⁻¹' (args a)) = ((Functor.map f) ⁻¹' (lifting l args)) + (Model.lift l F fun a ↦ f ⁻¹' (args a)) = ((Functor.map f) ⁻¹' (Model.lift l F args)) lifting_monotone {X : Type} (l : Λ) (args args' : Modalities.signature l → Set X) : - (∀ a, args a ⊆ args' a) → lifting l args ⊆ lifting l args' + (∀ a, args a ⊆ args' a) → Model.lift l F args ⊆ Model.lift l F args' lifting_dual {X : Type} (l : Λ) (args : Modalities.signature l → Set X) : - lifting (Modalities.dual l) (Modalities.dualSignature l args) = Set.compl (lifting l fun a ↦ Set.compl (args a)) + Model.lift (Modalities.dual l) F (Modalities.dualSignature l args) = (Model.lift l F fun a ↦ (args a)ᶜ)ᶜ variable {Λ : Type} [Modalities Λ] variable {F : Type → Type} [Functor F] [LawfulFunctor F] [Model Λ F] @@ -145,12 +150,12 @@ def interp {X : Type} (γ : X → F X) : Formula Λ → Environment X → Set X | .bot, _ => ∅ | .or φ ψ, xs => (interp γ φ xs) ∪ (interp γ ψ xs) | .and φ ψ, xs => (interp γ φ xs) ∩ (interp γ ψ xs) - | .modality l args, xs => γ ⁻¹' Model.lifting l fun a ↦ interp γ (args a) xs + | .modality l args, xs => γ ⁻¹' Model.lift l F fun a ↦ interp γ (args a) xs | .var x, xs => xs x | .lfp φ, xs => FixedPoints.lfp fun S ↦ interp γ φ (S :: xs) | .gfp φ, xs => FixedPoints.gfp fun S ↦ interp γ φ (S :: xs) -def interp_subst_monotone {X : Type} {γ : X → F X} (φ : Formula Λ) (xs : Environment X) (n : ℕ) : +def interp_subst_monotone [LawfulModel Λ F] {X : Type} {γ : X → F X} (φ : Formula Λ) (xs : Environment X) (n : ℕ) : Monotone fun x ↦ interp γ φ (xs.subst n x) := by induction φ generalizing xs n with | top => @@ -179,7 +184,7 @@ def interp_subst_monotone {X : Type} {γ : X → F X} (φ : Formula Λ) (xs : En intro S S' hle simp only [Set.le_eq_subset] apply Set.preimage_mono - apply Model.lifting_monotone + apply LawfulModel.lifting_monotone intro a exact ih a xs n hle | var x => @@ -210,22 +215,14 @@ def interp_subst_monotone {X : Type} {γ : X → F X} (φ : Formula Λ) (xs : En _ = interp γ φ (U :: xs.subst n S') := by rw [Environment.subst_add] · exact hx -lemma interp_lfp_isFixedPt {X : Type} (γ : X → F X) (φ : Formula Λ) (xs : Environment X) : - Function.IsFixedPt (fun S ↦ interp γ φ (S :: xs)) (interp γ (.lfp φ) xs) := by - apply FixedPoints.lfp_isFixedPt +lemma interp_lfp_isLeastFixedPt [LawfulModel Λ F] {X : Type} (γ : X → F X) (φ : Formula Λ) (xs : Environment X) : + Function.IsLeastFixedPt (fun S ↦ interp γ φ (S :: xs)) (interp γ (.lfp φ) xs) := by + apply FixedPoints.lfp_isLeastFixedPt simp [Environment.add, interp_subst_monotone] -lemma interp_lfp_is_least {X : Type} (γ : X → F X) (φ : Formula Λ) (xs : Environment X) : - ∀ x, Function.IsFixedPt (fun S ↦ interp γ φ (S :: xs)) x → interp γ (.lfp φ) xs ⊆ x := by - apply FixedPoints.lfp_is_least - -lemma interp_gfp_isFixedPt {X : Type} (γ : X → F X) (φ : Formula Λ) (xs : Environment X) : - Function.IsFixedPt (fun S ↦ interp γ φ (S :: xs)) (interp γ (.gfp φ) xs) := by - apply FixedPoints.gfp_isFixedPt +lemma interp_gfp_isGreatestFixedPt [LawfulModel Λ F] {X : Type} (γ : X → F X) (φ : Formula Λ) (xs : Environment X) : + Function.IsGreatestFixedPt (fun S ↦ interp γ φ (S :: xs)) (interp γ (.gfp φ) xs) := by + apply FixedPoints.gfp_isGreatestFixedPt simp [Environment.add, interp_subst_monotone] -lemma interp_gfp_is_greatest {X : Type} (γ : X → F X) (φ : Formula Λ) (xs : Environment X) : - ∀ x, Function.IsFixedPt (fun S ↦ interp γ φ (S :: xs)) x → x ⊆ interp γ (.gfp φ) xs := by - apply FixedPoints.gfp_is_greatest - end Semantics |