56 codata ('a, 'b, 'c) some_killing = |
56 codata ('a, 'b, 'c) some_killing = |
57 SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here" |
57 SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here" |
58 and ('a, 'b, 'c) in_here = |
58 and ('a, 'b, 'c) in_here = |
59 IH1 'b 'a | IH2 'c |
59 IH1 'b 'a | IH2 'c |
60 |
60 |
61 codata_raw some_killing': 'a = "'b \<Rightarrow> 'd \<Rightarrow> ('a + 'c)" |
61 codata ('a, 'b, 'c) some_killing' = |
62 and in_here': 'c = "'d + 'e" |
62 SK' "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing' + ('a, 'b, 'c) in_here'" |
|
63 and ('a, 'b, 'c) in_here' = |
|
64 IH1' 'b | IH2' 'c |
63 |
65 |
64 codata_raw some_killing'': 'a = "'b \<Rightarrow> 'c" |
66 codata ('a, 'b, 'c) some_killing'' = |
65 and in_here'': 'c = "'d \<times> 'b + 'e" |
67 SK'' "'a \<Rightarrow> ('a, 'b, 'c) in_here''" |
|
68 and ('a, 'b, 'c) in_here'' = |
|
69 IH1'' 'b 'a | IH2'' 'c |
66 |
70 |
67 codata ('b, 'c) less_killing = LK "'b \<Rightarrow> 'c" |
71 codata ('b, 'c) less_killing = LK "'b \<Rightarrow> 'c" |
68 |
72 |
69 codata 'b cps = CPS1 'b | CPS2 "'b \<Rightarrow> 'b cps" |
73 codata 'b cps = CPS1 'b | CPS2 "'b \<Rightarrow> 'b cps" |
70 |
74 |