equal
deleted
inserted
replaced
97 where |
97 where |
98 "non_empty (Narrowing_sum_of_products ps) = (\<not> (List.null ps))" |
98 "non_empty (Narrowing_sum_of_products ps) = (\<not> (List.null ps))" |
99 |
99 |
100 definition "apply" :: "('a => 'b) narrowing => 'a narrowing => 'b narrowing" |
100 definition "apply" :: "('a => 'b) narrowing => 'a narrowing => 'b narrowing" |
101 where |
101 where |
102 "apply f a d = |
102 "apply f a d = (if d > 0 then |
103 (case f d of Narrowing_cons (Narrowing_sum_of_products ps) cfs \<Rightarrow> |
103 (case f d of Narrowing_cons (Narrowing_sum_of_products ps) cfs \<Rightarrow> |
104 case a (d - 1) of Narrowing_cons ta cas \<Rightarrow> |
104 case a (d - 1) of Narrowing_cons ta cas \<Rightarrow> |
105 let |
105 let |
106 shallow = d > 0 \<and> non_empty ta; |
106 shallow = non_empty ta; |
107 cs = [(\<lambda>(x # xs) \<Rightarrow> cf xs (conv cas x)). shallow, cf \<leftarrow> cfs] |
107 cs = [(\<lambda>(x # xs) \<Rightarrow> cf xs (conv cas x)). shallow, cf \<leftarrow> cfs] |
108 in Narrowing_cons (Narrowing_sum_of_products [ta # p. shallow, p \<leftarrow> ps]) cs)" |
108 in Narrowing_cons (Narrowing_sum_of_products [ta # p. shallow, p \<leftarrow> ps]) cs) |
|
109 else Narrowing_cons (Narrowing_sum_of_products []) [])" |
109 |
110 |
110 definition sum :: "'a narrowing => 'a narrowing => 'a narrowing" |
111 definition sum :: "'a narrowing => 'a narrowing => 'a narrowing" |
111 where |
112 where |
112 "sum a b d = |
113 "sum a b d = |
113 (case a d of Narrowing_cons (Narrowing_sum_of_products ssa) ca => |
114 (case a d of Narrowing_cons (Narrowing_sum_of_products ssa) ca => |