src/HOL/Lambda/Type.thy
changeset 19363 667b5ea637dd
parent 19086 1b3780be6cc2
child 19380 b808efaa5828
     1.1 --- a/src/HOL/Lambda/Type.thy	Sat Apr 08 22:12:02 2006 +0200
     1.2 +++ b/src/HOL/Lambda/Type.thy	Sat Apr 08 22:51:06 2006 +0200
     1.3 @@ -14,10 +14,14 @@
     1.4  definition
     1.5    shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_<_:_>" [90, 0, 0] 91)
     1.6    "e<i:a> = (\<lambda>j. if j < i then e j else if j = i then a else e (j - 1))"
     1.7 -syntax (xsymbols)
     1.8 -  shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
     1.9 -syntax (HTML output)
    1.10 -  shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
    1.11 +
    1.12 +abbreviation (xsymbols)
    1.13 +  shift  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
    1.14 +  "e\<langle>i:a\<rangle> == e<i:a>"
    1.15 +
    1.16 +abbreviation (HTML output)
    1.17 +  shift  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
    1.18 +  "shift == xsymbols.shift"
    1.19  
    1.20  lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T"
    1.21    by (simp add: shift_def)
    1.22 @@ -47,23 +51,27 @@
    1.23    typing :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set"
    1.24    typings :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
    1.25  
    1.26 -abbreviation (output)
    1.27 +abbreviation
    1.28    funs :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "=>>" 200)
    1.29 -  "Ts =>> T = foldr Fun Ts T"
    1.30 +  "Ts =>> T == foldr Fun Ts T"
    1.31  
    1.32    typing_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ |- _ : _" [50, 50, 50] 50)
    1.33 -  "(env |- t : T) = ((env, t, T) \<in> typing)"
    1.34 +  "env |- t : T == (env, t, T) \<in> typing"
    1.35  
    1.36    typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
    1.37      ("_ ||- _ : _" [50, 50, 50] 50)
    1.38 -  "(env ||- ts : Ts) = typings env ts Ts"
    1.39 +  "env ||- ts : Ts == typings env ts Ts"
    1.40  
    1.41 -syntax (xsymbols)
    1.42 +abbreviation (xsymbols)
    1.43    typing_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile> _ : _" [50, 50, 50] 50)
    1.44 -syntax (latex)
    1.45 +  "env \<turnstile> t : T == env |- t : T"
    1.46 +
    1.47 +abbreviation (latex)
    1.48    funs :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "\<Rrightarrow>" 200)
    1.49 +  "op \<Rrightarrow> == op =>>"
    1.50    typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
    1.51      ("_ \<tturnstile> _ : _" [50, 50, 50] 50)
    1.52 +  "env \<tturnstile> ts : Ts == env ||- ts : Ts"
    1.53  
    1.54  inductive typing
    1.55    intros