(*
    $Id: sol.thy,v 1.2 2004/11/23 15:14:34 webertj Exp $
    Author: Farhad Mehta
*)

(*<*) theory sol imports Main begin (*>*)

consts
  occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat"
primrec
  "occurs a [] = 0"
  "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)"

lemma [simp]:"occurs a (xs @ ys) = occurs a xs + occurs a ys "
  apply (induct_tac xs)
  apply auto
  done

lemma "occurs a xs = occurs a (rev xs)"
  apply (induct_tac xs)  
  apply auto
  done

lemma "occurs a xs <= length xs"
  apply (induct_tac xs)  
  apply auto
  done

lemma "occurs a (replicate n a) = n"
  apply (induct_tac n)
  apply auto
  done

consts
  areAll :: "'a list \<Rightarrow> 'a \<Rightarrow> bool"
primrec
  "areAll [] a = True"
  "areAll (x#xs) a = ((x=a) \<and> (areAll xs a))"

lemma "areAll xs a \<longrightarrow> occurs a xs = length xs"
  apply (induct_tac xs)
  apply auto
  done

lemma "occurs a xs = length xs \<longrightarrow> areAll xs a"
  -- {* additional lemmas needed *}
  apply (induct_tac xs)  
     apply auto

  oops

   lemma l:"occurs a xs < Suc( length xs)"
     apply (induct_tac xs)  
     apply auto
     done

   lemma a:"(a::nat) < b \<longrightarrow> (a ~= b)"
     apply auto
     done

   lemma ne:"occurs a xs ~= Suc( length xs)"
     apply (auto simp:l a)
     done

   lemma "occurs a xs = length xs \<longrightarrow> areAll xs a"
     apply (induct_tac "xs")
     apply (auto simp:ne)
     done

consts
  delall :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
primrec
  "delall a [] = []"
  "delall a (x#xs) = (if (x=a) then (delall a xs) else (x#delall a xs))"


lemma "occurs a (delall a xs) = 0"
  apply (induct_tac xs)  
  apply auto
  done

consts
  del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
primrec
  "del1 a [] = []"
  "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"

(* A lemma, you'd think to be true from our experience with delAll *)
lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
  -- {* wrong; precondition needed *}
  oops

    lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
      apply (induct_tac xs)  
      apply auto
      -- {* still wrong *}
      oops

    lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
      apply (induct_tac xs)  
      apply auto
      -- {* correct! *}
      done

consts
  replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
primrec
  "replace a b [] = []"
  "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs)) 
                            else (x#(replace a b xs)))"

lemma "occurs a xs = occurs b (replace a b xs)"
  apply (induct_tac xs)  
  apply auto
  -- {* wrong; precondition needed *}
  oops

   lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
     apply (induct_tac xs)  
     apply auto
     done

consts
  remDups :: "'a list \<Rightarrow> 'a list"
primrec
  "remDups [] = []"
  "remDups (x#xs) = (if (0 < occurs x xs) then (remDups xs) 
                          else (x#(remDups xs)))"

lemma h:"occurs x xs = 0 \<longrightarrow> occurs x (remDups xs) = 0"
  apply (induct_tac xs)  
  apply auto
  done

lemma "occurs x (remDups xs) <= 1" 
  apply (induct_tac xs)  
  apply (auto simp:h)
  done

consts
  unique :: "'a list \<Rightarrow> bool"
primrec
  "unique [] = True"
  "unique (x#xs) = (if (occurs x xs = 0) then (unique xs) else False)"

lemma "unique(remDups xs)"
  apply (induct_tac xs)  
  apply (auto simp:h)
  done

end