Theory KAT2
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 (ctxt |> put_simpset HOL_basic_ss |> Simplifier.add_simps 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)
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)
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