theory Liste_predef_VI_cas
imports Main 

begin

no_notation Nil ("[]") and Cons (infixr "#" 65) and append (infixr "@" 65)
hide_const length
hide_const map
(*
hide_type list
hide_const rev
*)
datatype 'a lista = Nil ("[]") | Cons 'a "'a lista" (infixr "#" 65)

declare [[names_short]] 

primrec app :: "'a lista \<Rightarrow> 'a lista \<Rightarrow> 'a lista" (infixr "@" 65) where 
"[] @ ys = ys " | 
"(x # xs) @ ys = x # (xs @ ys)"

primrec rev :: "'a lista \<Rightarrow> 'a lista" where
"rev [] = [] " |
"rev (x # xs) = (rev xs) @ (x # [])"

value "Cons True (Cons False Nil)"
value "rev (True # False # [])"
value "rev (a # b # c # [])" 
value "(a0 # a1 # []) @ []"

(* 3 *)
lemma app_Nil2[simp]: "xs @ [] = xs"
  apply (induction xs)
   apply auto
  done
  
(* 4 *)
lemma app_assoc[simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
  apply (induction xs)
   apply auto
   done

(* 2 *)
lemma rev_app[simp]: "rev (xs @ ys) = rev ys @ rev xs"
  apply (induction xs)
  apply auto (* ne prolazi ni bazni slucaj, javlja se _ @ [], pa idemo na korak 3 
                nakon koraka 3 vracamo se na ovaj dokaz i vidimo da nam fali 
                asocijativnost @ i idemo na korak 4 *)
  done

(* 1 *)
theorem rev_rev[simp] : "rev (rev xs) = xs"
  apply (induction xs)
   apply (auto) (* vidimo da nam treba rev _ @ _ pa idemo na korak 2 *)
done 

primrec length :: "'a lista \<Rightarrow> nat" where 
"length [] = 0" | 
"length (x # xs) = Suc (length xs)"

primrec count :: "'a \<Rightarrow> 'a lista \<Rightarrow> nat" where
"count x [] = 0" |
"count x (y # xs) = (if x = y then Suc (count x xs) else count x xs)" 

lemma "count x xs \<le> length xs"
proof (induction xs)
case Nil
then show ?case 
by simp
next
case (Cons x1 xs)
thm Cons
show ?case 
proof (cases "x = x1")
case True
then have "count x (x1 # xs) = Suc (count x xs)" by simp
(* apply (simp only: count.simps split:if_split) 
   apply simp
   done
*)
also have "... \<le> Suc (length xs)" using Cons by simp
also have "... = length (x1 # xs)" by simp
finally show ?thesis .
next 
case False
then have "count x (x1 # xs) = count x xs" by simp
also have "... \<le> length xs" using Cons by simp
also have "... \<le> length (x1 # xs)" by simp
finally show ?thesis .
qed
qed

(* sve definicije nad listama se rade nad rekurzivnom strukturom liste i uvek cemo imati dva
   slucaja: prazna lista ([]) i lista koja ima makar jedan element (x1 # xs) *)

primrec snoc:: "'a lista \<Rightarrow> 'a \<Rightarrow> 'a lista" where
"snoc [] x = (x # [])" |
"snoc (x1 # xs) x = x1 # (snoc xs x)"

(* U drugom delu rekurzivne definicije moramo se pozivati na problem manje dimenzije, 
   kod lista je to najcesce rep liste *)

primrec rev_snoc :: "'a lista \<Rightarrow> 'a lista" where
"rev_snoc [] = [] " |
"rev_snoc (x1 # xs) = snoc (rev_snoc xs) x1"

(* Prilikom uvodjenja dodatnih lema u [simp] vodite racuna da ne napravite 
   beskonacnu petlju, tj. da se u simp-u ne nalaze dve leme koje svode A na B i
   B na A kada su A i B iste dimenzije *)

(* *** *)
lemma rev_snoc_levo[simp]: "rev_snoc (snoc xs x1) = x1 # rev_snoc xs"
apply (induction xs)
apply auto
done

lemma "rev_snoc(rev_snoc xs) = xs"
apply (induction xs)
apply auto (* javlja se rev_snoc (snoc _ _) pa dodajemo lemu sa oznakom *** *)
done

lemma rev_snoc_isar: "rev_snoc (rev_snoc xs) = xs" 
proof (induction xs)
case Nil
then show ?case by simp
next
case (Cons x1 xs)
thm Cons
have "rev_snoc (rev_snoc (x1 # xs)) = rev_snoc (snoc (rev_snoc xs) x1)"
by (simp only: rev_snoc.simps)
also have "... = x1 # rev_snoc (rev_snoc xs)" 
by (simp only: rev_snoc_levo[of "rev_snoc xs" x1])
also have "... = x1 # xs" 
using Cons by simp
finally show ?case .
qed


primrec map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a lista \<Rightarrow> 'b lista" where 
"map f [] = []" |
"map f (x # xs) = f x # (map f xs)"

(* Definisati funkciju intersperse_inside koja rasporedjuje element a iza svakog elemnta liste:
   a [x1, ..., xn] = [x1, a, x2, a, ..., a, xn, a]. *)
primrec intersperse :: "'a \<Rightarrow> 'a lista \<Rightarrow> 'a lista" where
"intersperse x [] = []" |
"intersperse x (x1 # xs) = x1 # x # intersperse x xs"

value "intersperse (1::nat)(2 # 3 # 4 # [])"
value "intersperse (1::nat)([])"
value "intersperse (1::nat)(2 # [])"

lemma "map f (intersperse x xs) = intersperse (f x) (map f xs)"
apply (induction xs)
apply auto
done

lemma map_isar: "map f (intersperse x xs) = intersperse (f x) (map f xs)"
proof (induction xs)
case Nil
then show ?case by simp
next
case (Cons x1 xs)
have "map f (intersperse x (x1 # xs)) = map f (x1 # x # intersperse x xs)" 
by (simp only: intersperse.simps)
also have "... = (f x1) # (f x) # map f (intersperse x xs)" 
by (simp only: map.simps)
also have "... = (f x1) # (f x) # intersperse (f x) (map f xs)" 
using Cons by simp
also have "... = intersperse (f x) ((f x1) # map f xs)" 
by (simp only: intersperse.simps)
also have "... = intersperse (f x) (map f (x1 # xs))"
by (simp only: map.simps)
finally show ?case .
qed

(* Definisati funkciju intersperse_inside koja rasporedjuje element a izmedju elemenata liste:
   a [x1, ..., xn] = [x1, a, x2, a, ..., a, xn]. *)
primrec intersperse_inside :: "'a \<Rightarrow> 'a lista \<Rightarrow> 'a lista" where
"intersperse_inside a [] = []" |
"intersperse_inside a (x1 # xs) = (if xs = [] then (x1 # []) else (x1 # a # (intersperse_inside a xs)))"

value "intersperse_inside (1::nat)(2 # 3 # 4 # [])"
value "intersperse_inside (1::nat)([])"
value "intersperse_inside (1::nat)(2 # [])"

lemma map_prazna[simp]: "map f xs = [] \<Longrightarrow> xs = []"
apply (cases xs)
apply auto
done

(* Krace zapisano:
lemma [simp]: "map f xs = [] \<Longrightarrow> xs = []"
by (cases xs) auto

The by command is useful for proofs like these that use assumption heavily. 
It executes an apply command, then tries to prove all remaining subgoals
using assumption . Since (if successful) it ends the proof, it also replaces the
done symbol.
*)


(* Dokazati narednu lemu automatski i uz pomoc isara *)
lemma "map f (intersperse_inside x xs) = intersperse_inside (f x) (map f xs)"
apply (induction xs)
apply auto (* vidimo da se javlja map f xs = [] pa uvodimo dodatnu lemu --- iznad *)
done

lemma map_inside_isar: "map f (intersperse_inside x xs) = intersperse_inside (f x) (map f xs)"
proof (induction xs)
case Nil
show ?case by simp
next
case (Cons x1 xs)
show ?case
proof (cases "xs = []")
case True
thus ?thesis by simp
next
case False
then have "map f (intersperse_inside x (x1 # xs)) = map f (x1 # x # intersperse_inside x xs)"
by simp
also have "... = f x1 # (map f (x # intersperse_inside x xs))" by simp
also have "... = f x1 # (f x # (map f (intersperse_inside x xs)))" by simp
also have "... = f x1 # (f x # (intersperse_inside (f x) (map f xs)))" 
using Cons by simp
also have "... = intersperse_inside (f x) (f x1 # (map f xs))" using `xs \<noteq> []` by auto
also have "... = intersperse_inside (f x) (map f (x1 # xs))" by (simp only: map.simps)
finally show ?thesis .
qed
qed

end