author  wenzelm 
Wed, 22 Apr 2020 19:22:43 +0200  
changeset 71787  acfe72ff00c2 
parent 61386  0a29a984a91b 
permissions  rwrr 
35762  1 
(* Title: Sequents/T.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 T 
7 
imports Modal0 

8 
begin 

9 

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

11 
(* Definition of the star operation using a set of Horn clauses *) 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

12 
(* For system T: gamma * == {P  []P : gamma} *) 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

13 
(* delta * == {P  <>P : delta} *) 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

14 

51309  15 
lstar0: "L>" and 
61385  16 
lstar1: "$G L> $H \<Longrightarrow> []P, $G L> P, $H" and 
17 
lstar2: "$G L> $H \<Longrightarrow> P, $G L> $H" and 

51309  18 
rstar0: "R>" and 
61385  19 
rstar1: "$G R> $H \<Longrightarrow> <>P, $G R> P, $H" and 
20 
rstar2: "$G R> $H \<Longrightarrow> P, $G R> $H" and 

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

21 

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

22 
(* Rules for [] and <> *) 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

23 

17481  24 
boxR: 
61385  25 
"\<lbrakk>$E L> $E'; $F R> $F'; $G R> $G'; 
61386  26 
$E' \<turnstile> $F', P, $G'\<rbrakk> \<Longrightarrow> $E \<turnstile> $F, []P, $G" and 
27 
boxL: "$E, P, $F \<turnstile> $G \<Longrightarrow> $E, []P, $F \<turnstile> $G" and 

28 
diaR: "$E \<turnstile> $F, P, $G \<Longrightarrow> $E \<turnstile> $F, <>P, $G" and 

17481  29 
diaL: 
61385  30 
"\<lbrakk>$E L> $E'; $F L> $F'; $G R> $G'; 
61386  31 
$E', P, $F'\<turnstile> $G'\<rbrakk> \<Longrightarrow> $E, <>P, $F \<turnstile> $G" 
17481  32 

60770  33 
ML \<open> 
21426  34 
structure T_Prover = Modal_ProverFun 
35 
( 

39159  36 
val rewrite_rls = @{thms rewrite_rls} 
37 
val safe_rls = @{thms safe_rls} 

38 
val unsafe_rls = @{thms unsafe_rls} @ [@{thm boxR}, @{thm diaL}] 

39 
val bound_rls = @{thms bound_rls} @ [@{thm boxL}, @{thm diaR}] 

40 
val aside_rls = [@{thm lstar0}, @{thm lstar1}, @{thm lstar2}, @{thm rstar0}, 

41 
@{thm rstar1}, @{thm rstar2}] 

21426  42 
) 
60770  43 
\<close> 
21426  44 

60770  45 
method_setup T_solve = \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (T_Prover.solve_tac ctxt 2))\<close> 
21426  46 

47 

48 
(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *) 

49 

61386  50 
lemma "\<turnstile> []P \<longrightarrow> P" by T_solve 
51 
lemma "\<turnstile> [](P \<longrightarrow> Q) \<longrightarrow> ([]P \<longrightarrow> []Q)" by T_solve (* normality*) 

52 
lemma "\<turnstile> (P < Q) \<longrightarrow> []P \<longrightarrow> []Q" by T_solve 

53 
lemma "\<turnstile> P \<longrightarrow> <>P" by T_solve 

21426  54 

61386  55 
lemma "\<turnstile> [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by T_solve 
56 
lemma "\<turnstile> <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by T_solve 

57 
lemma "\<turnstile> [](P \<longleftrightarrow> Q) \<longleftrightarrow> (P >< Q)" by T_solve 

58 
lemma "\<turnstile> <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" by T_solve 

59 
lemma "\<turnstile> []P \<longleftrightarrow> \<not> <>(\<not> P)" by T_solve 

60 
lemma "\<turnstile> [](\<not> P) \<longleftrightarrow> \<not> <>P" by T_solve 

61 
lemma "\<turnstile> \<not> []P \<longleftrightarrow> <>(\<not> P)" by T_solve 

62 
lemma "\<turnstile> [][]P \<longleftrightarrow> \<not> <><>(\<not> P)" by T_solve 

63 
lemma "\<turnstile> \<not> <>(P \<or> Q) \<longleftrightarrow> \<not> <>P \<and> \<not> <>Q" by T_solve 

21426  64 

61386  65 
lemma "\<turnstile> []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by T_solve 
66 
lemma "\<turnstile> <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by T_solve 

67 
lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by T_solve 

68 
lemma "\<turnstile> <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by T_solve 

69 
lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by T_solve 

70 
lemma "\<turnstile> <>(P \<longrightarrow> (Q \<and> R)) \<longrightarrow> ([]P \<longrightarrow> <>Q) \<and> ([]P \<longrightarrow> <>R)" by T_solve 

71 
lemma "\<turnstile> (P < Q) \<and> (Q < R ) \<longrightarrow> (P < R)" by T_solve 

72 
lemma "\<turnstile> []P \<longrightarrow> <>Q \<longrightarrow> <>(P \<and> Q)" by T_solve 

17481  73 

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

74 
end 