# HG changeset patch # User Christian Urban # Date 1273088396 -3600 # Node ID deb732753522c172d7fa20c96f2c3d8278baebeb # Parent c5d28ebf9dab3bd5a955056e933029f64d483b26# Parent e4e128e59c4142739ea4c8b05bb809f07cf2b543 merged diff -r e4e128e59c41 -r deb732753522 Nominal-General/Nominal2_Eqvt.thy --- a/Nominal-General/Nominal2_Eqvt.thy Wed May 05 09:23:10 2010 +0200 +++ b/Nominal-General/Nominal2_Eqvt.thy Wed May 05 20:39:56 2010 +0100 @@ -384,6 +384,12 @@ apply(perm_simp exclude: The) oops +lemma + fixes P :: "(('b \ bool) \ ('b::pt)) \ ('a::pt)" + shows "(p \ (P The)) = foo" +apply(perm_simp exclude: The) +oops + thm eqvts thm eqvts_raw diff -r e4e128e59c41 -r deb732753522 Nominal-General/nominal_eqvt.ML --- a/Nominal-General/nominal_eqvt.ML Wed May 05 09:23:10 2010 +0200 +++ b/Nominal-General/nominal_eqvt.ML Wed May 05 20:39:56 2010 +0100 @@ -75,9 +75,9 @@ *) fun transform_prem ctxt names thm = let - fun split_conj names (Const ("op &", _) $ p $ q) = - (case head_of p of - Const (name, _) => if name mem names then SOME q else NONE + fun split_conj names (Const ("op &", _) $ f1 $ f2) = + (case head_of f1 of + Const (name, _) => if name mem names then SOME f2 else NONE | _ => NONE) | split_conj _ _ = NONE; in @@ -102,6 +102,7 @@ SUBPROOF (fn {prems, context as ctxt, ...} => let val prems' = map (transform_prem ctxt pred_names) prems + val tac1 = resolve_tac prems' val tac2 = EVERY' [ rtac pi_intro_rule, eqvt_strict_tac ctxt perm_cancel pred_names, resolve_tac prems' ] diff -r e4e128e59c41 -r deb732753522 Nominal-General/nominal_permeq.ML --- a/Nominal-General/nominal_permeq.ML Wed May 05 09:23:10 2010 +0200 +++ b/Nominal-General/nominal_permeq.ML Wed May 05 20:39:56 2010 +0100 @@ -97,7 +97,7 @@ val term_insts = map SOME [p, f, x] in if has_bad_head bad_hds trm - then Conv.no_conv ctrm + then Conv.all_conv ctrm else Drule.instantiate' ty_insts term_insts @{thm eqvt_apply} end | _ => Conv.no_conv ctrm @@ -115,11 +115,11 @@ let fun msg trm = let - val hd = head_of trm + val hd = head_of trm in - if is_Const hd andalso (fst (dest_Const hd)) mem bad_hds then () - else (if strict_flag then error else warning) - ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm)) + if is_Const hd andalso (fst (dest_Const hd)) mem bad_hds then () + else (if strict_flag then error else warning) + ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm)) end val _ = case (term_of ctrm) of @@ -130,7 +130,7 @@ Conv.all_conv ctrm end -(* main conversion *) +(* main conversion *) fun eqvt_conv ctxt strict_flag user_thms bad_hds ctrm = let val first_conv_wrapper = @@ -150,13 +150,19 @@ ] ctrm end +(* the eqvt-tactics first eta-normalise goals in + order to avoid problems with inductions in the + equivaraince command. *) + (* raises an error if some permutations cannot be eliminated *) fun eqvt_strict_tac ctxt user_thms bad_hds = - CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt true user_thms bad_hds) ctxt) + CONVERSION (More_Conv.top_conv + (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt true user_thms bad_hds)) ctxt) (* prints a warning message if some permutations cannot be eliminated *) fun eqvt_tac ctxt user_thms bad_hds = - CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt false user_thms bad_hds) ctxt) + CONVERSION (More_Conv.top_conv + (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt false user_thms bad_hds)) ctxt) (* setup of the configuration value *) val setup = @@ -169,9 +175,7 @@ val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- (Scan.repeat (Args.const true))) [] -val args_parser = - add_thms_parser -- exclude_consts_parser || - exclude_consts_parser -- add_thms_parser >> swap +val args_parser = add_thms_parser -- exclude_consts_parser fun perm_simp_meth (thms, consts) ctxt = SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt thms consts)) diff -r e4e128e59c41 -r deb732753522 Nominal/Ex/Classical.thy --- a/Nominal/Ex/Classical.thy Wed May 05 09:23:10 2010 +0200 +++ b/Nominal/Ex/Classical.thy Wed May 05 20:39:56 2010 +0100 @@ -72,6 +72,7 @@ declare alpha_gen_eqvt[eqvt] equivariance alpha +equivariance alpha_trm_raw thm eqvts_raw diff -r e4e128e59c41 -r deb732753522 Nominal/Ex/ExCoreHaskell.thy --- a/Nominal/Ex/ExCoreHaskell.thy Wed May 05 09:23:10 2010 +0200 +++ b/Nominal/Ex/ExCoreHaskell.thy Wed May 05 20:39:56 2010 +0100 @@ -658,7 +658,7 @@ (* for the moment, we force it to be *) (*declare permute_pure[eqvt]*) -(*setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *} +(*setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *) thm eqvts thm eqvts_raw @@ -669,7 +669,7 @@ equivariance alpha_tkind_raw thm eqvts -thm eqvts_raw*) +thm eqvts_raw end diff -r e4e128e59c41 -r deb732753522 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Wed May 05 09:23:10 2010 +0200 +++ b/Nominal/Ex/SingleLet.thy Wed May 05 20:39:56 2010 +0100 @@ -27,12 +27,11 @@ ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *} thm trm_assg.fv[simplified trm_assg.supp(1-2)] -(* -setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *} declare permute_trm_raw_permute_assg_raw.simps[eqvt] declare alpha_gen_eqvt[eqvt] + equivariance alpha_trm_raw -*) + end diff -r e4e128e59c41 -r deb732753522 Pearl-jv/Paper.thy --- a/Pearl-jv/Paper.thy Wed May 05 09:23:10 2010 +0200 +++ b/Pearl-jv/Paper.thy Wed May 05 20:39:56 2010 +0100 @@ -44,30 +44,23 @@ section {* Introduction *} text {* - The purpose of Nominal Isabelle is to provide a proving infratructure - for conveninet reasoning about programming languages. At its core - Nominal Isabelle is based on nominal logic by Pitts at al - \cite{GabbayPitts02,Pitts03}. - - Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem - prover providing a proving infrastructure for convenient reasoning about - programming languages. At its core Nominal Isabelle is based on the nominal - logic work of Pitts et al \cite{GabbayPitts02,Pitts03}. The most basic - notion in this work is a sort-respecting permutation operation defined over - a countably infinite collection of sorted atoms. The atoms are used for - representing variables that might be bound. Multiple sorts are necessary for - being able to represent different kinds of variables. For example, in the - language Mini-ML there are bound term variables and bound type variables; - each kind needs to be represented by a different sort of atoms. - + Nominal Isabelle provides a proving infratructure for + convenient reasoning about programming languages. At its core Nominal + Isabelle is based on the nominal logic work by Pitts at al + \cite{GabbayPitts02,Pitts03}. The most basic notion in this work + is a sort-respecting permutation operation defined over a countably infinite + collection of sorted atoms. The atoms are used for representing variables + that might be bound. Multiple sorts are necessary for being able to + represent different kinds of variables. For example, in the language Mini-ML + there are bound term variables and bound type variables; each kind needs to + be represented by a different sort of atoms. Unfortunately, the type system of Isabelle/HOL is not a good fit for the way atoms and sorts are used in the original formulation of the nominal logic work. - Therefore it was decided in earlier versions of Nominal Isabelle to use a - separate type for each sort of atoms and let the type system enforce the - sort-respecting property of permutations. Inspired by the work on nominal - unification \cite{UrbanPittsGabbay04}, it seemed best at the time to also - implement permutations concretely as lists of pairs of atoms. Thus Nominal + The reason is that one has to ensure that permutations are sort-respecting. + This was done implicitly in the original nominal logic work \cite{Pitts03}. + + Isabelle used the two-place permutation operation with the generic type @{text [display,indent=10] "_ \ _ :: (\ \ \) list \ \ \ \"} @@ -225,6 +218,13 @@ \cite{PittsHOL4} where variables and variable binding depend on type annotations. + Therefore it was decided in earlier versions of Nominal Isabelle to use a + separate type for each sort of atoms and let the type system enforce the + sort-respecting property of permutations. Inspired by the work on nominal + unification \cite{UrbanPittsGabbay04}, it seemed best at the time to also + implement permutations concretely as lists of pairs of atoms. + + *} section {* Sorted Atoms and Sort-Respecting Permutations *} diff -r e4e128e59c41 -r deb732753522 Pearl-jv/document/root.tex --- a/Pearl-jv/document/root.tex Wed May 05 09:23:10 2010 +0200 +++ b/Pearl-jv/document/root.tex Wed May 05 20:39:56 2010 +0100 @@ -31,14 +31,13 @@ \begin{abstract} Pitts et al introduced a beautiful theory about names and binding based on the -notions of atoms, permutations and support. The engineering challenge -is to smoothly adapt this theory to a theorem prover environment, in our case +notions of atoms, permutations and support. The engineering challenge is to +smoothly adapt this theory to a theorem prover environment, in our case Isabelle/HOL. We present a formalisation of this work that is based on a -unified atom type (that includes all sorts of atoms) and that represents -permutations by bijective functions from atoms to atoms. Interestingly, we -allow swappings, which are permutations build from two atoms, to be -ill-sorted. Furthermore we can extend the nominal logic with names that carry -additional information. +unified atom type and that represents permutations by bijective functions from +atoms to atoms. Interestingly, we allow swappings, which are permutations +build from two atoms, to be ill-sorted. Furthermore we extend the nominal +logic work with names that carry additional information. \end{abstract} % generated text of all theories