*To*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] How to obtain all type variables declared in a proof context?*From*: mailing-list anonymous <mailing.list.anonymous at gmail.com>*Date*: Mon, 15 Jul 2019 17:11:24 +0300*Cc*: Alexander Krauss <krauss at in.tum.de>*In-reply-to*: <842be78f-41bf-edfc-1d63-72b96a00f5f7@in.tum.de>*References*: <CALaF1UJN1EyB6VZhrtDgo0u9c+DPOH2TH0+8SsthhVYVZMLcmQ@mail.gmail.com> <842be78f-41bf-edfc-1d63-72b96a00f5f7@in.tum.de>

Dear Alexander Krauss/All, Thank you for your reply. It is very useful to know that the functionality that I was looking for is not available. Indeed, my problem is slightly superficial and, generally, can be resolved by following one of the more traditional approaches, like the one that you suggested at the end of your email. Nevertheless, it seems that using such traditional approaches would result in redundant computations, given the problem at hand. Perhaps, there is another way to proceed. I would like to know if there is a way to reduce all indexnames in a theorem to zero in a context-aware fashion (please note that I am aware of the function Drule.zero_var_indexes, but it ignores the local context). Such a function could provide an efficient alternative to the solution of the problem that I am dealing with. As a side note, it seems that making a functionality that shows all entities declared in a context or, better yet, a context difference function would be very useful for the purposes of inspection/testing/verification/debugging. For example, I would like to ensure that my modules do not leave any redundant entities in the context. Given the information in your previous email, it seems that this is something that one cannot do at the moment. I would also like to make another remark that has some connection to the problem that I was trying to solve. I encountered a behaviour which I find difficult to understand. Somehow, given a locale context with declared (type) variables, it is still possible to register theorems in the locale context that, seemingly, ignore the sorts/types associated with the previously declared variables (see the code listing after my signature). Somehow, I was under the (seemingly, erroneous) impression that, unlike constants, variables are only allowed to have one type/sort in the same context... does there exist any documentation that explains this behaviour? The only references that I could find on this matter were in the implementation manual (p. 65 and p. 69): 1. "The core logic handles the type variables with the same name but different sorts as different, although the type-inference layer (which is outside the core) rejects anything like that." 2. "Type-inference rejects variables of the same name, but different types. In contrast, mixed instances of polymorphic constants occur routinely." However, these references do not explicitly state that it is, indeed, legal and appropriate to use the same variable with different type/sort in the same context. Why are the users allowed to forego a type inference before registering a theorem in a context or creating a proveable goal? Are there any practical use cases for this allowance? Most certainly, it enables the construction of slightly peculiar theorems. For example, I was able to produce the following theorem (see the code listing below): "(B::'b::plus) = B ⟹ B::'b::type ≡ B" Thank you declare [[show_sorts]] locale myloc = fixes B :: "'b::plus" assumes "B ≡ B" begin lemma tt: "True ≡ True" by auto ML ‹ val T = TVar (("'a", 0), ["Groups.plus"]); fun mk_eq_thm lthy = let val T = TVar (("'a", 1), ["HOL.type"]); val ct = Var (("A", 0), T) |> Thm.cterm_of lthy; val thm = ct |> Thm.reflexive; val lthy = Local_Theory.note ((@{binding mythm}, []), single thm) lthy |> snd in lthy end val q = Thm.implies_intr fun mk_eq_thm' lthy = let val T = TFree ("'b", ["HOL.type"]) val ct = Free ("B", T) |> Thm.cterm_of lthy val thm = ct |> Thm.reflexive val thm = Thm.implies_intr (@{term True} |> HOLogic.mk_Trueprop |> Thm.cterm_of lthy) thm val lthy = Local_Theory.note ((@{binding mythm'}, []), single thm) lthy |> snd in lthy end › local_setup ‹Local_Theory.target (Variable.declare_typ T)› (* Both produce an error similar to "Sort constraint type inconsistent with default plus for type variable "?'a"⌂": schematic_goal "(?A::?'a::type) = ?A" lemma "(Q::'b::type) = (Q::'b::type)" *) local_setup ‹mk_eq_thm› local_setup ‹mk_eq_thm'› thm mythm (* ?A::?'a::type ≡ ?A *) thm mythm' (* B::'b::type ≡ B *) (* peculiar theorem *) lemma QQ: "True" proof- (* the occurrences of B have different types in the goal *) define C where "C = (B = B)" have True_C: "C = True" unfolding C_def by auto have aaa: "True" by auto note mythm'' = mythm'[folded True_C, unfolded C_def] thm mythm'' (* (B::'b::plus) = B ⟹ B::'b::type ≡ B *) show ?thesis by auto qed (* It seems that it is possible to produce theorems in the locale context that use the default sort 'type' both for the schematic type variable with the indexname ("'a", 0) and the fixed type variable with the name 'b, as well as the type "'b::type" for the fixed variable B. Nevertheless, the sorts of the declared types are still 'Groups.plus'. This can be observed by trying to state the lemmas from the previous example: schematic_goal "(?A::?'a::type) = ?A" lemma "(Q::'b::type) = (Q::'b::type)" which results in the same error as before. *) end On Mon, Jul 15, 2019 at 10:18 AM Alexander Krauss <krauss at in.tum.de> wrote: > Am 14.07.2019 um 18:03 schrieb mailing-list anonymous: > > I am trying to obtain a list of all type variables that are declared > > in a proof context. It does not seem that the relevant data is exposed to > > the public interface. > > Yes, I think this is not exposed. As I understand it, it is more of an > implementation detail, and the "invent fresh names" operations are what > you are supposed to use. > > [...] > > > The use case is the generation of fresh schematic type variables. > > In this case, I would probably generate fixed type variables first (cf. > Variable.invent_types) and then generalize the final results (terms, > theorems) (cf. Variable.export_*) > > Hope this helps > > Alex > -- Please accept my apologies for posting anonymously. This is done to protect my privacy. I can make my identity and my real contact details available upon request in private communication under the condition that they are not to be mentioned on the mailing list.

**References**:**[isabelle] How to obtain all type variables declared in a proof context?***From:*mailing-list anonymous

**Re: [isabelle] How to obtain all type variables declared in a proof context?***From:*Alexander Krauss

- Previous by Date: Re: [isabelle] Non-ASCII characters and unsupported text structures
- Next by Date: Re: [isabelle] Non-ASCII characters and unsupported text structures
- Previous by Thread: Re: [isabelle] How to obtain all type variables declared in a proof context?
- Next by Thread: [isabelle] KTH announces 8 PhD student positions in cyber security
- Cl-isabelle-users July 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