src/ZF/Resid/Redex.thy
changeset 22808 a7daa74e2980
parent 16417 9bc16273c2d4
child 32960 69916a850301
     1.1 --- a/src/ZF/Resid/Redex.thy	Thu Apr 26 13:33:17 2007 +0200
     1.2 +++ b/src/ZF/Resid/Redex.thy	Thu Apr 26 14:24:08 2007 +0200
     1.3 @@ -19,21 +19,19 @@
     1.4    Ssub  :: "i"
     1.5    Scomp :: "i"
     1.6    Sreg  :: "i"
     1.7 -  union_aux        :: "i=>i"
     1.8 -  regular          :: "i=>o"
     1.9 -  
    1.10 -(*syntax??*)
    1.11 -  un               :: "[i,i]=>i"  (infixl 70)
    1.12 -  "<=="            :: "[i,i]=>o"  (infixl 70)
    1.13 -  "~"              :: "[i,i]=>o"  (infixl 70)
    1.14 +
    1.15 +abbreviation
    1.16 +  Ssub_rel  (infixl "<==" 70) where
    1.17 +  "a<==b == <a,b> \<in> Ssub"
    1.18  
    1.19 +abbreviation
    1.20 +  Scomp_rel  (infixl "~" 70) where
    1.21 +  "a ~ b == <a,b> \<in> Scomp"
    1.22  
    1.23 -translations
    1.24 -  "a<==b"        == "<a,b> \<in> Ssub"
    1.25 -  "a ~ b"        == "<a,b> \<in> Scomp"
    1.26 -  "regular(a)"   == "a \<in> Sreg"
    1.27 +abbreviation
    1.28 +  "regular(a) == a \<in> Sreg"
    1.29  
    1.30 -
    1.31 +consts union_aux        :: "i=>i"
    1.32  primrec (*explicit lambda is required because both arguments of "un" vary*)
    1.33    "union_aux(Var(n)) =
    1.34       (\<lambda>t \<in> redexes. redexes_case(%j. Var(n), %x. 0, %b x y.0, t))"
    1.35 @@ -47,13 +45,15 @@
    1.36          redexes_case(%j. 0, %y. 0,
    1.37  		     %c z u. App(b or c, union_aux(f)`z, union_aux(a)`u), t))"
    1.38  
    1.39 -defs
    1.40 -  union_def:  "u un v == union_aux(u)`v"
    1.41 +definition
    1.42 +  union  (infixl "un" 70) where
    1.43 +  "u un v == union_aux(u)`v"
    1.44  
    1.45 -syntax (xsymbols)
    1.46 -  "op un"             :: "[i,i]=>i"  (infixl "\<squnion>" 70)
    1.47 -  "op <=="            :: "[i,i]=>o"  (infixl "\<Longleftarrow>" 70)
    1.48 -  "op ~"              :: "[i,i]=>o"  (infixl "\<sim>" 70)
    1.49 +notation (xsymbols)
    1.50 +  union  (infixl "\<squnion>" 70) and
    1.51 +  Ssub_rel  (infixl "\<Longleftarrow>" 70) and
    1.52 +  Scomp_rel  (infixl "\<sim>" 70)
    1.53 +
    1.54  
    1.55  inductive
    1.56    domains       "Ssub" <= "redexes*redexes"