*To*: mailing-list anonymous <mailing.list.anonymous at gmail.com>*Subject*: Re: [isabelle] Amending an existing locale interpretation with additional rewrite rules*From*: Clemens Ballarin <ballarin at in.tum.de>*Date*: Tue, 24 Sep 2019 21:30:43 +0200*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <CALaF1UJd9na0SCWvRz2OTUT3Vqy+CginyR233qb3vxnPDvEvNg@mail.gmail.com>*References*: <CALaF1UJd9na0SCWvRz2OTUT3Vqy+CginyR233qb3vxnPDvEvNg@mail.gmail.com>*User-agent*: Roundcube Webmail/1.3.3

Clemens On 2019-09-20 19:02, mailing-list anonymous wrote:

Dear All, I would like to amend a locale interpretation with additional rewriterules. A (nearly) minimal example in the code listing below summarisestheproblem. I also make an attempt to explain my problem explicitly in the form of the following enumerated list:1. I create locales A and B and provide an interpretation of A in Bviathe command sublocale.2. After the interpretation, I provide several new constants withtheintention to state additional theorems about these constants in thecontextof A. 3. Once the constants are introduced, I would like to add additionalrewrite rules (for these constants) to the existing interpretationof A inB in a way such that the theorems stated in the context of A aftertheintroduction of the rewrite rules appear in their rewritten form inthecontext of B. I would like to know if this is something that can beachieved using the existing technology: a naive approach ofreinterpretingA in B with the new rewrite rules fails. section ‹Example› theory example imports Main begin locale ord = fixes le :: "'a ⇒ 'a ⇒ bool" (infix "≤⇩T" 50) and ls :: "'a ⇒ 'a ⇒ bool" (infix "<⇩T" 50) begin notation le ("'(≤⇩T')") and le (infix "≤⇩T" 50) and ls ("'(<⇩T')") and ls (infix "<⇩T" 50) abbreviation (input) ge (infix "≥⇩T" 50) where "x ≥⇩T y ≡ y ≤⇩T x" abbreviation (input) gt (infix ">⇩T" 50) where "x >⇩T y ≡ y <⇩T x" end locale preorder = ord le ls for le ls + assumes less_le_not_le: "ls x y ⟷ le x y ∧ ¬ (le y x)" and order_refl[iff]: "le x x" and order_trans: "le x y ⟹ le y z ⟹ le x z" locale preorder_dual = preorder context preorder_dual begin (* if the following interpretation is deleted, then the desired behaviour is achieved *) sublocale dual: preorder ge gt apply unfold_locales subgoal using less_le_not_le by blast subgoal by auto subgoal using order_trans by blast done end (* new definitions *) definition min :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ 'a" where "min le a b = (if le a b then a else b)" definition max :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ 'a" where "max le a b = (if le b a then a else b)" (* an attempt to reinterpret preorder in preorder_dual *) context preorder_dual begin sublocale dual: preorder ge gt rewrites "min ge ≡ max le" sorry end (* new theorems in preorder *) context preorder begin lemma min_absorb1: "x ≤⇩T y ⟹ min le x y = x" by (simp add: min_def) (*at this point dual.min_absorb1 does not exist *) end(*Demonstration of the failed attempt to introduce an additionalrewriterule*) context preorder_dual begin thm dual.min_absorb1 (* thm dual.min_absorb1 returns y ≤⇩T x ⟹ min (λx y. y ≤⇩T x) x y = x instead of the desired y ≤⇩T x ⟹ max le x y = x *) end end Thank you

**Follow-Ups**:**Re: [isabelle] Amending an existing locale interpretation with additional rewrite rules***From:*mailing-list anonymous

**References**:**[isabelle] Amending an existing locale interpretation with additional rewrite rules***From:*mailing-list anonymous

- Previous by Date: Re: [isabelle] Bad file 'root.tex'
- Next by Date: Re: [isabelle] Locale diagnostics
- Previous by Thread: [isabelle] Amending an existing locale interpretation with additional rewrite rules
- Next by Thread: Re: [isabelle] Amending an existing locale interpretation with additional rewrite rules
- Cl-isabelle-users September 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list