author  haftmann 
Thu, 23 Nov 2017 17:03:27 +0000  
changeset 67087  733017b19de9 
parent 61386  0a29a984a91b 
child 69593  3dda49e08b9d 
permissions  rwrr 
17481  1 
(* Title: Sequents/Sequents.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

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

3 
Copyright 1993 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 

60770  6 
section \<open>Parsing and prettyprinting of sequences\<close> 
17481  7 

8 
theory Sequents 

9 
imports Pure 

55228  10 
keywords "print_pack" :: diag 
17481  11 
begin 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

12 

39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
38499
diff
changeset

13 
setup Pure_Thy.old_appl_syntax_setup 
26956
1309a6a0a29f
setup PureThy.old_appl_syntax_setup  theory Pure provides regular application syntax by default;
wenzelm
parents:
24178
diff
changeset

14 

24178
4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
18176
diff
changeset

15 
declare [[unify_trace_bound = 20, unify_search_bound = 40]] 
4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
18176
diff
changeset

16 

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

18 

55228  19 

60770  20 
subsection \<open>Sequences\<close> 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

21 

61385  22 
typedecl seq' 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

23 
consts 
61386  24 
SeqO' :: "[o,seq']\<Rightarrow>seq'" 
25 
Seq1' :: "o\<Rightarrow>seq'" 

17481  26 

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

27 

60770  28 
subsection \<open>Concrete syntax\<close> 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

29 

41229
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
39557
diff
changeset

30 
nonterminal seq and seqobj and seqcont 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

31 

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

32 
syntax 
35113  33 
"_SeqEmp" :: seq ("") 
61386  34 
"_SeqApp" :: "[seqobj,seqcont] \<Rightarrow> seq" ("__") 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

35 

35113  36 
"_SeqContEmp" :: seqcont ("") 
61386  37 
"_SeqContApp" :: "[seqobj,seqcont] \<Rightarrow> seqcont" (",/ __") 
17481  38 

61386  39 
"_SeqO" :: "o \<Rightarrow> seqobj" ("_") 
40 
"_SeqId" :: "'a \<Rightarrow> seqobj" ("$_") 

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

41 

61386  42 
type_synonym single_seqe = "[seq,seqobj] \<Rightarrow> prop" 
43 
type_synonym single_seqi = "[seq'\<Rightarrow>seq',seq'\<Rightarrow>seq'] \<Rightarrow> prop" 

44 
type_synonym two_seqi = "[seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop" 

45 
type_synonym two_seqe = "[seq, seq] \<Rightarrow> prop" 

46 
type_synonym three_seqi = "[seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop" 

47 
type_synonym three_seqe = "[seq, seq, seq] \<Rightarrow> prop" 

48 
type_synonym four_seqi = "[seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop" 

49 
type_synonym four_seqe = "[seq, seq, seq, seq] \<Rightarrow> prop" 

50 
type_synonym sequence_name = "seq'\<Rightarrow>seq'" 

7166
a4a870ec2e67
Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents:
7121
diff
changeset

51 

a4a870ec2e67
Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents:
7121
diff
changeset

52 

14765  53 
syntax 
7166
a4a870ec2e67
Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents:
7121
diff
changeset

54 
(*Constant to allow definitions of SEQUENCES of formulas*) 
61386  55 
"_Side" :: "seq\<Rightarrow>(seq'\<Rightarrow>seq')" ("<<(_)>>") 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

56 

60770  57 
ML \<open> 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

58 

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

59 
(* parse translation for sequences *) 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

60 

35430
df2862dc23a8
adapted to authentic syntax  actual types are verbatim;
wenzelm
parents:
35363
diff
changeset

61 
fun abs_seq' t = Abs ("s", Type (@{type_name seq'}, []), t); 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

62 

35113  63 
fun seqobj_tr (Const (@{syntax_const "_SeqO"}, _) $ f) = 
64 
Const (@{const_syntax SeqO'}, dummyT) $ f 

65 
 seqobj_tr (_ $ i) = i; 

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

66 

35113  67 
fun seqcont_tr (Const (@{syntax_const "_SeqContEmp"}, _)) = Bound 0 
68 
 seqcont_tr (Const (@{syntax_const "_SeqContApp"}, _) $ so $ sc) = 

69 
seqobj_tr so $ seqcont_tr sc; 

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

70 

35113  71 
fun seq_tr (Const (@{syntax_const "_SeqEmp"}, _)) = abs_seq' (Bound 0) 
72 
 seq_tr (Const (@{syntax_const "_SeqApp"}, _) $ so $ sc) = 

73 
abs_seq'(seqobj_tr so $ seqcont_tr sc); 

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

74 

35113  75 
fun singlobj_tr (Const (@{syntax_const "_SeqO"},_) $ f) = 
76 
abs_seq' ((Const (@{const_syntax SeqO'}, dummyT) $ f) $ Bound 0); 

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

77 

17481  78 

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

79 
(* print translation for sequences *) 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

80 

17481  81 
fun seqcont_tr' (Bound 0) = 
35113  82 
Const (@{syntax_const "_SeqContEmp"}, dummyT) 
83 
 seqcont_tr' (Const (@{const_syntax SeqO'}, _) $ f $ s) = 

84 
Const (@{syntax_const "_SeqContApp"}, dummyT) $ 

85 
(Const (@{syntax_const "_SeqO"}, dummyT) $ f) $ seqcont_tr' s 

86 
 seqcont_tr' (i $ s) = 

87 
Const (@{syntax_const "_SeqContApp"}, dummyT) $ 

88 
(Const (@{syntax_const "_SeqId"}, dummyT) $ i) $ seqcont_tr' s; 

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

89 

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

90 
fun seq_tr' s = 
35113  91 
let 
92 
fun seq_itr' (Bound 0) = Const (@{syntax_const "_SeqEmp"}, dummyT) 

93 
 seq_itr' (Const (@{const_syntax SeqO'}, _) $ f $ s) = 

94 
Const (@{syntax_const "_SeqApp"}, dummyT) $ 

95 
(Const (@{syntax_const "_SeqO"}, dummyT) $ f) $ seqcont_tr' s 

96 
 seq_itr' (i $ s) = 

97 
Const (@{syntax_const "_SeqApp"}, dummyT) $ 

98 
(Const (@{syntax_const "_SeqId"}, dummyT) $ i) $ seqcont_tr' s 

99 
in 

100 
case s of 

101 
Abs (_, _, t) => seq_itr' t 

102 
 _ => s $ Bound 0 

103 
end; 

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

104 

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

105 

35113  106 
fun single_tr c [s1, s2] = 
107 
Const (c, dummyT) $ seq_tr s1 $ singlobj_tr s2; 

108 

109 
fun two_seq_tr c [s1, s2] = 

110 
Const (c, dummyT) $ seq_tr s1 $ seq_tr s2; 

111 

112 
fun three_seq_tr c [s1, s2, s3] = 

113 
Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3; 

114 

115 
fun four_seq_tr c [s1, s2, s3, s4] = 

116 
Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4; 

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

117 

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

118 

35113  119 
fun singlobj_tr' (Const (@{const_syntax SeqO'},_) $ fm) = fm 
120 
 singlobj_tr' id = Const (@{syntax_const "_SeqId"}, dummyT) $ id; 

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

121 

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

122 

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

123 
fun single_tr' c [s1, s2] = 
35113  124 
Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2; 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

125 

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

126 
fun two_seq_tr' c [s1, s2] = 
17481  127 
Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2; 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

128 

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

129 
fun three_seq_tr' c [s1, s2, s3] = 
17481  130 
Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3; 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

131 

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

132 
fun four_seq_tr' c [s1, s2, s3, s4] = 
17481  133 
Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3 $ seq_tr' s4; 
134 

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

135 

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

136 

7166
a4a870ec2e67
Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents:
7121
diff
changeset

137 
(** for the <<...>> notation **) 
17481  138 

7166
a4a870ec2e67
Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents:
7121
diff
changeset

139 
fun side_tr [s1] = seq_tr s1; 
60770  140 
\<close> 
7166
a4a870ec2e67
Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents:
7121
diff
changeset

141 

60770  142 
parse_translation \<open>[(@{syntax_const "_Side"}, K side_tr)]\<close> 
17481  143 

55228  144 

60770  145 
subsection \<open>Proof tools\<close> 
55228  146 

48891  147 
ML_file "prover.ML" 
17481  148 

149 
end 