theory Demo95 imports Main begin

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

-- {* a recursive data type: *}
datatype 'a tree = Tip | Node "'a tree" 'a "'a 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 [] = []" |
  (* complete *)


-- {* on trees *}
primrec
  mirror :: "'a tree => 'a 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 *}

theorem rv_rv: "rv (rv xs) = xs"
  oops


-- {* 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 "itrev xs ys = rev xs @ ys"
  oops


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


end