author | wenzelm |
Thu, 19 Sep 2019 16:38:05 +0200 | |
changeset 70735 | 561b11865cb5 |
parent 66258 | 2b83dd24b301 |
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 |
|
66258 | 8 |
imports Main |
25421 | 9 |
begin |
10 |
||
63361 | 11 |
text \<open>Decidability of equality on natural numbers.\<close> |
25421 | 12 |
|
13 |
lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n" |
|
14 |
apply (induct m) |
|
15 |
apply (case_tac n) |
|
16 |
apply (case_tac [3] n) |
|
17 |
apply (simp only: nat.simps, iprover?)+ |
|
18 |
done |
|
19 |
||
61986 | 20 |
text \<open> |
63361 | 21 |
Well-founded induction on natural numbers, derived using the standard |
22 |
structural induction rule. |
|
61986 | 23 |
\<close> |
25421 | 24 |
|
25 |
lemma nat_wf_ind: |
|
26 |
assumes R: "\<And>x::nat. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x" |
|
27 |
shows "P z" |
|
28 |
proof (rule R) |
|
29 |
show "\<And>y. y < z \<Longrightarrow> P y" |
|
30 |
proof (induct z) |
|
31 |
case 0 |
|
63361 | 32 |
then show ?case by simp |
25421 | 33 |
next |
34 |
case (Suc n y) |
|
35 |
from nat_eq_dec show ?case |
|
36 |
proof |
|
37 |
assume ny: "n = y" |
|
38 |
have "P n" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
25421
diff
changeset
|
39 |
by (rule R) (rule Suc) |
25421 | 40 |
with ny show ?case by simp |
41 |
next |
|
42 |
assume "n \<noteq> y" |
|
43 |
with Suc have "y < n" by simp |
|
63361 | 44 |
then show ?case by (rule Suc) |
25421 | 45 |
qed |
46 |
qed |
|
47 |
qed |
|
48 |
||
63361 | 49 |
text \<open>Bounded search for a natural number satisfying a decidable predicate.\<close> |
25421 | 50 |
|
51 |
lemma search: |
|
52 |
assumes dec: "\<And>x::nat. P x \<or> \<not> P x" |
|
53 |
shows "(\<exists>x<y. P x) \<or> \<not> (\<exists>x<y. P x)" |
|
54 |
proof (induct y) |
|
63361 | 55 |
case 0 |
56 |
show ?case by simp |
|
25421 | 57 |
next |
58 |
case (Suc z) |
|
63361 | 59 |
then show ?case |
25421 | 60 |
proof |
61 |
assume "\<exists>x<z. P x" |
|
62 |
then obtain x where le: "x < z" and P: "P x" by iprover |
|
63 |
from le have "x < Suc z" by simp |
|
64 |
with P show ?case by iprover |
|
65 |
next |
|
66 |
assume nex: "\<not> (\<exists>x<z. P x)" |
|
67 |
from dec show ?case |
|
68 |
proof |
|
69 |
assume P: "P z" |
|
70 |
have "z < Suc z" by simp |
|
71 |
with P show ?thesis by iprover |
|
72 |
next |
|
73 |
assume nP: "\<not> P z" |
|
74 |
have "\<not> (\<exists>x<Suc z. P x)" |
|
75 |
proof |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
25421
diff
changeset
|
76 |
assume "\<exists>x<Suc z. P x" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
25421
diff
changeset
|
77 |
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
|
78 |
have "x < z" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
25421
diff
changeset
|
79 |
proof (cases "x = z") |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
25421
diff
changeset
|
80 |
case True |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
25421
diff
changeset
|
81 |
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
|
82 |
next |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
25421
diff
changeset
|
83 |
case False |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
25421
diff
changeset
|
84 |
with le show ?thesis by simp |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
25421
diff
changeset
|
85 |
qed |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
25421
diff
changeset
|
86 |
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
|
87 |
with nex show False .. |
25421 | 88 |
qed |
63361 | 89 |
then show ?case by iprover |
25421 | 90 |
qed |
91 |
qed |
|
92 |
qed |
|
93 |
||
94 |
end |