Lines Matching refs:b2
29 * (abs_frac (a1,b1) = abs_frac (a2,b2)
31 * 0<b1, 0<b2 |- (abs_frac (a1,b1) = abs_frac (a1,b1))
32 * = (a1 = a2) /\ (b1 = b2) : thm
42 val (a2,b2) = dest_pair rha;
44 UNDISCH_ALL (SPECL[a1,b1,a2,b2] FRAC_EQ)
51 * ~((abs_frac (a1,b1) = abs_frac (a2,b2))
53 * 0<b1, 0<b2 |- ~(abs_frac (a1,b1) = abs_frac (a2,b2))
54 * = ~(a1 = a2) \/ ~(b1 = b2)
64 val (a2,b2) = dest_pair rha;
66 UNDISCH_ALL (SPECL[a1,b1,a2,b2] FRAC_NOT_EQ)
73 * A ?- abs_frac(a1,b1) = abs_frac(a2,b2)
75 * A ?- a1=a2 | A ?- b1=b2
84 val (a2,b2) = dest_pair rha;
88 val subgoal2 = mk_eq(b1,b2);
93 (SPEC b2 (SPEC a2 (SPEC b1 (SPEC a1 (
94 prove(``!a1 b1 a2 b2. (a1=a2) /\ (b1=b2) ==> (abs_frac(a1,b1)=abs_frac(a2,b2))``, RW_TAC int_ss [])
553 val b2 = ``& ^b2x + 1i``;
556 val dnm_thm2 = ARITH_PROVE ``0i < ^b2``;
557 val frac_thm = SPECL[a1,b1,a1,b2] FRAC_EQ
559 REWRITE_RULE [SIMP_CONV int_ss [] b2x] (EQT_ELIM (REWRITE_CONV [frac_save_def,LIST_MP [dnm_thm1,dnm_thm2] frac_thm,SIMP_CONV int_ss [] ``^b1 = ^b2``] to_show))