Theory WS1S_Alt_Examples

section ‹Examples for WS1S (Singleton Semantics)›

(*<*)
theory WS1S_Alt_Examples
imports Formula_Derivatives.WS1S_Alt_Formula
begin
(*>*)

abbreviation (input) FImp where "FImp φ ψ ≡ FOr (FNot φ) ψ"

definition "Thm idx φ = check_eqv idx φ (FBool True)"

export_code Thm in SML module_name Thm

abbreviation FTrue (‹⊤›) where "FTrue ≡ FBool True"
abbreviation FFalse (‹⊥›) where "FFalse ≡ FBool False"

notation FImp (infixr ‹-->› 25)
notation (output) FO (‹1›)
notation (output) SO (‹2›)
notation FEx (‹∃⇩_ _› [10] 10)
notation FAll (‹∀⇩_ _› [10] 10)
notation FNot (‹¬ _› [40] 40)
notation FOr (infixr ‹∨› 30)
notation FAnd (infixr ‹∧› 35)
abbreviation FLess (‹x⇩_ < x⇩_› [65, 66] 65) where "FLess m1 m2 ≡ FBase (Less m1 m2)"
abbreviation FIn (‹x⇩_ ∈ X⇘_⇙› [65, 66] 65) where "FIn m M ≡ FBase (In m M)"
abbreviation FQ (‹[x⇩_]› [66] 65) where "FQ m ≡ FBase (Fo m)"

declare check_eqv_code[code del]

(*true in M2L, false in WS1S*)
definition "M2L = (FEx SO (FAll FO (FBase (In 0 0))) :: formula)"
(*false in M2L, true in WS1S*)
definition "Φ = (FAll FO (FEx FO (FBase (Less 1 0))) :: formula)"

lemma "Thm (Abs_idx (0, 1)) (FNot M2L)"
  by (simp add: M2L_def Thm_def) check_equiv

lemma "Thm (Abs_idx (0, 0)) Φ"
  by (simp add: Thm_def Φ_def) check_equiv

abbreviation Globally (‹□_› [40] 40) where "Globally P == %n. FAll FO (FImp (FNot (FBase (Less (n+1) 0))) (P 0))"
abbreviation Future (‹◇_› [40] 40) where "Future P == %n. FEx FO (FAnd (FNot (FBase (Less (n+1) 0))) (P 0))"
abbreviation IMP (infixr ‹→› 50) where "IMP P1 P2 == %n. FImp (P1 n) (P2 n)"

definition Ψ :: "nat ⇒ formula" where
  "Ψ n = FAll FO (((□(foldr (λi φ. (λm. FBase (In m i)) → φ) [0..<n] (λm. FBase (In m n)))) →
     foldr (λi φ. (□(λm. FBase (In m i))) → φ) [0..<n] (□(λm. FBase (In m n)))) 0)"

lemma "Thm (Abs_idx (0, 1)) (Ψ 0)"
  by (simp add: Thm_def Ψ_def) check_equiv

lemma "Thm (Abs_idx (0, 2)) (Ψ 1)"
  by (simp add: Thm_def Ψ_def) check_equiv

lemma "Thm (Abs_idx (0, 3)) (Ψ 2)"
  by (simp add: Thm_def Ψ_def numeral_nat) check_equiv

lemma "Thm (Abs_idx (0, 4)) (Ψ 3)"
  by (simp add: Thm_def Ψ_def numeral_nat) check_equiv

lemma "Thm (Abs_idx (0, 5)) (Ψ 4)"
  by (simp add: Thm_def Ψ_def numeral_nat) check_equiv

lemma "Thm (Abs_idx (0, 6)) (Ψ 5)"
  by (simp add: Thm_def Ψ_def numeral_nat) check_equiv

(*<*)
end
(*>*)