summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Quickcheck_Narrowing.thy

changeset 65480 | 5407bc278c9a |

parent 61799 | 4cf66f21b764 |

child 65481 | b11b7ad22684 |

equal
deleted
inserted
replaced

65479:7ca8810b1d48 | 65480:5407bc278c9a |
---|---|

102 "non_empty (Narrowing_sum_of_products ps) = (\<not> (List.null ps))" |
102 "non_empty (Narrowing_sum_of_products ps) = (\<not> (List.null ps))" |

103 |
103 |

104 definition "apply" :: "('a => 'b) narrowing => 'a narrowing => 'b narrowing" |
104 definition "apply" :: "('a => 'b) narrowing => 'a narrowing => 'b narrowing" |

105 where |
105 where |

106 "apply f a d = |
106 "apply f a d = |

107 (case f d of Narrowing_cons (Narrowing_sum_of_products ps) cfs => |
107 (case f d of Narrowing_cons (Narrowing_sum_of_products ps) cfs \<Rightarrow> |

108 case a (d - 1) of Narrowing_cons ta cas => |
108 case a (d - 1) of Narrowing_cons ta cas \<Rightarrow> |

109 let |
109 let |

110 shallow = (d > 0 \<and> non_empty ta); |
110 shallow = d > 0 \<and> non_empty ta; |

111 cs = [(\<lambda>xs'. (case xs' of [] => undefined | x # xs => cf xs (conv cas x))). shallow, cf <- cfs] |
111 cs = [(\<lambda>(x # xs) \<Rightarrow> cf xs (conv cas x)). shallow, cf \<leftarrow> cfs] |

112 in Narrowing_cons (Narrowing_sum_of_products [ta # p. shallow, p <- ps]) cs)" |
112 in Narrowing_cons (Narrowing_sum_of_products [ta # p. shallow, p \<leftarrow> ps]) cs)" |

113 |
113 |

114 definition sum :: "'a narrowing => 'a narrowing => 'a narrowing" |
114 definition sum :: "'a narrowing => 'a narrowing => 'a narrowing" |

115 where |
115 where |

116 "sum a b d = |
116 "sum a b d = |

117 (case a d of Narrowing_cons (Narrowing_sum_of_products ssa) ca => |
117 (case a d of Narrowing_cons (Narrowing_sum_of_products ssa) ca => |