# HG changeset patch # User Cezary Kaliszyk # Date 1269328773 -3600 # Node ID b679900fa5f6709fce7c39f44e2966d42564af32 # Parent 2f1b00d83925c841db4557c72d4c71818ec79342 Move manual examples to a subdirectory. diff -r 2f1b00d83925 -r b679900fa5f6 Nominal/Manual/Term1.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Manual/Term1.thy Tue Mar 23 08:19:33 2010 +0100 @@ -0,0 +1,261 @@ +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 (Datatype.the_info @{theory} "Term1.rtrm1") 2 *} +thm permute_rtrm1_permute_bp.simps + +local_setup {* + snd o define_fv_alpha (Datatype.the_info @{theory} "Term1.rtrm1") + [[[], [], [(NONE, 0, 1)], [(SOME (@{term bv1}, true), 0, 2)]], + [[], [], []]] [(@{term bv1}, 1, [[], [0], [0, 1]])] *} + +notation + alpha_rtrm1 ("_ \1 _" [100, 100] 100) and + alpha_bp ("_ \1b _" [100, 100] 100) +thm alpha_rtrm1_alpha_bp_alpha_bv1.intros +(*thm fv_rtrm1_fv_bp.simps[no_vars]*) + +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp_alpha_bv1.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases alpha_bv1.cases} ctxt)) ctxt)) *} +thm alpha1_inj + +local_setup {* +snd o (build_eqvts @{binding bv1_eqvt} [@{term bv1}] (build_eqvts_tac @{thm rtrm1_bp.inducts(2)} @{thms bv1.simps permute_rtrm1_permute_bp.simps} @{context})) +*} + +local_setup {* +snd o build_eqvts @{binding fv_rtrm1_fv_bp_eqvt} [@{term fv_rtrm1}, @{term fv_bp}] (build_eqvts_tac @{thm rtrm1_bp.induct} @{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps} @{context}) +*} + +(*local_setup {* +snd o build_eqvts @{binding fv_rtrm1_fv_bv1_eqvt} [@{term fv_rtrm1}, @{term fv_bv1}] (build_eqvts_tac @{thm rtrm1_bp.induct} @{thms fv_rtrm1_fv_bv1.simps permute_rtrm1_permute_bp.simps} @{context}) +*} +print_theorems + +local_setup {* +snd o build_eqvts @{binding fv_bp_eqvt} [@{term fv_bp}] (build_eqvts_tac @{thm rtrm1_bp.inducts(2)} @{thms fv_rtrm1_fv_bv1.simps fv_bp.simps permute_rtrm1_permute_bp.simps} @{context}) +*} +print_theorems +*) + +local_setup {* +(fn ctxt => snd (Local_Theory.note ((@{binding alpha1_eqvt}, []), +build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}, @{term alpha_bv1}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm1_alpha_bp_alpha_bv1.induct} @{thms permute_rtrm1_permute_bp.simps alpha1_inj} ctxt 1) ctxt) ctxt)) *} + +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 +thm eqvts_raw(1) + +lemma "(b \1 a \ a \1 b) \ (x \1b y \ y \1b x) \ (alpha_bv1 x y \ alpha_bv1 y x)" +apply (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp_alpha_bv1.induct} @{thms alpha1_inj} @{thms alpha1_eqvt} @{context} 1 *}) +done + +lemma alpha1_equivp: + "equivp alpha_rtrm1" + "equivp alpha_bp" +sorry + +(* +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []), + (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}, @{term alpha_bv1}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp_alpha_bv1.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 + +local_setup {* snd o prove_const_rsp @{binding fv_rtrm1_rsp} [@{term fv_rtrm1}] + (fn _ => Skip_Proof.cheat_tac @{theory}) *} +local_setup {* snd o 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 {* snd o 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 {* snd o 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 {* snd o prove_const_rsp @{binding rLt1_rsp} [@{term rLt1}] + (fn _ => Skip_Proof.cheat_tac @{theory}) *} +local_setup {* snd o 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[quot_lifted] +and alpha1_INJ = alpha1_inj[unfolded alpha_gen2, unfolded alpha_gen, quot_lifted, folded alpha_gen2, 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(tactic {* ALLGOALS (supports_tac @{thms permute_trm1}) *}) +done + +prove rtrm1_bp_fs: {* snd (mk_fs [@{typ trm1}, @{typ bp}]) *} +apply (tactic {* fs_tac @{thm trm1_bp_induct} @{thms supports} 1 *}) +done + +instance trm1 and bp :: fs +apply default +apply (simp_all add: rtrm1_bp_fs) +done + +lemma fv_eq_bv_pre: "fv_bp bp = bv1 bp" +apply(induct bp rule: trm1_bp_inducts(2)) +apply(simp_all) +done + +lemma fv_eq_bv: "fv_bp = bv1" +apply(rule ext) +apply(rule fv_eq_bv_pre) +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_alpha_bv1.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 ex_out: + "(\x. Z x \ Q) = (Q \ (\x. Z x))" + "(\x. Q \ Z x) = (Q \ (\x. Z x))" + "(\x. P x \ Q \ Z x) = (Q \ (\x. P x \ Z x))" + "(\x. Q \ P x \ Z x) = (Q \ (\x. P x \ Z x))" + "(\x. Q \ P x \ Z x \ W x) = (Q \ (\x. P x \ Z x \ W x))" +apply (blast)+ +done + +lemma Collect_neg_conj: "{x. \(P x \ Q x)} = {x. \(P x)} \ {x. \(Q x)}" +by (simp add: Collect_imp_eq Collect_neg_eq[symmetric]) + +lemma supp_fv_let: + assumes sa : "fv_bp bp = supp bp" + shows "\fv_trm1 ta = supp ta; fv_trm1 tb = supp tb; fv_bp bp = supp bp\ + \ supp (Lt1 bp ta tb) = supp ta \ (supp (bp, tb) - supp bp)" +apply(fold supp_Abs) +apply(simp (no_asm) only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv,symmetric]) +apply(simp (no_asm) only: supp_def) +apply(simp only: permute_set_eq permute_trm1) +apply(simp only: alpha1_INJ alpha_bp_eq) +apply(simp only: ex_out) +apply(simp only: Collect_neg_conj) +apply(simp only: permute_ABS) +apply(simp only: Abs_eq_iff) +apply(simp only: alpha_gen supp_Pair split_conv eqvts) +apply(simp only: infinite_Un) +apply(simp only: Collect_disj_eq) +apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl) +apply (simp only: eqvts[symmetric] fv_trm1_eqvt[symmetric]) +apply (simp only: eqvts Pair_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 Un_commute) +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(simp add: supp_fv_let fv_trm1 fv_eq_bv supp_Pair) +apply blast +apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) +apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) +apply(simp only: supp_at_base[simplified supp_def]) +apply(simp (no_asm) only: supp_def permute_set_eq atom_eqvt permute_trm1 alpha1_INJ[simplified alpha_bp_eq]) +apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric]) +apply(fold supp_def) +apply simp +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 diff -r 2f1b00d83925 -r b679900fa5f6 Nominal/Manual/Term2.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Manual/Term2.thy Tue Mar 23 08:19:33 2010 +0100 @@ -0,0 +1,81 @@ +theory Term2 +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" +begin + +atom_decl name + +section {*** lets with single assignments ***} + +datatype rtrm2 = + rVr2 "name" +| rAp2 "rtrm2" "rtrm2" +| rLm2 "name" "rtrm2" --"bind (name) in (rtrm2)" +| rLt2 "rassign" "rtrm2" --"bind (bv2 rassign) in (rtrm2)" +and rassign = + rAs "name" "rtrm2" + +(* to be given by the user *) +primrec + rbv2 +where + "rbv2 (rAs x t) = {atom x}" + +setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term2.rtrm2") 2 *} + +local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term2.rtrm2") + [[[], + [], + [(NONE, 0, 1)], + [(SOME @{term rbv2}, 0, 1)]], + [[]]] *} + +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_eqvt: + "t \2 s \ (pi \ t) \2 (pi \ s)" + "a \2b b \ (pi \ a) \2b (pi \ b)" +sorry + +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha2_equivp}, []), + (build_equivps [@{term alpha_rtrm2}, @{term alpha_rassign}] @{thm rtrm2_rassign.induct} @{thm alpha_rtrm2_alpha_rassign.induct} @{thms rtrm2.inject rassign.inject} @{thms alpha2_inj} @{thms rtrm2.distinct rassign.distinct} @{thms alpha_rtrm2.cases alpha_rassign.cases} @{thms alpha2_eqvt} ctxt)) ctxt)) *} +thm alpha2_equivp + +local_setup {* define_quotient_type + [(([], @{binding trm2}, NoSyn), (@{typ rtrm2}, @{term alpha_rtrm2})), + (([], @{binding assign}, NoSyn), (@{typ rassign}, @{term alpha_rassign}))] + ((rtac @{thm alpha2_equivp(1)} 1) THEN (rtac @{thm alpha2_equivp(2)}) 1) *} + +local_setup {* +(fn ctxt => ctxt + |> snd o (Quotient_Def.quotient_lift_const ("Vr2", @{term rVr2})) + |> snd o (Quotient_Def.quotient_lift_const ("Ap2", @{term rAp2})) + |> snd o (Quotient_Def.quotient_lift_const ("Lm2", @{term rLm2})) + |> snd o (Quotient_Def.quotient_lift_const ("Lt2", @{term rLt2})) + |> snd o (Quotient_Def.quotient_lift_const ("As", @{term rAs})) + |> snd o (Quotient_Def.quotient_lift_const ("fv_trm2", @{term fv_rtrm2})) + |> snd o (Quotient_Def.quotient_lift_const ("bv2", @{term rbv2}))) +*} +print_theorems + +local_setup {* snd o prove_const_rsp @{binding fv_rtrm2_rsp} [@{term fv_rtrm2}, @{term fv_rassign}] + (fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.induct} @{thms fv_rtrm2_fv_rassign.simps} 1) *} +local_setup {* snd o prove_const_rsp @{binding rbv2_rsp} [@{term rbv2}] + (fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms rbv2.simps} 1) *} +local_setup {* snd o prove_const_rsp @{binding rVr2_rsp} [@{term rVr2}] + (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *} +local_setup {* snd o prove_const_rsp @{binding rAp2_rsp} [@{term rAp2}] + (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *} +local_setup {* snd o prove_const_rsp @{binding rLm2_rsp} [@{term rLm2}] + (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *} +local_setup {* snd o prove_const_rsp @{binding rLt2_rsp} [@{term rLt2}] + (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp rbv2_rsp} @{thms alpha2_equivp} 1) *} +local_setup {* snd o prove_const_rsp @{binding permute_rtrm2_rsp} [@{term "permute :: perm \ rtrm2 \ rtrm2"}] + (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha2_eqvt}) 1) *} + +end diff -r 2f1b00d83925 -r b679900fa5f6 Nominal/Manual/Term3.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Manual/Term3.thy Tue Mar 23 08:19:33 2010 +0100 @@ -0,0 +1,55 @@ +theory Term3 +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" +begin + +atom_decl name + +section {*** lets with many assignments ***} + +datatype rtrm3 = + rVr3 "name" +| rAp3 "rtrm3" "rtrm3" +| rLm3 "name" "rtrm3" --"bind (name) in (trm3)" +| rLt3 "rassigns" "rtrm3" --"bind (bv3 assigns) in (trm3)" +and rassigns = + rANil +| rACons "name" "rtrm3" "rassigns" + +(* to be given by the user *) +primrec + bv3 +where + "bv3 rANil = {}" +| "bv3 (rACons x t as) = {atom x} \ (bv3 as)" + +setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term3.rtrm3") 2 *} + +local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term3.rtrm3") + [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]], + [[], [[], [], []]]] *} +print_theorems + +notation + alpha_rtrm3 ("_ \3 _" [100, 100] 100) and + alpha_rassigns ("_ \3a _" [100, 100] 100) +thm alpha_rtrm3_alpha_rassigns.intros + +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha3_inj}, []), (build_alpha_inj @{thms alpha_rtrm3_alpha_rassigns.intros} @{thms rtrm3.distinct rtrm3.inject rassigns.distinct rassigns.inject} @{thms alpha_rtrm3.cases alpha_rassigns.cases} ctxt)) ctxt)) *} +thm alpha3_inj + +lemma alpha3_eqvt: + "t \3 s \ (pi \ t) \3 (pi \ s)" + "a \3a b \ (pi \ a) \3a (pi \ b)" +sorry + +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha3_equivp}, []), + (build_equivps [@{term alpha_rtrm3}, @{term alpha_rassigns}] @{thm rtrm3_rassigns.induct} @{thm alpha_rtrm3_alpha_rassigns.induct} @{thms rtrm3.inject rassigns.inject} @{thms alpha3_inj} @{thms rtrm3.distinct rassigns.distinct} @{thms alpha_rtrm3.cases alpha_rassigns.cases} @{thms alpha3_eqvt} ctxt)) ctxt)) *} +thm alpha3_equivp + +quotient_type + trm3 = rtrm3 / alpha_rtrm3 +and + assigns = rassigns / alpha_rassigns + by (rule alpha3_equivp(1)) (rule alpha3_equivp(2)) + +end diff -r 2f1b00d83925 -r b679900fa5f6 Nominal/Manual/Term4.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Manual/Term4.thy Tue Mar 23 08:19:33 2010 +0100 @@ -0,0 +1,121 @@ +theory Term4 +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" "Quotient_List" +begin + +atom_decl name + +section {*** lam with indirect list recursion ***} + +datatype rtrm4 = + rVr4 "name" +| rAp4 "rtrm4" "rtrm4 list" +| rLm4 "name" "rtrm4" --"bind (name) in (trm)" +print_theorems + +thm rtrm4.recs + +(* there cannot be a clause for lists, as *) +(* permutations are already defined in Nominal (also functions, options, and so on) *) +setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term4.rtrm4") 1 *} + +(* "repairing" of the permute function *) +lemma repaired: + fixes ts::"rtrm4 list" + shows "permute_rtrm4_list p ts = p \ ts" + apply(induct ts) + apply(simp_all) + done + +thm permute_rtrm4_permute_rtrm4_list.simps +thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] + +local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term4.rtrm4") + [[[], [], [(NONE, 0,1)]], [[], []] ] *} +print_theorems + +lemma fix2: "alpha_rtrm4_list = list_rel alpha_rtrm4" +apply (rule ext)+ +apply (induct_tac x xa rule: list_induct2') +apply (simp_all add: alpha_rtrm4_alpha_rtrm4_list.intros) +apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all) +apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all) +apply rule +apply (erule alpha_rtrm4_list.cases) +apply simp_all +apply (rule alpha_rtrm4_alpha_rtrm4_list.intros) +apply simp_all +done + +(* We need sth like: +lemma fix3: "fv_rtrm4_list = set o map fv_rtrm4" *) + +notation + alpha_rtrm4 ("_ \4 _" [100, 100] 100) and + alpha_rtrm4_list ("_ \4l _" [100, 100] 100) +thm alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2] + +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases[simplified fix2] alpha_rtrm4_list.cases[simplified fix2]} ctxt)) ctxt)) *} +thm alpha4_inj + +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj_no}, []), (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_no + +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_no}, []), + 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_no} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} ctxt) ctxt)) +*} +lemmas alpha4_eqvt = alpha4_eqvt_no[simplified fix2] + +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp_no}, []), + (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_no} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt_no} ctxt)) ctxt)) *} +lemmas alpha4_equivp = alpha4_equivp_no[simplified fix2] + +(*lemma fv_rtrm4_rsp: + "xa \4 ya \ fv_rtrm4 xa = fv_rtrm4 ya" + "x \4l y \ fv_rtrm4_list x = fv_rtrm4_list y" + apply (induct rule: alpha_rtrm4_alpha_rtrm4_list.inducts) + apply (simp_all add: alpha_gen) +done*) + + +quotient_type + trm4 = rtrm4 / alpha_rtrm4 +(*and + trm4list = "rtrm4 list" / alpha_rtrm4_list*) + by (simp_all add: alpha4_equivp) + +local_setup {* +(fn ctxt => ctxt + |> snd o (Quotient_Def.quotient_lift_const ("Vr4", @{term rVr4})) + |> snd o (Quotient_Def.quotient_lift_const ("Ap4", @{term rAp4})) + |> snd o (Quotient_Def.quotient_lift_const ("Lm4", @{term rLm4}))) +*} +print_theorems + +local_setup {* snd o prove_const_rsp @{binding fv_rtrm4_rsp} [@{term fv_rtrm4}] + (fn _ => fvbv_rsp_tac @{thm alpha_rtrm4_alpha_rtrm4_list.inducts(1)} @{thms fv_rtrm4_fv_rtrm4_list.simps} 1) *} +print_theorems + +local_setup {* snd o prove_const_rsp @{binding rVr4_rsp} [@{term rVr4}] + (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp} @{thms alpha4_equivp} 1) *} +lemma "(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4" +apply simp +apply clarify +apply (simp add: alpha4_inj) + + +local_setup {* snd o prove_const_rsp @{binding rLm4_rsp} [@{term rLm4}] + (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp} @{thms alpha4_equivp} 1) *} +local_setup {* snd o prove_const_rsp @{binding permute_rtrm4_rsp} + [@{term "permute :: perm \ rtrm4 \ rtrm4"}, @{term "permute :: perm \ rtrm4 list \ rtrm4 list"}] + (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *} + +thm rtrm4.induct +lemmas trm1_bp_induct = rtrm4.induct[quot_lifted] + +end diff -r 2f1b00d83925 -r b679900fa5f6 Nominal/Manual/Term5.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Manual/Term5.thy Tue Mar 23 08:19:33 2010 +0100 @@ -0,0 +1,344 @@ +theory Term5 +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" +begin + +atom_decl name + +datatype rtrm5 = + rVr5 "name" +| rAp5 "rtrm5" "rtrm5" +| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)" +and rlts = + rLnil +| rLcons "name" "rtrm5" "rlts" + +primrec + rbv5 +where + "rbv5 rLnil = {}" +| "rbv5 (rLcons n t ltl) = {atom n} \ (rbv5 ltl)" + + +setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term5.rtrm5") 2 *} +print_theorems + +local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5") + [[[], [], [(SOME (@{term rbv5}, true), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *} +print_theorems + +notation + alpha_rtrm5 ("_ \5 _" [100, 100] 100) and + alpha_rlts ("_ \l _" [100, 100] 100) +thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros + +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} ctxt)) ctxt)) *} +thm alpha5_inj + +lemma rbv5_eqvt[eqvt]: + "pi \ (rbv5 x) = rbv5 (pi \ x)" + apply (induct x) + apply (simp_all add: eqvts atom_eqvt) + done + +lemma fv_rtrm5_rlts_eqvt[eqvt]: + "pi \ (fv_rtrm5 x) = fv_rtrm5 (pi \ x)" + "pi \ (fv_rlts l) = fv_rlts (pi \ l)" + apply (induct x and l) + apply (simp_all add: eqvts atom_eqvt) + done + +(*lemma alpha5_eqvt: + "(xa \5 y \ (p \ xa) \5 (p \ y)) \ + (xb \l ya \ (p \ xb) \l (p \ ya)) \ + (alpha_rbv5 b c \ alpha_rbv5 (p \ b) (p \ c))" +apply (tactic {* alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} @{context} 1 *}) +done*) + +local_setup {* +(fn ctxt => snd (Local_Theory.note ((@{binding alpha5_eqvt}, []), +build_alpha_eqvts [@{term alpha_rtrm5}, @{term alpha_rlts}, @{term alpha_rbv5}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} ctxt 1) ctxt) ctxt)) *} +print_theorems + +lemma alpha5_reflp: +"y \5 y \ (x \l x \ alpha_rbv5 x x)" +apply (rule rtrm5_rlts.induct) +apply (simp_all add: alpha5_inj) +apply (rule_tac x="0::perm" in exI) +apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm) +done + +lemma alpha5_symp: +"(a \5 b \ b \5 a) \ +(x \l y \ y \l x) \ +(alpha_rbv5 x y \ alpha_rbv5 y x)" +apply (tactic {* symp_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms alpha5_eqvt} @{context} 1 *}) +done + +lemma alpha5_symp1: +"(a \5 b \ b \5 a) \ +(x \l y \ y \l x) \ +(alpha_rbv5 x y \ alpha_rbv5 y x)" +apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) +apply (simp_all add: alpha5_inj) +apply (erule exE) +apply (rule_tac x="- pi" in exI) +apply (simp add: alpha_gen) + apply(simp add: fresh_star_def fresh_minus_perm) +apply clarify +apply (rule conjI) +apply (rotate_tac 3) +apply (frule_tac p="- pi" in alpha5_eqvt(2)) +apply simp +apply (rule conjI) +apply (rotate_tac 5) +apply (frule_tac p="- pi" in alpha5_eqvt(1)) +apply simp +apply (rotate_tac 6) +apply simp +apply (drule_tac p1="- pi" in permute_eq_iff[symmetric,THEN iffD1]) +apply (simp) +done + +thm alpha_gen_sym[no_vars] +thm alpha_gen_compose_sym[no_vars] + +lemma tt: + "\R (- p \ x) y \ R (p \ y) x; (bs, x) \gen R f (- p) (cs, y)\ \ (cs, y) \gen R f p (bs, x)" + unfolding alphas + unfolding fresh_star_def + by (auto simp add: fresh_minus_perm) + +lemma alpha5_symp2: + shows "a \5 b \ b \5 a" + and "x \l y \ y \l x" + and "alpha_rbv5 x y \ alpha_rbv5 y x" +apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) +(* non-binding case *) +apply(simp add: alpha5_inj) +(* non-binding case *) +apply(simp add: alpha5_inj) +(* binding case *) +apply(simp add: alpha5_inj) +apply(erule exE) +apply(rule_tac x="- pi" in exI) +apply(rule tt) +apply(simp add: alphas) +apply(erule conjE)+ +apply(drule_tac p="- pi" in alpha5_eqvt(2)) +apply(drule_tac p="- pi" in alpha5_eqvt(2)) +apply(drule_tac p="- pi" in alpha5_eqvt(1)) +apply(drule_tac p="- pi" in alpha5_eqvt(1)) +apply(simp) +apply(simp add: alphas) +apply(erule conjE)+ +apply metis +(* non-binding case *) +apply(simp add: alpha5_inj) +(* non-binding case *) +apply(simp add: alpha5_inj) +(* non-binding case *) +apply(simp add: alpha5_inj) +(* non-binding case *) +apply(simp add: alpha5_inj) +done + +lemma alpha5_transp: +"(a \5 b \ (\c. b \5 c \ a \5 c)) \ +(x \l y \ (\z. y \l z \ x \l z)) \ +(alpha_rbv5 k l \ (\m. alpha_rbv5 l m \ alpha_rbv5 k m))" +(*apply (tactic {* transp_tac @{context} @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} [] @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{thms alpha5_eqvt} 1 *})*) +apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) +apply (rule_tac [!] allI) +apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) +apply (simp_all add: alpha5_inj) +apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) +apply (simp_all add: alpha5_inj) +apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) +apply (simp_all add: alpha5_inj) +defer +apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) +apply (simp_all add: alpha5_inj) +apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) +apply (simp_all add: alpha5_inj) +apply (tactic {* eetac @{thm exi_sum} @{context} 1 *}) +(* HERE *) +(* +apply(rule alpha_gen_trans) +thm alpha_gen_trans +defer +apply (simp add: alpha_gen) +apply clarify +apply(simp add: fresh_star_plus) +apply (rule conjI) +apply (erule_tac x="- pi \ rltsaa" in allE) +apply (rotate_tac 5) +apply (drule_tac p="- pi" in alpha5_eqvt(2)) +apply simp +apply (drule_tac p="pi" in alpha5_eqvt(2)) +apply simp +apply (erule_tac x="- pi \ rtrm5aa" in allE) +apply (rotate_tac 7) +apply (drule_tac p="- pi" in alpha5_eqvt(1)) +apply simp +apply (rotate_tac 3) +apply (drule_tac p="pi" in alpha5_eqvt(1)) +apply simp +done +*) +sorry + +lemma alpha5_equivp: + "equivp alpha_rtrm5" + "equivp alpha_rlts" + unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def + apply (simp_all only: alpha5_reflp) + apply (meson alpha5_symp alpha5_transp) + apply (meson alpha5_symp alpha5_transp) + done + +quotient_type + trm5 = rtrm5 / alpha_rtrm5 +and + lts = rlts / alpha_rlts + by (auto intro: alpha5_equivp) + +local_setup {* +(fn ctxt => ctxt + |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5})) + |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5})) + |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5})) + |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil})) + |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons})) + |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5})) + |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts})) + |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5})) + |> snd o (Quotient_Def.quotient_lift_const ("alpha_bv5", @{term alpha_rbv5}))) +*} +print_theorems + +lemma alpha5_rfv: + "(t \5 s \ fv_rtrm5 t = fv_rtrm5 s)" + "(l \l m \ fv_rlts l = fv_rlts m)" + "(alpha_rbv5 b c \ True)" + apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) + apply(simp_all add: eqvts) + apply(simp add: alpha_gen) + apply(clarify) + apply blast +done + +lemma bv_list_rsp: + shows "x \l y \ rbv5 x = rbv5 y" + apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) + apply(simp_all) + apply(clarify) + apply simp + done + +local_setup {* snd o Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel @{context} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases}) [(@{thms rtrm5.distinct}, @{term alpha_rtrm5}), (@{thms rlts.distinct}, @{term alpha_rlts}), (@{thms rlts.distinct}, @{term alpha_rbv5})]))) *} +print_theorems + +local_setup {* snd o Local_Theory.note ((@{binding alpha_bn_rsp}, []), prove_alpha_bn_rsp [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts} @{thms rtrm5.exhaust rlts.exhaust} @{thms alpha5_inj alpha_dis} @{thms alpha5_equivp} @{context} (@{term alpha_rbv5}, 1)) *} +thm alpha_bn_rsp + +lemma [quot_respect]: + "(alpha_rlts ===> op =) fv_rlts fv_rlts" + "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5" + "(alpha_rlts ===> op =) rbv5 rbv5" + "(op = ===> alpha_rtrm5) rVr5 rVr5" + "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5" + "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" + "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" + "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" + "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" + "(alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5" + apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha_bn_rsp) + apply (clarify) + apply (rule_tac x="0" in exI) + apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) +done + + +lemma + shows "(alpha_rlts ===> op =) rbv5 rbv5" + by (simp add: bv_list_rsp) + +lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted] + +instantiation trm5 and lts :: pt +begin + +quotient_definition + "permute_trm5 :: perm \ trm5 \ trm5" +is + "permute :: perm \ rtrm5 \ rtrm5" + +quotient_definition + "permute_lts :: perm \ lts \ lts" +is + "permute :: perm \ rlts \ rlts" + +instance by default + (simp_all add: permute_rtrm5_permute_rlts_zero[quot_lifted] permute_rtrm5_permute_rlts_append[quot_lifted]) + +end + +lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] +lemmas bv5[simp] = rbv5.simps[quot_lifted] +lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] +lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen2, unfolded alpha_gen, quot_lifted, folded alpha_gen2, folded alpha_gen] +lemmas alpha5_DIS = alpha_dis[quot_lifted] + +(* why is this not in Isabelle? *) +lemma set_sub: "{a, b} - {b} = {a} - {b}" +by auto + +lemma lets_bla: + "x \ z \ y \ z \ x \ y \(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) \ (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))" +apply (simp only: alpha5_INJ bv5) +apply simp +apply (rule allI) +apply (simp_all add: alpha_gen) +apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ eqvts) +apply (rule impI) +apply (rule impI) +apply (rule impI) +apply (simp add: set_sub) +done + +lemma lets_ok: + "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" +thm alpha5_INJ +apply (simp only: alpha5_INJ) +apply (rule_tac x="(x \ y)" in exI) +apply (simp_all add: alpha_gen) +apply (simp add: permute_trm5_lts fresh_star_def) +apply (simp add: eqvts) +done + +lemma lets_ok3: + "x \ y \ + (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \ + (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" +apply (simp add: permute_trm5_lts alpha_gen alpha5_INJ) +done + + +lemma lets_not_ok1: + "x \ y \ + (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \ + (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" +apply (simp add: alpha5_INJ alpha_gen) +apply (simp add: permute_trm5_lts eqvts) +apply (simp add: alpha5_INJ) +done + +lemma lets_nok: + "x \ y \ x \ z \ z \ y \ + (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \ + (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" +apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def) +apply (simp add: alpha5_DIS alpha5_INJ permute_trm5_lts) +done + +end diff -r 2f1b00d83925 -r b679900fa5f6 Nominal/Manual/Term5n.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Manual/Term5n.thy Tue Mar 23 08:19:33 2010 +0100 @@ -0,0 +1,228 @@ +theory Term5 +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" +begin + +atom_decl name + +datatype rtrm5 = + rVr5 "name" +| rAp5 "rtrm5" "rtrm5" +| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)" +and rlts = + rLnil +| rLcons "name" "rtrm5" "rlts" + +primrec + rbv5 +where + "rbv5 rLnil = {}" +| "rbv5 (rLcons n t ltl) = {atom n} \ (rbv5 ltl)" + + +setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term5.rtrm5") 2 *} +print_theorems + +local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5") + [[[], [], [(SOME (@{term rbv5}, false), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *} +print_theorems + +notation + alpha_rtrm5 ("_ \5 _" [100, 100] 100) and + alpha_rlts ("_ \l _" [100, 100] 100) +thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros + +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} ctxt)) ctxt)) *} +thm alpha5_inj + +lemma rbv5_eqvt[eqvt]: + "pi \ (rbv5 x) = rbv5 (pi \ x)" + apply (induct x) + apply (simp_all add: eqvts atom_eqvt) + done + +lemma fv_rtrm5_rlts_eqvt[eqvt]: + "pi \ (fv_rtrm5 x) = fv_rtrm5 (pi \ x)" + "pi \ (fv_rlts l) = fv_rlts (pi \ l)" + "pi \ (fv_rbv5 l) = fv_rbv5 (pi \ l)" + apply (induct x and l) + apply (simp_all add: eqvts atom_eqvt) + done + +local_setup {* +(fn ctxt => snd (Local_Theory.note ((@{binding alpha5_eqvt}, []), +build_alpha_eqvts [@{term alpha_rtrm5}, @{term alpha_rlts}, @{term alpha_rbv5}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} ctxt 1) ctxt) ctxt)) *} +print_theorems + +lemma alpha5_reflp: +"y \5 y \ (x \l x \ alpha_rbv5 x x)" +apply (rule rtrm5_rlts.induct) +apply (simp_all add: alpha5_inj) +apply (rule_tac x="0::perm" in exI) +apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm) +done + +lemma alpha5_symp: +"(a \5 b \ b \5 a) \ +(x \l y \ y \l x) \ +(alpha_rbv5 x y \ alpha_rbv5 y x)" +sorry + +lemma alpha5_transp: +"(a \5 b \ (\c. b \5 c \ a \5 c)) \ +(x \l y \ (\z. y \l z \ x \l z)) \ +(alpha_rbv5 k l \ (\m. alpha_rbv5 l m \ alpha_rbv5 k m))" +sorry + +lemma alpha5_equivp: + "equivp alpha_rtrm5" + "equivp alpha_rlts" + unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def + apply (simp_all only: alpha5_reflp) + apply (meson alpha5_symp alpha5_transp) + apply (meson alpha5_symp alpha5_transp) + done + +quotient_type + trm5 = rtrm5 / alpha_rtrm5 +and + lts = rlts / alpha_rlts + by (auto intro: alpha5_equivp) + +local_setup {* +(fn ctxt => ctxt + |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5})) + |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5})) + |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5})) + |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil})) + |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons})) + |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5})) + |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts})) + |> snd o (Quotient_Def.quotient_lift_const ("fv_bv5", @{term fv_rbv5})) + |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5})) + |> snd o (Quotient_Def.quotient_lift_const ("alpha_bv5", @{term alpha_rbv5}))) +*} +print_theorems + +lemma alpha5_rfv: + "(t \5 s \ fv_rtrm5 t = fv_rtrm5 s)" + "(l \l m \ (fv_rlts l = fv_rlts m \ fv_rbv5 l = fv_rbv5 m))" + "(alpha_rbv5 b c \ fv_rbv5 b = fv_rbv5 c)" + apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) + apply(simp_all) + apply(simp add: alpha_gen) + done + +lemma bv_list_rsp: + shows "x \l y \ rbv5 x = rbv5 y" + apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) + apply(simp_all) + apply(clarify) + apply simp + done + +local_setup {* snd o Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel @{context} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases}) [(@{thms rtrm5.distinct}, @{term alpha_rtrm5}), (@{thms rlts.distinct}, @{term alpha_rlts}), (@{thms rlts.distinct}, @{term alpha_rbv5})]))) *} +print_theorems + +local_setup {* snd o Local_Theory.note ((@{binding alpha_bn_rsp}, []), prove_alpha_bn_rsp [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts} @{thms alpha5_inj alpha_dis} @{thms alpha5_equivp} @{context} (@{term alpha_rbv5}, 1)) *} +thm alpha_bn_rsp + + +lemma [quot_respect]: + "(alpha_rlts ===> op =) fv_rlts fv_rlts" + "(alpha_rlts ===> op =) fv_rbv5 fv_rbv5" + "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5" + "(alpha_rlts ===> op =) rbv5 rbv5" + "(op = ===> alpha_rtrm5) rVr5 rVr5" + "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5" + "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" + "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" + "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" + "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" + "(alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5" + apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha5_reflp alpha_bn_rsp) + apply (clarify) + apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) +done + +lemma + shows "(alpha_rlts ===> op =) rbv5 rbv5" + by (simp add: bv_list_rsp) + +lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted] + +instantiation trm5 and lts :: pt +begin + +quotient_definition + "permute_trm5 :: perm \ trm5 \ trm5" +is + "permute :: perm \ rtrm5 \ rtrm5" + +quotient_definition + "permute_lts :: perm \ lts \ lts" +is + "permute :: perm \ rlts \ rlts" + +instance by default + (simp_all add: permute_rtrm5_permute_rlts_zero[quot_lifted] permute_rtrm5_permute_rlts_append[quot_lifted]) + +end + +lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] +lemmas bv5[simp] = rbv5.simps[quot_lifted] +lemmas fv_trm5_bv5[simp] = fv_rtrm5_fv_rbv5.simps[quot_lifted] +lemmas fv_lts[simp] = fv_rlts.simps[quot_lifted] +lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] + +lemma lets_bla: + "x \ z \ y \ z \ x \ y \(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) \ (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))" +apply (simp only: alpha5_INJ) +apply (simp only: bv5) +apply simp +done + +lemma lets_ok: + "(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" +apply (simp add: alpha5_INJ) +apply (rule_tac x="(x \ y)" in exI) +apply (simp_all add: alpha_gen) +apply (simp add: permute_trm5_lts fresh_star_def eqvts) +done + +lemma lets_ok3: + "x \ y \ + (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \ + (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" +apply (simp add: permute_trm5_lts alpha_gen alpha5_INJ) +done + + +lemma lets_not_ok1: + "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = + (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" +apply (simp add: alpha5_INJ alpha_gen) +apply (rule_tac x="0::perm" in exI) +apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1) eqvts) +apply blast +done + +lemma distinct_helper: + shows "\(rVr5 x \5 rAp5 y z)" + apply auto + apply (erule alpha_rtrm5.cases) + apply (simp_all only: rtrm5.distinct) + done + +lemma distinct_helper2: + shows "(Vr5 x) \ (Ap5 y z)" + by (lifting distinct_helper) + +lemma lets_nok: + "x \ y \ x \ z \ z \ y \ + (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \ + (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" +apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def) +apply (simp add: distinct_helper2 alpha5_INJ permute_trm5_lts) +done + +end diff -r 2f1b00d83925 -r b679900fa5f6 Nominal/Manual/Term8.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Manual/Term8.thy Tue Mar 23 08:19:33 2010 +0100 @@ -0,0 +1,61 @@ +theory Term8 +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" +begin + +atom_decl name + +datatype rfoo8 = + Foo0 "name" +| Foo1 "rbar8" "rfoo8" --"bind bv(bar) in foo" +and rbar8 = + Bar0 "name" +| Bar1 "name" "name" "rbar8" --"bind second name in b" + +primrec + rbv8 +where + "rbv8 (Bar0 x) = {}" +| "rbv8 (Bar1 v x b) = {atom v}" + +setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term8.rfoo8") 2 *} +print_theorems + +local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term8.rfoo8") [ + [[[]], [[], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *} +notation + alpha_rfoo8 ("_ \f' _" [100, 100] 100) and + alpha_rbar8 ("_ \b' _" [100, 100] 100) +thm alpha_rfoo8_alpha_rbar8.intros + + +inductive + alpha8f :: "rfoo8 \ rfoo8 \ bool" ("_ \f _" [100, 100] 100) +and + alpha8b :: "rbar8 \ rbar8 \ bool" ("_ \b _" [100, 100] 100) +where + a1: "a = b \ (Foo0 a) \f (Foo0 b)" +| a2: "a = b \ (Bar0 a) \b (Bar0 b)" +| a3: "b1 \b b2 \ (\pi. (((rbv8 b1), t1) \gen alpha8f fv_rfoo8 pi ((rbv8 b2), t2))) \ Foo1 b1 t1 \f Foo1 b2 t2" +| a4: "v1 = v2 \ (\pi. (({atom x1}, t1) \gen alpha8b fv_rbar8 pi ({atom x2}, t2))) \ Bar1 v1 x1 t1 \b Bar1 v2 x2 t2" + +lemma "(alpha8b ===> op =) rbv8 rbv8" + apply simp apply clarify + apply (erule alpha8f_alpha8b.inducts(2)) + apply (simp_all) +done + +lemma fv_rbar8_rsp_hlp: "x \b y \ fv_rbar8 x = fv_rbar8 y" + apply (erule alpha8f_alpha8b.inducts(2)) + apply (simp_all add: alpha_gen) +done +lemma "(alpha8b ===> op =) fv_rbar8 fv_rbar8" + apply simp apply clarify apply (simp add: fv_rbar8_rsp_hlp) +done + +lemma "(alpha8f ===> op =) fv_rfoo8 fv_rfoo8" + apply simp apply clarify + apply (erule alpha8f_alpha8b.inducts(1)) + apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp) +done + +end diff -r 2f1b00d83925 -r b679900fa5f6 Nominal/Term1.thy --- a/Nominal/Term1.thy Tue Mar 23 08:16:39 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,261 +0,0 @@ -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 (Datatype.the_info @{theory} "Term1.rtrm1") 2 *} -thm permute_rtrm1_permute_bp.simps - -local_setup {* - snd o define_fv_alpha (Datatype.the_info @{theory} "Term1.rtrm1") - [[[], [], [(NONE, 0, 1)], [(SOME (@{term bv1}, true), 0, 2)]], - [[], [], []]] [(@{term bv1}, 1, [[], [0], [0, 1]])] *} - -notation - alpha_rtrm1 ("_ \1 _" [100, 100] 100) and - alpha_bp ("_ \1b _" [100, 100] 100) -thm alpha_rtrm1_alpha_bp_alpha_bv1.intros -(*thm fv_rtrm1_fv_bp.simps[no_vars]*) - -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp_alpha_bv1.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases alpha_bv1.cases} ctxt)) ctxt)) *} -thm alpha1_inj - -local_setup {* -snd o (build_eqvts @{binding bv1_eqvt} [@{term bv1}] (build_eqvts_tac @{thm rtrm1_bp.inducts(2)} @{thms bv1.simps permute_rtrm1_permute_bp.simps} @{context})) -*} - -local_setup {* -snd o build_eqvts @{binding fv_rtrm1_fv_bp_eqvt} [@{term fv_rtrm1}, @{term fv_bp}] (build_eqvts_tac @{thm rtrm1_bp.induct} @{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps} @{context}) -*} - -(*local_setup {* -snd o build_eqvts @{binding fv_rtrm1_fv_bv1_eqvt} [@{term fv_rtrm1}, @{term fv_bv1}] (build_eqvts_tac @{thm rtrm1_bp.induct} @{thms fv_rtrm1_fv_bv1.simps permute_rtrm1_permute_bp.simps} @{context}) -*} -print_theorems - -local_setup {* -snd o build_eqvts @{binding fv_bp_eqvt} [@{term fv_bp}] (build_eqvts_tac @{thm rtrm1_bp.inducts(2)} @{thms fv_rtrm1_fv_bv1.simps fv_bp.simps permute_rtrm1_permute_bp.simps} @{context}) -*} -print_theorems -*) - -local_setup {* -(fn ctxt => snd (Local_Theory.note ((@{binding alpha1_eqvt}, []), -build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}, @{term alpha_bv1}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm1_alpha_bp_alpha_bv1.induct} @{thms permute_rtrm1_permute_bp.simps alpha1_inj} ctxt 1) ctxt) ctxt)) *} - -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 -thm eqvts_raw(1) - -lemma "(b \1 a \ a \1 b) \ (x \1b y \ y \1b x) \ (alpha_bv1 x y \ alpha_bv1 y x)" -apply (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp_alpha_bv1.induct} @{thms alpha1_inj} @{thms alpha1_eqvt} @{context} 1 *}) -done - -lemma alpha1_equivp: - "equivp alpha_rtrm1" - "equivp alpha_bp" -sorry - -(* -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []), - (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}, @{term alpha_bv1}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp_alpha_bv1.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 - -local_setup {* snd o prove_const_rsp @{binding fv_rtrm1_rsp} [@{term fv_rtrm1}] - (fn _ => Skip_Proof.cheat_tac @{theory}) *} -local_setup {* snd o 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 {* snd o 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 {* snd o 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 {* snd o prove_const_rsp @{binding rLt1_rsp} [@{term rLt1}] - (fn _ => Skip_Proof.cheat_tac @{theory}) *} -local_setup {* snd o 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[quot_lifted] -and alpha1_INJ = alpha1_inj[unfolded alpha_gen2, unfolded alpha_gen, quot_lifted, folded alpha_gen2, 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(tactic {* ALLGOALS (supports_tac @{thms permute_trm1}) *}) -done - -prove rtrm1_bp_fs: {* snd (mk_fs [@{typ trm1}, @{typ bp}]) *} -apply (tactic {* fs_tac @{thm trm1_bp_induct} @{thms supports} 1 *}) -done - -instance trm1 and bp :: fs -apply default -apply (simp_all add: rtrm1_bp_fs) -done - -lemma fv_eq_bv_pre: "fv_bp bp = bv1 bp" -apply(induct bp rule: trm1_bp_inducts(2)) -apply(simp_all) -done - -lemma fv_eq_bv: "fv_bp = bv1" -apply(rule ext) -apply(rule fv_eq_bv_pre) -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_alpha_bv1.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 ex_out: - "(\x. Z x \ Q) = (Q \ (\x. Z x))" - "(\x. Q \ Z x) = (Q \ (\x. Z x))" - "(\x. P x \ Q \ Z x) = (Q \ (\x. P x \ Z x))" - "(\x. Q \ P x \ Z x) = (Q \ (\x. P x \ Z x))" - "(\x. Q \ P x \ Z x \ W x) = (Q \ (\x. P x \ Z x \ W x))" -apply (blast)+ -done - -lemma Collect_neg_conj: "{x. \(P x \ Q x)} = {x. \(P x)} \ {x. \(Q x)}" -by (simp add: Collect_imp_eq Collect_neg_eq[symmetric]) - -lemma supp_fv_let: - assumes sa : "fv_bp bp = supp bp" - shows "\fv_trm1 ta = supp ta; fv_trm1 tb = supp tb; fv_bp bp = supp bp\ - \ supp (Lt1 bp ta tb) = supp ta \ (supp (bp, tb) - supp bp)" -apply(fold supp_Abs) -apply(simp (no_asm) only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv,symmetric]) -apply(simp (no_asm) only: supp_def) -apply(simp only: permute_set_eq permute_trm1) -apply(simp only: alpha1_INJ alpha_bp_eq) -apply(simp only: ex_out) -apply(simp only: Collect_neg_conj) -apply(simp only: permute_ABS) -apply(simp only: Abs_eq_iff) -apply(simp only: alpha_gen supp_Pair split_conv eqvts) -apply(simp only: infinite_Un) -apply(simp only: Collect_disj_eq) -apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl) -apply (simp only: eqvts[symmetric] fv_trm1_eqvt[symmetric]) -apply (simp only: eqvts Pair_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 Un_commute) -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(simp add: supp_fv_let fv_trm1 fv_eq_bv supp_Pair) -apply blast -apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) -apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) -apply(simp only: supp_at_base[simplified supp_def]) -apply(simp (no_asm) only: supp_def permute_set_eq atom_eqvt permute_trm1 alpha1_INJ[simplified alpha_bp_eq]) -apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric]) -apply(fold supp_def) -apply simp -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 diff -r 2f1b00d83925 -r b679900fa5f6 Nominal/Term2.thy --- a/Nominal/Term2.thy Tue Mar 23 08:16:39 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,81 +0,0 @@ -theory Term2 -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" -begin - -atom_decl name - -section {*** lets with single assignments ***} - -datatype rtrm2 = - rVr2 "name" -| rAp2 "rtrm2" "rtrm2" -| rLm2 "name" "rtrm2" --"bind (name) in (rtrm2)" -| rLt2 "rassign" "rtrm2" --"bind (bv2 rassign) in (rtrm2)" -and rassign = - rAs "name" "rtrm2" - -(* to be given by the user *) -primrec - rbv2 -where - "rbv2 (rAs x t) = {atom x}" - -setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term2.rtrm2") 2 *} - -local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term2.rtrm2") - [[[], - [], - [(NONE, 0, 1)], - [(SOME @{term rbv2}, 0, 1)]], - [[]]] *} - -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_eqvt: - "t \2 s \ (pi \ t) \2 (pi \ s)" - "a \2b b \ (pi \ a) \2b (pi \ b)" -sorry - -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha2_equivp}, []), - (build_equivps [@{term alpha_rtrm2}, @{term alpha_rassign}] @{thm rtrm2_rassign.induct} @{thm alpha_rtrm2_alpha_rassign.induct} @{thms rtrm2.inject rassign.inject} @{thms alpha2_inj} @{thms rtrm2.distinct rassign.distinct} @{thms alpha_rtrm2.cases alpha_rassign.cases} @{thms alpha2_eqvt} ctxt)) ctxt)) *} -thm alpha2_equivp - -local_setup {* define_quotient_type - [(([], @{binding trm2}, NoSyn), (@{typ rtrm2}, @{term alpha_rtrm2})), - (([], @{binding assign}, NoSyn), (@{typ rassign}, @{term alpha_rassign}))] - ((rtac @{thm alpha2_equivp(1)} 1) THEN (rtac @{thm alpha2_equivp(2)}) 1) *} - -local_setup {* -(fn ctxt => ctxt - |> snd o (Quotient_Def.quotient_lift_const ("Vr2", @{term rVr2})) - |> snd o (Quotient_Def.quotient_lift_const ("Ap2", @{term rAp2})) - |> snd o (Quotient_Def.quotient_lift_const ("Lm2", @{term rLm2})) - |> snd o (Quotient_Def.quotient_lift_const ("Lt2", @{term rLt2})) - |> snd o (Quotient_Def.quotient_lift_const ("As", @{term rAs})) - |> snd o (Quotient_Def.quotient_lift_const ("fv_trm2", @{term fv_rtrm2})) - |> snd o (Quotient_Def.quotient_lift_const ("bv2", @{term rbv2}))) -*} -print_theorems - -local_setup {* snd o prove_const_rsp @{binding fv_rtrm2_rsp} [@{term fv_rtrm2}, @{term fv_rassign}] - (fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.induct} @{thms fv_rtrm2_fv_rassign.simps} 1) *} -local_setup {* snd o prove_const_rsp @{binding rbv2_rsp} [@{term rbv2}] - (fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms rbv2.simps} 1) *} -local_setup {* snd o prove_const_rsp @{binding rVr2_rsp} [@{term rVr2}] - (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *} -local_setup {* snd o prove_const_rsp @{binding rAp2_rsp} [@{term rAp2}] - (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *} -local_setup {* snd o prove_const_rsp @{binding rLm2_rsp} [@{term rLm2}] - (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *} -local_setup {* snd o prove_const_rsp @{binding rLt2_rsp} [@{term rLt2}] - (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp rbv2_rsp} @{thms alpha2_equivp} 1) *} -local_setup {* snd o prove_const_rsp @{binding permute_rtrm2_rsp} [@{term "permute :: perm \ rtrm2 \ rtrm2"}] - (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha2_eqvt}) 1) *} - -end diff -r 2f1b00d83925 -r b679900fa5f6 Nominal/Term3.thy --- a/Nominal/Term3.thy Tue Mar 23 08:16:39 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,55 +0,0 @@ -theory Term3 -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" -begin - -atom_decl name - -section {*** lets with many assignments ***} - -datatype rtrm3 = - rVr3 "name" -| rAp3 "rtrm3" "rtrm3" -| rLm3 "name" "rtrm3" --"bind (name) in (trm3)" -| rLt3 "rassigns" "rtrm3" --"bind (bv3 assigns) in (trm3)" -and rassigns = - rANil -| rACons "name" "rtrm3" "rassigns" - -(* to be given by the user *) -primrec - bv3 -where - "bv3 rANil = {}" -| "bv3 (rACons x t as) = {atom x} \ (bv3 as)" - -setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term3.rtrm3") 2 *} - -local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term3.rtrm3") - [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]], - [[], [[], [], []]]] *} -print_theorems - -notation - alpha_rtrm3 ("_ \3 _" [100, 100] 100) and - alpha_rassigns ("_ \3a _" [100, 100] 100) -thm alpha_rtrm3_alpha_rassigns.intros - -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha3_inj}, []), (build_alpha_inj @{thms alpha_rtrm3_alpha_rassigns.intros} @{thms rtrm3.distinct rtrm3.inject rassigns.distinct rassigns.inject} @{thms alpha_rtrm3.cases alpha_rassigns.cases} ctxt)) ctxt)) *} -thm alpha3_inj - -lemma alpha3_eqvt: - "t \3 s \ (pi \ t) \3 (pi \ s)" - "a \3a b \ (pi \ a) \3a (pi \ b)" -sorry - -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha3_equivp}, []), - (build_equivps [@{term alpha_rtrm3}, @{term alpha_rassigns}] @{thm rtrm3_rassigns.induct} @{thm alpha_rtrm3_alpha_rassigns.induct} @{thms rtrm3.inject rassigns.inject} @{thms alpha3_inj} @{thms rtrm3.distinct rassigns.distinct} @{thms alpha_rtrm3.cases alpha_rassigns.cases} @{thms alpha3_eqvt} ctxt)) ctxt)) *} -thm alpha3_equivp - -quotient_type - trm3 = rtrm3 / alpha_rtrm3 -and - assigns = rassigns / alpha_rassigns - by (rule alpha3_equivp(1)) (rule alpha3_equivp(2)) - -end diff -r 2f1b00d83925 -r b679900fa5f6 Nominal/Term4.thy --- a/Nominal/Term4.thy Tue Mar 23 08:16:39 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,121 +0,0 @@ -theory Term4 -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" "Quotient_List" -begin - -atom_decl name - -section {*** lam with indirect list recursion ***} - -datatype rtrm4 = - rVr4 "name" -| rAp4 "rtrm4" "rtrm4 list" -| rLm4 "name" "rtrm4" --"bind (name) in (trm)" -print_theorems - -thm rtrm4.recs - -(* there cannot be a clause for lists, as *) -(* permutations are already defined in Nominal (also functions, options, and so on) *) -setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term4.rtrm4") 1 *} - -(* "repairing" of the permute function *) -lemma repaired: - fixes ts::"rtrm4 list" - shows "permute_rtrm4_list p ts = p \ ts" - apply(induct ts) - apply(simp_all) - done - -thm permute_rtrm4_permute_rtrm4_list.simps -thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] - -local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term4.rtrm4") - [[[], [], [(NONE, 0,1)]], [[], []] ] *} -print_theorems - -lemma fix2: "alpha_rtrm4_list = list_rel alpha_rtrm4" -apply (rule ext)+ -apply (induct_tac x xa rule: list_induct2') -apply (simp_all add: alpha_rtrm4_alpha_rtrm4_list.intros) -apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all) -apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all) -apply rule -apply (erule alpha_rtrm4_list.cases) -apply simp_all -apply (rule alpha_rtrm4_alpha_rtrm4_list.intros) -apply simp_all -done - -(* We need sth like: -lemma fix3: "fv_rtrm4_list = set o map fv_rtrm4" *) - -notation - alpha_rtrm4 ("_ \4 _" [100, 100] 100) and - alpha_rtrm4_list ("_ \4l _" [100, 100] 100) -thm alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2] - -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases[simplified fix2] alpha_rtrm4_list.cases[simplified fix2]} ctxt)) ctxt)) *} -thm alpha4_inj - -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj_no}, []), (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_no - -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_no}, []), - 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_no} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} ctxt) ctxt)) -*} -lemmas alpha4_eqvt = alpha4_eqvt_no[simplified fix2] - -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp_no}, []), - (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_no} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt_no} ctxt)) ctxt)) *} -lemmas alpha4_equivp = alpha4_equivp_no[simplified fix2] - -(*lemma fv_rtrm4_rsp: - "xa \4 ya \ fv_rtrm4 xa = fv_rtrm4 ya" - "x \4l y \ fv_rtrm4_list x = fv_rtrm4_list y" - apply (induct rule: alpha_rtrm4_alpha_rtrm4_list.inducts) - apply (simp_all add: alpha_gen) -done*) - - -quotient_type - trm4 = rtrm4 / alpha_rtrm4 -(*and - trm4list = "rtrm4 list" / alpha_rtrm4_list*) - by (simp_all add: alpha4_equivp) - -local_setup {* -(fn ctxt => ctxt - |> snd o (Quotient_Def.quotient_lift_const ("Vr4", @{term rVr4})) - |> snd o (Quotient_Def.quotient_lift_const ("Ap4", @{term rAp4})) - |> snd o (Quotient_Def.quotient_lift_const ("Lm4", @{term rLm4}))) -*} -print_theorems - -local_setup {* snd o prove_const_rsp @{binding fv_rtrm4_rsp} [@{term fv_rtrm4}] - (fn _ => fvbv_rsp_tac @{thm alpha_rtrm4_alpha_rtrm4_list.inducts(1)} @{thms fv_rtrm4_fv_rtrm4_list.simps} 1) *} -print_theorems - -local_setup {* snd o prove_const_rsp @{binding rVr4_rsp} [@{term rVr4}] - (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp} @{thms alpha4_equivp} 1) *} -lemma "(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4" -apply simp -apply clarify -apply (simp add: alpha4_inj) - - -local_setup {* snd o prove_const_rsp @{binding rLm4_rsp} [@{term rLm4}] - (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp} @{thms alpha4_equivp} 1) *} -local_setup {* snd o prove_const_rsp @{binding permute_rtrm4_rsp} - [@{term "permute :: perm \ rtrm4 \ rtrm4"}, @{term "permute :: perm \ rtrm4 list \ rtrm4 list"}] - (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *} - -thm rtrm4.induct -lemmas trm1_bp_induct = rtrm4.induct[quot_lifted] - -end diff -r 2f1b00d83925 -r b679900fa5f6 Nominal/Term5.thy --- a/Nominal/Term5.thy Tue Mar 23 08:16:39 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,344 +0,0 @@ -theory Term5 -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" -begin - -atom_decl name - -datatype rtrm5 = - rVr5 "name" -| rAp5 "rtrm5" "rtrm5" -| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)" -and rlts = - rLnil -| rLcons "name" "rtrm5" "rlts" - -primrec - rbv5 -where - "rbv5 rLnil = {}" -| "rbv5 (rLcons n t ltl) = {atom n} \ (rbv5 ltl)" - - -setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term5.rtrm5") 2 *} -print_theorems - -local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5") - [[[], [], [(SOME (@{term rbv5}, true), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *} -print_theorems - -notation - alpha_rtrm5 ("_ \5 _" [100, 100] 100) and - alpha_rlts ("_ \l _" [100, 100] 100) -thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros - -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} ctxt)) ctxt)) *} -thm alpha5_inj - -lemma rbv5_eqvt[eqvt]: - "pi \ (rbv5 x) = rbv5 (pi \ x)" - apply (induct x) - apply (simp_all add: eqvts atom_eqvt) - done - -lemma fv_rtrm5_rlts_eqvt[eqvt]: - "pi \ (fv_rtrm5 x) = fv_rtrm5 (pi \ x)" - "pi \ (fv_rlts l) = fv_rlts (pi \ l)" - apply (induct x and l) - apply (simp_all add: eqvts atom_eqvt) - done - -(*lemma alpha5_eqvt: - "(xa \5 y \ (p \ xa) \5 (p \ y)) \ - (xb \l ya \ (p \ xb) \l (p \ ya)) \ - (alpha_rbv5 b c \ alpha_rbv5 (p \ b) (p \ c))" -apply (tactic {* alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} @{context} 1 *}) -done*) - -local_setup {* -(fn ctxt => snd (Local_Theory.note ((@{binding alpha5_eqvt}, []), -build_alpha_eqvts [@{term alpha_rtrm5}, @{term alpha_rlts}, @{term alpha_rbv5}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} ctxt 1) ctxt) ctxt)) *} -print_theorems - -lemma alpha5_reflp: -"y \5 y \ (x \l x \ alpha_rbv5 x x)" -apply (rule rtrm5_rlts.induct) -apply (simp_all add: alpha5_inj) -apply (rule_tac x="0::perm" in exI) -apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm) -done - -lemma alpha5_symp: -"(a \5 b \ b \5 a) \ -(x \l y \ y \l x) \ -(alpha_rbv5 x y \ alpha_rbv5 y x)" -apply (tactic {* symp_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms alpha5_eqvt} @{context} 1 *}) -done - -lemma alpha5_symp1: -"(a \5 b \ b \5 a) \ -(x \l y \ y \l x) \ -(alpha_rbv5 x y \ alpha_rbv5 y x)" -apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) -apply (simp_all add: alpha5_inj) -apply (erule exE) -apply (rule_tac x="- pi" in exI) -apply (simp add: alpha_gen) - apply(simp add: fresh_star_def fresh_minus_perm) -apply clarify -apply (rule conjI) -apply (rotate_tac 3) -apply (frule_tac p="- pi" in alpha5_eqvt(2)) -apply simp -apply (rule conjI) -apply (rotate_tac 5) -apply (frule_tac p="- pi" in alpha5_eqvt(1)) -apply simp -apply (rotate_tac 6) -apply simp -apply (drule_tac p1="- pi" in permute_eq_iff[symmetric,THEN iffD1]) -apply (simp) -done - -thm alpha_gen_sym[no_vars] -thm alpha_gen_compose_sym[no_vars] - -lemma tt: - "\R (- p \ x) y \ R (p \ y) x; (bs, x) \gen R f (- p) (cs, y)\ \ (cs, y) \gen R f p (bs, x)" - unfolding alphas - unfolding fresh_star_def - by (auto simp add: fresh_minus_perm) - -lemma alpha5_symp2: - shows "a \5 b \ b \5 a" - and "x \l y \ y \l x" - and "alpha_rbv5 x y \ alpha_rbv5 y x" -apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) -(* non-binding case *) -apply(simp add: alpha5_inj) -(* non-binding case *) -apply(simp add: alpha5_inj) -(* binding case *) -apply(simp add: alpha5_inj) -apply(erule exE) -apply(rule_tac x="- pi" in exI) -apply(rule tt) -apply(simp add: alphas) -apply(erule conjE)+ -apply(drule_tac p="- pi" in alpha5_eqvt(2)) -apply(drule_tac p="- pi" in alpha5_eqvt(2)) -apply(drule_tac p="- pi" in alpha5_eqvt(1)) -apply(drule_tac p="- pi" in alpha5_eqvt(1)) -apply(simp) -apply(simp add: alphas) -apply(erule conjE)+ -apply metis -(* non-binding case *) -apply(simp add: alpha5_inj) -(* non-binding case *) -apply(simp add: alpha5_inj) -(* non-binding case *) -apply(simp add: alpha5_inj) -(* non-binding case *) -apply(simp add: alpha5_inj) -done - -lemma alpha5_transp: -"(a \5 b \ (\c. b \5 c \ a \5 c)) \ -(x \l y \ (\z. y \l z \ x \l z)) \ -(alpha_rbv5 k l \ (\m. alpha_rbv5 l m \ alpha_rbv5 k m))" -(*apply (tactic {* transp_tac @{context} @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} [] @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{thms alpha5_eqvt} 1 *})*) -apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) -apply (rule_tac [!] allI) -apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) -apply (simp_all add: alpha5_inj) -apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) -apply (simp_all add: alpha5_inj) -apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) -apply (simp_all add: alpha5_inj) -defer -apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) -apply (simp_all add: alpha5_inj) -apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) -apply (simp_all add: alpha5_inj) -apply (tactic {* eetac @{thm exi_sum} @{context} 1 *}) -(* HERE *) -(* -apply(rule alpha_gen_trans) -thm alpha_gen_trans -defer -apply (simp add: alpha_gen) -apply clarify -apply(simp add: fresh_star_plus) -apply (rule conjI) -apply (erule_tac x="- pi \ rltsaa" in allE) -apply (rotate_tac 5) -apply (drule_tac p="- pi" in alpha5_eqvt(2)) -apply simp -apply (drule_tac p="pi" in alpha5_eqvt(2)) -apply simp -apply (erule_tac x="- pi \ rtrm5aa" in allE) -apply (rotate_tac 7) -apply (drule_tac p="- pi" in alpha5_eqvt(1)) -apply simp -apply (rotate_tac 3) -apply (drule_tac p="pi" in alpha5_eqvt(1)) -apply simp -done -*) -sorry - -lemma alpha5_equivp: - "equivp alpha_rtrm5" - "equivp alpha_rlts" - unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def - apply (simp_all only: alpha5_reflp) - apply (meson alpha5_symp alpha5_transp) - apply (meson alpha5_symp alpha5_transp) - done - -quotient_type - trm5 = rtrm5 / alpha_rtrm5 -and - lts = rlts / alpha_rlts - by (auto intro: alpha5_equivp) - -local_setup {* -(fn ctxt => ctxt - |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5})) - |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5})) - |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5})) - |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil})) - |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons})) - |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5})) - |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts})) - |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5})) - |> snd o (Quotient_Def.quotient_lift_const ("alpha_bv5", @{term alpha_rbv5}))) -*} -print_theorems - -lemma alpha5_rfv: - "(t \5 s \ fv_rtrm5 t = fv_rtrm5 s)" - "(l \l m \ fv_rlts l = fv_rlts m)" - "(alpha_rbv5 b c \ True)" - apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) - apply(simp_all add: eqvts) - apply(simp add: alpha_gen) - apply(clarify) - apply blast -done - -lemma bv_list_rsp: - shows "x \l y \ rbv5 x = rbv5 y" - apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) - apply(simp_all) - apply(clarify) - apply simp - done - -local_setup {* snd o Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel @{context} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases}) [(@{thms rtrm5.distinct}, @{term alpha_rtrm5}), (@{thms rlts.distinct}, @{term alpha_rlts}), (@{thms rlts.distinct}, @{term alpha_rbv5})]))) *} -print_theorems - -local_setup {* snd o Local_Theory.note ((@{binding alpha_bn_rsp}, []), prove_alpha_bn_rsp [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts} @{thms rtrm5.exhaust rlts.exhaust} @{thms alpha5_inj alpha_dis} @{thms alpha5_equivp} @{context} (@{term alpha_rbv5}, 1)) *} -thm alpha_bn_rsp - -lemma [quot_respect]: - "(alpha_rlts ===> op =) fv_rlts fv_rlts" - "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5" - "(alpha_rlts ===> op =) rbv5 rbv5" - "(op = ===> alpha_rtrm5) rVr5 rVr5" - "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5" - "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" - "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" - "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" - "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" - "(alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5" - apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha_bn_rsp) - apply (clarify) - apply (rule_tac x="0" in exI) - apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) -done - - -lemma - shows "(alpha_rlts ===> op =) rbv5 rbv5" - by (simp add: bv_list_rsp) - -lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted] - -instantiation trm5 and lts :: pt -begin - -quotient_definition - "permute_trm5 :: perm \ trm5 \ trm5" -is - "permute :: perm \ rtrm5 \ rtrm5" - -quotient_definition - "permute_lts :: perm \ lts \ lts" -is - "permute :: perm \ rlts \ rlts" - -instance by default - (simp_all add: permute_rtrm5_permute_rlts_zero[quot_lifted] permute_rtrm5_permute_rlts_append[quot_lifted]) - -end - -lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] -lemmas bv5[simp] = rbv5.simps[quot_lifted] -lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] -lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen2, unfolded alpha_gen, quot_lifted, folded alpha_gen2, folded alpha_gen] -lemmas alpha5_DIS = alpha_dis[quot_lifted] - -(* why is this not in Isabelle? *) -lemma set_sub: "{a, b} - {b} = {a} - {b}" -by auto - -lemma lets_bla: - "x \ z \ y \ z \ x \ y \(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) \ (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))" -apply (simp only: alpha5_INJ bv5) -apply simp -apply (rule allI) -apply (simp_all add: alpha_gen) -apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ eqvts) -apply (rule impI) -apply (rule impI) -apply (rule impI) -apply (simp add: set_sub) -done - -lemma lets_ok: - "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" -thm alpha5_INJ -apply (simp only: alpha5_INJ) -apply (rule_tac x="(x \ y)" in exI) -apply (simp_all add: alpha_gen) -apply (simp add: permute_trm5_lts fresh_star_def) -apply (simp add: eqvts) -done - -lemma lets_ok3: - "x \ y \ - (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \ - (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" -apply (simp add: permute_trm5_lts alpha_gen alpha5_INJ) -done - - -lemma lets_not_ok1: - "x \ y \ - (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \ - (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" -apply (simp add: alpha5_INJ alpha_gen) -apply (simp add: permute_trm5_lts eqvts) -apply (simp add: alpha5_INJ) -done - -lemma lets_nok: - "x \ y \ x \ z \ z \ y \ - (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \ - (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" -apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def) -apply (simp add: alpha5_DIS alpha5_INJ permute_trm5_lts) -done - -end diff -r 2f1b00d83925 -r b679900fa5f6 Nominal/Term5n.thy --- a/Nominal/Term5n.thy Tue Mar 23 08:16:39 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,228 +0,0 @@ -theory Term5 -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" -begin - -atom_decl name - -datatype rtrm5 = - rVr5 "name" -| rAp5 "rtrm5" "rtrm5" -| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)" -and rlts = - rLnil -| rLcons "name" "rtrm5" "rlts" - -primrec - rbv5 -where - "rbv5 rLnil = {}" -| "rbv5 (rLcons n t ltl) = {atom n} \ (rbv5 ltl)" - - -setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term5.rtrm5") 2 *} -print_theorems - -local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5") - [[[], [], [(SOME (@{term rbv5}, false), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *} -print_theorems - -notation - alpha_rtrm5 ("_ \5 _" [100, 100] 100) and - alpha_rlts ("_ \l _" [100, 100] 100) -thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros - -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} ctxt)) ctxt)) *} -thm alpha5_inj - -lemma rbv5_eqvt[eqvt]: - "pi \ (rbv5 x) = rbv5 (pi \ x)" - apply (induct x) - apply (simp_all add: eqvts atom_eqvt) - done - -lemma fv_rtrm5_rlts_eqvt[eqvt]: - "pi \ (fv_rtrm5 x) = fv_rtrm5 (pi \ x)" - "pi \ (fv_rlts l) = fv_rlts (pi \ l)" - "pi \ (fv_rbv5 l) = fv_rbv5 (pi \ l)" - apply (induct x and l) - apply (simp_all add: eqvts atom_eqvt) - done - -local_setup {* -(fn ctxt => snd (Local_Theory.note ((@{binding alpha5_eqvt}, []), -build_alpha_eqvts [@{term alpha_rtrm5}, @{term alpha_rlts}, @{term alpha_rbv5}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} ctxt 1) ctxt) ctxt)) *} -print_theorems - -lemma alpha5_reflp: -"y \5 y \ (x \l x \ alpha_rbv5 x x)" -apply (rule rtrm5_rlts.induct) -apply (simp_all add: alpha5_inj) -apply (rule_tac x="0::perm" in exI) -apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm) -done - -lemma alpha5_symp: -"(a \5 b \ b \5 a) \ -(x \l y \ y \l x) \ -(alpha_rbv5 x y \ alpha_rbv5 y x)" -sorry - -lemma alpha5_transp: -"(a \5 b \ (\c. b \5 c \ a \5 c)) \ -(x \l y \ (\z. y \l z \ x \l z)) \ -(alpha_rbv5 k l \ (\m. alpha_rbv5 l m \ alpha_rbv5 k m))" -sorry - -lemma alpha5_equivp: - "equivp alpha_rtrm5" - "equivp alpha_rlts" - unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def - apply (simp_all only: alpha5_reflp) - apply (meson alpha5_symp alpha5_transp) - apply (meson alpha5_symp alpha5_transp) - done - -quotient_type - trm5 = rtrm5 / alpha_rtrm5 -and - lts = rlts / alpha_rlts - by (auto intro: alpha5_equivp) - -local_setup {* -(fn ctxt => ctxt - |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5})) - |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5})) - |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5})) - |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil})) - |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons})) - |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5})) - |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts})) - |> snd o (Quotient_Def.quotient_lift_const ("fv_bv5", @{term fv_rbv5})) - |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5})) - |> snd o (Quotient_Def.quotient_lift_const ("alpha_bv5", @{term alpha_rbv5}))) -*} -print_theorems - -lemma alpha5_rfv: - "(t \5 s \ fv_rtrm5 t = fv_rtrm5 s)" - "(l \l m \ (fv_rlts l = fv_rlts m \ fv_rbv5 l = fv_rbv5 m))" - "(alpha_rbv5 b c \ fv_rbv5 b = fv_rbv5 c)" - apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) - apply(simp_all) - apply(simp add: alpha_gen) - done - -lemma bv_list_rsp: - shows "x \l y \ rbv5 x = rbv5 y" - apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) - apply(simp_all) - apply(clarify) - apply simp - done - -local_setup {* snd o Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel @{context} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases}) [(@{thms rtrm5.distinct}, @{term alpha_rtrm5}), (@{thms rlts.distinct}, @{term alpha_rlts}), (@{thms rlts.distinct}, @{term alpha_rbv5})]))) *} -print_theorems - -local_setup {* snd o Local_Theory.note ((@{binding alpha_bn_rsp}, []), prove_alpha_bn_rsp [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts} @{thms alpha5_inj alpha_dis} @{thms alpha5_equivp} @{context} (@{term alpha_rbv5}, 1)) *} -thm alpha_bn_rsp - - -lemma [quot_respect]: - "(alpha_rlts ===> op =) fv_rlts fv_rlts" - "(alpha_rlts ===> op =) fv_rbv5 fv_rbv5" - "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5" - "(alpha_rlts ===> op =) rbv5 rbv5" - "(op = ===> alpha_rtrm5) rVr5 rVr5" - "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5" - "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" - "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" - "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" - "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" - "(alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5" - apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha5_reflp alpha_bn_rsp) - apply (clarify) - apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) -done - -lemma - shows "(alpha_rlts ===> op =) rbv5 rbv5" - by (simp add: bv_list_rsp) - -lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted] - -instantiation trm5 and lts :: pt -begin - -quotient_definition - "permute_trm5 :: perm \ trm5 \ trm5" -is - "permute :: perm \ rtrm5 \ rtrm5" - -quotient_definition - "permute_lts :: perm \ lts \ lts" -is - "permute :: perm \ rlts \ rlts" - -instance by default - (simp_all add: permute_rtrm5_permute_rlts_zero[quot_lifted] permute_rtrm5_permute_rlts_append[quot_lifted]) - -end - -lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] -lemmas bv5[simp] = rbv5.simps[quot_lifted] -lemmas fv_trm5_bv5[simp] = fv_rtrm5_fv_rbv5.simps[quot_lifted] -lemmas fv_lts[simp] = fv_rlts.simps[quot_lifted] -lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] - -lemma lets_bla: - "x \ z \ y \ z \ x \ y \(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) \ (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))" -apply (simp only: alpha5_INJ) -apply (simp only: bv5) -apply simp -done - -lemma lets_ok: - "(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" -apply (simp add: alpha5_INJ) -apply (rule_tac x="(x \ y)" in exI) -apply (simp_all add: alpha_gen) -apply (simp add: permute_trm5_lts fresh_star_def eqvts) -done - -lemma lets_ok3: - "x \ y \ - (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \ - (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" -apply (simp add: permute_trm5_lts alpha_gen alpha5_INJ) -done - - -lemma lets_not_ok1: - "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = - (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" -apply (simp add: alpha5_INJ alpha_gen) -apply (rule_tac x="0::perm" in exI) -apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1) eqvts) -apply blast -done - -lemma distinct_helper: - shows "\(rVr5 x \5 rAp5 y z)" - apply auto - apply (erule alpha_rtrm5.cases) - apply (simp_all only: rtrm5.distinct) - done - -lemma distinct_helper2: - shows "(Vr5 x) \ (Ap5 y z)" - by (lifting distinct_helper) - -lemma lets_nok: - "x \ y \ x \ z \ z \ y \ - (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \ - (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" -apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def) -apply (simp add: distinct_helper2 alpha5_INJ permute_trm5_lts) -done - -end diff -r 2f1b00d83925 -r b679900fa5f6 Nominal/Term8.thy --- a/Nominal/Term8.thy Tue Mar 23 08:16:39 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,61 +0,0 @@ -theory Term8 -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" -begin - -atom_decl name - -datatype rfoo8 = - Foo0 "name" -| Foo1 "rbar8" "rfoo8" --"bind bv(bar) in foo" -and rbar8 = - Bar0 "name" -| Bar1 "name" "name" "rbar8" --"bind second name in b" - -primrec - rbv8 -where - "rbv8 (Bar0 x) = {}" -| "rbv8 (Bar1 v x b) = {atom v}" - -setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term8.rfoo8") 2 *} -print_theorems - -local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term8.rfoo8") [ - [[[]], [[], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *} -notation - alpha_rfoo8 ("_ \f' _" [100, 100] 100) and - alpha_rbar8 ("_ \b' _" [100, 100] 100) -thm alpha_rfoo8_alpha_rbar8.intros - - -inductive - alpha8f :: "rfoo8 \ rfoo8 \ bool" ("_ \f _" [100, 100] 100) -and - alpha8b :: "rbar8 \ rbar8 \ bool" ("_ \b _" [100, 100] 100) -where - a1: "a = b \ (Foo0 a) \f (Foo0 b)" -| a2: "a = b \ (Bar0 a) \b (Bar0 b)" -| a3: "b1 \b b2 \ (\pi. (((rbv8 b1), t1) \gen alpha8f fv_rfoo8 pi ((rbv8 b2), t2))) \ Foo1 b1 t1 \f Foo1 b2 t2" -| a4: "v1 = v2 \ (\pi. (({atom x1}, t1) \gen alpha8b fv_rbar8 pi ({atom x2}, t2))) \ Bar1 v1 x1 t1 \b Bar1 v2 x2 t2" - -lemma "(alpha8b ===> op =) rbv8 rbv8" - apply simp apply clarify - apply (erule alpha8f_alpha8b.inducts(2)) - apply (simp_all) -done - -lemma fv_rbar8_rsp_hlp: "x \b y \ fv_rbar8 x = fv_rbar8 y" - apply (erule alpha8f_alpha8b.inducts(2)) - apply (simp_all add: alpha_gen) -done -lemma "(alpha8b ===> op =) fv_rbar8 fv_rbar8" - apply simp apply clarify apply (simp add: fv_rbar8_rsp_hlp) -done - -lemma "(alpha8f ===> op =) fv_rfoo8 fv_rfoo8" - apply simp apply clarify - apply (erule alpha8f_alpha8b.inducts(1)) - apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp) -done - -end