diff -r 6d140b2c751f -r f7aca5601279 Nominal/Terms.thy --- a/Nominal/Terms.thy Thu Feb 25 14:20:10 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1049 +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 - -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 - -ML {* -fun build_eqvts bind funs perms simps induct ctxt = -let - val pi = Free ("p", @{typ perm}); - val types = map (domain_type o fastype_of) funs; - val indnames = Name.variant_list ["pi"] (Datatype_Prop.make_tnames (map body_type types)); - val args = map Free (indnames ~~ types); - val perm_at = @{term "permute :: perm \ atom set \ atom set"} - fun eqvtc (fnctn, (arg, perm)) = - HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm $ pi $ arg))) - val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms)))) - fun tac _ = (indtac induct indnames THEN_ALL_NEW - (asm_full_simp_tac (HOL_ss addsimps - (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))) 1 - val thm = Goal.prove ctxt ("p" :: indnames) [] gl tac - val thms = HOLogic.conj_elims thm -in - Local_Theory.note ((bind, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt -end -*} - -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} -*} - -ML {* -fun build_alpha_eqvts funs perms simps induct ctxt = -let - val pi = Free ("p", @{typ perm}); - val types = map (domain_type o fastype_of) funs; - val indnames = Name.variant_list ["pi"] (Datatype_Prop.make_tnames (map body_type types)); - val indnames2 = Name.variant_list ("pi" :: indnames) (Datatype_Prop.make_tnames (map body_type types)); - val args = map Free (indnames ~~ types); - val args2 = map Free (indnames2 ~~ types); - fun eqvtc ((alpha, perm), (arg, arg2)) = - HOLogic.mk_imp (alpha $ arg $ arg2, - (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2))) - val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2)))) - fun tac _ = (rtac induct THEN_ALL_NEW - (asm_full_simp_tac (HOL_ss addsimps - (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))) - THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW - (etac @{thm alpha_gen_compose_eqvt})) THEN_ALL_NEW - (asm_full_simp_tac (HOL_ss addsimps - (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))) -) 1 - val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac -in - map (fn x => mp OF [x]) (HOLogic.conj_elims thm) -end -*} - -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 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 - -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