--- 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:
"(\<exists>p. (bs, x) \<approx>lst (op=) f p (cs, y)) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>lst (op=) supp p (cs, y))"
-oops
+sorry
lemma Abs_eq_iff:
shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
@@ -49,7 +49,6 @@
and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
by (lifting alphas_abs)
-(*
lemma supp_fv:
"supp t = fv_trm t \<and> 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 \<Rightarrow> trm \<Rightarrow> trm"
consts perm_bn_assg :: "perm \<Rightarrow> assg \<Rightarrow> assg"
--- 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
--- 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
--- 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 <type>_perm whould be called permute_<type>.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'.