--- a/IsaMakefile Wed Mar 17 18:52:59 2010 +0100
+++ b/IsaMakefile Wed Mar 17 18:53:23 2010 +0100
@@ -27,7 +27,7 @@
$(LOG)/HOL-Nominal2-Paper.gz: Paper/ROOT.ML Paper/document/root.tex Paper/*.thy
@$(USEDIR) -D generated HOL Paper
- $(ISATOOL) document -o pdf Paper/generated
+ $(ISABELLE_TOOL) document -o pdf Paper/generated
@cp Paper/document.pdf paper.pdf
## clean
--- a/Nominal/Parser.thy Wed Mar 17 18:52:59 2010 +0100
+++ b/Nominal/Parser.thy Wed Mar 17 18:53:23 2010 +0100
@@ -276,14 +276,14 @@
*}
(* These 2 are critical, we don't know how to do it in term5 *)
-ML {* val cheat_fv_rsp = ref true *}
-ML {* val cheat_const_rsp = ref true *} (* For alpha_bn 0 and alpha_bn_rsp *)
+ML {* val cheat_fv_rsp = Unsynchronized.ref true *}
+ML {* val cheat_const_rsp = Unsynchronized.ref true *} (* For alpha_bn 0 and alpha_bn_rsp *)
-ML {* val cheat_equivp = ref true *}
+ML {* val cheat_equivp = Unsynchronized.ref true *}
(* Fixes for these 2 are known *)
-ML {* val cheat_fv_eqvt = ref true *} (* The tactic works, building the goal needs fixing *)
-ML {* val cheat_alpha_eqvt = ref true *} (* The tactic works, building the goal needs fixing *)
+ML {* val cheat_fv_eqvt = Unsynchronized.ref true *} (* The tactic works, building the goal needs fixing *)
+ML {* val cheat_alpha_eqvt = Unsynchronized.ref true *} (* The tactic works, building the goal needs fixing *)
ML {*
@@ -522,7 +522,7 @@
*}
ML {*
-val recursive = ref false
+val recursive = Unsynchronized.ref false
*}
ML {*
--- a/Nominal/ROOT.ML Wed Mar 17 18:52:59 2010 +0100
+++ b/Nominal/ROOT.ML Wed Mar 17 18:53:23 2010 +0100
@@ -5,6 +5,14 @@
"Nominal2_Eqvt",
"Nominal2_Atoms",
"Nominal2_Supp",
+ "Test"]
+
+(*
+no_document use_thys
+ ["Nominal2_Base",
+ "Nominal2_Eqvt",
+ "Nominal2_Atoms",
+ "Nominal2_Supp",
"Test",
"Term1",
"Term2",
@@ -17,3 +25,4 @@
"Term9",
"TySch",
"LFex"];
+*)
\ No newline at end of file
--- a/Nominal/Test.thy Wed Mar 17 18:52:59 2010 +0100
+++ b/Nominal/Test.thy Wed Mar 17 18:53:23 2010 +0100
@@ -6,10 +6,103 @@
atom_decl name
+(* maybe should be added to Infinite.thy *)
+lemma infinite_Un:
+ shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
+ by simp
+
ML {* val _ = cheat_alpha_eqvt := false *}
ML {* val _ = cheat_fv_eqvt := false *}
ML {* val _ = recursive := false *}
+nominal_datatype lm =
+ Vr "name"
+| Ap "lm" "lm"
+| Lm x::"name" l::"lm" bind x in l
+
+lemma finite_fv:
+ shows "finite (fv_lm t)"
+apply(induct t rule: lm_induct)
+apply(simp_all add: lm_fv)
+done
+
+lemma supp_fn:
+ shows "supp t = fv_lm t"
+apply(induct t rule: lm_induct)
+apply(simp_all add: lm_fv)
+apply(simp only: supp_def)
+apply(simp only: lm_perm)
+apply(simp only: lm_inject)
+apply(simp only: supp_def[symmetric])
+apply(simp only: supp_at_base)
+apply(simp (no_asm) only: supp_def)
+apply(simp only: lm_perm)
+apply(simp only: lm_inject)
+apply(simp only: de_Morgan_conj)
+apply(simp only: Collect_disj_eq)
+apply(simp only: infinite_Un)
+apply(simp only: Collect_disj_eq)
+apply(simp only: supp_def[symmetric])
+apply(rule_tac t="supp (Lm name lm_raw)" and s="supp (Abs {atom name} lm_raw)" in subst)
+apply(simp (no_asm) only: supp_def)
+apply(simp only: lm_perm)
+apply(simp only: permute_ABS)
+apply(simp only: lm_inject)
+apply(simp only: Abs_eq_iff)
+apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
+apply(simp only: alpha_gen)
+apply(simp only: supp_eqvt[symmetric])
+apply(simp only: eqvts)
+apply(simp only: supp_Abs)
+done
+
+lemmas supp_fn' = lm_fv[simplified supp_fn[symmetric]]
+
+lemma obtain_atom_ex:
+ assumes fin: "finite (supp x)"
+ shows "\<exists>a. a \<sharp> x \<and> sort_of a = s"
+using obtain_atom[OF fin]
+unfolding fresh_def
+by blast
+
+lemma
+ assumes a0: "finite (supp c)"
+ and a1: "\<And>name c. P c (Vr name)"
+ and a2: "\<And>lm_raw1 lm_raw2 c. \<lbrakk>\<And>d. P d lm_raw1; \<And>d. P d lm_raw2\<rbrakk> \<Longrightarrow> P c (Ap lm_raw1 lm_raw2)"
+ and a3: "\<And>name lm_raw c. \<lbrakk>\<And>d. P d lm_raw\<rbrakk> \<Longrightarrow> P c (Lm name lm_raw)"
+ shows "P c lm"
+proof -
+ have "\<And>p c. P c (p \<bullet> lm)"
+ apply(induct lm rule: lm_induct)
+ apply(simp only: lm_perm)
+ apply(rule a1)
+ apply(simp only: lm_perm)
+ apply(rule a2)
+ apply(assumption)
+ apply(assumption)
+ apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm_raw))
+ \<and> sort_of (atom new) = sort_of (atom name)")
+ apply(erule exE)
+ apply(rule_tac t="(p \<bullet> Lm name lm_raw)" and
+ s="((((atom (p \<bullet> name)) \<rightleftharpoons> (atom new)) + p) \<bullet> Lm name lm_raw)" in subst)
+ apply(simp)
+ apply(subst lm_perm)
+ apply(subst (2) lm_perm)
+ apply(rule swap_fresh_fresh)
+ apply(simp add: fresh_def)
+ apply(simp only: supp_fn')
+ apply(simp)
+ apply(simp add: fresh_Pair)
+ apply(simp add: lm_perm)
+ apply(rule a3)
+ apply(drule_tac x="(atom (p \<bullet> name) \<rightleftharpoons> atom new) + p" in meta_spec)
+ apply(simp)
+ sorry (* use at_set_avoiding *)
+ then have "P c (0 \<bullet> lm)" by blast
+ then show "P c lm" by simp
+qed
+
+
nominal_datatype lam =
VAR "name"
| APP "lam" "lam"
@@ -33,11 +126,6 @@
term "supp (x :: lam)"
-(* maybe should be added to Infinite.thy *)
-lemma infinite_Un:
- shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
- by simp
-
lemma bi_eqvt:
shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)"
by (rule eqvts)
@@ -107,44 +195,7 @@
thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]]
-lemma supports_lam_bp:
- "(supp (atom a)) supports (VAR a)"
- "(supp t \<union> supp s) supports (APP t s)"
- "(supp (atom a) \<union> supp t) supports (LAM a t)"
- "(supp b \<union> supp t) supports (LET b t)"
- "(supp (atom a) \<union> supp t) supports (BP a t)"
-apply -
-apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *})
-apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *})
-apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *})
-apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *})
-apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *})
-done
-
-lemma finite_supp_lam_bp:
- fixes lam::"lam"
- and bp::"bp"
- shows "finite (supp lam)"
- and "finite (supp bp)"
-apply(induct lam and bp rule: lam_bp_inducts)
-apply(rule supports_finite)
-apply(rule supports_lam_bp)
-apply(simp add: supp_atom)
-apply(rule supports_finite)
-apply(rule supports_lam_bp)
-apply(simp)
-apply(rule supports_finite)
-apply(rule supports_lam_bp)
-apply(simp add: supp_atom)
-apply(rule supports_finite)
-apply(rule supports_lam_bp)
-apply(simp)
-apply(rule supports_finite)
-apply(rule supports_lam_bp)
-apply(simp add: supp_atom)
-done
-
-
+ML {* val _ = cheat_alpha_eqvt := true *}
ML {* val _ = recursive := true *}
nominal_datatype lam' =
--- a/Paper/Paper.thy Wed Mar 17 18:52:59 2010 +0100
+++ b/Paper/Paper.thy Wed Mar 17 18:53:23 2010 +0100
@@ -7,10 +7,38 @@
section {* Introduction *}
text {*
- Here can come any text.
+
+ It has not yet fared so well in the POPLmark challenge
+ as the second part contain a formalisation of records
+ where ...
+
+ The difficulty can be appreciated by considering that the
+ definition given by Leroy in [] is incorrect (it omits a
+ side-condition).
+
+ Examples: type-schemes
+
+ Contributions: We provide definitions for when terms
+ involving general bindings are alpha-equivelent.
+*}
+
+text {* A Brief Overview about the Nominal Logic Work *}
+
+text {* Abstractions *}
+
+text {* Alpha-Equivalence and Free Variables *}
+
+
+text {*
+ Acknowledgements: We thank Andrew Pitts for the many discussions
+ about the topic. We thank Peter Sewell for making [] available
+ to us and explaining some of the finer points of the OTT tool.
+
*}
+
+
(*<*)
end
(*>*)
\ No newline at end of file
--- a/Paper/ROOT.ML Wed Mar 17 18:52:59 2010 +0100
+++ b/Paper/ROOT.ML Wed Mar 17 18:53:23 2010 +0100
@@ -1,3 +1,3 @@
-no_document use_thys ["../Quot/QuotMain"];
-
+quick_and_dirty := true;
+no_document use_thys ["../Nominal/Test"];
use_thys ["Paper"];
\ No newline at end of file
--- a/Paper/document/root.tex Wed Mar 17 18:52:59 2010 +0100
+++ b/Paper/document/root.tex Wed Mar 17 18:53:23 2010 +0100
@@ -1,6 +1,9 @@
-\documentstyle[epsf]{acmconf}
+\documentclass{acmconf}
\usepackage{isabelle,isabellesym}
+\ConferenceShortName{ICFP}
+\ConferenceName{International Conference on Functional Programming}
+
% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed
@@ -45,6 +48,7 @@
\newenvironment{example}[0]{\begin{Example} \it}{\end{Example}}
\newenvironment{proof-of}[1]{{\em Proof of #1:}}{}
+
\begin{document}
\title{\LARGE\bf General Binding Structures in Nominal Isabelle, or How to
@@ -53,7 +57,11 @@
\maketitle
\begin{abstract}
-TODO
+Nominal Isabelle is a definitional extension of the Isabelle/HOL
+theorem prover. It provides a reasoning infrastructure for formalisations
+of programming language calculi. In this paper we present an extension
+of Nominal Isabelle with general binding constructs. Such constructs
+are important in formalisation ...
\end{abstract}
% generated text of all theories