A couple of questions that might point you to a mistake:
- Do you expect the left-hand side of thm4 to be the same as the
right-hand side of thm6?
(It is not.)
- Do you expect thm4 and thm4b to have the same conclusion?
(They do.)
On Sun, Oct 21, 2012 at 6:03 PM, Tony Johnson
<[email protected]>wrote:
> Hi,
>
> I'm having an issue that should be simple to resolve but I can't seem to
> figure it out.
>
> so I have this....
>
> val def = realTheory.abs;
> val def1 = SPEC (--`(a * b)`--) def;
> val def2 = INST_TYPE [alpha |-> Type`:real`] COND_DEF;
> val thm1 = SUBS [def2] def1;
> val thm2 = BETA_CONV (--`( \(t:bool) (t1:real) (t2:real). @x.((t = T)
> ==> (x = t1)) /\ ((t = F) ==> (x = t2))) (0 <= a * b) `--);
> val thm3 = BETA_CONV (--`( \(t1:real) (t2:real). @x.((0 <= a * b = T)
> ==> (x = t1)) /\ ((0 <= a * b = F) ==> (x = t2)) ) (a * b) `--);
> val thm4 = BETA_CONV (--`( \(t2:real). @x.((0 <= a * b = T) ==> (x = (a
> * b)) /\ ((0 <= a * b = F) ==> (x = t2)))) (-(a * b)) `--);
> val thm4b = BETA_CONV (--`( \(t2:real). @x. ((0 <= a * b = T) ==> (x =
> (a * b)) /\ ((0 <= a * b = F) ==> (x = t2)) )) (-(a * b)) `--);
> val thm5 = SUBS [thm2] thm1;
> val thm6 = SUBS [thm3] thm5;
>
> which gives me...
>
> - thm6;
> > val it =
> |- abs ((a :real) * (b :real)) =
> (λ(t2 :real).
> @(x :real).
> (((0 :real) ≤ a * b ⇔ T) ⇒ (x = a * b)) ∧
> (((0 :real) ≤ a * b ⇔ F) ⇒ (x = t2))) (-(a * b)) : thm
>
> and if I understand what is going on correctly, then this...
>
> val thm7 = SUBS [thm4b] thm6;
>
> should give me
>
> `abs(a * b:real) = @x.(0 <= a:real * b = T) ==> (x = a * b) /\ ((0 <= a
> * b = F) ==> (x = -(a * b))) ``;
>
> but it does not.
>
> however when I do this.
>
> val thm10 = ASSUME(--`(f a) = ((\t:bool. @x:real.((x = 1) ==> t)) a)`--);
> val thm11 = BETA_CONV (--`((\t. @x.((x = 1) ==> t)) a)`--);
> val thm12 = SUBS [thm11] thm10;
>
> I get
>
> - thm12;
> > val it =
> [.] |- (f :bool -> real) (a :bool) = @(x :real). (x = (1 :real)) ⇒ a :
> thm
> -
> so am misunderstanding something fundamental about how SUBS and thus I
> suppose how SUBST works?
>
>
> Thanks,
> -Tony
>
>
>
> ------------------------------------------------------------------------------
> Everyone hates slow websites. So do we.
> Make your web apps faster with AppDynamics
> Download AppDynamics Lite for free today:
> http://p.sf.net/sfu/appdyn_sfd2d_oct
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
Everyone hates slow websites. So do we.
Make your web apps faster with AppDynamics
Download AppDynamics Lite for free today:
http://p.sf.net/sfu/appdyn_sfd2d_oct
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
