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 |
310 (conj refl_eqs, (conj sym_eqs, conj trans_eqs)) |
310 (conj refl_eqs, (conj sym_eqs, conj trans_eqs)) |
311 end |
311 end |
312 *} |
312 *} |
313 |
313 |
314 ML {* |
314 ML {* |
315 fun reflp_tac induct inj = |
315 fun reflp_tac induct inj ctxt = |
316 rtac induct THEN_ALL_NEW |
316 rtac induct THEN_ALL_NEW |
317 asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW |
317 simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW |
318 (* TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW*) |
318 split_conjs THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]} |
319 (rtac @{thm exI[of _ "0 :: perm"]} THEN' |
319 THEN_ALL_NEW split_conjs THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps |
320 asm_full_simp_tac (HOL_ss addsimps |
320 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv |
321 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) |
321 add_0_left supp_zero_perm Int_empty_left}) |
322 *} |
322 *} |
|
323 |
323 |
324 |
324 lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi" |
325 lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi" |
325 apply (erule exE) |
326 apply (erule exE) |
326 apply (rule_tac x="-pi" in exI) |
327 apply (rule_tac x="-pi" in exI) |
327 by auto |
328 by auto |
328 |
329 |
329 ML {* |
330 ML {* |
330 fun symp_tac induct inj eqvt = |
331 fun symp_tac induct inj eqvt ctxt = |
331 (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
332 ind_tac induct THEN_ALL_NEW |
332 asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW |
333 simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW split_conjs |
333 (REPEAT o etac conjE THEN' etac @{thm exi_neg} THEN' REPEAT o etac conjE THEN' |
334 THEN_ALL_NEW |
334 (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW |
335 REPEAT o etac @{thm exi_neg} |
335 (asm_full_simp_tac HOL_ss) THEN_ALL_NEW |
336 THEN_ALL_NEW |
336 (etac @{thm alpha_gen_compose_sym} THEN' |
337 split_conjs THEN_ALL_NEW |
337 (asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: eqvt))))) |
338 asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW |
|
339 (rtac @{thm alpha_gen_compose_sym} THEN' RANGE [ |
|
340 (asm_full_simp_tac (HOL_ss addsimps @{thms plus_perm_eq})), |
|
341 (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt))) |
|
342 ]) |
338 *} |
343 *} |
339 |
344 |
340 ML {* |
345 ML {* |
341 fun imp_elim_tac case_rules = |
346 fun imp_elim_tac case_rules = |
342 Subgoal.FOCUS (fn {concl, context, ...} => |
347 Subgoal.FOCUS (fn {concl, context, ...} => |
365 apply (erule exE)+ |
370 apply (erule exE)+ |
366 apply (rule_tac x="pia + pi" in exI) |
371 apply (rule_tac x="pia + pi" in exI) |
367 by auto |
372 by auto |
368 |
373 |
369 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 {* |
370 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 = |
371 ((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
399 ind_tac induct THEN_ALL_NEW |
372 (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 |
373 ( |
401 asm_full_simp_tac ((mk_minimal_ss ctxt) addsimps alpha_inj) THEN_ALL_NEW |
374 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 |
375 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))) |
376 (REPEAT o etac conjE THEN' (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) |
404 THEN_ALL_NEW split_conjs THEN_ALL_NEW |
377 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 |
378 (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))) |
379 (asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: eqvt))) |
|
380 ) |
|
381 *} |
407 *} |
382 |
408 |
383 lemma transp_aux: |
409 lemma transp_aux: |
384 "(\<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" |
385 unfolding transp_def |
411 unfolding transp_def |
398 ML {* |
424 ML {* |
399 fun build_equivps alphas term_induct alpha_induct term_inj alpha_inj distinct cases eqvt ctxt = |
425 fun build_equivps alphas term_induct alpha_induct term_inj alpha_inj distinct cases eqvt ctxt = |
400 let |
426 let |
401 val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt; |
427 val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt; |
402 val (reflg, (symg, transg)) = build_alpha_refl_gl alphas (x, y, z) |
428 val (reflg, (symg, transg)) = build_alpha_refl_gl alphas (x, y, z) |
403 fun reflp_tac' _ = reflp_tac term_induct alpha_inj 1; |
429 fun reflp_tac' _ = reflp_tac term_induct alpha_inj ctxt 1; |
404 fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt 1; |
430 fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt ctxt 1; |
405 fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1; |
431 fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1; |
406 val reflt = Goal.prove ctxt' [] [] reflg reflp_tac'; |
432 val reflt = Goal.prove ctxt' [] [] reflg reflp_tac'; |
407 val symt = Goal.prove ctxt' [] [] symg symp_tac'; |
433 val symt = Goal.prove ctxt' [] [] symg symp_tac'; |
408 val transt = Goal.prove ctxt' [] [] transg transp_tac'; |
434 val transt = Goal.prove ctxt' [] [] transg transp_tac'; |
409 val [refltg, symtg, transtg] = Variable.export ctxt' ctxt [reflt, symt, transt] |
435 val [refltg, symtg, transtg] = Variable.export ctxt' ctxt [reflt, symt, transt] |