| changeset 62144 | bdab93ccfaf8 |
| parent 61386 | 0a29a984a91b |
| child 69593 | 3dda49e08b9d |
| 62143:3c9a0985e6be | 62144:bdab93ccfaf8 |
|---|---|
10 ML_file "modal.ML" |
10 ML_file "modal.ML" |
11 |
11 |
12 consts |
12 consts |
13 box :: "o\<Rightarrow>o" ("[]_" [50] 50) |
13 box :: "o\<Rightarrow>o" ("[]_" [50] 50) |
14 dia :: "o\<Rightarrow>o" ("<>_" [50] 50) |
14 dia :: "o\<Rightarrow>o" ("<>_" [50] 50) |
15 strimp :: "[o,o]\<Rightarrow>o" (infixr "--<" 25) |
|
16 streqv :: "[o,o]\<Rightarrow>o" (infixr ">-<" 25) |
|
17 Lstar :: "two_seqi" |
15 Lstar :: "two_seqi" |
18 Rstar :: "two_seqi" |
16 Rstar :: "two_seqi" |
19 |
17 |
20 syntax |
18 syntax |
21 "_Lstar" :: "two_seqe" ("(_)|L>(_)" [6,6] 5) |
19 "_Lstar" :: "two_seqe" ("(_)|L>(_)" [6,6] 5) |
34 print_translation \<open> |
32 print_translation \<open> |
35 [(@{const_syntax Lstar}, K (star_tr' @{syntax_const "_Lstar"})), |
33 [(@{const_syntax Lstar}, K (star_tr' @{syntax_const "_Lstar"})), |
36 (@{const_syntax Rstar}, K (star_tr' @{syntax_const "_Rstar"}))] |
34 (@{const_syntax Rstar}, K (star_tr' @{syntax_const "_Rstar"}))] |
37 \<close> |
35 \<close> |
38 |
36 |
39 defs |
37 definition strimp :: "[o,o]\<Rightarrow>o" (infixr "--<" 25) |
40 strimp_def: "P --< Q == [](P \<longrightarrow> Q)" |
38 where "P --< Q == [](P \<longrightarrow> Q)" |
41 streqv_def: "P >-< Q == (P --< Q) \<and> (Q --< P)" |
39 |
40 definition streqv :: "[o,o]\<Rightarrow>o" (infixr ">-<" 25) |
|
41 where "P >-< Q == (P --< Q) \<and> (Q --< P)" |
|
42 |
42 |
43 |
43 |
44 lemmas rewrite_rls = strimp_def streqv_def |
44 lemmas rewrite_rls = strimp_def streqv_def |
45 |
45 |
46 lemma iffR: "\<lbrakk>$H,P \<turnstile> $E,Q,$F; $H,Q \<turnstile> $E,P,$F\<rbrakk> \<Longrightarrow> $H \<turnstile> $E, P \<longleftrightarrow> Q, $F" |
46 lemma iffR: "\<lbrakk>$H,P \<turnstile> $E,Q,$F; $H,Q \<turnstile> $E,P,$F\<rbrakk> \<Longrightarrow> $H \<turnstile> $E, P \<longleftrightarrow> Q, $F" |