19 |
19 |
20 subsection \<open>Sequences\<close> |
20 subsection \<open>Sequences\<close> |
21 |
21 |
22 typedecl seq' |
22 typedecl seq' |
23 consts |
23 consts |
24 SeqO' :: "[o,seq']=>seq'" |
24 SeqO' :: "[o,seq']\<Rightarrow>seq'" |
25 Seq1' :: "o=>seq'" |
25 Seq1' :: "o\<Rightarrow>seq'" |
26 |
26 |
27 |
27 |
28 subsection \<open>Concrete syntax\<close> |
28 subsection \<open>Concrete syntax\<close> |
29 |
29 |
30 nonterminal seq and seqobj and seqcont |
30 nonterminal seq and seqobj and seqcont |
31 |
31 |
32 syntax |
32 syntax |
33 "_SeqEmp" :: seq ("") |
33 "_SeqEmp" :: seq ("") |
34 "_SeqApp" :: "[seqobj,seqcont] => seq" ("__") |
34 "_SeqApp" :: "[seqobj,seqcont] \<Rightarrow> seq" ("__") |
35 |
35 |
36 "_SeqContEmp" :: seqcont ("") |
36 "_SeqContEmp" :: seqcont ("") |
37 "_SeqContApp" :: "[seqobj,seqcont] => seqcont" (",/ __") |
37 "_SeqContApp" :: "[seqobj,seqcont] \<Rightarrow> seqcont" (",/ __") |
38 |
38 |
39 "_SeqO" :: "o => seqobj" ("_") |
39 "_SeqO" :: "o \<Rightarrow> seqobj" ("_") |
40 "_SeqId" :: "'a => seqobj" ("$_") |
40 "_SeqId" :: "'a \<Rightarrow> seqobj" ("$_") |
41 |
41 |
42 type_synonym single_seqe = "[seq,seqobj] => prop" |
42 type_synonym single_seqe = "[seq,seqobj] \<Rightarrow> prop" |
43 type_synonym single_seqi = "[seq'=>seq',seq'=>seq'] => prop" |
43 type_synonym single_seqi = "[seq'\<Rightarrow>seq',seq'\<Rightarrow>seq'] \<Rightarrow> prop" |
44 type_synonym two_seqi = "[seq'=>seq', seq'=>seq'] => prop" |
44 type_synonym two_seqi = "[seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop" |
45 type_synonym two_seqe = "[seq, seq] => prop" |
45 type_synonym two_seqe = "[seq, seq] \<Rightarrow> prop" |
46 type_synonym three_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq'] => 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] => prop" |
47 type_synonym three_seqe = "[seq, seq, seq] \<Rightarrow> prop" |
48 type_synonym four_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => 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] => prop" |
49 type_synonym four_seqe = "[seq, seq, seq, seq] \<Rightarrow> prop" |
50 type_synonym sequence_name = "seq'=>seq'" |
50 type_synonym sequence_name = "seq'\<Rightarrow>seq'" |
51 |
51 |
52 |
52 |
53 syntax |
53 syntax |
54 (*Constant to allow definitions of SEQUENCES of formulas*) |
54 (*Constant to allow definitions of SEQUENCES of formulas*) |
55 "_Side" :: "seq=>(seq'=>seq')" ("<<(_)>>") |
55 "_Side" :: "seq\<Rightarrow>(seq'\<Rightarrow>seq')" ("<<(_)>>") |
56 |
56 |
57 ML \<open> |
57 ML \<open> |
58 |
58 |
59 (* parse translation for sequences *) |
59 (* parse translation for sequences *) |
60 |
60 |