src/Sequents/Sequents.thy

primitive add_def: strip sorts in axiom;

(*  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

declare [[unify_trace_bound = 20, unify_search_bound = 40]]

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