# HG changeset patch # User Christian Urban # Date 1283055280 -28800 # Node ID 39f8d405d7a2a2a386a592198387e315e1260c5f # Parent d2e929f51fa9457dbe37c0e7f1f93a073fb41d05 updated todos diff -r d2e929f51fa9 -r 39f8d405d7a2 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Sun Aug 29 01:45:07 2010 +0800 +++ b/Nominal/Ex/SingleLet.thy Sun Aug 29 12:14:40 2010 +0800 @@ -41,7 +41,7 @@ lemma test: "(\p. (bs, x) \lst (op=) f p (cs, y)) \ (\p. (bs, x) \lst (op=) supp p (cs, y))" -oops +sorry lemma Abs_eq_iff: shows "Abs bs x = Abs cs y \ (\p. (bs, x) \gen (op =) supp p (cs, y))" @@ -49,7 +49,6 @@ and "Abs_lst bsl x = Abs_lst csl y \ (\p. (bsl, x) \lst (op =) supp p (csl, y))" by (lifting alphas_abs) -(* lemma supp_fv: "supp t = fv_trm t \ supp b = fv_bn b" apply(rule single_let.induct) @@ -65,19 +64,17 @@ apply(subgoal_tac "supp (Lam name trm) = supp (Abs_lst [atom name] trm)") apply(simp only: single_let.fv_defs) apply(simp only: supp_abs) +apply(simp) apply(simp (no_asm) only: supp_def) apply(simp only: single_let.perm_simps) apply(simp only: single_let.eq_iff) +apply(simp only: permute_abs atom_eqvt permute_list.simps) +apply(simp only: Abs_eq_iff) apply(subst test) -apply(simp only: Abs_eq_iff[symmetric]) -apply(simp only: alphas_abs[symmetric]) -apply(simp only: eqvts) -thm Abs_eq_iff -apply(simp only: alphas) +apply(rule refl) sorry -*) + (* - consts perm_bn_trm :: "perm \ trm \ trm" consts perm_bn_assg :: "perm \ assg \ assg" diff -r d2e929f51fa9 -r 39f8d405d7a2 PAPER-TODO --- a/PAPER-TODO Sun Aug 29 01:45:07 2010 +0800 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,17 +0,0 @@ -_{res} -> _{\textrm{res}} etc.; same for =^{def}? - -Nominal Isabelle view, rather than functional programming view -(e.g. first sentence of Abstract and Intro) - - -:: for cons might need some explanations, esp. that it's also used later -next to labels in nominal types (e.g. x::name t::lam). - - -Ott-tool -> Ott tool (throughout) - -I didn't quite get top of second column, p. 6 - -the equation in the first actuall bullet on p. 8 lacks it =? - -missing v. spaces, top of 2nd col p. 8 \ No newline at end of file diff -r d2e929f51fa9 -r 39f8d405d7a2 README --- a/README Sun Aug 29 01:45:07 2010 +0800 +++ b/README Sun Aug 29 12:14:40 2010 +0800 @@ -1,7 +1,21 @@ This repository contain a new implementation of Nominal Isabelle. + Subdirectories: +=============== + +Nominal ... main files for new Nominal Isabelle + +Nominal/Ex ... examples for new implementation + +Nominal-General . implementation of the abstract nominal theory + + + + +Outher Subdirectories: +====================== Attic ... old version of the quotient package (is now part of the Isabelle distribution) @@ -9,15 +23,9 @@ Literature ... some relevant papers about binders and Core-Haskell -Nominal-General . implementation of the abstract nominal theory - -Nominal ... main files for new Nominal Isabelle - -Nominal/Ex ... examples for new implementation - Paper ... submitted to POPL Pearl ... accepted at ITP Pearl-jv ... journal version -Quotient-Paper .. submitted to APLAS \ No newline at end of file +Quotient-Paper .. submitted to SAC \ No newline at end of file diff -r d2e929f51fa9 -r 39f8d405d7a2 TODO --- a/TODO Sun Aug 29 01:45:07 2010 +0800 +++ b/TODO Sun Aug 29 12:14:40 2010 +0800 @@ -1,16 +1,6 @@ -Automatically created functions: - - ty1_tyn.bn[simp] lifted equations for bn funs - ty1_tyn.fv[simp] lifted equations for fv funs - ty1_tyn.perm[simp] lifted permutation equations - ty1_tyn.distinct[simp] lifted distincts - ty1_tyn.eq_iff - ty1_tyn.induct - ty1_tyn.inducts - instance ty1 and tyn :: fs - ty1_tyn.supp empty when for too many bindings Parser should check that: + - types of bindings match types of binding functions - fsets are not bound in lst bindings - bound arguments are not datatypes @@ -18,22 +8,11 @@ Smaller things: -- lam.perm should be called permute_lam.simps (that is - the convention from Nominal2) - - maybe _perm whould be called permute_.simps; that would conform with the terminology in Nominal2 -- we also need to lift the size function for nominal - datatypes -- Abs.thy contains lemmas for equivariance of the alphas; - they are not yet used anywhere - -Bigger things: - -- Parser adds syntax for raw datatype, but should - add for lifted datatype. +Other: - nested recursion, like types "trm list" in a constructor @@ -43,21 +22,6 @@ - strong induction rules -- check support equations for more bindings per constructor - -- For binding functions that call other binding functions - the following are proved with cheat_tac: constr_rsp - - store information about defined nominal datatypes, so that it can be used to define new types that depend on these -- make parser aware of recursive and of different versions of abs - -Less important: - -- fv_rsp uses 'blast' to show goals of the type: - a u b = c u d ==> a u x u b = c u x u d - -When cleaning: - -- remove all 'PolyML.makestring'.