author  wenzelm 
Mon, 11 Jan 2016 21:20:44 +0100  
changeset 62144  bdab93ccfaf8 
parent 61386  0a29a984a91b 
child 69605  3dda49e08b9d 
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) 

17481  15 
Lstar :: "two_seqi" 
16 
Rstar :: "two_seqi" 

14765  17 

18 
syntax 

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

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

21 

60770  22 
ML \<open> 
35113  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; 

60770  25 
\<close> 
17481  26 

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

60770  30 
\<close> 
35113  31 

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

60770  35 
\<close> 
17481  36 

62144  37 
definition strimp :: "[o,o]\<Rightarrow>o" (infixr "<" 25) 
38 
where "P < Q == [](P \<longrightarrow> Q)" 

39 

40 
definition streqv :: "[o,o]\<Rightarrow>o" (infixr "><" 25) 

41 
where "P >< Q == (P < Q) \<and> (Q < P)" 

17481  42 

21426  43 

44 
lemmas rewrite_rls = strimp_def streqv_def 

45 

61386  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" 
21426  47 
apply (unfold iff_def) 
48 
apply (assumption  rule conjR impR)+ 

49 
done 

50 

61386  51 
lemma iffL: "\<lbrakk>$H,$G \<turnstile> $E,P,Q; $H,Q,P,$G \<turnstile> $E \<rbrakk> \<Longrightarrow> $H, P \<longleftrightarrow> Q, $G \<turnstile> $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 