Email Gateway (Aug 19 2022 at 16:48): Email Gateway (Aug 19 2022 at 16:48):From: Joachim Breitner <breitner@kit.edu>
Hi,
I have another Isabelle/ML beginner’s question, and hope to get some
help with a tricky point.
My goal is to program some automation around inductive predicate and
inductive proofs. At some point, I have theorems which match precisely
the assumption of the induct theorem of an inductive predicate. I.e.
foo.induct:
"!! P a b.
foo a b ==>
(!! x y. Q1 y x ==> Q2 y x ==> P x y) ==>
(!! x y z. foo x y ==> P x z ==> P y z) ==>
P a b"
hyp1: "(!! x y. Q1 y x ==> Q2 y x ==> some_P x y)"
hyp2: "(!! x y z. foo x y ==> some_P x z ==> some_P y z)"
what is the proper way to obtain
some_P: "!! a b . foo a b ==> some_P a b"
from this?
Naively, I would expect something like foo.induct[meta_OF _ hyp1 hyp2]
to exist, but could not find such a thing.
It would of course work with the equivalent of
lemma some_P: "!! a b . foo a b ==> some_P a b"
apply (rule foo.induct)
apply assumption
apply (rule hyp1)
apply assumption
apply assumption
apply (rule hyp2)
apply assumption
apply assumption
done
but that seems far too fragile (i.e. how many assumptions? What if the
there are multiple unifiers along the way, before the next assumption
determines the choice?) when a direct unification of the non-atomic
terms appears to be so much more reliable and predictable.
Thanks,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 16:48):From: Dmitriy Traytel <traytel@in.tum.de>
Hi Joachim,
in my experience, a backwards proof (your apply script) is usually less
fragile than a forward proof (meta_OF if existed).
Finding out "How many assumptions?" is easy (or even not necessary):
rtac hyp1 THEN_ALL_NEW atac
To avoid HO problems, you will probably find the need to instantiate P
from foo.induct with some_P (look for usages of Drule.instantiate' and
friends in src/HOL/Tools to see some examples).
Hope that helps,
Dmitriy
Email Gateway (Aug 19 2022 at 16:48):From: Thomas Sewell <thomas.sewell@nicta.com.au>
If you really need to use it, there is a primitive compose operation
which is available via compose_tac, Thm.bicompose etc in the ML sources.
This avoids some of the normal automation done around the meta-operators.
This can be used in your case, e.g:
ML_val {*
val foo_induct = Thm.assume @{cprop "!! P a b.
foo a b ==>
(!! x y. Q1 y x ==> Q2 y x ==> P x y) ==>
(!! x y z. foo x y ==> P x z ==> P y z) ==>
P a b"}
val hyp1 = Thm.assume @{cprop "(!! x y. Q1 y x ==> Q2 y x ==> some_P x y)"}
val it = Thm.bicompose {flatten = false, incremented = false, match = false}
(false, hyp1, 0)
2
@{thm foo_induct}
|> Seq.list_of
*}
(I tried to do this using the structured mechanisms to create
foo_induct, hyp1 etc, and then Isabelle really wanted to export hyp1 as
"Q1 ?y ?x ==> Q2 ?y ?x ==> some_P x y" which won't work with bicompose.)
I'm not sure if the result is exactly what you want, but maybe it helps.
Cheers,
Thomas.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 19 2022 at 16:49):From: Makarius <makarius@sketis.net>
This belongs to the "do not try it at home" category. The COMP family
with its many options and modes is sometimes given as secret advice, but
it requires a lot of thinking around it to get it really right. It is
easier to stick to the normal way of things around the RS/OF family.
Note that in most situations COMP_INCR or INCR_COMP is actually needed
instead of COMP without the increment mode.
Makarius
http://stop-ttip.org 1,122,353 people so far
Email Gateway (Aug 19 2022 at 17:10):From: Joachim Breitner <breitner@kit.edu>
Hi List,
not sure if it is any better from the point of view of someone who has
experience with ML, but I found this idiom to be quite useful to
discharge assumptions in thm, when I know that the thms in hyp_thms
match its assumptions up to unification:
val thm' = rule_by_tactic ctxt (EVERY1 (map (single #> solve_tac) hyp_thms)) thm
Maybe this will finally quench my putative thirst for a META_OF :-)
Greetings,
Joachim
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC