55075
|
1 |
(* Title: HOL/BNF_Examples/Misc_Primcorec.thy
|
54193
|
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, 'b, '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_pair 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> is_J21 (j2_sum n)" |
|
|
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 |
freeze_exp :: "('b \<Rightarrow> 'a) \<Rightarrow> ('a, 'b) exp \<Rightarrow> ('a, 'b) exp" and
|
|
88 |
freeze_trm :: "('b \<Rightarrow> 'a) \<Rightarrow> ('a, 'b) trm \<Rightarrow> ('a, 'b) trm" and
|
|
89 |
freeze_factor :: "('b \<Rightarrow> 'a) \<Rightarrow> ('a, 'b) factor \<Rightarrow> ('a, 'b) factor"
|
|
90 |
where
|
|
91 |
"freeze_exp g e =
|
|
92 |
(case e of
|
|
93 |
Term t \<Rightarrow> Term (freeze_trm g t)
|
|
94 |
| Sum t e \<Rightarrow> Sum (freeze_trm g t) (freeze_exp g e))" |
|
|
95 |
"freeze_trm g t =
|
|
96 |
(case t of
|
|
97 |
Factor f \<Rightarrow> Factor (freeze_factor g f)
|
|
98 |
| Prod f t \<Rightarrow> Prod (freeze_factor g f) (freeze_trm g t))" |
|
|
99 |
"freeze_factor g f =
|
|
100 |
(case f of
|
|
101 |
C a \<Rightarrow> C a
|
|
102 |
| V b \<Rightarrow> C (g b)
|
|
103 |
| Paren e \<Rightarrow> Paren (freeze_exp g e))"
|
|
104 |
|
|
105 |
primcorec poly_unity :: "'a poly_unit" where
|
|
106 |
"poly_unity = U (\<lambda>_. poly_unity)"
|
|
107 |
|
|
108 |
primcorec build_cps :: "('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> bool stream) \<Rightarrow> 'a \<Rightarrow> bool stream \<Rightarrow> 'a cps" where
|
|
109 |
"shd b \<Longrightarrow> build_cps f g a b = CPS1 a" |
|
|
110 |
"_ \<Longrightarrow> build_cps f g a b = CPS2 (\<lambda>a. build_cps f g (f a) (g a))"
|
|
111 |
|
|
112 |
end
|