Email Gateway (Aug 22 2022 at 13:39): Email Gateway (Aug 22 2022 at 13:39):From: Peter Lammich <lammich@in.tum.de>
Hi List,
I have a problem with Specification.definition:
I want to implement the following functionality on ML-level:
context
fixes a::'a
begin
(* Want to implement these 3 definitions: *)
definition "bar = ((a,1::nat),(a,True))"
definition "foo b = (a,b)"
lemmas test = bar_def[folded foo_def]
>>> theorem test: local.bar = (local.foo 1, local.foo True)
My first attempt was:
context
fixes a::'a
begin
local_setup ‹fn lthy => let
val ((_,(_,bar'_thm)),lthy) = Specification.definition (NONE,
((Binding.empty,[]),@{prop "bar' = ((a,1::nat),(a,True))"})) lthy
val ((_,(_,foo'_thm)),lthy) = Specification.definition (NONE,
((Binding.empty,[]),@{prop "foo' b = (a,b)"})) lthy
val _ = @{make_string} [foo'_thm, bar'_thm] |> tracing
val test_thm = Local_Defs.fold lthy [foo'_thm] bar'_thm
val (_,lthy) = Local_Theory.note ((@{binding test'},[]),
[test_thm]) lthy
in
lthy
end
›
thm test'
However, the theorem does not look as expected, foo is not folded. A
quick inspection of the generated theorems (see tracing-output) quickly
reveals the reason for that:
tracing output is:
["foo' ?b = (a, ?b)" [.], "bar' = ((a, 1), a, True)" [.]]
where foo' and bar' are free variables (!) rather than constants, and
the type of ?b is ?b::'b, which, obviously, does not unify with nat nor
bool.
My question:
What is the correct way to implement the above in Isabelle-ML?
Is there a way to get a _def-theorem that contains a Const rather than
a Free, and a ?b::?'b rather than ?b::'b ?
Thanks in advance for any help,
Peter
Email Gateway (Aug 22 2022 at 13:39):From: Lars Hupel <hupel@in.tum.de>
Hi Peter,
that you get frees/tfrees out of Specification.definition is as
expected. In order to obtain something with schematic variables, you
need to look, or rather, obtain the "foundation" of the newly-introduced
definitions. This can be done with appropriate morphisms:
local_setup ‹fn lthy =>
let
val (_, lthy') = Local_Theory.open_target lthy
val ((_,(_,bar'_thm)),lthy') = Specification.definition
(NONE, ((Binding.empty,[]),
@{prop "bar' = ((a,1::nat),(a,True))"})) lthy'
val ((_,(_,foo'_thm)),lthy') = Specification.definition
(NONE, ((Binding.empty,[]),@{prop "foo' b = (a,b)"})) lthy'
val _ = map (Thm.pretty_thm lthy') [foo'_thm, bar'_thm]
|> Pretty.big_list "before" |> Pretty.writeln
val lthy'' = Local_Theory.close_target lthy'
val phi = Proof_Context.export_morphism lthy' lthy''
val foo'_thm = Morphism.thm phi foo'_thm
val bar'_thm = Morphism.thm phi bar'_thm
val _ = map (Thm.pretty_thm lthy') [foo'_thm, bar'_thm]
|> Pretty.big_list "after" |> Pretty.writeln
val test_thm = Local_Defs.fold lthy'' [foo'_thm] bar'_thm
val (_, lthy'') =
Local_Theory.note ((@{binding test'},[]), [test_thm]) lthy''
in
lthy''
end›
thm test'
The pattern open_target/close_target is used all over BNF, presumably
with the same intent, although I'm not quite sure whether I've
reproduced it fully canonically here.
Cheers
Lars
Last updated: Apr 30 2024 at 01:06 UTC