Examples (6)

　IMAGEの用例です．

# IMAGE;;
val it : thm = |- !s f. IMAGE f s = {y | ?x. x IN s /\ y = f x}

# g`y IN (IMAGE (\x. x+ &1) {x| &0 &1 &1 < y`

# e (REWRITE_TAC[IMAGE;IN_ELIM_THM]);;
val it : goalstack = 1 subgoal (1 total)

`(?x. &0 < x /\ y = x + &1) <=> &1 < y`

# e EQ_TAC;;
val it : goalstack = 2 subgoals (2 total)

`&1 < y ==> (?x. &0 < x /\ y = x + &1)`

`(?x. &0 < x /\ y = x + &1) ==> &1 < y`

# e STRIP_TAC;;
val it : goalstack = 1 subgoal (2 total)

0 [`&0 < x`]
1 [`y = x + &1`]

`&1 < y`

# e(ASM_REAL_ARITH_TAC);;
val it : goalstack = 1 subgoal (1 total)

`&1 < y ==> (?x. &0 < x /\ y = x + &1)`

# e STRIP_TAC;;
val it : goalstack = 1 subgoal (1 total)

0 [`&1 < y`]

`?x. &0 < x /\ y = x + &1`

# e(EXISTS_TAC `y- &1` );;
val it : goalstack = 1 subgoal (1 total)

0 [`&1 < y`]

`&0 < y - &1 /\ y = y - &1 + &1`

# e(ASM_REAL_ARITH_TAC);;
val it : goalstack = No subgoals