src/HOL/Datatype_Examples/Misc_Primcorec.thy
 author haftmann Fri Oct 10 19:55:32 2014 +0200 (2014-10-10) changeset 58646 cd63a4b12a33 parent 58309 a09ec6daaa19 child 58889 5b7a9633cfa8 permissions -rw-r--r--
specialized specification: avoid trivial instances
```     1 (*  Title:      HOL/Datatype_Examples/Misc_Primcorec.thy
```
```     2     Author:     Jasmin Blanchette, TU Muenchen
```
```     3     Copyright   2013
```
```     4
```
```     5 Miscellaneous primitive corecursive function definitions.
```
```     6 *)
```
```     7
```
```     8 header {* Miscellaneous Primitive Corecursive Function Definitions *}
```
```     9
```
```    10 theory Misc_Primcorec
```
```    11 imports Misc_Codatatype
```
```    12 begin
```
```    13
```
```    14 primcorec simple_of_bools :: "bool \<Rightarrow> bool \<Rightarrow> simple" where
```
```    15   "simple_of_bools b b' = (if b then if b' then X1 else X2 else if b' then X3 else X4)"
```
```    16
```
```    17 primcorec simple'_of_bools :: "bool \<Rightarrow> bool \<Rightarrow> simple'" where
```
```    18   "simple'_of_bools b b' =
```
```    19      (if b then if b' then X1' () else X2' () else if b' then X3' () else X4' ())"
```
```    20
```
```    21 primcorec inc_simple'' :: "nat \<Rightarrow> simple'' \<Rightarrow> simple''" where
```
```    22   "inc_simple'' k s = (case s of X1'' n i \<Rightarrow> X1'' (n + k) (i + int k) | X2'' \<Rightarrow> X2'')"
```
```    23
```
```    24 primcorec sinterleave :: "'a stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where
```
```    25   "sinterleave s s' = Stream (shd s) (sinterleave s' (stl s))"
```
```    26
```
```    27 primcorec myapp :: "'a mylist \<Rightarrow> 'a mylist \<Rightarrow> 'a mylist" where
```
```    28   "myapp xs ys =
```
```    29      (if xs = MyNil then ys
```
```    30       else if ys = MyNil then xs
```
```    31       else MyCons (myhd xs) (myapp (mytl xs) ys))"
```
```    32
```
```    33 primcorec shuffle_sp :: "('a \<Colon> ord, 'b \<Colon> ord, 'c, 'd) some_passive \<Rightarrow> ('d, 'a, 'b, 'c) some_passive" where
```
```    34   "shuffle_sp sp =
```
```    35      (case sp of
```
```    36        SP1 sp' \<Rightarrow> SP1 (shuffle_sp sp')
```
```    37      | SP2 a \<Rightarrow> SP3 a
```
```    38      | SP3 b \<Rightarrow> SP4 b
```
```    39      | SP4 c \<Rightarrow> SP5 c
```
```    40      | SP5 d \<Rightarrow> SP2 d)"
```
```    41
```
```    42 primcorec rename_lam :: "(string \<Rightarrow> string) \<Rightarrow> lambda \<Rightarrow> lambda" where
```
```    43   "rename_lam f l =
```
```    44      (case l of
```
```    45        Var s \<Rightarrow> Var (f s)
```
```    46      | App l l' \<Rightarrow> App (rename_lam f l) (rename_lam f l')
```
```    47      | Abs s l \<Rightarrow> Abs (f s) (rename_lam f l)
```
```    48      | Let SL l \<Rightarrow> Let (fimage (map_prod f (rename_lam f)) SL) (rename_lam f l))"
```
```    49
```
```    50 primcorec
```
```    51   j1_sum :: "('a\<Colon>{zero,one,plus}) \<Rightarrow> 'a J1" and
```
```    52   j2_sum :: "'a \<Rightarrow> 'a J2"
```
```    53 where
```
```    54   "n = 0 \<Longrightarrow> is_J11 (j1_sum n)" |
```
```    55   "un_J111 (j1_sum _) = 0" |
```
```    56   "un_J112 (j1_sum _) = j1_sum 0" |
```
```    57   "un_J121 (j1_sum n) = n + 1" |
```
```    58   "un_J122 (j1_sum n) = j2_sum (n + 1)" |
```
```    59   "n = 0 \<Longrightarrow> j2_sum n = J21" |
```
```    60   "un_J221 (j2_sum n) = j1_sum (n + 1)" |
```
```    61   "un_J222 (j2_sum n) = j2_sum (n + 1)"
```
```    62
```
```    63 primcorec forest_of_mylist :: "'a tree mylist \<Rightarrow> 'a forest" where
```
```    64   "forest_of_mylist ts =
```
```    65      (case ts of
```
```    66        MyNil \<Rightarrow> FNil
```
```    67      | MyCons t ts \<Rightarrow> FCons t (forest_of_mylist ts))"
```
```    68
```
```    69 primcorec mylist_of_forest :: "'a forest \<Rightarrow> 'a tree mylist" where
```
```    70   "mylist_of_forest f =
```
```    71      (case f of
```
```    72        FNil \<Rightarrow> MyNil
```
```    73      | FCons t ts \<Rightarrow> MyCons t (mylist_of_forest ts))"
```
```    74
```
```    75 primcorec semi_stream :: "'a stream \<Rightarrow> 'a stream" where
```
```    76   "semi_stream s = Stream (shd s) (semi_stream (stl (stl s)))"
```
```    77
```
```    78 primcorec
```
```    79   tree'_of_stream :: "'a stream \<Rightarrow> 'a tree'" and
```
```    80   branch_of_stream :: "'a stream \<Rightarrow> 'a branch"
```
```    81 where
```
```    82   "tree'_of_stream s =
```
```    83      TNode' (branch_of_stream (semi_stream s)) (branch_of_stream (semi_stream (stl s)))" |
```
```    84   "branch_of_stream s = (case s of Stream h t \<Rightarrow> Branch h (tree'_of_stream t))"
```
```    85
```
```    86 primcorec
```
```    87   id_tree :: "'a bin_rose_tree \<Rightarrow> 'a bin_rose_tree" and
```
```    88   id_trees1 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist" and
```
```    89   id_trees2 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist"
```
```    90 where
```
```    91   "id_tree t = (case t of BRTree a ts ts' \<Rightarrow> BRTree a (id_trees1 ts) (id_trees2 ts'))" |
```
```    92   "id_trees1 ts = (case ts of
```
```    93        MyNil \<Rightarrow> MyNil
```
```    94      | MyCons t ts \<Rightarrow> MyCons (id_tree t) (id_trees1 ts))" |
```
```    95   "id_trees2 ts = (case ts of
```
```    96        MyNil \<Rightarrow> MyNil
```
```    97      | MyCons t ts \<Rightarrow> MyCons (id_tree t) (id_trees2 ts))"
```
```    98
```
```    99 primcorec
```
```   100   trunc_tree :: "'a bin_rose_tree \<Rightarrow> 'a bin_rose_tree" and
```
```   101   trunc_trees1 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist" and
```
```   102   trunc_trees2 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist"
```
```   103 where
```
```   104   "trunc_tree t = (case t of BRTree a ts ts' \<Rightarrow> BRTree a (trunc_trees1 ts) (trunc_trees2 ts'))" |
```
```   105   "trunc_trees1 ts = (case ts of
```
```   106        MyNil \<Rightarrow> MyNil
```
```   107      | MyCons t _ \<Rightarrow> MyCons (trunc_tree t) MyNil)" |
```
```   108   "trunc_trees2 ts = (case ts of
```
```   109        MyNil \<Rightarrow> MyNil
```
```   110      | MyCons t ts \<Rightarrow> MyCons (trunc_tree t) MyNil)"
```
```   111
```
```   112 primcorec
```
```   113   freeze_exp :: "('b \<Rightarrow> 'a) \<Rightarrow> ('a, 'b) exp \<Rightarrow> ('a, 'b) exp" and
```
```   114   freeze_trm :: "('b \<Rightarrow> 'a) \<Rightarrow> ('a, 'b) trm \<Rightarrow> ('a, 'b) trm" and
```
```   115   freeze_factor :: "('b \<Rightarrow> 'a) \<Rightarrow> ('a, 'b) factor \<Rightarrow> ('a, 'b) factor"
```
```   116 where
```
```   117   "freeze_exp g e =
```
```   118      (case e of
```
```   119        Term t \<Rightarrow> Term (freeze_trm g t)
```
```   120      | Sum t e \<Rightarrow> Sum (freeze_trm g t) (freeze_exp g e))" |
```
```   121   "freeze_trm g t =
```
```   122      (case t of
```
```   123        Factor f \<Rightarrow> Factor (freeze_factor g f)
```
```   124      | Prod f t \<Rightarrow> Prod (freeze_factor g f) (freeze_trm g t))" |
```
```   125   "freeze_factor g f =
```
```   126      (case f of
```
```   127        C a \<Rightarrow> C a
```
```   128      | V b \<Rightarrow> C (g b)
```
```   129      | Paren e \<Rightarrow> Paren (freeze_exp g e))"
```
```   130
```
```   131 primcorec poly_unity :: "'a poly_unit" where
```
```   132   "poly_unity = U (\<lambda>_. poly_unity)"
```
```   133
```
```   134 primcorec build_cps :: "('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> bool stream) \<Rightarrow> 'a \<Rightarrow> bool stream \<Rightarrow> 'a cps" where
```
```   135   "shd b \<Longrightarrow> build_cps f g a b = CPS1 a" |
```
```   136   "_ \<Longrightarrow> build_cps f g a b = CPS2 (\<lambda>a. build_cps f g (f a) (g a))"
```
```   137
```
```   138 end
```