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