diff -r 4b0563bc4b03 -r 7d8949da7d99 Nominal/Terms.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Terms.thy Thu Feb 25 07:48:33 2010 +0100 @@ -0,0 +1,1043 @@ +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 + +lemma alpha_bp_refl: "alpha_bp a a" +apply induct +apply (simp_all add: alpha1_inj) +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: alpha_bp_refl) +done + +lemma alpha_bp_eq: "alpha_bp = (op =)" +apply (rule ext)+ +apply (rule alpha_bp_eq_eq) +done + +lemma bv1_eqvt[eqvt]: + shows "(pi \ bv1 x) = bv1 (pi \ x)" + apply (induct x) + apply (simp_all add: atom_eqvt eqvts) + done + +lemma fv_rtrm1_eqvt[eqvt]: + "(pi\fv_rtrm1 t) = fv_rtrm1 (pi\t)" + "(pi\fv_bp b) = fv_bp (pi\b)" + apply (induct t and b) + apply (simp_all add: insert_eqvt atom_eqvt empty_eqvt union_eqvt Diff_eqvt bv1_eqvt) + done + +lemma alpha1_eqvt: + "t \1 s \ (pi \ t) \1 (pi \ s)" + "alpha_bp a b \ alpha_bp (pi \ a) (pi \ b)" + apply (induct t s and a b rule: alpha_rtrm1_alpha_bp.inducts) + apply (simp_all add:eqvts alpha1_inj) + apply (erule exE) + apply (rule_tac x="pi \ pia" in exI) + apply (simp add: alpha_gen) + apply(erule conjE)+ + apply(rule conjI) + apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) + apply(simp add: atom_eqvt Diff_eqvt insert_eqvt empty_eqvt fv_rtrm1_eqvt) + apply(rule conjI) + apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) + apply(simp add: atom_eqvt Diff_eqvt fv_rtrm1_eqvt insert_eqvt empty_eqvt) + apply(simp add: permute_eqvt[symmetric]) + apply (erule exE) + apply (erule exE) + apply (rule conjI) + apply (rule_tac x="pi \ pia" in exI) + apply (simp add: alpha_gen) + apply(erule conjE)+ + apply(rule conjI) + apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) + apply(simp add: fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) + apply(rule conjI) + apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) + apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) + apply(simp add: permute_eqvt[symmetric]) + apply (rule_tac x="pi \ piaa" in exI) + apply (simp add: alpha_gen) + apply(erule conjE)+ + apply(rule conjI) + apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) + apply(simp add: fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) + apply(rule conjI) + apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) + apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) + apply(simp add: permute_eqvt[symmetric]) + 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] + +instantiation trm1 and bp :: pt +begin + +quotient_definition + "permute_trm1 :: perm \ trm1 \ trm1" +is + "permute :: perm \ rtrm1 \ rtrm1" + +instance by default + (simp_all add: permute_rtrm1_permute_bp_zero[quot_lifted] permute_rtrm1_permute_bp_append[quot_lifted]) + +end + +lemmas + permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted] +and fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted] +and fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted] +and 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 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 + +lemma alpha4_eqvt: + "t \4 s \ (pi \ t) \4 (pi \ s)" + "a \4l b \ (pi \ a) \4l (pi \ b)" +sorry + +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: + "pi \ (rbv5 x) = rbv5 (pi \ x)" +sorry + +lemma fv_rtrm5_eqvt: + "pi \ (fv_rtrm5 x) = fv_rtrm5 (pi \ x)" +sorry + +lemma fv_rlts_eqvt: + "pi \ (fv_rlts x) = fv_rlts (pi \ x)" +sorry + +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 (erule exE)+ + apply(unfold alpha_gen) + apply (erule conjE)+ + apply (rule conjI) + apply (rule_tac x="x \ pi" in exI) + apply (rule conjI) + apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1]) + apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt) + apply(rule conjI) + apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1]) + apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt) + apply (subst permute_eqvt[symmetric]) + apply (simp) + apply (rule_tac x="x \ pia" in exI) + apply (rule conjI) + apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1]) + apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt) + apply(rule conjI) + apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1]) + apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt) + apply (subst permute_eqvt[symmetric]) + apply (simp) + 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 + +lemma alpha6_eqvt: + "xa \6 y \ (x \ xa) \6 (x \ y)" +sorry + +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