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