マッカーシーの91関数

g `!(x:int). x <= &101 ==> (?n k. 91 <= k /\ k <= 101 /\ x = &k - &(11 * n))` ;;
e( REPEAT STRIP_TAC );;
e( SUBGOAL_THEN `?m:num. &101 - x:int = &m` MP_TAC );;
e( ASM_CASES_TAC `&101 - x:int = &0` );;
e( EXISTS_TAC `0` THEN ASM_SIMP_TAC []);;
e( SUBGOAL_TAC "" `&0 < &101 - x:int` [ASM_INT_ARITH_TAC]);;
e( MP_TAC (SPEC`&101 - x:int`INT_IMAGE) THEN STRIP_TAC );;
e( EXISTS_TAC `n:num` THEN ASM_SIMP_TAC [] );;
e ASM_INT_ARITH_TAC ;;
e STRIP_TAC ;;
e( MP_TAC (SPECL[`m:num`;`11`]DIVMOD_EXIST) THEN SIMP_TAC [ARITH] THEN STRIP_TAC );;
e( EXISTS_TAC `q:num` THEN EXISTS_TAC `101 - r` THEN REPEAT STRIP_TAC );;
e( ASM_ARITH_TAC );;
e( ASM_ARITH_TAC );;
e( SUBGOAL_TAC "" `r <= 101` [ASM_ARITH_TAC] );;
e( ASM_SIMP_TAC [GSYM INT_OF_NUM_SUB;GSYM INT_OF_NUM_MUL] );;

e( SUBGOAL_TAC "" `&m = &q * &11 + &r:int` [ASM_SIMP_TAC [GSYM INT_OF_NUM_MUL;GSYM INT_OF_NUM_ADD]] );;
e ASM_INT_ARITH_TAC ;;
let lemma06 = top_thm ();;

let lemma02 = ARITH_RULE`91 <= k /\ k <= 101 <=> k = 91 \/ k = 92 \/ k = 93 \/ k = 94 \/ k = 95 \/ k = 96 \/ k = 97 \/ k = 98 \/ k = 99 \/ k = 100 \/ k = 101`;;

g `!(f:int->int). (!x. f x = if &101 <= x then x - &10 else f (f (x + &11))) ==> (!(x:int). x <= &101 ==> f x = &91)` ;;
e( REPEAT STRIP_TAC );;

e( FIRST_ASSUM (MP_TAC o (MATCH_MP lemma06)) THEN REPEAT STRIP_TAC );;
e( POP_ASSUM SUBST1_TAC );;

e( SUBGOAL_THEN `!j. 91 <= j /\ j <= 100 ==> (f:int->int) (&j) = f(&j + &1)` ASSUME_TAC );;
e( REPEAT STRIP_TAC );;
e( FIRST_ASSUM (SUBST_ALL_TAC o SPEC`&j:int`) );;
e( SUBGOAL_THEN `~(&101 <= &j:int)` (fun th -> SIMP_TAC [th]));;
e( DEL_TAC 0 );;
e( SIMP_TAC [REAL_LE] THEN ASM_ARITH_TAC );;

e( FIRST_ASSUM (SUBST_ALL_TAC o SPEC`&j + &11:int`) );;
e( SUBGOAL_THEN `&101 <= &j + &11:int` (fun th -> SIMP_TAC [th]));;
e( DEL_TAC 0 );;
e( SIMP_TAC [REAL_ADD;REAL_LE] THEN ASM_ARITH_TAC );;
e( SIMP_TAC [INT_ARITH`(&j + &11) - &10 = &j + &1:int`] );;

e( FIRST_ASSUM (MP_TAC o SPEC`&101:int`) );;
e( SIMP_TAC [INT_ARITH`&101 <= &101:int /\ &101 - &10 = &91:int`] );;

e( FIRST_ASSUM (MP_TAC o SPEC`100`) );;
e( FIRST_ASSUM (MP_TAC o SPEC`99`) );;
e( FIRST_ASSUM (MP_TAC o SPEC`98`) );;
e( FIRST_ASSUM (MP_TAC o SPEC`97`) );;
e( FIRST_ASSUM (MP_TAC o SPEC`96`) );;
e( FIRST_ASSUM (MP_TAC o SPEC`95`) );;
e( FIRST_ASSUM (MP_TAC o SPEC`94`) );;
e( FIRST_ASSUM (MP_TAC o SPEC`93`) );;
e( FIRST_ASSUM (MP_TAC o SPEC`92`) );;
e( FIRST_ASSUM (MP_TAC o SPEC`91`) );;
e( SIMP_TAC [INT_OF_NUM_ADD;ARITH] );;

e( REPEAT DISCH_TAC );;

e( SPEC_TAC (`n:num`,`n:num`) );;
e( INDUCT_TAC );;

e( SIMP_TAC [MULT_0;INT_SUB_RZERO] );;

e( MP_TAC lemma02);;
e( DEL_TAC 0 );;

e( ASM_SIMP_TAC [] );;

e( REPEAT STRIP_TAC );;

e( ASM_SIMP_TAC [] );;
e( ASM_SIMP_TAC [] );;
e( ASM_SIMP_TAC [] );;
e( ASM_SIMP_TAC [] );;
e( ASM_SIMP_TAC [] );;
e( ASM_SIMP_TAC [] );;
e( ASM_SIMP_TAC [] );;
e( ASM_SIMP_TAC [] );;
e( ASM_SIMP_TAC [] );;
e( ASM_SIMP_TAC [] );;
e( ASM_SIMP_TAC [] );;

e( FIRST_ASSUM (SUBST_ALL_TAC o SPEC`&k - &(11 * SUC n):int`) );;
e( DEL_TAC 0 );;

e( ASM_SIMP_TAC [INT_ARITH`&k:int <= &101 ==> ~ (&101:int <= &k - &11 * (&n + &1))`;INT_OF_NUM_LE;GSYM INT_OF_NUM_MUL;GSYM INT_OF_NUM_SUC] );;

e( ASM_SIMP_TAC [INT_OF_NUM_MUL;INT_ARITH`&k:int - &11 * (&n + &1) + &11 = &k - &11 * &n`] );;

let mcc = top_thm ();;

val mcc : thm =
  |- !f. (!x. f x = (if &101 <= x then x - &10 else f (f (x + &11))))
         ==> (!x. x <= &101 ==> f x = &91)