Theory Misc_Primcorec

theory Misc_Primcorec
imports Misc_Codatatype
```(*  Title:      HOL/Datatype_Examples/Misc_Primcorec.thy
Author:     Jasmin Blanchette, TU Muenchen

Miscellaneous primitive corecursive function definitions.
*)

section ‹Miscellaneous Primitive Corecursive Function Definitions›

theory Misc_Primcorec
imports Misc_Codatatype
begin

primcorec simple_of_bools :: "bool ⇒ bool ⇒ simple" where
"simple_of_bools b b' = (if b then if b' then X1 else X2 else if b' then X3 else X4)"

primcorec simple'_of_bools :: "bool ⇒ bool ⇒ simple'" where
"simple'_of_bools b b' =
(if b then if b' then X1' () else X2' () else if b' then X3' () else X4' ())"

primcorec inc_simple'' :: "nat ⇒ simple'' ⇒ simple''" where
"inc_simple'' k s = (case s of X1'' n i ⇒ X1'' (n + k) (i + int k) | X2'' ⇒ X2'')"

primcorec sinterleave :: "'a stream ⇒ 'a stream ⇒ 'a stream" where
"sinterleave s s' = Stream (shd s) (sinterleave s' (stl s))"

primcorec myapp :: "'a mylist ⇒ 'a mylist ⇒ 'a mylist" where
"myapp xs ys =
(if xs = MyNil then ys
else if ys = MyNil then xs
else MyCons (myhd xs) (myapp (mytl xs) ys))"

primcorec shuffle_sp :: "('a :: ord, 'b :: ord, 'c, 'd) some_passive ⇒ ('d, 'a, 'b, 'c) some_passive" where
"shuffle_sp sp =
(case sp of
SP1 sp' ⇒ SP1 (shuffle_sp sp')
| SP2 a ⇒ SP3 a
| SP3 b ⇒ SP4 b
| SP4 c ⇒ SP5 c
| SP5 d ⇒ SP2 d)"

primcorec rename_lam :: "(string ⇒ string) ⇒ lambda ⇒ lambda" where
"rename_lam f l =
(case l of
Var s ⇒ Var (f s)
| App l l' ⇒ App (rename_lam f l) (rename_lam f l')
| Abs s l ⇒ Abs (f s) (rename_lam f l)
| Let SL l ⇒ Let (fimage (map_prod f (rename_lam f)) SL) (rename_lam f l))"

primcorec
j1_sum :: "('a::{zero,one,plus}) ⇒ 'a J1" and
j2_sum :: "'a ⇒ 'a J2"
where
"n = 0 ⟹ is_J11 (j1_sum n)" |
"un_J111 (j1_sum _) = 0" |
"un_J112 (j1_sum _) = j1_sum 0" |
"un_J121 (j1_sum n) = n + 1" |
"un_J122 (j1_sum n) = j2_sum (n + 1)" |
"n = 0 ⟹ j2_sum n = J21" |
"un_J221 (j2_sum n) = j1_sum (n + 1)" |
"un_J222 (j2_sum n) = j2_sum (n + 1)"

primcorec forest_of_mylist :: "'a tree mylist ⇒ 'a forest" where
"forest_of_mylist ts =
(case ts of
MyNil ⇒ FNil
| MyCons t ts ⇒ FCons t (forest_of_mylist ts))"

primcorec mylist_of_forest :: "'a forest ⇒ 'a tree mylist" where
"mylist_of_forest f =
(case f of
FNil ⇒ MyNil
| FCons t ts ⇒ MyCons t (mylist_of_forest ts))"

primcorec semi_stream :: "'a stream ⇒ 'a stream" where
"semi_stream s = Stream (shd s) (semi_stream (stl (stl s)))"

primcorec
tree'_of_stream :: "'a stream ⇒ 'a tree'" and
branch_of_stream :: "'a stream ⇒ 'a branch"
where
"tree'_of_stream s =
TNode' (branch_of_stream (semi_stream s)) (branch_of_stream (semi_stream (stl s)))" |
"branch_of_stream s = (case s of Stream h t ⇒ Branch h (tree'_of_stream t))"

primcorec
id_tree :: "'a bin_rose_tree ⇒ 'a bin_rose_tree" and
id_trees1 :: "'a bin_rose_tree mylist ⇒ 'a bin_rose_tree mylist" and
id_trees2 :: "'a bin_rose_tree mylist ⇒ 'a bin_rose_tree mylist"
where
"id_tree t = (case t of BRTree a ts ts' ⇒ BRTree a (id_trees1 ts) (id_trees2 ts'))" |
"id_trees1 ts = (case ts of
MyNil ⇒ MyNil
| MyCons t ts ⇒ MyCons (id_tree t) (id_trees1 ts))" |
"id_trees2 ts = (case ts of
MyNil ⇒ MyNil
| MyCons t ts ⇒ MyCons (id_tree t) (id_trees2 ts))"

primcorec
trunc_tree :: "'a bin_rose_tree ⇒ 'a bin_rose_tree" and
trunc_trees1 :: "'a bin_rose_tree mylist ⇒ 'a bin_rose_tree mylist" and
trunc_trees2 :: "'a bin_rose_tree mylist ⇒ 'a bin_rose_tree mylist"
where
"trunc_tree t = (case t of BRTree a ts ts' ⇒ BRTree a (trunc_trees1 ts) (trunc_trees2 ts'))" |
"trunc_trees1 ts = (case ts of
MyNil ⇒ MyNil
| MyCons t _ ⇒ MyCons (trunc_tree t) MyNil)" |
"trunc_trees2 ts = (case ts of
MyNil ⇒ MyNil
| MyCons t ts ⇒ MyCons (trunc_tree t) MyNil)"

primcorec
freeze_exp :: "('b ⇒ 'a) ⇒ ('a, 'b) exp ⇒ ('a, 'b) exp" and
freeze_trm :: "('b ⇒ 'a) ⇒ ('a, 'b) trm ⇒ ('a, 'b) trm" and
freeze_factor :: "('b ⇒ 'a) ⇒ ('a, 'b) factor ⇒ ('a, 'b) factor"
where
"freeze_exp g e =
(case e of
Term t ⇒ Term (freeze_trm g t)
| Sum t e ⇒ Sum (freeze_trm g t) (freeze_exp g e))" |
"freeze_trm g t =
(case t of
Factor f ⇒ Factor (freeze_factor g f)
| Prod f t ⇒ Prod (freeze_factor g f) (freeze_trm g t))" |
"freeze_factor g f =
(case f of
C a ⇒ C a
| V b ⇒ C (g b)
| Paren e ⇒ Paren (freeze_exp g e))"

primcorec poly_unity :: "'a poly_unit" where
"poly_unity = U (λ_. poly_unity)"

primcorec build_cps :: "('a ⇒ 'a) ⇒ ('a ⇒ bool stream) ⇒ 'a ⇒ bool stream ⇒ 'a cps" where
"shd b ⟹ build_cps f g a b = CPS1 a" |
"_ ⟹ build_cps f g a b = CPS2 (λa. build_cps f g (f a) (g a))"

end
```