src/Sequents/Sequents.thy
author hoelzl
Mon, 08 Aug 2016 14:13:14 +0200
changeset 63627 6ddb43c6b711
parent 61386 0a29a984a91b
child 69593 3dda49e08b9d
permissions -rw-r--r--
rename HOL-Multivariate_Analysis to HOL-Analysis.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
     1
(*  Title:      Sequents/Sequents.thy
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     3
    Copyright   1993  University of Cambridge
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     4
*)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     5
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
     6
section \<open>Parsing and pretty-printing of sequences\<close>
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
     7
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
     8
theory Sequents
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
     9
imports Pure
55228
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 52143
diff changeset
    10
keywords "print_pack" :: diag
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    11
begin
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    12
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 38499
diff changeset
    13
setup Pure_Thy.old_appl_syntax_setup
26956
1309a6a0a29f setup PureThy.old_appl_syntax_setup -- theory Pure provides regular application syntax by default;
wenzelm
parents: 24178
diff changeset
    14
24178
4ff1dc2aa18d turned Unify flags into configuration options (global only);
wenzelm
parents: 18176
diff changeset
    15
declare [[unify_trace_bound = 20, unify_search_bound = 40]]
4ff1dc2aa18d turned Unify flags into configuration options (global only);
wenzelm
parents: 18176
diff changeset
    16
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    17
typedecl o
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    18
55228
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 52143
diff changeset
    19
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
    20
subsection \<open>Sequences\<close>
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    21
61385
538100cc4399 more symbols;
wenzelm
parents: 60770
diff changeset
    22
typedecl seq'
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    23
consts
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    24
 SeqO'         :: "[o,seq']\<Rightarrow>seq'"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    25
 Seq1'         :: "o\<Rightarrow>seq'"
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    26
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    27
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
    28
subsection \<open>Concrete syntax\<close>
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    29
41229
d797baa3d57c replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents: 39557
diff changeset
    30
nonterminal seq and seqobj and seqcont
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    31
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    32
syntax
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    33
 "_SeqEmp"         :: seq                                  ("")
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    34
 "_SeqApp"         :: "[seqobj,seqcont] \<Rightarrow> seq"            ("__")
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    35
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    36
 "_SeqContEmp"     :: seqcont                              ("")
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    37
 "_SeqContApp"     :: "[seqobj,seqcont] \<Rightarrow> seqcont"        (",/ __")
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    38
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    39
 "_SeqO"           :: "o \<Rightarrow> seqobj"                        ("_")
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    40
 "_SeqId"          :: "'a \<Rightarrow> seqobj"                       ("$_")
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    41
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    42
type_synonym single_seqe = "[seq,seqobj] \<Rightarrow> prop"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    43
type_synonym single_seqi = "[seq'\<Rightarrow>seq',seq'\<Rightarrow>seq'] \<Rightarrow> prop"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    44
type_synonym two_seqi = "[seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    45
type_synonym two_seqe = "[seq, seq] \<Rightarrow> prop"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    46
type_synonym three_seqi = "[seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    47
type_synonym three_seqe = "[seq, seq, seq] \<Rightarrow> prop"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    48
type_synonym four_seqi = "[seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    49
type_synonym four_seqe = "[seq, seq, seq, seq] \<Rightarrow> prop"
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    50
type_synonym sequence_name = "seq'\<Rightarrow>seq'"
7166
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
    51
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
    52
14765
bafb24c150c1 proper use of 'syntax';
wenzelm
parents: 7166
diff changeset
    53
syntax
7166
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
    54
  (*Constant to allow definitions of SEQUENCES of formulas*)
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    55
  "_Side"        :: "seq\<Rightarrow>(seq'\<Rightarrow>seq')"     ("<<(_)>>")
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    56
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
    57
ML \<open>
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    58
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    59
(* parse translation for sequences *)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    60
35430
df2862dc23a8 adapted to authentic syntax -- actual types are verbatim;
wenzelm
parents: 35363
diff changeset
    61
fun abs_seq' t = Abs ("s", Type (@{type_name seq'}, []), t);
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    62
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    63
fun seqobj_tr (Const (@{syntax_const "_SeqO"}, _) $ f) =
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    64
      Const (@{const_syntax SeqO'}, dummyT) $ f
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    65
  | seqobj_tr (_ $ i) = i;
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    66
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    67
fun seqcont_tr (Const (@{syntax_const "_SeqContEmp"}, _)) = Bound 0
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    68
  | seqcont_tr (Const (@{syntax_const "_SeqContApp"}, _) $ so $ sc) =
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    69
      seqobj_tr so $ seqcont_tr sc;
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    70
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    71
fun seq_tr (Const (@{syntax_const "_SeqEmp"}, _)) = abs_seq' (Bound 0)
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    72
  | seq_tr (Const (@{syntax_const "_SeqApp"}, _) $ so $ sc) =
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    73
      abs_seq'(seqobj_tr so $ seqcont_tr sc);
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    74
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    75
fun singlobj_tr (Const (@{syntax_const "_SeqO"},_) $ f) =
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    76
  abs_seq' ((Const (@{const_syntax SeqO'}, dummyT) $ f) $ Bound 0);
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    77
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    78
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    79
(* print translation for sequences *)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    80
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    81
fun seqcont_tr' (Bound 0) =
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    82
      Const (@{syntax_const "_SeqContEmp"}, dummyT)
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    83
  | seqcont_tr' (Const (@{const_syntax SeqO'}, _) $ f $ s) =
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    84
      Const (@{syntax_const "_SeqContApp"}, dummyT) $
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    85
        (Const (@{syntax_const "_SeqO"}, dummyT) $ f) $ seqcont_tr' s
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    86
  | seqcont_tr' (i $ s) =
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    87
      Const (@{syntax_const "_SeqContApp"}, dummyT) $
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    88
        (Const (@{syntax_const "_SeqId"}, dummyT) $ i) $ seqcont_tr' s;
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    89
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    90
fun seq_tr' s =
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    91
  let
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    92
    fun seq_itr' (Bound 0) = Const (@{syntax_const "_SeqEmp"}, dummyT)
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    93
      | seq_itr' (Const (@{const_syntax SeqO'}, _) $ f $ s) =
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    94
          Const (@{syntax_const "_SeqApp"}, dummyT) $
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    95
            (Const (@{syntax_const "_SeqO"}, dummyT) $ f) $ seqcont_tr' s
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    96
      | seq_itr' (i $ s) =
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    97
          Const (@{syntax_const "_SeqApp"}, dummyT) $
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    98
            (Const (@{syntax_const "_SeqId"}, dummyT) $ i) $ seqcont_tr' s
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
    99
  in
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
   100
    case s of
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
   101
      Abs (_, _, t) => seq_itr' t
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
   102
    | _ => s $ Bound 0
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
   103
  end;
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   104
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   105
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
   106
fun single_tr c [s1, s2] =
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
   107
  Const (c, dummyT) $ seq_tr s1 $ singlobj_tr s2;
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
   108
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
   109
fun two_seq_tr c [s1, s2] =
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
   110
  Const (c, dummyT) $ seq_tr s1 $ seq_tr s2;
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
   111
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
   112
fun three_seq_tr c [s1, s2, s3] =
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
   113
  Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3;
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
   114
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
   115
fun four_seq_tr c [s1, s2, s3, s4] =
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
   116
  Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4;
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   117
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   118
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
   119
fun singlobj_tr' (Const (@{const_syntax SeqO'},_) $ fm) = fm
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
   120
  | singlobj_tr' id = Const (@{syntax_const "_SeqId"}, dummyT) $ id;
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   121
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   122
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   123
fun single_tr' c [s1, s2] =
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 26956
diff changeset
   124
  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   125
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   126
fun two_seq_tr' c [s1, s2] =
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   127
  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   128
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   129
fun three_seq_tr' c [s1, s2, s3] =
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   130
  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3;
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   131
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   132
fun four_seq_tr' c [s1, s2, s3, s4] =
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   133
  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3 $ seq_tr' s4;
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   134
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   135
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   136
7166
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
   137
(** for the <<...>> notation **)
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   138
7166
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
   139
fun side_tr [s1] = seq_tr s1;
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   140
\<close>
7166
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
   141
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   142
parse_translation \<open>[(@{syntax_const "_Side"}, K side_tr)]\<close>
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   143
55228
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 52143
diff changeset
   144
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   145
subsection \<open>Proof tools\<close>
55228
901a6696cdd8 misc tuning and modernization;
wenzelm
parents: 52143
diff changeset
   146
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 42463
diff changeset
   147
ML_file "prover.ML"
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   148
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   149
end