src/CTT/Arith.thy
changeset 58318 f95754ca7082
parent 39159 0dec18004e75
child 58889 5b7a9633cfa8
equal deleted inserted replaced
58317:21fac057681e 58318:f95754ca7082
   457 (*case analysis on   succ(u mod b)|-|b  *)
   457 (*case analysis on   succ(u mod b)|-|b  *)
   458 apply (rule_tac a1 = "succ (u mod b) |-| b" in iszero_decidable [THEN PlusE])
   458 apply (rule_tac a1 = "succ (u mod b) |-| b" in iszero_decidable [THEN PlusE])
   459 apply (erule_tac [3] SumE)
   459 apply (erule_tac [3] SumE)
   460 apply (tactic {* hyp_arith_rew_tac (@{thms div_typing_rls} @
   460 apply (tactic {* hyp_arith_rew_tac (@{thms div_typing_rls} @
   461   [@{thm modC0}, @{thm modC_succ}, @{thm divC0}, @{thm divC_succ2}]) *})
   461   [@{thm modC0}, @{thm modC_succ}, @{thm divC0}, @{thm divC_succ2}]) *})
   462 (*Replace one occurence of  b  by succ(u mod b).  Clumsy!*)
   462 (*Replace one occurrence of  b  by succ(u mod b).  Clumsy!*)
   463 apply (rule add_typingL [THEN trans_elem])
   463 apply (rule add_typingL [THEN trans_elem])
   464 apply (erule EqE [THEN absdiff_eq0, THEN sym_elem])
   464 apply (erule EqE [THEN absdiff_eq0, THEN sym_elem])
   465 apply (rule_tac [3] refl_elem)
   465 apply (rule_tac [3] refl_elem)
   466 apply (tactic {* hyp_arith_rew_tac @{thms div_typing_rls} *})
   466 apply (tactic {* hyp_arith_rew_tac @{thms div_typing_rls} *})
   467 done
   467 done