|
(* Title: Sequents/Sequents.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
*)
section \<open>Parsing and pretty-printing of sequences\<close>
theory Sequents
imports Pure
keywords "print_pack" :: diag
begin
setup Pure_Thy.old_appl_syntax_setup
declare [[unify_trace_bound = 20, unify_search_bound = 40]]
typedecl o
subsection \<open>Sequences\<close>
typedecl seq'
consts
SeqO' :: "[o,seq']\<Rightarrow>seq'"
Seq1' :: "o\seq'"
subsection \<open>Concrete syntax\<close>
nonterminal seq and seqobj and seqcont
syntax
"_SeqEmp" :: seq ("")
"_SeqApp" :: "[seqobj,seqcont] \ seq" ("__")
"_SeqContEmp" :: seqcont ("")
"_SeqContApp" :: "[seqobj,seqcont] \ seqcont" (",/ __")
"_SeqO" :: "o \ seqobj" ("_")
"_SeqId" :: "'a \ seqobj" ("$_")
type_synonym single_seqe = "[seq,seqobj] \ prop"
type_synonym single_seqi = "[seq'\seq',seq'\seq'] \ prop"
type_synonym two_seqi = "[seq'\seq', seq'\seq'] \ prop"
type_synonym two_seqe = "[seq, seq] \ prop"
type_synonym three_seqi = "[seq'\seq', seq'\seq', seq'\seq'] \ prop"
type_synonym three_seqe = "[seq, seq, seq] \ prop"
type_synonym four_seqi = "[seq'\seq', seq'\seq', seq'\seq', seq'\seq'] \ prop"
type_synonym four_seqe = "[seq, seq, seq, seq] \ prop"
type_synonym sequence_name = "seq'\seq'"
syntax
(*Constant to allow definitions of SEQUENCES of formulas*)
"_Side" :: "seq\(seq'\seq')" ("<<(_)>>")
ML \<open>
(* parse translation for sequences *)
fun abs_seq' t = Abs ("s", Type (\<^type_name>\seq'\, []), t);
fun seqobj_tr (Const (\<^syntax_const>\<open>_SeqO\<close>, _) $ f) =
Const (\<^const_syntax>\<open>SeqO'\<close>, dummyT) $ f
| seqobj_tr (_ $ i) = i;
fun seqcont_tr (Const (\<^syntax_const>\<open>_SeqContEmp\<close>, _)) = Bound 0
| seqcont_tr (Const (\<^syntax_const>\<open>_SeqContApp\<close>, _) $ so $ sc) =
seqobj_tr so $ seqcont_tr sc;
fun seq_tr (Const (\<^syntax_const>\<open>_SeqEmp\<close>, _)) = abs_seq' (Bound 0)
| seq_tr (Const (\<^syntax_const>\<open>_SeqApp\<close>, _) $ so $ sc) =
abs_seq'(seqobj_tr so $ seqcont_tr sc);
fun singlobj_tr (Const (\<^syntax_const>\<open>_SeqO\<close>,_) $ f) =
abs_seq' ((Const (\<^const_syntax>\SeqO'\, dummyT) $ f) $ Bound 0);
(* print translation for sequences *)
fun seqcont_tr' (Bound 0) =
Const (\<^syntax_const>\<open>_SeqContEmp\<close>, dummyT)
| seqcont_tr' (Const (\<^const_syntax>\SeqO'\, _) $ f $ s) =
Const (\<^syntax_const>\<open>_SeqContApp\<close>, dummyT) $
(Const (\<^syntax_const>\<open>_SeqO\<close>, dummyT) $ f) $ seqcont_tr' s
| seqcont_tr' (i $ s) =
Const (\<^syntax_const>\<open>_SeqContApp\<close>, dummyT) $
(Const (\<^syntax_const>\<open>_SeqId\<close>, dummyT) $ i) $ seqcont_tr' s;
fun seq_tr' s =
let
fun seq_itr' (Bound 0) = Const (\<^syntax_const>\_SeqEmp\, dummyT)
| seq_itr' (Const (\<^const_syntax>\SeqO'\, _) $ f $ s) =
Const (\<^syntax_const>\<open>_SeqApp\<close>, dummyT) $
(Const (\<^syntax_const>\<open>_SeqO\<close>, dummyT) $ f) $ seqcont_tr' s
| seq_itr' (i $ s) =
Const (\<^syntax_const>\<open>_SeqApp\<close>, dummyT) $
(Const (\<^syntax_const>\<open>_SeqId\<close>, dummyT) $ i) $ seqcont_tr' s
in
case s of
Abs (_, _, t) => seq_itr' t
| _ => s $ Bound 0
end;
fun single_tr c [s1, s2] =
Const (c, dummyT) $ seq_tr s1 $ singlobj_tr s2;
fun two_seq_tr c [s1, s2] =
Const (c, dummyT) $ seq_tr s1 $ seq_tr s2;
fun three_seq_tr c [s1, s2, s3] =
Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3;
fun four_seq_tr c [s1, s2, s3, s4] =
Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4;
fun singlobj_tr' (Const (\<^const_syntax>\SeqO'\,_) $ fm) = fm
| singlobj_tr' id = Const (\<^syntax_const>\_SeqId\, dummyT) $ id;
fun single_tr' c [s1, s2] =
Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
fun two_seq_tr' c [s1, s2] =
Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
fun three_seq_tr' c [s1, s2, s3] =
Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3;
fun four_seq_tr' c [s1, s2, s3, s4] =
Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3 $ seq_tr' s4;
(** for the <<...>> notation **)
fun side_tr [s1] = seq_tr s1;
\<close>
parse_translation \<open>[(\<^syntax_const>\<open>_Side\<close>, K side_tr)]\<close>
subsection \<open>Proof tools\<close>
ML_file \<open>prover.ML\<close>
end
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
