41 Second step: Translation of ANDL specification to HOLCF Specification |
43 Second step: Translation of ANDL specification to HOLCF Specification |
42 --------------------------------------------------------------------- |
44 --------------------------------------------------------------------- |
43 |
45 |
44 Specification of agent f ist translated to predicate is_f |
46 Specification of agent f ist translated to predicate is_f |
45 |
47 |
46 is_f :: ('b stream * ('b,'c) tc stream -> |
48 is_f :: ('b stream * ('b,'c) tc stream -> |
47 'c stream * ('b,'c) tc stream) => bool |
49 'c stream * ('b,'c) tc stream) => bool |
48 |
50 |
49 is_f f = !i1 i2 o1 o2. |
51 is_f f = !i1 i2 o1 o2. |
50 f$<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2) |
52 f$<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2) |
51 |
53 |
52 Specification of agent g is translated to predicate is_g which uses |
54 Specification of agent g is translated to predicate is_g which uses |
53 predicate is_net_g |
55 predicate is_net_g |
54 |
56 |
55 is_net_g :: ('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => |
57 is_net_g :: ('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => |
56 'b stream => 'c stream => bool |
58 'b stream => 'c stream => bool |
57 |
59 |
58 is_net_g f x y = |
60 is_net_g f x y = |
59 ? z. <y,z> = f$<x,z> & |
61 ? z. <y,z> = f$<x,z> & |
60 !oy hz. <oy,hz> = f$<x,hz> --> z << hz |
62 !oy hz. <oy,hz> = f$<x,hz> --> z << hz |
61 |
63 |
62 |
64 |
63 is_g :: ('b stream -> 'c stream) => bool |
65 is_g :: ('b stream -> 'c stream) => bool |
64 |
66 |
65 is_g g = ? f. is_f f & (!x y. g$x = y --> is_net_g f x y |
67 is_g g = ? f. is_f f & (!x y. g$x = y --> is_net_g f x y |
66 |
68 |
67 Third step: (show conservativity) |
69 Third step: (show conservativity) |
68 ----------- |
70 ----------- |
69 |
71 |
70 Suppose we have a model for the theory TH1 which contains the axiom |
72 Suppose we have a model for the theory TH1 which contains the axiom |
71 |
73 |
72 ? f. is_f f |
74 ? f. is_f f |
73 |
75 |
74 In this case there is also a model for the theory TH2 that enriches TH1 by |
76 In this case there is also a model for the theory TH2 that enriches TH1 by |
75 axiom |
77 axiom |
76 |
78 |
77 ? g. is_g g |
79 ? g. is_g g |
78 |
80 |
79 The result is proved by showing that there is a definitional extension |
81 The result is proved by showing that there is a definitional extension |
80 that extends TH1 by a definition of g. |
82 that extends TH1 by a definition of g. |
81 |
83 |
82 |
84 |
83 We define: |
85 We define: |
84 |
86 |
85 def_g g = |
87 def_g g = |
86 (? f. is_f f & |
88 (? f. is_f f & |
87 g = (LAM x. cfst$(f$<x,fix$(LAM k.csnd$(f$<x,k>))>)) ) |
89 g = (LAM x. cfst$(f$<x,fix$(LAM k.csnd$(f$<x,k>))>)) ) |
88 |
90 |
89 Now we prove: |
91 Now we prove: |
90 |
92 |
91 (? f. is_f f ) --> (? g. is_g g) |
93 (? f. is_f f ) --> (? g. is_g g) |
92 |
94 |
93 using the theorems |
95 using the theorems |
94 |
96 |
95 loopback_eq) def_g = is_g (real work) |
97 loopback_eq) def_g = is_g (real work) |
96 |
98 |
97 L1) (? f. is_f f ) --> (? g. def_g g) (trivial) |
99 L1) (? f. is_f f ) --> (? g. def_g g) (trivial) |
98 |
100 |
99 *) |
101 *) |
100 |
102 |
101 Focus_ex = Stream + |
103 theory Focus_ex |
|
104 imports Stream |
|
105 begin |
102 |
106 |
103 types tc 2 |
107 typedecl ('a, 'b) tc |
104 |
108 arities tc:: (pcpo, pcpo) pcpo |
105 arities tc:: (pcpo,pcpo)pcpo |
|
106 |
109 |
107 consts |
110 consts |
108 |
111 |
109 is_f :: |
112 is_f :: |
110 "('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => bool" |
113 "('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => bool" |
111 is_net_g :: "('b stream *('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => |
114 is_net_g :: "('b stream *('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => |
112 'b stream => 'c stream => bool" |
115 'b stream => 'c stream => bool" |
113 is_g :: "('b stream -> 'c stream) => bool" |
116 is_g :: "('b stream -> 'c stream) => bool" |
114 def_g :: "('b stream -> 'c stream) => bool" |
117 def_g :: "('b stream -> 'c stream) => bool" |
115 Rf :: |
118 Rf :: |
116 "('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool" |
119 "('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool" |
117 |
120 |
118 defs |
121 defs |
119 |
122 |
120 is_f "is_f f == (!i1 i2 o1 o2. |
123 is_f: "is_f f == (!i1 i2 o1 o2. |
121 f$<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2))" |
124 f$<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2))" |
122 |
125 |
123 is_net_g "is_net_g f x y == (? z. |
126 is_net_g: "is_net_g f x y == (? z. |
124 <y,z> = f$<x,z> & |
127 <y,z> = f$<x,z> & |
125 (!oy hz. <oy,hz> = f$<x,hz> --> z << hz))" |
128 (!oy hz. <oy,hz> = f$<x,hz> --> z << hz))" |
126 |
129 |
127 is_g "is_g g == (? f. |
130 is_g: "is_g g == (? f. |
128 is_f f & |
131 is_f f & |
129 (!x y. g$x = y --> is_net_g f x y))" |
132 (!x y. g$x = y --> is_net_g f x y))" |
130 |
133 |
131 |
134 |
132 def_g "def_g g == (? f. |
135 def_g: "def_g g == (? f. |
133 is_f f & |
136 is_f f & |
134 g = (LAM x. cfst$(f$<x,fix$(LAM k. csnd$(f$<x,k>))>)))" |
137 g = (LAM x. cfst$(f$<x,fix$(LAM k. csnd$(f$<x,k>))>)))" |
|
138 |
|
139 ML {* use_legacy_bindings (the_context ()) *} |
135 |
140 |
136 end |
141 end |