--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Simult.thy Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,82 @@
+(* 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