src/ZF/ex/Comb.thy
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 515 abcc438e7c27
child 753 ec86863e87c8
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
     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 = Univ + "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 rules
    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