# HG changeset patch # User Christian Urban # Date 1267097077 -3600 # Node ID 70c2cde06c4ed07a16566bd583d488c0414feaf6 # Parent b0a120469041eaa830c09732c340be2ab466caa5# Parent 1dedc0b76f327d53aa3f7f0d96304c79e94154d3 merged diff -r b0a120469041 -r 70c2cde06c4e Nominal/LFex.thy --- a/Nominal/LFex.thy Thu Feb 25 11:51:34 2010 +0100 +++ b/Nominal/LFex.thy Thu Feb 25 12:24:37 2010 +0100 @@ -51,15 +51,12 @@ apply(induct rule: alpha_rkind_alpha_rty_alpha_rtrm.inducts) apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros) apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj) -apply (rule alpha_gen_atom_eqvt) -apply (simp add: rfv_eqvt) -apply assumption -apply (rule alpha_gen_atom_eqvt) -apply (simp add: rfv_eqvt) -apply assumption -apply (rule alpha_gen_atom_eqvt) -apply (simp add: rfv_eqvt) -apply assumption +apply (erule alpha_gen_compose_eqvt) +apply (simp_all add: rfv_eqvt eqvts atom_eqvt) +apply (erule alpha_gen_compose_eqvt) +apply (simp_all add: rfv_eqvt eqvts atom_eqvt) +apply (erule alpha_gen_compose_eqvt) +apply (simp_all add: rfv_eqvt eqvts atom_eqvt) done local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_equivps}, []), diff -r b0a120469041 -r 70c2cde06c4e Nominal/Terms.thy --- a/Nominal/Terms.thy Thu Feb 25 11:51:34 2010 +0100 +++ b/Nominal/Terms.thy Thu Feb 25 12:24:37 2010 +0100 @@ -1,5 +1,5 @@ theory Terms -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../../Attic/Prove" +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" begin atom_decl name @@ -62,31 +62,83 @@ apply (rule alpha_bp_eq_eq) done -lemma bv1_eqvt[eqvt]: - shows "(pi \ bv1 x) = bv1 (pi \ x)" - apply (induct x) - apply (simp_all add: eqvts atom_eqvt) - done +ML {* +fun build_eqvts bind funs perms simps induct ctxt = +let + val pi = Free ("p", @{typ perm}); + val types = map (domain_type o fastype_of) funs; + val indnames = Name.variant_list ["pi"] (Datatype_Prop.make_tnames (map body_type types)); + val args = map Free (indnames ~~ types); + val perm_at = @{term "permute :: perm \ atom set \ atom set"} + fun eqvtc (fnctn, (arg, perm)) = + HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm $ pi $ arg))) + val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms)))) + fun tac _ = (indtac induct indnames THEN_ALL_NEW + (asm_full_simp_tac (HOL_ss addsimps + (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))) 1 + val thm = Goal.prove ctxt ("p" :: indnames) [] gl tac + val thms = HOLogic.conj_elims thm +in + Local_Theory.note ((bind, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt +end +*} -lemma fv_rtrm1_eqvt[eqvt]: - "(pi\fv_rtrm1 t) = fv_rtrm1 (pi\t)" - "(pi\fv_bp b) = fv_bp (pi\b)" - apply (induct t and b) - apply (simp_all add: eqvts atom_eqvt) - done +local_setup {* +snd o (build_eqvts @{binding bv1_eqvt} [@{term bv1}] [@{term "permute :: perm \ bp \ bp"}] (@{thms bv1.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.inducts(2)}) +*} + +local_setup {* +snd o build_eqvts @{binding fv_rtrm1_fv_bp_eqvt} [@{term fv_rtrm1}, @{term fv_bp}] [@{term "permute :: perm \ rtrm1 \ rtrm1"},@{term "permute :: perm \ bp \ bp"}] (@{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.induct} +*} -lemma alpha1_eqvt: - "t \1 s \ (pi \ t) \1 (pi \ s)" - "alpha_bp a b \ alpha_bp (pi \ a) (pi \ b)" - apply (induct t s and a b rule: alpha_rtrm1_alpha_bp.inducts) - apply (simp_all add:eqvts alpha1_inj) - apply (tactic {* - ALLGOALS ( - TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW - (etac @{thm alpha_gen_compose_eqvt}) - ) *}) - apply (simp_all only: eqvts atom_eqvt) - done +ML {* +fun build_alpha_eqvts funs perms simps induct ctxt = +let + val pi = Free ("p", @{typ perm}); + val types = map (domain_type o fastype_of) funs; + val indnames = Name.variant_list ["pi"] (Datatype_Prop.make_tnames (map body_type types)); + val indnames2 = Name.variant_list ("pi" :: indnames) (Datatype_Prop.make_tnames (map body_type types)); + val args = map Free (indnames ~~ types); + val args2 = map Free (indnames2 ~~ types); + fun eqvtc ((alpha, perm), (arg, arg2)) = + HOLogic.mk_imp (alpha $ arg $ arg2, + (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2))) + val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2)))) + fun tac _ = (rtac induct THEN_ALL_NEW + (asm_full_simp_tac (HOL_ss addsimps + (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))) + THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW + (etac @{thm alpha_gen_compose_eqvt})) THEN_ALL_NEW + (asm_full_simp_tac (HOL_ss addsimps + (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))) +) 1 + val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac +in + map (fn x => mp OF [x]) (HOLogic.conj_elims thm) +end +*} + +local_setup {* +(fn ctxt => snd (Local_Theory.note ((@{binding alpha1_eqvt}, []), + build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}] [@{term "permute :: perm \ rtrm1 \ rtrm1"},@{term "permute :: perm \ bp \ bp"}] @{thms permute_rtrm1_permute_bp.simps alpha1_inj} @{thm alpha_rtrm1_alpha_bp.induct} ctxt) ctxt)) +*} +print_theorems + +lemma alpha1_eqvt_proper[eqvt]: + "pi \ (t \1 s) = ((pi \ t) \1 (pi \ s))" + "pi \ (alpha_bp a b) = (alpha_bp (pi \ a) (pi \ b))" + apply (simp_all only: eqvts) + apply rule + apply (simp_all add: alpha1_eqvt) + apply (subst permute_minus_cancel(2)[symmetric,of "t" "pi"]) + apply (subst permute_minus_cancel(2)[symmetric,of "s" "pi"]) + apply (simp_all only: alpha1_eqvt) + apply rule + apply (simp_all add: alpha1_eqvt) + apply (subst permute_minus_cancel(2)[symmetric,of "a" "pi"]) + apply (subst permute_minus_cancel(2)[symmetric,of "b" "pi"]) + apply (simp_all only: alpha1_eqvt) +done local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []), (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} ctxt)) ctxt)) *} @@ -128,7 +180,7 @@ lemmas permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted] and fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted] -and fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted] +and fv_trm1_eqvt = fv_rtrm1_fv_bp_eqvt(1)[quot_lifted] and alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] lemma supports: @@ -374,11 +426,18 @@ local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *} thm alpha4_inj +thm alpha_rtrm4_alpha_rtrm4_list.induct -lemma alpha4_eqvt: - "t \4 s \ (pi \ t) \4 (pi \ s)" - "a \4l b \ (pi \ a) \4l (pi \ b)" -sorry +local_setup {* +snd o build_eqvts @{binding fv_rtrm4_fv_rtrm4_list_eqvt} [@{term fv_rtrm4}, @{term fv_rtrm4_list}] [@{term "permute :: perm \ rtrm4 \ rtrm4"},@{term "permute :: perm \ rtrm4 list \ rtrm4 list"}] (@{thms fv_rtrm4_fv_rtrm4_list.simps permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]}) @{thm rtrm4.induct} +*} +print_theorems + +local_setup {* +(fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt}, []), + build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] [@{term "permute :: perm \ rtrm4 \ rtrm4"},@{term "permute :: perm \ rtrm4 list \ rtrm4 list"}] @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} ctxt) ctxt)) +*} +print_theorems local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []), (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *}