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
