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