# HG changeset patch # User Cezary Kaliszyk # Date 1268848403 -3600 # Node ID 9923b2cee778496a649ad17bb074d1aab379d006 # Parent b9caceeec805608ab2fb86482619aa6a1e36f033# Parent f86710d35146b841ae29a4bc47bbc9017d473faf merge diff -r b9caceeec805 -r 9923b2cee778 IsaMakefile --- 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 diff -r b9caceeec805 -r 9923b2cee778 Nominal/Parser.thy --- 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 {* diff -r b9caceeec805 -r 9923b2cee778 Nominal/ROOT.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 diff -r b9caceeec805 -r 9923b2cee778 Nominal/Test.thy --- 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 \ T) \ infinite S \ 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 "\a. a \ x \ sort_of a = s" +using obtain_atom[OF fin] +unfolding fresh_def +by blast + +lemma + assumes a0: "finite (supp c)" + and a1: "\name c. P c (Vr name)" + and a2: "\lm_raw1 lm_raw2 c. \\d. P d lm_raw1; \d. P d lm_raw2\ \ P c (Ap lm_raw1 lm_raw2)" + and a3: "\name lm_raw c. \\d. P d lm_raw\ \ P c (Lm name lm_raw)" + shows "P c lm" +proof - + have "\p c. P c (p \ 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 "\new::name. (atom new) \ (c, Lm (p \ name) (p \ lm_raw)) + \ sort_of (atom new) = sort_of (atom name)") + apply(erule exE) + apply(rule_tac t="(p \ Lm name lm_raw)" and + s="((((atom (p \ name)) \ (atom new)) + p) \ 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 \ name) \ atom new) + p" in meta_spec) + apply(simp) + sorry (* use at_set_avoiding *) + then have "P c (0 \ 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 \ T) \ infinite S \ infinite T" - by simp - lemma bi_eqvt: shows "(p \ (bi b)) = bi (p \ 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 \ supp s) supports (APP t s)" - "(supp (atom a) \ supp t) supports (LAM a t)" - "(supp b \ supp t) supports (LET b t)" - "(supp (atom a) \ 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' = diff -r b9caceeec805 -r 9923b2cee778 Paper/Paper.thy --- 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 diff -r b9caceeec805 -r 9923b2cee778 Paper/ROOT.ML --- 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 diff -r b9caceeec805 -r 9923b2cee778 Paper/document/root.tex --- 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