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 + xx  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