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