src/ZF/Resid/Reduction.thy
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 11319 8b84ee2cc79c
     1.1 --- a/src/ZF/Resid/Reduction.thy	Mon Feb 05 21:33:14 1996 +0100
     1.2 +++ b/src/ZF/Resid/Reduction.thy	Tue Feb 06 12:27:17 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	Reduction.thy
     1.5 +(*  Title:      Reduction.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Ole Rasmussen
     1.8 +    Author:     Ole Rasmussen
     1.9      Copyright   1995  University of Cambridge
    1.10      Logic Image: ZF
    1.11  *)
    1.12 @@ -21,39 +21,39 @@
    1.13  inductive
    1.14    domains       "Sred1" <= "lambda*lambda"
    1.15    intrs
    1.16 -    beta	"[|m:lambda; n:lambda|] ==> Apl(Fun(m),n) -1-> n/m"
    1.17 -    rfun  	"[|m -1-> n|] ==> Fun(m) -1-> Fun(n)"
    1.18 -    apl_l	"[|m2:lambda; m1 -1-> n1|] ==>   
    1.19 -		 	          Apl(m1,m2) -1-> Apl(n1,m2)"
    1.20 -    apl_r	"[|m1:lambda; m2 -1-> n2|] ==>   
    1.21 -		 	          Apl(m1,m2) -1-> Apl(m1,n2)"
    1.22 -  type_intrs	"red_typechecks"
    1.23 +    beta        "[|m:lambda; n:lambda|] ==> Apl(Fun(m),n) -1-> n/m"
    1.24 +    rfun        "[|m -1-> n|] ==> Fun(m) -1-> Fun(n)"
    1.25 +    apl_l       "[|m2:lambda; m1 -1-> n1|] ==>   
    1.26 +                                  Apl(m1,m2) -1-> Apl(n1,m2)"
    1.27 +    apl_r       "[|m1:lambda; m2 -1-> n2|] ==>   
    1.28 +                                  Apl(m1,m2) -1-> Apl(m1,n2)"
    1.29 +  type_intrs    "red_typechecks"
    1.30  
    1.31  inductive
    1.32    domains       "Sred" <= "lambda*lambda"
    1.33    intrs
    1.34 -    one_step	"[|m-1->n|] ==> m--->n"
    1.35 -    refl  	"m:lambda==>m --->m"
    1.36 -    trans	"[|m--->n; n--->p|]==>m--->p"
    1.37 -  type_intrs	"[Sred1.dom_subset RS subsetD]@red_typechecks"
    1.38 +    one_step    "[|m-1->n|] ==> m--->n"
    1.39 +    refl        "m:lambda==>m --->m"
    1.40 +    trans       "[|m--->n; n--->p|]==>m--->p"
    1.41 +  type_intrs    "[Sred1.dom_subset RS subsetD]@red_typechecks"
    1.42  
    1.43  inductive
    1.44    domains       "Spar_red1" <= "lambda*lambda"
    1.45    intrs
    1.46 -    beta	"[|m =1=> m';   
    1.47 -		 n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'"
    1.48 -    rvar	"n:nat==> Var(n) =1=> Var(n)"
    1.49 -    rfun	"[|m =1=> m'|]==> Fun(m) =1=> Fun(m')"
    1.50 -    rapl	"[|m =1=> m';   
    1.51 -		 n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')"
    1.52 -  type_intrs	"red_typechecks"
    1.53 +    beta        "[|m =1=> m';   
    1.54 +                 n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'"
    1.55 +    rvar        "n:nat==> Var(n) =1=> Var(n)"
    1.56 +    rfun        "[|m =1=> m'|]==> Fun(m) =1=> Fun(m')"
    1.57 +    rapl        "[|m =1=> m';   
    1.58 +                 n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')"
    1.59 +  type_intrs    "red_typechecks"
    1.60  
    1.61    inductive
    1.62    domains       "Spar_red" <= "lambda*lambda"
    1.63    intrs
    1.64 -    one_step	"[|m =1=> n|] ==> m ===> n"
    1.65 -    trans	"[|m===>n; n===>p|]==>m===>p"
    1.66 -  type_intrs	"[Spar_red1.dom_subset RS subsetD]@red_typechecks"
    1.67 +    one_step    "[|m =1=> n|] ==> m ===> n"
    1.68 +    trans       "[|m===>n; n===>p|]==>m===>p"
    1.69 +  type_intrs    "[Spar_red1.dom_subset RS subsetD]@red_typechecks"
    1.70  
    1.71  
    1.72  end