1(* Title: Sequents/Modal0.thy 2 Author: Martin Coen 3 Copyright 1991 University of Cambridge 4*) 5 6theory Modal0 7imports LK0 8begin 9 10ML_file \<open>modal.ML\<close> 11 12consts 13 box :: "o\<Rightarrow>o" ("[]_" [50] 50) 14 dia :: "o\<Rightarrow>o" ("<>_" [50] 50) 15 Lstar :: "two_seqi" 16 Rstar :: "two_seqi" 17 18syntax 19 "_Lstar" :: "two_seqe" ("(_)|L>(_)" [6,6] 5) 20 "_Rstar" :: "two_seqe" ("(_)|R>(_)" [6,6] 5) 21 22ML \<open> 23 fun star_tr c [s1, s2] = Const(c, dummyT) $ seq_tr s1 $ seq_tr s2; 24 fun star_tr' c [s1, s2] = Const(c, dummyT) $ seq_tr' s1 $ seq_tr' s2; 25\<close> 26 27parse_translation \<open> 28 [(\<^syntax_const>\<open>_Lstar\<close>, K (star_tr \<^const_syntax>\<open>Lstar\<close>)), 29 (\<^syntax_const>\<open>_Rstar\<close>, K (star_tr \<^const_syntax>\<open>Rstar\<close>))] 30\<close> 31 32print_translation \<open> 33 [(\<^const_syntax>\<open>Lstar\<close>, K (star_tr' \<^syntax_const>\<open>_Lstar\<close>)), 34 (\<^const_syntax>\<open>Rstar\<close>, K (star_tr' \<^syntax_const>\<open>_Rstar\<close>))] 35\<close> 36 37definition strimp :: "[o,o]\<Rightarrow>o" (infixr "--<" 25) 38 where "P --< Q == [](P \<longrightarrow> Q)" 39 40definition streqv :: "[o,o]\<Rightarrow>o" (infixr ">-<" 25) 41 where "P >-< Q == (P --< Q) \<and> (Q --< P)" 42 43 44lemmas rewrite_rls = strimp_def streqv_def 45 46lemma iffR: "\<lbrakk>$H,P \<turnstile> $E,Q,$F; $H,Q \<turnstile> $E,P,$F\<rbrakk> \<Longrightarrow> $H \<turnstile> $E, P \<longleftrightarrow> Q, $F" 47 apply (unfold iff_def) 48 apply (assumption | rule conjR impR)+ 49 done 50 51lemma iffL: "\<lbrakk>$H,$G \<turnstile> $E,P,Q; $H,Q,P,$G \<turnstile> $E \<rbrakk> \<Longrightarrow> $H, P \<longleftrightarrow> Q, $G \<turnstile> $E" 52 apply (unfold iff_def) 53 apply (assumption | rule conjL impL basic)+ 54 done 55 56lemmas safe_rls = basic conjL conjR disjL disjR impL impR notL notR iffL iffR 57 and unsafe_rls = allR exL 58 and bound_rls = allL exR 59 60end 61