42 VOID :: "void" ("'(')") |
42 VOID :: "void" ("'(')") |
43 PAIR :: "['a,'b] => 'a*'b" ("(1<_,/_>)" [0,0] 100) |
43 PAIR :: "['a,'b] => 'a*'b" ("(1<_,/_>)" [0,0] 100) |
44 COND :: "[tr,'a,'a] => 'a" ("(_ =>/ (_ |/ _))" [60,60,60] 60) |
44 COND :: "[tr,'a,'a] => 'a" ("(_ =>/ (_ |/ _))" [60,60,60] 60) |
45 less :: "['a,'a] => o" (infixl "<<" 50) |
45 less :: "['a,'a] => o" (infixl "<<" 50) |
46 |
46 |
47 axioms |
47 axiomatization where |
48 (** DOMAIN THEORY **) |
48 (** DOMAIN THEORY **) |
49 |
49 |
50 eq_def: "x=y == x << y & y << x" |
50 eq_def: "x=y == x << y & y << x" and |
51 |
51 |
52 less_trans: "[| x << y; y << z |] ==> x << z" |
52 less_trans: "[| x << y; y << z |] ==> x << z" and |
53 |
53 |
54 less_ext: "(ALL x. f(x) << g(x)) ==> f << g" |
54 less_ext: "(ALL x. f(x) << g(x)) ==> f << g" and |
55 |
55 |
56 mono: "[| f << g; x << y |] ==> f(x) << g(y)" |
56 mono: "[| f << g; x << y |] ==> f(x) << g(y)" and |
57 |
57 |
58 minimal: "UU << x" |
58 minimal: "UU << x" and |
59 |
59 |
60 FIX_eq: "f(FIX(f)) = FIX(f)" |
60 FIX_eq: "\<And>f. f(FIX(f)) = FIX(f)" |
61 |
61 |
|
62 axiomatization where |
62 (** TR **) |
63 (** TR **) |
63 |
64 |
64 tr_cases: "p=UU | p=TT | p=FF" |
65 tr_cases: "p=UU | p=TT | p=FF" and |
65 |
66 |
66 not_TT_less_FF: "~ TT << FF" |
67 not_TT_less_FF: "~ TT << FF" and |
67 not_FF_less_TT: "~ FF << TT" |
68 not_FF_less_TT: "~ FF << TT" and |
68 not_TT_less_UU: "~ TT << UU" |
69 not_TT_less_UU: "~ TT << UU" and |
69 not_FF_less_UU: "~ FF << UU" |
70 not_FF_less_UU: "~ FF << UU" and |
70 |
71 |
71 COND_UU: "UU => x | y = UU" |
72 COND_UU: "UU => x | y = UU" and |
72 COND_TT: "TT => x | y = x" |
73 COND_TT: "TT => x | y = x" and |
73 COND_FF: "FF => x | y = y" |
74 COND_FF: "FF => x | y = y" |
74 |
75 |
|
76 axiomatization where |
75 (** PAIRS **) |
77 (** PAIRS **) |
76 |
78 |
77 surj_pairing: "<FST(z),SND(z)> = z" |
79 surj_pairing: "<FST(z),SND(z)> = z" and |
78 |
80 |
79 FST: "FST(<x,y>) = x" |
81 FST: "FST(<x,y>) = x" and |
80 SND: "SND(<x,y>) = y" |
82 SND: "SND(<x,y>) = y" |
81 |
83 |
|
84 axiomatization where |
82 (*** STRICT SUM ***) |
85 (*** STRICT SUM ***) |
83 |
86 |
84 INL_DEF: "~x=UU ==> ~INL(x)=UU" |
87 INL_DEF: "~x=UU ==> ~INL(x)=UU" and |
85 INR_DEF: "~x=UU ==> ~INR(x)=UU" |
88 INR_DEF: "~x=UU ==> ~INR(x)=UU" and |
86 |
89 |
87 INL_STRICT: "INL(UU) = UU" |
90 INL_STRICT: "INL(UU) = UU" and |
88 INR_STRICT: "INR(UU) = UU" |
91 INR_STRICT: "INR(UU) = UU" and |
89 |
92 |
90 WHEN_UU: "WHEN(f,g,UU) = UU" |
93 WHEN_UU: "WHEN(f,g,UU) = UU" and |
91 WHEN_INL: "~x=UU ==> WHEN(f,g,INL(x)) = f(x)" |
94 WHEN_INL: "~x=UU ==> WHEN(f,g,INL(x)) = f(x)" and |
92 WHEN_INR: "~x=UU ==> WHEN(f,g,INR(x)) = g(x)" |
95 WHEN_INR: "~x=UU ==> WHEN(f,g,INR(x)) = g(x)" and |
93 |
96 |
94 SUM_EXHAUSTION: |
97 SUM_EXHAUSTION: |
95 "z = UU | (EX x. ~x=UU & z = INL(x)) | (EX y. ~y=UU & z = INR(y))" |
98 "z = UU | (EX x. ~x=UU & z = INL(x)) | (EX y. ~y=UU & z = INR(y))" |
96 |
99 |
|
100 axiomatization where |
97 (** VOID **) |
101 (** VOID **) |
98 |
102 |
99 void_cases: "(x::void) = UU" |
103 void_cases: "(x::void) = UU" |
100 |
104 |
101 (** INDUCTION **) |
105 (** INDUCTION **) |
102 |
106 |
|
107 axiomatization where |
103 induct: "[| adm(P); P(UU); ALL x. P(x) --> P(f(x)) |] ==> P(FIX(f))" |
108 induct: "[| adm(P); P(UU); ALL x. P(x) --> P(f(x)) |] ==> P(FIX(f))" |
104 |
109 |
|
110 axiomatization where |
105 (** Admissibility / Chain Completeness **) |
111 (** Admissibility / Chain Completeness **) |
106 (* All rules can be found on pages 199--200 of Larry's LCF book. |
112 (* All rules can be found on pages 199--200 of Larry's LCF book. |
107 Note that "easiness" of types is not taken into account |
113 Note that "easiness" of types is not taken into account |
108 because it cannot be expressed schematically; flatness could be. *) |
114 because it cannot be expressed schematically; flatness could be. *) |
109 |
115 |
110 adm_less: "adm(%x. t(x) << u(x))" |
116 adm_less: "\<And>t u. adm(%x. t(x) << u(x))" and |
111 adm_not_less: "adm(%x.~ t(x) << u)" |
117 adm_not_less: "\<And>t u. adm(%x.~ t(x) << u)" and |
112 adm_not_free: "adm(%x. A)" |
118 adm_not_free: "\<And>A. adm(%x. A)" and |
113 adm_subst: "adm(P) ==> adm(%x. P(t(x)))" |
119 adm_subst: "\<And>P t. adm(P) ==> adm(%x. P(t(x)))" and |
114 adm_conj: "[| adm(P); adm(Q) |] ==> adm(%x. P(x)&Q(x))" |
120 adm_conj: "\<And>P Q. [| adm(P); adm(Q) |] ==> adm(%x. P(x)&Q(x))" and |
115 adm_disj: "[| adm(P); adm(Q) |] ==> adm(%x. P(x)|Q(x))" |
121 adm_disj: "\<And>P Q. [| adm(P); adm(Q) |] ==> adm(%x. P(x)|Q(x))" and |
116 adm_imp: "[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x. P(x)-->Q(x))" |
122 adm_imp: "\<And>P Q. [| adm(%x.~P(x)); adm(Q) |] ==> adm(%x. P(x)-->Q(x))" and |
117 adm_all: "(!!y. adm(P(y))) ==> adm(%x. ALL y. P(y,x))" |
123 adm_all: "\<And>P. (!!y. adm(P(y))) ==> adm(%x. ALL y. P(y,x))" |
118 |
124 |
119 |
125 |
120 lemma eq_imp_less1: "x = y ==> x << y" |
126 lemma eq_imp_less1: "x = y ==> x << y" |
121 by (simp add: eq_def) |
127 by (simp add: eq_def) |
122 |
128 |