proper use of 'syntax';
authorwenzelm
Fri May 21 21:14:18 2004 +0200 (2004-05-21)
changeset 14765bafb24c150c1
parent 14764 5d8a9900cabc
child 14766 c0401da7726d
proper use of 'syntax';
src/CCL/Term.thy
src/CCL/Type.thy
src/CTT/CTT.thy
src/HOL/Induct/SList.thy
src/Sequents/ILL.thy
src/Sequents/LK0.thy
src/Sequents/Modal0.thy
src/Sequents/S43.thy
src/Sequents/Sequents.thy
     1.1 --- a/src/CCL/Term.thy	Wed May 19 11:41:58 2004 +0200
     1.2 +++ b/src/CCL/Term.thy	Fri May 21 21:14:18 2004 +0200
     1.3 @@ -37,6 +37,7 @@
     1.4    letrec2    :: "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i"
     1.5    letrec3    :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i"  
     1.6  
     1.7 +syntax
     1.8    "@let"     :: "[idt,i,i]=>i"             ("(3let _ be _/ in _)"
     1.9                          [0,0,60] 60)
    1.10  
    1.11 @@ -49,6 +50,7 @@
    1.12    "@letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)"
    1.13                          [0,0,0,0,0,60] 60)
    1.14  
    1.15 +consts
    1.16    napply     :: "[i=>i,i,i]=>i"            ("(_ ^ _ ` _)" [56,56,56] 56)
    1.17  
    1.18  rules
     2.1 --- a/src/CCL/Type.thy	Wed May 19 11:41:58 2004 +0200
     2.2 +++ b/src/CCL/Type.thy	Fri May 21 21:14:18 2004 +0200
     2.3 @@ -27,6 +27,7 @@
     2.4  
     2.5    SPLIT         :: "[i, [i, i] => i set] => i set"
     2.6  
     2.7 +syntax
     2.8    "@Pi"         :: "[idt, i set, i set] => i set"    ("(3PROD _:_./ _)"
     2.9                                  [0,0,60] 60)
    2.10  
     3.1 --- a/src/CTT/CTT.thy	Wed May 19 11:41:58 2004 +0200
     3.2 +++ b/src/CTT/CTT.thy	Fri May 21 21:14:18 2004 +0200
     3.3 @@ -34,6 +34,8 @@
     3.4    split     :: "[i, [i,i]=>i] =>i"
     3.5    (*General Product and Function Space*)
     3.6    Prod      :: "[t, i=>t]=>t"
     3.7 +  (*Types*)
     3.8 +  "+"       :: "[t,t]=>t"           (infixr 40)
     3.9    (*Equality type*)
    3.10    Eq        :: "[t,i,i]=>t"
    3.11    eq        :: "i"
    3.12 @@ -44,12 +46,7 @@
    3.13    Eqelem    :: "[i,i,t]=>prop"      ("(_ =/ _ :/ _)" [10,10,10] 5)
    3.14    Reduce    :: "[i,i]=>prop"        ("Reduce[_,_]")
    3.15    (*Types*)
    3.16 -  "@PROD"   :: "[idt,t,t]=>t"       ("(3PROD _:_./ _)" 10)
    3.17 -  "@SUM"    :: "[idt,t,t]=>t"       ("(3SUM _:_./ _)" 10)
    3.18 -  "+"       :: "[t,t]=>t"           (infixr 40)
    3.19 -  (*Invisible infixes!*)
    3.20 -  "@-->"    :: "[t,t]=>t"           ("(_ -->/ _)" [31,30] 30)
    3.21 -  "@*"      :: "[t,t]=>t"           ("(_ */ _)" [51,50] 50)
    3.22 +
    3.23    (*Functions*)
    3.24    lambda    :: "(i => i) => i"      (binder "lam " 10)
    3.25    "`"       :: "[i,i]=>i"           (infixl 60)
    3.26 @@ -58,6 +55,12 @@
    3.27    (*Pairing*)
    3.28    pair      :: "[i,i]=>i"           ("(1<_,/_>)")
    3.29  
    3.30 +syntax
    3.31 +  "@PROD"   :: "[idt,t,t]=>t"       ("(3PROD _:_./ _)" 10)
    3.32 +  "@SUM"    :: "[idt,t,t]=>t"       ("(3SUM _:_./ _)" 10)
    3.33 +  "@-->"    :: "[t,t]=>t"           ("(_ -->/ _)" [31,30] 30)
    3.34 +  "@*"      :: "[t,t]=>t"           ("(_ */ _)" [51,50] 50)
    3.35 +
    3.36  translations
    3.37    "PROD x:A. B" => "Prod(A, %x. B)"
    3.38    "A --> B"     => "Prod(A, _K(B))"
     4.1 --- a/src/HOL/Induct/SList.thy	Wed May 19 11:41:58 2004 +0200
     4.2 +++ b/src/HOL/Induct/SList.thy	Fri May 21 21:14:18 2004 +0200
     4.3 @@ -90,6 +90,7 @@
     4.4  (* list Enumeration *)
     4.5  consts
     4.6    "[]"      :: "'a list"                            ("[]")
     4.7 +syntax
     4.8    "@list"   :: "args => 'a list"                    ("[(_)]")
     4.9  
    4.10  translations
     5.1 --- a/src/Sequents/ILL.thy	Wed May 19 11:41:58 2004 +0200
     5.2 +++ b/src/Sequents/ILL.thy	Fri May 21 21:14:18 2004 +0200
     5.3 @@ -8,12 +8,7 @@
     5.4  ILL = Sequents +
     5.5  
     5.6  consts
     5.7 -
     5.8 -  
     5.9 - Trueprop	:: "two_seqi"
    5.10 - "@Trueprop"	:: "single_seqe" ("((_)/ |- (_))" [6,6] 5)
    5.11 - 
    5.12 - 
    5.13 +  Trueprop       :: "two_seqi"
    5.14  
    5.15  "><"    ::"[o, o] => o"        (infixr 35)
    5.16  "-o"    ::"[o, o] => o"        (infixr 45)
    5.17 @@ -27,15 +22,18 @@
    5.18  aneg    ::"o=>o"               ("~_")
    5.19  
    5.20  
    5.21 -  (* syntax for context manipulation *)
    5.22 +  (* context manipulation *)
    5.23  
    5.24   Context      :: "two_seqi"
    5.25 -"@Context"    :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)
    5.26  
    5.27 -  (* syntax for promotion rule *)
    5.28 +  (* promotion rule *)
    5.29  
    5.30    PromAux :: "three_seqi"
    5.31 -"@PromAux":: "three_seqe" ("promaux {_||_||_}")
    5.32 +
    5.33 +syntax
    5.34 +  "@Trueprop" :: "single_seqe" ("((_)/ |- (_))" [6,6] 5)
    5.35 +  "@Context"  :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)
    5.36 +  "@PromAux"  :: "three_seqe" ("promaux {_||_||_}")
    5.37  
    5.38  defs
    5.39  
    5.40 @@ -47,7 +45,7 @@
    5.41  
    5.42  
    5.43  rules
    5.44 -  
    5.45 +
    5.46  identity        "P |- P"
    5.47  
    5.48  zerol           "$G, 0, $H |- A"
    5.49 @@ -58,7 +56,7 @@
    5.50    (* unfortunately, this one removes !A  *)
    5.51  
    5.52  contract  "$F, !A, !A, $G |- C ==> $F, !A, $G |- C"
    5.53 -  
    5.54 +
    5.55  weaken     "$F, $G |- C ==> $G, !A, $F |- C"
    5.56    (* weak form of weakening, in practice just to clean context *)
    5.57    (* weaken and contract not needed (CHECK)  *)
    5.58 @@ -69,7 +67,7 @@
    5.59  promote0        "$G |- A ==> promaux {$G || || A}"
    5.60  
    5.61  
    5.62 -  
    5.63 +
    5.64  tensl     "$H, A, B, $G |- C ==> $H, A >< B, $G |- C"
    5.65  
    5.66  impr      "A, $F |- B ==> $F |- A -o B"
    5.67 @@ -101,7 +99,7 @@
    5.68                         $G |- A |]
    5.69                      ==> $J, A -o B, $H |- C"
    5.70  
    5.71 -    
    5.72 +
    5.73  cut " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
    5.74           $H1, $H2, $H3, $H4 |- A ;
    5.75           $J1, $J2, A, $J3, $J4 |- B |]  ==> $F |- B"
    5.76 @@ -118,7 +116,7 @@
    5.77  
    5.78  
    5.79  
    5.80 - 
    5.81 +
    5.82  end
    5.83  
    5.84  ML
    5.85 @@ -131,4 +129,4 @@
    5.86                           ("Context",Sequents.two_seq_tr'"@Context"),
    5.87                           ("PromAux", Sequents.three_seq_tr'"@PromAux")];
    5.88  
    5.89 - 
    5.90 +
     6.1 --- a/src/Sequents/LK0.thy	Wed May 19 11:41:58 2004 +0200
     6.2 +++ b/src/Sequents/LK0.thy	Fri May 21 21:14:18 2004 +0200
     6.3 @@ -22,7 +22,6 @@
     6.4  consts
     6.5  
     6.6   Trueprop	:: "two_seqi"
     6.7 - "@Trueprop"	:: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
     6.8  
     6.9    True,False   :: o
    6.10    "="          :: ['a,'a] => o       (infixl 50)
    6.11 @@ -35,6 +34,7 @@
    6.12    Ex           :: ('a => o) => o     (binder "EX " 10)
    6.13  
    6.14  syntax
    6.15 + "@Trueprop"	:: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
    6.16    "_not_equal" :: ['a, 'a] => o                (infixl "~=" 50)
    6.17  
    6.18  translations
     7.1 --- a/src/Sequents/Modal0.thy	Wed May 19 11:41:58 2004 +0200
     7.2 +++ b/src/Sequents/Modal0.thy	Fri May 21 21:14:18 2004 +0200
     7.3 @@ -10,9 +10,11 @@
     7.4    box           :: "o=>o"       ("[]_" [50] 50)
     7.5    dia           :: "o=>o"       ("<>_" [50] 50)
     7.6    "--<",">-<"   :: "[o,o]=>o"   (infixr 25)
     7.7 +  Lstar,Rstar   :: "two_seqi"
     7.8 +
     7.9 +syntax
    7.10    "@Lstar"      :: "two_seqe"   ("(_)|L>(_)" [6,6] 5)
    7.11    "@Rstar"      :: "two_seqe"   ("(_)|R>(_)" [6,6] 5)
    7.12 -  Lstar,Rstar   :: "two_seqi"
    7.13  
    7.14  rules
    7.15    (* Definitions *)
     8.1 --- a/src/Sequents/S43.thy	Wed May 19 11:41:58 2004 +0200
     8.2 +++ b/src/Sequents/S43.thy	Fri May 21 21:14:18 2004 +0200
     8.3 @@ -11,6 +11,7 @@
     8.4  consts
     8.5    S43pi :: "[seq'=>seq', seq'=>seq', seq'=>seq',
     8.6               seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
     8.7 +syntax
     8.8    "@S43pi" :: "[seq, seq, seq, seq, seq, seq] => prop"
     8.9                           ("S43pi((_);(_);(_);(_);(_);(_))" [] 5)
    8.10  
     9.1 --- a/src/Sequents/Sequents.thy	Wed May 19 11:41:58 2004 +0200
     9.2 +++ b/src/Sequents/Sequents.thy	Fri May 21 21:14:18 2004 +0200
     9.3 @@ -30,7 +30,7 @@
     9.4  
     9.5  (* concrete syntax *)
     9.6  
     9.7 -types
     9.8 +nonterminals
     9.9    seq seqobj seqcont
    9.10  
    9.11  
    9.12 @@ -59,7 +59,7 @@
    9.13   sequence_name = seq'=>seq'
    9.14  
    9.15  
    9.16 -consts
    9.17 +syntax
    9.18    (*Constant to allow definitions of SEQUENCES of formulas*)
    9.19    "@Side"        :: seq=>(seq'=>seq')     ("<<(_)>>")
    9.20