# HG changeset patch # User Cezary Kaliszyk # Date 1266788351 -3600 # Node ID ab942ba2d24341f6acea74bc1af5ad00c30f4ffd # Parent 6d220060358544c54bf948180048880b5fb958b7 Removed bindings 'in itself' where possible. diff -r 6d2200603585 -r ab942ba2d243 Quot/Nominal/Terms.thy --- a/Quot/Nominal/Terms.thy Sat Feb 20 06:31:03 2010 +0100 +++ b/Quot/Nominal/Terms.thy Sun Feb 21 22:39:11 2010 +0100 @@ -41,6 +41,7 @@ alpha_rtrm1 ("_ \1 _" [100, 100] 100) and alpha_bp ("_ \1b _" [100, 100] 100) thm alpha_rtrm1_alpha_bp.intros +thm fv_rtrm1_fv_bp.simps 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 @@ -134,7 +135,7 @@ lemma alpha_rfv1: shows "t \1 s \ fv_rtrm1 t = fv_rtrm1 s" apply(induct rule: alpha_rtrm1_alpha_bp.inducts(1)) - apply(simp_all add: alpha_gen.simps) + apply(simp_all add: alpha_gen.simps alpha_bp_eq) done lemma [quot_respect]: @@ -142,7 +143,7 @@ "(alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rAp1 rAp1" "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) rLm1 rLm1" "(op = ===> alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rLt1 rLt1" -apply (auto simp add: alpha1_inj) +apply (auto simp add: alpha1_inj alpha_bp_eq) apply (rule_tac [!] x="0" in exI) apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1 alpha_bp_eq) done @@ -238,8 +239,9 @@ done lemma supp_fv: - shows "supp t = fv_trm1 t" -apply(induct t rule: trm1_bp_inducts(1)) + "supp t = fv_trm1 t" + "supp b = fv_bp b" +apply(induct t and b rule: trm1_bp_inducts) apply(simp_all) apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) apply(simp only: supp_at_base[simplified supp_def]) @@ -260,6 +262,12 @@ apply(simp add: alpha_gen) apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv) apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper) +apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt) +apply(simp (no_asm) add: supp_def eqvts) +apply(fold supp_def) +apply(simp add: supp_at_base) +apply(simp (no_asm) add: supp_def Collect_imp_eq Collect_neg_eq) +apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric] supp_def[symmetric]) done lemma trm1_supp: @@ -296,7 +304,7 @@ setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *} local_setup {* snd o define_fv_alpha "Terms.rtrm2" - [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv2}, 0)], [(SOME @{term rbv2}, 0)]]], + [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv2}, 0)]]], [[[], []]]] *} notation @@ -353,7 +361,7 @@ setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.assigns"] *} local_setup {* snd o define_fv_alpha "Terms.trm3" - [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv3}, 0)], [(SOME @{term bv3}, 0)]]], + [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]], [[], [[], [], []]]] *} print_theorems @@ -665,7 +673,7 @@ print_theorems local_setup {* snd o define_fv_alpha "Terms.rtrm6" [ - [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv6}, 0)], [(SOME @{term rbv6}, 0)]]]] *} + [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *} notation alpha_rtrm6 ("_ \6 _" [100, 100] 100) (* HERE THE RULES DIFFER *) thm alpha_rtrm6.intros @@ -736,7 +744,6 @@ "(alpha_rtrm6 ===> alpha_rtrm6 ===> alpha_rtrm6) rLt6 rLt6" apply auto apply (simp_all add: alpha6_inj) -apply (rule conjI) apply (rule_tac [!] x="0::perm" in exI) apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm) (* needs rbv6_rsp *) @@ -762,8 +769,7 @@ (fv_trm6 rtrm6 - {atom name}) \* pi \ pi \ rtrm6 = rtrm6a \ P (pi \ rtrm6) rtrm6a\ \ P (Lm6 name rtrm6) (Lm6 namea rtrm6a); \rtrm61 rtrm61a rtrm62 rtrm62a. - \\pi. fv_trm6 rtrm61 - bv6 rtrm61 = fv_trm6 rtrm61a - bv6 rtrm61a \ - (fv_trm6 rtrm61 - bv6 rtrm61) \* pi \ pi \ rtrm61 = rtrm61a \ P (pi \ rtrm61) rtrm61a; + \rtrm61 = rtrm61a; P rtrm61 rtrm61a; \pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \ (fv_trm6 rtrm62 - bv6 rtrm61) \* pi \ pi \ rtrm62 = rtrm62a \ P (pi \ rtrm62) rtrm62a\ \ P (Lt6 rtrm61 rtrm62) (Lt6 rtrm61a rtrm62a)\ @@ -775,8 +781,7 @@ lemma lifted_inject_a3: "(Lt6 rtrm61 rtrm62 = Lt6 rtrm61a rtrm62a) = -((\pi. fv_trm6 rtrm61 - bv6 rtrm61 = fv_trm6 rtrm61a - bv6 rtrm61a \ - (fv_trm6 rtrm61 - bv6 rtrm61) \* pi \ pi \ rtrm61 = rtrm61a) \ +(rtrm61 = rtrm61a \ (\pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \ (fv_trm6 rtrm62 - bv6 rtrm61) \* pi \ pi \ rtrm62 = rtrm62a))" apply(lifting alpha6_inj(3)[unfolded alpha_gen]) @@ -805,7 +810,7 @@ thm permute_rtrm7.simps local_setup {* snd o define_fv_alpha "Terms.rtrm7" [ - [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv7}, 0)], [(SOME @{term rbv7}, 0)]]]] *} + [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv7}, 0)]]]] *} print_theorems notation alpha_rtrm7 ("_ \7a _" [100, 100] 100) @@ -852,7 +857,7 @@ print_theorems local_setup {* snd o define_fv_alpha "Terms.rfoo8" [ - [[[]], [[(SOME @{term rbv8}, 0)], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *} + [[[]], [[], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *} notation alpha_rfoo8 ("_ \f' _" [100, 100] 100) and alpha_rbar8 ("_ \b' _" [100, 100] 100) @@ -888,9 +893,6 @@ apply simp apply clarify apply (erule alpha8f_alpha8b.inducts(1)) apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp) - apply clarify - apply (erule alpha8f_alpha8b.inducts(2)) - apply (simp_all) done @@ -914,7 +916,7 @@ print_theorems local_setup {* snd o define_fv_alpha "Terms.rlam9" [ - [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[(SOME @{term rbv9}, 0)], [(SOME @{term rbv9}, 0)]]]] *} + [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[], [(SOME @{term rbv9}, 0)]]]] *} notation alpha_rlam9 ("_ \9l' _" [100, 100] 100) and alpha_rbla9 ("_ \9b' _" [100, 100] 100)