equal
deleted
inserted
replaced
|
1 (* Title: ZF/ex/contract.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow & Lawrence C Paulson |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Inductive definition of (1-step) contractions and (mult-step) reductions |
|
7 *) |
|
8 |
|
9 Contract0 = Comb + |
|
10 consts |
|
11 diamond :: "i => o" |
|
12 I :: "i" |
|
13 |
|
14 contract :: "i" |
|
15 "-1->" :: "[i,i] => o" (infixl 50) |
|
16 "--->" :: "[i,i] => o" (infixl 50) |
|
17 |
|
18 parcontract :: "i" |
|
19 "=1=>" :: "[i,i] => o" (infixl 50) |
|
20 "===>" :: "[i,i] => o" (infixl 50) |
|
21 |
|
22 translations |
|
23 "p -1-> q" == "<p,q> : contract" |
|
24 "p ---> q" == "<p,q> : contract^*" |
|
25 "p =1=> q" == "<p,q> : parcontract" |
|
26 "p ===> q" == "<p,q> : parcontract^+" |
|
27 |
|
28 rules |
|
29 |
|
30 diamond_def "diamond(r) == ALL x y. <x,y>:r --> \ |
|
31 \ (ALL y'. <x,y'>:r --> \ |
|
32 \ (EX z. <y,z>:r & <y',z> : r))" |
|
33 |
|
34 I_def "I == S#K#K" |
|
35 |
|
36 end |