diff -r 2f1b00d83925 -r b679900fa5f6 Nominal/Manual/Term5.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Manual/Term5.thy Tue Mar 23 08:19:33 2010 +0100 @@ -0,0 +1,344 @@ +theory Term5 +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" +begin + +atom_decl name + +datatype rtrm5 = + rVr5 "name" +| rAp5 "rtrm5" "rtrm5" +| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)" +and rlts = + rLnil +| rLcons "name" "rtrm5" "rlts" + +primrec + rbv5 +where + "rbv5 rLnil = {}" +| "rbv5 (rLcons n t ltl) = {atom n} \ (rbv5 ltl)" + + +setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term5.rtrm5") 2 *} +print_theorems + +local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5") + [[[], [], [(SOME (@{term rbv5}, true), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *} +print_theorems + +notation + alpha_rtrm5 ("_ \5 _" [100, 100] 100) and + alpha_rlts ("_ \l _" [100, 100] 100) +thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros + +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} ctxt)) ctxt)) *} +thm alpha5_inj + +lemma rbv5_eqvt[eqvt]: + "pi \ (rbv5 x) = rbv5 (pi \ x)" + apply (induct x) + apply (simp_all add: eqvts atom_eqvt) + done + +lemma fv_rtrm5_rlts_eqvt[eqvt]: + "pi \ (fv_rtrm5 x) = fv_rtrm5 (pi \ x)" + "pi \ (fv_rlts l) = fv_rlts (pi \ l)" + apply (induct x and l) + apply (simp_all add: eqvts atom_eqvt) + done + +(*lemma alpha5_eqvt: + "(xa \5 y \ (p \ xa) \5 (p \ y)) \ + (xb \l ya \ (p \ xb) \l (p \ ya)) \ + (alpha_rbv5 b c \ alpha_rbv5 (p \ b) (p \ c))" +apply (tactic {* alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} @{context} 1 *}) +done*) + +local_setup {* +(fn ctxt => snd (Local_Theory.note ((@{binding alpha5_eqvt}, []), +build_alpha_eqvts [@{term alpha_rtrm5}, @{term alpha_rlts}, @{term alpha_rbv5}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} ctxt 1) ctxt) ctxt)) *} +print_theorems + +lemma alpha5_reflp: +"y \5 y \ (x \l x \ alpha_rbv5 x x)" +apply (rule rtrm5_rlts.induct) +apply (simp_all add: alpha5_inj) +apply (rule_tac x="0::perm" in exI) +apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm) +done + +lemma alpha5_symp: +"(a \5 b \ b \5 a) \ +(x \l y \ y \l x) \ +(alpha_rbv5 x y \ alpha_rbv5 y x)" +apply (tactic {* symp_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms alpha5_eqvt} @{context} 1 *}) +done + +lemma alpha5_symp1: +"(a \5 b \ b \5 a) \ +(x \l y \ y \l x) \ +(alpha_rbv5 x y \ alpha_rbv5 y x)" +apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) +apply (simp_all add: alpha5_inj) +apply (erule exE) +apply (rule_tac x="- pi" in exI) +apply (simp add: alpha_gen) + apply(simp add: fresh_star_def fresh_minus_perm) +apply clarify +apply (rule conjI) +apply (rotate_tac 3) +apply (frule_tac p="- pi" in alpha5_eqvt(2)) +apply simp +apply (rule conjI) +apply (rotate_tac 5) +apply (frule_tac p="- pi" in alpha5_eqvt(1)) +apply simp +apply (rotate_tac 6) +apply simp +apply (drule_tac p1="- pi" in permute_eq_iff[symmetric,THEN iffD1]) +apply (simp) +done + +thm alpha_gen_sym[no_vars] +thm alpha_gen_compose_sym[no_vars] + +lemma tt: + "\R (- p \ x) y \ R (p \ y) x; (bs, x) \gen R f (- p) (cs, y)\ \ (cs, y) \gen R f p (bs, x)" + unfolding alphas + unfolding fresh_star_def + by (auto simp add: fresh_minus_perm) + +lemma alpha5_symp2: + shows "a \5 b \ b \5 a" + and "x \l y \ y \l x" + and "alpha_rbv5 x y \ alpha_rbv5 y x" +apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) +(* non-binding case *) +apply(simp add: alpha5_inj) +(* non-binding case *) +apply(simp add: alpha5_inj) +(* binding case *) +apply(simp add: alpha5_inj) +apply(erule exE) +apply(rule_tac x="- pi" in exI) +apply(rule tt) +apply(simp add: alphas) +apply(erule conjE)+ +apply(drule_tac p="- pi" in alpha5_eqvt(2)) +apply(drule_tac p="- pi" in alpha5_eqvt(2)) +apply(drule_tac p="- pi" in alpha5_eqvt(1)) +apply(drule_tac p="- pi" in alpha5_eqvt(1)) +apply(simp) +apply(simp add: alphas) +apply(erule conjE)+ +apply metis +(* non-binding case *) +apply(simp add: alpha5_inj) +(* non-binding case *) +apply(simp add: alpha5_inj) +(* non-binding case *) +apply(simp add: alpha5_inj) +(* non-binding case *) +apply(simp add: alpha5_inj) +done + +lemma alpha5_transp: +"(a \5 b \ (\c. b \5 c \ a \5 c)) \ +(x \l y \ (\z. y \l z \ x \l z)) \ +(alpha_rbv5 k l \ (\m. alpha_rbv5 l m \ alpha_rbv5 k m))" +(*apply (tactic {* transp_tac @{context} @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} [] @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{thms alpha5_eqvt} 1 *})*) +apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) +apply (rule_tac [!] allI) +apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) +apply (simp_all add: alpha5_inj) +apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) +apply (simp_all add: alpha5_inj) +apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) +apply (simp_all add: alpha5_inj) +defer +apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) +apply (simp_all add: alpha5_inj) +apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) +apply (simp_all add: alpha5_inj) +apply (tactic {* eetac @{thm exi_sum} @{context} 1 *}) +(* HERE *) +(* +apply(rule alpha_gen_trans) +thm alpha_gen_trans +defer +apply (simp add: alpha_gen) +apply clarify +apply(simp add: fresh_star_plus) +apply (rule conjI) +apply (erule_tac x="- pi \ rltsaa" in allE) +apply (rotate_tac 5) +apply (drule_tac p="- pi" in alpha5_eqvt(2)) +apply simp +apply (drule_tac p="pi" in alpha5_eqvt(2)) +apply simp +apply (erule_tac x="- pi \ rtrm5aa" in allE) +apply (rotate_tac 7) +apply (drule_tac p="- pi" in alpha5_eqvt(1)) +apply simp +apply (rotate_tac 3) +apply (drule_tac p="pi" in alpha5_eqvt(1)) +apply simp +done +*) +sorry + +lemma alpha5_equivp: + "equivp alpha_rtrm5" + "equivp alpha_rlts" + unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def + apply (simp_all only: alpha5_reflp) + apply (meson alpha5_symp alpha5_transp) + apply (meson alpha5_symp alpha5_transp) + done + +quotient_type + trm5 = rtrm5 / alpha_rtrm5 +and + lts = rlts / alpha_rlts + by (auto intro: alpha5_equivp) + +local_setup {* +(fn ctxt => ctxt + |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5})) + |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5})) + |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5})) + |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil})) + |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons})) + |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5})) + |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts})) + |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5})) + |> snd o (Quotient_Def.quotient_lift_const ("alpha_bv5", @{term alpha_rbv5}))) +*} +print_theorems + +lemma alpha5_rfv: + "(t \5 s \ fv_rtrm5 t = fv_rtrm5 s)" + "(l \l m \ fv_rlts l = fv_rlts m)" + "(alpha_rbv5 b c \ True)" + apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) + apply(simp_all add: eqvts) + apply(simp add: alpha_gen) + apply(clarify) + apply blast +done + +lemma bv_list_rsp: + shows "x \l y \ rbv5 x = rbv5 y" + apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) + apply(simp_all) + apply(clarify) + apply simp + done + +local_setup {* snd o Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel @{context} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases}) [(@{thms rtrm5.distinct}, @{term alpha_rtrm5}), (@{thms rlts.distinct}, @{term alpha_rlts}), (@{thms rlts.distinct}, @{term alpha_rbv5})]))) *} +print_theorems + +local_setup {* snd o Local_Theory.note ((@{binding alpha_bn_rsp}, []), prove_alpha_bn_rsp [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts} @{thms rtrm5.exhaust rlts.exhaust} @{thms alpha5_inj alpha_dis} @{thms alpha5_equivp} @{context} (@{term alpha_rbv5}, 1)) *} +thm alpha_bn_rsp + +lemma [quot_respect]: + "(alpha_rlts ===> op =) fv_rlts fv_rlts" + "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5" + "(alpha_rlts ===> op =) rbv5 rbv5" + "(op = ===> alpha_rtrm5) rVr5 rVr5" + "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5" + "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" + "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" + "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" + "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" + "(alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5" + apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha_bn_rsp) + apply (clarify) + apply (rule_tac x="0" in exI) + apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) +done + + +lemma + shows "(alpha_rlts ===> op =) rbv5 rbv5" + by (simp add: bv_list_rsp) + +lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted] + +instantiation trm5 and lts :: pt +begin + +quotient_definition + "permute_trm5 :: perm \ trm5 \ trm5" +is + "permute :: perm \ rtrm5 \ rtrm5" + +quotient_definition + "permute_lts :: perm \ lts \ lts" +is + "permute :: perm \ rlts \ rlts" + +instance by default + (simp_all add: permute_rtrm5_permute_rlts_zero[quot_lifted] permute_rtrm5_permute_rlts_append[quot_lifted]) + +end + +lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] +lemmas bv5[simp] = rbv5.simps[quot_lifted] +lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] +lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen2, unfolded alpha_gen, quot_lifted, folded alpha_gen2, folded alpha_gen] +lemmas alpha5_DIS = alpha_dis[quot_lifted] + +(* why is this not in Isabelle? *) +lemma set_sub: "{a, b} - {b} = {a} - {b}" +by auto + +lemma lets_bla: + "x \ z \ y \ z \ x \ y \(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) \ (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))" +apply (simp only: alpha5_INJ bv5) +apply simp +apply (rule allI) +apply (simp_all add: alpha_gen) +apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ eqvts) +apply (rule impI) +apply (rule impI) +apply (rule impI) +apply (simp add: set_sub) +done + +lemma lets_ok: + "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" +thm alpha5_INJ +apply (simp only: alpha5_INJ) +apply (rule_tac x="(x \ y)" in exI) +apply (simp_all add: alpha_gen) +apply (simp add: permute_trm5_lts fresh_star_def) +apply (simp add: eqvts) +done + +lemma lets_ok3: + "x \ y \ + (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \ + (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" +apply (simp add: permute_trm5_lts alpha_gen alpha5_INJ) +done + + +lemma lets_not_ok1: + "x \ y \ + (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \ + (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" +apply (simp add: alpha5_INJ alpha_gen) +apply (simp add: permute_trm5_lts eqvts) +apply (simp add: alpha5_INJ) +done + +lemma lets_nok: + "x \ y \ x \ z \ z \ y \ + (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \ + (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" +apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def) +apply (simp add: alpha5_DIS alpha5_INJ permute_trm5_lts) +done + +end