theory Examples
imports
Complex_Main
begin
section \Main example\
text \Write a function that removes the first occurrence of a given element from a given list.\
(*
datatype 'a list2 =
Nil
| Cons 'a \'a list2\
datatype nat2 =
Zero
| Succ nat2
fun length where
\length Nil = Zero\
| \length (Cons x xs) = Succ (length xs)\
fun less where
\less _ Zero = False\
| \less Zero _ = True\
| \less (Succ n) (Succ m) = less n m\
fun set where
\set Nil = {}\
| \set (Cons x xs) = {x} \ set xs\
*)
subsection \Implementation\
(*
fun remove1 where
\remove1 _ Nil = Nil\
| \remove1 y (Cons x xs) = (if x = y then xs else remove1 y xs)\
*)
fun remove1 where
\remove1 _ Nil = Nil\
| \remove1 y (Cons x xs) = (if x = y then xs else Cons x (remove1 y xs))\
subsection \Specification\
lemma \y \ set xs \ less (length (remove1 y xs)) (length xs)\
proof (induction xs)
case Nil
then show ?case
by simp
next
case (Cons x xs)
then show ?case
proof (cases \x = y\)
case True
then have \remove1 y (Cons x xs) = xs\
using Cons by simp
then have \length (remove1 y (Cons x xs)) = length xs\
by simp
moreover have \less (length xs) (length (Cons x xs))\
by (induction xs) auto
ultimately show ?thesis
by simp
next
case False
then have \y \ set xs\
using Cons by simp
then have \less (length (remove1 y xs)) (length xs)\
using Cons by simp
then show ?thesis
using False by simp
qed
qed
lemma \x \ y \ x \ set xs \ x \ set (remove1 y xs)\
proof (induction xs)
case Nil
then show ?case by simp
next
case (Cons x1 xs)
then show ?case by auto
qed
lemma \y \ set xs \ length xs = length (remove1 y xs)\
proof (induction xs)
case Nil
then show ?case by simp
next
case (Cons x1 xs)
then show ?case by auto
qed
subsection \Evaluation\
value \remove1 ''a'' (Cons ''a'' (Cons ''b'' (Cons ''a'' Nil)))\
subsection \Automation\
lemma \y \ set xs \ less (length (remove1 y xs)) (length xs)\
by (induction xs) auto
lemma \x \ y \ x \ set xs \ x \ set (remove1 y xs)\
by (induction xs) auto
lemma \y \ set xs \ length xs = length (remove1 y xs)\
by (induction xs) auto
subsection \Sledgehammer\
lemma \xs @ ys = ys @ xs \ length xs = length ys \ xs = ys\
using append_eq_append_conv by blast
subsection \Code export\
export_code remove1 in Haskell
section \Classical\
subsection \LEM\
lemma \p \ \ p\
by simp
subsection \Proof by contradiction\
lemma \\x. drunk x \ (\x. drunk x)\
proof (cases \\x. drunk x\)
case True
then have \drunk a \ (\x. drunk x)\ for a by (rule impI)
then show ?thesis by (rule exI)
next
case False
then have \\x. \ drunk x\ by simp
then obtain a where \\ drunk a\ by (rule exE)
have \drunk a \ (\x. drunk x)\
proof
assume \drunk a\
with \\ drunk a\ show \\x. drunk x\ by contradiction
qed
then show ?thesis by (rule exI)
qed
lemma \\x. drunk x \ (\x. drunk x)\
by blast
section \Working with infinite sets\
definition \positive_reals \ {x | x. 0 < x} :: real set\
section \Axiom of choice (Hilbert epsilon)\
definition \smallest_positive_real \ Inf {x | x. 0 < x} :: real\
section \Coinduction and corecursion\
codatatype (sset: 'a) Stream = SCons (shd: 'a) (stl: \'a Stream\)
for map: smap
primcorec siterate :: \('a \ 'a) \ 'a \ 'a Stream\ where
\siterate f a = SCons a (siterate f (f a))\
lemma \smap f (siterate f x) = siterate f (f x)\
proof (coinduction arbitrary: x)
case Eq_Stream
then show ?case
by (metis Stream.map_sel(1) Stream.map_sel(2) siterate.simps(1) siterate.simps(2))
qed
primrec stake :: \nat \ 'a Stream \ 'a list\ where
\stake 0 s = []\
| \stake (Suc n) s = shd s # stake n (stl s)\
section \Termination proofs\
function sum :: \nat \ nat \ nat\ where
\sum i N = (if i > N then 0 else i + sum (Suc i) N)\
by pat_completeness auto
termination
by (relation \measure (\(i,N). N + 1 - i)\) auto
fun sum' where \sum' n = sum 0 n\
value \sum' 10\
end