Theory DRAT2

(* Title:      Demonic refinement algebra
   Author:     Alasdair Armstrong, Victor B. F. Gomes, Georg Struth
   Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
*)

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 (put_simpset HOL_basic_ss ctxt addsimps 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`  `py  x`  `!py  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 "`px = pxq`  `px!q = 0`"
  nitpick oops

lemma test1: "`px!q = 0`  `px = pxq`"
  by (metis add_0_left distrib_left mult_oner test_comp_add1)

lemma test2: "`pqp = pq`"
  by (metis inf.commute inf.left_idem test_inf)

lemma test3: "`pq!p = 0`"
  by (metis inf.assoc inf.idem inf.left_commute inf_compl_bot test_bot test_inf test_not)

lemma test4: "`!pqp = 0`"
  by (metis double_compl test3 test_not)

lemma total_correctness: "`px!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: "`px  xp`  `px  xp`"
  by (metis iteration_sim)

lemma test_iteration_annir: "`!p(px) = !p`"
  by (metis annil iteration_idep mult.assoc test_comp_mult1)

end

end