src/ZF/ex/Comb.thy
 author clasohm Tue Feb 06 12:27:17 1996 +0100 (1996-02-06) changeset 1478 2b8c2a7547ab parent 1401 0c439768f45c child 1702 4aa538e82f76 permissions -rw-r--r--
expanded tabs
1 (*  Title:      ZF/ex/Comb.thy
2     ID:         \$Id\$
3     Author:     Lawrence C Paulson
4     Copyright   1994  University of Cambridge
6 Combinatory Logic example: the Church-Rosser Theorem
7 Curiously, combinators do not include free variables.
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 *)
16 Comb = Datatype +
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)
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)
33 translations
34   "p -1-> q" == "<p,q> : contract"
35   "p ---> q" == "<p,q> : contract^*"
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"
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)
55 translations
56   "p =1=> q" == "<p,q> : parcontract"
57   "p ===> q" == "<p,q> : parcontract^+"
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"
69 (*Misc definitions*)
70 consts
71   diamond   :: i => o
72   I         :: i
74 defs
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))"
80   I_def       "I == S#K#K"
82 end