1 (* Title: HOL/BNF_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 |
|