25421
|
1 |
(* Title: HOL/Extraction/Util.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Stefan Berghofer, TU Muenchen
|
|
4 |
*)
|
|
5 |
|
|
6 |
header {* Auxiliary lemmas used in program extraction examples *}
|
|
7 |
|
|
8 |
theory Util
|
|
9 |
imports Main
|
|
10 |
begin
|
|
11 |
|
|
12 |
text {*
|
|
13 |
Decidability of equality on natural numbers.
|
|
14 |
*}
|
|
15 |
|
|
16 |
lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n"
|
|
17 |
apply (induct m)
|
|
18 |
apply (case_tac n)
|
|
19 |
apply (case_tac [3] n)
|
|
20 |
apply (simp only: nat.simps, iprover?)+
|
|
21 |
done
|
|
22 |
|
|
23 |
text {*
|
|
24 |
Well-founded induction on natural numbers, derived using the standard
|
|
25 |
structural induction rule.
|
|
26 |
*}
|
|
27 |
|
|
28 |
lemma nat_wf_ind:
|
|
29 |
assumes R: "\<And>x::nat. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
|
|
30 |
shows "P z"
|
|
31 |
proof (rule R)
|
|
32 |
show "\<And>y. y < z \<Longrightarrow> P y"
|
|
33 |
proof (induct z)
|
|
34 |
case 0
|
|
35 |
thus ?case by simp
|
|
36 |
next
|
|
37 |
case (Suc n y)
|
|
38 |
from nat_eq_dec show ?case
|
|
39 |
proof
|
|
40 |
assume ny: "n = y"
|
|
41 |
have "P n"
|
|
42 |
by (rule R) (rule Suc)
|
|
43 |
with ny show ?case by simp
|
|
44 |
next
|
|
45 |
assume "n \<noteq> y"
|
|
46 |
with Suc have "y < n" by simp
|
|
47 |
thus ?case by (rule Suc)
|
|
48 |
qed
|
|
49 |
qed
|
|
50 |
qed
|
|
51 |
|
|
52 |
text {*
|
|
53 |
Bounded search for a natural number satisfying a decidable predicate.
|
|
54 |
*}
|
|
55 |
|
|
56 |
lemma search:
|
|
57 |
assumes dec: "\<And>x::nat. P x \<or> \<not> P x"
|
|
58 |
shows "(\<exists>x<y. P x) \<or> \<not> (\<exists>x<y. P x)"
|
|
59 |
proof (induct y)
|
|
60 |
case 0 show ?case by simp
|
|
61 |
next
|
|
62 |
case (Suc z)
|
|
63 |
thus ?case
|
|
64 |
proof
|
|
65 |
assume "\<exists>x<z. P x"
|
|
66 |
then obtain x where le: "x < z" and P: "P x" by iprover
|
|
67 |
from le have "x < Suc z" by simp
|
|
68 |
with P show ?case by iprover
|
|
69 |
next
|
|
70 |
assume nex: "\<not> (\<exists>x<z. P x)"
|
|
71 |
from dec show ?case
|
|
72 |
proof
|
|
73 |
assume P: "P z"
|
|
74 |
have "z < Suc z" by simp
|
|
75 |
with P show ?thesis by iprover
|
|
76 |
next
|
|
77 |
assume nP: "\<not> P z"
|
|
78 |
have "\<not> (\<exists>x<Suc z. P x)"
|
|
79 |
proof
|
|
80 |
assume "\<exists>x<Suc z. P x"
|
|
81 |
then obtain x where le: "x < Suc z" and P: "P x" by iprover
|
|
82 |
have "x < z"
|
|
83 |
proof (cases "x = z")
|
|
84 |
case True
|
|
85 |
with nP and P show ?thesis by simp
|
|
86 |
next
|
|
87 |
case False
|
|
88 |
with le show ?thesis by simp
|
|
89 |
qed
|
|
90 |
with P have "\<exists>x<z. P x" by iprover
|
|
91 |
with nex show False ..
|
|
92 |
qed
|
|
93 |
thus ?case by iprover
|
|
94 |
qed
|
|
95 |
qed
|
|
96 |
qed
|
|
97 |
|
|
98 |
end
|