Email Gateway (Aug 22 2022 at 20:30): Email Gateway (Aug 22 2022 at 20:30):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear Alexander Krauss,
Thank you for your reply. It is very useful to know that it is very
unlikely that it is possible to develop a general-purpose infrastructure
for the interpretation with quantification over types. At the very least it
gives me a certain level of confidence in that the methodology that I have
developed for my application cannot be significantly improved.
Email Gateway (Aug 22 2022 at 20:40):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
Part 1
I am in need of an infrastructure that provides a functionality similar to
the locale interpretation mechanism but allows one to work with the
assumptions that contain implicit quantification over types modelled via
the use of the schematic type variables (I use the word assumption in the
most general sense and not, necessarily, in the sense of the term that is
associated with the Isabelle/Pure context assumptions). Thus, for example,
given a set A that may contain terms of different types and a polymorphic
constant f::'a=>'b=>'c, such infrastructure would enable one to state that
(A, f) is a semigroup and generate the relevant semigroup theorems
automatically in their most general form.
If what I am trying to do can be easily achieved using the existing
technology, then I would appreciate if someone could point me in the right
direction. If such technology is not available at the moment, in Part 2 of
the question I describe my idea for the implementation of such
infrastructure, but also mention certain problems with this idea. I can
only hope that there exists a better solution and someone will be kind
enough to share it with me. Otherwise, I guess, I will have to proceed with
the implementation of the idea that I have already developed.
Part 2
The second part of the question is presented in the form of an Isabelle
theory (also please see the attachment):
section ‹Example›
theory example
imports Main
begin
text‹Consider the following definition of a polymorphic constant
\<^text>‹mkid›:›
definition mkid :: "'a ⇒ 'b ⇒ 'c ⇒ 'c"
where "mkid a b = id"
text‹
The constant \<^const>‹mkid› acts as a semigroup on the set of terms
\<^text>‹SG = {T. ∃σ. T::σ ⇒ σ}›,
i.e.
\<^text>‹∀a b c ∈ SG. mkid a (mkid b c) = mkid (mkid a b) c›
and
\<^text>‹∀a b ∈ SG. mkid a b = mkid b a›.
It is my understanding that the theorems above can be formalized in Isabelle
under the assumption that the schematic type variables provide a model of
the quantification over types:
›
lemma make_id_assoc:
"mkid (a::'a⇒'a) (mkid (b::'b⇒'b) (c::'c⇒'c)) = mkid (mkid a b) c"
unfolding mkid_def by simp
lemma make_id_commute: "mkid (a::'a⇒'a) (b::'b⇒'b) = mkid b a"
unfolding mkid_def by simp
text ‹Given the associativity and the commutativity of \<^const>‹mkid› it
is possible to prove the usual properties of the commutative semigroups for
\<^text>‹(SG, mkid)›:›
lemma make_id_left_commute:
"mkid (b::'b⇒'b) (mkid (a::'a⇒'a) (c::'c⇒'c)) = mkid a (mkid b c)"
by
(
rule trans[
OF make_id_assoc[
of b a c,
unfolded make_id_commute[of b a]
]
make_id_assoc[of a b c, symmetric]
]
)
text ‹More generally, consider an arbitrary polymorphic constant
\<^text>‹f›:›
consts f :: "'a ⇒ 'b ⇒ 'c"
text ‹It is possible to write a command (e.g. \<^text>‹comm_sg›) that
generates
the statement of the associativity and the commutativity from the
specification
of the constant and discharges the relevant proof obligations, e.g.
\<^text>‹comm_sg› \<^const>‹f›
proof-
show assoc: "\<^const>‹f› a (\<^const>‹f› b c) = \<^const>‹f› (\<^const>‹f›
a b) c"
for a b c
by simp
show commute: "\<^const>‹f› a b = \<^const>‹f› b a" for a b by simp
qed
›
lemma assoc: "f (a::'a) (f (b::'b) (c::'c)) ≡ f (f a b) c" sorry
lemma commute: "f (a::'a) (b::'b) ≡ f b a" sorry
text‹
Once the statements of the associativity and the commutativity are proven,
the command can generate the theorems of interest that are associated with
the
commutative semigroups for the constant \<^const>‹f›.
The problem, however, is that the only method that I can think of for
generating such theorems is forward reasoning in ML. Effectively,
the package would need to store the functions that can transform the
theorems
@{thm assoc}
and
@{thm commute}
to other theorems about commutative semigroups.
Therefore, I am curious whether there exists a methodology that could
simplify
the task of generating and proving further results given the statements
of @{thm [source] assoc} and @{thm [source] commute}. Ideally, one would
like to develop the theory of commutative semigroups in Isar and then
instantiate it for particular constants. However, I cannot immediately see
how this can be achieved.
›
ML ‹
val ctxt = @{context};
val assoc_thm = @{thm assoc};
val commute_thm = @{thm commute};
val dS = \<^sort>‹HOL.type›
fun mk_left_commute ctxt =
let
val ctxt' = Variable.variant_fixes ["a", "b", "c"] ctxt |> snd;
val aT = TFree ("'a", dS)
val bT = TFree ("'b", dS)
val cT = TFree ("'c", dS)
val fT = TFree ("'f", dS)
val at = Free ("a", aT);
val bt = Free ("b", bT);
val ct = Free ("c", cT);
val saT = TVar (("'a", 0), dS)
val sbT = TVar (("'b", 0), dS)
val scT = TVar (("'c", 0), dS)
val sfT = TVar (("'f", 0), dS)
val sat = Var (("a", 0), saT);
val sbt = Var (("b", 0), sbT);
val sct = Var (("c", 0), scT);
fun mk_insts (sTs, Ts) (sts, ts) =
let
fun mk_instsT (sTs, Ts) =
(sTs |> map dest_TVar) ~~ (Ts |> map (Thm.ctyp_of ctxt'))
val instsT = mk_instsT (sTs, Ts)
val map_terms =
(AList.lookup op= (instsT |> map (apsnd Thm.typ_of)) #> the)
|> map_type_tvar
|> map_types
val instst =
(sts |> map map_terms |> map dest_Var) ~~
(ts |> map (Thm.cterm_of ctxt))
in (instsT, instst) end
val insts = mk_insts ([saT, sbT, scT], [bT, aT, fT]) ([sat, sbt], [bt,
at])
val step1 = Drule.instantiate_normalize insts commute_thm;
val insts =
mk_insts
([saT, sbT, scT, sfT], [bT, aT, cT, fT])
([sat, sbt, sct], [bt, at, ct]);
val step2 = Drule.instantiate_normalize insts assoc_thm;
val step3 = Local_Defs.unfold ctxt' (step1 |> single) step2;
val insts =
mk_insts
([saT, sbT, scT, sfT], [aT, bT, cT, fT])
([sat, sbt, sct], [at, bt, ct]);
val step4 = assoc_thm
|> Drule.instantiate_normalize insts
|> Thm.symmetric;
val step5 = Thm.transitive step3 step4
val result = singleton (Proof_Context.export ctxt' ctxt) step5
in result end;
val left_commute_thm = mk_left_commute ctxt;
›
local_setup ‹
Local_Theory.note ((@{binding left_commute}, []), [left_commute_thm]) #> snd
›
thm left_commute
end
Thank you
example.thy
Email Gateway (Aug 22 2022 at 20:40):From: Alexander Krauss <krauss@in.tum.de>
Am 30.09.2019 um 01:51 schrieb mailing-list anonymous:
Part 1
I am in need of an infrastructure that provides a functionality similar to
the locale interpretation mechanism but allows one to work with the
assumptions that contain implicit quantification over types modelled via
the use of the schematic type variables
[...]
Part 2
Therefore, I am curious whether there exists a methodology that could
simplify
the task of generating and proving further results given the statements
of @{thm [source] assoc} and @{thm [source] commute}. Ideally, one would
like to develop the theory of commutative semigroups in Isar and then
instantiate it for particular constants. However, I cannot immediately see
how this can be achieved.
Experience suggests (but cannot prove) that there is no such methodology.
Tools in ML can help in specific well-defined cases, but a general
locale-like mechanism cannot exist, since we cannot state polymorphic
assumptions in HOL, so the main interpretation property cannot be stated
as a general theorem in HOL. So the only thing one can do is replay the
proof, which is what the ML function does.
The typical ways out of this dilemma:
Alex
Last updated: Nov 21 2024 at 12:39 UTC