10 |
10 |
11 theory Misc_Codata |
11 theory Misc_Codata |
12 imports "../Codatatype" |
12 imports "../Codatatype" |
13 begin |
13 begin |
14 |
14 |
15 codata_raw simple: 'a = "unit + unit + unit + unit" |
15 codata simple = X1 | X2 | X3 | X4 |
16 |
16 |
17 codata_raw stream: 's = "'a \<times> 's" |
17 codata simple' = X1' unit | X2' unit | X3' unit | X4' unit |
18 |
18 |
19 codata_raw llist: 'llist = "unit + 'a \<times> 'llist" |
19 codata 'a stream = Stream 'a "'a stream" |
20 |
20 |
21 codata_raw some_passive: 'a = "'a + 'b + 'c + 'd + 'e" |
21 codata 'a mylist = MyNil | MyCons 'a "'a mylist" |
|
22 |
|
23 codata ('b, 'c, 'd, 'e) some_passive = |
|
24 SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e |
|
25 |
|
26 codata lambda = |
|
27 Var string | |
|
28 App lambda lambda | |
|
29 Abs string lambda | |
|
30 Let "(string \<times> lambda) fset" lambda |
|
31 |
|
32 codata 'a par_lambda = |
|
33 PVar 'a | |
|
34 PApp "'a par_lambda" "'a par_lambda" | |
|
35 PAbs 'a "'a par_lambda" | |
|
36 PLet "('a \<times> 'a par_lambda) fset" "'a par_lambda" |
22 |
37 |
23 (* |
38 (* |
24 ('a, 'b1, 'b2) F1 = 'a * 'b1 + 'a * 'b2 |
39 ('a, 'b1, 'b2) F1 = 'a * 'b1 + 'a * 'b2 |
25 ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2 |
40 ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2 |
26 *) |
41 *) |
27 |
42 |
28 codata_raw F1: 'b1 = "'a \<times> 'b1 + 'a \<times> 'b2" |
43 codata 'a J1 = J11 'a "'a J1" | J12 'a "'a J2" |
29 and F2: 'b2 = "unit + 'b1 * 'b2" |
44 and 'a J2 = J21 | J22 "'a J1" "'a J2" |
30 |
45 |
31 codata_raw EXPR: 'E = "'T + 'T \<times> 'E" |
46 codata 'a tree = TEmpty | TNode 'a "'a forest" |
32 and TERM: 'T = "'F + 'F \<times> 'T" |
47 and 'a forest = FNil | FCons "'a tree" "'a forest" |
33 and FACTOR: 'F = "'a + 'b + 'E" |
|
34 |
48 |
35 codata_raw llambda: |
49 codata 'a tree' = TEmpty' | TNode' "'a branch" "'a branch" |
36 'trm = "string + |
50 and 'a branch = Branch 'a "'a tree'" |
37 'trm \<times> 'trm + |
|
38 string \<times> 'trm + |
|
39 (string \<times> 'trm) fset \<times> 'trm" |
|
40 |
51 |
41 codata_raw par_llambda: |
52 codata ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp" |
42 'trm = "'a + |
53 and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm" |
43 'trm \<times> 'trm + |
54 and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp" |
44 'a \<times> 'trm + |
|
45 ('a \<times> 'trm) fset \<times> 'trm" |
|
46 |
55 |
47 (* |
56 codata_raw some_killing: 'A = "'a \<Rightarrow> 'b \<Rightarrow> ('A + 'B)" |
48 'a tree = Empty | Node of 'a * 'a forest ('b = unit + 'a * 'c) |
57 and in_here: 'B = "'b \<times> 'a + 'c" |
49 'a forest = Nil | Cons of 'a tree * 'a forest ('c = unit + 'b * 'c) |
58 |
|
59 (* FIXME |
|
60 codata ('a, 'b, 'c) some_killing = |
|
61 SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here" |
|
62 and ('a, 'b, 'c) in_here = |
|
63 IH1 'b 'a | IH2 'c |
50 *) |
64 *) |
51 |
|
52 codata_raw tree: 'tree = "unit + 'a \<times> 'forest" |
|
53 and forest: 'forest = "unit + 'tree \<times> 'forest" |
|
54 |
|
55 codata_raw CPS: 'a = "'b + 'b \<Rightarrow> 'a" |
|
56 |
|
57 codata_raw fun_rhs: 'a = "'b1 \<Rightarrow> 'b2 \<Rightarrow> 'b3 \<Rightarrow> 'b4 \<Rightarrow> 'b5 \<Rightarrow> 'b6 \<Rightarrow> 'b7 \<Rightarrow> 'b8 \<Rightarrow> 'b9 \<Rightarrow> 'a" |
|
58 |
|
59 codata_raw fun_rhs': 'a = "'b1 \<Rightarrow> 'b2 \<Rightarrow> 'b3 \<Rightarrow> 'b4 \<Rightarrow> 'b5 \<Rightarrow> 'b6 \<Rightarrow> 'b7 \<Rightarrow> 'b8 \<Rightarrow> 'b9 \<Rightarrow> 'b10 \<Rightarrow> |
|
60 'b11 \<Rightarrow> 'b12 \<Rightarrow> 'b13 \<Rightarrow> 'b14 \<Rightarrow> 'b15 \<Rightarrow> 'b16 \<Rightarrow> 'b17 \<Rightarrow> 'b18 \<Rightarrow> 'b19 \<Rightarrow> 'b20 \<Rightarrow> 'a" |
|
61 |
|
62 codata_raw some_killing: 'a = "'b \<Rightarrow> 'd \<Rightarrow> ('a + 'c)" |
|
63 and in_here: 'c = "'d \<times> 'b + 'e" |
|
64 |
65 |
65 codata_raw some_killing': 'a = "'b \<Rightarrow> 'd \<Rightarrow> ('a + 'c)" |
66 codata_raw some_killing': 'a = "'b \<Rightarrow> 'd \<Rightarrow> ('a + 'c)" |
66 and in_here': 'c = "'d + 'e" |
67 and in_here': 'c = "'d + 'e" |
67 |
68 |
68 codata_raw some_killing'': 'a = "'b \<Rightarrow> 'c" |
69 codata_raw some_killing'': 'a = "'b \<Rightarrow> 'c" |
69 and in_here'': 'c = "'d \<times> 'b + 'e" |
70 and in_here'': 'c = "'d \<times> 'b + 'e" |
70 |
71 |
71 codata_raw less_killing: 'a = "'b \<Rightarrow> 'c" |
72 codata_raw less_killing: 'a = "'b \<Rightarrow> 'c" |
72 |
73 |
73 codata_raw |
74 codata 'b cps = CPS1 'b | CPS2 "'b \<Rightarrow> 'b cps" |
74 wit3_F1: 'b1 = "'a1 \<times> 'b1 \<times> 'b2" |
|
75 and wit3_F2: 'b2 = "'a2 \<times> 'b2" |
|
76 and wit3_F3: 'b3 = "'a1 \<times> 'a2 \<times> 'b1 + 'a3 \<times> 'a1 \<times> 'a2 \<times> 'b1" |
|
77 |
75 |
78 codata_raw |
76 codata ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9) fun_rhs = |
79 coind_wit1: 'a = "'c \<times> 'a \<times> 'b \<times> 'd" |
77 FR "'b1 \<Rightarrow> 'b2 \<Rightarrow> 'b3 \<Rightarrow> 'b4 \<Rightarrow> 'b5 \<Rightarrow> 'b6 \<Rightarrow> 'b7 \<Rightarrow> 'b8 \<Rightarrow> 'b9 \<Rightarrow> |
80 and coind_wit2: 'd = "'d \<times> 'e + 'c \<times> 'g" |
78 ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9) fun_rhs" |
81 and ind_wit: 'b = "unit + 'c" |
79 |
|
80 codata ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9, 'b10, 'b11, 'b12, 'b13, 'b14, 'b15, 'b16, 'b17, |
|
81 'b18, 'b19, 'b20) fun_rhs' = |
|
82 FR' "'b1 \<Rightarrow> 'b2 \<Rightarrow> 'b3 \<Rightarrow> 'b4 \<Rightarrow> 'b5 \<Rightarrow> 'b6 \<Rightarrow> 'b7 \<Rightarrow> 'b8 \<Rightarrow> 'b9 \<Rightarrow> 'b10 \<Rightarrow> 'b11 \<Rightarrow> 'b12 \<Rightarrow> 'b13 \<Rightarrow> 'b14 \<Rightarrow> |
|
83 'b15 \<Rightarrow> 'b16 \<Rightarrow> 'b17 \<Rightarrow> 'b18 \<Rightarrow> 'b19 \<Rightarrow> 'b20 \<Rightarrow> |
|
84 ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9, 'b10, 'b11, 'b12, 'b13, 'b14, 'b15, 'b16, 'b17, |
|
85 'b18, 'b19, 'b20) fun_rhs'" |
|
86 |
|
87 codata ('a, 'b, 'c) wit3_F1 = W1 'a "('a, 'b, 'c) wit3_F1" "('a, 'b, 'c) wit3_F2" |
|
88 and ('a, 'b, 'c) wit3_F2 = W2 'b "('a, 'b, 'c) wit3_F2" |
|
89 and ('a, 'b, 'c) wit3_F3 = W31 'a 'b "('a, 'b, 'c) wit3_F1" | W32 'c 'a 'b "('a, 'b, 'c) wit3_F1" |
|
90 |
|
91 codata ('c, 'e, 'g) coind_wit1 = |
|
92 CW1 'c "('c, 'e, 'g) coind_wit1" "('c, 'e, 'g) ind_wit" "('c, 'e, 'g) coind_wit2" |
|
93 and ('c, 'e, 'g) coind_wit2 = |
|
94 CW21 "('c, 'e, 'g) coind_wit2" 'e | CW22 'c 'g |
|
95 and ('c, 'e, 'g) ind_wit = |
|
96 IW1 | IW2 'c |
82 |
97 |
83 (* SLOW, MEMORY-HUNGRY |
98 (* SLOW, MEMORY-HUNGRY |
84 codata_raw K1': 'K1 = "'K2 + 'a list" |
99 codata ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list" |
85 and K2': 'K2 = "'K3 + 'c fset" |
100 and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list" |
86 and K3': 'K3 = "'K3 + 'K4 + 'K4 \<times> 'K5" |
101 and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5" |
87 and K4': 'K4 = "'K5 + 'a list list list" |
102 and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list" |
88 and K5': 'K5 = "'K6" |
103 and ('a, 'c) D5 = A5 "('a, 'c) D6" |
89 and K6': 'K6 = "'K7" |
104 and ('a, 'c) D6 = A6 "('a, 'c) D7" |
90 and K7': 'K7 = "'K8" |
105 and ('a, 'c) D7 = A7 "('a, 'c) D8" |
91 and K8': 'K8 = "'K1 list" |
106 and ('a, 'c) D8 = A8 "('a, 'c) D1 list" |
92 *) |
107 *) |
93 |
108 |
94 end |
109 end |