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