author | wenzelm |
Wed, 30 Dec 2015 18:25:39 +0100 | |
changeset 61986 | 2461779da2b8 |
parent 59730 | b7c394c7a619 |
child 63361 | d10eab0672f9 |
permissions | -rw-r--r-- |
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:
32960
diff
changeset
|
1 |
(* Title: HOL/Proofs/Extraction/Util.thy |
25421 | 2 |
Author: Stefan Berghofer, TU Muenchen |
3 |
*) |
|
4 |
||
61986 | 5 |
section \<open>Auxiliary lemmas used in program extraction examples\<close> |
25421 | 6 |
|
7 |
theory Util |
|
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
8 |
imports "~~/src/HOL/Library/Old_Datatype" |
25421 | 9 |
begin |
10 |
||
61986 | 11 |
text \<open> |
25421 | 12 |
Decidability of equality on natural numbers. |
61986 | 13 |
\<close> |
25421 | 14 |
|
15 |
lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n" |
|
16 |
apply (induct m) |
|
17 |
apply (case_tac n) |
|
18 |
apply (case_tac [3] n) |
|
19 |
apply (simp only: nat.simps, iprover?)+ |
|
20 |
done |
|
21 |
||
61986 | 22 |
text \<open> |
25421 | 23 |
Well-founded induction on natural numbers, derived using the standard |
24 |
structural induction rule. |
|
61986 | 25 |
\<close> |
25421 | 26 |
|
27 |
lemma nat_wf_ind: |
|
28 |
assumes R: "\<And>x::nat. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x" |
|
29 |
shows "P z" |
|
30 |
proof (rule R) |
|
31 |
show "\<And>y. y < z \<Longrightarrow> P y" |
|
32 |
proof (induct z) |
|
33 |
case 0 |
|
34 |
thus ?case by simp |
|
35 |
next |
|
36 |
case (Suc n y) |
|
37 |
from nat_eq_dec show ?case |
|
38 |
proof |
|
39 |
assume ny: "n = y" |
|
40 |
have "P n" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
25421
diff
changeset
|
41 |
by (rule R) (rule Suc) |
25421 | 42 |
with ny show ?case by simp |
43 |
next |
|
44 |
assume "n \<noteq> y" |
|
45 |
with Suc have "y < n" by simp |
|
46 |
thus ?case by (rule Suc) |
|
47 |
qed |
|
48 |
qed |
|
49 |
qed |
|
50 |
||
61986 | 51 |
text \<open> |
25421 | 52 |
Bounded search for a natural number satisfying a decidable predicate. |
61986 | 53 |
\<close> |
25421 | 54 |
|
55 |
lemma search: |
|
56 |
assumes dec: "\<And>x::nat. P x \<or> \<not> P x" |
|
57 |
shows "(\<exists>x<y. P x) \<or> \<not> (\<exists>x<y. P x)" |
|
58 |
proof (induct y) |
|
59 |
case 0 show ?case by simp |
|
60 |
next |
|
61 |
case (Suc z) |
|
62 |
thus ?case |
|
63 |
proof |
|
64 |
assume "\<exists>x<z. P x" |
|
65 |
then obtain x where le: "x < z" and P: "P x" by iprover |
|
66 |
from le have "x < Suc z" by simp |
|
67 |
with P show ?case by iprover |
|
68 |
next |
|
69 |
assume nex: "\<not> (\<exists>x<z. P x)" |
|
70 |
from dec show ?case |
|
71 |
proof |
|
72 |
assume P: "P z" |
|
73 |
have "z < Suc z" by simp |
|
74 |
with P show ?thesis by iprover |
|
75 |
next |
|
76 |
assume nP: "\<not> P z" |
|
77 |
have "\<not> (\<exists>x<Suc z. P x)" |
|
78 |
proof |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
25421
diff
changeset
|
79 |
assume "\<exists>x<Suc z. P x" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
25421
diff
changeset
|
80 |
then obtain x where le: "x < Suc z" and P: "P x" by iprover |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
25421
diff
changeset
|
81 |
have "x < z" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
25421
diff
changeset
|
82 |
proof (cases "x = z") |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
25421
diff
changeset
|
83 |
case True |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
25421
diff
changeset
|
84 |
with nP and P show ?thesis by simp |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
25421
diff
changeset
|
85 |
next |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
25421
diff
changeset
|
86 |
case False |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
25421
diff
changeset
|
87 |
with le show ?thesis by simp |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
25421
diff
changeset
|
88 |
qed |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
25421
diff
changeset
|
89 |
with P have "\<exists>x<z. P x" by iprover |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
25421
diff
changeset
|
90 |
with nex show False .. |
25421 | 91 |
qed |
92 |
thus ?case by iprover |
|
93 |
qed |
|
94 |
qed |
|
95 |
qed |
|
96 |
||
97 |
end |