t;2015200...@mail.buct.edu.cn>
Cc:
Subject: Re: [Hol-info] A problem of derivation
Hi Liu,
rewriting applies the provided equations left to write. So if if have
(A = A') /\ (B = B') ==> (f A B)
The simplifier (with std_ss) uses the precondition (A = A') /\ (B = B') as
context and add
Thank you very much,its works!
-Original Messages-
From:michael.norr...@data61.csiro.au
Sent Time:2017-11-09 11:15:52 (Thursday)
To: 2015200...@mail.buct.edu.cn
Cc:
Subject: Re: [Hol-info] A problem of derivation
Use the theorem SQRT_POW_2. E.g.:
Q.prove(
`!a b c d.(sqrt(c pow
Hi Liu,
rewriting applies the provided equations left to write. So if if have
(A = A') /\ (B = B') ==> (f A B)
The simplifier (with std_ss) uses the precondition (A = A') /\ (B = B')
as context and adds the rewrite rules
A -> A'
B -> B'
where "->" is an ad-hoc notation for "=" but only
Hi,
I want to prove the goal:
!a b c d.(sqrt(c pow 2 + d pow 2) pow 2 = c pow 2 + d pow 2) /\ (sqrt(a pow 2 +
b pow 2) pow 2 = a pow 2 + b pow 2) /\ sqrt(c pow 2 + d pow 2) pow 2 ≤ sqrt(a
pow 2 + b pow 2) pow 2 ==> c pow 2 + d pow 2 ≤ a pow 2 + b pow 2
In theory this goal can be proved by
