Theory WS1S_Nameful_Examples

section ‹Examples for Nameful WS1S Formulas›

(*<*)
theory WS1S_Nameful_Examples
imports Formula_Derivatives.WS1S_Nameful Show.Show_Instances
begin
(*>*)

lift_definition x :: fo is "''x''" by simp
lift_definition y :: fo is "''y''" by simp
lift_definition z :: fo is "''z''" by simp
lift_definition X :: so is "''X''" by simp
lift_definition Y :: so is "''Y''" by simp
lift_definition Z :: so is "''Z''" by simp
lift_definition Xi :: "nat ⇒ so" is "λi. ''X'' @ show i" by simp

abbreviation Imp where "Imp φ ψ ≡ Or (Not φ) ψ"
(*true in M2L, false in WS1S*)
definition "M2L = Ex2 X (All1 x (In x X))"
(*false in M2L, true in WS1S*)
definition "Φ = All1 x (Ex1 y (Lt x y))"

abbreviation Globally (‹□_› [40] 40) where
  "Globally P t ==  All1 z (Imp (Not (Lt t z)) (P z))"
abbreviation Future (‹◇_› [40] 40) where
  "Future P t == Ex1 z (And (Not (Lt t z)) (P z))"
abbreviation IMP (infixr ‹→› 50) where "IMP P1 P2 t == Imp (P1 t) (P2 t)"

definition Ψ :: "nat ⇒ ws1s" where
  "Ψ n = All1 x
     (((□(foldr (λi φ. (λm. In m (Xi i)) → φ) [0..<n] (λm. (In m (Xi n))))) →
     foldr (λi φ. (□(λm. (In m (Xi i)))) → φ) [0..<n]
       (□(λm. (In m (Xi n))))) x)"

method_setup check_equiv = ‹
  let
    fun tac ctxt =
      let
        val conv = @{computation_check terms: Trueprop
          "0 :: nat" "1 :: nat" "2 :: nat" "3 :: nat" Suc
          "plus :: nat ⇒ _" "minus :: nat ⇒ _"
          "times :: nat ⇒ _" "divide :: nat ⇒ _" "modulo :: nat ⇒ _"
          "0 :: int" "1 :: int" "2 :: int" "3 :: int" "-1 :: int"
          Thm x y z X Y Z Xi Ψ Φ M2L eqv datatypes: formula "int list" integer idx
         "nat × nat" "nat option" "bool option" ws1s} ctxt
      in
        CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN'
        resolve_tac ctxt [TrueI]
      end
  in
    Scan.succeed (SIMPLE_METHOD' o tac)
  end
›

lemma "Thm (Not M2L)"
  by check_equiv

lemma "Thm Φ"
  by check_equiv

lemma "eqv (And (Eq_Const x 10) (Eq_Const x 10000)) F"
  by check_equiv

lemma "Thm (Ψ 0)"
  by check_equiv

lemma "Thm (Ψ 1)"
  by check_equiv

lemma "Thm (Ψ 2)"
  by check_equiv

lemma "Thm (Ψ 3)"
  by check_equiv

lemma "Thm (Ψ 4)"
  by check_equiv

lemma "Thm (Ψ 5)"
  by check_equiv

lemma "Thm (Ψ 10)"
  by check_equiv

lemma "Thm (Ψ 15)"
  by check_equiv

(*<*)
end
(*>*)