Email Gateway (Aug 19 2022 at 17:06): Email Gateway (Aug 19 2022 at 17:06):From: Burkhart Wolff <Burkhart.Wolff@lri.fr>
Dear all,
is there any way to actually eliminate a parameter or a goal ?
After case-splits, parameters are often no longer of relevance.
MY PROBLEM:
============
I have something like:
"⋀S. PUT (S::(...) action⇩i⇩p⇩c)”
which I reduce via case-splitting to:
"(⋀S ipc_stage ipc_direction. PUT (IPC ipc_stage ipc_direction)) ⟹ (⋀S. PUT S)”
which I would like to reduce to:
"(⋀ ipc_stage ipc_direction. PUT (IPC ipc_stage ipc_direction)) ⟹ (⋀S. PUT S)”
(so canceling the parameter S irrelevant in the goal).
SOME ELEMENTS OF A SOLUTION:
I cooked up some sketch of a tactics which does nearly what I want:
ML{* val XX = Unsynchronized.ref(@{thm impI})
fun PEEK st = (XX:=st; all_tac st)
*}
lemma "⋀S. PUT (S::(...) action⇩i⇩p⇩c)"
apply(tactic "Induct_Tacs.case_tac @{context} \"S\" 1", hypsubst)
apply(tactic "PEEK")
oops
ML{* val st = !XX;
val thy = #thy (rep_thm (st));
val _ $ (_ $ Abs(x,ty,t)) = concl_of(st);
val cFree = cterm_of thy (Free(x,ty))
*}
ML{* val _ $ Abs(ss,_,T) = term_of (cprem_of (st) 1) ;
val T' = cterm_of thy (subst_bounds([Bound 0],T)) *}
ML{* val Q = Thm.assume T'*}
ML{* val Q' = Thm.forall_intr cFree (Q) ; *}
ML{* val Q'' = Thm.implies_intr T' Q'*}
ML{* val Q''' = Q'' RS (st)*}
Unfortunately, the very last composition step fails:
exception THM 1 raised (line 332 of "drule.ML"):
RSN: no unifiers
(⋀ipc_stage ipc_direction. PUT (IPC ipc_stage ipc_direction)) ⟹
(⋀S ipc_stage ipc_direction. PUT (IPC ipc_stage ipc_direction))
(⋀S ipc_stage ipc_direction. PUT (IPC ipc_stage ipc_direction)) ⟹ (⋀S. PUT S)
which looks bizarre. The types and class types are confrom.
Any ideas ?
Best
bu
Email Gateway (Aug 19 2022 at 17:06):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Burkhart,
I normally use apply(unfold triv_forall_equality) to get rid of all irrelevant parameters.
Best,
Andreas
Email Gateway (Aug 19 2022 at 17:07):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Burkhart,
If I wanted to do this in Isabelle 2005, I'd just try rewriting with the
following:
triv_forall_equality ;
val it = "(!!x. PROP ?V) == PROP ?V" : Thm.thm
Of course, I've no idea whether this is still available in the current
versions
Cheers,
Jeremy
Email Gateway (Aug 19 2022 at 17:07):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Burkhart,
is there any way to actually eliminate a parameter or a goal ?
This works for me:
apply (simp only: triv_forall_equality)
Cheers,
Jasmin
Last updated: Apr 25 2024 at 16:19 UTC