diff -r baa67b07f436 -r 4eaae533efc3 Nominal/Term5.thy --- a/Nominal/Term5.thy Wed Mar 10 12:48:38 2010 +0100 +++ b/Nominal/Term5.thy Wed Mar 10 12:48:55 2010 +0100 @@ -22,26 +22,16 @@ setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term5.rtrm5") 2 *} print_theorems - -local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5") [ - [ [], - [], - [(SOME @{term rbv5}, 0, 1)] ], - [ [], - []] ] *} +local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5") + [[[], [], [(SOME (@{term rbv5}, true), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *} print_theorems -(* 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 +thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases} ctxt)) ctxt)) *} +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} ctxt)) ctxt)) *} thm alpha5_inj lemma rbv5_eqvt[eqvt]: @@ -60,8 +50,15 @@ 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) + "alpha_rbv5 a b c \ True" +apply (induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) +apply (simp_all add: alpha5_inj) +apply (erule exE) +apply (rule_tac x="pi" in exI) +apply clarify +apply (simp add: alpha_gen fv_rtrm5_rlts_eqvt[symmetric] rbv5_eqvt[symmetric]) +apply (subst eqvts[symmetric]) +apply (subst eqvts[symmetric]) sorry lemma alpha5_equivp: @@ -84,25 +81,25 @@ |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons})) |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5})) |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts})) - |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5}))) + |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5})) + |> snd o (Quotient_Def.quotient_lift_const ("alpha_bv5", @{term alpha_rbv5}))) *} print_theorems lemma alpha5_rfv: - "(t \5 s \ fv_rtrm5 t = fv_rtrm5 s)" - "(l \l m \ fv_rlts l = fv_rlts m)" - apply(induct rule: alpha_rtrm5_alpha_rlts.inducts) + "(t \5 s \ fv_rtrm5 t = fv_rtrm5 s) \ (l \l m \ fv_rlts l = fv_rlts m) \ (alpha_rbv5 a b c \ True)" + apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) apply(simp_all) apply(simp add: alpha_gen) apply(erule conjE)+ apply(erule exE) apply(erule conjE)+ apply(simp_all) - done + sorry lemma bv_list_rsp: shows "x \l y \ rbv5 x = rbv5 y" - apply(induct rule: alpha_rtrm5_alpha_rlts.inducts(2)) + apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) apply(simp_all) apply(clarify) apply simp @@ -118,11 +115,22 @@ "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" + "(op = ===> alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5" apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp) apply (clarify) apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) - done - + defer + apply clarify + apply (erule alpha_rlts.cases) + apply (erule alpha_rlts.cases) + apply (simp_all) + defer + apply (erule alpha_rlts.cases) + apply (simp_all) + defer + apply clarify + apply (simp add: alpha5_inj) + sorry (* may be true? *) lemma shows "(alpha_rlts ===> op =) rbv5 rbv5" by (simp add: bv_list_rsp) @@ -147,11 +155,10 @@ 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] +lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] +lemmas bv5[simp] = rbv5.simps[quot_lifted] +lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] +lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] lemma lets_ok: "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" @@ -159,6 +166,7 @@ apply (rule_tac x="(x \ y)" in exI) apply (simp_all add: alpha_gen) apply (simp add: permute_trm5_lts fresh_star_def) +apply (metis flip_at_simps(1) supp_at_base supp_eqvt) done lemma lets_ok3: @@ -170,10 +178,12 @@ 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)))" + "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = + (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" apply (simp add: alpha5_INJ alpha_gen) -apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1)) +apply (rule_tac x="0::perm" in exI) +apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1) eqvts) +apply auto done lemma distinct_helper: @@ -192,7 +202,7 @@ (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) +apply (simp add: distinct_helper2 alpha5_INJ permute_trm5_lts) done end