Email Gateway (Nov 19 2024 at 21:41): Email Gateway (Nov 19 2024 at 21:41):From: Burkhart Wolff <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
I found a behaviour that is quite mysterious to me, and
would like to know if someone can help me out.
The condensed version of my tactic program looks like this:
>
ML‹
val SPY1 = Unsynchronized.ref(@{thm refl});
val SPY2 = Unsynchronized.ref(@{thm refl});
fun prove_ev_trans st =
let val _ = (SPY2:= st) in
case Thm.concl_of st of
@{term True} => all_tac st
| @{term False}=> all_tac st
end;
›
lemma HH5: "P XXX (2::int) XX "
apply(tactic ‹COND (fn thm => (SPY1:=thm; true)) all_tac all_tac›)
apply(tactic ‹prove_ev_trans ›)
sorry
ML‹Thm.concl_of(!SPY1);
Thm.concl_of(!SPY2);
›
<<<<<<<<<<<<<<<<<<<<<<
Do not worry that the body of prove_ev_trans is quite nonsensical and
do not worry that apply(tactic ‹prove_ev_trans ›) fails after all.
What really bothers me is the very different outcome in SPY1 and SPY2:
>
ML‹Thm.concl_of(!SPY1);
Thm.concl_of(!SPY2);
›
val it =
Const ("Pure.prop", "prop ⇒ prop") $
(Const ("HOL.Trueprop", "bool ⇒ prop") $
(Free ("P", "'a ⇒ int ⇒ 'b ⇒ bool") $ Free ("XXX", "'a") $
(Const ("Num.numeral_class.numeral", "num ⇒ int") $
(Const ("Num.num.Bit0", "num ⇒ num") $ Const ("Num.num.One", "num"))) $
Free ("XX", "'b"))):
term
val it = Const ("Pure.prop", "prop ⇒ prop") $ (Const ("Pure.term", "prop ⇒ prop") $ Const ("Pure.dummy_pattern", "prop")): term
<<<<<<<<<<<<<<<<
So, already in the call of the second tactic “” call the content of the thm is reduced to
Const ("Pure.dummy_pattern", "prop”)
(* it does not depend on the first
apply(tactic ‹COND (fn thm => (SPY1:=thm; true)) all_tac all_tac›)
call, commenting it out results in the same *)
Can someone explain this and better: find a way around this ?
I assume that this is connected to internal goal protection.
But I need the possibility to peek into the current proof state in
order to realise a very large case-match efficiently.
Best regards,
Burkhart
Email Gateway (Nov 23 2024 at 12:13):From: Burkhart Wolff <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
I found a behaviour that is quite mysterious to me, and
would like to know if someone can help me out.
The condensed version of my tactic program looks like this:
>
ML‹
val SPY1 = Unsynchronized.ref(@{thm refl});
val SPY2 = Unsynchronized.ref(@{thm refl});
fun prove_ev_trans st =
let val _ = (SPY2:= st) in
case Thm.concl_of st of
@{term True} => all_tac st
| @{term False}=> all_tac st
end;
›
lemma HH5: "P XXX (2::int) XX "
apply(tactic ‹COND (fn thm => (SPY1:=thm; true)) all_tac all_tac›)
apply(tactic ‹prove_ev_trans ›)
sorry
ML‹Thm.concl_of(!SPY1);
Thm.concl_of(!SPY2);
›
<<<<<<<<<<<<<<<<<<<<<<
Do not worry that the body of prove_ev_trans is quite nonsensical and
do not worry that apply(tactic ‹prove_ev_trans ›) fails after all.
What really bothers me is the very different outcome in SPY1 and SPY2:
ML‹Thm.concl_of(!SPY1);
Thm.concl_of(!SPY2);
›
val it =
Const ("Pure.prop", "prop ⇒ prop") $
(Const ("HOL.Trueprop", "bool ⇒ prop") $
(Free ("P", "'a ⇒ int ⇒ 'b ⇒ bool") $ Free ("XXX", "'a") $
(Const ("Num.numeral_class.numeral", "num ⇒ int") $
(Const ("Num.num.Bit0", "num ⇒ num") $ Const ("Num.num.One", "num"))) $
Free ("XX", "'b"))):
term
val it = Const ("Pure.prop", "prop ⇒ prop") $ (Const ("Pure.term", "prop ⇒ prop") $ Const ("Pure.dummy_pattern", "prop")): term
<<<<<<<<<<<<<<<<
So, already in the call of the second tactic “” call the content of the thm is reduced to
Const ("Pure.dummy_pattern", "prop”)
(* it does not depend on the first
apply(tactic ‹COND (fn thm => (SPY1:=thm; true)) all_tac all_tac›)
call, commenting it out results in the same *)
Can someone explain this and better: find a way around this ?
I assume that this is connected to internal goal protection.
But I need the possibility to peek into the current proof state in
order to realise a very large case-match efficiently.
Best regards,
Burkhart
Last updated: Jan 04 2025 at 20:18 UTC