src/HOL/Extraction/Pigeonhole.thy
changeset 17027 8bbe57116d13
parent 17024 ae4a8446df16
child 17145 e623e57b0f44
equal deleted inserted replaced
17026:43cc86fd3536 17027:8bbe57116d13
    22   apply (case_tac [3] n)
    22   apply (case_tac [3] n)
    23   apply (simp only: nat.simps, rules?)+
    23   apply (simp only: nat.simps, rules?)+
    24   done
    24   done
    25 
    25 
    26 text {*
    26 text {*
    27 We can decide whether an array @{term "f"} of length @{term "l+(1::nat)"}
    27 We can decide whether an array @{term "f"} of length @{term "l"}
    28 contains an element @{term "x"}.
    28 contains an element @{term "x"}.
    29 *}
    29 *}
    30 
    30 
    31 lemma search: "(\<exists>j<(l::nat). (x::nat) = f j) \<or> \<not> (\<exists>j<l. x = f j)"
    31 lemma search: "(\<exists>j<(l::nat). (x::nat) = f j) \<or> \<not> (\<exists>j<l. x = f j)"
    32 proof (induct l)
    32 proof (induct l)