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)"

(* Exercise 1 *)
(* append :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list *)

(* 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  


(* 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))"

fun member2:: "'a => 'a list => bool"
where
"member2 e []     = False" |
"member2 e (x#xs) = (e=x \<or> (member2 e xs))"

(* Example 17 *)
(* A function that is not sufficiently defined, i.e. incomplete or not total *)

fun secondElt:: "'a list \<Rightarrow> 'a"
where
"secondElt (x#(y#ys)) = y"

(* Exercise 6 *)

thm "length_append"

thm "member.simps"

thm "nth.simps"

find_theorems "rev" "length"

find_theorems "member"




(* Exercise 7 *)

(* We can perform rewriting step by step...*)
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 y [x,y,z]"
  (* ... or we can print all the rewriting steps using 'simp_trace', but it is hard to read! *)
  using [[simp_trace=true]]
  apply auto
  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 \<Rightarrow> 'a list => nat"
where
"index y (x#xs) = (if x=y then 0 else 1+(index y xs))"


thm "List.nth.simps"
value "List.nth [10::nat,20,30] 2"

export_code member index in Scala



end