equal
deleted
inserted
replaced
531 then show "y < x + x * (Quo x y)" by (simp add: Quo3) |
531 then show "y < x + x * (Quo x y)" by (simp add: Quo3) |
532 qed |
532 qed |
533 |
533 |
534 lemma Quo_div: |
534 lemma Quo_div: |
535 shows "Quo x y = y div x" |
535 shows "Quo x y = y div x" |
536 apply(case_tac "x = 0") |
536 by (metis Quo0 Quo1 Quo4 div_by_0 div_nat_eqI mult_Suc_right neq0_conv) |
537 apply(simp add: Quo0) |
|
538 apply(subst split_div_lemma[symmetric]) |
|
539 apply(auto intro: Quo1 Quo4) |
|
540 done |
|
541 |
537 |
542 lemma Quo_rec_quo: |
538 lemma Quo_rec_quo: |
543 shows "rec_eval rec_quo [y, x] = Quo x y" |
539 shows "rec_eval rec_quo [y, x] = Quo x y" |
544 by (induct y) (simp_all add: rec_quo_def) |
540 by (induct y) (simp_all add: rec_quo_def) |
545 |
541 |