Theory DRAT2
section ‹Two sorted Demonic Refinement Algebras›
theory DRAT2
imports Kleene_Algebra.DRA
begin
text ‹
As an alternative to the one-sorted implementation of demonic refinement algebra with tests,
we provide a two-sorted, more conventional one.
This alternative can be developed further along the lines of the one-sorted implementation.
›
syntax "_dra" :: "'a ⇒ 'a" (‹`_`›)
ML ‹
val dra_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) dra_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 DRAHomRules = Named_Thms
(val name = @{binding "kat_hom"}
val description = "KAT test homomorphism rules")
fun dra_hom_tac ctxt n =
let
val rev_rules = map (fn thm => thm RS @{thm sym}) (DRAHomRules.get ctxt)
in
asm_full_simp_tac (ctxt |> put_simpset HOL_basic_ss |> Simplifier.add_simps rev_rules) n
end
›
setup ‹DRAHomRules.setup›
method_setup kat_hom = ‹
Scan.succeed (fn ctxt => SIMPLE_METHOD (CHANGED (dra_hom_tac ctxt 1)))
›
parse_ast_translation ‹
let
fun dra_tr ctxt [t] = map_ast_variables t
in [(@{syntax_const "_dra"}, dra_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
(dra_hom_tac ctxt n
THEN REPEAT (vcg' (VCGRules.get ctxt))
THEN dra_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 drat =
fixes test :: "'a::boolean_algebra ⇒ 'b::dra"
and not :: "'b::dra ⇒ 'b::dra" (‹!›)
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}) (DRAHomRules.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 test_comp_add1 [simp]: "`!p + p = 1`"
by kat_hom (metis compl_sup_top)
lemma test_comp_add2 [simp]: "`p + !p = 1`"
by kat_hom (metis sup_compl_top)
lemma test_comp_mult1 [simp]: "`!p ⋅ p = 0`"
by (metis inf.commute inf_compl_bot test_bot test_inf test_not)
lemma test_comp_mult2 [simp]: "`p ⋅ !p = 0`"
by (metis inf_compl_bot test_bot test_inf test_not)
lemma test_eq1: "`y ≤ x` ⟷ `p⋅y ≤ x` ∧ `!p⋅y ≤ x`"
apply standard
apply (metis mult_isol_var mult_onel test_not test_one_top)
apply (subgoal_tac "`(p + !p)⋅y ≤ x`")
apply (metis mult_onel sup_compl_top test_not test_sup test_top)
by (metis distrib_right' join.sup.bounded_iff)
lemma "`p⋅x = p⋅x⋅q` ⟹ `p⋅x⋅!q = 0`"
nitpick oops
lemma test1: "`p⋅x⋅!q = 0` ⟹ `p⋅x = p⋅x⋅q`"
by (metis add_0_left distrib_left mult_oner test_comp_add1)
lemma test2: "`p⋅q⋅p = p⋅q`"
by (metis inf.commute inf.left_idem test_inf)
lemma test3: "`p⋅q⋅!p = 0`"
by (metis inf.assoc inf.idem inf.left_commute inf_compl_bot test_bot test_inf test_not)
lemma test4: "`!p⋅q⋅p = 0`"
by (metis double_compl test3 test_not)
lemma total_correctness: "`p⋅x⋅!q = 0` ⟷ `x⋅!q ≤ !p⋅⊤`"
apply standard
apply (metis join.bot.extremum mult.assoc test_eq1 top_elim)
by (metis (no_types, opaque_lifting) add_zeror annil less_eq_def mult.assoc mult_isol test_comp_mult2)
lemma test_iteration_sim: "`p⋅x ≤ x⋅p` ⟹ `p⋅x⇧∞ ≤ x⇧∞⋅p`"
by (metis iteration_sim)
lemma test_iteration_annir: "`!p⋅(p⋅x)⇧∞ = !p`"
by (metis annil iteration_idep mult.assoc test_comp_mult1)
end
end