Theory Test_Iterings

(* Title:      Test Iterings
   Author:     Walter Guttmann
   Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section Test Iterings

theory Test_Iterings

imports Stone_Kleene_Relation_Algebras.Iterings Tests

begin

class test_itering = itering + tests + while +
  assumes while_def: "p  y = (p * y) * -p"
begin

lemma wnf_lemma_5:
  "(-p  -q) * (-q * x  --q * y) = -q * x  --q * -p * y"
  by (smt (z3) mult_left_dist_sup sup_commute tests_dual.sba_dual.sub_sup_closed tests_dual.sba_dual.sup_complement_intro tests_dual.sba_dual.sup_idempotent tests_dual.sup_idempotent mult_assoc tests_dual.wnf_lemma_3)

lemma test_case_split_left_equal:
  "-z * x = -z * y  --z * x = --z * y  x = y"
  by (metis case_split_left_equal tests_dual.inf_complement)

lemma preserves_equation:
  "-y * x  x * -y  -y * x = -y * x * -y"
  apply (rule iffI)
  apply (simp add: test_preserves_equation tests_dual.sub_bot_least)
  by (simp add: test_preserves_equation tests_dual.sub_bot_least)

text Theorem 5

lemma preserve_test:
  "-y * x  x * -y  -y * x = -y * x * -y"
  using circ_simulate preserves_equation by blast

text Theorem 5

lemma import_test:
  "-y * x  x * -y  -y * x = -y * (-y * x)"
  by (simp add: circ_import tests_dual.sub_bot_least)

definition ite :: "'a  'a  'a  'a" ("_  _  _" [58,58,58] 57)
  where "x  p  y  p * x  -p * y"

definition it :: "'a  'a  'a" ("_  _" [58,58] 57)
  where "p  x  p * x  -p"

(*
definition while :: "'a ⇒ 'a ⇒ 'a" (infixr "⋆" 59)
  where "p ⋆ y ≡ (p * y) * -p"
*)

definition assigns :: "'a  'a  'a  bool"
  where "assigns x p q  x = x * (p * q  -p * -q)"

definition preserves :: "'a  'a  bool"
  where "preserves x p  p * x  x * p  -p * x  x * -p"

lemma ite_neg:
  "x  -p  y = y  --p  x"
  by (simp add: ite_def sup_commute)

lemma ite_import_true:
  "x  -p  y = -p * x  -p  y"
  by (metis ite_def tests_dual.sup_idempotent mult_assoc)

lemma ite_import_false:
  "x  -p  y = x  -p  --p * y"
  by (metis ite_import_true ite_neg)

lemma ite_import_true_false:
  "x  -p  y = -p * x  -p  --p * y"
  using ite_import_false ite_import_true by auto

lemma ite_context_true:
  "-p * (x  -p  y) = -p * x"
  by (metis sup_monoid.add_0_left tests_dual.sup_right_zero tests_dual.top_double_complement wnf_lemma_5 sup_bot_right ite_def mult_assoc mult_left_zero)

lemma ite_context_false:
  "--p * (x  -p  y) = --p * y"
  by (metis ite_neg ite_context_true)

lemma ite_context_import:
  "-p * (x  -q  y) = -p * (x  -p * -q  y)"
  by (smt ite_def mult_assoc tests_dual.sup_complement_intro tests_dual.sub_sup_demorgan tests_dual.sup_idempotent mult_left_dist_sup)

lemma ite_conjunction:
  "(x  -q  y)  -p  y = x  -p * -q  y"
  by (smt sup_assoc sup_commute ite_def mult_assoc tests_dual.sub_sup_demorgan mult_left_dist_sup mult_right_dist_sup tests_dual.inf_complement_intro)

lemma ite_disjunction:
  "x  -p  (x  -q  y) = x  -p  -q  y"
  by (smt (z3) tests_dual.sba_dual.sub_sup_closed sup_assoc ite_def mult_assoc tests_dual.sup_complement_intro tests_dual.sub_sup_demorgan mult_left_dist_sup mult_right_dist_sup tests_dual.inf_demorgan)

lemma wnf_lemma_6:
  "(-p  -q) * (x  --p * -q  y) = (-p  -q) * (y  -p  x)"
  by (smt (z3) ite_conjunction ite_context_false ite_context_true semiring.distrib_right tests_dual.sba_dual.inf_cases_2 tests_dual.sba_dual.sub_inf_def tests_dual.sba_dual.sup_complement_intro tests_dual.sub_complement)

lemma it_ite:
  "-p  x = x  -p  1"
  by (simp add: it_def ite_def)

lemma it_neg:
  "--p  x = 1  -p  x"
  using it_ite ite_neg by auto

lemma it_import_true:
  "-p  x = -p  -p * x"
  using it_ite ite_import_true by auto

lemma it_context_true:
  "-p * (-p  x) = -p * x"
  by (simp add: it_ite ite_context_true)

lemma it_context_false:
  "--p * (-p  x) = --p"
  using it_ite ite_context_false by force

lemma while_unfold_it:
  "-p  x = -p  x * (-p  x)"
  by (metis circ_loop_fixpoint it_def mult_assoc while_def)

lemma while_context_false:
  "--p * (-p  x) = --p"
  by (metis it_context_false while_unfold_it)

lemma while_context_true:
  "-p * (-p  x) = -p * x * (-p  x)"
  by (metis it_context_true mult_assoc while_unfold_it)

lemma while_zero:
  "bot  x = 1"
  by (metis circ_zero mult_left_one mult_left_zero one_def while_def)

lemma wnf_lemma_7:
  "1 * (bot  1) = 1"
  by (simp add: while_zero)

lemma while_import_condition:
  "-p  x = -p  -p * x"
  by (metis mult_assoc tests_dual.sup_idempotent while_def)

lemma while_import_condition_2:
  "-p * -q  x = -p * -q  -p * x"
  by (metis mult_assoc tests_dual.sup_idempotent sub_comm while_def)

lemma wnf_lemma_8:
  "-r * (-p  --p * -q)  (x  --p * -q  y) = -r * (-p  -q)  (y  -p  x)"
  by (metis mult_assoc while_def wnf_lemma_6 tests_dual.sba_dual.sup_complement_intro)

text Theorem 6 - see Theorem 31 on page 329 of Back and von Wright, Acta Informatica 36:295-334, 1999

lemma split_merge_loops:
  assumes "--p * y  y * --p"
    shows "(-p  -q)  (x  -p  y) = (-p  x) * (-q  y)"
proof -
  have "-p  -q  (x  -p  y) = (-p * x  --p * -q * y) * --p * --q"
    by (smt ite_def mult_assoc sup_commute tests_dual.inf_demorgan while_def wnf_lemma_5)
  thus ?thesis
    by (smt assms circ_sup_1 circ_slide import_test mult_assoc preserves_equation sub_comm while_context_false while_def)
qed

lemma assigns_same:
  "assigns x (-p) (-p)"
  by (simp add: assigns_def)

lemma preserves_equation_test:
  "preserves x (-p)  -p * x = -p * x * -p  --p * x = --p * x * --p"
  using preserves_def preserves_equation by auto

lemma preserves_test:
  "preserves (-q) (-p)"
  using tests_dual.sub_commutative preserves_def by auto

lemma preserves_zero:
  "preserves bot (-p)"
  using tests_dual.sba_dual.sub_bot_def preserves_test by blast

lemma preserves_one:
  "preserves 1 (-p)"
  using preserves_def by force

lemma preserves_sup:
  "preserves x (-p)  preserves y (-p)  preserves (x  y) (-p)"
  by (simp add: mult_left_dist_sup mult_right_dist_sup preserves_equation_test)

lemma preserves_mult:
  "preserves x (-p)  preserves y (-p)  preserves (x * y) (-p)"
  by (smt (verit, best) mult_assoc preserves_equation_test)

lemma preserves_ite:
  "preserves x (-p)  preserves y (-p)  preserves (x  -q  y) (-p)"
  by (simp add: ite_def preserves_mult preserves_sup preserves_test)

lemma preserves_it:
  "preserves x (-p)  preserves (-q  x) (-p)"
  by (simp add: it_ite preserves_ite preserves_one)

lemma preserves_circ:
  "preserves x (-p)  preserves (x) (-p)"
  by (meson circ_simulate preserves_def)

lemma preserves_while:
  "preserves x (-p)  preserves (-q  x) (-p)"
  using while_def preserves_circ preserves_mult preserves_test by auto

lemma preserves_test_neg:
  "preserves x (-p)  preserves x (--p)"
  using preserves_def by auto

lemma preserves_import_circ:
  "preserves x (-p)  -p * x = -p * (-p * x)"
  using import_test preserves_def by blast

lemma preserves_simulate:
  "preserves x (-p)  -p * x = -p * x * -p"
  using preserve_test preserves_def by auto

lemma preserves_import_ite:
  assumes "preserves z (-p)"
    shows "z * (x  -p  y) = z * x  -p  z * y"
proof -
  have 1: "-p * z * (x  -p  y) = -p * (z * x  -p  z * y)"
    by (smt assms ite_context_true mult_assoc preserves_equation_test)
  have "--p * z * (x  -p  y) = --p * (z * x  -p  z * y)"
    by (smt (z3) assms ite_context_false mult_assoc preserves_equation_test)
  thus ?thesis
    using 1 by (metis mult_assoc test_case_split_left_equal)
qed

lemma preserves_while_context:
  "preserves x (-p)  -p * (-q  x) = -p * (-p * -q  x)"
  by (smt (verit, del_insts) mult_assoc tests_dual.sup_complement_intro tests_dual.sub_sup_demorgan preserves_import_circ preserves_mult preserves_simulate preserves_test while_def)

lemma while_ite_context_false:
  assumes "preserves y (-p)"
    shows "--p * (-p  -q  (x  -p  y)) = --p * (-q  y)"
proof -
  have "--p * (-p  -q  (x  -p  y)) = --p * (--p * -q * y) * -(-p  -q)"
    by (smt (z3) assms import_test mult_assoc preserves_equation preserves_equation_test sub_comm while_def tests_dual.sba_dual.sub_sup_demorgan preserves_test split_merge_loops while_context_false)
  thus ?thesis
    by (metis (no_types, lifting) assms preserves_def mult.assoc split_merge_loops while_context_false)
qed

text Theorem 7.1

lemma while_ite_norm:
  assumes "assigns z (-p) (-q)"
      and "preserves x1 (-q)"
      and "preserves x2 (-q)"
      and "preserves y1 (-q)"
      and "preserves y2 (-q)"
    shows "z * (x1 * (-r1  y1)  -p  x2 * (-r2  y2)) = z * (x1  -q  x2) * ((-q * -r1  --q * -r2)  (y1  -q  y2))"
proof -
  have 1: "-(-q * -r1  --q * -r2) = -q * --r1  --q * --r2"
    by (smt (z3) tests_dual.complement_2 tests_dual.sub_sup_closed tests_dual.case_duality tests_dual.sub_sup_demorgan)
  have "-p * -q * x1 * (-q * -r1 * y1  --q * -r2 * y2) * (-q * --r1  --q * --r2) = -p * -q * x1 * -q * (-q * (-q * -r1 * y1  --q * -r2 * y2)) * (-q * --r1  --q * --r2)"
    by (smt (verit, del_insts) assms(2,4,5) mult_assoc preserves_sup preserves_equation_test preserves_import_circ preserves_mult preserves_test)
  also have "... = -p * -q * x1 * -q * (-q * -r1 * y1) * (-q * --r1  --q * --r2)"
    using ite_context_true ite_def mult_assoc by auto
  finally have 2: "-p * -q * x1 * (-q * -r1 * y1  --q * -r2 * y2) * (-q * --r1  --q * --r2) = -p * -q * x1 * (-r1 * y1) * --r1"
    by (smt (verit, del_insts) assms ite_context_true ite_def mult_assoc preserves_equation_test preserves_import_circ preserves_mult preserves_simulate preserves_test)
  have "--p * --q * x2 * (-q * -r1 * y1  --q * -r2 * y2) * (-q * --r1  --q * --r2) = --p * --q * x2 * --q * (--q * (-q * -r1 * y1  --q * -r2 * y2)) * (-q * --r1  --q * --r2)"
    by (smt (verit, del_insts) assms mult_assoc preserves_sup preserves_equation_test preserves_import_circ preserves_mult preserves_test preserves_test_neg)
  also have "... = --p * --q * x2 * --q * (--q * -r2 * y2) * (-q * --r1  --q * --r2)"
    using ite_context_false ite_def mult_assoc by auto
  finally have "--p * --q * x2 * (-q * -r1 * y1  --q * -r2 * y2) * (-q * --r1  --q * --r2) = --p * --q * x2 * (-r2 * y2) * --r2"
    by (smt (verit, del_insts) assms(3,5) ite_context_false ite_def mult_assoc preserves_equation_test preserves_import_circ preserves_mult preserves_simulate preserves_test preserves_test_neg)
  thus ?thesis
    using 1 2 by (smt (z3) assms(1) assigns_def mult_assoc mult_right_dist_sup while_def ite_context_false ite_context_true tests_dual.sub_commutative)
qed

lemma while_it_norm:
  "assigns z (-p) (-q)  preserves x (-q)  preserves y (-q)  z * (-p  x * (-r  y)) = z * (-q  x) * (-q * -r  y)"
  by (metis sup_bot_right tests_dual.sup_right_zero it_context_true it_ite tests_dual.complement_bot preserves_one while_import_condition_2 while_ite_norm wnf_lemma_7)

lemma while_else_norm:
  "assigns z (-p) (-q)  preserves x (-q)  preserves y (-q)  z * (1  -p  x * (-r  y)) = z * (1  -q  x) * (--q * -r  y)"
  by (metis sup_bot_left tests_dual.sup_right_zero ite_context_false tests_dual.complement_bot preserves_one while_import_condition_2 while_ite_norm wnf_lemma_7)

lemma while_while_pre_norm:
  "-p  x * (-q  y) = -p  x * (-p  -q  (y  -q  x))"
  by (smt sup_commute circ_sup_1 circ_left_unfold circ_slide it_def ite_def mult_assoc mult_left_one mult_right_dist_sup tests_dual.inf_demorgan while_def wnf_lemma_5)

text Theorem 7.2

lemma while_while_norm:
  "assigns z (-p) (-r)  preserves x (-r)  preserves y (-r)  z * (-p  x * (-q  y)) = z * (-r  x) * (-r * (-p  -q)  (y  -q  x))"
  by (smt tests_dual.double_negation tests_dual.sub_sup_demorgan tests_dual.inf_demorgan preserves_ite while_it_norm while_while_pre_norm)

lemma while_seq_replace:
  "assigns z (-p) (-q)  z * (-p  x * z) * y = z * (-q  x * z) * y"
  by (smt assigns_def circ_slide mult_assoc tests_dual.wnf_lemma_1 tests_dual.wnf_lemma_2 tests_dual.wnf_lemma_3 tests_dual.wnf_lemma_4 while_def)

lemma while_ite_replace:
  "assigns z (-p) (-q)  z * (x  -p  y) = z * (x  -q  y)"
  by (smt assigns_def ite_def mult_assoc mult_left_dist_sup sub_comm tests_dual.wnf_lemma_1 tests_dual.wnf_lemma_3)

lemma while_post_norm_an:
  assumes "preserves y (-p)"
    shows "(-p  x) * y = y  --p  (-p  x * (--p  y))"
proof -
  have "-p * (-p * x * (--p * y  -p)) * --p = -p * x * ((--p * y  -p) * -p * x) * (--p * y  -p) * --p"
    by (metis circ_slide_1 while_def mult_assoc while_context_true)
  also have "... = -p * x * (--p * y * bot  -p * x) * --p * y"
    by (smt assms sup_bot_right mult_assoc tests_dual.sup_complement tests_dual.sup_idempotent mult_left_zero mult_right_dist_sup preserves_equation_test sub_comm)
  finally have "-p * (-p * x * (--p * y  -p)) * --p = -p * x * (-p * x) * --p * y"
    by (metis circ_sup_mult_zero sup_commute mult_assoc)
  thus ?thesis
    by (smt circ_left_unfold tests_dual.double_negation it_def ite_def mult_assoc mult_left_one mult_right_dist_sup while_def)
qed

lemma while_post_norm:
  "preserves y (-p)  (-p  x) * y = -p  x * (1  -p  y)  -p  y"
  using it_neg ite_neg while_post_norm_an by force

lemma wnf_lemma_9:
  assumes "assigns z (-p) (-q)"
      and "preserves x1 (-q)"
      and "preserves y1 (-q)"
      and "preserves x2 (-q)"
      and "preserves y2 (-q)"
      and "preserves x2 (-p)"
      and "preserves y2 (-p)"
    shows "z * (x1  -q  x2) * (-q * -p  -r  (y1  -q * -p  y2)) = z * (x1  -p  x2) * (-p  -r  (y1  -p  y2))"
proof -
  have "z * --p * --q * (x1  -q  x2) * (-q * -p  -r  (y1  -q * -p  y2)) = z * --p * --q * x2 * --q * (--q * (-q * -p  -r)  (y1  -q * -p  y2))"
    by (smt (verit, del_insts) assms(3-5) tests_dual.double_negation ite_context_false mult_assoc tests_dual.sub_sup_demorgan tests_dual.inf_demorgan preserves_equation_test preserves_ite preserves_while_context)
  also have "... = z * --p * --q * x2 * --q * (--q * -r  --q * y2)"
    by (smt sup_bot_left tests_dual.double_negation ite_conjunction ite_context_false mult_assoc tests_dual.sup_complement mult_left_dist_sup mult_left_zero while_import_condition_2)
  also have "... = z * --p * --q * x2 * (-r  y2)"
    by (metis assms(4,5) mult_assoc preserves_equation_test preserves_test_neg preserves_while_context while_import_condition_2)
  finally have 1: "z * --p * --q * (x1  -q  x2) * (-q * -p  -r  (y1  -q * -p  y2)) = z * --p * --q * (x1  -q  x2) * (-p  -r  (y1  -p  y2))"
    by (smt assms(6,7) ite_context_false mult_assoc preserves_equation_test sub_comm while_ite_context_false)
  have "z * -p * -q * (x1  -q  x2) * (-q * -p  -r  (y1  -q * -p  y2)) = z * -p * -q * (x1  -q  x2) * -q * (-q * (-p  -r)  -q * (y1  -p  y2))"
    by (smt (verit, del_insts) assms(2-5) tests_dual.double_negation ite_context_import mult_assoc tests_dual.sub_sup_demorgan tests_dual.sup_idempotent mult_left_dist_sup tests_dual.inf_demorgan preserves_equation_test preserves_ite preserves_while_context while_import_condition_2)
  hence "z * -p * -q * (x1  -q  x2) * (-q * -p  -r  (y1  -q * -p  y2)) = z * -p * -q * (x1  -q  x2) * (-p  -r  (y1  -p  y2))"
    by (smt assms(2-5) tests_dual.double_negation mult_assoc tests_dual.sub_sup_demorgan tests_dual.sup_idempotent preserves_equation_test preserves_ite preserves_while_context while_import_condition_2)
  thus ?thesis
    using 1 by (smt assms(1) assigns_def mult_assoc mult_left_dist_sup mult_right_dist_sup while_ite_replace)
qed

text Theorem 7.3

lemma while_seq_norm:
  assumes "assigns z1 (-r1) (-q)"
      and "preserves x2 (-q)"
      and "preserves y2 (-q)"
      and "preserves z2 (-q)"
      and "z1 * z2 = z2 * z1"
      and "assigns z2 (-q) (-r)"
      and "preserves y1 (-r)"
      and "preserves z1 (-r)"
      and "preserves x2 (-r)"
      and "preserves y2 (-r)"
    shows "x1 * z1 * z2 * (-r1  y1 * z1) * x2 * (-r2  y2) = x1 * z1 * z2 * (y1 * z1 * (1  -q  x2)  -q  x2) * (-q  -r2  (y1 * z1 * (1  -q  x2)  -q  y2))"
proof -
  have 1: "preserves (y1 * z1 * (1  -q  x2)) (-r)"
    by (simp add: assms(7-9) ite_def preserves_mult preserves_sup preserves_test)
  hence 2: "preserves (y1 * z1 * (1  -q  x2)  -q  y2) (-r)"
    by (simp add: assms(10) preserves_ite)
  have "x1 * z1 * z2 * (-r1  y1 * z1) * x2 * (-r2  y2) = x1 * z1 * z2 * (-q  y1 * z1) * x2 * (-r2  y2)"
    using assms(1,5) mult_assoc while_seq_replace by auto
  also have "... = x1 * z1 * z2 * (-q  y1 * z1 * (1  -q  x2 * (-r2  y2))  -q  x2 * (-r2  y2))"
    by (smt assms(2,3) mult_assoc preserves_mult preserves_while while_post_norm)
  also have "... = x1 * z1 * (z2 * (-q  y1 * z1 * (1  -q  x2) * (--q * -r2  y2))  -q  z2 * x2 * (-r2  y2))"
    by (smt assms(2-4) assigns_same mult_assoc preserves_import_ite while_else_norm)
  also have "... = x1 * z1 * (z2 * (-r  y1 * z1 * (1  -q  x2)) * (-r * (-q  -r2)  (y1 * z1 * (1  -q  x2)  -q  y2))  -q  z2 * x2 * (-r2  y2))"
    by (smt assms(6-10) tests_dual.double_negation tests_dual.sub_sup_demorgan tests_dual.inf_demorgan preserves_ite preserves_mult preserves_one while_while_norm wnf_lemma_8)
  also have "... = x1 * z1 * z2 * ((-r  y1 * z1 * (1  -q  x2)) * (-r * (-q  -r2)  (y1 * z1 * (1  -q  x2)  -q  y2))  -r  x2 * (-r2  y2))"
    by (smt assms(4,6) mult_assoc preserves_import_ite while_ite_replace)
  also have "... = x1 * z1 * z2 * (-r * (y1 * z1 * (1  -q  x2)) * (-r * (-q  -r2)  (y1 * z1 * (1  -q  x2)  -q  y2))  -r  x2 * (-r2  y2))"
    by (smt mult_assoc it_context_true ite_import_true)
  also have "... = x1 * z1 * z2 * (-r * (y1 * z1 * (1  -q  x2)) * -r * (-r * (-q  -r2)  (y1 * z1 * (1  -q  x2)  -q  y2))  -r  x2 * (-r2  y2))"
    using 1 by (simp add: preserves_equation_test)
  also have "... = x1 * z1 * z2 * (-r * (y1 * z1 * (1  -q  x2)) * -r * (-q  -r2  (y1 * z1 * (1  -q  x2)  -q  y2))  -r  x2 * (-r2  y2))"
    using 2 by (smt (z3) tests_dual.sba_dual.sub_sup_closed mult_assoc preserves_while_context)
  also have "... = x1 * z1 * z2 * (y1 * z1 * (1  -q  x2) * (-q  -r2  (y1 * z1 * (1  -q  x2)  -q  y2))  -q  x2 * (-r2  y2))"
    by (smt assms(6-9) tests_dual.double_negation ite_import_true mult_assoc tests_dual.sup_idempotent preserves_equation_test preserves_ite preserves_one while_ite_replace)
  also have "... = x1 * z1 * z2 * (y1 * z1 * (1  -q  x2)  -r  x2) * ((-r * (-q  -r2)  --r * -r2)  ((y1 * z1 * (1  -q  x2)  -q  y2)  -r  y2))"
    by (smt assms(6-10) tests_dual.double_negation mult_assoc tests_dual.sub_sup_demorgan tests_dual.inf_demorgan preserves_ite preserves_mult preserves_one while_ite_norm)
  also have "... = x1 * z1 * z2 * (y1 * z1 * (1  -q  x2)  -r  x2) * ((-r * (-q  -r2)  --r * -r2)  (y1 * z1 * (1  -q  x2)  -r * -q  y2))"
    using ite_conjunction by simp
  also have "... = x1 * z1 * z2 * (y1 * z1 * (1  -q  x2)  -r  x2) * ((-r * -q  -r2)  (y1 * z1 * (1  -q  x2)  -r * -q  y2))"
    by (smt (z3) mult_left_dist_sup sup_assoc tests_dual.sba_dual.sup_cases tests_dual.sub_commutative)
  also have "... = x1 * z1 * z2 * (y1 * z1 * (1  -q  x2)  -q  x2) * (-q  -r2  (y1 * z1 * (1  -q  x2)  -q  y2))"
    using 1 by (metis assms(2,3,6,9,10) mult_assoc wnf_lemma_9)
  finally show ?thesis
    .
qed

end

end