--- 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 \<Rightarrow> bool) \<Rightarrow> ('b::pt)) \<Rightarrow> ('a::pt)"
+ shows "(p \<bullet> (P The)) = foo"
+apply(perm_simp exclude: The)
+oops
+
thm eqvts
thm eqvts_raw
--- 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' ]
--- 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))
--- 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
--- 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
--- 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
--- 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] "_ \<bullet> _ :: (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
@@ -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 *}
--- 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