Theory Pratts_Counterexamples

(* Title:      Regular Algebras
   Author:     Simon Foster, Georg Struth
   Maintainer: Simon Foster <s.foster at york.ac.uk>
               Georg Struth <g.struth at sheffield.ac.uk>               
*)

section ‹Pratt's Counterexamples›

theory Pratts_Counterexamples
  imports Regular_Algebras
begin

text ‹We create two regular algebra models due to Pratt~cite‹"Pratt"› which are used to
        distinguish K1 algebras from K1l and K1r algebras.›

datatype pratt1 = 
  P1Bot (‹⊥1›) |
  P1Nat nat (‹[_]1›) | 
  P1Infty (‹∞1›) |
  P1Top (‹⊤1›)

datatype pratt2 = 
  P2Bot (‹⊥2›) |
  P2Nat nat (‹[_]2›) | 
  P2Infty (‹∞2›) |
  P2Top (‹⊤2›)

fun pratt1_max where
  "pratt1_max [x]1 [y]1 = [max x y]1" |
  "pratt1_max x ⊥1 = x" |
  "pratt1_max ⊥1 y = y" |
  "pratt1_max ∞1 [y]1 = ∞1" |
  "pratt1_max [y]1 ∞1 = ∞1" |
  "pratt1_max ∞1 ∞1 = ∞1" |
  "pratt1_max ⊤1 x = ⊤1" |
  "pratt1_max x ⊤1 = ⊤1"

fun pratt1_plus :: "pratt1 ⇒ pratt1 ⇒ pratt1" (infixl ‹+1› 65) where
  "[x]1 +1 [y]1 = [x + y]1" |
  "⊥1 +1 x = ⊥1" |
  "x +1 ⊥1 = ⊥1" |
  "∞1 +1 [0]1 = ∞1" |
  "[0]1 +1 ∞1 = ∞1" |
  "∞1 +1 ∞1 = ⊤1" | (* Can be adjusted to PInfty *)
  "⊤1 +1 x = ⊤1" |
  "x +1 ⊤1 = ⊤1" |
  "[x]1 +1 ∞1 = ∞1" |
  "∞1 +1 x = ⊤1"

lemma plusl_top_infty: "⊤1 +1 ∞1 = ⊤1"
  by (simp)

lemma plusl_infty_top: "∞1 +1 ⊤1  = ⊤1"
  by (simp)

lemma plusl_bot_infty: "⊥1 +1 ∞1 = ⊥1"
  by (simp)

lemma plusl_infty_bot: "∞1 +1 ⊥1  = ⊥1"
  by (simp)

lemma plusl_zero_infty: "[0]1 +1 ∞1 = ∞1"
  by (simp)

lemma plusl_infty_zero: "∞1 +1 [0]1 = ∞1"
  by (simp)

lemma plusl_infty_num [simp]: "x > 0 ⟹ ∞1 +1 [x]1 = ⊤1"
  by (case_tac x, simp_all)

lemma plusl_num_infty [simp]: "x > 0 ⟹ [x]1 +1 ∞1 = ∞1"
  by (case_tac x, simp_all)

fun pratt2_max where
  "pratt2_max [x]2 [y]2 = [max x y]2" |
  "pratt2_max x ⊥2 = x" |
  "pratt2_max ⊥2 y = y" |
  "pratt2_max ∞2 [y]2 = ∞2" |
  "pratt2_max [y]2 ∞2 = ∞2" |
  "pratt2_max ∞2 ∞2 = ∞2" |
  "pratt2_max ⊤2 x = ⊤2" |
  "pratt2_max x ⊤2 = ⊤2"

fun pratt2_plus :: "pratt2 ⇒ pratt2 ⇒ pratt2" (infixl ‹+2› 65) where
  "[x]2 +2 [y]2 = [x + y]2" |
  "⊥2 +2 x = ⊥2" |
  "x +2 ⊥2 = ⊥2" |
  "∞2 +2 [0]2 = ∞2" |
  "[0]2 +2 ∞2 = ∞2" |
  "∞2 +2 ∞2 = ⊤2" | (* Can be adjusted to PInfty *)
  "⊤2 +2 x = ⊤2" |
  "x +2 ⊤2 = ⊤2" |
  "x +2 ∞2 = ⊤2" |
  "∞2 +2 [x]2 = ∞2"

instantiation pratt1 :: selective_semiring
begin

  definition zero_pratt1_def:
    "0 ≡ ⊥1"

  definition one_pratt1_def:
    "1 ≡ [0]1"

  definition plus_pratt1_def:
    "x + y ≡ pratt1_max x y"

  definition times_pratt1_def:
    "x * y ≡ x +1 y"

  definition less_eq_pratt1_def:
    "(x::pratt1) ≤ y ≡ x + y = y"

  definition less_pratt1_def:
    "(x::pratt1) < y ≡ x ≤ y ∧ x ≠ y"

  instance
  proof
    fix x y z :: pratt1
    show "x + y + z = x + (y + z)"
      by (case_tac x, case_tac[!] y, case_tac[!] z, simp_all add: plus_pratt1_def)
    show "x + y = y + x"
      by (cases x, case_tac[!] y, simp_all add: plus_pratt1_def)
    show "x * y * z = x * (y * z)"
      apply (cases x, case_tac[!] y, case_tac[!] z, simp_all add: plus_pratt1_def times_pratt1_def)
      apply (rename_tac[!] n, case_tac[!] n, auto)
      apply (metis nat.exhaust plusl_zero_infty pratt1_plus.simps(14))
      apply (metis not0_implies_Suc plusl_infty_zero plusl_zero_infty pratt1_plus.simps(14))
      apply (metis neq0_conv plusl_num_infty plusl_zero_infty pratt1_plus.simps(15))
      apply (metis not0_implies_Suc plusl_infty_zero pratt1_plus.simps(15) pratt1_plus.simps(9))
      apply (metis not0_implies_Suc plusl_infty_zero pratt1_plus.simps(15) pratt1_plus.simps(9))
    done
    show "(x + y) * z = x * z + y * z"
      apply (cases x, case_tac[!] y, case_tac[!] z, simp_all add: plus_pratt1_def times_pratt1_def)
      apply (rename_tac[!] n, case_tac[!] n, auto)
      apply (metis neq0_conv plusl_num_infty plusl_zero_infty pratt1_max.simps(8))+
    done
    show "1 * x = x"
      by (cases x, simp_all add: one_pratt1_def times_pratt1_def)
    show "x * 1 = x"
      by (cases x, simp_all add: one_pratt1_def times_pratt1_def)
    show "0 + x = x"
      by (cases x, simp_all add: plus_pratt1_def zero_pratt1_def)
    show "0 * x = 0"
      by (cases x, simp_all add: times_pratt1_def zero_pratt1_def)
    show "x * 0 = 0"
      by (cases x, simp_all add: times_pratt1_def zero_pratt1_def)
    show "x ≤ y ⟷ x + y = y"
      by (metis less_eq_pratt1_def)
    show "x < y ⟷ x ≤ y ∧ x ≠ y"
      by (metis less_pratt1_def)
    show "x + y = x ∨ x + y = y"
      by (cases x, case_tac[!] y, simp_all add: plus_pratt1_def max_def)
    show "x * (y + z) = x * y + x * z"
      apply (cases x, case_tac[!] y, case_tac[!] z, simp_all add: plus_pratt1_def times_pratt1_def)
      apply (rename_tac[!] n, case_tac[!] n, auto)
      apply (metis nat.exhaust plusl_zero_infty pratt1_max.simps(7) pratt1_plus.simps(14))
      apply (metis neq0_conv plusl_num_infty plusl_zero_infty pratt1_max.simps(7))
      apply (metis nat.exhaust plusl_zero_infty pratt1_max.simps(6) pratt1_plus.simps(14))
      apply (metis neq0_conv plusl_num_infty plusl_zero_infty pratt1_max.simps(6))
      apply (metis neq0_conv plusl_infty_num plusl_infty_zero pratt1_max.simps(10) pratt1_max.simps(8))
      apply (metis not0_implies_Suc plusl_infty_zero pratt1_max.simps(11) pratt1_max.simps(13) pratt1_plus.simps(15))
    done 
  qed
end 

instance pratt1 :: dioid_one_zero ..

instantiation pratt2 :: selective_semiring
begin

  definition zero_pratt2_def:
    "0 ≡ ⊥2"

  definition one_pratt2_def:
    "1 ≡ [0]2"

  definition times_pratt2_def:
    "x * y ≡ x +2 y"

  definition plus_pratt2 :: "pratt2 ⇒ pratt2 ⇒ pratt2" where
    "plus_pratt2 x y ≡ pratt2_max x y"

  definition less_eq_pratt2_def:
    "(x::pratt2) ≤ y ≡ x + y = y"

  definition less_pratt2_def:
    "(x::pratt2) < y ≡ x ≤ y ∧ x ≠ y"

  instance
  proof
    fix x y z :: pratt2
    show "x + y + z = x + (y + z)"
      by (case_tac x, case_tac[!] y, case_tac[!] z, simp_all add: plus_pratt2_def)
    show "x + y = y + x"
      by (cases x, case_tac[!] y, simp_all add: plus_pratt2_def)
    show "x * y * z = x * (y * z)"
      apply (cases x, case_tac[!] y, case_tac[!] z, auto simp add: times_pratt2_def)
      apply (rename_tac[!] n, case_tac[!] n, auto)
      apply (metis not0_implies_Suc pratt2_plus.simps(14) pratt2_plus.simps(6) pratt2_plus.simps(7) pratt2_plus.simps(9))
      apply (metis not0_implies_Suc pratt2_plus.simps(14) pratt2_plus.simps(15) pratt2_plus.simps(7) pratt2_plus.simps(9))
      apply (metis not0_implies_Suc pratt2_plus.simps(15) pratt2_plus.simps(6))
      apply (metis not0_implies_Suc pratt2_plus.simps(15) pratt2_plus.simps(6))
    done
    show "(x + y) * z = x * z + y * z"
      apply (cases x, case_tac[!] y, case_tac[!] z, simp_all add: plus_pratt2_def times_pratt2_def)
      apply (rename_tac[!] n, case_tac[!] n, auto)
      apply (metis not0_implies_Suc pratt2_max.simps(10) pratt2_max.simps(8) pratt2_plus.simps(14) pratt2_plus.simps(7))
      apply (metis max_0L max_0R max.left_idem nat.exhaust pratt2_max.simps(11) 
                   pratt2_max.simps(13) pratt2_plus.simps(14) pratt2_plus.simps(7))
    done
    show "1 * x = x"
      by (cases x, simp_all add: one_pratt2_def times_pratt2_def)
    show "x * 1 = x"
      by (cases x, simp_all add: one_pratt2_def times_pratt2_def)
    show "0 + x = x"
      by (cases x, simp_all add: plus_pratt2_def zero_pratt2_def)
    show "0 * x = 0"
      by (cases x, simp_all add: times_pratt2_def zero_pratt2_def)
    show "x * 0 = 0"
      by (cases x, simp_all add: times_pratt2_def zero_pratt2_def)
    show "x ≤ y ⟷ x + y = y"
      by (metis less_eq_pratt2_def)
    show "x < y ⟷ x ≤ y ∧ x ≠ y"
      by (metis less_pratt2_def)
    show "x + y = x ∨ x + y = y"
      by (cases x, case_tac[!] y, simp_all add: plus_pratt2_def max_def)
    show "x * (y + z) = x * y + x * z"
      apply (cases x, case_tac[!] y, case_tac[!] z, simp_all add: plus_pratt2_def times_pratt2_def)
      apply (rename_tac[!] n, case_tac[!] n, auto)
      apply (metis not0_implies_Suc pratt2_max.simps(12) pratt2_max.simps(7) pratt2_plus.simps(14) pratt2_plus.simps(7))
      apply (metis nat.exhaust pratt2_max.simps(12) pratt2_max.simps(7) pratt2_plus.simps(14) pratt2_plus.simps(7))
      apply (metis not0_implies_Suc pratt2_max.simps(6) pratt2_max.simps(9) pratt2_plus.simps(14) pratt2_plus.simps(7))
      apply (metis nat.exhaust pratt2_max.simps(6) pratt2_max.simps(9) pratt2_plus.simps(14) pratt2_plus.simps(7))
      apply (metis not0_implies_Suc pratt2_max.simps(8) pratt2_plus.simps(15) pratt2_plus.simps(6))
      apply (metis not0_implies_Suc pratt2_max.simps(8) pratt2_plus.simps(15) pratt2_plus.simps(6))
    done
  qed
end 

lemma top_greatest: "x ≤ ⊤1"
  by (case_tac x, auto simp add: less_eq_pratt1_def plus_pratt1_def)
  
instantiation pratt1 :: star_op
begin

  definition star_pratt1 where
    "x⋆ ≡ if (x = ⊥1 ∨ x = [0]1) then [0]1 else ⊤1"
  instance ..
end

instantiation pratt2 :: star_op
begin
  definition star_pratt2 where
    "x⋆ ≡ if (x = ⊥2 ∨ x = [0]2) then [0]2 else ⊤2"
  instance ..
end

instance pratt1 :: K1r_algebra
proof
  fix x :: pratt1
  show "1 + x⋆ ⋅ x ≤ x⋆"
    by  (case_tac x, auto simp add: star_pratt1_def one_pratt1_def times_pratt1_def less_eq_pratt1_def plus_pratt1_def)
next
  fix x y :: pratt1
  show "y ⋅ x ≤ y ⟹ y ⋅ x⋆ ≤ y"
    apply (case_tac x, case_tac[!] y)
    apply (auto simp add:star_pratt1_def one_pratt1_def times_pratt1_def less_eq_pratt1_def plus_pratt1_def)
    apply (rename_tac n, case_tac n)
    apply (simp_all)
    by (metis not0_implies_Suc plusl_zero_infty pratt1.distinct(7) pratt1_max.simps(6) pratt1_plus.simps(14))
qed

instance pratt2 :: K1l_algebra
proof
  fix x :: pratt2
  show "1 + x⋅x⋆ ≤ x⋆"
    by (case_tac x, auto simp add: star_pratt2_def one_pratt2_def times_pratt2_def less_eq_pratt2_def plus_pratt2_def)
next
  fix x y :: pratt2
  show "x ⋅ y ≤ y ⟹ x⋆ ⋅ y ≤ y"
    apply (case_tac x, case_tac[!] y)
    apply (auto simp add:star_pratt2_def one_pratt2_def times_pratt2_def less_eq_pratt2_def plus_pratt2_def)
    apply (rename_tac n, case_tac n)
    apply (simp_all)
    apply (rename_tac n, case_tac n)
    apply (auto simp add:star_pratt2_def one_pratt2_def times_pratt2_def less_eq_pratt2_def plus_pratt2_def)
  done
qed

lemma one_star_top: "[1]1⋆ = ⊤1"
  by (simp add:star_pratt1_def one_pratt1_def)

lemma pratt1_kozen_1l_counterexample:
  "∃ x y :: pratt1. ¬ (x ⋅ y ≤ y ∧ x⋆ ⋅ y ≤ y)"
proof -
  have "¬ ([1]1 ⋅ ∞1 ≤ ∞1 ∧ [1]1⋆ ⋅ ∞1 ≤ ∞1)"
    by (auto simp add: star_pratt1_def times_pratt1_def less_eq_pratt1_def plus_pratt1_def)
  thus ?thesis
    by auto
qed

lemma pratt2_kozen_1r_counterexample:
  "∃ x y :: pratt2. ¬ (y ⋅ x ≤ y ∧ y ⋅ x⋆ ≤ y)"
proof -
  have "¬ (∞2 ⋅ [1]2 ≤ ∞2 ∧ ∞2 ⋅ [1]2⋆ ≤ ∞2)"
    by (auto simp add: star_pratt2_def times_pratt2_def less_eq_pratt2_def plus_pratt2_def)
  thus ?thesis
    by auto
qed

end