--- a/Nominal/nominal_function_core.ML Mon Jun 06 13:11:04 2011 +0100
+++ b/Nominal/nominal_function_core.ML Tue Jun 07 08:52:59 2011 +0100
@@ -7,6 +7,49 @@
Core of the nominal function package.
*)
+
+structure Nominal_Function_Common =
+struct
+
+
+(* Configuration management *)
+datatype nominal_function_opt
+ = Sequential
+ | Default of string
+ | DomIntros
+ | No_Partials
+ | Invariant of string
+
+datatype nominal_function_config = NominalFunctionConfig of
+ {sequential: bool,
+ default: string option,
+ domintros: bool,
+ partials: bool,
+ inv: string option}
+
+fun apply_opt Sequential (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =
+ NominalFunctionConfig
+ {sequential=true, default=default, domintros=domintros, partials=partials, inv=inv}
+ | apply_opt (Default d) (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =
+ NominalFunctionConfig
+ {sequential=sequential, default=SOME d, domintros=domintros, partials=partials, inv=inv}
+ | apply_opt DomIntros (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =
+ NominalFunctionConfig
+ {sequential=sequential, default=default, domintros=true, partials=partials, inv=inv}
+ | apply_opt No_Partials (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =
+ NominalFunctionConfig
+ {sequential=sequential, default=default, domintros=domintros, partials=false, inv=inv}
+ | apply_opt (Invariant s) (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =
+ NominalFunctionConfig
+ {sequential=sequential, default=default, domintros=domintros, partials=partials, inv = SOME s}
+
+val nominal_default_config =
+ NominalFunctionConfig { sequential=false, default=NONE,
+ domintros=false, partials=true, inv=NONE}
+
+end
+
+
signature NOMINAL_FUNCTION_CORE =
sig
val trace: bool Unsynchronized.ref
@@ -18,7 +61,7 @@
-> local_theory
-> (term (* f *)
* thm (* goalstate *)
- * (thm -> Nominal_Function_Common.function_result) (* continuation *)
+ * (thm -> Function_Common.function_result) (* continuation *)
) * local_theory
end
@@ -33,6 +76,7 @@
val mk_eq = HOLogic.mk_eq
open Function_Lib
+open Function_Common
open Nominal_Function_Common
datatype globals = Globals of
@@ -123,6 +167,20 @@
|> HOLogic.mk_Trueprop
end
+fun mk_inv inv (f_trm, arg_trm) =
+ betapplys (inv, [arg_trm, (f_trm $ arg_trm)])
+ |> HOLogic.mk_Trueprop
+
+fun mk_invariant (Globals {x, y, ...}) G invariant =
+ let
+ val prem = HOLogic.mk_Trueprop (G $ x $ y)
+ val concl = HOLogic.mk_Trueprop (betapplys (invariant, [x, y]))
+ in
+ Logic.mk_implies (prem, concl)
+ |> mk_forall_rename ("y", y)
+ |> mk_forall_rename ("x", x)
+ end
+
(** building proof obligations *)
fun mk_eqvt_proof_obligation qs fvar (vs, assms, arg) =
mk_eqvt_at (fvar, arg)
@@ -131,18 +189,27 @@
|> curry Term.list_abs_free qs
|> strip_abs_body
+fun mk_inv_proof_obligation inv qs fvar (vs, assms, arg) =
+ mk_inv inv (fvar, arg)
+ |> curry Logic.list_implies (map prop_of assms)
+ |> curry Term.list_all_free vs
+ |> curry Term.list_abs_free qs
+ |> strip_abs_body
+
(** building proof obligations *)
-fun mk_compat_proof_obligations domT ranT fvar f RCss glrs =
+fun mk_compat_proof_obligations domT ranT fvar f RCss inv glrs =
let
fun mk_impl (((qs, gs, lhs, rhs), RCs), ((qs', gs', lhs', rhs'), _)) =
let
val shift = incr_boundvars (length qs')
val eqvts_proof_obligations = map (shift o mk_eqvt_proof_obligation qs fvar) RCs
+ val invs_proof_obligations = map (shift o mk_inv_proof_obligation inv qs fvar) RCs
in
Logic.mk_implies
(HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'),
HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))
|> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
+ |> fold_rev (curry Logic.mk_implies) invs_proof_obligations (* nominal *)
|> fold_rev (curry Logic.mk_implies) eqvts_proof_obligations (* nominal *)
|> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs')
|> curry abstract_over fvar
@@ -152,7 +219,6 @@
map mk_impl (unordered_pairs (glrs ~~ RCss))
end
-
fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =
let
fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =
@@ -260,7 +326,7 @@
(* nominal *)
(* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
(* if j < i, then turn around *)
-fun get_compat_thm thy cts eqvtsi eqvtsj i j ctxi ctxj =
+fun get_compat_thm thy cts eqvtsi eqvtsj invsi invsj i j ctxi ctxj =
let
val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,case_hyp=case_hypi,...} = ctxi
val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,case_hyp=case_hypj,...} = ctxj
@@ -273,6 +339,7 @@
compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
|> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
|> fold Thm.elim_implies eqvtsj (* nominal *)
+ |> fold Thm.elim_implies invsj (* nominal *)
|> fold Thm.elim_implies agsj
|> fold Thm.elim_implies agsi
|> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
@@ -284,6 +351,7 @@
compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
|> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
|> fold Thm.elim_implies eqvtsi (* nominal *)
+ |> fold Thm.elim_implies invsi (* nominal *)
|> fold Thm.elim_implies agsi
|> fold Thm.elim_implies agsj
|> Thm.elim_implies (Thm.assume lhsi_eq_lhsj)
@@ -347,7 +415,31 @@
end
(* nominal *)
-fun mk_uniqueness_clause thy globals compat_store eqvts clausei clausej RLj =
+fun mk_invariant_lemma thy ih_inv clause =
+ let
+ val ClauseInfo {cdata=ClauseContext {cqs, ags, case_hyp, ...}, RCs, ...} = clause
+
+ local open Conv in
+ val ih_conv = arg1_conv o arg_conv o arg_conv
+ end
+
+ val ih_inv_case =
+ Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_inv
+
+ fun prep_inv (RCInfo {llRI, RIvs, CCas, ...}) =
+ (llRI RS ih_inv_case)
+ |> fold_rev (Thm.implies_intr o cprop_of) CCas
+ |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
+ in
+ map prep_inv RCs
+ |> map (fold_rev (Thm.implies_intr o cprop_of) ags)
+ |> map (Thm.implies_intr (cprop_of case_hyp))
+ |> map (fold_rev Thm.forall_intr cqs)
+ |> map (Thm.close_derivation)
+ end
+
+(* nominal *)
+fun mk_uniqueness_clause thy globals compat_store eqvts invs clausei clausej RLj =
let
val Globals {h, y, x, fvar, ...} = globals
val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, cqs = cqsi,
@@ -383,7 +475,17 @@
|> map (fold Thm.elim_implies [case_hypj'])
|> map (fold Thm.elim_implies agsj')
- val compat = get_compat_thm thy compat_store eqvtsi eqvtsj i j cctxi cctxj
+ val invsi = nth invs (i - 1)
+ |> map (fold Thm.forall_elim cqsi)
+ |> map (fold Thm.elim_implies [case_hyp])
+ |> map (fold Thm.elim_implies agsi)
+
+ val invsj = nth invs (j - 1)
+ |> map (fold Thm.forall_elim cqsj')
+ |> map (fold Thm.elim_implies [case_hypj'])
+ |> map (fold Thm.elim_implies agsj')
+
+ val compat = get_compat_thm thy compat_store eqvtsi eqvtsj invsi invsj i j cctxi cctxj
in
(trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
@@ -402,7 +504,8 @@
end
(* nominal *)
-fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses replems eqvtlems clausei =
+fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses replems eqvtlems invlems
+ clausei =
let
val Globals {x, y, ranT, fvar, ...} = globals
val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
@@ -421,7 +524,7 @@
val G_lhs_y = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
val unique_clauses =
- map2 (mk_uniqueness_clause thy globals compat_store eqvtlems clausei) clauses replems
+ map2 (mk_uniqueness_clause thy globals compat_store eqvtlems invlems clausei) clauses replems
fun elim_implies_eta A AB =
Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single
@@ -459,7 +562,7 @@
(* nominal *)
-fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim G_eqvt f_def =
+fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim G_eqvt invariant f_def =
let
val Globals {h, domT, ranT, x, ...} = globals
val thy = ProofContext.theory_of ctxt
@@ -476,17 +579,21 @@
val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
|> instantiate' [] [NONE, SOME (cterm_of thy h)]
val ih_eqvt = ihyp_thm RS (G_eqvt RS (f_def RS @{thm fundef_ex1_eqvt_at}))
-
+ val ih_inv = ihyp_thm RS (invariant COMP (f_def RS @{thm fundef_ex1_prop}))
+
val _ = trace_msg (K "Proving Replacement lemmas...")
val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
val _ = trace_msg (K "Proving Equivariance lemmas...")
val eqvtLemmas = map (mk_eqvt_lemma thy ih_eqvt) clauses
+ val _ = trace_msg (K "Proving Invariance lemmas...")
+ val invLemmas = map (mk_invariant_lemma thy ih_inv) clauses
+
val _ = trace_msg (K "Proving cases for unique existence...")
val (ex1s, values) =
split_list (map (mk_uniqueness_case thy globals G f
- ihyp ih_intro G_elim compat_store clauses repLemmas eqvtLemmas) clauses)
+ ihyp ih_intro G_elim compat_store clauses repLemmas eqvtLemmas invLemmas) clauses)
val _ = trace_msg (K "Proving: Graph is a function")
val graph_is_function = complete
@@ -499,11 +606,12 @@
|> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
val goalstate =
- Conjunction.intr (Conjunction.intr graph_is_function complete) G_eqvt
+ Conjunction.intr (Conjunction.intr (Conjunction.intr graph_is_function complete) invariant) G_eqvt
|> Thm.close_derivation
|> Goal.protect
|> fold_rev (Thm.implies_intr o cprop_of) compat
|> Thm.implies_intr (cprop_of complete)
+ |> Thm.implies_intr (cprop_of invariant)
|> Thm.implies_intr (cprop_of G_eqvt)
in
(goalstate, values)
@@ -905,9 +1013,10 @@
(* nominal *)
fun prepare_nominal_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy =
let
- val NominalFunctionConfig {domintros, default=default_opt, ...} = config
+ val NominalFunctionConfig {domintros, default=default_opt, inv=invariant_opt,...} = config
val default_str = the_default "%x. undefined" default_opt (*FIXME dynamic scoping*)
+ val invariant_str = the_default "%x y. True" invariant_opt
val fvar = Free (fname, fT)
val domT = domain_type fT
val ranT = range_type fT
@@ -915,6 +1024,9 @@
val default = Syntax.parse_term lthy default_str
|> Type.constraint fT |> Syntax.check_term lthy
+ val invariant_trm = Syntax.parse_term lthy invariant_str
+ |> Type.constraint ([domT, ranT] ---> @{typ bool}) |> Syntax.check_term lthy
+
val (globals, ctxt') = fix_globals domT ranT fvar lthy
val Globals { x, h, ... } = globals
@@ -957,26 +1069,29 @@
mk_completeness globals clauses abstract_qglrs |> cert |> Thm.assume
val compat =
- mk_compat_proof_obligations domT ranT fvar f RCss abstract_qglrs
+ mk_compat_proof_obligations domT ranT fvar f RCss invariant_trm abstract_qglrs
|> map (cert #> Thm.assume)
val G_eqvt = mk_eqvt G |> cert |> Thm.assume
+ val invariant = mk_invariant globals G invariant_trm |> cert |> Thm.assume
+
val compat_store = store_compat_thms n compat
val (goalstate, values) = PROFILE "prove_stuff"
(prove_stuff lthy globals G f R xclauses complete compat
- compat_store G_elim G_eqvt) f_defthm
+ compat_store G_elim G_eqvt invariant) f_defthm
fun mk_partial_rules provedgoal =
let
val newthy = theory_of_thm provedgoal (*FIXME*)
- val ((graph_is_function, complete_thm), _) =
+ val (graph_is_function, complete_thm) =
provedgoal
+ |> fst o Conjunction.elim
+ |> fst o Conjunction.elim
|> Conjunction.elim
- |>> Conjunction.elim
- |>> apfst (Thm.forall_elim_vars 0)
+ |> apfst (Thm.forall_elim_vars 0)
val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
--- a/Pearl-jv/Paper.thy Mon Jun 06 13:11:04 2011 +0100
+++ b/Pearl-jv/Paper.thy Tue Jun 07 08:52:59 2011 +0100
@@ -80,7 +80,7 @@
type to represent atoms of different sorts. The other is how to
present sort-respecting permutations. For them we use the standard
technique of HOL-formalisations of introducing an appropriate
- substype of functions from atoms to atoms.
+ subtype of functions from atoms to atoms.
The nominal logic work has been the starting point for a number of proving
infrastructures, most notable by Norrish \cite{norrish04} in HOL4, by
@@ -323,7 +323,7 @@
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}l}
- i)~~@{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]}\\
+ i)~~@{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]}\smallskip\\
ii)~~@{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{9mm}
iii)~~@{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{9mm}
iv)~~@{thm group_add_class.left_minus[where a="\<pi>::perm"]}
@@ -357,7 +357,7 @@
\noindent
whereby @{text "\<beta>"} is a generic type for the object @{text
- x}.\footnote{We will use the standard notation @{text "((op \<bullet>) \<pi>)
+ x}.\footnote{We will write @{text "((op \<bullet>) \<pi>)
x"} for this operation in the few cases where we need to indicate
that it is a function applied with two arguments.} The definition
of this operation will be given by in terms of `induction' over this
@@ -506,7 +506,8 @@
\emph{equivariance} and the \emph{equivariance principle}. These
notions allows us to characterise how permutations act upon compound
statements in HOL by analysing how these statements are constructed.
- The notion of equivariance can defined as follows:
+ The notion of equivariance means that an object is invariant under
+ any permutations. This can be defined as follows:
\begin{definition}[Equivariance]\label{equivariance}
An object @{text "x"} of permutation type is \emph{equivariant} provided
@@ -518,8 +519,8 @@
@{text x} is a constant, but of course there is no way in
Isabelle/HOL to restrict this definition to just these cases.
- There are a number of equivalent formulations for the equivariance
- property. For example, assuming @{text f} is a function of permutation
+ There are a number of equivalent formulations for equivariance.
+ For example, assuming @{text f} is a function of permutation
type @{text "\<alpha> \<Rightarrow> \<beta>"}, then equivariance of @{text f} can also be stated as
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -529,7 +530,7 @@
\end{isabelle}
\noindent
- We will call this formulation of equivariance in \emph{fully applied form}.
+ We will say this formulation of equivariance is in \emph{fully applied form}.
To see that this formulation implies the definition, we just unfold
the definition of the permutation operation for functions and
simplify with the equation and the cancellation property shown in
@@ -602,8 +603,8 @@
legibility we leave the typing information implicit. We also assume
the usual notions for free and bound variables of a HOL-term.
Furthermore, HOL-terms are regarded as equal modulo alpha-, beta-
- and eta-equivalence. The equivariance principle can now be stated
- formally as follows:
+ and eta-equivalence. The equivariance principle can now
+ be stated formally as follows:
\begin{theorem}[Equivariance Principle]\label{eqvtprin}
Suppose a HOL-term @{text t} whose constants are all equivariant. For any
@@ -615,9 +616,20 @@
\noindent
The significance of this principle is that we can automatically establish
the equivariance of a constant for which equivariance is not yet
- known. For this we only have to make sure that the definiens of this
- constant is a HOL-term whose constants are all equivariant. For example
- the universal quantifier @{text "\<forall>"} is definied in HOL as
+ known. For this we only have to establish that the definiens of this
+ constant is a HOL-term whose constants are all equivariant.
+ This meshes well with how HOL is designed: except for a few axioms, every constant
+ is defined in terms of existing constants. For example an alternative way
+ to deduce that @{term True} is equivariant is to look at its
+ definition
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ @{thm True_def}
+ \end{isabelle}
+
+ \noindent
+ and observing that the only constant in the definiens, namely @{text "="}, is
+ equivariant. Similarly, the universal quantifier @{text "\<forall>"} is definied in HOL as
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@{text "\<forall>x. P x \<equiv> "}~@{thm (rhs) All_def[no_vars]}
@@ -629,7 +641,11 @@
the equivariance principle gives us
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- @{text "\<pi> \<bullet> (\<forall>x. P x) \<equiv> \<pi> \<bullet> (P = (\<lambda>x. True)) = ((\<pi> \<bullet> P) = (\<lambda>x. True)) \<equiv> \<forall>x. (\<pi> \<bullet> P) x"}
+ \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+ @{text "\<pi> \<bullet> (\<forall>x. P x)"} & @{text "\<equiv>"} & @{text "\<pi> \<bullet> (P = (\<lambda>x. True))"}\\
+ & @{text "="} & @{text "(\<pi> \<bullet> P) = (\<lambda>x. True)"}\\
+ & @{text "\<equiv>"} & @{text "\<forall>x. (\<pi> \<bullet> P) x"}
+ \end{tabular}
\end{isabelle}
\noindent
@@ -653,7 +669,8 @@
\noindent
with all constants on the right-hand side being equivariant. With this kind
- of reasoning we can build up a database of equivariant constants.
+ of reasoning we can build up a database of equivariant constants, which will
+ be handy for more complex calculations later on.
Before we proceed, let us give a justification for the equivariance principle.
This justification cannot be given directly inside Isabelle/HOL since we cannot
@@ -670,14 +687,15 @@
permutation inside the term @{text t}. We have implemented this as a
conversion tactic on the ML-level of Isabelle/HOL. In what follows,
we will show that this tactic produces only finitely many equations
- and also show that is correct (in the sense of pushing a permutation
+ and also show that it is correct (in the sense of pushing a permutation
@{text "\<pi>"} inside a term and the only remaining instances of @{text
- "\<pi>"} are in front of the term's free variables). The tactic applies
- four `oriented' equations. We will first give a naive version of
- this tactic, which however in some cornercases produces incorrect
+ "\<pi>"} are in front of the term's free variables).
+
+ The tactic applies four `oriented' equations.
+ We will first give a naive version of
+ our tactic, which however in some corner cases produces incorrect
results or does not terminate. We then give a modification in order
to obtain the desired properties.
-
Consider the following for oriented equations
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -697,10 +715,9 @@
and the fact that HOL-terms are equal modulo beta-equivalence.
The third is a consequence of \eqref{cancel} and the fourth from
Definition~\ref{equivariance}. Unfortunately, we have to be careful with
- the rules {\it i)} and {\it iv}) since they can lead to a loop whenever
- \mbox{@{text "t\<^isub>1 t\<^isub>2"}} is of the form @{text "((op \<bullet>) \<pi>') t"}.\footnote{Note we
- deviate here from our usual convention of writing the permutation operation infix,
- instead as an application.} Recall that we established in Lemma \ref{permutecompose} that the
+ the rules {\it i)} and {\it iv}) since they can lead to loops whenever
+ \mbox{@{text "t\<^isub>1 t\<^isub>2"}} is of the form @{text "((op \<bullet>) \<pi>') t"}.
+ Recall that we established in Lemma \ref{permutecompose} that the
constant @{text "(op \<bullet>)"} is equivariant and consider the infinite
reduction sequence
@@ -716,7 +733,7 @@
\end{isabelle}
\noindent
- where the last term is again an instance of rewrite rule {\it i}), but bigger.
+ where the last term is again an instance of rewrite rule {\it i}), but larger.
To avoid this loop we will apply the rewrite rule
using an `outside to inside' strategy. This strategy is sufficient
since we are only interested of rewriting terms of the form @{term
@@ -726,8 +743,8 @@
iii)} can `overlap'. For this note that the term @{term "\<pi>
\<bullet>(\<lambda>x. x)"} reduces by {\it ii)} to @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet> x"}, to
which we can apply rule {\it iii)} in order to obtain @{term
- "\<lambda>x. x"}, as is desired---since there is no free variable in the original
- term. the permutation should completely vanish. However, the
+ "\<lambda>x. x"}, as is desired: since there is no free variable in the original
+ term, the permutation should completely vanish. However, the
subterm @{text "(- \<pi>) \<bullet> x"} is also an application. Consequently,
the term @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet>x"} can also reduce to @{text "\<lambda>x. (- (\<pi>
\<bullet> \<pi>)) \<bullet> (\<pi> \<bullet> x)"} using {\it i)}. Given our strategy, we cannot
@@ -1222,11 +1239,11 @@
representation for permutations (for example @{term "(a \<rightleftharpoons> b)"} and
@{term "(b \<rightleftharpoons> a)"} are equal permutations), this representation does
not come automatically with an induction principle. Such an
- induction principle is however handy for generalising
- Lemma~\ref{swapfreshfresh} from swappings to permutations
+ induction principle is however useful for generalising
+ Lemma~\ref{swapfreshfresh} from swappings to permutations, namely
\begin{lemma}
- @{thm [mode=IfThen] perm_supp_eq[no_vars]}
+ @{thm [mode=IfThen] perm_supp_eq[where p="\<pi>", no_vars]}
\end{lemma}
\noindent
@@ -1238,7 +1255,7 @@
Using a the property from \cite{???}
\begin{lemma}\label{smallersupp}
- @{thm [mode=IfThen] smaller_supp[no_vars]}
+ @{thm [mode=IfThen] smaller_supp[where p="\<pi>", no_vars]}
\end{lemma}
*}