Don’t use abbreviations before starting your proof: it’s muddling your
quantifications.
Instead, use
!s. (?s0. s = StreamD s0) /\ P s ==> streams A s
as your goal and follow with
ho_match_mp_tac streams_coind >> dsimp[]
You will then end up with
∀s0.
P (StreamD s0) ⇒
∃a s0
Hi,
I see that the coinduction scheme obtained from coinductively definition
predicate, in some cases, may require lazy list must not be LNIL. For
instance,
using the LUNFOLD, I've defined the stream function mainly to rule out the
LNIL case as:
|- StreamD xs = LUNFOLD (\n. SOME (THE (LTL n),THE
The assumption of the rewrite theorem is not present in the assumptions of the
goal and so you get an invalid tactic.
Strictly speaking this is not REWRITE_TAC failing but e. Indeed, you should
find that REWRITE_TAC [second_b13_complete] applied to the goal works just fine.
Michael
From: Dyl
VERSION: HOL Light QE (augmentation of HOL Light, very similar)
Hello all. Today I’ve been having 2 issues with HOL. The first is that although
the documentation for REWRITE_TAC says that the tactic has no failure
conditions, when I use the following command:
# e (REWRITE_TAC[second_b13_complet
Two minor followups:
- there is evidently a bug in the position information when the leading
delimiter is a Unicode quote mark (the number of bytes gets counted rather than
the number of "characters");
- the unquote filter is built by the process of "configuring" the system before
building; act
The quotation filter doesn't really do any tokenization other than to spot
occurrences of the magic term and quotation delimiters:
` .. ` (a quotation)
‘ .. ’ (also a quotation, but with non-identical delimiters)
``:ty`` (an application of the type parser to a quotation)
“:ty”( dit
Dear experts on antiquotations HOL4,
I've looked through tools/Holmake/QuoteFilter, but could not read the
input format -- I am used to functional parser combinators instead of
lex + yacc.
Is there a specification of the input syntax in the documentation? But
it is also changing occasionally, so
