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