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