含意と特称

　以前にも書いた排中律ネタですが，今回は連言から存在量化を纏める形のものです．

g `!p:A->bool. !q:bool. (?x. p x ==> q) ==> (?y. q ==> p y) ==> (?z. p z <=> q)`;;
e( REPEAT STRIP_TAC );;
e( DISJ_CASES_TAC (SPEC `q:bool` EXCLUDED_MIDDLE) );;
e( EXISTS_TAC `y:A` THEN EQ_TAC );;
e( DISCH_TAC THEN GET_THEN 2 ACCEPT_TAC );;
e( GET_THEN 1 ACCEPT_TAC );;
e( EXISTS_TAC `x:A` THEN EQ_TAC );;
e( GET_THEN 0 ACCEPT_TAC );;
e( ONCE_REWRITE_TAC [GSYM CONTRAPOS_THM] );;
e( DISCH_TAC THEN GET_THEN 2 ACCEPT_TAC );;
(UNDISCH_ALL o SPEC_ALL) (top_thm ()) ;;

# g `!p:A->bool. !q:bool. (?x. p x ==> q) ==> (?y. q ==> p y) ==> (?z. p z <=> q)`;;
val it : goalstack = 1 subgoal (1 total)

`!p q. (?x. p x ==> q) ==> (?y. q ==> p y) ==> (?z. p z <=> q)`

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

  0 [`p x ==> q`]
  1 [`q ==> p y`]

`?z. p z <=> q`

# e( DISJ_CASES_TAC (SPEC `q:bool` EXCLUDED_MIDDLE) );;
val it : goalstack = 2 subgoals (2 total)

  0 [`p x ==> q`]
  1 [`q ==> p y`]
  2 [`~q`]

`?z. p z <=> q`

  0 [`p x ==> q`]
  1 [`q ==> p y`]
  2 [`q`]

`?z. p z <=> q`

# e( EXISTS_TAC `y:A` THEN EQ_TAC );;
val it : goalstack = 2 subgoals (3 total)

  0 [`p x ==> q`]
  1 [`q ==> p y`]
  2 [`q`]

`q ==> p y`

  0 [`p x ==> q`]
  1 [`q ==> p y`]
  2 [`q`]

`p y ==> q`

# e( DISCH_TAC THEN GET_THEN 2 ACCEPT_TAC );;
val it : goalstack = 1 subgoal (2 total)

  0 [`p x ==> q`]
  1 [`q ==> p y`]
  2 [`q`]

`q ==> p y`

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

  0 [`p x ==> q`]
  1 [`q ==> p y`]
  2 [`~q`]

`?z. p z <=> q`

# e( EXISTS_TAC `x:A` THEN EQ_TAC );;
val it : goalstack = 2 subgoals (2 total)

  0 [`p x ==> q`]
  1 [`q ==> p y`]
  2 [`~q`]

`q ==> p x`

  0 [`p x ==> q`]
  1 [`q ==> p y`]
  2 [`~q`]

`p x ==> q`

# e( GET_THEN 0 ACCEPT_TAC );;
val it : goalstack = 1 subgoal (1 total)

  0 [`p x ==> q`]
  1 [`q ==> p y`]
  2 [`~q`]

`q ==> p x`

# e( ONCE_REWRITE_TAC [GSYM CONTRAPOS_THM] );;
val it : goalstack = 1 subgoal (1 total)

  0 [`p x ==> q`]
  1 [`q ==> p y`]
  2 [`~q`]

`~p x ==> ~q`

# e( DISCH_TAC THEN GET_THEN 2 ACCEPT_TAC );;
val it : goalstack = No subgoals

# (UNDISCH_ALL o SPEC_ALL) (top_thm ()) ;;
val it : thm = ?y. q ==> p y, ?x. p x ==> q |- ?z. p z <=> q