src/Sequents/Sequents.thy
author wenzelm
Mon Mar 19 21:10:33 2012 +0100 (2012-03-19)
changeset 47022 8eac39af4ec0
parent 42463 f270e3e18be5
child 48891 c0eafbd55de3
permissions -rw-r--r--
moved some legacy stuff;
     1 (*  Title:      Sequents/Sequents.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1993  University of Cambridge
     4 *)
     5 
     6 header {* Parsing and pretty-printing of sequences *}
     7 
     8 theory Sequents
     9 imports Pure
    10 uses ("prover.ML")
    11 begin
    12 
    13 setup Pure_Thy.old_appl_syntax_setup
    14 
    15 declare [[unify_trace_bound = 20, unify_search_bound = 40]]
    16 
    17 typedecl o
    18 
    19 (* Sequences *)
    20 
    21 typedecl
    22  seq'
    23 
    24 consts
    25  SeqO'         :: "[o,seq']=>seq'"
    26  Seq1'         :: "o=>seq'"
    27 
    28 
    29 (* concrete syntax *)
    30 
    31 nonterminal seq and seqobj and seqcont
    32 
    33 syntax
    34  "_SeqEmp"         :: seq                                  ("")
    35  "_SeqApp"         :: "[seqobj,seqcont] => seq"            ("__")
    36 
    37  "_SeqContEmp"     :: seqcont                              ("")
    38  "_SeqContApp"     :: "[seqobj,seqcont] => seqcont"        (",/ __")
    39 
    40  "_SeqO"           :: "o => seqobj"                        ("_")
    41  "_SeqId"          :: "'a => seqobj"                       ("$_")
    42 
    43 type_synonym single_seqe = "[seq,seqobj] => prop"
    44 type_synonym single_seqi = "[seq'=>seq',seq'=>seq'] => prop"
    45 type_synonym two_seqi = "[seq'=>seq', seq'=>seq'] => prop"
    46 type_synonym two_seqe = "[seq, seq] => prop"
    47 type_synonym three_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
    48 type_synonym three_seqe = "[seq, seq, seq] => prop"
    49 type_synonym four_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
    50 type_synonym four_seqe = "[seq, seq, seq, seq] => prop"
    51 type_synonym sequence_name = "seq'=>seq'"
    52 
    53 
    54 syntax
    55   (*Constant to allow definitions of SEQUENCES of formulas*)
    56   "_Side"        :: "seq=>(seq'=>seq')"     ("<<(_)>>")
    57 
    58 ML {*
    59 
    60 (* parse translation for sequences *)
    61 
    62 fun abs_seq' t = Abs ("s", Type (@{type_name seq'}, []), t);
    63 
    64 fun seqobj_tr (Const (@{syntax_const "_SeqO"}, _) $ f) =
    65       Const (@{const_syntax SeqO'}, dummyT) $ f
    66   | seqobj_tr (_ $ i) = i;
    67 
    68 fun seqcont_tr (Const (@{syntax_const "_SeqContEmp"}, _)) = Bound 0
    69   | seqcont_tr (Const (@{syntax_const "_SeqContApp"}, _) $ so $ sc) =
    70       seqobj_tr so $ seqcont_tr sc;
    71 
    72 fun seq_tr (Const (@{syntax_const "_SeqEmp"}, _)) = abs_seq' (Bound 0)
    73   | seq_tr (Const (@{syntax_const "_SeqApp"}, _) $ so $ sc) =
    74       abs_seq'(seqobj_tr so $ seqcont_tr sc);
    75 
    76 fun singlobj_tr (Const (@{syntax_const "_SeqO"},_) $ f) =
    77   abs_seq' ((Const (@{const_syntax SeqO'}, dummyT) $ f) $ Bound 0);
    78 
    79 
    80 (* print translation for sequences *)
    81 
    82 fun seqcont_tr' (Bound 0) =
    83       Const (@{syntax_const "_SeqContEmp"}, dummyT)
    84   | seqcont_tr' (Const (@{const_syntax SeqO'}, _) $ f $ s) =
    85       Const (@{syntax_const "_SeqContApp"}, dummyT) $
    86         (Const (@{syntax_const "_SeqO"}, dummyT) $ f) $ seqcont_tr' s
    87   | seqcont_tr' (i $ s) =
    88       Const (@{syntax_const "_SeqContApp"}, dummyT) $
    89         (Const (@{syntax_const "_SeqId"}, dummyT) $ i) $ seqcont_tr' s;
    90 
    91 fun seq_tr' s =
    92   let
    93     fun seq_itr' (Bound 0) = Const (@{syntax_const "_SeqEmp"}, dummyT)
    94       | seq_itr' (Const (@{const_syntax SeqO'}, _) $ f $ s) =
    95           Const (@{syntax_const "_SeqApp"}, dummyT) $
    96             (Const (@{syntax_const "_SeqO"}, dummyT) $ f) $ seqcont_tr' s
    97       | seq_itr' (i $ s) =
    98           Const (@{syntax_const "_SeqApp"}, dummyT) $
    99             (Const (@{syntax_const "_SeqId"}, dummyT) $ i) $ seqcont_tr' s
   100   in
   101     case s of
   102       Abs (_, _, t) => seq_itr' t
   103     | _ => s $ Bound 0
   104   end;
   105 
   106 
   107 fun single_tr c [s1, s2] =
   108   Const (c, dummyT) $ seq_tr s1 $ singlobj_tr s2;
   109 
   110 fun two_seq_tr c [s1, s2] =
   111   Const (c, dummyT) $ seq_tr s1 $ seq_tr s2;
   112 
   113 fun three_seq_tr c [s1, s2, s3] =
   114   Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3;
   115 
   116 fun four_seq_tr c [s1, s2, s3, s4] =
   117   Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4;
   118 
   119 
   120 fun singlobj_tr' (Const (@{const_syntax SeqO'},_) $ fm) = fm
   121   | singlobj_tr' id = Const (@{syntax_const "_SeqId"}, dummyT) $ id;
   122 
   123 
   124 fun single_tr' c [s1, s2] =
   125   Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
   126 
   127 fun two_seq_tr' c [s1, s2] =
   128   Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
   129 
   130 fun three_seq_tr' c [s1, s2, s3] =
   131   Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3;
   132 
   133 fun four_seq_tr' c [s1, s2, s3, s4] =
   134   Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3 $ seq_tr' s4;
   135 
   136 
   137 
   138 (** for the <<...>> notation **)
   139 
   140 fun side_tr [s1] = seq_tr s1;
   141 *}
   142 
   143 parse_translation {* [(@{syntax_const "_Side"}, side_tr)] *}
   144 
   145 use "prover.ML"
   146 
   147 end
   148