Sara Kalvala: moving the <<...>> notation from LK to Sequents
authorpaulson
Tue Aug 03 13:16:29 1999 +0200 (1999-08-03)
changeset 7166a4a870ec2e67
parent 7165 8c937127fd8c
child 7167 0b2e3ef1d8f4
Sara Kalvala: moving the <<...>> notation from LK to Sequents
src/Sequents/LK0.thy
src/Sequents/Sequents.thy
     1.1 --- a/src/Sequents/LK0.thy	Tue Aug 03 13:15:54 1999 +0200
     1.2 +++ b/src/Sequents/LK0.thy	Tue Aug 03 13:16:29 1999 +0200
     1.3 @@ -24,9 +24,6 @@
     1.4   Trueprop	:: "two_seqi"
     1.5   "@Trueprop"	:: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
     1.6  
     1.7 -  (*Constant to allow definitions of SEQUENCES of formulas*)
     1.8 -  "@Side"        :: "seq=>(seq'=>seq')"     ("<<(_)>>")
     1.9 -
    1.10    True,False   :: o
    1.11    "="          :: ['a,'a] => o       (infixl 50)
    1.12    Not          :: o => o             ("~ _" [40] 40)
    1.13 @@ -138,9 +135,7 @@
    1.14  
    1.15  ML
    1.16  
    1.17 -fun side_tr [s1] = Sequents.seq_tr s1;
    1.18  
    1.19 -val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop"),
    1.20 -			 ("@Side", side_tr)];
    1.21 +val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop")];
    1.22  val print_translation = [("Trueprop",Sequents.two_seq_tr' "@Trueprop")];
    1.23  
     2.1 --- a/src/Sequents/Sequents.thy	Tue Aug 03 13:15:54 1999 +0200
     2.2 +++ b/src/Sequents/Sequents.thy	Tue Aug 03 13:16:29 1999 +0200
     2.3 @@ -3,7 +3,8 @@
     2.4      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     2.5      Copyright   1993  University of Cambridge
     2.6  
     2.7 -Classical First-Order Sequent Calculus
     2.8 +Basis theory for parsing and pretty-printing of sequences to be used in
     2.9 +Sequent Calculi. 
    2.10  *)
    2.11  
    2.12  Sequents = Pure +
    2.13 @@ -23,8 +24,8 @@
    2.14   seq'
    2.15  
    2.16  consts
    2.17 - SeqO'         :: "[o,seq']=>seq'"
    2.18 - Seq1'         :: "o=>seq'"
    2.19 + SeqO'         :: [o,seq']=>seq'
    2.20 + Seq1'         :: o=>seq'
    2.21      
    2.22  
    2.23  (* concrete syntax *)
    2.24 @@ -34,25 +35,33 @@
    2.25  
    2.26  
    2.27  syntax
    2.28 - SeqEmp         :: "seq"                                ("")
    2.29 - SeqApp         :: "[seqobj,seqcont] => seq"            ("__")
    2.30 + SeqEmp         :: seq                                ("")
    2.31 + SeqApp         :: [seqobj,seqcont] => seq            ("__")
    2.32  
    2.33 - SeqContEmp     :: "seqcont"                            ("")
    2.34 - SeqContApp     :: "[seqobj,seqcont] => seqcont"        (",/ __")
    2.35 + SeqContEmp     :: seqcont                            ("")
    2.36 + SeqContApp     :: [seqobj,seqcont] => seqcont        (",/ __")
    2.37    
    2.38 - SeqO           :: "o => seqobj"                        ("_")
    2.39 - SeqId          :: "'a => seqobj"                       ("$_")
    2.40 + SeqO           :: o => seqobj                        ("_")
    2.41 + SeqId          :: 'a => seqobj                       ("$_")
    2.42  
    2.43  types
    2.44      
    2.45 - single_seqe = "[seq,seqobj] => prop"
    2.46 - single_seqi = "[seq'=>seq',seq'=>seq'] => prop"
    2.47 - two_seqi = "[seq'=>seq', seq'=>seq'] => prop"
    2.48 - two_seqe = "[seq, seq] => prop"
    2.49 - three_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
    2.50 - three_seqe = "[seq, seq, seq] => prop"
    2.51 - four_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
    2.52 - four_seqe = "[seq, seq, seq, seq] => prop"
    2.53 + single_seqe = [seq,seqobj] => prop
    2.54 + single_seqi = [seq'=>seq',seq'=>seq'] => prop
    2.55 + two_seqi    = [seq'=>seq', seq'=>seq'] => prop
    2.56 + two_seqe    = [seq, seq] => prop
    2.57 + three_seqi  = [seq'=>seq', seq'=>seq', seq'=>seq'] => prop
    2.58 + three_seqe  = [seq, seq, seq] => prop
    2.59 + four_seqi   = [seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop
    2.60 + four_seqe   = [seq, seq, seq, seq] => prop
    2.61 +
    2.62 +
    2.63 + sequence_name = seq'=>seq'
    2.64 +
    2.65 +
    2.66 +consts
    2.67 +  (*Constant to allow definitions of SEQUENCES of formulas*)
    2.68 +  "@Side"        :: seq=>(seq'=>seq')     ("<<(_)>>")
    2.69  
    2.70  end
    2.71  
    2.72 @@ -146,3 +155,8 @@
    2.73  
    2.74  
    2.75  			 
    2.76 +(** for the <<...>> notation **)
    2.77 +  
    2.78 +fun side_tr [s1] = seq_tr s1;
    2.79 +
    2.80 +val parse_translation = [("@Side", side_tr)];