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