# HG changeset patch # User Christian Urban # Date 1265195602 -3600 # Node ID 6911934c98c737b4dd89fc0182be8ea43b0ece22 # Parent 2845e736dc1a872ab85484b1a06d90aab65977d3# Parent aaac8274f08c14e3afec651691b7832bcdfa7c3b merged diff -r aaac8274f08c -r 6911934c98c7 Quot/Nominal/Nominal2_Eqvt.thy --- a/Quot/Nominal/Nominal2_Eqvt.thy Wed Feb 03 12:11:23 2010 +0100 +++ b/Quot/Nominal/Nominal2_Eqvt.thy Wed Feb 03 12:13:22 2010 +0100 @@ -6,6 +6,7 @@ theory Nominal2_Eqvt imports Nominal2_Base uses ("nominal_thmdecls.ML") + ("nominal_permeq.ML") begin section {* Logical Operators *} @@ -43,25 +44,40 @@ by (simp add: permute_bool_def) lemma all_eqvt: + shows "p \ (\x. P x) = (\x. (p \ P) x)" + unfolding permute_fun_def permute_bool_def + by (auto, drule_tac x="p \ x" in spec, simp) + +lemma all_eqvt2: shows "p \ (\x. P x) = (\x. p \ P (- p \ x))" unfolding permute_fun_def permute_bool_def by (auto, drule_tac x="p \ x" in spec, simp) lemma ex_eqvt: + shows "p \ (\x. P x) = (\x. (p \ P) x)" + unfolding permute_fun_def permute_bool_def + by (auto, rule_tac x="p \ x" in exI, simp) + +lemma ex_eqvt2: shows "p \ (\x. P x) = (\x. p \ P (- p \ x))" unfolding permute_fun_def permute_bool_def by (auto, rule_tac x="p \ x" in exI, simp) lemma ex1_eqvt: + shows "p \ (\!x. P x) = (\!x. (p \ P) x)" + unfolding Ex1_def + by (simp add: ex_eqvt permute_fun_def conj_eqvt all_eqvt imp_eqvt eq_eqvt) + +lemma ex1_eqvt2: shows "p \ (\!x. P x) = (\!x. p \ P (- p \ x))" - unfolding Ex1_def ex_eqvt conj_eqvt all_eqvt imp_eqvt eq_eqvt + unfolding Ex1_def ex_eqvt2 conj_eqvt all_eqvt2 imp_eqvt eq_eqvt by simp lemma the_eqvt: assumes unique: "\!x. P x" shows "p \ (THE x. P x) = (THE x. p \ P (- p \ x))" apply(rule the1_equality [symmetric]) - apply(simp add: ex1_eqvt[symmetric]) + apply(simp add: ex1_eqvt2[symmetric]) apply(simp add: permute_bool_def unique) apply(simp add: permute_bool_def) apply(rule theI'[OF unique]) @@ -78,12 +94,16 @@ unfolding mem_def permute_fun_def by (simp add: Not_eqvt) lemma Collect_eqvt: + shows "p \ {x. P x} = {x. (p \ P) x}" + unfolding Collect_def permute_fun_def .. + +lemma Collect_eqvt2: shows "p \ {x. P x} = {x. p \ (P (-p \ x))}" unfolding Collect_def permute_fun_def .. lemma empty_eqvt: shows "p \ {} = {}" - unfolding empty_def Collect_eqvt False_eqvt .. + unfolding empty_def Collect_eqvt2 False_eqvt .. lemma supp_set_empty: shows "supp {} = {}" @@ -95,20 +115,20 @@ lemma UNIV_eqvt: shows "p \ UNIV = UNIV" - unfolding UNIV_def Collect_eqvt True_eqvt .. + unfolding UNIV_def Collect_eqvt2 True_eqvt .. lemma union_eqvt: shows "p \ (A \ B) = (p \ A) \ (p \ B)" - unfolding Un_def Collect_eqvt disj_eqvt mem_eqvt by simp + unfolding Un_def Collect_eqvt2 disj_eqvt mem_eqvt by simp lemma inter_eqvt: shows "p \ (A \ B) = (p \ A) \ (p \ B)" - unfolding Int_def Collect_eqvt conj_eqvt mem_eqvt by simp + unfolding Int_def Collect_eqvt2 conj_eqvt mem_eqvt by simp lemma Diff_eqvt: fixes A B :: "'a::pt set" shows "p \ (A - B) = p \ A - p \ B" - unfolding set_diff_eq Collect_eqvt conj_eqvt Not_eqvt mem_eqvt by simp + unfolding set_diff_eq Collect_eqvt2 conj_eqvt Not_eqvt mem_eqvt by simp lemma Compl_eqvt: fixes A :: "'a::pt set" @@ -122,7 +142,7 @@ lemma vimage_eqvt: shows "p \ (f -` A) = (p \ f) -` (p \ A)" unfolding vimage_def permute_fun_def [where f=f] - unfolding Collect_eqvt mem_eqvt .. + unfolding Collect_eqvt2 mem_eqvt .. lemma image_eqvt: shows "p \ (f ` A) = (p \ f) ` (p \ A)" @@ -139,11 +159,6 @@ shows "p \ finite A = finite (p \ A)" unfolding finite_permute_iff permute_bool_def .. -lemma supp_eqvt: "p \ supp S = supp (p \ S)" - unfolding supp_def - by (simp only: Collect_eqvt Not_eqvt finite_eqvt eq_eqvt - permute_eqvt [of p] swap_eqvt permute_minus_cancel) - section {* List Operations *} @@ -205,22 +220,20 @@ section {* Equivariance automation *} -text {* - below is a construction site for a conversion that - pushes permutations into a term as far as possible -*} - text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_force} *} use "nominal_thmdecls.ML" -setup "NominalThmDecls.setup" +setup "Nominal_ThmDecls.setup" lemmas [eqvt] = (* connectives *) eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt - True_eqvt False_eqvt + True_eqvt False_eqvt ex_eqvt all_eqvt imp_eqvt [folded induct_implies_def] + (* nominal *) + permute_eqvt supp_eqvt fresh_eqvt + (* datatypes *) permute_prod.simps fst_eqvt snd_eqvt @@ -229,142 +242,56 @@ empty_eqvt UNIV_eqvt union_eqvt inter_eqvt Diff_eqvt Compl_eqvt insert_eqvt -(* A simple conversion pushing permutations into a term *) - -ML {* -fun OF1 thm1 thm2 = thm2 RS thm1 - -fun get_eqvt_thms ctxt = - map (OF1 @{thm eq_reflection}) (NominalThmDecls.get_eqvt_thms ctxt) -*} +declare permute_pure [eqvt] -ML {* -fun eqvt_conv ctxt ctrm = - case (term_of ctrm) of - (Const (@{const_name "permute"}, _) $ _ $ t) => - (if is_Const (head_of t) - then (More_Conv.rewrs_conv (get_eqvt_thms ctxt) - then_conv eqvt_conv ctxt) ctrm - else Conv.comb_conv (eqvt_conv ctxt) ctrm) - | _ $ _ => Conv.comb_conv (eqvt_conv ctxt) ctrm - | Abs _ => Conv.abs_conv (fn (_, ctxt) => eqvt_conv ctxt) ctxt ctrm - | _ => Conv.all_conv ctrm -*} +thm eqvt -ML {* -fun eqvt_tac ctxt = - CONVERSION (More_Conv.bottom_conv (fn ctxt => eqvt_conv ctxt) ctxt) -*} - -lemma "p \ (A \ B = (C::bool))" -apply(tactic {* eqvt_tac @{context} 1 *}) -oops - -text {* - Another conversion for pushing permutations into a term. - It is designed not to apply rules like @{term permute_pure} to - applications or abstractions, only to constants or free - variables. Thus permutations are not removed too early, and they - have a chance to cancel with bound variables. -*} +text {* helper lemmas for the eqvt_tac *} definition "unpermute p = permute (- p)" -lemma push_apply: - fixes f :: "'a::pt \ 'b::pt" and x :: "'a::pt" +lemma eqvt_apply: + fixes f :: "'a::pt \ 'b::pt" + and x :: "'a::pt" shows "p \ (f x) \ (p \ f) (p \ x)" unfolding permute_fun_def by simp -lemma push_lambda: +lemma eqvt_lambda: fixes f :: "'a::pt \ 'b::pt" shows "p \ (\x. f x) \ (\x. p \ (f (unpermute p x)))" unfolding permute_fun_def unpermute_def by simp -lemma push_bound: +lemma eqvt_bound: shows "p \ unpermute p x \ x" unfolding unpermute_def by simp -ML {* -structure PushData = Named_Thms -( - val name = "push" - val description = "push permutations" -) - -local +use "nominal_permeq.ML" -fun push_apply_conv ctxt ct = - case (term_of ct) of - (Const (@{const_name "permute"}, _) $ _ $ (_ $ _)) => - let - val (perm, t) = Thm.dest_comb ct - val (_, p) = Thm.dest_comb perm - val (f, x) = Thm.dest_comb t - val a = ctyp_of_term x; - val b = ctyp_of_term t; - val ty_insts = map SOME [b, a] - val term_insts = map SOME [p, f, x] - in - Drule.instantiate' ty_insts term_insts @{thm push_apply} - end - | _ => Conv.no_conv ct - -fun push_lambda_conv ctxt ct = - case (term_of ct) of - (Const (@{const_name "permute"}, _) $ _ $ Abs _) => - Conv.rewr_conv @{thm push_lambda} ct - | _ => Conv.no_conv ct - -in -fun push_conv ctxt ct = - Conv.first_conv - [ Conv.rewr_conv @{thm push_bound}, - push_apply_conv ctxt - then_conv Conv.comb_conv (push_conv ctxt), - push_lambda_conv ctxt - then_conv Conv.abs_conv (fn (v, ctxt) => push_conv ctxt) ctxt, - More_Conv.rewrs_conv (PushData.get ctxt), - Conv.all_conv - ] ct - -fun push_tac ctxt = - CONVERSION (More_Conv.bottom_conv (fn ctxt => push_conv ctxt) ctxt) - -end -*} - -setup PushData.setup - -declare permute_pure [THEN eq_reflection, push] - -lemma push_eq [THEN eq_reflection, push]: - "p \ (op =) = (op =)" - by (simp add: expand_fun_eq permute_fun_def eq_eqvt) - -lemma push_All [THEN eq_reflection, push]: - "p \ All = All" - by (simp add: expand_fun_eq permute_fun_def all_eqvt) - -lemma push_Ex [THEN eq_reflection, push]: - "p \ Ex = Ex" - by (simp add: expand_fun_eq permute_fun_def ex_eqvt) - -lemma "p \ (A \ B = (C::bool))" -apply (tactic {* push_tac @{context} 1 *}) +lemma "p \ (A \ B = C)" +apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *}) oops -lemma "p \ (\x. A \ B x = (C::bool)) = foo" -apply (tactic {* push_tac @{context} 1 *}) +lemma "p \ (\(x::'a::pt). A \ (B::'a \ bool) x = C) = foo" +apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *}) oops lemma "p \ (\x y. \z. x = z \ x = y \ z \ x) = foo" -apply (tactic {* push_tac @{context} 1 *}) +apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *}) oops lemma "p \ (\f x. f (g (f x))) = foo" -apply (tactic {* push_tac @{context} 1 *}) +apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *}) +oops + +lemma "p \ (\q. q \ (r \ x)) = foo" +apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *}) oops +lemma "p \ (q \ r \ x) = foo" +apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *}) +oops + + end \ No newline at end of file diff -r aaac8274f08c -r 6911934c98c7 Quot/Nominal/nominal_permeq.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quot/Nominal/nominal_permeq.ML Wed Feb 03 12:13:22 2010 +0100 @@ -0,0 +1,71 @@ +(* Title: nominal_thmdecls.ML + Author: Brian Huffman, Christian Urban +*) + +signature NOMINAL_PERMEQ = +sig + val eqvt_tac: Proof.context -> int -> tactic + +end; + +(* TODO: + + - provide a method interface with the usual add and del options + + - print a warning if for a constant no eqvt lemma is stored + + - there seems to be too much simplified in case of multiple + permutations, like + + p o q o r o x + + we usually only want the outermost permutation to "float" in +*) + + +structure Nominal_Permeq: NOMINAL_PERMEQ = +struct + +local + +fun eqvt_apply_conv ctxt ct = + case (term_of ct) of + (Const (@{const_name "permute"}, _) $ _ $ (_ $ _)) => + let + val (perm, t) = Thm.dest_comb ct + val (_, p) = Thm.dest_comb perm + val (f, x) = Thm.dest_comb t + val a = ctyp_of_term x; + val b = ctyp_of_term t; + val ty_insts = map SOME [b, a] + val term_insts = map SOME [p, f, x] + in + Drule.instantiate' ty_insts term_insts @{thm eqvt_apply} + end + | _ => Conv.no_conv ct + +fun eqvt_lambda_conv ctxt ct = + case (term_of ct) of + (Const (@{const_name "permute"}, _) $ _ $ Abs _) => + Conv.rewr_conv @{thm eqvt_lambda} ct + | _ => Conv.no_conv ct + +in + +fun eqvt_conv ctxt ct = + Conv.first_conv + [ Conv.rewr_conv @{thm eqvt_bound}, + eqvt_apply_conv ctxt + then_conv Conv.comb_conv (eqvt_conv ctxt), + eqvt_lambda_conv ctxt + then_conv Conv.abs_conv (fn (v, ctxt) => eqvt_conv ctxt) ctxt, + More_Conv.rewrs_conv (Nominal_ThmDecls.get_eqvt_thms ctxt), + Conv.all_conv + ] ct + +fun eqvt_tac ctxt = + CONVERSION (More_Conv.bottom_conv (fn ctxt => eqvt_conv ctxt) ctxt) + +end + +end; (* structure *) \ No newline at end of file diff -r aaac8274f08c -r 6911934c98c7 Quot/Nominal/nominal_thmdecls.ML --- a/Quot/Nominal/nominal_thmdecls.ML Wed Feb 03 12:11:23 2010 +0100 +++ b/Quot/Nominal/nominal_thmdecls.ML Wed Feb 03 12:13:22 2010 +0100 @@ -1,13 +1,23 @@ -(* Title: HOL/Nominal/nominal_thmdecls.ML - Author: Julien Narboux, TU Muenchen - Author: Christian Urban, TU Muenchen +(* Title: nominal_thmdecls.ML + Author: Christian Urban + + Infrastructure for the lemma collection "eqvts". + + Provides the attributes [eqvt] and [eqvt_force], and the theorem + list eqvt. In contrast to eqvt-force, the eqvt-lemmas that will be + stored are expected to be of the form -Infrastructure for the lemma collection "eqvts". + p o (c x1 x2 ...) = c (p o x1) (p o x2) ... + + and are transformed into the form + + p o c == c -By attaching [eqvt] or [eqvt_force] to a lemma, it will get stored in -a data-slot in the context. Possible modifiers are [... add] and -[... del] for adding and deleting, respectively, the lemma from the -data-slot. + TODO + + - deal with eqvt-lemmas of the for + + c x1 x2 ... ==> c (p o x1) (p o x2) .. *) signature NOMINAL_THMDECLS = @@ -21,151 +31,89 @@ end; -structure NominalThmDecls: NOMINAL_THMDECLS = +structure Nominal_ThmDecls: NOMINAL_THMDECLS = struct -structure Data = Generic_Data +structure EqvtData = Generic_Data ( - type T = thm list - val empty = [] - val extend = I - val merge = Thm.merge_thms -) + type T = thm Item_Net.T; + val empty = Thm.full_rules; + val extend = I; + val merge = Item_Net.merge; +); + +val content = Item_Net.content o EqvtData.get; +val get_eqvt_thms = content o Context.Proof; -(* Exception for when a theorem does not conform with form of an equivariance lemma. *) -(* There are two forms: one is an implication (for relations) and the other is an *) -(* equality (for functions). In the implication-case, say P ==> Q, Q must be equal *) -(* to P except that every free variable of Q, say x, is replaced by pi o x. In the *) -(* equality case, say lhs = rhs, the lhs must be of the form pi o t and the rhs must *) -(* be equal to t except that every free variable, say x, is replaced by pi o x. In *) -(* the implicational case it is also checked that the variables and permutation fit *) -(* together, i.e. are of the right "pt_class", so that a stronger version of the *) -(* equality-lemma can be derived. *) -exception EQVT_FORM of string +val add_thm = EqvtData.map o Item_Net.update; +val del_thm = EqvtData.map o Item_Net.remove; + +val add_force_thm = EqvtData.map o Item_Net.update; +val del_force_thm = EqvtData.map o Item_Net.remove; + -val perm_boolE = - @{lemma "pi \ P ==> P" by (simp add: permute_bool_def)}; - -val perm_boolI = - @{lemma "P ==> pi \ P" by (simp add: permute_bool_def)}; +fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) + | dest_perm t = raise TERM("dest_perm", [t]) -fun prove_eqvt_tac ctxt orig_thm pi pi' = +fun mk_perm p trm = let - val mypi = Thm.cterm_of ctxt pi - val T = fastype_of pi' - val mypifree = Thm.cterm_of ctxt (Const (@{const_name "uminus"}, T --> T) $ pi') - val perm_pi_simp = @{thms permute_minus_cancel} + val ty = fastype_of trm in - EVERY1 [rtac @{thm iffI}, - dtac perm_boolE, - etac orig_thm, - dtac (Drule.cterm_instantiate [(mypi, mypifree)] orig_thm), - rtac perm_boolI, - full_simp_tac (HOL_basic_ss addsimps perm_pi_simp)] -end; - -fun get_derived_thm ctxt hyp concl orig_thm pi = - let - val thy = ProofContext.theory_of ctxt; - val pi' = Var (pi, @{typ "perm"}); - val lhs = Const (@{const_name "permute"}, @{typ "perm"} --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp; - val ([goal_term, pi''], ctxt') = Variable.import_terms false - [HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, concl)), pi'] ctxt - in - Goal.prove ctxt' [] [] goal_term - (fn _ => prove_eqvt_tac thy orig_thm pi' pi'') |> - singleton (ProofContext.export ctxt' ctxt) - end - -(* replaces in t every variable, say x, with pi o x *) -fun apply_pi trm pi = -let - fun replace n ty = - let - val c = Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) - val v1 = Var (pi, @{typ "perm"}) - val v2 = Var (n, ty) - in - c $ v1 $ v2 - end -in - map_aterms (fn Var (n, ty) => replace n ty | t => t) trm + Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm end -(* returns *the* pi which is in front of all variables, provided there *) -(* exists such a pi; otherwise raises EQVT_FORM *) -fun get_pi t thy = - let fun get_pi_aux s = - (case s of - (Const (@{const_name "permute"} ,typrm) $ - (Var (pi,_)) $ - (Var (n,ty))) => - if (Sign.of_sort thy (ty, @{sort pt})) - then [pi] - else raise - EQVT_FORM ("Could not find any permutation or an argument is not an instance of pt") - | Abs (_,_,t1) => get_pi_aux t1 - | (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2 - | _ => []) - in - (* collect first all pi's in front of variables in t and then use distinct *) - (* to ensure that all pi's must have been the same, i.e. distinct returns *) - (* a singleton-list *) - (case (distinct (op =) (get_pi_aux t)) of - [pi] => pi - | [] => raise EQVT_FORM "No permutations found" - | _ => raise EQVT_FORM "All permutation should be the same") - end; - -(* Either adds a theorem (orig_thm) to or deletes one from the equivariance *) -(* lemma list depending on flag. To be added the lemma has to satisfy a *) -(* certain form. *) +fun eqvt_transform_tac thm = REPEAT o FIRST' + [CHANGED o simp_tac (HOL_basic_ss addsimps @{thms permute_minus_cancel}), + rtac (thm RS @{thm trans}), + rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}] -fun eqvt_add_del_aux flag orig_thm context = - let - val thy = Context.theory_of context - val thms_to_be_added = (case (prop_of orig_thm) of - (* case: eqvt-lemma is of the implicational form *) - (Const("==>", _) $ (Const ("Trueprop",_) $ hyp) $ (Const ("Trueprop",_) $ concl)) => - let - val pi = get_pi concl thy - in - if (apply_pi hyp pi = concl) - then - (warning ("equivariance lemma of the relational form"); - [orig_thm, - get_derived_thm (Context.proof_of context) hyp concl orig_thm pi]) - else raise EQVT_FORM "Type Implication" - end - (* case: eqvt-lemma is of the equational form *) - | (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $ - (Const (@{const_name "permute"},typrm) $ Var (pi, _) $ lhs) $ rhs)) => - (if (apply_pi lhs pi) = rhs - then [orig_thm] - else raise EQVT_FORM "Type Equality") - | _ => raise EQVT_FORM "Type unknown") - in - fold (fn thm => Data.map (flag thm)) thms_to_be_added context - end - handle EQVT_FORM s => - error (Display.string_of_thm (Context.proof_of context) orig_thm ^ - " does not comply with the form of an equivariance lemma (" ^ s ^").") +(* transform equations into the required form *) +fun transform_eq ctxt thm lhs rhs = +let + val (p, t) = dest_perm lhs + val (c, args) = strip_comb t + val (c', args') = strip_comb rhs + val eargs = map Envir.eta_contract args + val eargs' = map Envir.eta_contract args' + val p_str = fst (fst (dest_Var p)) + val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) +in + if c <> c' + then error "eqvt lemma is not of the right form (constants do not agree)" + else if eargs' <> map (mk_perm p) eargs + then error "eqvt lemma is not of the right form (arguments do not agree)" + else if args = [] + then thm + else Goal.prove ctxt [p_str] [] goal + (fn _ => eqvt_transform_tac thm 1) +end + +fun transform addel_fn thm context = +let + val ctxt = Context.proof_of context + val trm = HOLogic.dest_Trueprop (prop_of thm) +in + case trm of + Const (@{const_name "op ="}, _) $ lhs $ rhs => + addel_fn (transform_eq ctxt thm lhs rhs RS @{thm eq_reflection}) context + | _ => raise (error "no other cases yet implemented") +end -val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (Thm.add_thm)); -val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (Thm.del_thm)); +val eqvt_add = Thm.declaration_attribute (transform add_thm); +val eqvt_del = Thm.declaration_attribute (transform del_thm); -val eqvt_force_add = Thm.declaration_attribute (Data.map o Thm.add_thm); -val eqvt_force_del = Thm.declaration_attribute (Data.map o Thm.del_thm); - -val get_eqvt_thms = Context.Proof #> Data.get; +val eqvt_force_add = Thm.declaration_attribute add_force_thm; +val eqvt_force_del = Thm.declaration_attribute del_force_thm; val setup = - Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del) - "equivariance theorem declaration" - #> Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del) - "equivariance theorem declaration (without checking the form of the lemma)" - #> PureThy.add_thms_dynamic (Binding.name "eqvts", Data.get) + Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) + (cat_lines ["declaration of equivariance lemmas - they will automtically be", + "brought into the form p o c = c"]) #> + Attrib.setup @{binding "eqvt_force"} (Attrib.add_del eqvt_force_add eqvt_force_del) + (cat_lines ["declaration of equivariance lemmas - they will will be", + "added/deleted directly to the eqvt thm-list"]) #> + PureThy.add_thms_dynamic (@{binding "eqvt"}, content); end;