Theory Misc_Primcorec

(*  Title:      HOL/Datatype_Examples/Misc_Primcorec.thy
    Author:     Jasmin Blanchette, TU Muenchen
    Copyright   2013

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