--- 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