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--
```     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
```