refactoring

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