Hi Dylan,
What I would try in HOL Light:
# g `a ==> b /\ c ==> d /\ e ==> k`;;
Warning: Free variables in goal: a, b, c, d, e, k
val it : goalstack = 1 subgoal (1 total)
`a ==> b /\ c ==> d /\ e ==> k`
# e (REPEAT DISCH_TAC);;
val it : goalstack = 1 subgoal (1 total)
0 [`a`]
1 [`b /\ c`]
Here's an old-school solution:
fun locate P left [] = NONE
| locate P left (h::t) =
if P h then
SOME (rev left, h, t)
else
locate P (h::left) t;
fun ASM_CONJ_TAC (asl,c) =
case locate is_conj [] asl
of NONE => raise ERR "ASM_CONJ_TAC" "no conj in assums"
| S
Hello,
On 06/28/2018 11:44 PM, Dylan Melville wrote:
Also, the version Im using is HOL - Light
On Jun 28, 2018, at 5:38 PM, Dylan Melville wrote:
Is there a tactic for splitting conjoined assumptions into separate assumptions?
In HOL-Light you can try using CONJ_PAIR[1] for an assumption o
Also, the version Im using is HOL - Light
> On Jun 28, 2018, at 5:38 PM, Dylan Melville wrote:
>
> Is there a tactic for splitting conjoined assumptions into separate
> assumptions?
--
Check out the vibrant tech commu
In HOL4, “fs[]” may do what you want.
On 28/06/18 16:38, Dylan Melville wrote:
> Is there a tactic for splitting conjoined assumptions into separate
> assumptions?
> --
> Check out the vibrant tech community on one of the
I think a good start to tracking it down would be to remove tactics from the
end of 't' (starting with 't2') until it doesn't fail. Then check that the
resulting goal states are alpha-equivalent. If they are then the culprit
should be the next tactic, otherwise carry on going back until the goal
Yes, I was not claiming that b() is the problem. I am just curious as to
why the tactic fails when I apply it a second time, since I can't find any
explicit use of references, and I think I'm only using tactics from bossLib
(and lcsymtacs).
On Mon, Jun 17, 2013 at 1:58 PM, Konrad Slind wrote:
>
t (top_goal());
val it = ([], fn): goal list * validation
t (top_goal());
Exception- HOL_ERR {message = "first subgoal not solved by second tactic",
origin_function = "THEN1", origin_structure = "Tactical"} raised
I didn't think there were any refs touched by t, but I'll have a look more
closely..
> Could you perhaps tell me what could possibly be behind the behaviour
above?
Superficial answer: refs
Do you get the same behaviour if you invoke t away from the goalstack?
t (top_goal()) = t (top_goal())
Konrad.
On Sun, Jun 16, 2013 at 3:03 PM, Ramana Kumar wrote:
> I have run into st
