Email Gateway (Aug 19 2022 at 16:13): Email Gateway (Aug 19 2022 at 16:13):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear all,
playing a little bit further, I could establish part of what I wanted by using lift_def_cmd and
converting types and terms back to strings (which are immediately parsed again in lift_def_cmd)
fun lift_def_ml (binding,mixfix) ty rhs ctxt tactic =
let val ctxt' = Config.put show_markup false ctxt
val term_to_string = Print_Mode.setmp [] (Syntax.string_of_term ctxt')
val typ_to_string = Print_Mode.setmp [] (Syntax.string_of_typ ctxt')
val state = Lifting_Def.lift_def_cmd
((binding, SOME (typ_to_string ty), mixfix), term_to_string rhs, []) ctxt
in
state
end
However, now I am left with turning a Proof.state into a context again (which should be done
via the provided tactic). So, is there some common function of type
state -> tactic -> context
In proof.ML I only found functions like
global_qed which take "Method.text_range option * bool", but no tactics.
Kind regards,
René
Email Gateway (Aug 19 2022 at 16:16):From: Makarius <makarius@sketis.net>
Just syntactically, this one works out, but I did not try it on concrete
examples:
val term_to_string = YXML.string_of_body o Term_XML.Encode.term;
val typ_to_string = YXML.string_of_body o Term_XML.Encode.typ;
fun lift_def_ml (binding, mx) ty rhs tactic lthy =
let
val method = (Method.Basic (SIMPLE_METHOD o tactic), Position.no_range);
in
lthy
|> Lifting_Def.lift_def_cmd
((binding, SOME (typ_to_string ty), mx), term_to_string rhs, [])
|> Proof.global_terminal_proof (method, NONE)
end
I have made this a bit more canonical according to Isabelle/ML standards,
concerning names and argument order. In particular, a lthy: local_theory
value should not be called "ctxt". See the "implementation" manual for
further important information on Isabelle/ML.
The YXML representation of typ/term values should help to circumvent the
accidental omission of proper ML programming interfaces: the inner syntax
parser understands that funny machine-oriented notation. Printing terms
for parsing them again should never be done in real life.
The Proof.global_terminal_proof is "by method" in Isar syntax.
You've put the term "ML-level of Isabelle" into the subject line. This is
leading to bad things as encountered here: people then wrongly think that
Isabelle/ML somehow happens in a cold and damp cellar, and "users" are
only found in Isar syntax (but I call the second category "end-users").
The comments in $ISABELLE_HOME/src/HOL/Tools/Lifting/lifting.ML use the
term "user-friendly" for lift_def_cmd in this defective sense: only a
source text interface, without a regular ML entry point (without the
"_cmd" suffix). It is quite awkward to imitate surface Isar syntax
wrapping in ML.
Isabelle/ML programming is a normal Isabelle user activity, happing at the
main user-level of Isabelle. Any package should provide normal ML
programming interfaces in parallel to the end-user version -- there are
standard patterns to fold the two implementations into one.
Makarius
Email Gateway (Aug 19 2022 at 16:17):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear Makarius,
However, now I am left with turning a Proof.state into a context again (which should be done via the provided tactic). So, is there some common function of type
state -> tactic -> context
In proof.ML I only found functions like
global_qed which take "Method.text_range option * bool", but no tactics.
Just syntactically, this one works out, but I did not try it on concrete
examples:val term_to_string = YXML.string_of_body o Term_XML.Encode.term;
val typ_to_string = YXML.string_of_body o Term_XML.Encode.typ;fun lift_def_ml (binding, mx) ty rhs tactic lthy =
let
val method = (Method.Basic (SIMPLE_METHOD o tactic), Position.no_range);
in
lthy
|> Lifting_Def.lift_def_cmd
((binding, SOME (typ_to_string ty), mx), term_to_string rhs, [])
|> Proof.global_terminal_proof (method, NONE)
end
thanks a lot, that works perfectly in my setting.
I have made this a bit more canonical according to Isabelle/ML standards, concerning names and argument order. In particular, a lthy: local_theory value should not be called "ctxt". See the "implementation" manual for further important information on Isabelle/ML.
done.
You've put the term "ML-level of Isabelle" into the subject line.
I'll try to use Isabelle/ML the next time.
Cheers,
René
Email Gateway (Aug 19 2022 at 16:23):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear all,
I have a question regarding the lifting package.
Is there some canonical way of simulating
lift_definition name :: typ is term <proof>
on the ML-level (where <proof> might be replaced by some tactic)
In the current interface I only found
val add_lift_def:
(binding * mixfix) -> typ -> term -> thm -> thm list -> local_theory -> local_theory
val lift_def_cmd:
(binding * string option * mixfix) * string * (Facts.ref * Args.src list) list -> local_theory -> Proof.state
where add_list_def seems more closely to what I need, but I have no clue what "thm" and "thm list" are good for.
If there would be something like the following, then everything is clear,
val add_lift_def:
(binding * mixfix) -> typ -> term -> tactic -> local_theory -> local_theory
but with the current add_lift_def and passing some thm and an empty thm list, I got complaints that
exception THM 1 raised (line 332 of "drule.ML"):
RSN: no unifiers
P defau
rel_fun (eq_onp (λx. x ∈ {(b, c). c ⟶ P b})) (eq_onp P) ?c ?c ⟹
?c' ≡ map_fun Test.Rep_restricted_cond Abs_restricted ?c ⟹
rel_fun Test.cr_restricted_cond cr_restricted ?c ?c'
Do I really have to create a theorem that unifies against internals in the lifting construction?
rel_fun (eq_onp (λx. x ∈ {(b, c). c ⟶ P b})) (eq_onp P) ?c ?c ⟹
?c' ≡ map_fun Test.Rep_restricted_cond Abs_restricted ?c ⟹
rel_fun Test.cr_restricted_cond cr_restricted ?c ?c' ?
To compare with, if I invoke the lift_definition command manually, the proof goal is
⋀prod. prod ∈ {(b, c). c ⟶ P b} ⟹ P (case prod of (b, c) ⇒ if c then b else defau)
so, some proof goal that I can easily discharge using "P defau" by (simp split: prod.splits)
Kind regards,
René
Last updated: Apr 27 2024 at 01:05 UTC