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