126 (map (Quotient_Tacs.lifted ctxt qtys simps |
141 (map (Quotient_Tacs.lifted ctxt qtys simps |
127 #> unraw_bounds_thm |
142 #> unraw_bounds_thm |
128 #> unraw_vars_thm |
143 #> unraw_vars_thm |
129 #> Drule.zero_var_indexes) thms, ctxt) |
144 #> Drule.zero_var_indexes) thms, ctxt) |
130 |
145 |
|
146 |
|
147 |
|
148 fun mk_supports_goal ctxt qtrm = |
|
149 let |
|
150 val vs = fresh_args ctxt qtrm |
|
151 val rhs = list_comb (qtrm, vs) |
|
152 val lhs = fold (curry HOLogic.mk_prod) vs @{term "()"} |
|
153 |> mk_supp |
|
154 in |
|
155 mk_supports lhs rhs |
|
156 |> HOLogic.mk_Trueprop |
|
157 end |
|
158 |
|
159 fun supports_tac ctxt perm_simps = |
|
160 let |
|
161 val ss1 = HOL_basic_ss addsimps @{thms supports_def fresh_def[symmetric]} |
|
162 val ss2 = HOL_ss addsimps @{thms swap_fresh_fresh fresh_Pair} |
|
163 in |
|
164 EVERY' [ simp_tac ss1, |
|
165 Nominal_Permeq.eqvt_strict_tac ctxt perm_simps [], |
|
166 simp_tac ss2 ] |
|
167 end |
|
168 |
|
169 fun prove_supports_single ctxt perm_simps qtrm = |
|
170 let |
|
171 val goal = mk_supports_goal ctxt qtrm |
|
172 val ctxt' = Variable.auto_fixes goal ctxt |
|
173 in |
|
174 Goal.prove ctxt' [] [] goal |
|
175 (K (HEADGOAL (supports_tac ctxt perm_simps))) |
|
176 |> singleton (ProofContext.export ctxt' ctxt) |
|
177 end |
|
178 |
|
179 fun prove_supports ctxt perm_simps qtrms = |
|
180 map (prove_supports_single ctxt perm_simps) qtrms |
|
181 |
|
182 |
|
183 (* finite supp lemmas for qtypes *) |
|
184 |
|
185 fun prove_fsupp ctxt qtys qinduct qsupports_thms = |
|
186 let |
|
187 val (vs, ctxt') = Variable.variant_fixes (replicate (length qtys) "x") ctxt |
|
188 val goals = vs ~~ qtys |
|
189 |> map Free |
|
190 |> map (mk_finite o mk_supp) |
|
191 |> foldr1 (HOLogic.mk_conj) |
|
192 |> HOLogic.mk_Trueprop |
|
193 |
|
194 val tac = |
|
195 EVERY' [ rtac @{thm supports_finite}, |
|
196 resolve_tac qsupports_thms, |
|
197 asm_simp_tac (HOL_ss addsimps @{thms finite_supp supp_Pair finite_Un}) ] |
|
198 in |
|
199 Goal.prove ctxt' [] [] goals |
|
200 (K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac))) |
|
201 |> singleton (ProofContext.export ctxt' ctxt) |
|
202 |> Datatype_Aux.split_conj_thm |
|
203 |> map zero_var_indexes |
|
204 end |
|
205 |
|
206 |
|
207 (* finite supp instances *) |
|
208 |
|
209 fun fs_instance qtys qfull_ty_names tvs qfsupp_thms lthy = |
|
210 let |
|
211 val lthy1 = |
|
212 lthy |
|
213 |> Local_Theory.exit_global |
|
214 |> Class.instantiation (qfull_ty_names, tvs, @{sort fs}) |
|
215 |
|
216 fun tac _ = |
|
217 Class.intro_classes_tac [] THEN |
|
218 (ALLGOALS (resolve_tac qfsupp_thms)) |
|
219 in |
|
220 lthy1 |
|
221 |> Class.prove_instantiation_exit tac |
|
222 |> Named_Target.theory_init |
|
223 end |
|
224 |
|
225 |
|
226 (* proves that fv and fv_bn equals supp *) |
|
227 |
|
228 fun gen_mk_goals fv supp = |
|
229 let |
|
230 val arg_ty = |
|
231 fastype_of fv |
|
232 |> domain_type |
|
233 in |
|
234 (arg_ty, fn x => HOLogic.mk_eq (fv $ x, supp x)) |
|
235 end |
|
236 |
|
237 fun mk_fvs_goals fv = gen_mk_goals fv mk_supp |
|
238 fun mk_fv_bns_goals fv_bn alpha_bn = gen_mk_goals fv_bn (mk_supp_rel alpha_bn) |
|
239 |
|
240 fun add_ss thms = |
|
241 HOL_basic_ss addsimps thms |
|
242 |
|
243 fun symmetric thms = |
|
244 map (fn thm => thm RS @{thm sym}) thms |
|
245 |
|
246 val supp_Abs_set = @{thms supp_Abs(1)[symmetric]} |
|
247 val supp_Abs_res = @{thms supp_Abs(2)[symmetric]} |
|
248 val supp_Abs_lst = @{thms supp_Abs(3)[symmetric]} |
|
249 |
|
250 fun mk_supp_abs ctxt (BC (Set, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_set |
|
251 | mk_supp_abs ctxt (BC (Res, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_res |
|
252 | mk_supp_abs ctxt (BC (Lst, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_lst |
|
253 |
|
254 fun mk_supp_abs_tac ctxt [] = [] |
|
255 | mk_supp_abs_tac ctxt (BC (_, [], _)::xs) = mk_supp_abs_tac ctxt xs |
|
256 | mk_supp_abs_tac ctxt (bc::xs) = (DETERM o mk_supp_abs ctxt bc)::mk_supp_abs_tac ctxt xs |
|
257 |
|
258 fun mk_bn_supp_abs_tac trm = |
|
259 trm |
|
260 |> fastype_of |
|
261 |> body_type |
|
262 |> (fn ty => case ty of |
|
263 @{typ "atom set"} => simp_tac (add_ss supp_Abs_set) |
|
264 | @{typ "atom list"} => simp_tac (add_ss supp_Abs_lst) |
|
265 | _ => raise TERM ("mk_bn_supp_abs_tac", [trm])) |
|
266 |
|
267 |
|
268 val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc} |
|
269 val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un} |
|
270 val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel_def permute_prod_def |
|
271 prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] finite.emptyI} |
|
272 |
|
273 fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns fv_simps eq_iffs perm_simps |
|
274 fv_bn_eqvts qinduct bclausess ctxt = |
|
275 let |
|
276 val goals1 = map mk_fvs_goals fvs |
|
277 val goals2 = map2 mk_fv_bns_goals fv_bns alpha_bns |
|
278 |
|
279 fun tac ctxt = |
|
280 SUBGOAL (fn (goal, i) => |
|
281 let |
|
282 val (fv_fun, arg) = |
|
283 goal |> Envir.eta_contract |
|
284 |> Logic.strip_assums_concl |
|
285 |> HOLogic.dest_Trueprop |
|
286 |> fst o HOLogic.dest_eq |
|
287 |> dest_comb |
|
288 val supp_abs_tac = |
|
289 case (AList.lookup (op=) (qtrms ~~ bclausess) (head_of arg)) of |
|
290 SOME bclauses => EVERY' (mk_supp_abs_tac ctxt bclauses) |
|
291 | NONE => mk_bn_supp_abs_tac fv_fun |
|
292 in |
|
293 EVERY' [ TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)), |
|
294 TRY o supp_abs_tac, |
|
295 TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}), |
|
296 TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], |
|
297 TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)), |
|
298 TRY o asm_full_simp_tac (add_ss thms3), |
|
299 TRY o simp_tac (add_ss thms2), |
|
300 TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts)))] i |
|
301 end) |
|
302 in |
|
303 induct_prove qtys (goals1 @ goals2) qinduct tac ctxt |
|
304 |> map atomize |
|
305 |> map (simplify (HOL_basic_ss addsimps @{thms fun_eq_iff[symmetric]})) |
|
306 end |
|
307 |
|
308 |
|
309 fun prove_bns_finite qtys qbns qinduct qbn_simps ctxt = |
|
310 let |
|
311 fun mk_goal qbn = |
|
312 let |
|
313 val arg_ty = domain_type (fastype_of qbn) |
|
314 val finite = @{term "finite :: atom set => bool"} |
|
315 in |
|
316 (arg_ty, fn x => finite $ (to_set (qbn $ x))) |
|
317 end |
|
318 |
|
319 val props = map mk_goal qbns |
|
320 val ss_tac = asm_full_simp_tac (HOL_basic_ss addsimps (qbn_simps @ |
|
321 @{thms set.simps set_append finite_insert finite.emptyI finite_Un})) |
|
322 in |
|
323 induct_prove qtys props qinduct (K ss_tac) ctxt |
|
324 end |
|
325 |
|
326 fun prove_perm_bn_alpha_thms qtys qperm_bns alpha_bns qinduct qperm_bn_simps qeq_iffs qalpha_refls ctxt = |
|
327 let |
|
328 val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt |
|
329 val p = Free (p, @{typ perm}) |
|
330 |
|
331 fun mk_goal qperm_bn alpha_bn = |
|
332 let |
|
333 val arg_ty = domain_type (fastype_of alpha_bn) |
|
334 in |
|
335 (arg_ty, fn x => (mk_id (Abs ("", arg_ty, alpha_bn $ Bound 0 $ (qperm_bn $ p $ Bound 0)))) $ x) |
|
336 end |
|
337 |
|
338 val props = map2 mk_goal qperm_bns alpha_bns |
|
339 val ss = @{thm id_def}::qperm_bn_simps @ qeq_iffs @ qalpha_refls |
|
340 val ss_tac = asm_full_simp_tac (HOL_ss addsimps ss) |
|
341 in |
|
342 induct_prove qtys props qinduct (K ss_tac) ctxt' |
|
343 |> ProofContext.export ctxt' ctxt |
|
344 |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) |
|
345 end |
|
346 |
|
347 |
|
348 |
131 end (* structure *) |
349 end (* structure *) |
132 |
350 |