# HG changeset patch # User Christian Urban # Date 1307433179 -3600 # Node ID c7d4bd9e89e0824f90c79c9c1243db32301f3989 # Parent 77e1d9f2925e022e54da50a5ca33adec871d11e0 fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant diff -r 77e1d9f2925e -r c7d4bd9e89e0 Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Mon Jun 06 13:11:04 2011 +0100 +++ b/Nominal/Ex/Lambda.thy Tue Jun 07 08:52:59 2011 +0100 @@ -47,6 +47,51 @@ apply(simp add: swap_commute) done +nominal_primrec (invariant "\x (y::atom set). finite y") + frees_set :: "lam \ atom set" +where + "frees_set (Var x) = {atom x}" +| "frees_set (App t1 t2) = frees_set t1 \ frees_set t2" +| "frees_set (Lam [x]. t) = (frees_set t) - {atom x}" +apply(simp add: eqvt_def frees_set_graph_def) +apply (rule, perm_simp, rule) +apply(erule frees_set_graph.induct) +apply(simp) +apply(simp) +apply(simp) +apply(rule_tac y="x" in lam.exhaust) +apply(auto)[6] +apply(simp) +apply(simp) +apply(simp) +apply (erule Abs1_eq_fdest) +apply(simp add: fresh_def) +apply(subst supp_of_finite_sets) +apply(simp) +apply(simp add: supp_atom) +apply(simp add: fresh_def) +apply(subst supp_of_finite_sets) +apply(simp) +apply(simp add: supp_atom) +apply(subst supp_finite_atom_set[symmetric]) +apply(simp) +apply(simp add: fresh_def[symmetric]) +apply(rule fresh_eqvt_at) +apply(assumption) +apply(simp add: finite_supp) +apply(simp) +apply(simp add: eqvt_at_def eqvts) +apply(simp) +done + +print_theorems + +termination + by (relation "measure size") (auto simp add: lam.size) + + +thm frees_set.simps + lemma fresh_fun_eqvt_app3: assumes a: "eqvt f" and b: "a \ x" "a \ y" "a \ z" @@ -72,6 +117,7 @@ apply (simp add: eqvt_def f_graph_def) apply (perm_simp) apply(simp add: eq[simplified eqvt_def]) + apply(rule TrueI) apply(rule_tac y="x" in lam.exhaust) apply(auto simp add: fresh_star_def) apply(erule Abs1_eq_fdest) @@ -91,6 +137,8 @@ termination by (relation "measure size") (auto simp add: lam.size) +thm f.simps + end diff -r 77e1d9f2925e -r c7d4bd9e89e0 Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Mon Jun 06 13:11:04 2011 +0100 +++ b/Nominal/Nominal2.thy Tue Jun 07 08:52:59 2011 +0100 @@ -6,7 +6,6 @@ ("nominal_dt_quot.ML") ("nominal_induct.ML") ("nominal_inductive.ML") - ("nominal_function_common.ML") ("nominal_function_core.ML") ("nominal_mutual.ML") ("nominal_function.ML") @@ -36,7 +35,6 @@ (***************************************) (* forked code of the function package *) (* for defining nominal functions *) -use "nominal_function_common.ML" use "nominal_function_core.ML" use "nominal_mutual.ML" use "nominal_function.ML" diff -r 77e1d9f2925e -r c7d4bd9e89e0 Nominal/nominal_function.ML --- a/Nominal/nominal_function.ML Mon Jun 06 13:11:04 2011 +0100 +++ b/Nominal/nominal_function.ML Tue Jun 07 08:52:59 2011 +0100 @@ -38,6 +38,7 @@ struct open Function_Lib +open Function_Common open Nominal_Function_Common diff -r 77e1d9f2925e -r c7d4bd9e89e0 Nominal/nominal_function_common.ML --- a/Nominal/nominal_function_common.ML Mon Jun 06 13:11:04 2011 +0100 +++ b/Nominal/nominal_function_common.ML Tue Jun 07 08:52:59 2011 +0100 @@ -1,6 +1,9 @@ (* Nominal Function Common Author: Christian Urban + heavily based on the code of Alexander Krauss + (code forked on 5 June 2011) + Common definitions and other infrastructure for the function package. *) @@ -350,7 +353,7 @@ fun config_parser default = (Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") []) - >> (fn opts => fold apply_opt opts default) + >> (fn opts => fold Nominal_Function_Common.apply_opt opts default) in fun function_parser default_cfg = config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs diff -r 77e1d9f2925e -r c7d4bd9e89e0 Nominal/nominal_function_core.ML --- 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) diff -r 77e1d9f2925e -r c7d4bd9e89e0 Nominal/nominal_mutual.ML --- a/Nominal/nominal_mutual.ML Mon Jun 06 13:11:04 2011 +0100 +++ b/Nominal/nominal_mutual.ML Tue Jun 07 08:52:59 2011 +0100 @@ -17,7 +17,7 @@ -> term list -> local_theory -> ((thm (* goalstate *) - * (thm -> Nominal_Function_Common.function_result) (* proof continuation *) + * (thm -> Function_Common.function_result) (* proof continuation *) ) * local_theory) end @@ -27,6 +27,7 @@ struct open Function_Lib +open Function_Common open Nominal_Function_Common type qgar = string * (string * typ) list * term list * term list * term diff -r 77e1d9f2925e -r c7d4bd9e89e0 Pearl-jv/Paper.thy --- 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="\\<^isub>1" and b="\\<^isub>2" and c="\\<^isub>3"]}\\ + i)~~@{thm add_assoc[where a="\\<^isub>1" and b="\\<^isub>2" and c="\\<^isub>3"]}\smallskip\\ ii)~~@{thm monoid_add_class.add_0_left[where a="\::perm"]} \hspace{9mm} iii)~~@{thm monoid_add_class.add_0_right[where a="\::perm"]} \hspace{9mm} iv)~~@{thm group_add_class.left_minus[where a="\::perm"]} @@ -357,7 +357,7 @@ \noindent whereby @{text "\"} is a generic type for the object @{text - x}.\footnote{We will use the standard notation @{text "((op \) \) + x}.\footnote{We will write @{text "((op \) \) 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 "\ \ \"}, 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 "\"} 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 "\"} is definied in HOL as \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% @{text "\x. P x \ "}~@{thm (rhs) All_def[no_vars]} @@ -629,7 +641,11 @@ the equivariance principle gives us \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - @{text "\ \ (\x. P x) \ \ \ (P = (\x. True)) = ((\ \ P) = (\x. True)) \ \x. (\ \ P) x"} + \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l} + @{text "\ \ (\x. P x)"} & @{text "\"} & @{text "\ \ (P = (\x. True))"}\\ + & @{text "="} & @{text "(\ \ P) = (\x. True)"}\\ + & @{text "\"} & @{text "\x. (\ \ 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 "\"} inside a term and the only remaining instances of @{text - "\"} 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 + "\"} 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 \) \') 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 \) \') t"}. + Recall that we established in Lemma \ref{permutecompose} that the constant @{text "(op \)"} 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 "\ \(\x. x)"} reduces by {\it ii)} to @{term "\x. \ \ (- \) \ x"}, to which we can apply rule {\it iii)} in order to obtain @{term - "\x. x"}, as is desired---since there is no free variable in the original - term. the permutation should completely vanish. However, the + "\x. x"}, as is desired: since there is no free variable in the original + term, the permutation should completely vanish. However, the subterm @{text "(- \) \ x"} is also an application. Consequently, the term @{term "\x. \ \ (- \) \x"} can also reduce to @{text "\x. (- (\ \ \)) \ (\ \ x)"} using {\it i)}. Given our strategy, we cannot @@ -1222,11 +1239,11 @@ representation for permutations (for example @{term "(a \ b)"} and @{term "(b \ 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="\", 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="\", no_vars]} \end{lemma} *}