# HG changeset patch # User Cezary Kaliszyk # Date 1267103648 -3600 # Node ID 8c3cf9f4f5f2cc1873255035ff530d2829e5bcb9 # Parent 76d4d66309bd1fcb109ec9b8c25ecaca00bf4b71 Split Terms into separate files and add them to tests. diff -r 76d4d66309bd -r 8c3cf9f4f5f2 Nominal/ROOT.ML --- a/Nominal/ROOT.ML Thu Feb 25 12:32:15 2010 +0100 +++ b/Nominal/ROOT.ML Thu Feb 25 14:14:08 2010 +0100 @@ -5,4 +5,15 @@ "Nominal2_Eqvt", "Nominal2_Atoms", "Nominal2_Supp", - "Test"]; + "Test", + "Term1", + "Term2", + "Term3", + "Term4", + "Term5", + "Term6", + "Term7", + "Term8", + "Term9", + "TySch", + "LFex"]; diff -r 76d4d66309bd -r 8c3cf9f4f5f2 Nominal/Term1.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Term1.thy Thu Feb 25 14:14:08 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 diff -r 76d4d66309bd -r 8c3cf9f4f5f2 Nominal/Term2.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Term2.thy Thu Feb 25 14:14:08 2010 +0100 @@ -0,0 +1,78 @@ +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 ["rtrm2", "rassign"] ["Term2.rtrm2", "Term2.rassign"] *} + +local_setup {* snd o define_fv_alpha "Term2.rtrm2" + [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv2}, 0)]]], + [[[], []]]] *} + +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 {* 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 {* 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 {* 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 {* 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 {* 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 {* 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 {* 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 76d4d66309bd -r 8c3cf9f4f5f2 Nominal/Term3.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Term3.thy Thu Feb 25 14:14:08 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 ["rtrm3", "rassigns"] ["Term3.rtrm3", "Term3.rassigns"] *} + +local_setup {* snd o define_fv_alpha "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 76d4d66309bd -r 8c3cf9f4f5f2 Nominal/Term4.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Term4.thy Thu Feb 25 14:14:08 2010 +0100 @@ -0,0 +1,65 @@ +theory Term4 +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" +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 ["rtrm4"] ["Term4.rtrm4"] *} + +(* "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 "Term4.rtrm4" [ + [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]] ] *} +print_theorems + +notation + alpha_rtrm4 ("_ \4 _" [100, 100] 100) and + alpha_rtrm4_list ("_ \4l _" [100, 100] 100) +thm alpha_rtrm4_alpha_rtrm4_list.intros + +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *} +thm alpha4_inj +thm alpha_rtrm4_alpha_rtrm4_list.induct + +local_setup {* +snd o build_eqvts @{binding fv_rtrm4_fv_rtrm4_list_eqvt} [@{term fv_rtrm4}, @{term fv_rtrm4_list}] [@{term "permute :: perm \ rtrm4 \ rtrm4"},@{term "permute :: perm \ rtrm4 list \ rtrm4 list"}] (@{thms fv_rtrm4_fv_rtrm4_list.simps permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]}) @{thm rtrm4.induct} +*} +print_theorems + +local_setup {* +(fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt}, []), + build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] [@{term "permute :: perm \ rtrm4 \ rtrm4"},@{term "permute :: perm \ rtrm4 list \ rtrm4 list"}] @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} ctxt) ctxt)) +*} +print_theorems + +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []), + (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *} +thm alpha4_equivp + +quotient_type + qrtrm4 = rtrm4 / alpha_rtrm4 and + qrtrm4list = "rtrm4 list" / alpha_rtrm4_list + by (simp_all add: alpha4_equivp) + +end diff -r 76d4d66309bd -r 8c3cf9f4f5f2 Nominal/Term5.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Term5.thy Thu Feb 25 14:14:08 2010 +0100 @@ -0,0 +1,203 @@ +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 ["rtrm5", "rlts"] ["Term5.rtrm5", "Term5.rlts"] *} +print_theorems + +local_setup {* snd o define_fv_alpha "Term5.rtrm5" [ + [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]] ] *} +print_theorems + +(* Alternate version with additional binding of name in rlts in rLcons *) +(*local_setup {* snd o define_fv_alpha "Term5.rtrm5" [ + [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE,0)], [], [(NONE,0)]]] ] *} +print_theorems*) + +notation + alpha_rtrm5 ("_ \5 _" [100, 100] 100) and + alpha_rlts ("_ \l _" [100, 100] 100) +thm alpha_rtrm5_alpha_rlts.intros + +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases} ctxt)) ctxt)) *} +thm alpha5_inj + +lemma 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 \ (x \ xa) \5 (x \ y)" + "xb \l ya \ (x \ xb) \l (x \ ya)" + apply (induct rule: alpha_rtrm5_alpha_rlts.inducts) + apply (simp_all add: alpha5_inj) + apply (tactic {* + ALLGOALS ( + TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW + (etac @{thm alpha_gen_compose_eqvt}) + ) *}) + apply (simp_all only: eqvts atom_eqvt) + done + +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_equivp}, []), + (build_equivps [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thm rtrm5_rlts.induct} @{thm alpha_rtrm5_alpha_rlts.induct} @{thms rtrm5.inject rlts.inject} @{thms alpha5_inj} @{thms rtrm5.distinct rlts.distinct} @{thms alpha_rtrm5.cases alpha_rlts.cases} @{thms alpha5_eqvt} ctxt)) ctxt)) *} +thm alpha5_equivp + +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}))) +*} +print_theorems + +lemma alpha5_rfv: + "(t \5 s \ fv_rtrm5 t = fv_rtrm5 s)" + "(l \l m \ fv_rlts l = fv_rlts m)" + apply(induct rule: alpha_rtrm5_alpha_rlts.inducts) + apply(simp_all add: alpha_gen) + done + +lemma bv_list_rsp: + shows "x \l y \ rbv5 x = rbv5 y" + apply(induct rule: alpha_rtrm5_alpha_rlts.inducts(2)) + apply(simp_all) + done + +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" + apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp) + apply (clarify) apply (rule conjI) + apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) + 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] +and alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] +and bv5[simp] = rbv5.simps[quot_lifted] +and fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] + +lemma lets_ok: + "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" +apply (subst alpha5_INJ) +apply (rule conjI) +apply (rule_tac x="(x \ y)" in exI) +apply (simp only: alpha_gen) +apply (simp add: permute_trm5_lts fresh_star_def) +apply (rule_tac x="(x \ y)" in exI) +apply (simp only: alpha_gen) +apply (simp add: permute_trm5_lts fresh_star_def) +done + +lemma lets_ok2: + "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = + (Lt5 (Lcons y (Vr5 y) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" +apply (subst alpha5_INJ) +apply (rule conjI) +apply (rule_tac x="(x \ y)" in exI) +apply (simp only: alpha_gen) +apply (simp add: permute_trm5_lts fresh_star_def) +apply (rule_tac x="0 :: perm" in exI) +apply (simp only: alpha_gen) +apply (simp add: permute_trm5_lts fresh_star_def) +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(3) alpha_gen) +apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1)) +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) +done + + +end diff -r 76d4d66309bd -r 8c3cf9f4f5f2 Nominal/Term6.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Term6.thy Thu Feb 25 14:14:08 2010 +0100 @@ -0,0 +1,155 @@ +theory Term6 +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" +begin + +atom_decl name + +(* example with a bn function defined over the type itself, NOT respectful. *) + +datatype rtrm6 = + rVr6 "name" +| rLm6 "name" "rtrm6" --"bind name in rtrm6" +| rLt6 "rtrm6" "rtrm6" --"bind (bv6 left) in (right)" + +primrec + rbv6 +where + "rbv6 (rVr6 n) = {}" +| "rbv6 (rLm6 n t) = {atom n} \ rbv6 t" +| "rbv6 (rLt6 l r) = rbv6 l \ rbv6 r" + +setup {* snd o define_raw_perms ["rtrm6"] ["Term6.rtrm6"] *} +print_theorems + +local_setup {* snd o define_fv_alpha "Term6.rtrm6" [ + [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *} +notation alpha_rtrm6 ("_ \6 _" [100, 100] 100) +thm alpha_rtrm6.intros + +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_inj}, []), (build_alpha_inj @{thms alpha_rtrm6.intros} @{thms rtrm6.distinct rtrm6.inject} @{thms alpha_rtrm6.cases} ctxt)) ctxt)) *} +thm alpha6_inj + +local_setup {* +snd o (build_eqvts @{binding rbv6_eqvt} [@{term rbv6}] [@{term "permute :: perm \ rtrm6 \ rtrm6"}] (@{thms rbv6.simps permute_rtrm6.simps}) @{thm rtrm6.induct}) +*} + +local_setup {* +snd o build_eqvts @{binding fv_rtrm6_eqvt} [@{term fv_rtrm6}] [@{term "permute :: perm \ rtrm6 \ rtrm6"}] (@{thms fv_rtrm6.simps permute_rtrm6.simps}) @{thm rtrm6.induct} +*} + +local_setup {* +(fn ctxt => snd (Local_Theory.note ((@{binding alpha6_eqvt}, []), + build_alpha_eqvts [@{term alpha_rtrm6}] [@{term "permute :: perm \ rtrm6 \ rtrm6"}] @{thms permute_rtrm6.simps alpha6_inj} @{thm alpha_rtrm6.induct} ctxt) ctxt)) +*} + +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_equivp}, []), + (build_equivps [@{term alpha_rtrm6}] @{thm rtrm6.induct} @{thm alpha_rtrm6.induct} @{thms rtrm6.inject} @{thms alpha6_inj} @{thms rtrm6.distinct} @{thms alpha_rtrm6.cases} @{thms alpha6_eqvt} ctxt)) ctxt)) *} +thm alpha6_equivp + +quotient_type + trm6 = rtrm6 / alpha_rtrm6 + by (auto intro: alpha6_equivp) + +local_setup {* +(fn ctxt => ctxt + |> snd o (Quotient_Def.quotient_lift_const ("Vr6", @{term rVr6})) + |> snd o (Quotient_Def.quotient_lift_const ("Lm6", @{term rLm6})) + |> snd o (Quotient_Def.quotient_lift_const ("Lt6", @{term rLt6})) + |> snd o (Quotient_Def.quotient_lift_const ("fv_trm6", @{term fv_rtrm6})) + |> snd o (Quotient_Def.quotient_lift_const ("bv6", @{term rbv6}))) +*} +print_theorems + +lemma [quot_respect]: + "(op = ===> alpha_rtrm6 ===> alpha_rtrm6) permute permute" +by (auto simp add: alpha6_eqvt) + +(* Definitely not true , see lemma below *) +lemma [quot_respect]:"(alpha_rtrm6 ===> op =) rbv6 rbv6" +apply simp apply clarify +apply (erule alpha_rtrm6.induct) +oops + +lemma "(a :: name) \ b \ \ (alpha_rtrm6 ===> op =) rbv6 rbv6" +apply simp +apply (rule_tac x="rLm6 (a::name) (rVr6 (a :: name))" in exI) +apply (rule_tac x="rLm6 (b::name) (rVr6 (b :: name))" in exI) +apply simp +apply (simp add: alpha6_inj) +apply (rule_tac x="(a \ b)" in exI) +apply (simp add: alpha_gen fresh_star_def) +apply (simp add: alpha6_inj) +done + +lemma fv6_rsp: "x \6 y \ fv_rtrm6 x = fv_rtrm6 y" +apply (induct_tac x y rule: alpha_rtrm6.induct) +apply simp_all +apply (erule exE) +apply (simp_all add: alpha_gen) +done + +lemma [quot_respect]:"(alpha_rtrm6 ===> op =) fv_rtrm6 fv_rtrm6" +by (simp add: fv6_rsp) + +lemma [quot_respect]: + "(op = ===> alpha_rtrm6) rVr6 rVr6" + "(op = ===> alpha_rtrm6 ===> alpha_rtrm6) rLm6 rLm6" +apply auto +apply (simp_all add: alpha6_inj) +apply (rule_tac x="0::perm" in exI) +apply (simp add: alpha_gen fv6_rsp fresh_star_def fresh_zero_perm) +done + +lemma [quot_respect]: + "(alpha_rtrm6 ===> alpha_rtrm6 ===> alpha_rtrm6) rLt6 rLt6" +apply auto +apply (simp_all add: alpha6_inj) +apply (rule_tac [!] x="0::perm" in exI) +apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm) +(* needs rbv6_rsp *) +oops + +instantiation trm6 :: pt begin + +quotient_definition + "permute_trm6 :: perm \ trm6 \ trm6" +is + "permute :: perm \ rtrm6 \ rtrm6" + +instance +apply default +sorry +end + +lemma lifted_induct: +"\x1 = x2; \name namea. name = namea \ P (Vr6 name) (Vr6 namea); + \name rtrm6 namea rtrm6a. + \True; + \pi. fv_trm6 rtrm6 - {atom name} = fv_trm6 rtrm6a - {atom namea} \ + (fv_trm6 rtrm6 - {atom name}) \* pi \ pi \ rtrm6 = rtrm6a \ P (pi \ rtrm6) rtrm6a\ + \ P (Lm6 name rtrm6) (Lm6 namea rtrm6a); + \rtrm61 rtrm61a rtrm62 rtrm62a. + \rtrm61 = rtrm61a; P rtrm61 rtrm61a; + \pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \ + (fv_trm6 rtrm62 - bv6 rtrm61) \* pi \ pi \ rtrm62 = rtrm62a \ P (pi \ rtrm62) rtrm62a\ + \ P (Lt6 rtrm61 rtrm62) (Lt6 rtrm61a rtrm62a)\ +\ P x1 x2" +apply (lifting alpha_rtrm6.induct[unfolded alpha_gen]) +apply injection +(* notice unsolvable goals: (alpha_rtrm6 ===> op =) rbv6 rbv6 *) +oops + +lemma lifted_inject_a3: +"(Lt6 rtrm61 rtrm62 = Lt6 rtrm61a rtrm62a) = +(rtrm61 = rtrm61a \ + (\pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \ + (fv_trm6 rtrm62 - bv6 rtrm61) \* pi \ pi \ rtrm62 = rtrm62a))" +apply(lifting alpha6_inj(3)[unfolded alpha_gen]) +apply injection +(* notice unsolvable goals: (alpha_rtrm6 ===> op =) rbv6 rbv6 *) +oops + + + + +end diff -r 76d4d66309bd -r 8c3cf9f4f5f2 Nominal/Term7.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Term7.thy Thu Feb 25 14:14:08 2010 +0100 @@ -0,0 +1,50 @@ +theory Term7 +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" +begin + +atom_decl name + +(* example with a respectful bn function defined over the type itself *) + +datatype rtrm7 = + rVr7 "name" +| rLm7 "name" "rtrm7" --"bind left in right" +| rLt7 "rtrm7" "rtrm7" --"bind (bv7 left) in (right)" + +primrec + rbv7 +where + "rbv7 (rVr7 n) = {atom n}" +| "rbv7 (rLm7 n t) = rbv7 t - {atom n}" +| "rbv7 (rLt7 l r) = rbv7 l \ rbv7 r" + +setup {* snd o define_raw_perms ["rtrm7"] ["Term7.rtrm7"] *} +thm permute_rtrm7.simps + +local_setup {* snd o define_fv_alpha "Term7.rtrm7" [ + [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv7}, 0)]]]] *} +print_theorems +notation + alpha_rtrm7 ("_ \7a _" [100, 100] 100) +thm alpha_rtrm7.intros +thm fv_rtrm7.simps +inductive + alpha7 :: "rtrm7 \ rtrm7 \ bool" ("_ \7 _" [100, 100] 100) +where + a1: "a = b \ (rVr7 a) \7 (rVr7 b)" +| a2: "(\pi. (({atom a}, t) \gen alpha7 fv_rtrm7 pi ({atom b}, s))) \ rLm7 a t \7 rLm7 b s" +| a3: "(\pi. (((rbv7 t1), s1) \gen alpha7 fv_rtrm7 pi ((rbv7 t2), s2))) \ rLt7 t1 s1 \7 rLt7 t2 s2" + +lemma "(x::name) \ y \ \ (alpha7 ===> op =) rbv7 rbv7" + apply simp + apply (rule_tac x="rLt7 (rVr7 x) (rVr7 x)" in exI) + apply (rule_tac x="rLt7 (rVr7 y) (rVr7 y)" in exI) + apply simp + apply (rule a3) + apply (rule_tac x="(x \ y)" in exI) + apply (simp_all add: alpha_gen fresh_star_def) + apply (rule a1) + apply (rule refl) +done + +end diff -r 76d4d66309bd -r 8c3cf9f4f5f2 Nominal/Term8.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Term8.thy Thu Feb 25 14:14:08 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 ["rfoo8", "rbar8"] ["Term8.rfoo8", "Term8.rbar8"] *} +print_theorems + +local_setup {* snd o define_fv_alpha "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 76d4d66309bd -r 8c3cf9f4f5f2 Nominal/Term9.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Term9.thy Thu Feb 25 14:14:08 2010 +0100 @@ -0,0 +1,78 @@ +theory Term9 +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" +begin + +atom_decl name + +datatype rlam9 = + Var9 "name" +| Lam9 "name" "rlam9" --"bind name in rlam" +and rbla9 = + Bla9 "rlam9" "rlam9" --"bind bv(first) in second" + +primrec + rbv9 +where + "rbv9 (Var9 x) = {}" +| "rbv9 (Lam9 x b) = {atom x}" + +setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Term9.rlam9", "Term9.rbla9"] *} +print_theorems + +local_setup {* snd o define_fv_alpha "Term9.rlam9" [ + [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[], [(SOME @{term rbv9}, 0)]]]] *} +notation + alpha_rlam9 ("_ \9l' _" [100, 100] 100) and + alpha_rbla9 ("_ \9b' _" [100, 100] 100) +thm alpha_rlam9_alpha_rbla9.intros + + +inductive + alpha9l :: "rlam9 \ rlam9 \ bool" ("_ \9l _" [100, 100] 100) +and + alpha9b :: "rbla9 \ rbla9 \ bool" ("_ \9b _" [100, 100] 100) +where + a1: "a = b \ (Var9 a) \9l (Var9 b)" +| a4: "(\pi. (({atom x1}, t1) \gen alpha9l fv_rlam9 pi ({atom x2}, t2))) \ Lam9 x1 t1 \9l Lam9 x2 t2" +| a3: "b1 \9l b2 \ (\pi. (((rbv9 b1), t1) \gen alpha9l fv_rlam9 pi ((rbv9 b2), t2))) \ Bla9 b1 t1 \9b Bla9 b2 t2" + +quotient_type + lam9 = rlam9 / alpha9l and bla9 = rbla9 / alpha9b +sorry + +local_setup {* +(fn ctxt => ctxt + |> snd o (Quotient_Def.quotient_lift_const ("qVar9", @{term Var9})) + |> snd o (Quotient_Def.quotient_lift_const ("qLam9", @{term Lam9})) + |> snd o (Quotient_Def.quotient_lift_const ("qBla9", @{term Bla9})) + |> snd o (Quotient_Def.quotient_lift_const ("fv_lam9", @{term fv_rlam9})) + |> snd o (Quotient_Def.quotient_lift_const ("fv_bla9", @{term fv_rbla9})) + |> snd o (Quotient_Def.quotient_lift_const ("bv9", @{term rbv9}))) +*} +print_theorems + +instantiation lam9 and bla9 :: pt +begin + +quotient_definition + "permute_lam9 :: perm \ lam9 \ lam9" +is + "permute :: perm \ rlam9 \ rlam9" + +quotient_definition + "permute_bla9 :: perm \ bla9 \ bla9" +is + "permute :: perm \ rbla9 \ rbla9" + +instance +sorry + +end + +lemma "\b1 = b2; \pi. fv_lam9 t1 - bv9 b1 = fv_lam9 t2 - bv9 b2 \ (fv_lam9 t1 - bv9 b1) \* pi \ pi \ t1 = t2\ + \ qBla9 b1 t1 = qBla9 b2 t2" +apply (lifting a3[unfolded alpha_gen]) +apply injection +sorry + +end diff -r 76d4d66309bd -r 8c3cf9f4f5f2 Nominal/Terms.thy --- a/Nominal/Terms.thy Thu Feb 25 12:32:15 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1006 +0,0 @@ -theory Terms -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" -begin - -atom_decl name - -text {* primrec seems to be genarally faster than fun *} - -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"] ["Terms.rtrm1", "Terms.bp"] *} -thm permute_rtrm1_permute_bp.simps - -local_setup {* - snd o define_fv_alpha "Terms.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 ["Terms.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 - -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 ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *} - -local_setup {* snd o define_fv_alpha "Terms.rtrm2" - [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv2}, 0)]]], - [[[], []]]] *} - -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 {* 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 {* 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 {* 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 {* 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 {* 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 {* 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 {* prove_const_rsp @{binding permute_rtrm2_rsp} [@{term "permute :: perm \ rtrm2 \ rtrm2"}] - (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha2_eqvt}) 1) *} - - -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 ["rtrm3", "rassigns"] ["Terms.rtrm3", "Terms.rassigns"] *} - -local_setup {* snd o define_fv_alpha "Terms.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)) - - -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 ["rtrm4"] ["Terms.rtrm4"] *} - -(* "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 "Terms.rtrm4" [ - [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]] ] *} -print_theorems - -notation - alpha_rtrm4 ("_ \4 _" [100, 100] 100) and - alpha_rtrm4_list ("_ \4l _" [100, 100] 100) -thm alpha_rtrm4_alpha_rtrm4_list.intros - -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *} -thm alpha4_inj -thm alpha_rtrm4_alpha_rtrm4_list.induct - -local_setup {* -snd o build_eqvts @{binding fv_rtrm4_fv_rtrm4_list_eqvt} [@{term fv_rtrm4}, @{term fv_rtrm4_list}] [@{term "permute :: perm \ rtrm4 \ rtrm4"},@{term "permute :: perm \ rtrm4 list \ rtrm4 list"}] (@{thms fv_rtrm4_fv_rtrm4_list.simps permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]}) @{thm rtrm4.induct} -*} -print_theorems - -local_setup {* -(fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt}, []), - build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] [@{term "permute :: perm \ rtrm4 \ rtrm4"},@{term "permute :: perm \ rtrm4 list \ rtrm4 list"}] @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} ctxt) ctxt)) -*} -print_theorems - -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []), - (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *} -thm alpha4_equivp - -quotient_type - qrtrm4 = rtrm4 / alpha_rtrm4 and - qrtrm4list = "rtrm4 list" / alpha_rtrm4_list - by (simp_all add: alpha4_equivp) - - -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 ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *} -print_theorems - -local_setup {* snd o define_fv_alpha "Terms.rtrm5" [ - [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]] ] *} -print_theorems - -(* Alternate version with additional binding of name in rlts in rLcons *) -(*local_setup {* snd o define_fv_alpha "Terms.rtrm5" [ - [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE,0)], [], [(NONE,0)]]] ] *} -print_theorems*) - -notation - alpha_rtrm5 ("_ \5 _" [100, 100] 100) and - alpha_rlts ("_ \l _" [100, 100] 100) -thm alpha_rtrm5_alpha_rlts.intros - -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases} ctxt)) ctxt)) *} -thm alpha5_inj - -lemma 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 \ (x \ xa) \5 (x \ y)" - "xb \l ya \ (x \ xb) \l (x \ ya)" - apply (induct rule: alpha_rtrm5_alpha_rlts.inducts) - apply (simp_all add: alpha5_inj) - apply (tactic {* - ALLGOALS ( - TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW - (etac @{thm alpha_gen_compose_eqvt}) - ) *}) - apply (simp_all only: eqvts atom_eqvt) - done - -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_equivp}, []), - (build_equivps [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thm rtrm5_rlts.induct} @{thm alpha_rtrm5_alpha_rlts.induct} @{thms rtrm5.inject rlts.inject} @{thms alpha5_inj} @{thms rtrm5.distinct rlts.distinct} @{thms alpha_rtrm5.cases alpha_rlts.cases} @{thms alpha5_eqvt} ctxt)) ctxt)) *} -thm alpha5_equivp - -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}))) -*} -print_theorems - -lemma alpha5_rfv: - "(t \5 s \ fv_rtrm5 t = fv_rtrm5 s)" - "(l \l m \ fv_rlts l = fv_rlts m)" - apply(induct rule: alpha_rtrm5_alpha_rlts.inducts) - apply(simp_all add: alpha_gen) - done - -lemma bv_list_rsp: - shows "x \l y \ rbv5 x = rbv5 y" - apply(induct rule: alpha_rtrm5_alpha_rlts.inducts(2)) - apply(simp_all) - done - -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" - apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp) - apply (clarify) apply (rule conjI) - apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) - 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] -and alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] -and bv5[simp] = rbv5.simps[quot_lifted] -and fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] - -lemma lets_ok: - "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" -apply (subst alpha5_INJ) -apply (rule conjI) -apply (rule_tac x="(x \ y)" in exI) -apply (simp only: alpha_gen) -apply (simp add: permute_trm5_lts fresh_star_def) -apply (rule_tac x="(x \ y)" in exI) -apply (simp only: alpha_gen) -apply (simp add: permute_trm5_lts fresh_star_def) -done - -lemma lets_ok2: - "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = - (Lt5 (Lcons y (Vr5 y) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" -apply (subst alpha5_INJ) -apply (rule conjI) -apply (rule_tac x="(x \ y)" in exI) -apply (simp only: alpha_gen) -apply (simp add: permute_trm5_lts fresh_star_def) -apply (rule_tac x="0 :: perm" in exI) -apply (simp only: alpha_gen) -apply (simp add: permute_trm5_lts fresh_star_def) -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(3) alpha_gen) -apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1)) -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) -done - - -(* example with a bn function defined over the type itself *) -datatype rtrm6 = - rVr6 "name" -| rLm6 "name" "rtrm6" --"bind name in rtrm6" -| rLt6 "rtrm6" "rtrm6" --"bind (bv6 left) in (right)" - -primrec - rbv6 -where - "rbv6 (rVr6 n) = {}" -| "rbv6 (rLm6 n t) = {atom n} \ rbv6 t" -| "rbv6 (rLt6 l r) = rbv6 l \ rbv6 r" - -setup {* snd o define_raw_perms ["rtrm6"] ["Terms.rtrm6"] *} -print_theorems - -local_setup {* snd o define_fv_alpha "Terms.rtrm6" [ - [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *} -notation alpha_rtrm6 ("_ \6 _" [100, 100] 100) -(* HERE THE RULES DIFFER *) -thm alpha_rtrm6.intros - -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_inj}, []), (build_alpha_inj @{thms alpha_rtrm6.intros} @{thms rtrm6.distinct rtrm6.inject} @{thms alpha_rtrm6.cases} ctxt)) ctxt)) *} -thm alpha6_inj - -local_setup {* -snd o (build_eqvts @{binding rbv6_eqvt} [@{term rbv6}] [@{term "permute :: perm \ rtrm6 \ rtrm6"}] (@{thms rbv6.simps permute_rtrm6.simps}) @{thm rtrm6.induct}) -*} - -local_setup {* -snd o build_eqvts @{binding fv_rtrm6_eqvt} [@{term fv_rtrm6}] [@{term "permute :: perm \ rtrm6 \ rtrm6"}] (@{thms fv_rtrm6.simps permute_rtrm6.simps}) @{thm rtrm6.induct} -*} - -local_setup {* -(fn ctxt => snd (Local_Theory.note ((@{binding alpha6_eqvt}, []), - build_alpha_eqvts [@{term alpha_rtrm6}] [@{term "permute :: perm \ rtrm6 \ rtrm6"}] @{thms permute_rtrm6.simps alpha6_inj} @{thm alpha_rtrm6.induct} ctxt) ctxt)) -*} - -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_equivp}, []), - (build_equivps [@{term alpha_rtrm6}] @{thm rtrm6.induct} @{thm alpha_rtrm6.induct} @{thms rtrm6.inject} @{thms alpha6_inj} @{thms rtrm6.distinct} @{thms alpha_rtrm6.cases} @{thms alpha6_eqvt} ctxt)) ctxt)) *} -thm alpha6_equivp - -quotient_type - trm6 = rtrm6 / alpha_rtrm6 - by (auto intro: alpha6_equivp) - -local_setup {* -(fn ctxt => ctxt - |> snd o (Quotient_Def.quotient_lift_const ("Vr6", @{term rVr6})) - |> snd o (Quotient_Def.quotient_lift_const ("Lm6", @{term rLm6})) - |> snd o (Quotient_Def.quotient_lift_const ("Lt6", @{term rLt6})) - |> snd o (Quotient_Def.quotient_lift_const ("fv_trm6", @{term fv_rtrm6})) - |> snd o (Quotient_Def.quotient_lift_const ("bv6", @{term rbv6}))) -*} -print_theorems - -lemma [quot_respect]: - "(op = ===> alpha_rtrm6 ===> alpha_rtrm6) permute permute" -by (auto simp add: alpha6_eqvt) - -(* Definitely not true , see lemma below *) -lemma [quot_respect]:"(alpha_rtrm6 ===> op =) rbv6 rbv6" -apply simp apply clarify -apply (erule alpha_rtrm6.induct) -oops - -lemma "(a :: name) \ b \ \ (alpha_rtrm6 ===> op =) rbv6 rbv6" -apply simp -apply (rule_tac x="rLm6 (a::name) (rVr6 (a :: name))" in exI) -apply (rule_tac x="rLm6 (b::name) (rVr6 (b :: name))" in exI) -apply simp -apply (simp add: alpha6_inj) -apply (rule_tac x="(a \ b)" in exI) -apply (simp add: alpha_gen fresh_star_def) -apply (simp add: alpha6_inj) -done - -lemma fv6_rsp: "x \6 y \ fv_rtrm6 x = fv_rtrm6 y" -apply (induct_tac x y rule: alpha_rtrm6.induct) -apply simp_all -apply (erule exE) -apply (simp_all add: alpha_gen) -done - -lemma [quot_respect]:"(alpha_rtrm6 ===> op =) fv_rtrm6 fv_rtrm6" -by (simp add: fv6_rsp) - -lemma [quot_respect]: - "(op = ===> alpha_rtrm6) rVr6 rVr6" - "(op = ===> alpha_rtrm6 ===> alpha_rtrm6) rLm6 rLm6" -apply auto -apply (simp_all add: alpha6_inj) -apply (rule_tac x="0::perm" in exI) -apply (simp add: alpha_gen fv6_rsp fresh_star_def fresh_zero_perm) -done - -lemma [quot_respect]: - "(alpha_rtrm6 ===> alpha_rtrm6 ===> alpha_rtrm6) rLt6 rLt6" -apply auto -apply (simp_all add: alpha6_inj) -apply (rule_tac [!] x="0::perm" in exI) -apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm) -(* needs rbv6_rsp *) -oops - -instantiation trm6 :: pt begin - -quotient_definition - "permute_trm6 :: perm \ trm6 \ trm6" -is - "permute :: perm \ rtrm6 \ rtrm6" - -instance -apply default -sorry -end - -lemma lifted_induct: -"\x1 = x2; \name namea. name = namea \ P (Vr6 name) (Vr6 namea); - \name rtrm6 namea rtrm6a. - \True; - \pi. fv_trm6 rtrm6 - {atom name} = fv_trm6 rtrm6a - {atom namea} \ - (fv_trm6 rtrm6 - {atom name}) \* pi \ pi \ rtrm6 = rtrm6a \ P (pi \ rtrm6) rtrm6a\ - \ P (Lm6 name rtrm6) (Lm6 namea rtrm6a); - \rtrm61 rtrm61a rtrm62 rtrm62a. - \rtrm61 = rtrm61a; P rtrm61 rtrm61a; - \pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \ - (fv_trm6 rtrm62 - bv6 rtrm61) \* pi \ pi \ rtrm62 = rtrm62a \ P (pi \ rtrm62) rtrm62a\ - \ P (Lt6 rtrm61 rtrm62) (Lt6 rtrm61a rtrm62a)\ -\ P x1 x2" -apply (lifting alpha_rtrm6.induct[unfolded alpha_gen]) -apply injection -(* notice unsolvable goals: (alpha_rtrm6 ===> op =) rbv6 rbv6 *) -oops - -lemma lifted_inject_a3: -"(Lt6 rtrm61 rtrm62 = Lt6 rtrm61a rtrm62a) = -(rtrm61 = rtrm61a \ - (\pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \ - (fv_trm6 rtrm62 - bv6 rtrm61) \* pi \ pi \ rtrm62 = rtrm62a))" -apply(lifting alpha6_inj(3)[unfolded alpha_gen]) -apply injection -(* notice unsolvable goals: (alpha_rtrm6 ===> op =) rbv6 rbv6 *) -oops - - - - -(* example with a respectful bn function defined over the type itself *) - -datatype rtrm7 = - rVr7 "name" -| rLm7 "name" "rtrm7" --"bind left in right" -| rLt7 "rtrm7" "rtrm7" --"bind (bv7 left) in (right)" - -primrec - rbv7 -where - "rbv7 (rVr7 n) = {atom n}" -| "rbv7 (rLm7 n t) = rbv7 t - {atom n}" -| "rbv7 (rLt7 l r) = rbv7 l \ rbv7 r" - -setup {* snd o define_raw_perms ["rtrm7"] ["Terms.rtrm7"] *} -thm permute_rtrm7.simps - -local_setup {* snd o define_fv_alpha "Terms.rtrm7" [ - [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv7}, 0)]]]] *} -print_theorems -notation - alpha_rtrm7 ("_ \7a _" [100, 100] 100) -(* HERE THE RULES DIFFER *) -thm alpha_rtrm7.intros -thm fv_rtrm7.simps -inductive - alpha7 :: "rtrm7 \ rtrm7 \ bool" ("_ \7 _" [100, 100] 100) -where - a1: "a = b \ (rVr7 a) \7 (rVr7 b)" -| a2: "(\pi. (({atom a}, t) \gen alpha7 fv_rtrm7 pi ({atom b}, s))) \ rLm7 a t \7 rLm7 b s" -| a3: "(\pi. (((rbv7 t1), s1) \gen alpha7 fv_rtrm7 pi ((rbv7 t2), s2))) \ rLt7 t1 s1 \7 rLt7 t2 s2" - -lemma "(x::name) \ y \ \ (alpha7 ===> op =) rbv7 rbv7" - apply simp - apply (rule_tac x="rLt7 (rVr7 x) (rVr7 x)" in exI) - apply (rule_tac x="rLt7 (rVr7 y) (rVr7 y)" in exI) - apply simp - apply (rule a3) - apply (rule_tac x="(x \ y)" in exI) - apply (simp_all add: alpha_gen fresh_star_def) - apply (rule a1) - apply (rule refl) -done - - - - - -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 ["rfoo8", "rbar8"] ["Terms.rfoo8", "Terms.rbar8"] *} -print_theorems - -local_setup {* snd o define_fv_alpha "Terms.rfoo8" [ - [[[]], [[], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *} -notation - alpha_rfoo8 ("_ \f' _" [100, 100] 100) and - alpha_rbar8 ("_ \b' _" [100, 100] 100) -(* HERE THE RULE DIFFERS *) -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 - - - - - - -datatype rlam9 = - Var9 "name" -| Lam9 "name" "rlam9" --"bind name in rlam" -and rbla9 = - Bla9 "rlam9" "rlam9" --"bind bv(first) in second" - -primrec - rbv9 -where - "rbv9 (Var9 x) = {}" -| "rbv9 (Lam9 x b) = {atom x}" - -setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Terms.rlam9", "Terms.rbla9"] *} -print_theorems - -local_setup {* snd o define_fv_alpha "Terms.rlam9" [ - [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[], [(SOME @{term rbv9}, 0)]]]] *} -notation - alpha_rlam9 ("_ \9l' _" [100, 100] 100) and - alpha_rbla9 ("_ \9b' _" [100, 100] 100) -(* HERE THE RULES DIFFER *) -thm alpha_rlam9_alpha_rbla9.intros - - -inductive - alpha9l :: "rlam9 \ rlam9 \ bool" ("_ \9l _" [100, 100] 100) -and - alpha9b :: "rbla9 \ rbla9 \ bool" ("_ \9b _" [100, 100] 100) -where - a1: "a = b \ (Var9 a) \9l (Var9 b)" -| a4: "(\pi. (({atom x1}, t1) \gen alpha9l fv_rlam9 pi ({atom x2}, t2))) \ Lam9 x1 t1 \9l Lam9 x2 t2" -| a3: "b1 \9l b2 \ (\pi. (((rbv9 b1), t1) \gen alpha9l fv_rlam9 pi ((rbv9 b2), t2))) \ Bla9 b1 t1 \9b Bla9 b2 t2" - -quotient_type - lam9 = rlam9 / alpha9l and bla9 = rbla9 / alpha9b -sorry - -local_setup {* -(fn ctxt => ctxt - |> snd o (Quotient_Def.quotient_lift_const ("qVar9", @{term Var9})) - |> snd o (Quotient_Def.quotient_lift_const ("qLam9", @{term Lam9})) - |> snd o (Quotient_Def.quotient_lift_const ("qBla9", @{term Bla9})) - |> snd o (Quotient_Def.quotient_lift_const ("fv_lam9", @{term fv_rlam9})) - |> snd o (Quotient_Def.quotient_lift_const ("fv_bla9", @{term fv_rbla9})) - |> snd o (Quotient_Def.quotient_lift_const ("bv9", @{term rbv9}))) -*} -print_theorems - -instantiation lam9 and bla9 :: pt -begin - -quotient_definition - "permute_lam9 :: perm \ lam9 \ lam9" -is - "permute :: perm \ rlam9 \ rlam9" - -quotient_definition - "permute_bla9 :: perm \ bla9 \ bla9" -is - "permute :: perm \ rbla9 \ rbla9" - -instance -sorry - -end - -lemma "\b1 = b2; \pi. fv_lam9 t1 - bv9 b1 = fv_lam9 t2 - bv9 b2 \ (fv_lam9 t1 - bv9 b1) \* pi \ pi \ t1 = t2\ - \ qBla9 b1 t1 = qBla9 b2 t2" -apply (lifting a3[unfolded alpha_gen]) -apply injection -sorry - - - - - - - - -text {* type schemes *} -datatype ty = - Var "name" -| Fun "ty" "ty" - -setup {* snd o define_raw_perms ["ty"] ["Terms.ty"] *} -print_theorems - -datatype tyS = - All "name set" "ty" - -setup {* snd o define_raw_perms ["tyS"] ["Terms.tyS"] *} -print_theorems - -local_setup {* snd o define_fv_alpha "Terms.ty" [[[[]], [[], []]]] *} -print_theorems - -(* -Doesnot work yet since we do not refer to fv_ty -local_setup {* define_raw_fv "Terms.tyS" [[[[], []]]] *} -print_theorems -*) - -primrec - fv_tyS -where - "fv_tyS (All xs T) = (fv_ty T - atom ` xs)" - -inductive - alpha_tyS :: "tyS \ tyS \ bool" ("_ \tyS _" [100, 100] 100) -where - a1: "\pi. ((atom ` xs1, T1) \gen (op =) fv_ty pi (atom ` xs2, T2)) - \ All xs1 T1 \tyS All xs2 T2" - -lemma - shows "All {a, b} (Fun (Var a) (Var b)) \tyS All {b, a} (Fun (Var a) (Var b))" - apply(rule a1) - apply(simp add: alpha_gen) - apply(rule_tac x="0::perm" in exI) - apply(simp add: fresh_star_def) - done - -lemma - shows "All {a, b} (Fun (Var a) (Var b)) \tyS All {a, b} (Fun (Var b) (Var a))" - apply(rule a1) - apply(simp add: alpha_gen) - apply(rule_tac x="(atom a \ atom b)" in exI) - apply(simp add: fresh_star_def) - done - -lemma - shows "All {a, b, c} (Fun (Var a) (Var b)) \tyS All {a, b} (Fun (Var a) (Var b))" - apply(rule a1) - apply(simp add: alpha_gen) - apply(rule_tac x="0::perm" in exI) - apply(simp add: fresh_star_def) - done - -lemma - assumes a: "a \ b" - shows "\(All {a, b} (Fun (Var a) (Var b)) \tyS All {c} (Fun (Var c) (Var c)))" - using a - apply(clarify) - apply(erule alpha_tyS.cases) - apply(simp add: alpha_gen) - apply(erule conjE)+ - apply(erule exE) - apply(erule conjE)+ - apply(clarify) - apply(simp) - apply(simp add: fresh_star_def) - apply(auto) - done - - -end