Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] [isabelle-dev] Syntax.read_term ctxt

Email Gateway (Aug 18 2022 at 17:20):

From: e0726734@student.tuwien.ac.at
thank you for looking at my question!
but as far as i can see there seems to be a misunderstanding
(#####################)
so i kindly ask once more:

---- Makarius <makarius@sketis.net> wrote:

On Thu, 3 Mar 2011, bonzai@inode.at wrote:

i studied isabelle/isar implementation, isabelle/isar reference
manual and the isabelle cookbook.
what am i still doing wrong ?

structure Data = Proof_Data
(type T = term list
fun init _ = []);
val ctxt =
ProofContext.init_global @{theory} |>
Data.map (fn ts => @{term "x::int"}::ts);
#############################------######
Data.get ctxt;

Syntax.read_term ctxt "x + 1 = 2";
(* we get Free ("x", "'a") etc, but would expect ...
##############################----------------##
val it =
Const ("HOL.eq", "Int.int \<Rightarrow> Int.int \<Rightarrow>
HOL.bool") $
(Const ("Groups.plus_class.plus", "Int.int \<Rightarrow> Int.int
\<Rightarrow> Int.int") $
Free ("x", "Int.int") $ Const ("Groups.one_class.one", "Int.int")) $
#################------###################
(Const ("Int.number_class.number_of", "Int.int \<Rightarrow>
Int.int") $
(Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $
(Const ("...", "Int.int \<Rightarrow> Int.int") $
Const ("Int.Pls...", "Int.int")))):
term
*)

I cannot reproduce the problem. This is the output of ML toplevel
declarations produced here:

structure Data : PROOF_DATA
val ctxt = <context>: Proof.context
val it = [Free ("x", "Int.int")]: Data.T
val it =
Const ("HOL.eq", "'a \<Rightarrow> 'a \<Rightarrow> HOL.bool") $
(Const ("Groups.plus_class.plus", "'a \<Rightarrow> 'a
\<Rightarrow> 'a") $ Free ("x", "'a") $
###########################################################################-----####
(we would like to have Int.int here
##################################################################################
Const ("Groups.one_class.one", "'a")) $
(Const ("Int.number_class.number_of", "Int.int \<Rightarrow> 'a") $
(Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $
(Const ("...", "Int.int \<Rightarrow> Int.int") $ Const
("Int.Pls...", "Int.int")))):
term
[...]
* You can ask questions about Isabelle/ML on the isabelle-users mailing
list. isabelle-dev means you are hooked on unofficial repository
versions for some reason, in which case you should also say which
one it is (e.g. via isabelle version -i).

Makarius

Thank you very much for any help,
Mathias Lehnfeld

Email Gateway (Aug 18 2022 at 17:20):

From: Makarius <makarius@sketis.net>
This is getting increasingly hard to read. Note that he private Data slot
is really just a list of terms that the system maintains for you in
Proof.context. Its meaning is determined by what you do with it in user
code -- the system ignores it.

This means the Syntax.read_term produces a term according to the regular
context, and there "x" is undeclared. So "x + 1 = 2" gets a very general
type.

Here is an example (in Isabelle2011) that illustrates how to use the
context for locally fixed variables, potentially with type constraints
(these are two different things):

notepad
begin
term "x + 1 = 2" -- {* x undeclared; general type *}

fix x :: int -- {* x locally fixed, with type constraint *}
term "x + 1 = 2"
end

notepad
begin
ML_val {*
val ctxt = @{context};
val (_, ctxt') = ProofContext.add_fixes [(@{binding x}, SOME @{typ int}, NoSyn)] ctxt;
val t = Syntax.read_term ctxt "x + 1 = 2";
val t' = Syntax.read_term ctxt' "x + 1 = 2";
*}
end

As a general principle, whenever there is some surprise about results it
is often due to "bad context", cf. ctxt vs. ctxt' above.

Makarius

Last updated: Apr 25 2024 at 20:15 UTC