1 (* Title: LCF/lcf.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 Natural Deduction Rules for LCF |
|
7 *) |
|
8 |
|
9 LCF = FOL + |
|
10 |
|
11 classes cpo < term |
|
12 |
|
13 default cpo |
|
14 |
|
15 types |
|
16 tr |
|
17 void |
|
18 ('a,'b) "*" (infixl 6) |
|
19 ('a,'b) "+" (infixl 5) |
|
20 |
|
21 arities |
|
22 fun, "*", "+" :: (cpo,cpo)cpo |
|
23 tr,void :: cpo |
|
24 |
|
25 consts |
|
26 UU :: "'a" |
|
27 TT,FF :: "tr" |
|
28 FIX :: "('a => 'a) => 'a" |
|
29 FST :: "'a*'b => 'a" |
|
30 SND :: "'a*'b => 'b" |
|
31 INL :: "'a => 'a+'b" |
|
32 INR :: "'b => 'a+'b" |
|
33 WHEN :: "['a=>'c, 'b=>'c, 'a+'b] => 'c" |
|
34 adm :: "('a => o) => o" |
|
35 VOID :: "void" ("()") |
|
36 PAIR :: "['a,'b] => 'a*'b" ("(1<_,/_>)" [0,0] 100) |
|
37 COND :: "[tr,'a,'a] => 'a" ("(_ =>/ (_ |/ _))" [60,60,60] 60) |
|
38 "<<" :: "['a,'a] => o" (infixl 50) |
|
39 rules |
|
40 (** DOMAIN THEORY **) |
|
41 |
|
42 eq_def "x=y == x << y & y << x" |
|
43 |
|
44 less_trans "[| x << y; y << z |] ==> x << z" |
|
45 |
|
46 less_ext "(ALL x. f(x) << g(x)) ==> f << g" |
|
47 |
|
48 mono "[| f << g; x << y |] ==> f(x) << g(y)" |
|
49 |
|
50 minimal "UU << x" |
|
51 |
|
52 FIX_eq "f(FIX(f)) = FIX(f)" |
|
53 |
|
54 (** TR **) |
|
55 |
|
56 tr_cases "p=UU | p=TT | p=FF" |
|
57 |
|
58 not_TT_less_FF "~ TT << FF" |
|
59 not_FF_less_TT "~ FF << TT" |
|
60 not_TT_less_UU "~ TT << UU" |
|
61 not_FF_less_UU "~ FF << UU" |
|
62 |
|
63 COND_UU "UU => x | y = UU" |
|
64 COND_TT "TT => x | y = x" |
|
65 COND_FF "FF => x | y = y" |
|
66 |
|
67 (** PAIRS **) |
|
68 |
|
69 surj_pairing "<FST(z),SND(z)> = z" |
|
70 |
|
71 FST "FST(<x,y>) = x" |
|
72 SND "SND(<x,y>) = y" |
|
73 |
|
74 (*** STRICT SUM ***) |
|
75 |
|
76 INL_DEF "~x=UU ==> ~INL(x)=UU" |
|
77 INR_DEF "~x=UU ==> ~INR(x)=UU" |
|
78 |
|
79 INL_STRICT "INL(UU) = UU" |
|
80 INR_STRICT "INR(UU) = UU" |
|
81 |
|
82 WHEN_UU "WHEN(f,g,UU) = UU" |
|
83 WHEN_INL "~x=UU ==> WHEN(f,g,INL(x)) = f(x)" |
|
84 WHEN_INR "~x=UU ==> WHEN(f,g,INR(x)) = g(x)" |
|
85 |
|
86 SUM_EXHAUSTION |
|
87 "z = UU | (EX x. ~x=UU & z = INL(x)) | (EX y. ~y=UU & z = INR(y))" |
|
88 |
|
89 (** VOID **) |
|
90 |
|
91 void_cases "(x::void) = UU" |
|
92 |
|
93 (** INDUCTION **) |
|
94 |
|
95 induct "[| adm(P); P(UU); ALL x. P(x) --> P(f(x)) |] ==> P(FIX(f))" |
|
96 |
|
97 (** Admissibility / Chain Completeness **) |
|
98 (* All rules can be found on pages 199--200 of Larry's LCF book. |
|
99 Note that "easiness" of types is not taken into account |
|
100 because it cannot be expressed schematically; flatness could be. *) |
|
101 |
|
102 adm_less "adm(%x.t(x) << u(x))" |
|
103 adm_not_less "adm(%x.~ t(x) << u)" |
|
104 adm_not_free "adm(%x.A)" |
|
105 adm_subst "adm(P) ==> adm(%x.P(t(x)))" |
|
106 adm_conj "[| adm(P); adm(Q) |] ==> adm(%x.P(x)&Q(x))" |
|
107 adm_disj "[| adm(P); adm(Q) |] ==> adm(%x.P(x)|Q(x))" |
|
108 adm_imp "[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x.P(x)-->Q(x))" |
|
109 adm_all "(!!y.adm(P(y))) ==> adm(%x.ALL y.P(y,x))" |
|
110 end |
|