equal
deleted
inserted
replaced
6 |
6 |
7 theory Util |
7 theory Util |
8 imports "~~/src/HOL/Library/Old_Datatype" |
8 imports "~~/src/HOL/Library/Old_Datatype" |
9 begin |
9 begin |
10 |
10 |
11 text \<open> |
11 text \<open>Decidability of equality on natural numbers.\<close> |
12 Decidability of equality on natural numbers. |
|
13 \<close> |
|
14 |
12 |
15 lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n" |
13 lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n" |
16 apply (induct m) |
14 apply (induct m) |
17 apply (case_tac n) |
15 apply (case_tac n) |
18 apply (case_tac [3] n) |
16 apply (case_tac [3] n) |
19 apply (simp only: nat.simps, iprover?)+ |
17 apply (simp only: nat.simps, iprover?)+ |
20 done |
18 done |
21 |
19 |
22 text \<open> |
20 text \<open> |
23 Well-founded induction on natural numbers, derived using the standard |
21 Well-founded induction on natural numbers, derived using the standard |
24 structural induction rule. |
22 structural induction rule. |
25 \<close> |
23 \<close> |
26 |
24 |
27 lemma nat_wf_ind: |
25 lemma nat_wf_ind: |
28 assumes R: "\<And>x::nat. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x" |
26 assumes R: "\<And>x::nat. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x" |
29 shows "P z" |
27 shows "P z" |
30 proof (rule R) |
28 proof (rule R) |
31 show "\<And>y. y < z \<Longrightarrow> P y" |
29 show "\<And>y. y < z \<Longrightarrow> P y" |
32 proof (induct z) |
30 proof (induct z) |
33 case 0 |
31 case 0 |
34 thus ?case by simp |
32 then show ?case by simp |
35 next |
33 next |
36 case (Suc n y) |
34 case (Suc n y) |
37 from nat_eq_dec show ?case |
35 from nat_eq_dec show ?case |
38 proof |
36 proof |
39 assume ny: "n = y" |
37 assume ny: "n = y" |
41 by (rule R) (rule Suc) |
39 by (rule R) (rule Suc) |
42 with ny show ?case by simp |
40 with ny show ?case by simp |
43 next |
41 next |
44 assume "n \<noteq> y" |
42 assume "n \<noteq> y" |
45 with Suc have "y < n" by simp |
43 with Suc have "y < n" by simp |
46 thus ?case by (rule Suc) |
44 then show ?case by (rule Suc) |
47 qed |
45 qed |
48 qed |
46 qed |
49 qed |
47 qed |
50 |
48 |
51 text \<open> |
49 text \<open>Bounded search for a natural number satisfying a decidable predicate.\<close> |
52 Bounded search for a natural number satisfying a decidable predicate. |
|
53 \<close> |
|
54 |
50 |
55 lemma search: |
51 lemma search: |
56 assumes dec: "\<And>x::nat. P x \<or> \<not> P x" |
52 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)" |
53 shows "(\<exists>x<y. P x) \<or> \<not> (\<exists>x<y. P x)" |
58 proof (induct y) |
54 proof (induct y) |
59 case 0 show ?case by simp |
55 case 0 |
|
56 show ?case by simp |
60 next |
57 next |
61 case (Suc z) |
58 case (Suc z) |
62 thus ?case |
59 then show ?case |
63 proof |
60 proof |
64 assume "\<exists>x<z. P x" |
61 assume "\<exists>x<z. P x" |
65 then obtain x where le: "x < z" and P: "P x" by iprover |
62 then obtain x where le: "x < z" and P: "P x" by iprover |
66 from le have "x < Suc z" by simp |
63 from le have "x < Suc z" by simp |
67 with P show ?case by iprover |
64 with P show ?case by iprover |
87 with le show ?thesis by simp |
84 with le show ?thesis by simp |
88 qed |
85 qed |
89 with P have "\<exists>x<z. P x" by iprover |
86 with P have "\<exists>x<z. P x" by iprover |
90 with nex show False .. |
87 with nex show False .. |
91 qed |
88 qed |
92 thus ?case by iprover |
89 then show ?case by iprover |
93 qed |
90 qed |
94 qed |
91 qed |
95 qed |
92 qed |
96 |
93 |
97 end |
94 end |