ToyList.thy

theory ToyList
  imports Main
begin
no_notation Nil ("[]") and Cons (infixr "#" 65) and append (infixr "@" 65)
hide_type list
hide_const rev

datatype 'a list = Nil                 ("[]")
  | Cons 'a "'a list"    (infixr "#" 65)

primrec append :: "'a list => 'a list => 'a list" (infixr "@" 65)
  where
  "[] @ ys      = ys" |
  "(x # xs) @ ys = x # (xs @ ys)"

value "append (1 # 2 # 3 # []) (4 # 5 # 6 # [])"
value "append (a # b # c # []) []"

lemma app_Nil [simp]: "xs @ [] = xs"
  apply (induct_tac xs)
  apply simp
  apply simp
  done

lemma app_Nil2 [simp]: "xs @ [] = xs"
  apply(induct_tac xs)
  apply auto
  done

lemma app_Nil3 [simp]: "[] @ xs = xs"
  apply(induct_tac xs)
  apply auto
  done


lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
  apply (induct_tac xs)
  apply auto
  done


export_code append in Scala module_name Example file "Example.scala"

end