author  wenzelm 
Sat, 10 Oct 2015 20:51:39 +0200  
changeset 61385  538100cc4399 
parent 60770  240563fbf41d 
child 61386  0a29a984a91b 
permissions  rwrr 
17481  1 
(* Title: Sequents/Modal0.thy 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

2 
Author: Martin Coen 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

3 
Copyright 1991 University of Cambridge 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

4 
*) 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

5 

17481  6 
theory Modal0 
7 
imports LK0 

8 
begin 

2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

9 

48891  10 
ML_file "modal.ML" 
11 

2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

12 
consts 
61385  13 
box :: "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) 

17481  17 
Lstar :: "two_seqi" 
18 
Rstar :: "two_seqi" 

14765  19 

20 
syntax 

35113  21 
"_Lstar" :: "two_seqe" ("(_)L>(_)" [6,6] 5) 
22 
"_Rstar" :: "two_seqe" ("(_)R>(_)" [6,6] 5) 

2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

23 

60770  24 
ML \<open> 
35113  25 
fun star_tr c [s1, s2] = Const(c, dummyT) $ seq_tr s1 $ seq_tr s2; 
26 
fun star_tr' c [s1, s2] = Const(c, dummyT) $ seq_tr' s1 $ seq_tr' s2; 

60770  27 
\<close> 
17481  28 

60770  29 
parse_translation \<open> 
52143  30 
[(@{syntax_const "_Lstar"}, K (star_tr @{const_syntax Lstar})), 
31 
(@{syntax_const "_Rstar"}, K (star_tr @{const_syntax Rstar}))] 

60770  32 
\<close> 
35113  33 

60770  34 
print_translation \<open> 
52143  35 
[(@{const_syntax Lstar}, K (star_tr' @{syntax_const "_Lstar"})), 
36 
(@{const_syntax Rstar}, K (star_tr' @{syntax_const "_Rstar"}))] 

60770  37 
\<close> 
17481  38 

39 
defs 

61385  40 
strimp_def: "P < Q == [](P \<longrightarrow> Q)" 
41 
streqv_def: "P >< Q == (P < Q) \<and> (Q < P)" 

17481  42 

21426  43 

44 
lemmas rewrite_rls = strimp_def streqv_def 

45 

61385  46 
lemma iffR: "\<lbrakk>$H,P  $E,Q,$F; $H,Q  $E,P,$F\<rbrakk> \<Longrightarrow> $H  $E, P \<longleftrightarrow> Q, $F" 
21426  47 
apply (unfold iff_def) 
48 
apply (assumption  rule conjR impR)+ 

49 
done 

50 

61385  51 
lemma iffL: "\<lbrakk>$H,$G  $E,P,Q; $H,Q,P,$G  $E \<rbrakk> \<Longrightarrow> $H, P \<longleftrightarrow> Q, $G  $E" 
21426  52 
apply (unfold iff_def) 
53 
apply (assumption  rule conjL impL basic)+ 

54 
done 

55 

56 
lemmas 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 

17481  59 

60 
end 