--- a/src/Sequents/Modal0.thy Mon Nov 20 21:23:12 2006 +0100
+++ b/src/Sequents/Modal0.thy Mon Nov 20 23:47:10 2006 +0100
@@ -12,8 +12,8 @@
consts
box :: "o=>o" ("[]_" [50] 50)
dia :: "o=>o" ("<>_" [50] 50)
- "--<" :: "[o,o]=>o" (infixr 25)
- ">-<" :: "[o,o]=>o" (infixr 25)
+ strimp :: "[o,o]=>o" (infixr "--<" 25)
+ streqv :: "[o,o]=>o" (infixr ">-<" 25)
Lstar :: "two_seqi"
Rstar :: "two_seqi"
@@ -38,6 +38,23 @@
strimp_def: "P --< Q == [](P --> Q)"
streqv_def: "P >-< Q == (P --< Q) & (Q --< P)"
-ML {* use_legacy_bindings (the_context ()) *}
+
+lemmas rewrite_rls = strimp_def streqv_def
+
+lemma 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
+
+lemma 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
+
+lemmas safe_rls = basic conjL conjR disjL disjR impL impR notL notR iffL iffR
+ and unsafe_rls = allR exL
+ and bound_rls = allL exR
end