0
|
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
|