src/HOL/Induct/Simult.thy

Adapted to new datatype package.

(*  Title:      HOL/ex/Simult
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

A simultaneous recursive type definition: trees & forests

This is essentially the same data structure that on ex/term.ML, which is
simpler because it uses list as a new type former.  The approach in this
file may be superior for other simultaneous recursions.

The inductive definition package does not help defining this sort of mutually
recursive data structure because it uses Inl, Inr instead of In0, In1.
*)

Simult = SList +

types    'a tree
         'a forest

arities  tree,forest :: (term)term

consts
  TF          :: 'a item set => 'a item set
  FNIL        :: 'a item
  TCONS,FCONS :: ['a item, 'a item] => 'a item
  Rep_Tree    :: 'a tree => 'a item
  Abs_Tree    :: 'a item => 'a tree
  Rep_Forest  :: 'a forest => 'a item
  Abs_Forest  :: 'a item => 'a forest
  Tcons       :: ['a, 'a forest] => 'a tree
  Fcons       :: ['a tree, 'a forest] => 'a forest
  Fnil        :: 'a forest
  TF_rec      :: ['a item, ['a item , 'a item, 'b]=>'b,     
                 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b
  tree_rec    :: ['a tree, ['a, 'a forest, 'b]=>'b,          
                 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b
  forest_rec  :: ['a forest, ['a, 'a forest, 'b]=>'b,        
                  'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b

defs
     (*the concrete constants*)
  TCONS_def     "TCONS M N == In0(M $ N)"
  FNIL_def      "FNIL      == In1(NIL)"
  FCONS_def     "FCONS M N == In1(CONS M N)"
     (*the abstract constants*)
  Tcons_def     "Tcons a ts == Abs_Tree(TCONS (Leaf a) (Rep_Forest ts))"
  Fnil_def      "Fnil       == Abs_Forest(FNIL)"
  Fcons_def     "Fcons t ts == Abs_Forest(FCONS (Rep_Tree t) (Rep_Forest ts))"

  TF_def        "TF(A) == lfp(%Z. A <*> Part Z In1 
                           <+> ({Numb(0)} <+> Part Z In0 <*> Part Z In1))"

rules
  (*faking a type definition for tree...*)
  Rep_Tree         "Rep_Tree(n): Part (TF(range Leaf)) In0"
  Rep_Tree_inverse "Abs_Tree(Rep_Tree(t)) = t"
  Abs_Tree_inverse "z: Part (TF(range Leaf)) In0 ==> Rep_Tree(Abs_Tree(z)) = z"
    (*faking a type definition for forest...*)
  Rep_Forest         "Rep_Forest(n): Part (TF(range Leaf)) In1"
  Rep_Forest_inverse "Abs_Forest(Rep_Forest(ts)) = ts"
  Abs_Forest_inverse 
        "z: Part (TF(range Leaf)) In1 ==> Rep_Forest(Abs_Forest(z)) = z"


defs
     (*recursion*)
  TF_rec_def    
   "TF_rec M b c d == wfrec (trancl pred_sexp)
               (%g. Case (Split(%x y. b x y (g y))) 
                      (List_case c (%x y. d x y (g x) (g y)))) M"

  tree_rec_def
   "tree_rec t b c d == 
   TF_rec (Rep_Tree t) (%x y r. b (inv Leaf x) (Abs_Forest y) r) 
          c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"

  forest_rec_def
   "forest_rec tf b c d == 
   TF_rec (Rep_Forest tf) (%x y r. b (inv Leaf x) (Abs_Forest y) r) 
          c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"
end