|
1048
|
1 |
(* Title: Conversion.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Ole Rasmussen
|
|
|
4 |
Copyright 1995 University of Cambridge
|
|
|
5 |
Logic Image: ZF
|
|
|
6 |
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
Conversion = Confluence+
|
|
|
10 |
|
|
|
11 |
consts
|
|
|
12 |
Sconv1 :: "i"
|
|
|
13 |
"<-1->" :: "[i,i]=>o" (infixl 50)
|
|
|
14 |
Sconv :: "i"
|
|
|
15 |
"<--->" :: "[i,i]=>o" (infixl 50)
|
|
|
16 |
|
|
|
17 |
translations
|
|
|
18 |
"a<-1->b" == "<a,b>:Sconv1"
|
|
|
19 |
"a<--->b" == "<a,b>:Sconv"
|
|
|
20 |
|
|
|
21 |
inductive
|
|
|
22 |
domains "Sconv1" <= "lambda*lambda"
|
|
|
23 |
intrs
|
|
|
24 |
red1 "m -1-> n ==> m<-1->n"
|
|
|
25 |
expl "n -1-> m ==> m<-1->n"
|
|
|
26 |
type_intrs "[red1D1,red1D2]@lambda.intrs@bool_typechecks"
|
|
|
27 |
|
|
|
28 |
inductive
|
|
|
29 |
domains "Sconv" <= "lambda*lambda"
|
|
|
30 |
intrs
|
|
|
31 |
one_step "m<-1->n ==> m<--->n"
|
|
|
32 |
refl "m:lambda ==> m<--->m"
|
|
|
33 |
trans "[|m<--->n; n<--->p|] ==> m<--->p"
|
|
|
34 |
type_intrs "[Sconv1.dom_subset RS subsetD]@lambda.intrs@bool_typechecks"
|
|
|
35 |
end
|
|
|
36 |
|