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
lcp@515
     1
(*  Title: 	ZF/ex/Comb.thy
lcp@515
     2
    ID:         $Id$
lcp@515
     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@515
    16
Comb = Univ + "Datatype" +
lcp@515
    17
lcp@515
    18
(** Datatype definition of combinators S and K, with infixed application **)
lcp@515
    19
consts comb :: "i"
lcp@515
    20
datatype (* <= "univ(0)" *)
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
lcp@515
    29
  contract  :: "i"
lcp@515
    30
  "-1->"    :: "[i,i] => o"    			(infixl 50)
lcp@515
    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
lcp@515
    51
  parcontract :: "i"
lcp@515
    52
  "=1=>"    :: "[i,i] => o"    			(infixl 50)
lcp@515
    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*)
lcp@515
    70
consts
lcp@515
    71
  diamond   :: "i => o"
lcp@515
    72
  I         :: "i"
lcp@515
    73
lcp@515
    74
rules
lcp@515
    75
lcp@515
    76
  diamond_def "diamond(r) == ALL x y. <x,y>:r --> \
lcp@515
    77
\                            (ALL y'. <x,y'>:r --> \
lcp@515
    78
\                                 (EX z. <y,z>:r & <y',z> : r))"
lcp@515
    79
lcp@515
    80
  I_def       "I == S#K#K"
lcp@515
    81
lcp@515
    82
end