(* 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