### new entry KAD

parent 06c5e4b99081
This diff is collapsed.
This diff is collapsed.
 (* Title: Modal Kleene Algebras Author: Victor B. F. Gomes, Walter Guttmann, Peter Höfner, Georg Struth, Tjark Weber Maintainer: Walter Guttmann Georg Struth Tjark Weber *) section {* Modal Kleene Algebras *} text {* This section studies laws that relate antidomain and antirange semirings and Kleene algebra, notably Galois connections and conjugations as those studied in~\cite{MoellerStruth,DesharnaisStruthSCP}. *} theory Modal_Kleene_Algebra imports Range_Semiring begin class modal_semiring = antidomain_semiring + antirange_semiring + assumes domrange [simp]: "d (r x) = r x" and rangedom [simp]: "r (d x) = d x" begin text {* These axioms force that the domain algebra and the range algebra coincide. *} lemma domrangefix: "d x = x \ r x = x" by (metis domrange rangedom) lemma box_diamond_galois_1: assumes "d p = p" and "d q = q" shows "\x| p \ q \ p \ |x] q" proof - have "\x| p \ q \ p \ x \ x \ q" by (metis assms domrangefix local.ardual.ds.fdemodalisation2 local.ars_r_def) thus ?thesis by (metis assms fbox_demodalisation3) qed lemma box_diamond_galois_2: assumes "d p = p" and "d q = q" shows "|x\ p \ q \ p \ [x| q" proof - have "|x\ p \ q \ x \ p \ q \ x" by (metis assms local.ads_d_def local.ds.fdemodalisation2) thus ?thesis by (metis assms domrangefix local.ardual.fbox_demodalisation3) qed lemma diamond_conjugation_var_1: assumes "d p = p" and "d q = q" shows "|x\ p \ ad q \ \x| q \ ad p" proof - have "|x\ p \ ad q \ x \ p \ ad q \ x" by (metis assms local.ads_d_def local.ds.fdemodalisation2) also have "... \ q \ x \ x \ ad p" by (metis assms local.ads_d_def local.kat_1_equiv_opp) finally show ?thesis by (metis assms box_diamond_galois_1 local.ads_d_def local.fbox_demodalisation3) qed lemma diamond_conjungation_aux: assumes "d p = p" and "d q = q" shows "\x| p \ ad q \ q \ \x| p = 0" apply standard apply (metis assms(2) local.a_antitone' local.a_gla local.ads_d_def) proof - assume a1: "q \ \x| p = zero_class.zero" have "ad (ad q) = q" using assms(2) local.ads_d_def by fastforce then show "\x| p \ ad q" using a1 by (metis (no_types) domrangefix local.a_gla local.ads_d_def local.antisym local.ardual.a_gla2 local.ardual.gla_1 local.ars_r_def local.bdia_def local.eq_refl) qed lemma diamond_conjugation: assumes "d p = p" and "d q = q" shows "p \ |x\ q = 0 \ q \ \x| p = 0" proof - have "p \ |x\ q = 0 \ |x\ q \ ad p" by (metis assms(1) local.a_gla local.ads_d_def local.am2 local.fdia_def) also have "... \ \x| p \ ad q" by (simp add: assms diamond_conjugation_var_1) finally show ?thesis by (simp add: assms diamond_conjungation_aux) qed lemma box_conjugation_var_1: assumes "d p = p" and "d q = q" shows "ad p \ [x| q \ ad q \ |x] p" by (metis assms box_diamond_galois_1 box_diamond_galois_2 diamond_conjugation_var_1 local.ads_d_def) lemma box_diamond_cancellation_1: "d p = p \ p \ |x] \x| p" using box_diamond_galois_1 domrangefix local.ars_r_def local.bdia_def by fastforce lemma box_diamond_cancellation_2: "d p = p \ p \ [x| |x\ p" by (metis box_diamond_galois_2 local.ads_d_def local.dpdz.domain_invol local.eq_refl local.fdia_def) lemma box_diamond_cancellation_3: "d p = p \ |x\ [x| p \ p" using box_diamond_galois_2 domrangefix local.ardual.fdia_fbox_de_morgan_2 local.ars_r_def local.bbox_def local.bdia_def by auto lemma box_diamond_cancellation_4: "d p = p \ \x| |x] p \ p" using box_diamond_galois_1 local.ads_d_def local.fbox_def local.fdia_def local.fdia_fbox_de_morgan_2 by auto end class modal_kleene_algebra = modal_semiring + kleene_algebra begin subclass antidomain_kleene_algebra .. subclass antirange_kleene_algebra .. end end
This diff is collapsed.
 (* Title: Models of Modal Kleene Algebras Author: Victor B. F. Gomes, Walter Guttmann, Peter Höfner, Georg Struth, Tjark Weber Maintainer: Walter Guttmann Georg Struth Tjark Weber *) section {* Models of Modal Kleene Algebras *} theory Modal_Kleene_Algebra_Models imports "../Kleene_Algebra/Kleene_Algebra_Models" Modal_Kleene_Algebra begin text {* This section develops the relation model. We also briefly develop the trace model for antidomain Kleene algebras, but not for antirange or full modal Kleene algebras. The reason is that traces are implemented as lists; we therefore expect tedious inductive proofs in the presence of range. The language model is not particularly interesting. *} definition rel_ad :: "'a rel \ 'a rel" where "rel_ad R = {(x,x) | x. \ (\y. (x,y) \ R)}" interpretation rel_antidomain_kleene_algebra: antidomain_kleene_algebra rel_ad "op \" "op O" Id "{}" "op \" "op \" rtrancl by unfold_locales (auto simp: rel_ad_def) definition trace_a :: "('p, 'a) trace set \ ('p, 'a) trace set" where "trace_a X = {(p,[]) | p. \ (\x. x \ X \ p = first x)}" interpretation trace_antidomain_kleene_algebra: antidomain_kleene_algebra trace_a "op \" t_prod t_one t_zero "op \" "op \" t_star proof show "\x. t_prod (trace_a x) x = t_zero" by (auto simp: trace_a_def t_prod_def t_fusion_def t_zero_def) show "\x y. trace_a (t_prod x y) \ trace_a (t_prod x (trace_a (trace_a y))) = trace_a (t_prod x (trace_a (trace_a y)))" by (auto simp: trace_a_def t_prod_def t_fusion_def) show "\x. trace_a (trace_a x) \ trace_a x = t_one" by (auto simp: trace_a_def t_one_def) qed text {* The trace model should be extended to cover modal Kleene algebras in the future. *} definition rel_ar :: "'a rel \ 'a rel" where "rel_ar R = {(y,y) | y. \ (\x. (x,y) \ R)}" interpretation rel_antirange_kleene_algebra: antirange_semiring "op \" "op O" Id "{}" rel_ar "op \" "op \" apply unfold_locales apply (simp_all add: rel_ar_def) by auto interpretation rel_modal_kleene_algebra: modal_kleene_algebra "op \" "op O" Id "{}" "op \" "op \" rtrancl rel_ad rel_ar apply standard apply (metis (no_types, lifting) rel_antidomain_kleene_algebra.a_d_closed rel_antidomain_kleene_algebra.a_one rel_antidomain_kleene_algebra.addual.ars_r_def rel_antidomain_kleene_algebra.am5_lem rel_antidomain_kleene_algebra.am6_lem rel_antidomain_kleene_algebra.apd_d_def rel_antidomain_kleene_algebra.dka.dns1 rel_antidomain_kleene_algebra.dpdz.dom_one rel_antirange_kleene_algebra.ardual.a_comm' rel_antirange_kleene_algebra.ardual.a_d_closed rel_antirange_kleene_algebra.ardual.a_mul_d' rel_antirange_kleene_algebra.ardual.a_mult_idem rel_antirange_kleene_algebra.ardual.a_zero rel_antirange_kleene_algebra.ardual.ads_d_def rel_antirange_kleene_algebra.ardual.am6_lem rel_antirange_kleene_algebra.ardual.apd_d_def rel_antirange_kleene_algebra.ardual.s4) by (metis rel_antidomain_kleene_algebra.a_zero rel_antidomain_kleene_algebra.addual.ars1 rel_antidomain_kleene_algebra.addual.ars_r_def rel_antidomain_kleene_algebra.am5_lem rel_antidomain_kleene_algebra.am6_lem rel_antidomain_kleene_algebra.ds.ddual.mult_oner rel_antidomain_kleene_algebra.s4 rel_antirange_kleene_algebra.ardual.ads_d_def rel_antirange_kleene_algebra.ardual.am6_lem rel_antirange_kleene_algebra.ardual.apd1 rel_antirange_kleene_algebra.ardual.dpdz.dns1'') end
thys/KAD/ROOT 0 → 100644
 chapter AFP session "KAD" (AFP) = "HOL" + options [timeout = 600] theories [document = false] "../Kleene_Algebra/Kleene_Algebra" "../Kleene_Algebra/Kleene_Algebra_Models" theories Domain_Semiring Antidomain_Semiring Range_Semiring Modal_Kleene_Algebra Modal_Kleene_Algebra_Models Modal_Kleene_Algebra_Applications document_files "root.bib" "root.tex"
 (* Title: Range and Antirange Semirings Author: Victor B. F. Gomes, Walter Guttmann, Peter Höfner, Georg Struth, Tjark Weber Maintainer: Walter Guttmann Georg Struth Tjark Weber *) section {* Range and Antirange Semirings *} theory Range_Semiring imports Antidomain_Semiring begin subsection {* Range Semirings *} text {* We set up the duality between domain and antidomain semirings on the one hand and range and antirange semirings on the other hand. *} class range_op = fixes range_op :: "'a \ 'a" ("r") class range_semiring = semiring_one_zero + plus_ord + range_op + assumes rsr1 [simp]: "x + (x \ r x) = x \ r x" and rsr2 [simp]: "r (r x \ y) = r(x \ y)" and rsr3 [simp]: "r x + 1 = 1" and rsr4 [simp]: "r 0 = 0" and rsr5 [simp]: "r (x + y) = r x + r y" begin definition bd :: "'a \ 'a \ 'a" ("\_| _" [61,81] 82) where "\x| y = r (y \ x)" no_notation range_op ("r") end sublocale range_semiring \ rdual: domain_semiring "op +" "\x y. y \ x" 1 0 range_op "op \" "op <" rewrites "rdual.fd x y = \x| y" proof - show "class.domain_semiring op + (\x y. y \ x) 1 0 range_op op \ op <" by (standard, auto simp: mult_assoc distrib_left) then interpret rdual: domain_semiring "op +" "\x y. y \ x" 1 0 range_op "op \" "op <" . show "rdual.fd x y = \x| y" unfolding rdual.fd_def bd_def by auto qed sublocale domain_semiring \ ddual: range_semiring "op +" "\x y. y \ x" 1 0 domain_op "op \" "op <" rewrites "ddual.bd x y = domain_semiringl_class.fd x y" proof - show "class.range_semiring op + (\x y. y \ x) 1 0 domain_op op \ op <" by (standard, auto simp: mult_assoc distrib_left) then interpret ddual: range_semiring "op +" "\x y. y \ x" 1 0 domain_op "op \" "op <" . show "ddual.bd x y = domain_semiringl_class.fd x y" unfolding ddual.bd_def fd_def by auto qed subsection {* Antirange Semirings *} class antirange_op = fixes antirange_op :: "'a \ 'a" ("ar _"  1000) class antirange_semiring = semiring_one_zero + plus_ord + antirange_op + assumes ars1 [simp]: "x \ ar x = 0" and ars2 [simp]: "ar (x \ y) + ar (ar ar x \ y) = ar (ar ar x \ y)" and ars3 [simp]: "ar ar x + ar x = 1" begin no_notation bd ("\_| _" [61,81] 82) definition ars_r :: "'a \ 'a" ("r") where "r x = ar (ar x)" definition bdia :: "'a \ 'a \ 'a" ("\_| _" [61,81] 82) where "\x| y = ar ar (y \ x)" definition bbox :: "'a \ 'a \ 'a" ("[_| _" [61,81] 82) where "[x| y = ar (ar y \ x)" end sublocale antirange_semiring \ ardual: antidomain_semiring antirange_op "op +" "\x y. y \ x" 1 0 "op \" "op <" rewrites "ardual.ads_d x = r x" and "ardual.fdia x y = \x| y" and "ardual.fbox x y = [x| y" proof - show "class.antidomain_semiring antirange_op op + (\x y. y \ x) 1 0 op \ op <" by (standard, auto simp: mult_assoc distrib_left) then interpret ardual: antidomain_semiring antirange_op "op +" "\x y. y \ x" 1 0 "op \" "op <" . show "ardual.ads_d x = r x" by (simp add: ardual.ads_d_def local.ars_r_def) show "ardual.fdia x y = \x| y" unfolding ardual.fdia_def bdia_def by auto show "ardual.fbox x y = [x| y" unfolding ardual.fbox_def bbox_def by auto qed context antirange_semiring begin sublocale rs: range_semiring "op +" "op \" 1 0 "\x. ar ar x" "op \" "op <" by unfold_locales end sublocale antidomain_semiring \ addual: antirange_semiring "op +" "\x y. y \ x" 1 0 antidomain_op "op \" "op <" rewrites "addual.ars_r x = d x" and "addual.bdia x y = |x\ y" and "addual.bbox x y = |x] y" proof - show "class.antirange_semiring op + (\x y. y \ x) 1 0 antidomain_op op \ op <" by (standard, auto simp: mult_assoc distrib_left) then interpret addual: antirange_semiring "op +" "\x y. y \ x" 1 0 antidomain_op "op \" "op <" . show "addual.ars_r x = d x" by (simp add: addual.ars_r_def local.ads_d_def) show "addual.bdia x y = |x\ y" unfolding addual.bdia_def fdia_def by auto show "addual.bbox x y = |x] y" unfolding addual.bbox_def fbox_def by auto qed subsection {* Antirange Kleene Algebras *} class antirange_kleene_algebra = antirange_semiring + kleene_algebra sublocale antirange_kleene_algebra \ dual: antidomain_kleene_algebra antirange_op "op +" "\x y. y \ x" 1 0 "op \" "op <" "star" by (standard, auto simp: local.star_inductr' local.star_inductl) sublocale antidomain_kleene_algebra \ dual: antirange_kleene_algebra "op +" "\x y. y \ x" 1 0 "op \" "op <" "star" antidomain_op by (standard, simp_all add: star_inductr star_inductl) text {* Hence all range theorems have been derived by duality in a generic way. *} end
thys/KAD/config 0 → 100644
 # -*- shell-script -*- # Get email when automated build fails. May be empty. # values: "email1 email2 .. emailn" NOTIFY="walter.guttman@canterbury.ac.nz g.struth@sheffield.ac.uk tjark.weber@it.uu.se" # Participate in frequent (nightly) build (only for small submissions) # values: "yes" "no" FREQUENT="yes"
 @inproceedings{DesharnaisJipsenStruth, author = {Desharnais, J. and Jipsen, P. and Struth, G.}, title = {Domain and Antidomain Semigroups}, booktitle = {Relations and {Kleene} Algebra in Computer Science}, editor = {Berghammer, R. and Jaoua, A. and M{\"{o}}ller, B.}, series = {Lecture Notes in Computer Science}, volume = {5827}, publisher = {Springer}, year = {2009}, pages = {73--87}, year = {2009} } @article{DesharnaisMoellerStruthLMCS, author = {Desharnais, J. and M{\"{o}}ller, B. and Struth, G.}, title = {Algebraic Notions of Termination}, journal = {Logical Methods in Computer Science}, volume = {7}, number = {1}, year = {2011} } @inproceedings{DesharnaisStruthAMAST, author = {Desharnais, J. and Struth, G.}, title = {Domain Axioms for a Family of Near-Semirings}, booktitle = {{AMAST} 2008}, pages = {330--345}, year = {2008}, editor = {Meseguer, J. and Rosu, G.}, series = {Lecture Notes in Computer Science}, volume = {5140}, publisher = {Springer}, year = {2008} } @article{DesharnaisStruthSCP, author = {Desharnais, J. and Struth, G.}, title = {Internal axioms for domain semirings}, journal = {Science of Computer Programming}, volume = {76}, number = {3}, pages = {181--203}, year = {2011} } @article{FurusawaStruth, author = {Furusawa, H. and Struth, G.}, title = {Concurrent Dynamic Algebra}, journal = {{ACM} {TOCL}}, volume = {16}, number = {4}, pages = {30}, year = {2015} } @article{MoellerStruth, author = {M{\"{o}}ller, B. and Struth, G.}, title = {Algebras of modal operators and partial correctness}, journal = {Theoretical Computer Science}, volume = {351}, number = {2}, pages = {221--239}, year = {2006} } @article{Solin11, author = {Solin, K.}, title = {Normal forms in total correctness for while programs and action systems}, journal = {J.\ Logic and Algebraic Programming}, volume = {80}, number = {6}, year = {2011}, pages = {362--375} } @inproceedings{armstrongstruth12hoka, author = {Alasdair Armstrong and Georg Struth}, title = {Automated Reasoning in Higher-Order Regular Algebra}, booktitle = {{RAMICS} 2012}, year = {2012}, pages = {66-81}, ee = {http://dx.doi.org/10.1007/978-3-642-33314-9_5}, editor = {Wolfram Kahl and Timothy G. Griffin}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {7560} } @inproceedings{bachmair86commutation, author = {Leo Bachmair and Nachum Dershowitz}, title = {Commutation, Transformation, and Termination}, editor = {J{\"o}rg H. Siekmann}, booktitle = {Conference on Automated Deduction}, volume = {230}, series = {Lecture Notes in Computer Science}, pages = {5--20}, publisher = {Springer}, year = {1986}, ee = {http://dx.doi.org/10.1007/3-540-16780-3_76} } @book{birkhoff67lattices, author = {Garrett Birkhoff}, title = {Lattice Theory}, publisher = {American Mathematical Society Colloquium Publications}, year = {1967} } @article{boffa90remarque, author = {Maurice Boffa}, title = {Une remarque sur les syst\`emes complets d'identit\'es rationnelles}, journal = {Informatique The\'eorique et Applications}, year = {1990}, volume = {24}, number = {4}, pages = {419--423} } @inproceedings{cohen00omega, author = {Ernie Cohen}, title = {Separation and Reduction}, booktitle = {MPC}, year = {2000}, pages = {45--59}, ee = {http://dx.doi.org/10.1007/10722010_4}, editor = {Roland Carl Backhouse and Jos{\'e} Nuno Oliveira}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {1837} } @book{conway71regular, author = {Conway, John Horton}, title = {Regular Algebra and Finite Machines}, publisher = {Chapman and Hall}, year = {1971} } @inproceedings{dershowitz09lazy, author = {Nachum Dershowitz}, title = {On Lazy Commutation}, editor = {Orna Grumberg and Michael Kaminski and Shmuel Katz and Shuly Wintner}, booktitle = {Languages: From Formal to Natural}, volume = {5533}, series = {Lecture Notes in Computer Science}, pages = {59--82}, publisher = {Springer}, year = {2009}, ee = {http://dx.doi.org/10.1007/978-3-642-01748-3_5} } @article{desharnaismoellerstruth06kad, author = {Jules Desharnais and Bernhard M{\"o}ller and Georg Struth}, title = {{Kleene} Algebra with Domain}, journal = {ACM {TOCL}}, volume = {7}, number = {4}, year = {2006}, pages = {798-833}, ee = {http://doi.acm.org/10.1145/1183278.1183285} } @article{doornbos97calculational, author = {Henk Doornbos and Roland Carl Backhouse and Jaap van der Woude}, title = {A Calculational Approach to Mathematical Induction}, journal = {Theoretical Computer Science}, volume = {179}, number = {1--2}, year = {1997}, pages = {103--135}, ee = {http://dx.doi.org/10.1016/S0304-3975(96)00154-5} } @inproceedings{fosterstruth12regalg, author = {Simon Foster and Georg Struth}, title = {Automated Analysis of Regular Algebra}, booktitle = {{IJCAR} 2012}, year = {2012}, pages = {271--285}, ee = {http://dx.doi.org/10.1007/978-3-642-31365-3_22}, editor = {Bernhard Gramlich and Dale Miller and Uli Sattler}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {7364} } @inproceedings{fosterstruthweber11tutorial, author = {Simon Foster and Georg Struth and Tjark Weber}, title = {Automated Engineering of Relational and Algebraic Methods in {Isabelle}/{HOL} -- (Invited Tutorial)}, booktitle = {{RAMICS}}, year = {2011}, editor = {Harrie C. M. de Swart}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {6663}, pages = {52--67}, ee = {http://dx.doi.org/10.1007/978-3-642-21070-9_5} } @book{galatosjipsenkowalskiono07residuated, author = {Nikolaos Galatos and Peter Jipsen and Tomasz Kowalski and Hiroakira Ono}, title = {Resituated Lattices: An Algebraic Glimpse at Substructural Logics}, publisher = {Elsevier}, year = {2007} } @book{gondran10graphs, author = {Michel Gondran and Michel Minoux}, title = {Graphs, Dioids and Semirings: New Models and Algorithms}, volume = {41}, series = {Operations Research/Computer Science Interfaces}, publisher = {Springer}, year = {2010} } @inproceedings{guttmannstruthweber11algmeth, author = {Walter Guttmann and Georg Struth and Tjark Weber}, title = {Automating Algebraic Methods in {Isabelle}}, booktitle = {{ICFEM} 2011}, year = {2011}, pages = {617-632}, ee = {http://dx.doi.org/10.1007/978-3-642-24559-6_41}, editor = {Shengchao Qin and Zongyan Qiu}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {6991} } @inproceedings{guttmannstruthweber11tarskikleene, author = {Walter Guttmann and Georg Struth and Tjark Weber}, title = {A Repository for {Tarski}-{Kleene} Algebras}, booktitle = {{ATE} 2011}, year = {2011}, pages = {30--39}, ee = {http://ceur-ws.org/Vol-760/paper5.pdf}, editor = {Peter H{\"o}fner and Annabelle McIver and Georg Struth}, publisher = {CEUR-WS.org}, series = {CEUR Workshop Proceedings}, volume = {760} } @book{harelkozentiuryn00dynamic, author = {David Haren and Dexter Kozen and Jerzy Tiuryn}, title = {Dynamic Logic}, publisher = {MIT Press}, year = {2000} } @article{hofnerstruth10nontermination, author = {Peter H{\"o}fner and Georg Struth}, title = {Algebraic notions of nontermination: Omega and divergence in idempotent semirings}, journal = {J.\ Log.\ Algebr.\ Program.}, volume = {79}, number = {8}, year = {2010}, pages = {794-811}, ee = {http://dx.doi.org/10.1016/j.jlap.2010.07.016} } @article{ka, author = {Armstrong, A. and Gomes, Victor B. F. and Struth, G. and Weber, T.}, title = {{Kleene} Algebra}, journal = {Archive of Formal Proofs}, year = {2013} } @article{kat, author = {Armstrong, A. and Gomes, Victor B. F. and Struth, G.}, title = {Kleene Algebra with Tests}, journal = {Archive of Formal Proofs}, year = {2014} } @article{kad, author = {Gomes, Victor B. F. and Guttmann, W. and H{\"o}fner, P. and Struth, G. and Weber, T.}, title = {Kleene Algebra with Domain},