author  wenzelm 
Sat, 25 May 2013 15:37:53 +0200  
changeset 52143  36ffe23b25f8 
parent 48891  c0eafbd55de3 
child 60770  240563fbf41d 
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 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

13 
box :: "o=>o" ("[]_" [50] 50) 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

14 
dia :: "o=>o" ("<>_" [50] 50) 
21426  15 
strimp :: "[o,o]=>o" (infixr "<" 25) 
16 
streqv :: "[o,o]=>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 

17481  24 
ML {* 
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; 

17481  27 
*} 
28 

35113  29 
parse_translation {* 
52143  30 
[(@{syntax_const "_Lstar"}, K (star_tr @{const_syntax Lstar})), 
31 
(@{syntax_const "_Rstar"}, K (star_tr @{const_syntax Rstar}))] 

35113  32 
*} 
33 

34 
print_translation {* 

52143  35 
[(@{const_syntax Lstar}, K (star_tr' @{syntax_const "_Lstar"})), 
36 
(@{const_syntax Rstar}, K (star_tr' @{syntax_const "_Rstar"}))] 

35113  37 
*} 
17481  38 

39 
defs 

40 
strimp_def: "P < Q == [](P > Q)" 

41 
streqv_def: "P >< Q == (P < Q) & (Q < P)" 

42 

21426  43 

44 
lemmas rewrite_rls = strimp_def streqv_def 

45 

46 
lemma iffR: 

47 
"[ $H,P  $E,Q,$F; $H,Q  $E,P,$F ] ==> $H  $E, P <> Q, $F" 

48 
apply (unfold iff_def) 

49 
apply (assumption  rule conjR impR)+ 

50 
done 

51 

52 
lemma iffL: 

53 
"[ $H,$G  $E,P,Q; $H,Q,P,$G  $E ] ==> $H, P <> Q, $G  $E" 

54 
apply (unfold iff_def) 

55 
apply (assumption  rule conjL impL basic)+ 

56 
done 

57 

58 
lemmas safe_rls = basic conjL conjR disjL disjR impL impR notL notR iffL iffR 

59 
and unsafe_rls = allR exL 

60 
and bound_rls = allL exR 

17481  61 

62 
end 