# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269068699 -3600
# Node ID d375804ce6bada279282777390837ff25b13a6e1
# Parent  a5ba76208983c579c0611967712ec1d8c27a6581
Prove reflp for all relations.

diff -r a5ba76208983 -r d375804ce6ba Nominal/Fv.thy
--- a/Nominal/Fv.thy	Sat Mar 20 04:51:26 2010 +0100
+++ b/Nominal/Fv.thy	Sat Mar 20 08:04:59 2010 +0100
@@ -655,7 +655,7 @@
 *}
 
 ML {*
-fun build_alpha_refl_gl alphas (x, y, z) =
+fun build_alpha_sym_trans_gl alphas (x, y, z) =
 let
   fun build_alpha alpha =
     let
@@ -668,26 +668,54 @@
         HOLogic.mk_all (z, ty,
           HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3)))
     in
-      ((alpha $ var $ var), (symp, transp))
+      (symp, transp)
     end;
-  val (refl_eqs, eqs) = split_list (map build_alpha alphas)
+  val eqs = map build_alpha alphas
   val (sym_eqs, trans_eqs) = split_list eqs
   fun conj l = @{term Trueprop} $ foldr1 HOLogic.mk_conj l
 in
-  (conj refl_eqs, (conj sym_eqs, conj trans_eqs))
+  (conj sym_eqs, conj trans_eqs)
 end
 *}
 
 ML {*
-fun reflp_tac induct inj ctxt =
+fun build_alpha_refl_gl fv_alphas_lst =
+let
+  val (fvs_alphas, ls) = split_list fv_alphas_lst;
+  val (_, alpha_ts) = split_list fvs_alphas;
+  val tys = map (domain_type o fastype_of) alpha_ts;
+  val names = Datatype_Prop.make_tnames tys;
+  val args = map Free (names ~~ tys);
+  fun mk_alpha_refl arg (_, alpha) = alpha $ arg $ arg;
+  fun refl_eq_arg ((alpha, arg), l) =
+    foldr1 HOLogic.mk_conj
+      ((alpha $ arg $ arg) ::
+       (map (mk_alpha_refl arg) l))
+  val eqs = map refl_eq_arg ((alpha_ts ~~ args) ~~ ls)
+in
+  (names, HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj eqs))
+end
+*}
+
+ML {*
+fun reflp_tac induct eq_iff ctxt =
   rtac induct THEN_ALL_NEW
-  simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW
+  simp_tac ((mk_minimal_ss ctxt) addsimps eq_iff) THEN_ALL_NEW
   split_conjs THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
   THEN_ALL_NEW split_conjs THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
      @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv
        add_0_left supp_zero_perm Int_empty_left split_conv})
 *}
 
+ML {*
+fun build_alpha_refl fv_alphas_lst induct eq_iff ctxt =
+let
+  val (names, gl) = build_alpha_refl_gl fv_alphas_lst;
+  val refl_conj = Goal.prove ctxt names [] gl (fn _ => reflp_tac induct eq_iff ctxt 1);
+in
+  HOLogic.conj_elims refl_conj
+end
+*}
 
 lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi"
 apply (erule exE)
@@ -787,25 +815,22 @@
 *}
 
 ML {*
-fun build_equivps alphas term_induct alpha_induct term_inj alpha_inj distinct cases eqvt ctxt =
+fun build_equivps alphas reflps alpha_induct term_inj alpha_inj distinct cases eqvt ctxt =
 let
   val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt;
-  val (reflg, (symg, transg)) = build_alpha_refl_gl alphas (x, y, z)
-  fun reflp_tac' _ = reflp_tac term_induct alpha_inj ctxt 1;
+  val (symg, transg) = build_alpha_sym_trans_gl alphas (x, y, z)
   fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt ctxt 1;
   fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1;
-  val reflt = Goal.prove ctxt' [] [] reflg reflp_tac';
-  val symt = Goal.prove ctxt' [] [] symg symp_tac';
-  val transt = Goal.prove ctxt' [] [] transg transp_tac';
-  val [refltg, symtg, transtg] = Variable.export ctxt' ctxt [reflt, symt, transt]
-  val reflts = HOLogic.conj_elims refltg
-  val symts = HOLogic.conj_elims symtg
-  val transts = HOLogic.conj_elims transtg
+  val symp_loc = Goal.prove ctxt' [] [] symg symp_tac';
+  val transp_loc = Goal.prove ctxt' [] [] transg transp_tac';
+  val [symp, transp] = Variable.export ctxt' ctxt [symp_loc, transp_loc]
+  val symps = HOLogic.conj_elims symp
+  val transps = HOLogic.conj_elims transp
   fun equivp alpha =
     let
       val equivp = Const (@{const_name equivp}, fastype_of alpha --> @{typ bool})
       val goal = @{term Trueprop} $ (equivp $ alpha)
-      fun tac _ = equivp_tac reflts symts transts 1
+      fun tac _ = equivp_tac reflps symps transps 1
     in
       Goal.prove ctxt [] [] goal tac
     end
diff -r a5ba76208983 -r d375804ce6ba Nominal/Parser.thy
--- a/Nominal/Parser.thy	Sat Mar 20 04:51:26 2010 +0100
+++ b/Nominal/Parser.thy	Sat Mar 20 08:04:59 2010 +0100
@@ -332,9 +332,11 @@
     else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff @ raw_fv_bv_eqvt) lthy6a 1
   val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6a;
   val _ = tracing "Proving equivalence";
+  val fv_alpha_all = combine_fv_alpha_bns (fv_ts_nobn, fv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
+  val reflps = build_alpha_refl fv_alpha_all induct alpha_eq_iff lthy6a;
   val alpha_equivp =
     if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts_nobn
-    else build_equivps alpha_ts induct alpha_induct
+    else build_equivps alpha_ts reflps alpha_induct
       inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6a;
   val qty_binds = map (fn (_, b, _, _) => b) dts;
   val qty_names = map Name.of_binding qty_binds;