(* Title: Sequents/Sequents.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge *) header {* Parsing and pretty-printing of sequences *} theory Sequents imports Pure uses ("prover.ML") begin global typedecl o (* Sequences *) typedecl seq' consts SeqO' :: "[o,seq']=>seq'" Seq1' :: "o=>seq'" (* concrete syntax *) nonterminals seq seqobj seqcont syntax SeqEmp :: seq ("") SeqApp :: "[seqobj,seqcont] => seq" ("__") SeqContEmp :: seqcont ("") SeqContApp :: "[seqobj,seqcont] => seqcont" (",/ __") SeqO :: "o => seqobj" ("_") SeqId :: "'a => seqobj" ("$_") types single_seqe = "[seq,seqobj] => prop" single_seqi = "[seq'=>seq',seq'=>seq'] => prop" two_seqi = "[seq'=>seq', seq'=>seq'] => prop" two_seqe = "[seq, seq] => prop" three_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq'] => prop" three_seqe = "[seq, seq, seq] => prop" four_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop" four_seqe = "[seq, seq, seq, seq] => prop" sequence_name = "seq'=>seq'" syntax (*Constant to allow definitions of SEQUENCES of formulas*) "@Side" :: "seq=>(seq'=>seq')" ("<<(_)>>") ML {* (* parse translation for sequences *) fun abs_seq' t = Abs("s", Type("seq'",[]), t); fun seqobj_tr(Const("SeqO",_) $ f) = Const("SeqO'",dummyT) $ f | seqobj_tr(_ $ i) = i; fun seqcont_tr(Const("SeqContEmp",_)) = Bound 0 | seqcont_tr(Const("SeqContApp",_) $ so $ sc) = (seqobj_tr so) $ (seqcont_tr sc); fun seq_tr(Const("SeqEmp",_)) = abs_seq'(Bound 0) | seq_tr(Const("SeqApp",_) $ so $ sc) = abs_seq'(seqobj_tr(so) $ seqcont_tr(sc)); fun singlobj_tr(Const("SeqO",_) $ f) = abs_seq' ((Const("SeqO'",dummyT) $ f) $ Bound 0); (* print translation for sequences *) fun seqcont_tr' (Bound 0) = Const("SeqContEmp",dummyT) | seqcont_tr' (Const("SeqO'",_) $ f $ s) = Const("SeqContApp",dummyT) $ (Const("SeqO",dummyT) $ f) $ (seqcont_tr' s) | (* seqcont_tr' ((a as Abs(_,_,_)) $ s)= seqcont_tr'(Term.betapply(a,s)) | *) seqcont_tr' (i $ s) = Const("SeqContApp",dummyT) $ (Const("SeqId",dummyT) $ i) $ (seqcont_tr' s); fun seq_tr' s = let fun seq_itr' (Bound 0) = Const("SeqEmp",dummyT) | seq_itr' (Const("SeqO'",_) $ f $ s) = Const("SeqApp",dummyT) $ (Const("SeqO",dummyT) $ f) $ (seqcont_tr' s) | (* seq_itr' ((a as Abs(_,_,_)) $ s) = seq_itr'(Term.betapply(a,s)) | *) seq_itr' (i $ s) = Const("SeqApp",dummyT) $ (Const("SeqId",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("SeqO'",_) $ fm) = fm | singlobj_tr'(id) = 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; *} parse_translation {* [("@Side", side_tr)] *} use "prover.ML" end