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