# HG changeset patch # User Cezary Kaliszyk # Date 1266594324 -3600 # Node ID 5770c73f24153ae736cc790d937f1b44273b0d7e # Parent 5523d5713a65650429dc8cf51f299839c890cbe7 Automatic production and proving of pseudo-injectivity. diff -r 5523d5713a65 -r 5770c73f2415 Quot/Nominal/Fv.thy --- a/Quot/Nominal/Fv.thy Fri Feb 19 12:05:58 2010 +0100 +++ b/Quot/Nominal/Fv.thy Fri Feb 19 16:45:24 2010 +0100 @@ -215,23 +215,39 @@ print_theorems *) + ML {* -fun build_alpha_inj_gl thms ctxt = +fun alpha_inj_tac dist_inj intrs elims = + SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE' + 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))] +*} + +ML {* +fun build_alpha_inj_gl thm = + let + val prop = prop_of thm; + val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop); + val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop); + fun list_conj l = foldr1 HOLogic.mk_conj l; + in + if hyps = [] then concl + else HOLogic.mk_eq (concl, list_conj hyps) + end; +*} + +ML {* +fun build_alpha_inj intrs dist_inj elims ctxt = let - (* TODO: use the context for export *) - val ((_, thms_imp), ctxt') = Variable.import false thms ctxt; - fun inj_thm thm_imp = - let - val prop = prop_of thm_imp; - val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop); - val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop); - fun list_conj l = foldr1 HOLogic.mk_conj l; - in - if hyps = [] then concl - else HOLogic.mk_eq (concl, list_conj hyps) - end; + val ((_, thms_imp), ctxt') = Variable.import false intrs ctxt; + val gls = map (HOLogic.mk_Trueprop o build_alpha_inj_gl) thms_imp; + fun tac _ = alpha_inj_tac dist_inj intrs elims 1; + val thms = map (fn gl => Goal.prove ctxt' [] [] gl tac) gls; in - Logic.mk_conjunction_list (map (HOLogic.mk_Trueprop o inj_thm) thms_imp) + Variable.export ctxt' ctxt thms end *} diff -r 5523d5713a65 -r 5770c73f2415 Quot/Nominal/Terms.thy --- a/Quot/Nominal/Terms.thy Fri Feb 19 12:05:58 2010 +0100 +++ b/Quot/Nominal/Terms.thy Fri Feb 19 16:45:24 2010 +0100 @@ -31,22 +31,10 @@ setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *} -ML {* - val elims_ref = ref (@{thms refl}) - val intrs_ref = ref (@{thms refl}) -*} -ML elims_ref local_setup {* -fn ctxt => - let val ((fv, ind), ctxt') = - define_fv_alpha "Terms.rtrm1" + snd o define_fv_alpha "Terms.rtrm1" [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]], - [[], [[]], [[], []]]] ctxt; - val elims' = ProofContext.export ctxt' ctxt (#elims ind) - val intrs' = ProofContext.export ctxt' ctxt (#intrs ind) - val _ = (elims_ref := elims'); - val _ = (intrs_ref := intrs'); - in ctxt' end *} + [[], [[]], [[], []]]] *} print_theorems notation @@ -54,38 +42,8 @@ alpha_bp ("_ \1b _" [100, 100] 100) thm alpha_rtrm1_alpha_bp.intros -prove {* build_alpha_inj_gl @{thms alpha_rtrm1_alpha_bp.intros} @{context} *} -apply - -prefer 4 -apply (rule iffI) -apply (tactic {* eresolve_tac (!elims_ref) 1 *}) -apply (simp only: rtrm1.distinct) -apply (simp only: rtrm1.distinct) -apply (simp only: rtrm1.distinct) -apply (rule conjI) apply (simp only: rtrm1.inject) -apply (rule conjI) apply (simp only: rtrm1.inject) -apply (simp only: rtrm1.inject) -apply (simp only: alpha_rtrm1_alpha_bp.intros) -sorry - -lemma alpha1_inj: -"(rVr1 a \1 rVr1 b) = (a = b)" -"(rAp1 t1 s1 \1 rAp1 t2 s2) = (t1 \1 t2 \ s1 \1 s2)" -"(rLm1 aa t \1 rLm1 ab s) = (\pi. (({atom aa}, t) \gen alpha_rtrm1 fv_rtrm1 pi ({atom ab}, s)))" -"(rLt1 bp rtrm11 rtrm12 \1 rLt1 bpa rtrm11a rtrm12a) = - ((\pi. (bv1 bp, bp) \gen alpha_bp fv_bp pi (bv1 bpa, bpa)) \ rtrm11 \1 rtrm11a \ - (\pi. (bv1 bp, rtrm12) \gen alpha_rtrm1 fv_rtrm1 pi (bv1 bpa, rtrm12a)))" -"alpha_bp BUnit BUnit" -"(alpha_bp (BVr name) (BVr namea)) = (name = namea)" -"(alpha_bp (BPr bp1 bp2) (BPr bp1a bp2a)) = (alpha_bp bp1 bp1a \ alpha_bp bp2 bp2a)" -apply - -apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros) -apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros) -apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros) -apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros) -apply rule apply (erule alpha_bp.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros) -apply rule apply (erule alpha_bp.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros) -done +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases} ctxt)) ctxt)) *} +thm alpha1_inj lemma alpha_bp_refl: "alpha_bp a a" apply induct @@ -344,13 +302,16 @@ local_setup {* snd o define_fv_alpha "Terms.rtrm2" [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv2}, 0)], [(SOME @{term rbv2}, 0)]]], [[[], []]]] *} -print_theorems notation alpha_rtrm2 ("_ \2 _" [100, 100] 100) and alpha_rassign ("_ \2b _" [100, 100] 100) thm alpha_rtrm2_alpha_rassign.intros +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha2_inj}, []), (build_alpha_inj @{thms alpha_rtrm2_alpha_rassign.intros} @{thms rtrm2.distinct rtrm2.inject rassign.distinct rassign.inject} @{thms alpha_rtrm2.cases alpha_rassign.cases} ctxt)) ctxt)) *} +thm alpha2_inj + + lemma alpha2_equivp: "equivp alpha_rtrm2" "equivp alpha_rassign" @@ -492,28 +453,8 @@ alpha_rlts ("_ \l _" [100, 100] 100) thm alpha_rtrm5_alpha_rlts.intros -lemma alpha5_inj: - "((rVr5 a) \5 (rVr5 b)) = (a = b)" - "(rAp5 t1 s1 \5 rAp5 t2 s2) = (t1 \5 t2 \ s1 \5 s2)" - "(rLt5 l1 t1 \5 rLt5 l2 t2) = ((\pi. ((rbv5 l1, t1) \gen alpha_rtrm5 fv_rtrm5 pi (rbv5 l2, t2))) \ - (\pi. ((rbv5 l1, l1) \gen alpha_rlts fv_rlts pi (rbv5 l2, l2))))" - "rLnil \l rLnil" - "(rLcons n1 t1 ls1 \l rLcons n2 t2 ls2) = (n1 = n2 \ ls1 \l ls2 \ t1 \5 t2)" -apply - -apply (simp_all add: alpha_rtrm5_alpha_rlts.intros) -apply rule -apply (erule alpha_rtrm5.cases) -apply (simp_all add: alpha_rtrm5_alpha_rlts.intros) -apply rule -apply (erule alpha_rtrm5.cases) -apply (simp_all add: alpha_rtrm5_alpha_rlts.intros) -apply rule -apply (erule alpha_rtrm5.cases) -apply (simp_all add: alpha_rtrm5_alpha_rlts.intros) -apply rule -apply (erule alpha_rlts.cases) -apply (simp_all add: alpha_rtrm5_alpha_rlts.intros) -done +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases} ctxt)) ctxt)) *} +thm alpha5_inj lemma alpha5_equivps: shows "equivp alpha_rtrm5" @@ -560,6 +501,15 @@ apply(unfold alpha_gen) apply (erule conjE)+ apply (rule conjI) + apply (rule_tac x="x \ pi" in exI) + apply (rule conjI) + apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1]) + apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt) + apply(rule conjI) + apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1]) + apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt) + apply (subst permute_eqvt[symmetric]) + apply (simp) apply (rule_tac x="x \ pia" in exI) apply (rule conjI) apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1]) @@ -569,15 +519,6 @@ apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt) apply (subst permute_eqvt[symmetric]) apply (simp) - apply (rule_tac x="x \ pi" in exI) - apply (rule conjI) - apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1]) - apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt) - apply(rule conjI) - apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1]) - apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt) - apply (subst permute_eqvt[symmetric]) - apply (simp) done lemma alpha5_rfv: @@ -678,10 +619,10 @@ (Lt5 (Lcons y (Vr5 y) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" apply (subst alpha5_INJ) apply (rule conjI) -apply (rule_tac x="0 :: perm" in exI) +apply (rule_tac x="(x \ y)" in exI) apply (simp only: alpha_gen) apply (simp add: permute_trm5_lts fresh_star_def) -apply (rule_tac x="(x \ y)" in exI) +apply (rule_tac x="0 :: perm" in exI) apply (simp only: alpha_gen) apply (simp add: permute_trm5_lts fresh_star_def) done @@ -697,7 +638,7 @@ apply (simp add: alpha5_INJ(5)) apply(clarify) apply (simp add: alpha5_INJ(2)) -apply (simp only: alpha5_INJ(1)) +apply (simp add: alpha5_INJ(1)) done lemma distinct_helper: @@ -1068,7 +1009,7 @@ setup {* snd o define_raw_perms ["tyS"] ["Terms.tyS"] *} print_theorems -local_setup {* define_raw_fv "Terms.ty" [[[[]], [[], []]]] *} +local_setup {* snd o define_fv_alpha "Terms.ty" [[[[]], [[], []]]] *} print_theorems (*