src/Sequents/Sequents.thy
author wenzelm
Sat Jun 02 22:40:03 2018 +0200 (17 months ago)
changeset 68358 e761afd35baa
parent 61386 0a29a984a91b
child 69593 3dda49e08b9d
permissions -rw-r--r--
tuned proofs;
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@60770
     6
section \<open>Parsing and pretty-printing of sequences\<close>
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@60770
    20
subsection \<open>Sequences\<close>
paulson@2073
    21
wenzelm@61385
    22
typedecl seq'
paulson@2073
    23
consts
wenzelm@61386
    24
 SeqO'         :: "[o,seq']\<Rightarrow>seq'"
wenzelm@61386
    25
 Seq1'         :: "o\<Rightarrow>seq'"
wenzelm@17481
    26
paulson@2073
    27
wenzelm@60770
    28
subsection \<open>Concrete syntax\<close>
paulson@2073
    29
wenzelm@41229
    30
nonterminal seq and seqobj and seqcont
paulson@2073
    31
paulson@2073
    32
syntax
wenzelm@35113
    33
 "_SeqEmp"         :: seq                                  ("")
wenzelm@61386
    34
 "_SeqApp"         :: "[seqobj,seqcont] \<Rightarrow> seq"            ("__")
paulson@2073
    35
wenzelm@35113
    36
 "_SeqContEmp"     :: seqcont                              ("")
wenzelm@61386
    37
 "_SeqContApp"     :: "[seqobj,seqcont] \<Rightarrow> seqcont"        (",/ __")
wenzelm@17481
    38
wenzelm@61386
    39
 "_SeqO"           :: "o \<Rightarrow> seqobj"                        ("_")
wenzelm@61386
    40
 "_SeqId"          :: "'a \<Rightarrow> seqobj"                       ("$_")
paulson@2073
    41
wenzelm@61386
    42
type_synonym single_seqe = "[seq,seqobj] \<Rightarrow> prop"
wenzelm@61386
    43
type_synonym single_seqi = "[seq'\<Rightarrow>seq',seq'\<Rightarrow>seq'] \<Rightarrow> prop"
wenzelm@61386
    44
type_synonym two_seqi = "[seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop"
wenzelm@61386
    45
type_synonym two_seqe = "[seq, seq] \<Rightarrow> prop"
wenzelm@61386
    46
type_synonym three_seqi = "[seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop"
wenzelm@61386
    47
type_synonym three_seqe = "[seq, seq, seq] \<Rightarrow> prop"
wenzelm@61386
    48
type_synonym four_seqi = "[seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop"
wenzelm@61386
    49
type_synonym four_seqe = "[seq, seq, seq, seq] \<Rightarrow> prop"
wenzelm@61386
    50
type_synonym sequence_name = "seq'\<Rightarrow>seq'"
paulson@7166
    51
paulson@7166
    52
wenzelm@14765
    53
syntax
paulson@7166
    54
  (*Constant to allow definitions of SEQUENCES of formulas*)
wenzelm@61386
    55
  "_Side"        :: "seq\<Rightarrow>(seq'\<Rightarrow>seq')"     ("<<(_)>>")
paulson@2073
    56
wenzelm@60770
    57
ML \<open>
paulson@2073
    58
paulson@2073
    59
(* parse translation for sequences *)
paulson@2073
    60
wenzelm@35430
    61
fun abs_seq' t = Abs ("s", Type (@{type_name seq'}, []), t);
paulson@2073
    62
wenzelm@35113
    63
fun seqobj_tr (Const (@{syntax_const "_SeqO"}, _) $ f) =
wenzelm@35113
    64
      Const (@{const_syntax SeqO'}, dummyT) $ f
wenzelm@35113
    65
  | seqobj_tr (_ $ i) = i;
paulson@2073
    66
wenzelm@35113
    67
fun seqcont_tr (Const (@{syntax_const "_SeqContEmp"}, _)) = Bound 0
wenzelm@35113
    68
  | seqcont_tr (Const (@{syntax_const "_SeqContApp"}, _) $ so $ sc) =
wenzelm@35113
    69
      seqobj_tr so $ seqcont_tr sc;
paulson@2073
    70
wenzelm@35113
    71
fun seq_tr (Const (@{syntax_const "_SeqEmp"}, _)) = abs_seq' (Bound 0)
wenzelm@35113
    72
  | seq_tr (Const (@{syntax_const "_SeqApp"}, _) $ so $ sc) =
wenzelm@35113
    73
      abs_seq'(seqobj_tr so $ seqcont_tr sc);
paulson@2073
    74
wenzelm@35113
    75
fun singlobj_tr (Const (@{syntax_const "_SeqO"},_) $ f) =
wenzelm@35113
    76
  abs_seq' ((Const (@{const_syntax SeqO'}, dummyT) $ f) $ Bound 0);
paulson@2073
    77
wenzelm@17481
    78
paulson@2073
    79
(* print translation for sequences *)
paulson@2073
    80
wenzelm@17481
    81
fun seqcont_tr' (Bound 0) =
wenzelm@35113
    82
      Const (@{syntax_const "_SeqContEmp"}, dummyT)
wenzelm@35113
    83
  | seqcont_tr' (Const (@{const_syntax SeqO'}, _) $ f $ s) =
wenzelm@35113
    84
      Const (@{syntax_const "_SeqContApp"}, dummyT) $
wenzelm@35113
    85
        (Const (@{syntax_const "_SeqO"}, dummyT) $ f) $ seqcont_tr' s
wenzelm@35113
    86
  | seqcont_tr' (i $ s) =
wenzelm@35113
    87
      Const (@{syntax_const "_SeqContApp"}, dummyT) $
wenzelm@35113
    88
        (Const (@{syntax_const "_SeqId"}, dummyT) $ i) $ seqcont_tr' s;
paulson@2073
    89
paulson@2073
    90
fun seq_tr' s =
wenzelm@35113
    91
  let
wenzelm@35113
    92
    fun seq_itr' (Bound 0) = Const (@{syntax_const "_SeqEmp"}, dummyT)
wenzelm@35113
    93
      | seq_itr' (Const (@{const_syntax SeqO'}, _) $ f $ s) =
wenzelm@35113
    94
          Const (@{syntax_const "_SeqApp"}, dummyT) $
wenzelm@35113
    95
            (Const (@{syntax_const "_SeqO"}, dummyT) $ f) $ seqcont_tr' s
wenzelm@35113
    96
      | seq_itr' (i $ s) =
wenzelm@35113
    97
          Const (@{syntax_const "_SeqApp"}, dummyT) $
wenzelm@35113
    98
            (Const (@{syntax_const "_SeqId"}, dummyT) $ i) $ seqcont_tr' s
wenzelm@35113
    99
  in
wenzelm@35113
   100
    case s of
wenzelm@35113
   101
      Abs (_, _, t) => seq_itr' t
wenzelm@35113
   102
    | _ => s $ Bound 0
wenzelm@35113
   103
  end;
paulson@2073
   104
paulson@2073
   105
wenzelm@35113
   106
fun single_tr c [s1, s2] =
wenzelm@35113
   107
  Const (c, dummyT) $ seq_tr s1 $ singlobj_tr s2;
wenzelm@35113
   108
wenzelm@35113
   109
fun two_seq_tr c [s1, s2] =
wenzelm@35113
   110
  Const (c, dummyT) $ seq_tr s1 $ seq_tr s2;
wenzelm@35113
   111
wenzelm@35113
   112
fun three_seq_tr c [s1, s2, s3] =
wenzelm@35113
   113
  Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3;
wenzelm@35113
   114
wenzelm@35113
   115
fun four_seq_tr c [s1, s2, s3, s4] =
wenzelm@35113
   116
  Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4;
paulson@2073
   117
paulson@2073
   118
wenzelm@35113
   119
fun singlobj_tr' (Const (@{const_syntax SeqO'},_) $ fm) = fm
wenzelm@35113
   120
  | singlobj_tr' id = Const (@{syntax_const "_SeqId"}, dummyT) $ id;
paulson@2073
   121
paulson@2073
   122
paulson@2073
   123
fun single_tr' c [s1, s2] =
wenzelm@35113
   124
  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
paulson@2073
   125
paulson@2073
   126
fun two_seq_tr' c [s1, s2] =
wenzelm@17481
   127
  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
paulson@2073
   128
paulson@2073
   129
fun three_seq_tr' c [s1, s2, s3] =
wenzelm@17481
   130
  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3;
paulson@2073
   131
paulson@2073
   132
fun four_seq_tr' c [s1, s2, s3, s4] =
wenzelm@17481
   133
  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3 $ seq_tr' s4;
wenzelm@17481
   134
paulson@2073
   135
paulson@2073
   136
paulson@7166
   137
(** for the <<...>> notation **)
wenzelm@17481
   138
paulson@7166
   139
fun side_tr [s1] = seq_tr s1;
wenzelm@60770
   140
\<close>
paulson@7166
   141
wenzelm@60770
   142
parse_translation \<open>[(@{syntax_const "_Side"}, K side_tr)]\<close>
wenzelm@17481
   143
wenzelm@55228
   144
wenzelm@60770
   145
subsection \<open>Proof tools\<close>
wenzelm@55228
   146
wenzelm@48891
   147
ML_file "prover.ML"
wenzelm@17481
   148
wenzelm@17481
   149
end