diff -r 6d140b2c751f -r f7aca5601279 Nominal/Term1.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Term1.thy Thu Feb 25 14:20:40 2010 +0100 @@ -0,0 +1,218 @@ +theory Term1 +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" +begin + +atom_decl name + +section {*** lets with binding patterns ***} + +datatype rtrm1 = + rVr1 "name" +| rAp1 "rtrm1" "rtrm1" +| rLm1 "name" "rtrm1" --"name is bound in trm1" +| rLt1 "bp" "rtrm1" "rtrm1" --"all variables in bp are bound in the 2nd trm1" +and bp = + BUnit +| BVr "name" +| BPr "bp" "bp" + +print_theorems + +(* to be given by the user *) + +primrec + bv1 +where + "bv1 (BUnit) = {}" +| "bv1 (BVr x) = {atom x}" +| "bv1 (BPr bp1 bp2) = (bv1 bp1) \ (bv1 bp2)" + +setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Term1.rtrm1", "Term1.bp"] *} +thm permute_rtrm1_permute_bp.simps + +local_setup {* + snd o define_fv_alpha "Term1.rtrm1" + [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]], + [[], [[]], [[], []]]] *} + +notation + 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 + +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} +*} + + +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)) *} +thm alpha1_equivp + +local_setup {* define_quotient_type [(([], @{binding trm1}, NoSyn), (@{typ rtrm1}, @{term alpha_rtrm1}))] + (rtac @{thm alpha1_equivp(1)} 1) *} + +local_setup {* +(fn ctxt => ctxt + |> snd o (Quotient_Def.quotient_lift_const ("Vr1", @{term rVr1})) + |> snd o (Quotient_Def.quotient_lift_const ("Ap1", @{term rAp1})) + |> snd o (Quotient_Def.quotient_lift_const ("Lm1", @{term rLm1})) + |> snd o (Quotient_Def.quotient_lift_const ("Lt1", @{term rLt1})) + |> snd o (Quotient_Def.quotient_lift_const ("fv_trm1", @{term fv_rtrm1}))) +*} +print_theorems + +thm alpha_rtrm1_alpha_bp.induct +local_setup {* prove_const_rsp @{binding fv_rtrm1_rsp} [@{term fv_rtrm1}] + (fn _ => fvbv_rsp_tac @{thm alpha_rtrm1_alpha_bp.inducts(1)} @{thms fv_rtrm1_fv_bp.simps} 1) *} +local_setup {* prove_const_rsp @{binding rVr1_rsp} [@{term rVr1}] + (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} +local_setup {* prove_const_rsp @{binding rAp1_rsp} [@{term rAp1}] + (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} +local_setup {* prove_const_rsp @{binding rLm1_rsp} [@{term rLm1}] + (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} +local_setup {* prove_const_rsp @{binding rLt1_rsp} [@{term rLt1}] + (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} +local_setup {* prove_const_rsp @{binding permute_rtrm1_rsp} [@{term "permute :: perm \ rtrm1 \ rtrm1"}] + (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}) 1) *} + +lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted] +lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted] + +setup {* define_lifted_perms ["Term1.trm1"] [("permute_trm1", @{term "permute :: perm \ rtrm1 \ rtrm1"})] + @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append} *} + +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_fv_bp_eqvt(1)[quot_lifted] +and alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] + +lemma supports: + "(supp (atom x)) supports (Vr1 x)" + "(supp t \ supp s) supports (Ap1 t s)" + "(supp (atom x) \ supp t) supports (Lm1 x t)" + "(supp b \ supp t \ supp s) supports (Lt1 b t s)" + "{} supports BUnit" + "(supp (atom x)) supports (BVr x)" + "(supp a \ supp b) supports (BPr a b)" +apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh permute_trm1) +apply(rule_tac [!] allI)+ +apply(rule_tac [!] impI) +apply(tactic {* ALLGOALS (REPEAT o etac conjE) *}) +apply(simp_all add: fresh_atom) +done + +lemma rtrm1_bp_fs: + "finite (supp (x :: trm1))" + "finite (supp (b :: bp))" + apply (induct x and b rule: trm1_bp_inducts) + apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *}) + apply(simp_all add: supp_atom) + done + +instance trm1 :: fs +apply default +apply (rule rtrm1_bp_fs(1)) +done + +lemma fv_eq_bv: "fv_bp bp = bv1 bp" +apply(induct bp rule: trm1_bp_inducts(2)) +apply(simp_all) +done + +lemma helper2: "{b. \pi. pi \ (a \ b) \ bp \ bp} = {}" +apply auto +apply (rule_tac x="(x \ a)" in exI) +apply auto +done + +lemma alpha_bp_eq_eq: "alpha_bp a b = (a = b)" +apply rule +apply (induct a b rule: alpha_rtrm1_alpha_bp.inducts(2)) +apply (simp_all add: equivp_reflp[OF alpha1_equivp(2)]) +done + +lemma alpha_bp_eq: "alpha_bp = (op =)" +apply (rule ext)+ +apply (rule alpha_bp_eq_eq) +done + +lemma supp_fv: + "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]) +apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) +apply(simp add: Collect_imp_eq Collect_neg_eq) +apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)") +apply(simp add: supp_Abs fv_trm1) +apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt permute_trm1) +apply(simp add: alpha1_INJ) +apply(simp add: Abs_eq_iff) +apply(simp add: alpha_gen.simps) +apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric]) +apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \ supp (Abs (bv1 bp) rtrm12)") +apply(simp add: supp_Abs fv_trm1 fv_eq_bv) +apply(simp (no_asm) add: supp_def permute_trm1) +apply(simp add: alpha1_INJ alpha_bp_eq) +apply(simp add: Abs_eq_iff) +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 helper2) +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: + "supp (Vr1 x) = {atom x}" + "supp (Ap1 t1 t2) = supp t1 \ supp t2" + "supp (Lm1 x t) = (supp t) - {atom x}" + "supp (Lt1 b t s) = supp t \ (supp s - bv1 b)" +by (simp_all add: supp_fv fv_trm1 fv_eq_bv) + +lemma trm1_induct_strong: + assumes "\name b. P b (Vr1 name)" + and "\rtrm11 rtrm12 b. \\c. P c rtrm11; \c. P c rtrm12\ \ P b (Ap1 rtrm11 rtrm12)" + and "\name rtrm1 b. \\c. P c rtrm1; (atom name) \ b\ \ P b (Lm1 name rtrm1)" + and "\bp rtrm11 rtrm12 b. \\c. P c rtrm11; \c. P c rtrm12; bv1 bp \* b\ \ P b (Lt1 bp rtrm11 rtrm12)" + shows "P a rtrma" +sorry + +end