theory Demo9 imports Main begin

-- -----------------------------------------------------------------------

-- {* a recursive data type: *}
datatype ('a,'b) tree = Tip | Node "('a,'b) tree" 'b "('a,'b) tree"

print_theorems

-- {* distincteness of constructors automatic: *}
lemma "Tip ~= Node l x r" by simp


-- {* case sytax, case distinction manual *}
lemma "(1::nat) \<le> (case t of Tip \<Rightarrow> 1 | Node l x r \<Rightarrow> x+1)"
  apply(case_tac t)
  apply auto
  done

-- {* inifinitely branching: *}
datatype 'a inftree = Tp | Nd 'a "nat \<Rightarrow> 'a inftree"

-- {* mutually recursive *} 
datatype 
  ty = Integer | Real | RefT ref
  and
  ref = Class | Array ty







-- -----------------------------------------------------------------  

-- {* primitive recursion *}

primrec
  app :: "'a list => 'a list => 'a list"
where
  "app Nil ys = ys" |
  "app (Cons x xs) ys = Cons x (app xs ys)"

print_theorems

primrec
  rv :: "'a list => 'a list"
where
  "rv [] = []" |
  "rv (x#xs) = app (rv xs) [x]"


-- {* on trees *}
primrec
  mirror :: "('a,'b) tree => ('a,'b) tree"
where
  "mirror Tip = Tip" |
  "mirror (Node l x r) = Node (mirror r) x (mirror l)"

print_theorems


-- {* mutual recursion *}
primrec
  has_int :: "ty \<Rightarrow> bool" and
  has_int_ref :: "ref \<Rightarrow> bool"
where
  "has_int Integer       = True" |
  "has_int Real          = False" |
  "has_int (RefT T)      = has_int_ref T" |

  "has_int_ref Class     = False" |
  "has_int_ref (Array T) = has_int T"



-- ------------------------------------------------------------------

-- {* structural induction *}

-- {* finding lemmas *}

lemma app' [simp]: "app xs [] = xs"
  apply (induct xs)
  apply auto
  done

lemma app'' [simp]: 
  "app (app xs ys) zs = app xs (app ys zs)"
  apply (induct xs)
   apply simp
  apply simp
  done

lemma app [simp]: "rv (app xs ys) = app (rv ys) (rv xs)"
  apply (induct xs)
   apply simp
  apply simp
  done
   
theorem rv_rv: "rv (rv xs) = xs"
  apply (induct xs)
   apply simp
  apply simp
  done


-- {* induction heuristics *}

primrec
  itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
  "itrev [] ys = ys" |
  "itrev (x#xs) ys = itrev xs (x#ys)"

lemma x: "\<forall>ys. itrev xs ys = rev xs @ ys"
  apply (induct_tac xs)
   apply simp
  apply simp
  done

lemma "itrev xs [] = rev xs"
  apply (simp add: x)
  done


-- ------------------------------------------------------------------

primrec
  lsum :: "nat list \<Rightarrow> nat"
where
  "lsum [] = 0" |
  "lsum (x#xs) = x + lsum xs"

lemma lsum_append [simp]:
  "lsum (xs @ ys) = lsum xs + lsum ys"
  apply (induct_tac xs)
   apply simp
  apply simp
  done

lemma 
  "2 * lsum [0 ..< Suc n] = n * (n + 1)"
  apply (induct_tac n)
   apply simp
  apply simp
  done

lemma 
  "lsum (replicate n a) = n * a"
  apply (induct_tac n)
   apply simp
  apply simp
  done

primrec
  lsumT :: "nat list \<Rightarrow> nat \<Rightarrow> nat" 
where
  "lsumT [] s = s"
| "lsumT (x#xs) s = lsumT xs (s + x)"

lemma lsumT_is_correct:
  "\<forall>n. lsumT xs n = lsum xs + n"
  apply (induct_tac xs)
   apply auto
  done

lemma lsum_really_is_correct:
  "lsumT xs 0 = lsum xs"
  by (simp add: lsumT_is_correct)
 

end