src/Sequents/Sequents.thy
author haftmann
Fri Jun 19 21:08:07 2009 +0200 (2009-06-19)
changeset 31726 ffd2dc631d88
parent 26956 1309a6a0a29f
child 35113 1a0c129bb2e0
permissions -rw-r--r--
merged
     1 (*  Title:      Sequents/Sequents.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 *)
     6 
     7 header {* Parsing and pretty-printing of sequences *}
     8 
     9 theory Sequents
    10 imports Pure
    11 uses ("prover.ML")
    12 begin
    13 
    14 setup PureThy.old_appl_syntax_setup
    15 
    16 declare [[unify_trace_bound = 20, unify_search_bound = 40]]
    17 
    18 global
    19 
    20 typedecl o
    21 
    22 (* Sequences *)
    23 
    24 typedecl
    25  seq'
    26 
    27 consts
    28  SeqO'         :: "[o,seq']=>seq'"
    29  Seq1'         :: "o=>seq'"
    30 
    31 
    32 (* concrete syntax *)
    33 
    34 nonterminals
    35   seq seqobj seqcont
    36 
    37 
    38 syntax
    39  SeqEmp         :: seq                                  ("")
    40  SeqApp         :: "[seqobj,seqcont] => seq"            ("__")
    41 
    42  SeqContEmp     :: seqcont                              ("")
    43  SeqContApp     :: "[seqobj,seqcont] => seqcont"        (",/ __")
    44 
    45  SeqO           :: "o => seqobj"                        ("_")
    46  SeqId          :: "'a => seqobj"                       ("$_")
    47 
    48 types
    49  single_seqe = "[seq,seqobj] => prop"
    50  single_seqi = "[seq'=>seq',seq'=>seq'] => prop"
    51  two_seqi    = "[seq'=>seq', seq'=>seq'] => prop"
    52  two_seqe    = "[seq, seq] => prop"
    53  three_seqi  = "[seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
    54  three_seqe  = "[seq, seq, seq] => prop"
    55  four_seqi   = "[seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
    56  four_seqe   = "[seq, seq, seq, seq] => prop"
    57 
    58  sequence_name = "seq'=>seq'"
    59 
    60 
    61 syntax
    62   (*Constant to allow definitions of SEQUENCES of formulas*)
    63   "@Side"        :: "seq=>(seq'=>seq')"     ("<<(_)>>")
    64 
    65 ML {*
    66 
    67 (* parse translation for sequences *)
    68 
    69 fun abs_seq' t = Abs("s", Type("seq'",[]), t);
    70 
    71 fun seqobj_tr(Const("SeqO",_) $ f) = Const("SeqO'",dummyT) $ f |
    72     seqobj_tr(_ $ i) = i;
    73 
    74 fun seqcont_tr(Const("SeqContEmp",_)) = Bound 0 |
    75     seqcont_tr(Const("SeqContApp",_) $ so $ sc) =
    76       (seqobj_tr so) $ (seqcont_tr sc);
    77 
    78 fun seq_tr(Const("SeqEmp",_)) = abs_seq'(Bound 0) |
    79     seq_tr(Const("SeqApp",_) $ so $ sc) =
    80       abs_seq'(seqobj_tr(so) $ seqcont_tr(sc));
    81 
    82 
    83 fun singlobj_tr(Const("SeqO",_) $ f) =
    84     abs_seq' ((Const("SeqO'",dummyT) $ f) $ Bound 0);
    85 
    86 
    87 
    88 (* print translation for sequences *)
    89 
    90 fun seqcont_tr' (Bound 0) =
    91       Const("SeqContEmp",dummyT) |
    92     seqcont_tr' (Const("SeqO'",_) $ f $ s) =
    93       Const("SeqContApp",dummyT) $
    94       (Const("SeqO",dummyT) $ f) $
    95       (seqcont_tr' s) |
    96 (*    seqcont_tr' ((a as Abs(_,_,_)) $ s)=
    97       seqcont_tr'(Term.betapply(a,s)) | *)
    98     seqcont_tr' (i $ s) =
    99       Const("SeqContApp",dummyT) $
   100       (Const("SeqId",dummyT) $ i) $
   101       (seqcont_tr' s);
   102 
   103 fun seq_tr' s =
   104     let fun seq_itr' (Bound 0) =
   105               Const("SeqEmp",dummyT) |
   106             seq_itr' (Const("SeqO'",_) $ f $ s) =
   107               Const("SeqApp",dummyT) $
   108               (Const("SeqO",dummyT) $ f) $ (seqcont_tr' s) |
   109 (*            seq_itr' ((a as Abs(_,_,_)) $ s) =
   110               seq_itr'(Term.betapply(a,s)) |    *)
   111             seq_itr' (i $ s) =
   112               Const("SeqApp",dummyT) $
   113               (Const("SeqId",dummyT) $ i) $
   114               (seqcont_tr' s)
   115     in case s of
   116          Abs(_,_,t) => seq_itr' t |
   117          _ => s $ (Bound 0)
   118     end;
   119 
   120 
   121 
   122 
   123 fun single_tr c [s1,s2] =
   124     Const(c,dummyT) $ seq_tr s1 $ singlobj_tr s2;
   125 
   126 fun two_seq_tr c [s1,s2] =
   127     Const(c,dummyT) $ seq_tr s1 $ seq_tr s2;
   128 
   129 fun three_seq_tr c [s1,s2,s3] =
   130     Const(c,dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3;
   131 
   132 fun 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 fun singlobj_tr'(Const("SeqO'",_) $ fm) = fm |
   137     singlobj_tr'(id) = Const("@SeqId",dummyT) $ id;
   138 
   139 
   140 fun single_tr' c [s1, s2] =
   141 (Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 );
   142 
   143 
   144 fun two_seq_tr' c [s1, s2] =
   145   Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
   146 
   147 fun three_seq_tr' c [s1, s2, s3] =
   148   Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3;
   149 
   150 fun four_seq_tr' c [s1, s2, s3, s4] =
   151   Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3 $ seq_tr' s4;
   152 
   153 
   154 
   155 (** for the <<...>> notation **)
   156 
   157 fun side_tr [s1] = seq_tr s1;
   158 *}
   159 
   160 parse_translation {* [("@Side", side_tr)] *}
   161 
   162 use "prover.ML"
   163 
   164 end
   165