Commit 5e67b770 authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files

Fixed a very slow step

parent d320adc2c11c
......@@ -1975,6 +1975,24 @@ abstract =
in KAT and its relational model and present a simple formally verified
program verification tool prototype based on the algebraic approach.
title = Kleene Algebras with Domain
author = Victor B. F. Gomes, Walter Guttmann, Peter Höfner, Georg Struth, Tjark Weber
date = 2016-04-12
topic = Automata and Formal Languages; Programming Languages (Logics); Algebra
abstract =
Kleene algebras with domain are Kleene algebras endowed with an
operation that maps each element of the algebra to its domain of
definition (or its complement) in abstract fashion. They form a simple
algebraic basis for Hoare logics, dynamic logics or predicate
transformer semantics. We formalise a modular hierarchy of algebras
with domain and antidomain (domain complement) operations in
Isabelle/HOL that ranges from domain and antidomain semigroups to
modal Kleene algebras and divergence Kleene algebras. We link these
algebras with models of binary relations and program traces. We
include some examples from modal logics, termination and program
title = Regular Algebras
author = Simon Foster <>, Georg Struth <>
......@@ -39,11 +39,11 @@ by (metis omega.cases)
lemma omega_coinduct: "X x z \<Longrightarrow>
(\<And>x z. X x z \<Longrightarrow> \<exists>y. (x, y) \<in> R \<and> (X y z \<or> (y, z) \<in> omega R)) \<Longrightarrow>
(x, z) \<in> omega R"
by (metis omega.coinduct)
by (metis (full_types) omega.coinduct)
lemma omega_weak_coinduct: "X x z \<Longrightarrow>
(\<And>x z. X x z \<Longrightarrow> \<exists>y. (x, y) \<in> R \<and> X y z) \<Longrightarrow>
(x, z) \<in> omega R"
(x, z) \<in> omega R"
by (metis omega.coinduct)
lemma context_conjI_R:
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment