summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Proofs/Extraction/Util.thy

author | wenzelm |

Sun Nov 02 18:21:45 2014 +0100 (2014-11-02) | |

changeset 58889 | 5b7a9633cfa8 |

parent 58372 | bfd497f2f4c2 |

child 59730 | b7c394c7a619 |

permissions | -rw-r--r-- |

modernized header uniformly as section;

1 (* Title: HOL/Proofs/Extraction/Util.thy

2 Author: Stefan Berghofer, TU Muenchen

3 *)

5 section {* Auxiliary lemmas used in program extraction examples *}

7 theory Util

8 imports Old_Datatype

9 begin

11 text {*

12 Decidability of equality on natural numbers.

13 *}

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

22 text {*

23 Well-founded induction on natural numbers, derived using the standard

24 structural induction rule.

25 *}

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

51 text {*

52 Bounded search for a natural number satisfying a decidable predicate.

53 *}

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

97 end