author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 35113  1a0c129bb2e0 
child 48891  c0eafbd55de3 
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 
uses "modal.ML" 

9 
begin 

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

10 

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

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

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

13 
dia :: "o=>o" ("<>_" [50] 50) 
21426  14 
strimp :: "[o,o]=>o" (infixr "<" 25) 
15 
streqv :: "[o,o]=>o" (infixr "><" 25) 

17481  16 
Lstar :: "two_seqi" 
17 
Rstar :: "two_seqi" 

14765  18 

19 
syntax 

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

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

22 

17481  23 
ML {* 
35113  24 
fun star_tr c [s1, s2] = Const(c, dummyT) $ seq_tr s1 $ seq_tr s2; 
25 
fun star_tr' c [s1, s2] = Const(c, dummyT) $ seq_tr' s1 $ seq_tr' s2; 

17481  26 
*} 
27 

35113  28 
parse_translation {* 
29 
[(@{syntax_const "_Lstar"}, star_tr @{const_syntax Lstar}), 

30 
(@{syntax_const "_Rstar"}, star_tr @{const_syntax Rstar})] 

31 
*} 

32 

33 
print_translation {* 

34 
[(@{const_syntax Lstar}, star_tr' @{syntax_const "_Lstar"}), 

35 
(@{const_syntax Rstar}, star_tr' @{syntax_const "_Rstar"})] 

36 
*} 

17481  37 

38 
defs 

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

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

41 

21426  42 

43 
lemmas rewrite_rls = strimp_def streqv_def 

44 

45 
lemma iffR: 

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

47 
apply (unfold iff_def) 

48 
apply (assumption  rule conjR impR)+ 

49 
done 

50 

51 
lemma iffL: 

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

53 
apply (unfold iff_def) 

54 
apply (assumption  rule conjL impL basic)+ 

55 
done 

56 

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

58 
and unsafe_rls = allR exL 

59 
and bound_rls = allL exR 

17481  60 

61 
end 