src/HOL/Induct/Simult.thy
author berghofe
Fri, 24 Jul 1998 13:39:47 +0200
changeset 5191 8ceaa19f7717
parent 3120 c58423c20740
permissions -rw-r--r--
Renamed '$' to 'Scons' because of clashes with constants of the same name in theories using datatypes.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     1
(*  Title:      HOL/ex/Simult
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     2
    ID:         $Id$
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     5
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     6
A simultaneous recursive type definition: trees & forests
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     7
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     8
This is essentially the same data structure that on ex/term.ML, which is
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     9
simpler because it uses list as a new type former.  The approach in this
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    10
file may be superior for other simultaneous recursions.
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    11
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    12
The inductive definition package does not help defining this sort of mutually
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    13
recursive data structure because it uses Inl, Inr instead of In0, In1.
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    14
*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    15
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    16
Simult = SList +
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    17
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    18
types    'a tree
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    19
         'a forest
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    20
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    21
arities  tree,forest :: (term)term
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    22
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    23
consts
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    24
  TF          :: 'a item set => 'a item set
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    25
  FNIL        :: 'a item
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    26
  TCONS,FCONS :: ['a item, 'a item] => 'a item
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    27
  Rep_Tree    :: 'a tree => 'a item
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    28
  Abs_Tree    :: 'a item => 'a tree
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    29
  Rep_Forest  :: 'a forest => 'a item
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    30
  Abs_Forest  :: 'a item => 'a forest
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    31
  Tcons       :: ['a, 'a forest] => 'a tree
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    32
  Fcons       :: ['a tree, 'a forest] => 'a forest
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    33
  Fnil        :: 'a forest
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    34
  TF_rec      :: ['a item, ['a item , 'a item, 'b]=>'b,     
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    35
                 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    36
  tree_rec    :: ['a tree, ['a, 'a forest, 'b]=>'b,          
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    37
                 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    38
  forest_rec  :: ['a forest, ['a, 'a forest, 'b]=>'b,        
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    39
                  'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    40
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    41
defs
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    42
     (*the concrete constants*)
5191
8ceaa19f7717 Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents: 3120
diff changeset
    43
  TCONS_def     "TCONS M N == In0 (Scons M N)"
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    44
  FNIL_def      "FNIL      == In1(NIL)"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    45
  FCONS_def     "FCONS M N == In1(CONS M N)"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    46
     (*the abstract constants*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    47
  Tcons_def     "Tcons a ts == Abs_Tree(TCONS (Leaf a) (Rep_Forest ts))"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    48
  Fnil_def      "Fnil       == Abs_Forest(FNIL)"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    49
  Fcons_def     "Fcons t ts == Abs_Forest(FCONS (Rep_Tree t) (Rep_Forest ts))"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    50
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    51
  TF_def        "TF(A) == lfp(%Z. A <*> Part Z In1 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    52
                           <+> ({Numb(0)} <+> Part Z In0 <*> Part Z In1))"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    53
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    54
rules
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    55
  (*faking a type definition for tree...*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    56
  Rep_Tree         "Rep_Tree(n): Part (TF(range Leaf)) In0"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    57
  Rep_Tree_inverse "Abs_Tree(Rep_Tree(t)) = t"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    58
  Abs_Tree_inverse "z: Part (TF(range Leaf)) In0 ==> Rep_Tree(Abs_Tree(z)) = z"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    59
    (*faking a type definition for forest...*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    60
  Rep_Forest         "Rep_Forest(n): Part (TF(range Leaf)) In1"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    61
  Rep_Forest_inverse "Abs_Forest(Rep_Forest(ts)) = ts"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    62
  Abs_Forest_inverse 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    63
        "z: Part (TF(range Leaf)) In1 ==> Rep_Forest(Abs_Forest(z)) = z"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    64
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    65
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    66
defs
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    67
     (*recursion*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    68
  TF_rec_def    
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    69
   "TF_rec M b c d == wfrec (trancl pred_sexp)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    70
               (%g. Case (Split(%x y. b x y (g y))) 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    71
                      (List_case c (%x y. d x y (g x) (g y)))) M"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    72
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    73
  tree_rec_def
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    74
   "tree_rec t b c d == 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    75
   TF_rec (Rep_Tree t) (%x y r. b (inv Leaf x) (Abs_Forest y) r) 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    76
          c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    77
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    78
  forest_rec_def
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    79
   "forest_rec tf b c d == 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    80
   TF_rec (Rep_Forest tf) (%x y r. b (inv Leaf x) (Abs_Forest y) r) 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    81
          c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    82
end