| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Sequents/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 1 kB |
|
Quelle Modal0.thySprache: 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
¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet am 2026-06-09) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09