
diff -r 160343d86a6f -r 20f76fde8ef1 Quot/Nominal/Fv.thy
--- a/Quot/Nominal/Fv.thy	Tue Feb 23 13:32:35 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Tue Feb 23 13:33:01 2010 +0100
@@ -90,6 +90,7 @@
 
 *}
 
+(* TODO: Notice datatypes without bindings and replace alpha with equality *)
 ML {*
 (* Currently needs just one full_tname to access Datatype *)
 fun define_fv_alpha full_tname bindsall lthy =
@@ -219,11 +220,11 @@
 ML {*
 fun alpha_inj_tac dist_inj intrs elims =
   SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE'
-  rtac @{thm iffI} THEN' RANGE [
+  (rtac @{thm iffI} THEN' RANGE [
      (eresolve_tac elims THEN_ALL_NEW
        asm_full_simp_tac (HOL_ss addsimps dist_inj)
      ),
-     (asm_full_simp_tac (HOL_ss addsimps intrs))]
+     asm_full_simp_tac (HOL_ss addsimps intrs)])
 *}
 
 ML {*
@@ -251,4 +252,148 @@
 end
 *}
 
+ML {*
+fun build_alpha_refl_gl alphas (x, y, z) =
+let
+  fun build_alpha alpha =
+    let
+      val ty = domain_type (fastype_of alpha);
+      val var = Free(x, ty);
+      val var2 = Free(y, ty);
+      val var3 = Free(z, ty);
+      val symp = HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var);
+      val transp = HOLogic.mk_imp (alpha $ var $ var2,
+        HOLogic.mk_all (z, ty,
+          HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3)))
+    in
+      ((alpha $ var $ var), (symp, transp))
+    end;
+  val (refl_eqs, eqs) = split_list (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))
 end
+*}
+
+ML {*
+fun reflp_tac induct inj =
+  rtac induct THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW
+  TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
+  (rtac @{thm exI[of _ "0 :: perm"]} THEN'
+   asm_full_simp_tac (HOL_ss addsimps
+     @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv}))
+*}
+
+ML {*
+fun symp_tac induct inj eqvt =
+  ((rtac @{thm impI} THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW
+  TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
+  (etac @{thm alpha_gen_compose_sym} THEN' eresolve_tac eqvt)
+*}
+
+ML {*
+fun imp_elim_tac case_rules =
+  Subgoal.FOCUS (fn {concl, context, ...} =>
+    case term_of concl of
+      _ $ (_ $ asm $ _) =>
+        let
+          fun filter_fn case_rule = (
+            case Logic.strip_assums_hyp (prop_of case_rule) of
+              ((_ $ asmc) :: _) =>
+                let
+                  val thy = ProofContext.theory_of context
+                in
+                  Pattern.matches thy (asmc, asm)
+                end
+            | _ => false)
+          val matching_rules = filter filter_fn case_rules
+        in
+         (rtac impI THEN' rotate_tac (~1) THEN' eresolve_tac matching_rules) 1
+        end
+    | _ => no_tac
+  )
+*}
+
+ML {*
+fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt =
+  ((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
+  (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW
+  (
+    asm_full_simp_tac (HOL_ss addsimps alpha_inj @ term_inj @ distinct) THEN'
+    TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
+    (etac @{thm alpha_gen_compose_trans} THEN' RANGE [atac, eresolve_tac eqvt])
+  )
+*}
+
+lemma transp_aux:
+  "(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> transp R"
+  unfolding transp_def
+  by blast
+
+ML {*
+fun equivp_tac reflps symps transps =
+  simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def})
+  THEN' rtac conjI THEN' rtac allI THEN'
+  resolve_tac reflps THEN'
+  rtac conjI THEN' rtac allI THEN' rtac allI THEN'
+  resolve_tac symps THEN'
+  rtac @{thm transp_aux} THEN' resolve_tac transps
+*}
+
+ML {*
+fun build_equivps alphas term_induct 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 1;
+  fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt 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
+  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
+    in
+      Goal.prove ctxt [] [] goal tac
+    end
+in
+  map equivp alphas
+end
+*}
+
+(*
+Tests:
+prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
+by (tactic {* reflp_tac @{thm rtrm1_bp.induct} @{thms alpha1_inj} 1 *})
+
+prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
+by (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms alpha1_eqvt} 1 *})
+
+prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
+by (tactic {* transp_tac @{context} @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms rtrm1.inject bp.inject} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} 1 *})
+
+lemma alpha1_equivp:
+  "equivp alpha_rtrm1"
+  "equivp alpha_bp"
+apply (tactic {*
+  (simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def})
+  THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN'
+  resolve_tac (HOLogic.conj_elims @{thm alpha1_reflp_aux})
+  THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN'
+  resolve_tac (HOLogic.conj_elims @{thm alpha1_symp_aux}) THEN' rtac @{thm transp_aux}
+  THEN' resolve_tac (HOLogic.conj_elims @{thm alpha1_transp_aux})
+)
+1 *})
+done*)
+
+end




