src/ZF/ex/Comb.thy
 author clasohm Tue Feb 06 12:27:17 1996 +0100 (1996-02-06) changeset 1478 2b8c2a7547ab parent 1401 0c439768f45c child 1702 4aa538e82f76 permissions -rw-r--r--
expanded tabs
```     1 (*  Title:      ZF/ex/Comb.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson
```
```     4     Copyright   1994  University of Cambridge
```
```     5
```
```     6 Combinatory Logic example: the Church-Rosser Theorem
```
```     7 Curiously, combinators do not include free variables.
```
```     8
```
```     9 Example taken from
```
```    10     J. Camilleri and T. F. Melham.
```
```    11     Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
```
```    12     Report 265, University of Cambridge Computer Laboratory, 1992.
```
```    13 *)
```
```    14
```
```    15
```
```    16 Comb = Datatype +
```
```    17
```
```    18 (** Datatype definition of combinators S and K, with infixed application **)
```
```    19 consts comb :: i
```
```    20 datatype (* <= "univ(0)" *)
```
```    21   "comb" = K
```
```    22          | S
```
```    23          | "#" ("p: comb", "q: comb")   (infixl 90)
```
```    24
```
```    25 (** Inductive definition of contractions, -1->
```
```    26              and (multi-step) reductions, --->
```
```    27 **)
```
```    28 consts
```
```    29   contract  :: i
```
```    30   "-1->"    :: [i,i] => o                       (infixl 50)
```
```    31   "--->"    :: [i,i] => o                       (infixl 50)
```
```    32
```
```    33 translations
```
```    34   "p -1-> q" == "<p,q> : contract"
```
```    35   "p ---> q" == "<p,q> : contract^*"
```
```    36
```
```    37 inductive
```
```    38   domains   "contract" <= "comb*comb"
```
```    39   intrs
```
```    40     K     "[| p:comb;  q:comb |] ==> K#p#q -1-> p"
```
```    41     S     "[| p:comb;  q:comb;  r:comb |] ==> S#p#q#r -1-> (p#r)#(q#r)"
```
```    42     Ap1   "[| p-1->q;  r:comb |] ==> p#r -1-> q#r"
```
```    43     Ap2   "[| p-1->q;  r:comb |] ==> r#p -1-> r#q"
```
```    44   type_intrs "comb.intrs"
```
```    45
```
```    46
```
```    47 (** Inductive definition of parallel contractions, =1=>
```
```    48              and (multi-step) parallel reductions, ===>
```
```    49 **)
```
```    50 consts
```
```    51   parcontract :: i
```
```    52   "=1=>"    :: [i,i] => o                       (infixl 50)
```
```    53   "===>"    :: [i,i] => o                       (infixl 50)
```
```    54
```
```    55 translations
```
```    56   "p =1=> q" == "<p,q> : parcontract"
```
```    57   "p ===> q" == "<p,q> : parcontract^+"
```
```    58
```
```    59 inductive
```
```    60   domains   "parcontract" <= "comb*comb"
```
```    61   intrs
```
```    62     refl  "[| p:comb |] ==> p =1=> p"
```
```    63     K     "[| p:comb;  q:comb |] ==> K#p#q =1=> p"
```
```    64     S     "[| p:comb;  q:comb;  r:comb |] ==> S#p#q#r =1=> (p#r)#(q#r)"
```
```    65     Ap    "[| p=1=>q;  r=1=>s |] ==> p#r =1=> q#s"
```
```    66   type_intrs "comb.intrs"
```
```    67
```
```    68
```
```    69 (*Misc definitions*)
```
```    70 consts
```
```    71   diamond   :: i => o
```
```    72   I         :: i
```
```    73
```
```    74 defs
```
```    75
```
```    76   diamond_def "diamond(r) == ALL x y. <x,y>:r -->
```
```    77                             (ALL y'. <x,y'>:r -->
```
```    78                                  (EX z. <y,z>:r & <y',z> : r))"
```
```    79
```
```    80   I_def       "I == S#K#K"
```
```    81
```
```    82 end
```