src/ZF/Resid/Conversion.thy

tuned;
prepare ext;

(*  Title:      Conversion.thy
    ID:         $Id$
    Author:     Ole Rasmussen
    Copyright   1995  University of Cambridge
    Logic Image: ZF

*)

Conversion = Confluence+

consts
  Sconv1        :: i
  "<-1->"       :: [i,i]=>o (infixl 50)
  Sconv         :: i
  "<--->"       :: [i,i]=>o (infixl 50)

translations
  "a<-1->b"    == "<a,b>:Sconv1"
  "a<--->b"    == "<a,b>:Sconv"
  
inductive
  domains       "Sconv1" <= "lambda*lambda"
  intrs
    red1        "m -1-> n ==> m<-1->n"
    expl        "n -1-> m ==> m<-1->n"
  type_intrs    "[red1D1,red1D2]@lambda.intrs@bool_typechecks"

inductive
  domains       "Sconv" <= "lambda*lambda"
  intrs
    one_step    "m<-1->n  ==> m<--->n"
    refl        "m:lambda ==> m<--->m"
    trans       "[|m<--->n; n<--->p|] ==> m<--->p"
  type_intrs    "[Sconv1.dom_subset RS subsetD]@lambda.intrs@bool_typechecks"
end