1(*  Title:      Sequents/Sequents.thy
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1993  University of Cambridge
4*)
5
6section \<open>Parsing and pretty-printing of sequences\<close>
7
8theory Sequents
9imports Pure
10keywords "print_pack" :: diag
11begin
12
13setup Pure_Thy.old_appl_syntax_setup
14
15declare [[unify_trace_bound = 20, unify_search_bound = 40]]
16
17typedecl o
18
19
20subsection \<open>Sequences\<close>
21
22typedecl seq'
23consts
24 SeqO'         :: "[o,seq']\<Rightarrow>seq'"
25 Seq1'         :: "o\<Rightarrow>seq'"
26
27
28subsection \<open>Concrete syntax\<close>
29
30nonterminal seq and seqobj and seqcont
31
32syntax
33 "_SeqEmp"         :: seq                                  ("")
34 "_SeqApp"         :: "[seqobj,seqcont] \<Rightarrow> seq"            ("__")
35
36 "_SeqContEmp"     :: seqcont                              ("")
37 "_SeqContApp"     :: "[seqobj,seqcont] \<Rightarrow> seqcont"        (",/ __")
38
39 "_SeqO"           :: "o \<Rightarrow> seqobj"                        ("_")
40 "_SeqId"          :: "'a \<Rightarrow> seqobj"                       ("$_")
41
42type_synonym single_seqe = "[seq,seqobj] \<Rightarrow> prop"
43type_synonym single_seqi = "[seq'\<Rightarrow>seq',seq'\<Rightarrow>seq'] \<Rightarrow> prop"
44type_synonym two_seqi = "[seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop"
45type_synonym two_seqe = "[seq, seq] \<Rightarrow> prop"
46type_synonym three_seqi = "[seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop"
47type_synonym three_seqe = "[seq, seq, seq] \<Rightarrow> prop"
48type_synonym four_seqi = "[seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop"
49type_synonym four_seqe = "[seq, seq, seq, seq] \<Rightarrow> prop"
50type_synonym sequence_name = "seq'\<Rightarrow>seq'"
51
52
53syntax
54  (*Constant to allow definitions of SEQUENCES of formulas*)
55  "_Side"        :: "seq\<Rightarrow>(seq'\<Rightarrow>seq')"     ("<<(_)>>")
56
57ML \<open>
58
59(* parse translation for sequences *)
60
61fun abs_seq' t = Abs ("s", Type (\<^type_name>\<open>seq'\<close>, []), t);
62
63fun seqobj_tr (Const (\<^syntax_const>\<open>_SeqO\<close>, _) $ f) =
64      Const (\<^const_syntax>\<open>SeqO'\<close>, dummyT) $ f
65  | seqobj_tr (_ $ i) = i;
66
67fun seqcont_tr (Const (\<^syntax_const>\<open>_SeqContEmp\<close>, _)) = Bound 0
68  | seqcont_tr (Const (\<^syntax_const>\<open>_SeqContApp\<close>, _) $ so $ sc) =
69      seqobj_tr so $ seqcont_tr sc;
70
71fun seq_tr (Const (\<^syntax_const>\<open>_SeqEmp\<close>, _)) = abs_seq' (Bound 0)
72  | seq_tr (Const (\<^syntax_const>\<open>_SeqApp\<close>, _) $ so $ sc) =
73      abs_seq'(seqobj_tr so $ seqcont_tr sc);
74
75fun singlobj_tr (Const (\<^syntax_const>\<open>_SeqO\<close>,_) $ f) =
76  abs_seq' ((Const (\<^const_syntax>\<open>SeqO'\<close>, dummyT) $ f) $ Bound 0);
77
78
79(* print translation for sequences *)
80
81fun seqcont_tr' (Bound 0) =
82      Const (\<^syntax_const>\<open>_SeqContEmp\<close>, dummyT)
83  | seqcont_tr' (Const (\<^const_syntax>\<open>SeqO'\<close>, _) $ f $ s) =
84      Const (\<^syntax_const>\<open>_SeqContApp\<close>, dummyT) $
85        (Const (\<^syntax_const>\<open>_SeqO\<close>, dummyT) $ f) $ seqcont_tr' s
86  | seqcont_tr' (i $ s) =
87      Const (\<^syntax_const>\<open>_SeqContApp\<close>, dummyT) $
88        (Const (\<^syntax_const>\<open>_SeqId\<close>, dummyT) $ i) $ seqcont_tr' s;
89
90fun seq_tr' s =
91  let
92    fun seq_itr' (Bound 0) = Const (\<^syntax_const>\<open>_SeqEmp\<close>, dummyT)
93      | seq_itr' (Const (\<^const_syntax>\<open>SeqO'\<close>, _) $ f $ s) =
94          Const (\<^syntax_const>\<open>_SeqApp\<close>, dummyT) $
95            (Const (\<^syntax_const>\<open>_SeqO\<close>, dummyT) $ f) $ seqcont_tr' s
96      | seq_itr' (i $ s) =
97          Const (\<^syntax_const>\<open>_SeqApp\<close>, dummyT) $
98            (Const (\<^syntax_const>\<open>_SeqId\<close>, dummyT) $ i) $ seqcont_tr' s
99  in
100    case s of
101      Abs (_, _, t) => seq_itr' t
102    | _ => s $ Bound 0
103  end;
104
105
106fun single_tr c [s1, s2] =
107  Const (c, dummyT) $ seq_tr s1 $ singlobj_tr s2;
108
109fun two_seq_tr c [s1, s2] =
110  Const (c, dummyT) $ seq_tr s1 $ seq_tr s2;
111
112fun three_seq_tr c [s1, s2, s3] =
113  Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3;
114
115fun four_seq_tr c [s1, s2, s3, s4] =
116  Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4;
117
118
119fun singlobj_tr' (Const (\<^const_syntax>\<open>SeqO'\<close>,_) $ fm) = fm
120  | singlobj_tr' id = Const (\<^syntax_const>\<open>_SeqId\<close>, dummyT) $ id;
121
122
123fun single_tr' c [s1, s2] =
124  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
125
126fun two_seq_tr' c [s1, s2] =
127  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
128
129fun three_seq_tr' c [s1, s2, s3] =
130  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3;
131
132fun four_seq_tr' c [s1, s2, s3, s4] =
133  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3 $ seq_tr' s4;
134
135
136
137(** for the <<...>> notation **)
138
139fun side_tr [s1] = seq_tr s1;
140\<close>
141
142parse_translation \<open>[(\<^syntax_const>\<open>_Side\<close>, K side_tr)]\<close>
143
144
145subsection \<open>Proof tools\<close>
146
147ML_file \<open>prover.ML\<close>
148
149end
150