theory cm2 imports Main HOL.Rat "~~/src/HOL/Library/Code_Target_Nat" (* to hide 0, Succ rep. of nats *) begin (* Terms and types *) value "True" value "1" value "1::nat" value "2+5::nat" value "2+3::nat" value "[True,False]" value "x" value "[x,y,z]" value "[1,2,3]" value "[2::nat,6,10]" value "[(2::nat),6,10]" value "[x,y,z]" value "(x,y,z)" value "(x,x,x)" value "append" value "\x. x" (* Exercise 1 *) (* Exercice 2 *) (* Exercise 3 *) (* Exercise 4 *) value "-56.188::rat" value "''toto''" (* Every data has a (hidden) constructor representation *) value "1::nat" value "2::nat" (* Integers are represented by couples of nat (x,y), where the integer value is x-y *) lemma "(Abs_Integ(1,4) + Abs_Integ(3,0)) = 0" sorry (* by (smt plus_int.abs_eq nat.abs_eq split_conv) *) (* found by hand :/ *) (* Exercise 5 *) (* Example 14 *) fun member:: "'a => 'a list => bool" where "member e [] = False" | "member e (x#xs) = (if e=x then True else (member e xs))" thm "member.simps" thm "length_append" find_theorems "rev" "length" fun member2:: "'a => 'a list => bool" where "member2 e [] = False" | "member2 e (x#xs) = (e=x \ (member2 e xs))" (* Example 17 *) (* A function that is not sufficiently defined, i.e. incomplete or not total *) fun secondElt:: "'a list \ 'a" where "secondElt (x#(y#ys)) = y" (* Exercise 6 *) (* Exercise 7 *) lemma "member (2::nat) [1,2,3] = True" apply (subst member.simps) apply (simp del:member.simps) apply (subst member.simps) apply (simp del:member.simps) done lemma "member y [x,y,z]" apply (subst member.simps) apply (subst member.simps) apply simp done lemma "member u (append [u] v)" apply (subst append.simps) apply (subst member.simps) apply simp done (* Exercice 8 *) lemma "member v (append u [v])" apply (subst append.simps) apply (subst member.simps) sorry (* Exercise 9 *) fun index:: "'a \ 'a list => nat" where "index y (x#xs) = (if x=y then 0 else 1+(index y xs))" export_code member index in Scala (* file "test.scala" *) end