src/HOL/Proofs/Extraction/QuotRem.thy
author haftmann
Sat, 05 Jul 2014 11:01:53 +0200
changeset 57514 bdc2c6b40bf2
parent 45170 7dd207fe7b6e
child 58889 5b7a9633cfa8
permissions -rw-r--r--
prefer ac_simps collections over separate name bindings for add and mult
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39157
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 36862
diff changeset
     1
(*  Title:      HOL/Proofs/Extraction/QuotRem.thy
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
     2
    Author:     Stefan Berghofer, TU Muenchen
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
     3
*)
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
     4
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
     5
header {* Quotient and remainder *}
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
     6
27436
9581777503e9 code antiquotation roaring ahead
haftmann
parents: 25419
diff changeset
     7
theory QuotRem
9581777503e9 code antiquotation roaring ahead
haftmann
parents: 25419
diff changeset
     8
imports Util
9581777503e9 code antiquotation roaring ahead
haftmann
parents: 25419
diff changeset
     9
begin
9581777503e9 code antiquotation roaring ahead
haftmann
parents: 25419
diff changeset
    10
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    11
text {* Derivation of quotient and remainder using program extraction. *}
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    12
13931
38d43d168e87 Converted main proof to Isar.
berghofe
parents: 13405
diff changeset
    13
theorem division: "\<exists>r q. a = Suc b * q + r \<and> r \<le> b"
38d43d168e87 Converted main proof to Isar.
berghofe
parents: 13405
diff changeset
    14
proof (induct a)
38d43d168e87 Converted main proof to Isar.
berghofe
parents: 13405
diff changeset
    15
  case 0
38d43d168e87 Converted main proof to Isar.
berghofe
parents: 13405
diff changeset
    16
  have "0 = Suc b * 0 + 0 \<and> 0 \<le> b" by simp
17604
5f30179fbf44 rules -> iprover
nipkow
parents: 17145
diff changeset
    17
  thus ?case by iprover
13931
38d43d168e87 Converted main proof to Isar.
berghofe
parents: 13405
diff changeset
    18
next
38d43d168e87 Converted main proof to Isar.
berghofe
parents: 13405
diff changeset
    19
  case (Suc a)
17604
5f30179fbf44 rules -> iprover
nipkow
parents: 17145
diff changeset
    20
  then obtain r q where I: "a = Suc b * q + r" and "r \<le> b" by iprover
13931
38d43d168e87 Converted main proof to Isar.
berghofe
parents: 13405
diff changeset
    21
  from nat_eq_dec show ?case
38d43d168e87 Converted main proof to Isar.
berghofe
parents: 13405
diff changeset
    22
  proof
38d43d168e87 Converted main proof to Isar.
berghofe
parents: 13405
diff changeset
    23
    assume "r = b"
38d43d168e87 Converted main proof to Isar.
berghofe
parents: 13405
diff changeset
    24
    with I have "Suc a = Suc b * (Suc q) + 0 \<and> 0 \<le> b" by simp
17604
5f30179fbf44 rules -> iprover
nipkow
parents: 17145
diff changeset
    25
    thus ?case by iprover
13931
38d43d168e87 Converted main proof to Isar.
berghofe
parents: 13405
diff changeset
    26
  next
38d43d168e87 Converted main proof to Isar.
berghofe
parents: 13405
diff changeset
    27
    assume "r \<noteq> b"
23373
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 22845
diff changeset
    28
    with `r \<le> b` have "r < b" by (simp add: order_less_le)
13931
38d43d168e87 Converted main proof to Isar.
berghofe
parents: 13405
diff changeset
    29
    with I have "Suc a = Suc b * q + (Suc r) \<and> (Suc r) \<le> b" by simp
17604
5f30179fbf44 rules -> iprover
nipkow
parents: 17145
diff changeset
    30
    thus ?case by iprover
13931
38d43d168e87 Converted main proof to Isar.
berghofe
parents: 13405
diff changeset
    31
  qed
38d43d168e87 Converted main proof to Isar.
berghofe
parents: 13405
diff changeset
    32
qed
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    33
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    34
extract division
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    35
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    36
text {*
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    37
  The program extracted from the above proof looks as follows
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    38
  @{thm [display] division_def [no_vars]}
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    39
  The corresponding correctness theorem is
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    40
  @{thm [display] division_correctness [no_vars]}
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    41
*}
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    42
27436
9581777503e9 code antiquotation roaring ahead
haftmann
parents: 25419
diff changeset
    43
lemma "division 9 2 = (0, 3)" by eval
20593
5af400cc64d5 added some stuff for code generation 2
haftmann
parents: 17604
diff changeset
    44
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
    45
end