182 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; |
182 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; |
183 val alpha_gen = Syntax.check_term lthy alpha_gen_pre |
183 val alpha_gen = Syntax.check_term lthy alpha_gen_pre |
184 val pi_supps = map ((curry op $) @{term "supp :: perm \<Rightarrow> atom set"}) rpis; |
184 val pi_supps = map ((curry op $) @{term "supp :: perm \<Rightarrow> atom set"}) rpis; |
185 val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"}) |
185 val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"}) |
186 in |
186 in |
187 if length pi_supps > 1 then |
187 (*if length pi_supps > 1 then |
188 HOLogic.mk_conj (alpha_gen, pi_supps_eq) else alpha_gen |
188 HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*) alpha_gen |
189 (* TODO Add some test that is makes sense *) |
189 (* TODO Add some test that is makes sense *) |
190 end else @{term "True"} |
190 end else @{term "True"} |
191 end |
191 end |
192 val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2)) |
192 val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2)) |
193 val alpha_lhss = mk_conjl alphas |
193 val alpha_lhss = mk_conjl alphas |
370 apply (erule exE)+ |
370 apply (erule exE)+ |
371 apply (rule_tac x="pia + pi" in exI) |
371 apply (rule_tac x="pia + pi" in exI) |
372 by auto |
372 by auto |
373 |
373 |
374 ML {* |
374 ML {* |
|
375 fun is_ex (Const ("Ex", _) $ Abs _) = true |
|
376 | is_ex _ = false; |
|
377 *} |
|
378 |
|
379 ML {* |
|
380 fun eetac rule = Subgoal.FOCUS_PARAMS |
|
381 (fn (focus) => |
|
382 let |
|
383 val concl = #concl focus |
|
384 val prems = Logic.strip_imp_prems (term_of concl) |
|
385 val exs = filter (fn x => is_ex (HOLogic.dest_Trueprop x)) prems |
|
386 val cexs = map (SOME o (cterm_of (ProofContext.theory_of (#context focus)))) exs |
|
387 val thins = map (fn cex => Drule.instantiate' [] [cex] Drule.thin_rl) cexs |
|
388 in |
|
389 (etac rule THEN' RANGE[ |
|
390 atac, |
|
391 eresolve_tac thins |
|
392 ]) 1 |
|
393 end |
|
394 ) |
|
395 *} |
|
396 |
|
397 ML {* |
375 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt = |
398 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt = |
376 ((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
399 ind_tac induct THEN_ALL_NEW |
377 (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW |
400 (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW |
378 ( |
401 asm_full_simp_tac ((mk_minimal_ss ctxt) addsimps alpha_inj) THEN_ALL_NEW |
379 asm_full_simp_tac (HOL_ss addsimps alpha_inj @ term_inj @ distinct) |
402 split_conjs THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conjs |
380 THEN_ALL_NEW (REPEAT o etac conjE THEN' etac @{thm exi_sum} THEN' RANGE [atac]) THEN_ALL_NEW |
403 THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct))) |
381 (REPEAT o etac conjE THEN' (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) |
404 THEN_ALL_NEW split_conjs THEN_ALL_NEW |
382 THEN_ALL_NEW (asm_full_simp_tac HOL_ss) THEN_ALL_NEW |
405 TRY o (etac @{thm alpha_gen_compose_trans} THEN' RANGE[atac]) THEN_ALL_NEW |
383 (etac @{thm alpha_gen_compose_trans} THEN' RANGE[atac]) THEN_ALL_NEW |
406 (asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ eqvt @ term_inj @ distinct))) |
384 (asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: eqvt))) |
|
385 ) |
|
386 *} |
407 *} |
387 |
408 |
388 lemma transp_aux: |
409 lemma transp_aux: |
389 "(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> transp R" |
410 "(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> transp R" |
390 unfolding transp_def |
411 unfolding transp_def |