src/q/selftest.sml

38 val _ = new_constant ("zero", ``:num``)
65 val glmrt3 = ([] : term list, ``f zero zero = (z:'a)``)
74 val expected_mat1a1 = ``Abbrev (b = zero)``
109           ``!x. x * SUC (SUC zero) < y * (z + SUC zero) * (y + a)``)
111     ``!x. x * SUC (SUC zero) < y * (z + SUC zero) * (y + c)``
119           ``!x. x * SUC (SUC zero) < y * (z + SUC zero) * (y + a)``)
121     ``!x. x * SUC (SUC zero) < y * s * (y + a)``
123     ``Abbrev(s = z + SUC zero)``
133            ``!x. x * SUC zero < y * (z + SUC zero) * (z + SUC (SUC zero))``)
142 val gl2a = ([] : term list, ``!x. x * SUC zero < z``)
152 val gl3 = ([``P (x:num): bool``, ``Q (x < SUC (SUC (SUC zero))) : bool``],
153            ``x + y < SUC (SUC zero)``);
156 val expected_c = ``x + y < SUC (SUC zero)``
166 val gl3 = ([``P (x:num): bool``, ``Q (x < SUC (SUC (SUC zero))) : bool``],
167            ``x + y < SUC (SUC zero)``);
168 val expected_a1 = ``Abbrev(two = SUC (SUC zero))``
191     Q.PAT_ABBREV_TAC `v = (x < SUC w)` ([], ``y < SUC zero ==> y < z``)
194             if Term.aconv abb ``Abbrev(v = y < SUC zero)`` andalso
202                    ([], ``!x. x < SUC zero``)
206                    ([], ``!y. y < SUC zero``)
210                    ([], ``(!y. y < SUC zero) /\ y < zero``)
214                   ([], ``(!y. y < SUC zero) /\ u < SUC (SUC zero)``)
217             if Term.aconv abb ``Abbrev (v = u < SUC (SUC zero))`` andalso
218                Term.aconv sg ``(!y. y < SUC zero) /\ v``
225                   ([], ``(!x. x < SUC zero) /\ u < SUC (SUC zero)``)
228             if Term.aconv abb ``Abbrev (v = u < SUC (SUC zero))`` andalso
229                Term.aconv sg ``(!y. y < SUC zero) /\ v``
247 val fa_n = ``!n:num. SUC n < zero``
255           [([fa_y], ``SUC x < zero ==> x < x``)]),
259           [([fa_y], ``SUC (SUC x) < zero ==> x < f (y:int)``)]),