Theory KAT2

(* Title:      Kleene Algebra with Tests
   Author:     Alasdair Armstrong, Victor B. F. Gomes, Georg Struth
   Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
*)

section ‹Two sorted Kleene Algebra with Tests›

theory KAT2
  imports Kleene_Algebra.Kleene_Algebra
begin

text ‹
  As an alternative to the one-sorted implementation of tests, we provide a two-sorted, more 
  conventional one. In this setting, Isabelle's Boolean algebra theory can be used.
  This alternative can be developed further along the lines of the one-sorted implementation.
›

syntax "_kat" :: "'a ⇒ 'a" ("`_`")

ML ‹
val kat_test_vars = ["p","q","r","s","t","p'","q'","r'","s'","t'","p''","q''","r''","s''","t''"]

fun map_ast_variables ast =
  case ast of
    (Ast.Variable v) =>
      if exists (fn tv => tv = v) kat_test_vars
      then Ast.Appl [Ast.Variable "test", Ast.Variable v]
      else Ast.Variable v
  | (Ast.Constant c) => Ast.Constant c
  | (Ast.Appl []) => Ast.Appl []
  | (Ast.Appl (f :: xs)) => Ast.Appl (f :: map map_ast_variables xs)

structure KATHomRules = Named_Thms
  (val name = @{binding "kat_hom"}
   val description = "KAT test homomorphism rules")

fun kat_hom_tac ctxt n =
  let
    val rev_rules = map (fn thm => thm RS @{thm sym}) (KATHomRules.get ctxt)
  in
    asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps rev_rules) n
  end
›

setup ‹KATHomRules.setup›

method_setup kat_hom = ‹
Scan.succeed (fn ctxt => SIMPLE_METHOD (CHANGED (kat_hom_tac ctxt 1)))
›

parse_ast_translation ‹
let
  fun kat_tr ctxt [t] = map_ast_variables t
in [(@{syntax_const "_kat"}, kat_tr)] end
›

ML ‹
structure VCGRules = Named_Thms
  (val name = @{binding "vcg"}
   val description = "verification condition generator rules")

fun vcg_tac ctxt n =
  let
    fun vcg' [] = no_tac
      | vcg' (r :: rs) = resolve_tac ctxt [r] n ORELSE vcg' rs;
  in REPEAT (CHANGED
       (kat_hom_tac ctxt n
        THEN REPEAT (vcg' (VCGRules.get ctxt))
        THEN kat_hom_tac ctxt n
        THEN TRY (resolve_tac ctxt @{thms order_refl} n ORELSE asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) n)))
  end
›

method_setup vcg = ‹
Scan.succeed (fn ctxt => SIMPLE_METHOD (CHANGED (vcg_tac ctxt 1)))
›

setup ‹VCGRules.setup›

locale dioid_tests =
  fixes test :: "'a::boolean_algebra ⇒ 'b::dioid_one_zerol"
  and not :: "'b::dioid_one_zerol ⇒ 'b::dioid_one_zerol" ("-")
  assumes test_sup [simp,kat_hom]: "test (sup p q) = `p + q`"
  and test_inf [simp,kat_hom]: "test (inf p q) = `p ⋅ q`"
  and test_top [simp,kat_hom]: "test top = 1"
  and test_bot [simp,kat_hom]: "test bot = 0"
  and test_not [simp,kat_hom]: "test (- p) = `-p`"
  and test_iso_eq [kat_hom]: "p ≤ q ⟷ `p ≤ q`"
begin

notation test ("ι")

lemma test_eq [kat_hom]: "p = q ⟷ `p = q`"
  by (metis eq_iff test_iso_eq)

ML_val ‹map (fn thm => thm RS @{thm sym}) (KATHomRules.get @{context})›

lemma test_iso: "p ≤ q ⟹ `p ≤ q`"
  by (simp add: test_iso_eq)

(* Import lemmas and modify them to fit KAT syntax *)

lemma test_meet_comm: "`p ⋅ q = q ⋅ p`"
  by kat_hom (fact inf_commute)

lemmas test_one_top[simp] = test_iso[OF top_greatest, simplified]

lemma [simp]: "`-p + p = 1`"
  by kat_hom (metis compl_sup_top)

lemma [simp]: "`p + (-p) = 1`"
  by kat_hom (metis sup_compl_top)

lemma [simp]: "`(-p) ⋅ p = 0`"
  by (metis inf.commute inf_compl_bot test_bot test_inf test_not)

lemma [simp]: "`p ⋅ (-p) = 0`"
  by (metis inf_compl_bot test_bot test_inf test_not)

end

locale kat = 
  fixes test :: "'a::boolean_algebra ⇒ 'b::kleene_algebra"
  and not :: "'b::kleene_algebra ⇒ 'b::kleene_algebra" ("!")
  assumes is_dioid_tests: "dioid_tests test not"

sublocale kat ⊆ dioid_tests using is_dioid_tests .

context kat
begin

notation test ("ι")

lemma test_eq [kat_hom]: "p = q ⟷ `p = q`"
  by (metis eq_iff test_iso_eq)

ML_val ‹map (fn thm => thm RS @{thm sym}) (KATHomRules.get @{context})›

lemma test_iso: "p ≤ q ⟹ `p ≤ q`"
  by (simp add: test_iso_eq)

(* Import lemmas and modify them to fit KAT syntax *)

lemma test_meet_comm: "`p ⋅ q = q ⋅ p`"
  by kat_hom (fact inf_commute)

lemmas test_one_top[simp] = test_iso[OF top_greatest, simplified]

lemma test_star [simp]: "`p⇧⋆ = 1`"
  by (metis star_subid test_iso test_top top_greatest)

lemmas [kat_hom] = test_star[symmetric]

lemma [simp]: "`!p + p = 1`"
  by kat_hom (metis compl_sup_top)

lemma [simp]: "`p + !p = 1`"
  by kat_hom (metis sup_compl_top)

lemma [simp]: "`!p ⋅ p = 0`"
  by (metis inf.commute inf_compl_bot test_bot test_inf test_not)

lemma [simp]: "`p ⋅ !p = 0`"
  by (metis inf_compl_bot test_bot test_inf test_not)

definition hoare_triple :: "'b ⇒ 'b ⇒ 'b ⇒ bool" ("⦃_⦄ _ ⦃_⦄") where
  "⦃p⦄ c ⦃q⦄ ≡ p⋅c ≤ c⋅q"

declare hoare_triple_def[iff]

lemma hoare_triple_def_var: "`p⋅c ≤ c⋅q ⟷ p⋅c⋅!q = 0`"
  apply (intro iffI antisym)
  apply (rule order_trans[of _ "`c ⋅ q ⋅ !q`"])
  apply (rule mult_isor[rule_format])
  apply (simp add: mult.assoc)+
  apply (simp add: mult.assoc[symmetric])
  apply (rule order_trans[of _ "`p⋅c⋅(!q + q)`"])
  apply simp
  apply (simp only: distrib_left add_zerol)
  apply (rule order_trans[of _ "`1 ⋅ c ⋅ q`"])
  apply (simp only: mult.assoc)
  apply (rule mult_isor[rule_format])
  by simp_all

lemmas [intro!] = star_sim2[rule_format]

lemma hoare_weakening: "p ≤ p' ⟹ q' ≤ q ⟹ `⦃p'⦄ c ⦃q'⦄` ⟹ `⦃p⦄ c ⦃q⦄`"
  by auto (metis mult_isol mult_isor order_trans test_iso)

lemma hoare_star: "`⦃p⦄ c ⦃p⦄` ⟹ `⦃p⦄ c⇧⋆ ⦃p⦄`"
  by auto

lemmas [vcg] = hoare_weakening[OF order_refl _ hoare_star]

lemma hoare_test [vcg]: "`p ⋅ t ≤ q` ⟹ `⦃p⦄ t ⦃q⦄`"
  by auto (metis inf_le2 le_inf_iff test_inf test_iso_eq)

lemma hoare_mult [vcg]: "`⦃p⦄ x ⦃r⦄` ⟹ `⦃r⦄ y ⦃q⦄` ⟹ `⦃p⦄ x⋅y ⦃q⦄`"
proof auto
  assume [simp]: "`p ⋅ x ≤ x ⋅ r`" and [simp]: "`r ⋅ y ≤ y ⋅ q`"
  have "`p ⋅ (x ⋅ y) ≤ x ⋅ r ⋅ y`"
    by (auto simp add: mult.assoc[symmetric] intro!: mult_isor[rule_format])
  also have "`... ≤ x ⋅ y ⋅ q`"
    by (auto simp add: mult.assoc intro!: mult_isol[rule_format])
  finally show "`p ⋅ (x ⋅ y) ≤ x ⋅ y ⋅ q`" .
qed

lemma [simp]: "`!p ⋅ !p = !p`"
  by (metis inf.idem test_inf test_not)

lemma hoare_plus [vcg]: "`⦃p⦄ x ⦃q⦄` ⟹ `⦃p⦄ y ⦃q⦄` ⟹ `⦃p⦄ x + y ⦃q⦄`"
proof -
  assume a1: "⦃ι p⦄ x ⦃ι q⦄"
  assume "⦃ι p⦄ y ⦃ι q⦄"
  hence "ι p ⋅ (x + y) ≤ x ⋅ ι q + y ⋅ ι q"
    using a1 by (metis (no_types) distrib_left hoare_triple_def join.sup.mono)
  thus ?thesis
    by force
qed

definition While :: "'b ⇒ 'b ⇒ 'b" ("While _ Do _ End" [50,50] 51) where
  "While t Do c End = (t⋅c)⇧⋆⋅!t"

lemma hoare_while: "`⦃p ⋅ t⦄ c ⦃p⦄` ⟹ `⦃p⦄ While t Do c End ⦃!t ⋅ p⦄`"
  unfolding While_def by vcg (metis inf_commute order_refl)

lemma [vcg]: "`⦃p ⋅ t⦄ c ⦃p⦄` ⟹ `!t ⋅ p ≤ q` ⟹ `⦃p⦄ While t Do c End ⦃q⦄`"
  by (metis hoare_weakening hoare_while order_refl test_inf test_iso_eq test_not)

definition If :: "'b ⇒ 'b ⇒ 'b ⇒ 'b" ("If _ Then _ Else _" [50,50,50] 51) where
  "If p Then c1 Else c2 ≡ p⋅c1 + !p⋅c2"

lemma hoare_if [vcg]: "`⦃p ⋅ t⦄ c1 ⦃q⦄` ⟹ `⦃p ⋅ !t⦄ c2 ⦃q⦄` ⟹ `⦃p⦄ If t Then c1 Else c2 ⦃q⦄`"
  unfolding If_def by vcg assumption

end

end