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 *)
     4 
     5 section {* Auxiliary lemmas used in program extraction examples *}
     6 
     7 theory Util
     8 imports Old_Datatype
     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