On 11/7/18 10:37 AM, Rene Vestergaard wrote:
"Proofs of life: molecular-biology reasoning simulates cell behaviors
from first principles" is now at http://arxiv.org/abs/1811.02478
accompanying video, with proof visualization and more:
Open problems
Questions
Dear Jose M:
In addition:
We have many and may problems, for example, could you derive the values of
the Gamma function at the singular points?
With best,
SS
2019.3.20.10:35
Dear Jose M.
I was able to know some about Isabelle HO/L from my colleague
Thanks for the suggestion! I can use satTheory.AND_IMP to renormalize the
intermediate resolution back to an implicative form, which should work.
The reason that this issue came up is that asm_simp_tac seems to be
sensitive to the ordering of antecedents/assumptions. I was trying to do a
step
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
I have two assumptions both in implicative forms with universal
quantification. I would like to obtain an MP in the spirit of the following
theorem:
val GEN_IMP_TRANS = store_thm("GEN_IMP_TRANS",
``!P Q R S. (!x. P x ==> Q (R x)) ==> (!x. Q x ==> S x) ==> (!x. P x
==> S (R x))``,
