--- a/ex/Simult.thy Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,82 +0,0 @@
-(* 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), M,
- Case(Split(%x y g. b(x,y,g(y))),
- List_case(%g.c, %x y g. d(x,y,g(x),g(y)))))"
-
- 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