Theory Old_Show_Examples

Copyright 2009-2014 Christian Sternagel, René Thiemann

This file is part of IsaFoR/CeTA.

IsaFoR/CeTA is free software: you can redistribute it and/or modify it under the
terms of the GNU Lesser General Public License as published by the Free Software
Foundation, either version 3 of the License, or (at your option) any later

IsaFoR/CeTA is distributed in the hope that it will be useful, but WITHOUT ANY
WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A
PARTICULAR PURPOSE.  See the GNU Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public License along
with IsaFoR/CeTA. If not, see <>.
section ‹Testing Generator on Examples from AFP-Entry Datatype-Order-Generator›

theory Old_Show_Examples
subsection ‹Without Nested Recursion›

(* datatype 'a bintree = BEmpty | BNode "'a bintree" 'a "'a bintree" *)

derive "show" bintree

subsection ‹Using Other Datatypes›

(* datatype nat_list_list = NNil | CCons "nat list" nat_list_list *)

derive "show" nat_list_list

subsection ‹Explicit Mutual Recursion›

  'a mtree = MEmpty | MNode 'a "'a mtree_list" and
  'a mtree_list = MNil | MCons "'a mtree" "'a mtree_list"

derive "show" mtree

subsection ‹Implicit mutual recursion›

(*  datatype 'a tree = Empty | Node 'a "'a tree list"  *)

derive "show" tree

(* datatype 'a ttree = TEmpty | TNode 'a "'a ttree list tree" *)

derive "show" ttree

subsection ‹Examples from IsaFoR›

(* datatype ('f,'v) "term" = Var 'v | Fun 'f "('f,'v) term list" *)

derive "show" "term"

datatype ('f, 'l) lab =
  Lab "('f, 'l) lab" 'l |
  FunLab "('f, 'l) lab" "('f, 'l) lab list" |
  UnLab 'f |
  Sharp "('f, 'l) lab"

derive "show" lab

subsection ‹A Complex Datatype›

datatype ('a, 'b) complex = 
  C1 nat "'a ttree" |
  C2 "('a, 'b) complex list tree tree" 'b "('a, 'b) complex" "('a, 'b) complex2 ttree list"
and ('a, 'b) complex2 = D1 "('a, 'b) complex ttree"

datatype_compat complex complex2

derive "show" complex