1 (* Title: HOL/Extraction/Util.thy |
|
2 Author: Stefan Berghofer, TU Muenchen |
|
3 *) |
|
4 |
|
5 header {* Auxiliary lemmas used in program extraction examples *} |
|
6 |
|
7 theory Util |
|
8 imports Main |
|
9 begin |
|
10 |
|
11 text {* |
|
12 Decidability of equality on natural numbers. |
|
13 *} |
|
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 |
|
22 text {* |
|
23 Well-founded induction on natural numbers, derived using the standard |
|
24 structural induction rule. |
|
25 *} |
|
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" |
|
41 by (rule R) (rule Suc) |
|
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 |
|
51 text {* |
|
52 Bounded search for a natural number satisfying a decidable predicate. |
|
53 *} |
|
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 |
|
79 assume "\<exists>x<Suc z. P x" |
|
80 then obtain x where le: "x < Suc z" and P: "P x" by iprover |
|
81 have "x < z" |
|
82 proof (cases "x = z") |
|
83 case True |
|
84 with nP and P show ?thesis by simp |
|
85 next |
|
86 case False |
|
87 with le show ?thesis by simp |
|
88 qed |
|
89 with P have "\<exists>x<z. P x" by iprover |
|
90 with nex show False .. |
|
91 qed |
|
92 thus ?case by iprover |
|
93 qed |
|
94 qed |
|
95 qed |
|
96 |
|
97 end |
|