Theory M2L_Examples

(* Author: Dmitriy Traytel *)

theory M2L_Examples
imports M2L_Equivalence_Checking "HOL-Library.Char_ord"
    "HOL-Library.Product_Lexorder"
begin

abbreviation FALSE where "FALSE ≡ FExists (FLess 0 0)"
abbreviation TRUE where "TRUE ≡ FNot FALSE"
abbreviation All where "All φ ≡ FNot (FExists (FNot φ))"
abbreviation AL where "AL φ ≡ FNot (FEXISTS (FNot φ))"
abbreviation Imp where "Imp φ ψ ≡ FOr (FNot φ) ψ"
abbreviation Iff where "Iff φ ψ ≡ FAnd (Imp φ ψ) (Imp ψ φ)"
abbreviation Ball where "Ball X φ ≡ All (Imp (FIn 0 (X+1)) φ)"
abbreviation Bex where "Bex X φ ≡ FExists (FAnd (FIn 0 (X+1)) φ)"

abbreviation Eq where "Eq x y ≡ FAnd (FNot (FLess x y)) (FNot (FLess y x))"
abbreviation SUBSET where "SUBSET X Y ≡ Ball X (FIn 0 (Y+1))"
abbreviation EQ where "EQ X Y ≡ FAnd (SUBSET X Y) (SUBSET Y X)"
abbreviation First where "First x ≡ FNot (FExists (FLess 0 (x+1)))"
abbreviation Last where "Last x ≡ FNot (FExists (FLess (x+1) 0))"
abbreviation Suc where "Suc sucx x ≡ FAnd (FLess x sucx) (FNot (FExists (FAnd (FLess (x+1) 0) (FLess 0 (sucx+1)))))"

definition "Thm (type :: 'a :: {enum, linorder} itself) n φ = fast.check_eqv n (FNot φ :: 'a formula) FALSE"
definition "Thm_slow (type :: 'a :: {enum, linorder} itself) n φ = slow.check_eqv n (FNot φ :: 'a formula) FALSE"
definition "Thm_dual (type :: 'a :: {enum, linorder} itself) n φ = dual.check_eqv n (FNot φ :: 'a formula) FALSE"

definition "M2L = (FEXISTS (All (FIn 0 1)) :: Enum.finite_1 formula)"

lemma "Thm TYPE(Enum.finite_1) 0 M2L" by eval
lemma "Thm TYPE(Enum.finite_1) 0 (FNot (All (FExists (FLess 1 0))))" by eval
lemma "Thm (TYPE(bool)) 0 (FNot (FExists (FExists (FAnd (FLess 0 1) (FLess 1 0)))))" by eval
lemma Drinker: "Thm (TYPE(bool)) 1 (FExists (Imp (FIn 0 1) (All (FIn 0 2))))" by eval
lemma "Thm (TYPE(bool)) 1 (Imp (All (FIn 0 1)) (FExists (FIn 0 1)))" by eval

(*
definition "mod_two a b c d = Iff a (Iff b (Iff c d))"
definition "at_least_two a b c d = Iff d (FOr (FAnd a b) (FOr (FAnd b c) (FAnd a c)))"

definition "ADD S A B = FEXISTS (FAnd (All (Imp (First 0) (FNot (FIn 0 1))))
  (All (FAnd (mod_two (FIn 0 (A+2)) (FIn 0 (B+2)) (FIn 0 1) (FIn 0 (S+2)))
       (Imp (FExists (FAnd (Last 0) (FLess 1 0)))
            (at_least_two (FIn 0 (A+2)) (FIn 0 (B+2)) (FIn 0 1) (All (Imp (Suc 0 1) (FIn 0 2))))))))"

definition Comm_Lemma :: "Enum.finite_1 formula" where
  "Comm_Lemma = AL (AL (FEXISTS (FAnd (ADD 0 1 2) (FEXISTS (FAnd (ADD 0 3 2) (EQ 0 1))))))"

lemma "Thm TYPE(bool) 0 (AL (AL (FEXISTS (ADD 0 1 2))))"
  by eval

lemma "Thm TYPE(Enum.finite_1) 0 Comm_Lemma"
  by eval
*)

abbreviation Globally ("□_" [40] 40) where "Globally P == %n. All (Imp (FNot (FLess (n+1) 0)) (P 0))"
abbreviation Future ("◇_" [40] 40) where "Future P == %n. FExists (FAnd (FNot (FLess (n+1) 0)) (P 0))"
abbreviation IMP (infixr "→" 50) where "IMP P1 P2 == %n. Imp (P1 n) (P2 n)"

abbreviation "FOR xs n ≡ rexp_of_list FOr FALSE (map (λx. FQ x n) xs)"

abbreviation Φ0 :: "bool formula" where "Φ0 ≡
  (All (((□(FOR [(True)])) → (□(FOR [(True)]))) 0))"

abbreviation Φ1 :: "(bool × bool) formula" where "Φ1 ≡
  (All (((□(FOR [(True, True), (True, False)] →
            FOR [(True, True), (False, True)])) →
         (□(FOR [(True, True), (True, False)])) →
         (□(FOR [(True, True), (False, True)]))) 0))"

abbreviation Φ2 :: "(bool × bool × bool) formula" where "Φ2 ≡ 
  (All (((□(FOR [(True, True, True), (True, True, False), (True, False, True), (True, False, False)] →
            FOR [(True, True, True), (True, True, False), (False, True, True), (False, True, False)] →
            FOR [(True, True, True), (True, False, True), (False, True, True), (False, False, True)])) →
        (□(FOR [(True, True, True), (True, True, False), (True, False, True), (True, False, False)])) →
        (□(FOR [(True, True, True), (True, True, False), (False, True, True), (False, True, False)])) →
        (□(FOR [(True, True, True), (True, True, False), (False, True, True), (False, True, False)]))) 0))"

definition Ψ :: "nat ⇒ Enum.finite_1 formula" where
  "Ψ n = All (((□(foldr (λi φ. (λm. FIn m (2 + i)) → φ) [0..<n] (λm. FIn m (n + 2)))) →
     foldr (λi φ. (□(λm. FIn m (2 + i))) → φ) [0..<n] (□(λm. FIn m (n + 2)))) 0)"

definition "Thm1 n = Thm (TYPE(Enum.finite_1)) (n + 1) (Ψ n)"
definition "Thm1_slow n = Thm_slow (TYPE(Enum.finite_1)) (n + 1) (Ψ n)"
definition "Thm1_dual n = Thm_dual (TYPE(Enum.finite_1)) (n + 1) (Ψ n)"

lemma "Thm1 0" by eval
lemma "Thm1 1" by eval
lemma "Thm1 2" by eval

lemma "Thm (TYPE(bool)) 0 Φ0" by eval
lemma "Thm (TYPE(bool * bool)) 0 Φ1" by eval
lemma "Thm (TYPE(bool * bool * bool)) 0 Φ2" by eval

(*
export_code Thm1 Nat in SML module_name M2L_Thm1 file "M2L_Thm1.ML"
export_code Thm1_slow Nat in SML module_name M2L_Thm1_slow file "M2L_Thm1_slow.ML"
export_code Thm1_dual Nat in SML module_name M2L_Thm1_dual file "M2L_Thm1_dual.ML"

ML_file "M2L_Thm1.ML"
ML_file "M2L_Thm1_slow.ML"
ML_file "M2L_Thm1_dual.ML"

ML {* PolyML.timing true; open M2L_Thm1; thm1 (Nat 0); thm1 (Nat 1); thm1 (Nat 2); thm1 (Nat 3); *}
ML {* PolyML.timing true; open M2L_Thm1_dual; thm1_dual (Nat 0); thm1_dual (Nat 1); thm1_dual (Nat 2); thm1_dual (Nat 3); *}
ML {* PolyML.timing true; open M2L_Thm1_slow; thm1_slow (Nat 0); thm1_slow (Nat 1); thm1_slow (Nat 2); *}
*)
end