1227
|
1 |
theory Rsp
|
1653
|
2 |
imports Abs Tacs
|
1227
|
3 |
begin
|
|
4 |
|
|
5 |
ML {*
|
1683
f78c820f67c3
Automatically lift theorems and constants only using the new quotient types. Requires new Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
6 |
fun const_rsp qtys lthy const =
|
1227
|
7 |
let
|
1683
f78c820f67c3
Automatically lift theorems and constants only using the new quotient types. Requires new Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
8 |
val nty = fastype_of (Quotient_Term.quotient_lift_const qtys ("", const) lthy)
|
1227
|
9 |
val rel = Quotient_Term.equiv_relation_chk lthy (fastype_of const, nty);
|
|
10 |
in
|
|
11 |
HOLogic.mk_Trueprop (rel $ const $ const)
|
|
12 |
end
|
|
13 |
*}
|
|
14 |
|
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
15 |
(* Replaces bounds by frees and meta implications by implications *)
|
1227
|
16 |
ML {*
|
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
17 |
fun prepare_goal trm =
|
1227
|
18 |
let
|
|
19 |
val vars = strip_all_vars trm
|
|
20 |
val fs = rev (map Free vars)
|
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
21 |
val (fixes, no_alls) = ((map fst vars), subst_bounds (fs, (strip_all_body trm)))
|
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
22 |
val prems = map HOLogic.dest_Trueprop (Logic.strip_imp_prems no_alls)
|
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
23 |
val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl no_alls)
|
1227
|
24 |
in
|
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
25 |
(fixes, fold (curry HOLogic.mk_imp) prems concl)
|
1227
|
26 |
end
|
|
27 |
*}
|
|
28 |
|
|
29 |
ML {*
|
|
30 |
fun get_rsp_goal thy trm =
|
|
31 |
let
|
|
32 |
val goalstate = Goal.init (cterm_of thy trm);
|
|
33 |
val tac = REPEAT o rtac @{thm fun_rel_id};
|
|
34 |
in
|
|
35 |
case (SINGLE (tac 1) goalstate) of
|
|
36 |
NONE => error "rsp_goal failed"
|
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
37 |
| SOME th => prepare_goal (term_of (cprem_of th 1))
|
1227
|
38 |
end
|
|
39 |
*}
|
|
40 |
|
|
41 |
ML {*
|
1683
f78c820f67c3
Automatically lift theorems and constants only using the new quotient types. Requires new Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
42 |
fun prove_const_rsp qtys bind consts tac ctxt =
|
1227
|
43 |
let
|
1683
f78c820f67c3
Automatically lift theorems and constants only using the new quotient types. Requires new Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
44 |
val rsp_goals = map (const_rsp qtys ctxt) consts
|
1227
|
45 |
val thy = ProofContext.theory_of ctxt
|
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
46 |
val (fixed, user_goals) = split_list (map (get_rsp_goal thy) rsp_goals)
|
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
47 |
val fixed' = distinct (op =) (flat fixed)
|
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
48 |
val user_goal = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj user_goals)
|
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
49 |
val user_thm = Goal.prove ctxt fixed' [] user_goal tac
|
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
50 |
val user_thms = map repeat_mp (HOLogic.conj_elims user_thm)
|
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
51 |
fun tac _ = (REPEAT o rtac @{thm fun_rel_id} THEN' resolve_tac user_thms THEN_ALL_NEW atac) 1
|
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
52 |
val rsp_thms = map (fn gl => Goal.prove ctxt [] [] gl tac) rsp_goals
|
1227
|
53 |
in
|
|
54 |
ctxt
|
|
55 |
|> snd o Local_Theory.note
|
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
56 |
((Binding.empty, [Attrib.internal (fn _ => Quotient_Info.rsp_rules_add)]), rsp_thms)
|
1278
|
57 |
|> Local_Theory.note ((bind, []), user_thms)
|
1227
|
58 |
end
|
|
59 |
*}
|
|
60 |
|
1573
|
61 |
ML {*
|
|
62 |
fun fvbv_rsp_tac induct fvbv_simps ctxt =
|
1653
|
63 |
rel_indtac induct THEN_ALL_NEW
|
1573
|
64 |
(TRY o rtac @{thm TrueI}) THEN_ALL_NEW
|
1673
e8cf0520c820
New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
65 |
asm_full_simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
|
1672
|
66 |
asm_full_simp_tac (HOL_ss addsimps (@{thms alphas} @ fvbv_simps)) THEN_ALL_NEW
|
1573
|
67 |
REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW
|
|
68 |
asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW
|
|
69 |
TRY o blast_tac (claset_of ctxt)
|
1227
|
70 |
*}
|
|
71 |
|
|
72 |
ML {*
|
1553
4355eb3b7161
Automatically derive support for datatypes with at-most one binding per constructor.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
73 |
fun sym_eqvts ctxt = map (fn x => sym OF [x]) (Nominal_ThmDecls.get_eqvts_thms ctxt)
|
4355eb3b7161
Automatically derive support for datatypes with at-most one binding per constructor.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
74 |
fun all_eqvts ctxt =
|
4355eb3b7161
Automatically derive support for datatypes with at-most one binding per constructor.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
75 |
Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt
|
1416
|
76 |
*}
|
|
77 |
|
|
78 |
ML {*
|
1561
|
79 |
fun constr_rsp_tac inj rsp =
|
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
80 |
REPEAT o rtac impI THEN'
|
1653
|
81 |
simp_tac (HOL_ss addsimps inj) THEN' split_conj_tac THEN_ALL_NEW
|
1227
|
82 |
(asm_simp_tac HOL_ss THEN_ALL_NEW (
|
1561
|
83 |
REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW
|
1673
e8cf0520c820
New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
84 |
simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
|
1561
|
85 |
asm_full_simp_tac (HOL_ss addsimps (rsp @
|
1744
|
86 |
@{thms split_conv alphas fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left}))
|
1227
|
87 |
))
|
|
88 |
*}
|
|
89 |
|
1268
d1999540d23a
Move the eqvt code out of Terms and fixed induction for single-rule examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
90 |
ML {*
|
1445
|
91 |
fun perm_arg arg =
|
|
92 |
let
|
|
93 |
val ty = fastype_of arg
|
|
94 |
in
|
|
95 |
Const (@{const_name permute}, @{typ perm} --> ty --> ty)
|
|
96 |
end
|
1268
d1999540d23a
Move the eqvt code out of Terms and fixed induction for single-rule examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
97 |
*}
|
d1999540d23a
Move the eqvt code out of Terms and fixed induction for single-rule examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
98 |
|
1300
|
99 |
lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi"
|
|
100 |
apply (erule exE)
|
|
101 |
apply (rule_tac x="pi \<bullet> pia" in exI)
|
|
102 |
by auto
|
1268
d1999540d23a
Move the eqvt code out of Terms and fixed induction for single-rule examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
103 |
|
1331
|
104 |
|
|
105 |
ML {*
|
|
106 |
fun alpha_eqvt_tac induct simps ctxt =
|
1653
|
107 |
rel_indtac induct THEN_ALL_NEW
|
1656
|
108 |
simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW
|
1653
|
109 |
REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW
|
1331
|
110 |
asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW
|
|
111 |
asm_full_simp_tac (HOL_ss addsimps
|
1672
|
112 |
@{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alphas}) THEN_ALL_NEW
|
1653
|
113 |
(split_conj_tac THEN_ALL_NEW TRY o resolve_tac
|
1331
|
114 |
@{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]})
|
|
115 |
THEN_ALL_NEW
|
1494
923413256cbb
Clean 'Lift', start working only on exported things in Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
116 |
asm_full_simp_tac (HOL_ss addsimps (@{thms split_conv permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt @ simps))
|
1331
|
117 |
*}
|
|
118 |
|
|
119 |
ML {*
|
1445
|
120 |
fun build_alpha_eqvt alpha names =
|
1268
d1999540d23a
Move the eqvt code out of Terms and fixed induction for single-rule examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
121 |
let
|
d1999540d23a
Move the eqvt code out of Terms and fixed induction for single-rule examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
122 |
val pi = Free ("p", @{typ perm});
|
1445
|
123 |
val (tys, _) = strip_type (fastype_of alpha)
|
|
124 |
val indnames = Name.variant_list names (Datatype_Prop.make_tnames (map body_type tys));
|
|
125 |
val args = map Free (indnames ~~ tys);
|
|
126 |
val perm_args = map (fn x => perm_arg x $ pi $ x) args
|
|
127 |
in
|
|
128 |
(HOLogic.mk_imp (list_comb (alpha, args), list_comb (alpha, perm_args)), indnames @ names)
|
|
129 |
end
|
|
130 |
*}
|
|
131 |
|
|
132 |
ML {*
|
|
133 |
fun build_alpha_eqvts funs tac ctxt =
|
|
134 |
let
|
|
135 |
val (gls, names) = fold_map build_alpha_eqvt funs ["p"]
|
|
136 |
val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj gls)
|
|
137 |
val thm = Goal.prove ctxt names [] gl tac
|
1268
d1999540d23a
Move the eqvt code out of Terms and fixed induction for single-rule examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
138 |
in
|
d1999540d23a
Move the eqvt code out of Terms and fixed induction for single-rule examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
139 |
map (fn x => mp OF [x]) (HOLogic.conj_elims thm)
|
d1999540d23a
Move the eqvt code out of Terms and fixed induction for single-rule examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
140 |
end
|
d1999540d23a
Move the eqvt code out of Terms and fixed induction for single-rule examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
141 |
*}
|
d1999540d23a
Move the eqvt code out of Terms and fixed induction for single-rule examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
142 |
|
1308
|
143 |
ML {*
|
1573
|
144 |
fun prove_fv_rsp fv_alphas_lst all_alphas tac ctxt =
|
|
145 |
let
|
|
146 |
val (fvs_alphas, ls) = split_list fv_alphas_lst;
|
|
147 |
val (fv_ts, alpha_ts) = split_list fvs_alphas;
|
|
148 |
val tys = map (domain_type o fastype_of) alpha_ts;
|
|
149 |
val names = Datatype_Prop.make_tnames tys;
|
|
150 |
val names2 = Name.variant_list names names;
|
|
151 |
val args = map Free (names ~~ tys);
|
|
152 |
val args2 = map Free (names2 ~~ tys);
|
|
153 |
fun mk_fv_rsp arg arg2 (fv, alpha) = HOLogic.mk_eq ((fv $ arg), (fv $ arg2));
|
|
154 |
fun fv_rsp_arg (((fv, alpha), (arg, arg2)), l) =
|
|
155 |
HOLogic.mk_imp (
|
|
156 |
(alpha $ arg $ arg2),
|
|
157 |
(foldr1 HOLogic.mk_conj
|
|
158 |
(HOLogic.mk_eq (fv $ arg, fv $ arg2) ::
|
|
159 |
(map (mk_fv_rsp arg arg2) l))));
|
|
160 |
val nobn_eqs = map fv_rsp_arg (((fv_ts ~~ alpha_ts) ~~ (args ~~ args2)) ~~ ls);
|
|
161 |
fun mk_fv_rsp_bn arg arg2 (fv, alpha) =
|
|
162 |
HOLogic.mk_imp (
|
|
163 |
(alpha $ arg $ arg2),
|
|
164 |
HOLogic.mk_eq ((fv $ arg), (fv $ arg2)));
|
|
165 |
fun fv_rsp_arg_bn ((arg, arg2), l) =
|
|
166 |
map (mk_fv_rsp_bn arg arg2) l;
|
|
167 |
val bn_eqs = flat (map fv_rsp_arg_bn ((args ~~ args2) ~~ ls));
|
|
168 |
val (_, add_alphas) = chop (length (nobn_eqs @ bn_eqs)) all_alphas;
|
|
169 |
val atys = map (domain_type o fastype_of) add_alphas;
|
|
170 |
val anames = Name.variant_list (names @ names2) (Datatype_Prop.make_tnames atys);
|
|
171 |
val aargs = map Free (anames ~~ atys);
|
|
172 |
val aeqs = map2 (fn alpha => fn arg => HOLogic.mk_imp (alpha $ arg $ arg, @{term True}))
|
|
173 |
add_alphas aargs;
|
|
174 |
val eq = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (nobn_eqs @ bn_eqs @ aeqs));
|
|
175 |
val th = Goal.prove ctxt (names @ names2) [] eq tac;
|
|
176 |
val ths = HOLogic.conj_elims th;
|
|
177 |
val (ths_nobn, ths_bn) = chop (length ls) ths;
|
|
178 |
fun project (th, l) =
|
|
179 |
Project_Rule.projects ctxt (1 upto (length l + 1)) (hd (Project_Rule.projections ctxt th))
|
|
180 |
val ths_nobn_pr = map project (ths_nobn ~~ ls);
|
|
181 |
in
|
|
182 |
(flat ths_nobn_pr @ ths_bn)
|
1268
d1999540d23a
Move the eqvt code out of Terms and fixed induction for single-rule examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
183 |
end
|
1573
|
184 |
*}
|
|
185 |
|
1653
|
186 |
(** alpha_bn_rsp **)
|
|
187 |
|
1575
|
188 |
lemma equivp_rspl:
|
|
189 |
"equivp r \<Longrightarrow> r a b \<Longrightarrow> r a c = r b c"
|
|
190 |
unfolding equivp_reflp_symp_transp symp_def transp_def
|
|
191 |
by blast
|
|
192 |
|
|
193 |
lemma equivp_rspr:
|
|
194 |
"equivp r \<Longrightarrow> r a b \<Longrightarrow> r c a = r c b"
|
|
195 |
unfolding equivp_reflp_symp_transp symp_def transp_def
|
|
196 |
by blast
|
|
197 |
|
|
198 |
ML {*
|
1653
|
199 |
fun alpha_bn_rsp_tac simps res exhausts a ctxt =
|
|
200 |
rtac allI THEN_ALL_NEW
|
|
201 |
case_rules_tac ctxt a exhausts THEN_ALL_NEW
|
|
202 |
asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW
|
|
203 |
TRY o REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \<and>"]}) THEN_ALL_NEW
|
|
204 |
TRY o eresolve_tac res THEN_ALL_NEW
|
|
205 |
asm_full_simp_tac (HOL_ss addsimps simps);
|
|
206 |
*}
|
|
207 |
|
|
208 |
|
|
209 |
ML {*
|
|
210 |
fun build_alpha_bn_rsp_gl a alphas alpha_bn ctxt =
|
1575
|
211 |
let
|
1653
|
212 |
val ty = domain_type (fastype_of alpha_bn);
|
|
213 |
val (l, r) = the (AList.lookup (op=) alphas ty);
|
1575
|
214 |
in
|
1653
|
215 |
([HOLogic.mk_all (a, ty, HOLogic.mk_eq (alpha_bn $ l $ Bound 0, alpha_bn $ r $ Bound 0)),
|
|
216 |
HOLogic.mk_all (a, ty, HOLogic.mk_eq (alpha_bn $ Bound 0 $ l, alpha_bn $ Bound 0 $ r))], ctxt)
|
1575
|
217 |
end
|
|
218 |
*}
|
|
219 |
|
1653
|
220 |
ML {*
|
|
221 |
fun prove_alpha_bn_rsp alphas ind simps equivps exhausts alpha_bns ctxt =
|
|
222 |
let
|
|
223 |
val ([a], ctxt') = Variable.variant_fixes ["a"] ctxt;
|
|
224 |
val resl = map (fn x => @{thm equivp_rspl} OF [x]) equivps;
|
|
225 |
val resr = map (fn x => @{thm equivp_rspr} OF [x]) equivps;
|
|
226 |
val ths_loc = prove_by_rel_induct alphas (build_alpha_bn_rsp_gl a) ind
|
|
227 |
(alpha_bn_rsp_tac simps (resl @ resr) exhausts a) alpha_bns ctxt
|
|
228 |
in
|
|
229 |
Variable.export ctxt' ctxt ths_loc
|
|
230 |
end
|
|
231 |
*}
|
1573
|
232 |
|
1656
|
233 |
ML {*
|
|
234 |
fun build_alpha_alpha_bn_gl alphas alpha_bn ctxt =
|
|
235 |
let
|
|
236 |
val ty = domain_type (fastype_of alpha_bn);
|
|
237 |
val (l, r) = the (AList.lookup (op=) alphas ty);
|
|
238 |
in
|
|
239 |
([alpha_bn $ l $ r], ctxt)
|
1573
|
240 |
end
|
1656
|
241 |
*}
|
|
242 |
|
|
243 |
ML {*
|
|
244 |
fun prove_alpha_alphabn alphas ind simps alpha_bns ctxt =
|
|
245 |
prove_by_rel_induct alphas build_alpha_alpha_bn_gl ind
|
|
246 |
(fn _ => asm_full_simp_tac (HOL_ss addsimps simps)) alpha_bns ctxt
|
|
247 |
*}
|
|
248 |
|
|
249 |
ML {*
|
|
250 |
fun build_rsp_gl alphas fnctn ctxt =
|
|
251 |
let
|
|
252 |
val typ = domain_type (fastype_of fnctn);
|
|
253 |
val (argl, argr) = the (AList.lookup (op=) alphas typ);
|
|
254 |
in
|
|
255 |
([HOLogic.mk_eq (fnctn $ argl, fnctn $ argr)], ctxt)
|
|
256 |
end
|
|
257 |
*}
|
|
258 |
|
|
259 |
ML {*
|
|
260 |
fun fvbv_rsp_tac' simps ctxt =
|
1673
e8cf0520c820
New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
261 |
asm_full_simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
|
1672
|
262 |
asm_full_simp_tac (HOL_ss addsimps (@{thms alphas} @ simps)) THEN_ALL_NEW
|
1656
|
263 |
REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW
|
|
264 |
asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW
|
|
265 |
TRY o blast_tac (claset_of ctxt)
|
|
266 |
*}
|
|
267 |
|
|
268 |
ML {*
|
|
269 |
fun build_fvbv_rsps alphas ind simps fnctns ctxt =
|
|
270 |
prove_by_rel_induct alphas build_rsp_gl ind (fvbv_rsp_tac' simps) fnctns ctxt
|
|
271 |
*}
|
|
272 |
|
|
273 |
end
|