Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Sequents.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      Sequents/Sequents.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge
*)

section \<open>Parsing and pretty-printing of sequences\<close>

theory Sequents
imports Pure
keywords "print_pack" :: diag
begin

setup Pure_Thy.old_appl_syntax_setup

declare [[unify_trace_bound = 20, unify_search_bound = 40]]

typedecl o

subsection \<open>Sequences\<close>

typedecl seq'
consts
SeqO' :: "[o,seq']\<Rightarrow>seq'"
Seq1' :: "o\seq'"

subsection \<open>Concrete syntax\<close>

nonterminal seq and seqobj and seqcont

syntax
"_SeqEmp"         :: seq                                  ("")
"_SeqApp"         :: "[seqobj,seqcont] \ seq" ("__")

"_SeqContEmp"     :: seqcont                              ("")
"_SeqContApp"     :: "[seqobj,seqcont] \ seqcont" (",/ __")

"_SeqO"           :: "o \ seqobj" ("_")
"_SeqId"          :: "'a \ seqobj" ("$_")

type_synonym single_seqe = "[seq,seqobj] \ prop"
type_synonym single_seqi = "[seq'\seq',seq'\seq'] \ prop"
type_synonym two_seqi = "[seq'\seq', seq'\seq'] \ prop"
type_synonym two_seqe = "[seq, seq] \ prop"
type_synonym three_seqi = "[seq'\seq', seq'\seq', seq'\seq'] \ prop"
type_synonym three_seqe = "[seq, seq, seq] \ prop"
type_synonym four_seqi = "[seq'\seq', seq'\seq', seq'\seq', seq'\seq'] \ prop"
type_synonym four_seqe = "[seq, seq, seq, seq] \ prop"
type_synonym sequence_name = "seq'\seq'"

syntax
  (*Constant to allow definitions of SEQUENCES of formulas*)
  "_Side"        :: "seq\(seq'\seq')" ("<<(_)>>")

ML \<open>

(* parse translation for sequences *)

fun abs_seq' t = Abs ("s", Type (\<^type_name>\seq'\, []), t);

fun seqobj_tr (Const (\<^syntax_const>\<open>_SeqO\<close>, _) $ f) =
      Const (\<^const_syntax>\<open>SeqO'\<close>, dummyT) $ f
  | seqobj_tr (_ $ i) = i;

fun seqcont_tr (Const (\<^syntax_const>\<open>_SeqContEmp\<close>, _)) = Bound 0
  | seqcont_tr (Const (\<^syntax_const>\<open>_SeqContApp\<close>, _) $ so $ sc) =
      seqobj_tr so $ seqcont_tr sc;

fun seq_tr (Const (\<^syntax_const>\<open>_SeqEmp\<close>, _)) = abs_seq' (Bound 0)
  | seq_tr (Const (\<^syntax_const>\<open>_SeqApp\<close>, _) $ so $ sc) =
      abs_seq'(seqobj_tr so $ seqcont_tr sc);

fun singlobj_tr (Const (\<^syntax_const>\<open>_SeqO\<close>,_) $ f) =
  abs_seq' ((Const (\<^const_syntax>\SeqO'\, dummyT) $ f) $ Bound 0);

(* print translation for sequences *)

fun seqcont_tr' (Bound 0) =
      Const (\<^syntax_const>\<open>_SeqContEmp\<close>, dummyT)
  | seqcont_tr' (Const (\<^const_syntax>\SeqO'\, _) $ f $ s) =
      Const (\<^syntax_const>\<open>_SeqContApp\<close>, dummyT) $
        (Const (\<^syntax_const>\<open>_SeqO\<close>, dummyT) $ f) $ seqcont_tr' s
  | seqcont_tr' (i $ s) =
      Const (\<^syntax_const>\<open>_SeqContApp\<close>, dummyT) $
        (Const (\<^syntax_const>\<open>_SeqId\<close>, dummyT) $ i) $ seqcont_tr' s;

fun seq_tr' s =
  let
    fun seq_itr' (Bound 0) = Const (\<^syntax_const>\_SeqEmp\, dummyT)
      | seq_itr' (Const (\<^const_syntax>\SeqO'\, _) $ f $ s) =
          Const (\<^syntax_const>\<open>_SeqApp\<close>, dummyT) $
            (Const (\<^syntax_const>\<open>_SeqO\<close>, dummyT) $ f) $ seqcont_tr' s
      | seq_itr' (i $ s) =
          Const (\<^syntax_const>\<open>_SeqApp\<close>, dummyT) $
            (Const (\<^syntax_const>\<open>_SeqId\<close>, dummyT) $ i) $ seqcont_tr' s
  in
    case s of
      Abs (_, _, t) => seq_itr' t
    | _ => s $ Bound 0
  end;

fun single_tr c [s1, s2] =
  Const (c, dummyT) $ seq_tr s1 $ singlobj_tr s2;

fun two_seq_tr c [s1, s2] =
  Const (c, dummyT) $ seq_tr s1 $ seq_tr s2;

fun three_seq_tr c [s1, s2, s3] =
  Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3;

fun four_seq_tr c [s1, s2, s3, s4] =
  Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4;

fun singlobj_tr' (Const (\<^const_syntax>\SeqO'\,_) $ fm) = fm
  | singlobj_tr' id = Const (\<^syntax_const>\_SeqId\, dummyT) $ id;

fun single_tr' c [s1, s2] =
  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2;

fun two_seq_tr' c [s1, s2] =
  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2;

fun three_seq_tr' c [s1, s2, s3] =
  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3;

fun four_seq_tr' c [s1, s2, s3, s4] =
  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3 $ seq_tr' s4;

(** for the <<...>> notation **)

fun side_tr [s1] = seq_tr s1;
\<close>

parse_translation \<open>[(\<^syntax_const>\<open>_Side\<close>, K side_tr)]\<close>

subsection \<open>Proof tools\<close>

ML_file \<open>prover.ML\<close>

end

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.