src/ZF/Resid/Reduction.thy
author clasohm
Sat Dec 09 13:36:11 1995 +0100 (1995-12-09 ago)
changeset 1401 0c439768f45c
parent 1155 928a16e02f9f
child 1478 2b8c2a7547ab
permissions -rw-r--r--
removed quotes from consts and syntax sections
lcp@1048
     1
(*  Title: 	Reduction.thy
lcp@1048
     2
    ID:         $Id$
lcp@1048
     3
    Author: 	Ole Rasmussen
lcp@1048
     4
    Copyright   1995  University of Cambridge
lcp@1048
     5
    Logic Image: ZF
lcp@1048
     6
*)
lcp@1048
     7
lcp@1048
     8
Reduction = Terms+
lcp@1048
     9
lcp@1048
    10
consts
clasohm@1401
    11
  Sred1, Sred,  Spar_red1,Spar_red    :: i
clasohm@1401
    12
  "-1->","--->","=1=>",   "===>"      :: [i,i]=>o (infixl 50)
lcp@1048
    13
lcp@1048
    14
translations
lcp@1048
    15
  "a -1-> b" == "<a,b>:Sred1"
lcp@1048
    16
  "a ---> b" == "<a,b>:Sred"
lcp@1048
    17
  "a =1=> b" == "<a,b>:Spar_red1"
lcp@1048
    18
  "a ===> b" == "<a,b>:Spar_red"
lcp@1048
    19
  
lcp@1048
    20
  
lcp@1048
    21
inductive
lcp@1048
    22
  domains       "Sred1" <= "lambda*lambda"
lcp@1048
    23
  intrs
lcp@1048
    24
    beta	"[|m:lambda; n:lambda|] ==> Apl(Fun(m),n) -1-> n/m"
lcp@1048
    25
    rfun  	"[|m -1-> n|] ==> Fun(m) -1-> Fun(n)"
clasohm@1155
    26
    apl_l	"[|m2:lambda; m1 -1-> n1|] ==>   
clasohm@1155
    27
		 	          Apl(m1,m2) -1-> Apl(n1,m2)"
clasohm@1155
    28
    apl_r	"[|m1:lambda; m2 -1-> n2|] ==>   
clasohm@1155
    29
		 	          Apl(m1,m2) -1-> Apl(m1,n2)"
lcp@1048
    30
  type_intrs	"red_typechecks"
lcp@1048
    31
lcp@1048
    32
inductive
lcp@1048
    33
  domains       "Sred" <= "lambda*lambda"
lcp@1048
    34
  intrs
lcp@1048
    35
    one_step	"[|m-1->n|] ==> m--->n"
lcp@1048
    36
    refl  	"m:lambda==>m --->m"
lcp@1048
    37
    trans	"[|m--->n; n--->p|]==>m--->p"
lcp@1048
    38
  type_intrs	"[Sred1.dom_subset RS subsetD]@red_typechecks"
lcp@1048
    39
lcp@1048
    40
inductive
lcp@1048
    41
  domains       "Spar_red1" <= "lambda*lambda"
lcp@1048
    42
  intrs
clasohm@1155
    43
    beta	"[|m =1=> m';   
clasohm@1155
    44
		 n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'"
lcp@1048
    45
    rvar	"n:nat==> Var(n) =1=> Var(n)"
lcp@1048
    46
    rfun	"[|m =1=> m'|]==> Fun(m) =1=> Fun(m')"
clasohm@1155
    47
    rapl	"[|m =1=> m';   
clasohm@1155
    48
		 n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')"
lcp@1048
    49
  type_intrs	"red_typechecks"
lcp@1048
    50
lcp@1048
    51
  inductive
lcp@1048
    52
  domains       "Spar_red" <= "lambda*lambda"
lcp@1048
    53
  intrs
lcp@1048
    54
    one_step	"[|m =1=> n|] ==> m ===> n"
lcp@1048
    55
    trans	"[|m===>n; n===>p|]==>m===>p"
lcp@1048
    56
  type_intrs	"[Spar_red1.dom_subset RS subsetD]@red_typechecks"
lcp@1048
    57
lcp@1048
    58
lcp@1048
    59
end
lcp@1048
    60