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



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.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.