Hi Haitao,
You can introduce the conjunction among the antecedents as:
val GEN_IMP_TRANS_conj = (REWRITE_RULE [GSYM satTheory.AND_IMP]
GEN_IMP_TRANS);
val GEN_IMP_TRANS_conj =
⊢ ∀P Q R S. (∀x. P x ⇒ Q (R x)) ∧ (∀x. Q x ⇒ S x) ⇒ ∀x. P x ⇒ S (R x):
thm
On Tue, Mar 19, 2019 at 5:30 AM
Hi Chun,
I run some experiments so to check if it is violating any fundamental rule.
So far it went good.
On Tue, Feb 19, 2019 at 5:31 PM Chun Tian (binghe)
wrote:
> Some further updates:
>
> With my last definition of `extreal_div`, I still have:
>
> |- !x. x / 0 = ARB
>
> and
>
> |- 0 /
Hi Chun,
>
> I think it’s better to let HOL maintainers to decide if we should keep the
> old version (14,700 lines) in “examples”, e.g. “examples/old-probability”.
> I personally don’t like this idea, because the old version is always
> accessible from previous HOL releases. And there’re still
subgoal?
On Fri, Sep 21, 2018 at 3:00 AM wrote:
> match_mp_tac is indeed causing an error because it is not applicable in
> the other subgoals.
>
>
>
> Michael
>
>
>
> *From: *Waqar Ahmad via hol-info
> *Reply-To: *Waqar Ahmad <12phdwah...@seecs.edu.pk>
>
mp_tac succeeding. So the proof is failing
> before it gets to the THEN_LT.
>
> Konrad.
>
>
> On Thu, Sep 20, 2018 at 2:05 PM Waqar Ahmad via hol-info <
> hol-info@lists.sourceforge.net> wrote:
>
>> Hi,
>>
>> I'm trying to use the tactical SPLIT_
Hi,
I'm trying to use the tactical SPLIT_LT to multiple subgoals. However, I'm
facing error with assumption matching. For instance, I've a proof goal of
this form:
`(A1 ==> B1) ==> (B1 /\ SG2 /\ SG3)`
rw []
\\ (pop_assum (fn th => match_mp_tac th)) THEN_LT SPLIT_LT 1 (ALL_LT,
ALLGOALS (rw[]))
Hi,
I'd like to try converting the equality to SUBSET form by using
Pred_setTheory.SUBSET_ANTISYM (THEOREM)
---
|- !s t. s SUBSET t /\ t SUBSET s ==> (s = t)
and then use property like
topology_hvgTheory.BIGUNION_MONO_IMAGE (THEOREM) [1]
Hi,
Lately, I proved the equivalence of two supremum functions as:
|- !P.
(!x y. P x /\ P y ==> x <= y) /\ P <> {} ==>
(BIGSUP $<= P P = SOME (sup P)): thm
where BIGSUP is defined in [1] and "sup" can be found in HOL realTheory.
I'm not sure why the premise (!x y. P x /\ P
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'. (StreamD s0 = a:::StreamD s0') ∧ a ∈ A ∧ P (StreamD s0')
>
> a
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
Hi,
> I have a question about the new version of measureTheory
> (measure_hvgScript.sml): why the Carathéodory's extension theorem
> (CARATHEODORY), with all related definitions and lemmas, are removed?
>
> [CARATHEODORY]
> |- ∀m0.
> algebra (m_space m0,measurable_sets m0) ∧ positive
Hi,
I appreciate the changes that you are making but I'm still not sure that
why are you re-proving the existing properties that are present in the
latest version [1]. For instance, EXTREAL_SUM_IMAGE_INSERT is already
existed in [1] in different forms:
P_RULE (srw_ss())
> []
> |> SIMP_RULE bool_ss [COND_RAND, Once COND_RATOR]
> |> SIMP_RULE bool_ss [Once COND_RATOR]
> |> SIMP_RULE (srw_ss()) [until0_T]
>
> val until0_FNIL =
> until0_def |> Q.SPEC `P` |> Q.SPEC ‘(F,
bool_ss [Once COND_RATOR]
> |> SIMP_RULE (srw_ss()) [until0_T]
>
> val until0_FNIL =
> until0_def |> Q.SPEC `P` |> Q.SPEC ‘(F, [||])’ |> SIMP_RULE (srw_ss()) []
>
> val until_def = Define‘until P ll = until0 P (F, ll)’
>
> val until_thm = LIST_CONJ (m
Hi,
You're welcome to suggest improvements.. maybe step forward to put the
extrealTheory on right footings.. I'll be more than happy, if I could be of
any help to you at any point.
On Tue, Aug 7, 2018 at 11:56 AM Chun Tian (binghe)
wrote:
> Hi,
>
> I just want to see a textbook-correct theory
Hi,
> let me make a little more comments to the formalized extended reals.
>
> I’m actually reviewing the improved version of extrealTheory as part of
> [1] (the link "Required Theories”). I don’t know if there’re further
> updates, but comparing with the existing definitions shipped in HOL4, I
Hi all,
Is there any easy way to define the following partial function on lazy list
val recur_llist_fn_def = Define
`recur_llist_fn P w =
if P (THE (LHD w)) then [|THE (LHD w)|]
else (THE (LHD w)):::(recur_llist_fn P (THE (LTL w)))`;
Otherwise, I can also include the LNIL case as
val
Hi Chun,
I'm not sure about your potential conflict question but we are now using an
improved definition of "extreal_add_def"
val extreal_add_def = Define`
(extreal_add (Normal x) (Normal y) = (Normal (x + y))) /\
(extreal_add (Normal _) a = a) /\
(extreal_add b (Normal _) = b) /\
Hi,
You can rewrite your goal with thm2 by using
e (SIMP_TAC [GSYM thm2]);
and then use
e (SIMP_TAC [thm1]);
On Wed, Jul 18, 2018 at 4:43 PM Dylan Melville
wrote:
> I have a set of theorems, which state:
>
> let thm1 = A;;
> let thm2 = A <=> B;;
>
> And I want a theorem that states B. I tried
α llist -> (α # α llist) option
>
>
>
> For the co-algebraic numbers it’s
>
>
>
> num -> num option
>
>
>
> For arbitrarily (but finite)-branching trees, it’s
>
>
>
> Tree -> Tree list
>
>
>
> (If you change list to llist
Hi all,
I observed a strange behavior of the same tactic in HOL-k10 vs HOL-k12
Consider a proof goal
``?!m. ((m = n) \/ m < n) /\ ((if m < n then f m else a) = x)``
e (CONV_TAC(ONCE_DEPTH_CONV COND_ELIM_CONV));
(* In HOL-k10, the tactic results a desired behavior*)
?!m. ((m = n) \/ m < n) /\
I'm not sure what actually you desired with WHILE function but I can
explain its functioning that might help you to define your function.
For instance, you can define a function that continue traversing over a
list until "P h" is true otherwise return the remaining part of the list.
!P L.
(ll2 = (if LFINITE xs then LAPPEND (g (THE (LTL xs))) [|THE
(LHD xs)|]
else xs))`
but at some point in proof I cannot reason it further. Any suggestion or
comments?
>
> Michael
>
>
>
> *From: *Waqar Ahmad via hol-info <hol-info@lists.sourceforge.net>
> *
Hi,
Lately, I've been trying to define the "reverse" function on lazy lists but
I'm facing some issues. I understand that, unlike lists, in order to define
recursive function over lazy lists every time I need to justify the
definition of (co-)recursive functions (reverse in my case) that map into
“general” destructor
>
>
>
> myType -> F(myType)
>
>
>
> For lazy lists, this is
>
>
>
> α llist -> (α # α llist) option
>
>
>
> For the co-algebraic numbers it’s
>
>
>
> num -> num option
>
>
>
> For arbitrari
aic each might be iterable an infinite number of times. (The
> corresponding destructors in the algebraic types are always well-founded.)
>
>
>
> What are the co-algebras for your desired types? I don’t think I’ve
> understood what you want, but it superficially appears
-founded.)
>
>
>
> What are the co-algebras for your desired types? I don’t think I’ve
> understood what you want, but it superficially appears as if you want
> dependent types, where you combine the type with some term-level predicate.
> That sort of thing is impossible to capture withi
Hi,
Lately, I've been exploring the HOL4 lazy list theory "llistTheory", which
is developed based on the co-algebraic datatype. I understand that the
datatype *'a llist *is derived as a subset of the option type *:num -> 'a
option. * Now, I want to define a new datatype based on datatype 'a
Thanks..that solves the issue...
On Mon, Oct 30, 2017 at 4:20 AM, <michael.norr...@data61.csiro.au> wrote:
> That’s a Poly/ML bug. Please use the 5.7 release available at
>
>
>
> https://github.com/polyml/polyml/archive/v5.7.tar.gz
>
>
>
> Michael
>
>
&g
29 matches
Mail list logo
