author berghofe Mon Apr 28 10:33:57 2003 +0200 (2003-04-28) changeset 13931 38d43d168e87 parent 13930 562fd03b266d child 13932 0eb3d91b519a
Converted main proof to Isar.
```     1.1 --- a/src/HOL/Extraction/QuotRem.thy	Mon Apr 28 10:33:42 2003 +0200
1.2 +++ b/src/HOL/Extraction/QuotRem.thy	Mon Apr 28 10:33:57 2003 +0200
1.3 @@ -9,36 +9,33 @@
1.4
1.5  text {* Derivation of quotient and remainder using program extraction. *}
1.6
1.7 -consts_code
1.8 -  arbitrary :: sumbool ("{* Left *}")
1.9 -
1.10 -lemma le_lt_eq_dec: "\<And>m::nat. n <= m \<Longrightarrow> n < m \<or> n = m"
1.11 -  apply (induct n)
1.12 -  apply (case_tac m)
1.13 -  apply simp
1.14 -  apply simp
1.15 -  apply (case_tac m)
1.16 -  apply simp
1.17 -  apply simp
1.18 +lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n"
1.19 +  apply (induct m)
1.20 +  apply (case_tac n)
1.21 +  apply (case_tac  na)
1.22 +  apply (simp only: nat.simps, rules?)+
1.23    done
1.24
1.25 -lemma division: "\<exists>r q. a = Suc b * q + r \<and> r <= b"
1.26 -  apply (induct a)
1.27 -  apply (rule_tac x = 0 in exI)
1.28 -  apply (rule_tac x = 0 in exI)
1.29 -  apply simp
1.30 -  apply (erule exE)
1.31 -  apply (erule exE)
1.32 -  apply (erule conjE)
1.33 -  apply (drule le_lt_eq_dec)
1.34 -  apply (erule disjE)
1.35 -  apply (rule_tac x = "Suc r" in exI)
1.36 -  apply (rule_tac x = q in exI)
1.37 -  apply simp
1.38 -  apply (rule_tac x = 0 in exI)
1.39 -  apply (rule_tac x = "Suc q" in exI)
1.40 -  apply simp
1.41 -  done
1.42 +theorem division: "\<exists>r q. a = Suc b * q + r \<and> r \<le> b"
1.43 +proof (induct a)
1.44 +  case 0
1.45 +  have "0 = Suc b * 0 + 0 \<and> 0 \<le> b" by simp
1.46 +  thus ?case by rules
1.47 +next
1.48 +  case (Suc a)
1.49 +  then obtain r q where I: "a = Suc b * q + r" and "r \<le> b" by rules
1.50 +  from nat_eq_dec show ?case
1.51 +  proof
1.52 +    assume "r = b"
1.53 +    with I have "Suc a = Suc b * (Suc q) + 0 \<and> 0 \<le> b" by simp
1.54 +    thus ?case by rules
1.55 +  next
1.56 +    assume "r \<noteq> b"
1.57 +    hence "r < b" by (simp add: order_less_le)
1.58 +    with I have "Suc a = Suc b * q + (Suc r) \<and> (Suc r) \<le> b" by simp
1.59 +    thus ?case by rules
1.60 +  qed
1.61 +qed
1.62
1.63  extract division
1.64
```