28 qed "SPLITB"; |
28 qed "SPLITB"; |
29 |
29 |
30 val prems = goalw Wfd.thy [letrec2_def] |
30 val prems = goalw Wfd.thy [letrec2_def] |
31 "[| a : A; b : B; \ |
31 "[| a : A; b : B; \ |
32 \ !!p q g.[| p:A; q:B; \ |
32 \ !!p q g.[| p:A; q:B; \ |
33 \ ALL x:A.ALL y:{y: B. <<x,y>,<p,q>>:wf(R)}. g(x,y) : D(x,y) |] ==>\ |
33 \ ALL x:A. ALL y:{y: B. <<x,y>,<p,q>>:wf(R)}. g(x,y) : D(x,y) |] ==>\ |
34 \ h(p,q,g) : D(p,q) |] ==> \ |
34 \ h(p,q,g) : D(p,q) |] ==> \ |
35 \ letrec g x y be h(x,y,g) in g(a,b) : D(a,b)"; |
35 \ letrec g x y be h(x,y,g) in g(a,b) : D(a,b)"; |
36 by (rtac (SPLITB RS subst) 1); |
36 by (rtac (SPLITB RS subst) 1); |
37 by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1)); |
37 by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1)); |
38 by (stac SPLITB 1); |
38 by (stac SPLITB 1); |
40 by (rtac (SPLITB RS subst) 1); |
40 by (rtac (SPLITB RS subst) 1); |
41 by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE |
41 by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE |
42 eresolve_tac [bspec,SubtypeE,sym RS subst] 1)); |
42 eresolve_tac [bspec,SubtypeE,sym RS subst] 1)); |
43 qed "letrec2T"; |
43 qed "letrec2T"; |
44 |
44 |
45 goal Wfd.thy "SPLIT(<a,<b,c>>,%x xs.SPLIT(xs,%y z.B(x,y,z))) = B(a,b,c)"; |
45 goal Wfd.thy "SPLIT(<a,<b,c>>,%x xs. SPLIT(xs,%y z. B(x,y,z))) = B(a,b,c)"; |
46 by (simp_tac (ccl_ss addsimps [SPLITB]) 1); |
46 by (simp_tac (ccl_ss addsimps [SPLITB]) 1); |
47 qed "lemma"; |
47 qed "lemma"; |
48 |
48 |
49 val prems = goalw Wfd.thy [letrec3_def] |
49 val prems = goalw Wfd.thy [letrec3_def] |
50 "[| a : A; b : B; c : C; \ |
50 "[| a : A; b : B; c : C; \ |
51 \ !!p q r g.[| p:A; q:B; r:C; \ |
51 \ !!p q r g.[| p:A; q:B; r:C; \ |
52 \ ALL x:A.ALL y:B.ALL z:{z:C. <<x,<y,z>>,<p,<q,r>>> : wf(R)}. \ |
52 \ ALL x:A. ALL y:B. ALL z:{z:C. <<x,<y,z>>,<p,<q,r>>> : wf(R)}. \ |
53 \ g(x,y,z) : D(x,y,z) |] ==>\ |
53 \ g(x,y,z) : D(x,y,z) |] ==>\ |
54 \ h(p,q,r,g) : D(p,q,r) |] ==> \ |
54 \ h(p,q,r,g) : D(p,q,r) |] ==> \ |
55 \ letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)"; |
55 \ letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)"; |
56 by (rtac (lemma RS subst) 1); |
56 by (rtac (lemma RS subst) 1); |
57 by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1)); |
57 by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1)); |
73 \ g(a) : E"; |
73 \ g(a) : E"; |
74 by (REPEAT (ares_tac ([SubtypeI,major RS bspec,major]@prems) 1)); |
74 by (REPEAT (ares_tac ([SubtypeI,major RS bspec,major]@prems) 1)); |
75 qed "rcallT"; |
75 qed "rcallT"; |
76 |
76 |
77 val major::prems = goal Wfd.thy |
77 val major::prems = goal Wfd.thy |
78 "[| ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \ |
78 "[| ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \ |
79 \ g(a,b) : D(a,b) ==> g(a,b) : E; a:A; b:B; <<a,b>,<p,q>>:wf(R) |] ==> \ |
79 \ g(a,b) : D(a,b) ==> g(a,b) : E; a:A; b:B; <<a,b>,<p,q>>:wf(R) |] ==> \ |
80 \ g(a,b) : E"; |
80 \ g(a,b) : E"; |
81 by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec,major]@prems) 1)); |
81 by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec,major]@prems) 1)); |
82 qed "rcall2T"; |
82 qed "rcall2T"; |
83 |
83 |
84 val major::prems = goal Wfd.thy |
84 val major::prems = goal Wfd.thy |
85 "[| ALL x:A.ALL y:B.ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}. g(x,y,z):D(x,y,z); \ |
85 "[| ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}. g(x,y,z):D(x,y,z); \ |
86 \ g(a,b,c) : D(a,b,c) ==> g(a,b,c) : E; \ |
86 \ g(a,b,c) : D(a,b,c) ==> g(a,b,c) : E; \ |
87 \ a:A; b:B; c:C; <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==> \ |
87 \ a:A; b:B; c:C; <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==> \ |
88 \ g(a,b,c) : E"; |
88 \ g(a,b,c) : E"; |
89 by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec RS bspec,major]@prems) 1)); |
89 by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec RS bspec,major]@prems) 1)); |
90 qed "rcall3T"; |
90 qed "rcall3T"; |
114 by (rtac rcallT 1); |
114 by (rtac rcallT 1); |
115 by (REPEAT (ares_tac prems 1)); |
115 by (REPEAT (ares_tac prems 1)); |
116 qed "hyprcallT"; |
116 qed "hyprcallT"; |
117 |
117 |
118 val prems = goal Wfd.thy |
118 val prems = goal Wfd.thy |
119 "[| g(a,b) = c; ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \ |
119 "[| g(a,b) = c; ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \ |
120 \ [| c=g(a,b); g(a,b) : D(a,b) |] ==> P; \ |
120 \ [| c=g(a,b); g(a,b) : D(a,b) |] ==> P; \ |
121 \ a:A; b:B; <<a,b>,<p,q>>:wf(R) |] ==> \ |
121 \ a:A; b:B; <<a,b>,<p,q>>:wf(R) |] ==> \ |
122 \ P"; |
122 \ P"; |
123 by (resolve_tac (prems) 1); |
123 by (resolve_tac (prems) 1); |
124 by (resolve_tac (prems RL [sym]) 1); |
124 by (resolve_tac (prems RL [sym]) 1); |
126 by (REPEAT (ares_tac prems 1)); |
126 by (REPEAT (ares_tac prems 1)); |
127 qed "hyprcall2T"; |
127 qed "hyprcall2T"; |
128 |
128 |
129 val prems = goal Wfd.thy |
129 val prems = goal Wfd.thy |
130 "[| g(a,b,c) = d; \ |
130 "[| g(a,b,c) = d; \ |
131 \ ALL x:A.ALL y:B.ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); \ |
131 \ ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); \ |
132 \ [| d=g(a,b,c); g(a,b,c) : D(a,b,c) |] ==> P; \ |
132 \ [| d=g(a,b,c); g(a,b,c) : D(a,b,c) |] ==> P; \ |
133 \ a:A; b:B; c:C; <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==> \ |
133 \ a:A; b:B; c:C; <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==> \ |
134 \ P"; |
134 \ P"; |
135 by (resolve_tac (prems) 1); |
135 by (resolve_tac (prems) 1); |
136 by (resolve_tac (prems RL [sym]) 1); |
136 by (resolve_tac (prems RL [sym]) 1); |
147 \ P"; |
147 \ P"; |
148 by (REPEAT (ares_tac prems 1)); |
148 by (REPEAT (ares_tac prems 1)); |
149 qed "rmIH1"; |
149 qed "rmIH1"; |
150 |
150 |
151 val prems = goal Wfd.thy |
151 val prems = goal Wfd.thy |
152 "[| ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P |] ==> \ |
152 "[| ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P |] ==> \ |
153 \ P"; |
153 \ P"; |
154 by (REPEAT (ares_tac prems 1)); |
154 by (REPEAT (ares_tac prems 1)); |
155 qed "rmIH2"; |
155 qed "rmIH2"; |
156 |
156 |
157 val prems = goal Wfd.thy |
157 val prems = goal Wfd.thy |
158 "[| ALL x:A.ALL y:B.ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); \ |
158 "[| ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); \ |
159 \ P |] ==> \ |
159 \ P |] ==> \ |
160 \ P"; |
160 \ P"; |
161 by (REPEAT (ares_tac prems 1)); |
161 by (REPEAT (ares_tac prems 1)); |
162 qed "rmIH3"; |
162 qed "rmIH3"; |
163 |
163 |