# HG changeset patch # User Cezary Kaliszyk # Date 1333463936 -7200 # Node ID 7ad3b1421b82a99e5ec9c73ec2c69aa791ef661d # Parent 78c0a707fb2db911ce4a5f5078a35200296c63ec A recursive function over let-recs with eqvt problems diff -r 78c0a707fb2d -r 7ad3b1421b82 Nominal/Ex/LetRecFunNo.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Ex/LetRecFunNo.thy Tue Apr 03 16:38:56 2012 +0200 @@ -0,0 +1,299 @@ +theory Let +imports "../Nominal2" +begin + +atom_decl name + +nominal_datatype trm = + Var "name" +| App "trm" "trm" +| Let as::"assn" t::"trm" binds "bn as" in as t +and assn = + ANil +| ACons "name" "trm" "assn" +binder + bn +where + "bn ANil = []" +| "bn (ACons x t as) = (atom x) # (bn as)" + +nominal_primrec substrec where + "substrec fa fl fd y z (Var x) = (if (y = x) then z else (Var x))" +| "substrec fa fl fd y z (App l r) = fa l r" +| "(set (bn as) \* (Let as t, y, z) \ (\bs s. set (bn bs) \* (Let bs s, y, z) \ Let as t = Let bs s \ fl as t = fl bs s)) \ + substrec fa fl fd y z (Let as t) = fl as t" +| "(set (bn as) \* (Let as t, y, z) \ \(\bs s. set (bn bs) \* (Let bs s, y, z) \ Let as t = Let bs s \ fl as t = fl bs s)) \ + substrec fa fl fd y z (Let as t) = fd" + unfolding eqvt_def substrec_graph_def + apply (rule, perm_simp, rule, rule) + apply (case_tac x) + apply (rule_tac y="f" and c="(f, d, e)" in trm_assn.strong_exhaust(1)) + apply metis + apply metis + apply (thin_tac "\fa fl fd y z xa. x = (fa, fl, fd, y, z, Var xa) \ P") + apply (thin_tac "\fa fl fd y z l r. x = (fa, fl, fd, y, z, App l r) \ P") + apply (drule_tac x="assn" in meta_spec)+ + apply (drule_tac x="trm" in meta_spec)+ + apply (drule_tac x="d" in meta_spec)+ + apply (drule_tac x="e" in meta_spec)+ + apply (drule_tac x="b" in meta_spec)+ + apply (drule_tac x="a" in meta_spec)+ + apply (drule_tac x="c" in meta_spec)+ + apply (case_tac "(\bs s. + set (bn bs) \* (Let bs s, d, e) \ + Let.Let assn trm = Let.Let bs s \ b assn trm = b bs s)") + apply simp + apply (thin_tac "set (bn assn) \* (Let assn trm, d, e) \ + (\bs s. + set (bn bs) \* (Let bs s, d, e) \ + Let.Let assn trm = Let.Let bs s \ b assn trm = b bs s) \ + x = (a, b, c, d, e, Let.Let assn trm) \ P") + apply simp + apply simp_all + apply clarify + apply metis + done +termination (eqvt) by lexicographic_order + +nominal_primrec substarec :: "(name \ trm \ assn \ assn) \ assn \ assn" where + "substarec fac ANil = ANil" +| "substarec fac (ACons x t as) = fac x t as" + unfolding eqvt_def substarec_graph_def + apply (rule, perm_simp, rule, rule) + apply (case_tac x) + apply (rule_tac y="b" in trm_assn.exhaust(2)) + apply auto + done +termination (eqvt) by lexicographic_order + +lemma [fundef_cong]: + "(\t1 t2. t = App t1 t2 \ fa t1 t2 = fa' t1 t2) \ + (\as s. t = Let as s \ fl as s = fl' as s) \ + substrec fa fl fd y z t = substrec fa' fl' fd y z t" + apply (rule_tac y="t" and c="(t, y, z)" in trm_assn.strong_exhaust(1)) + apply auto + apply (case_tac "(\bs s. set (bn bs) \* (Let bs s, y, z) \ Let assn trm = Let bs s \ fl assn trm = fl bs s)") + apply (subst substrec.simps(3)) apply simp + apply (subst substrec.simps(3)) apply simp + apply metis + apply (subst substrec.simps(4)) apply simp + apply (subst substrec.simps(4)) apply simp_all + done + +lemma [fundef_cong]: + "(\x s as. t = ACons x s as \ fac x s as = fac' x s as) \ + substarec fac t = substarec fac' t" + by (rule_tac y="t" in trm_assn.exhaust(2)) simp_all + +function + subst :: "name \ trm \ trm \ trm" +and substa :: "name \ trm \ assn \ assn" +where + [simp del]: "subst y z t = substrec + (\l r. App (subst y z l) (subst y z r)) + (\as t. Let (substa y z as) (subst y z t)) + (Let (ACons y (Var y) ANil) (Var y)) y z t" +| [simp del]: "substa y z t = substarec + (\x t as. ACons x (subst y z t) (substa y z as)) t" + by pat_completeness auto + +termination by lexicographic_order + +lemma testl: + assumes a: "\y. f x = Inl y" + shows "(p \ (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \ f) (p \ x))" +using a +apply clarify +apply(frule_tac p="p" in permute_boolI) +apply(simp (no_asm_use) only: eqvts) +apply(subst (asm) permute_fun_app_eq) +back +apply(simp) +done + +lemma testr: + assumes a: "\y. f x = Inr y" + shows "(p \ (Sum_Type.Projr (f x))) = Sum_Type.Projr ((p \ f) (p \ x))" +using a +apply clarify +apply(frule_tac p="p" in permute_boolI) +apply(simp (no_asm_use) only: eqvts) +apply(subst (asm) permute_fun_app_eq) +back +apply(simp) +done + +lemma permute_move: "p \ x = y \ x = -p \ y" + by (metis eqvt_bound unpermute_def) + +lemma "subst_substa_graph x t \ subst_substa_graph (p \ x) (p \ t)" +proof (induct arbitrary: p rule: subst_substa_graph.induct) +fix f y z t p +assume a: "\t1 t2 p. t = App t1 t2 \ subst_substa_graph (p \ Inl (y, z, t1)) (p \ f (Inl (y, z, t1)))" + and b: "\t1 t2 p. t = App t1 t2 \ subst_substa_graph (p \ Inl (y, z, t2)) (p \ f (Inl (y, z, t2)))" + and c: "\as s p. t = Let.Let as s \ subst_substa_graph (p \ Inr (y, z, as)) (p \ f (Inr (y, z, as)))" + and d: "\as s p. t = Let.Let as s \ subst_substa_graph (p \ Inl (y, z, s)) (p \ f (Inl (y, z, s)))" + then show "subst_substa_graph (p \ Inl (y, z, t)) + (p \ Inl (substrec + (\l r. App (Sum_Type.Projl (f (Inl (y, z, l)))) + (Sum_Type.Projl (f (Inl (y, z, r))))) + (\as t. Let.Let (Sum_Type.Projr (f (Inr (y, z, as)))) + (Sum_Type.Projl (f (Inl (y, z, t))))) + (Let.Let (ACons y (Var y) ANil) (Var y)) y z t))" + proof (rule_tac y="t" and c="(t, y, z)" in trm_assn.strong_exhaust(1)) + fix name + assume "t = Var name" + then show ?thesis + apply (simp add: eqvts split del: if_splits) + apply (simp only: trm_assn.perm_simps) + apply (rule subst_substa_graph.intros(1)[of "Var (p \ name)" "p \ y" "p \ z", simplified]) + by simp_all + next + fix trm1 trm2 + assume e: "t = App trm1 trm2" + then show ?thesis + apply (simp add: eqvts) + apply (subst testl) back + apply (rule subst_substa_graph.cases[OF a[OF e, of 0, simplified]]) + apply metis apply simp + apply (subst testl) back + apply (rule subst_substa_graph.cases[OF b[OF e, of 0, simplified]]) + apply metis apply (simp add: eqvts) + apply (simp only: Inl_eqvt) apply simp + apply (rule subst_substa_graph.intros(1)[of "App (p \ trm1) (p \ trm2)" "p \ y" "p \ z", simplified]) + apply simp_all apply clarify + using a[OF e, simplified Inl_eqvt, simplified] + apply (metis (lifting) Inl_eqvt permute_fun_app_eq permute_prod.simps) + apply clarify + using b[OF e, simplified Inl_eqvt, simplified] + by (metis (lifting) Inl_eqvt permute_fun_app_eq permute_prod.simps) + next + fix assn trm + assume e: "t = Let.Let assn trm" and f: "set (bn assn) \* (t, y, z)" + then show ?thesis + apply (simp add: eqvts) + apply (simp only: permute_fun_def) + apply (simp only: eqvts permute_minus_cancel) + apply (case_tac "(\bs s. set (bn bs) \* (Let.Let bs s, p \ y, p \ z) \ + Let.Let (p \ assn) (p \ trm) = Let.Let bs s \ + Let.Let (p \ Sum_Type.Projr (f (Inr (y, z, - p \ p \ assn)))) + (p \ Sum_Type.Projl (f (Inl (y, z, - p \ p \ trm)))) = + Let.Let (p \ Sum_Type.Projr (f (Inr (y, z, - p \ bs)))) + (p \ Sum_Type.Projl (f (Inl (y, z, - p \ s)))))") + prefer 2 + apply (subst substrec.simps(4)) + apply rule + apply (simp add: fresh_star_Pair) + apply (intro conjI) + apply (metis fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4) trm_assn.perm_simps(3)) + apply (metis (lifting) fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4)) + apply (metis (lifting) fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4)) + apply assumption + prefer 2 + apply (subst substrec.simps(3)) + apply rule + apply (simp add: fresh_star_Pair) + apply (intro conjI) + apply (metis fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4) trm_assn.perm_simps(3)) + apply (metis (lifting) fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4)) + apply (metis (lifting) fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4)) + apply assumption +(* The following subgoal is motivated by: + thm subst_substa_graph.intros(1)[of "Let (p \ assn) (p \ trm)" "p \ y" "p \ z" "(p \ f)", simplified]*) + apply (subgoal_tac "subst_substa_graph (Inl (p \ y, p \ z, Let.Let (p \ assn) (p \ trm))) + (Inl (substrec + (\l r. App (Sum_Type.Projl ((p \ f) (Inl (p \ y, p \ z, l)))) + (Sum_Type.Projl ((p \ f) (Inl (p \ y, p \ z, r))))) + (\as t. Let.Let (Sum_Type.Projr ((p \ f) (Inr (p \ y, p \ z, as)))) + (Sum_Type.Projl ((p \ f) (Inl (p \ y, p \ z, t))))) + (Let.Let (ACons (p \ y) (Var (p \ y)) ANil) (Var (p \ y))) (p \ y) (p \ z) + (Let.Let (p \ assn) (p \ trm))))") + apply (subst (asm) substrec.simps(3)) + apply rule + apply (simp add: fresh_star_Pair) + apply (intro conjI) + apply (metis fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4) trm_assn.perm_simps(3)) + apply (metis (lifting) fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4)) + apply (metis (lifting) fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4)) + (* We don't have equivariance of Projl/Projr at the arbitrary 'bs' point *) + defer + apply (subst testr) back + apply (rule subst_substa_graph.cases[OF c[OF e, of 0, simplified]]) + apply simp apply simp + apply (subst testl) back + apply (rule subst_substa_graph.cases[OF d[OF e, of 0, simplified]]) + apply simp apply simp apply simp + apply (rule subst_substa_graph.intros(1)[of "Let (p \ assn) (p \ trm)" "p \ y" "p \ z" "(p \ f)", simplified]) + apply simp apply simp (* These two should follow by d for arbitrary 'as' point *) + defer defer + sorry + qed + next + fix f y z t p + show "subst_substa_graph (p \ Inr (y, z, t)) (p \ Inr (substarec (\x t as. ACons + x (Sum_Type.Projl (f (Inl (y, z, t)))) (Sum_Type.Projr (f (Inr (y, z, as))))) t))" + sorry + qed + +(* Will follow from above and accp *) +lemma [eqvt]: + "p \ (subst y z t) = subst (p \ y) (p \ z) (p \ t)" + "p \ (substa y z t2) = substa (p \ y) (p \ z) (p \ t2)" + sorry + +lemma substa_simps[simp]: + "substa y z ANil = ANil" + "substa y z (ACons x t as) = ACons x (subst y z t) (substa y z as)" + apply (subst substa.simps) apply (subst substarec.simps) apply rule + apply (subst substa.simps) apply (subst substarec.simps) apply rule + done + +lemma bn_substa: "bn (substa y z t) = bn t" + by (induct t rule: trm_assn.inducts(2)) (simp_all add: trm_assn.bn_defs) + +lemma fresh_fun_eqvt_app3: + assumes e: "eqvt f" + shows "\a \ x; a \ y; a \ z\ \ a \ f x y z" + using fresh_fun_eqvt_app[OF e] fresh_fun_app by (metis (lifting, full_types)) + +lemma + "subst y z (Var x) = (if (y = x) then z else (Var x))" + "subst y z (App l r) = App (subst y z l) (subst y z r)" + "set (bn as) \* (Let as t, y, z) \ subst y z (Let as t) = Let (substa y z as) (subst y z t)" + apply (subst subst.simps) apply (subst substrec.simps) apply rule + apply (subst subst.simps) apply (subst substrec.simps) apply rule + apply (subst subst.simps) apply (subst substrec.simps) apply auto + apply (subst (asm) Abs_eq_iff2) + apply clarify + apply (simp add: alphas bn_substa) + apply (rule_tac s="p \ ([bn as]lst. (substa y z as, subst y z t))" in trans) + apply (rule sym) + defer + apply (simp add: eqvts) + apply (subgoal_tac "supp p \* y") + apply (subgoal_tac "supp p \* z") + apply (simp add: perm_supp_eq) + apply (simp add: fresh_Pair fresh_star_def) + apply blast + apply (simp add: fresh_Pair fresh_star_def) + apply blast + apply (rule perm_supp_eq) + apply (simp add: fresh_star_Pair) + apply (simp add: fresh_star_def Abs_fresh_iff) + apply (auto) + apply (simp add: bn_substa fresh_Pair) + apply (rule) + apply (rule fresh_fun_eqvt_app3[of substa]) + apply (simp add: eqvt_def eqvts_raw) + apply (metis (lifting) Diff_partition Un_iff) + apply (metis (lifting) Diff_partition Un_iff) + apply (simp add: fresh_def trm_assn.supp) + apply (metis (lifting) DiffI UnI1 supp_Pair) + apply (rule fresh_fun_eqvt_app3[of subst]) + apply (simp add: eqvt_def eqvts_raw) + apply (metis (lifting) Diff_partition Un_iff) + apply (metis (lifting) Diff_partition Un_iff) + apply (simp add: fresh_def trm_assn.supp) + by (metis Diff_iff Un_iff supp_Pair) + +end