Quellcode-Bibliothek Modal0.thy

Sprache: Isabelle

(*  Title:      Sequents/Modal0.thy
    Author:     Martin Coen
    Copyright   1991  University of Cambridge
*)

theory Modal0
imports LK0
begin

ML_file ‹modal.ML›

consts
  box           :: "o==>o"       (‹[]_› [50] 50)
  dia           :: "o==>o"       (‹<>_› [50] 50)
  Lstar         :: "two_seqi"
  Rstar         :: "two_seqi"

syntax
  "_Lstar"      :: "two_seqe"   (‹(_)|L>(_)› [6,6] 5)
  "_Rstar"      :: "two_seqe"   (‹(_)|R>(_)› [6,6] 5)

ML ‹
fun star_tr c [s1, s2] = Syntax.const c $ seq_tr s1 $ seq_tr s2;
fun star_tr' c [s1, s2] = Syntax.const c $ seq_tr' s1 $ seq_tr' s2;
›

parse_translation ‹
[(🍋‹_Lstar›, K (star_tr 🍋‹Lstar›)),
(🍋‹_Rstar›, K (star_tr 🍋‹Rstar›))]
›

print_translation ‹
[(🍋‹Lstar›, K (star_tr' 🍋‹_Lstar›)),
(🍋‹Rstar›, K (star_tr' 🍋‹_Rstar›))]
›

definition strimp :: "[o,o]==>o"   (infixr ‹--<\<close> 25)
where "P --< Q == [](P ⟶ Q)"

streqv :: "[o,o]==>o" (infixr ‹>-<\<close> 25)
where "P >-< Q == (P --< Q) ∧ (Q --< P)"

rewrite_rls = strimp_def streqv_def

iffR: "[$H,P ⊨ $E,Q,$F; $H,Q ⊨ $E,P,$F] ==> $H ⊨ $E, P ⟷ Q, $F"
apply (unfold iff_def)
apply (assumption | rule conjR impR)+
done

iffL: "[$H,$G ⊨ $E,P,Q; $H,Q,P,$G ⊨ $E ] ==> $H, P ⟷ Q, $G ⊨ $E"
apply (unfold iff_def)
apply (assumption | rule conjL impL basic)+
done

safe_rls = basic conjL conjR disjL disjR impL impR notL notR iffL iffR
and unsafe_rls = allR exL
and bound_rls = allL exR

Messung V0.5 in Prozent

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.11Bemerkung: (vorverarbeitet am 2026-06-09) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.