2570
|
1 |
(* first some logical trading *)
|
|
2 |
|
|
3 |
val prems = goal Focus_ex.thy
|
|
4 |
"is_g(g) = \
|
10835
|
5 |
\ (? f. is_f(f) & (!x.(? z. <g$x,z> = f$<x,z> & \
|
|
6 |
\ (! w y. <y,w> = f$<x,w> --> z << w))))";
|
2570
|
7 |
by (simp_tac (HOL_ss addsimps [is_g,is_net_g]) 1);
|
|
8 |
by (fast_tac HOL_cs 1);
|
|
9 |
val lemma1 = result();
|
|
10 |
|
|
11 |
val prems = goal Focus_ex.thy
|
10835
|
12 |
"(? f. is_f(f) & (!x. (? z. <g$x,z> = f$<x,z> & \
|
|
13 |
\ (!w y. <y,w> = f$<x,w> --> z << w)))) \
|
2570
|
14 |
\ = \
|
|
15 |
\ (? f. is_f(f) & (!x. ? z.\
|
10835
|
16 |
\ g$x = cfst$(f$<x,z>) & \
|
|
17 |
\ z = csnd$(f$<x,z>) & \
|
|
18 |
\ (! w y. <y,w> = f$<x,w> --> z << w)))";
|
2570
|
19 |
by (rtac iffI 1);
|
|
20 |
by (etac exE 1);
|
|
21 |
by (res_inst_tac [("x","f")] exI 1);
|
|
22 |
by (REPEAT (etac conjE 1));
|
|
23 |
by (etac conjI 1);
|
|
24 |
by (strip_tac 1);
|
|
25 |
by (etac allE 1);
|
|
26 |
by (etac exE 1);
|
|
27 |
by (res_inst_tac [("x","z")] exI 1);
|
|
28 |
by (REPEAT (etac conjE 1));
|
|
29 |
by (rtac conjI 1);
|
|
30 |
by (rtac conjI 2);
|
|
31 |
by (atac 3);
|
|
32 |
by (dtac sym 1);
|
|
33 |
by (asm_simp_tac HOLCF_ss 1);
|
|
34 |
by (dtac sym 1);
|
|
35 |
by (asm_simp_tac HOLCF_ss 1);
|
|
36 |
by (etac exE 1);
|
|
37 |
by (res_inst_tac [("x","f")] exI 1);
|
|
38 |
by (REPEAT (etac conjE 1));
|
|
39 |
by (etac conjI 1);
|
|
40 |
by (strip_tac 1);
|
|
41 |
by (etac allE 1);
|
|
42 |
by (etac exE 1);
|
|
43 |
by (res_inst_tac [("x","z")] exI 1);
|
|
44 |
by (REPEAT (etac conjE 1));
|
|
45 |
by (rtac conjI 1);
|
|
46 |
by (atac 2);
|
|
47 |
by (rtac trans 1);
|
|
48 |
by (rtac (surjective_pairing_Cprod2) 2);
|
|
49 |
by (etac subst 1);
|
|
50 |
by (etac subst 1);
|
|
51 |
by (rtac refl 1);
|
|
52 |
val lemma2 = result();
|
|
53 |
|
|
54 |
(* direction def_g(g) --> is_g(g) *)
|
|
55 |
|
|
56 |
val prems = goal Focus_ex.thy "def_g(g) --> is_g(g)";
|
|
57 |
by (simp_tac (HOL_ss addsimps [def_g,lemma1, lemma2]) 1);
|
|
58 |
by (rtac impI 1);
|
|
59 |
by (etac exE 1);
|
|
60 |
by (res_inst_tac [("x","f")] exI 1);
|
|
61 |
by (REPEAT (etac conjE 1));
|
|
62 |
by (etac conjI 1);
|
|
63 |
by (strip_tac 1);
|
10835
|
64 |
by (res_inst_tac [("x","fix$(LAM k. csnd$(f$<x,k>))")] exI 1);
|
2570
|
65 |
by (rtac conjI 1);
|
|
66 |
by (asm_simp_tac HOLCF_ss 1);
|
|
67 |
by (rtac trans 1);
|
|
68 |
by (rtac surjective_pairing_Cprod2 2);
|
|
69 |
by (rtac cfun_arg_cong 1);
|
|
70 |
by (rtac trans 1);
|
|
71 |
by (rtac fix_eq 1);
|
|
72 |
by (Simp_tac 1);
|
|
73 |
by (strip_tac 1);
|
|
74 |
by (rtac fix_least 1);
|
|
75 |
by (Simp_tac 1);
|
3018
|
76 |
by (etac exE 1);
|
2570
|
77 |
by (dtac sym 1);
|
|
78 |
back();
|
|
79 |
by (asm_simp_tac HOLCF_ss 1);
|
|
80 |
val lemma3 = result();
|
|
81 |
|
|
82 |
(* direction is_g(g) --> def_g(g) *)
|
|
83 |
val prems = goal Focus_ex.thy "is_g(g) --> def_g(g)";
|
|
84 |
by (simp_tac (HOL_ss delsimps (ex_simps @ all_simps)
|
3018
|
85 |
addsimps [lemma1,lemma2,def_g]) 1);
|
2570
|
86 |
by (rtac impI 1);
|
|
87 |
by (etac exE 1);
|
|
88 |
by (res_inst_tac [("x","f")] exI 1);
|
|
89 |
by (REPEAT (etac conjE 1));
|
|
90 |
by (etac conjI 1);
|
|
91 |
by (rtac ext_cfun 1);
|
|
92 |
by (eres_inst_tac [("x","x")] allE 1);
|
|
93 |
by (etac exE 1);
|
|
94 |
by (REPEAT (etac conjE 1));
|
10835
|
95 |
by (subgoal_tac "fix$(LAM k. csnd$(f$<x, k>)) = z" 1);
|
2570
|
96 |
by (asm_simp_tac HOLCF_ss 1);
|
10835
|
97 |
by (subgoal_tac "! w y. f$<x, w> = <y, w> --> z << w" 1);
|
2570
|
98 |
by (rtac sym 1);
|
|
99 |
by (rtac fix_eqI 1);
|
|
100 |
by (asm_simp_tac HOLCF_ss 1);
|
|
101 |
by (rtac allI 1);
|
|
102 |
by (simp_tac HOLCF_ss 1);
|
|
103 |
by (strip_tac 1);
|
10835
|
104 |
by (subgoal_tac "f$<x, za> = <cfst$(f$<x,za>),za>" 1);
|
2570
|
105 |
by (fast_tac HOL_cs 1);
|
|
106 |
by (rtac trans 1);
|
|
107 |
by (rtac (surjective_pairing_Cprod2 RS sym) 1);
|
|
108 |
by (etac cfun_arg_cong 1);
|
|
109 |
by (strip_tac 1);
|
|
110 |
by (REPEAT (etac allE 1));
|
|
111 |
by (etac mp 1);
|
|
112 |
by (etac sym 1);
|
|
113 |
val lemma4 = result();
|
|
114 |
|
|
115 |
(* now we assemble the result *)
|
|
116 |
|
|
117 |
val prems = goal Focus_ex.thy "def_g = is_g";
|
|
118 |
by (rtac ext 1);
|
|
119 |
by (rtac iffI 1);
|
|
120 |
by (etac (lemma3 RS mp) 1);
|
|
121 |
by (etac (lemma4 RS mp) 1);
|
|
122 |
val loopback_eq = result();
|
|
123 |
|
|
124 |
val prems = goal Focus_ex.thy
|
|
125 |
"(? f.\
|
|
126 |
\ is_f(f::'b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream))\
|
|
127 |
\ -->\
|
|
128 |
\ (? g. def_g(g::'b stream -> 'c stream ))";
|
|
129 |
by (simp_tac (HOL_ss addsimps [def_g]) 1);
|
|
130 |
val L2 = result();
|
|
131 |
|
|
132 |
val prems = goal Focus_ex.thy
|
|
133 |
"(? f.\
|
|
134 |
\ is_f(f::'b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream))\
|
|
135 |
\ -->\
|
|
136 |
\ (? g. is_g(g::'b stream -> 'c stream ))";
|
|
137 |
by (rtac (loopback_eq RS subst) 1);
|
|
138 |
by (rtac L2 1);
|
|
139 |
val conservative_loopback = result();
|