src/HOL/Induct/Comb.thy
author paulson
Wed May 07 12:50:26 1997 +0200 (1997-05-07)
changeset 3120 c58423c20740
child 3309 992a25b24d0d
permissions -rw-r--r--
New directory to contain examples of (co)inductive definitions
paulson@3120
     1
(*  Title:      HOL/ex/Comb.thy
paulson@3120
     2
    ID:         $Id$
paulson@3120
     3
    Author:     Lawrence C Paulson
paulson@3120
     4
    Copyright   1996  University of Cambridge
paulson@3120
     5
paulson@3120
     6
Combinatory Logic example: the Church-Rosser Theorem
paulson@3120
     7
Curiously, combinators do not include free variables.
paulson@3120
     8
paulson@3120
     9
Example taken from
paulson@3120
    10
    J. Camilleri and T. F. Melham.
paulson@3120
    11
    Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
paulson@3120
    12
    Report 265, University of Cambridge Computer Laboratory, 1992.
paulson@3120
    13
*)
paulson@3120
    14
paulson@3120
    15
paulson@3120
    16
Comb = Trancl +
paulson@3120
    17
paulson@3120
    18
(** Datatype definition of combinators S and K, with infixed application **)
paulson@3120
    19
datatype comb = K
paulson@3120
    20
              | S
paulson@3120
    21
              | "#" comb comb (infixl 90)
paulson@3120
    22
paulson@3120
    23
(** Inductive definition of contractions, -1->
paulson@3120
    24
             and (multi-step) reductions, --->
paulson@3120
    25
**)
paulson@3120
    26
consts
paulson@3120
    27
  contract  :: "(comb*comb) set"
paulson@3120
    28
  "-1->"    :: [comb,comb] => bool   (infixl 50)
paulson@3120
    29
  "--->"    :: [comb,comb] => bool   (infixl 50)
paulson@3120
    30
paulson@3120
    31
translations
paulson@3120
    32
  "x -1-> y" == "(x,y) : contract"
paulson@3120
    33
  "x ---> y" == "(x,y) : contract^*"
paulson@3120
    34
paulson@3120
    35
inductive contract
paulson@3120
    36
  intrs
paulson@3120
    37
    K     "K#x#y -1-> x"
paulson@3120
    38
    S     "S#x#y#z -1-> (x#z)#(y#z)"
paulson@3120
    39
    Ap1   "x-1->y ==> x#z -1-> y#z"
paulson@3120
    40
    Ap2   "x-1->y ==> z#x -1-> z#y"
paulson@3120
    41
paulson@3120
    42
paulson@3120
    43
(** Inductive definition of parallel contractions, =1=>
paulson@3120
    44
             and (multi-step) parallel reductions, ===>
paulson@3120
    45
**)
paulson@3120
    46
consts
paulson@3120
    47
  parcontract :: "(comb*comb) set"
paulson@3120
    48
  "=1=>"    :: [comb,comb] => bool   (infixl 50)
paulson@3120
    49
  "===>"    :: [comb,comb] => bool   (infixl 50)
paulson@3120
    50
paulson@3120
    51
translations
paulson@3120
    52
  "x =1=> y" == "(x,y) : parcontract"
paulson@3120
    53
  "x ===> y" == "(x,y) : parcontract^*"
paulson@3120
    54
paulson@3120
    55
inductive parcontract
paulson@3120
    56
  intrs
paulson@3120
    57
    refl  "x =1=> x"
paulson@3120
    58
    K     "K#x#y =1=> x"
paulson@3120
    59
    S     "S#x#y#z =1=> (x#z)#(y#z)"
paulson@3120
    60
    Ap    "[| x=1=>y;  z=1=>w |] ==> x#z =1=> y#w"
paulson@3120
    61
paulson@3120
    62
paulson@3120
    63
(*Misc definitions*)
paulson@3120
    64
constdefs
paulson@3120
    65
  I :: comb
paulson@3120
    66
  "I == S#K#K"
paulson@3120
    67
paulson@3120
    68
  (*confluence; Lambda/Commutation treats this more abstractly*)
paulson@3120
    69
  diamond   :: "('a * 'a)set => bool"	
paulson@3120
    70
  "diamond(r) == ALL x y. (x,y):r --> 
paulson@3120
    71
                  (ALL y'. (x,y'):r --> 
paulson@3120
    72
                    (EX z. (y,z):r & (y',z) : r))"
paulson@3120
    73
paulson@3120
    74
end