Converted main proof to Isar.
authorberghofe
Mon Apr 28 10:33:57 2003 +0200 (2003-04-28)
changeset 1393138d43d168e87
parent 13930 562fd03b266d
child 13932 0eb3d91b519a
Converted main proof to Isar.
src/HOL/Extraction/QuotRem.thy
     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 [3] 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