321 in |
325 in |
322 Variable.export ctxt' ctxt thms |
326 Variable.export ctxt' ctxt thms |
323 |> map mk_simp_rule |
327 |> map mk_simp_rule |
324 end |
328 end |
325 |
329 |
|
330 |
|
331 |
|
332 (** symmetry proof for the alphas **) |
|
333 |
|
334 val exi_neg = @{lemma "(EX (p::perm). P p) ==> (!!q. P q ==> Q (- q)) ==> EX p. Q p" |
|
335 by (erule exE, rule_tac x="-p" in exI, auto)} |
|
336 |
|
337 (* for premises that contain binders *) |
|
338 fun prem_bound_tac pred_names ctxt = |
|
339 let |
|
340 fun trans_prem_tac pred_names ctxt = |
|
341 SUBPROOF (fn {prems, context, ...} => |
|
342 let |
|
343 val prems' = map (transform_prem1 context pred_names) prems |
|
344 in |
|
345 resolve_tac prems' 1 |
|
346 end) ctxt |
|
347 val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def prod_rel.simps alphas} |
|
348 in |
|
349 EVERY' |
|
350 [ etac exi_neg, |
|
351 resolve_tac @{thms alpha_gen_sym_eqvt}, |
|
352 asm_full_simp_tac (HOL_ss addsimps prod_simps), |
|
353 Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl}, |
|
354 trans_prem_tac pred_names ctxt ] |
|
355 end |
|
356 |
|
357 fun prove_sym_tac pred_names intros induct ctxt = |
|
358 let |
|
359 val prem_eq_tac = rtac @{thm sym} THEN' atac |
|
360 val prem_unbound_tac = atac |
|
361 |
|
362 val prem_cases_tacs = FIRST' |
|
363 [prem_eq_tac, prem_unbound_tac, prem_bound_tac pred_names ctxt] |
|
364 in |
|
365 HEADGOAL (rtac induct THEN_ALL_NEW |
|
366 (resolve_tac intros THEN_ALL_NEW prem_cases_tacs)) |
|
367 end |
|
368 |
|
369 fun prep_sym_goal alpha_trm (arg1, arg2) = |
|
370 let |
|
371 val lhs = alpha_trm $ arg1 $ arg2 |
|
372 val rhs = alpha_trm $ arg2 $ arg1 |
|
373 in |
|
374 HOLogic.mk_imp (lhs, rhs) |
|
375 end |
|
376 |
|
377 fun raw_prove_sym alpha_trms alpha_intros alpha_induct ctxt = |
|
378 let |
|
379 val alpha_names = map (fst o dest_Const) alpha_trms |
|
380 val arg_tys = |
|
381 alpha_trms |
|
382 |> map fastype_of |
|
383 |> map domain_type |
|
384 val (arg_names1, (arg_names2, ctxt')) = |
|
385 ctxt |
|
386 |> Variable.variant_fixes (replicate (length arg_tys) "x") |
|
387 ||> Variable.variant_fixes (replicate (length arg_tys) "y") |
|
388 val args1 = map Free (arg_names1 ~~ arg_tys) |
|
389 val args2 = map Free (arg_names2 ~~ arg_tys) |
|
390 val goal = HOLogic.mk_Trueprop |
|
391 (foldr1 HOLogic.mk_conj (map2 prep_sym_goal alpha_trms (args1 ~~ args2))) |
|
392 in |
|
393 Goal.prove ctxt' [] [] goal |
|
394 (fn {context,...} => prove_sym_tac alpha_names alpha_intros alpha_induct context) |
|
395 |> singleton (ProofContext.export ctxt' ctxt) |
|
396 |> Datatype_Aux.split_conj_thm |
|
397 |> map (fn th => zero_var_indexes (th RS mp)) |
|
398 end |
|
399 |
|
400 |
|
401 (** transitivity proof for alphas **) |
|
402 |
|
403 fun prove_trans_tac pred_names raw_dt_thms intros induct cases ctxt = |
|
404 let |
|
405 val _ = ("induct\n" ^ Syntax.string_of_term ctxt (prop_of induct)) |
|
406 |
|
407 val tac1 = asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms) |
|
408 fun tac i = (EVERY' [rtac @{thm allI}, rtac @{thm impI}, rotate_tac ~1, |
|
409 etac (nth cases i) THEN_ALL_NEW tac1]) i |
|
410 in |
|
411 HEADGOAL (rtac induct THEN_ALL_NEW tac) |
|
412 end |
|
413 |
|
414 fun prep_trans_goal alpha_trm ((arg1, arg2), arg_ty) = |
|
415 let |
|
416 val lhs = alpha_trm $ arg1 $ arg2 |
|
417 val mid = alpha_trm $ arg2 $ (Bound 0) |
|
418 val rhs = alpha_trm $ arg1 $ (Bound 0) |
|
419 in |
|
420 HOLogic.mk_imp (lhs, |
|
421 HOLogic.all_const arg_ty $ Abs ("z", arg_ty, |
|
422 HOLogic.mk_imp (mid, rhs))) |
|
423 end |
|
424 |
|
425 fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases ctxt = |
|
426 let |
|
427 val alpha_names = map (fst o dest_Const) alpha_trms |
|
428 val arg_tys = |
|
429 alpha_trms |
|
430 |> map fastype_of |
|
431 |> map domain_type |
|
432 val (arg_names1, (arg_names2, ctxt')) = |
|
433 ctxt |
|
434 |> Variable.variant_fixes (replicate (length arg_tys) "x") |
|
435 ||> Variable.variant_fixes (replicate (length arg_tys) "y") |
|
436 val args1 = map Free (arg_names1 ~~ arg_tys) |
|
437 val args2 = map Free (arg_names2 ~~ arg_tys) |
|
438 val goal = HOLogic.mk_Trueprop |
|
439 (foldr1 HOLogic.mk_conj (map2 prep_trans_goal alpha_trms (args1 ~~ args2 ~~ arg_tys))) |
|
440 in |
|
441 Goal.prove ctxt' [] [] goal |
|
442 (fn {context,...} => |
|
443 prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_induct alpha_cases context) |
|
444 |> singleton (ProofContext.export ctxt' ctxt) |
|
445 |> Datatype_Aux.split_conj_thm |
|
446 end |
|
447 |
326 end (* structure *) |
448 end (* structure *) |
327 |
449 |